new constructor for function_application_exprt

The new constructor
1) moves the arguments
2) enforces the type of the function to be mathematical_function
3) automatically sets the type of the application to be the codomain of the
function.
4) checks that the right number of arguments is given.

Note that the function symbol can't be moved during construction as its type
is needed.  The types of the arguments are not checked.

Author: Daniel Kroening

src/solvers/smt2/smt2_parser.cpp

@@ -818,10 +818,7 @@ exprt smt2_parsert::function_application()
           if(id_it->second.type.id()==ID_mathematical_function)
           {
             return function_application_exprt(
-              symbol_exprt(final_id, id_it->second.type),
-              op,
-              to_mathematical_function_type(
-                id_it->second.type).codomain());
+              symbol_exprt(final_id, id_it->second.type), op);
           }
           else
             return symbol_exprt(final_id, id_it->second.type);

src/util/mathematical_expr.cpp

@@ -7,3 +7,17 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "mathematical_expr.h"
+#include "mathematical_types.h"
+
+function_application_exprt::function_application_exprt(
+  const symbol_exprt &_function,
+  argumentst _arguments)
+  : binary_exprt(
+      _function,
+      ID_function_application,
+      multi_ary_exprt(irep_idt(), std::move(_arguments), typet()),
+      to_mathematical_function_type(_function.type()).codomain())
+{
+  const auto &domain = to_mathematical_function_type(_function.type()).domain();
+  PRECONDITION(domain.size() == arguments().size());
+}

src/util/mathematical_expr.h

@@ -192,6 +192,7 @@ class function_application_exprt : public binary_exprt
 public:
   using argumentst = exprt::operandst;
 
+  DEPRECATED("use function_application_exprt(fkt, arg) instead")
   function_application_exprt(
     const symbol_exprt &_function,
     const argumentst &_arguments,
@@ -201,6 +202,10 @@ class function_application_exprt : public binary_exprt
     arguments() = _arguments;
   }
 
+  function_application_exprt(
+    const symbol_exprt &_function,
+    argumentst _arguments);
+
   symbol_exprt &function()
   {
     return static_cast<symbol_exprt &>(op0());