Merge pull request #4661 from diffblue/smt2_arguments_check

smt2 frontend: check the number of types of function arguments

Author: tautschnig

regression/smt2_solver/function-applications/function-application3.desc

@@ -0,0 +1,7 @@
+CORE
+function-application3.smt2
+
+^EXIT=20$
+^SIGNAL=0$
+^\(error "line 4: wrong number of arguments for function"\)$
+--

regression/smt2_solver/function-applications/function-application3.smt2

@@ -0,0 +1,6 @@
+(set-logic LIA)
+
+(define-fun next ((x Int)) Int x )
+(assert (= (next ) 243))
+
+(check-sat)

src/solvers/smt2/smt2_parser.cpp

@@ -291,26 +291,22 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
 }
 
 exprt smt2_parsert::function_application(
-  const irep_idt &,
-  const exprt::operandst &)
+  const symbol_exprt &function,
+  const exprt::operandst &op)
 {
-  #if 0
-  const auto &f = id_map[identifier];
+  const auto &function_type = to_mathematical_function_type(function.type());
 
   // check the arguments
-  if(op.size()!=f.type.variables().size())
+  if(op.size() != function_type.domain().size())
     throw error("wrong number of arguments for function");
 
   for(std::size_t i=0; i<op.size(); i++)
   {
-    if(op[i].type() != f.type.variables()[i].type())
+    if(op[i].type() != function_type.domain()[i])
       throw error("wrong type for arguments for function");
   }
 
-  return function_application_exprt(
-    symbol_exprt(identifier, f.type), op, f.type.range());
-  #endif
-  return nil_exprt();
+  return function_application_exprt(function, op);
 }
 
 exprt::operandst smt2_parsert::cast_bv_to_signed(const exprt::operandst &op)
@@ -826,7 +822,7 @@ exprt smt2_parsert::function_application()
         {
           if(id_it->second.type.id()==ID_mathematical_function)
           {
-            return function_application_exprt(
+            return function_application(
               symbol_exprt(final_id, id_it->second.type), op);
           }
           else

src/solvers/smt2/smt2_parser.h

@@ -136,7 +136,7 @@ class smt2_parsert
   exprt let_expression();
   exprt quantifier_expression(irep_idt);
   exprt function_application(
-    const irep_idt &identifier,
+    const symbol_exprt &function,
     const exprt::operandst &op);
 
   /// Apply typecast to signedbv to expressions in vector