From a8e67cbc118b52d9776b3e7d58a2bc2fdc13a9b8 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Mon, 4 Mar 2019 11:29:22 +0000
Subject: [PATCH] use a tuple for function arguments

This is follow-up from PR #4317.

This introduces tuple_exprt.

function_application_exprt now uses tuple_exprt for the argument operand,
instead of an expression with empty ID.
---
 src/util/irep_ids.def          |  1 +
 src/util/mathematical_expr.cpp |  2 +-
 src/util/mathematical_expr.h   | 16 ++++++++++++++--
 3 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index a07b4a25c83..bf8dda518a3 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -720,6 +720,7 @@ IREP_ID_ONE(typeid)
 IREP_ID_TWO(C_quoted, #quoted)
 IREP_ID_ONE(to_member)
 IREP_ID_ONE(pointer_to_member)
+IREP_ID_ONE(tuple)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree
diff --git a/src/util/mathematical_expr.cpp b/src/util/mathematical_expr.cpp
index 062226e3816..bffacefd9e6 100644
--- a/src/util/mathematical_expr.cpp
+++ b/src/util/mathematical_expr.cpp
@@ -15,7 +15,7 @@ function_application_exprt::function_application_exprt(
   : binary_exprt(
       _function,
       ID_function_application,
-      multi_ary_exprt(irep_idt(), std::move(_arguments), typet()),
+      tuple_exprt(std::move(_arguments)),
       to_mathematical_function_type(_function.type()).codomain())
 {
   const auto &domain = to_mathematical_function_type(_function.type()).domain();
diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h
index de8bcde3427..ea793dd4ee3 100644
--- a/src/util/mathematical_expr.h
+++ b/src/util/mathematical_expr.h
@@ -186,6 +186,15 @@ inline void validate_expr(const factorial_power_exprt &value)
   validate_operands(value, 2, "Factorial power must have two operands");
 }
 
+class tuple_exprt : public multi_ary_exprt
+{
+public:
+  explicit tuple_exprt(exprt::operandst operands)
+    : multi_ary_exprt(ID_tuple, std::move(operands), typet())
+  {
+  }
+};
+
 /// \brief Application of (mathematical) function
 class function_application_exprt : public binary_exprt
 {
@@ -197,9 +206,12 @@ class function_application_exprt : public binary_exprt
     const symbol_exprt &_function,
     const argumentst &_arguments,
     const typet &_type)
-    : binary_exprt(_function, ID_function_application, exprt(), _type)
+    : binary_exprt(
+        _function,
+        ID_function_application,
+        tuple_exprt(_arguments),
+        _type)
   {
-    arguments() = _arguments;
   }
 
   function_application_exprt(