Merge pull request #5791 from diffblue/smt2-uf

SMT2 uninterpreted functions

Author: kroening

regression/cbmc/uninterpreted_function/uf2.c

@@ -1,4 +1,5 @@
 int __CPROVER_uninterpreted_f(int, int);
+__CPROVER_bool __CPROVER_uninterpreted_g(int, int);
 
 main()
 {
@@ -8,5 +9,11 @@ main()
   int inst2 = __CPROVER_uninterpreted_f(1, b);
 
   if(a == b)
-    __CPROVER_assert(inst1 == inst2, "functional consistency");
+    __CPROVER_assert(inst1 == inst2, "functional consistency for f");
+
+  int inst3 = __CPROVER_uninterpreted_g(1, a);
+  int inst4 = __CPROVER_uninterpreted_g(1, b);
+
+  if(a == b)
+    __CPROVER_assert(inst3 == inst4, "functional consistency for g");
 }

regression/smt2_solver/uninterpreted-functions/boolean_uf1.desc

@@ -0,0 +1,7 @@
+CORE
+boolean_uf1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/uninterpreted-functions/boolean_uf1.smt2

@@ -0,0 +1,11 @@
+(set-logic QF_UFBV)
+
+(declare-fun myfun ((_ BitVec 32)) Bool)
+
+(assert (myfun (_ bv10 32)))
+
+(declare-const x (_ BitVec 32))
+(assert (= x (_ bv10 32)))
+(assert (not (myfun x)))
+
+(check-sat)

regression/smt2_solver/uninterpreted-functions/uf1.desc

@@ -0,0 +1,7 @@
+CORE
+uf1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/uninterpreted-functions/uf1.smt2

@@ -0,0 +1,11 @@
+(set-logic QF_UFBV)
+
+(declare-fun myfun ((_ BitVec 32)) (_ BitVec 32))
+
+(assert (= (myfun (_ bv10 32)) (_ bv20 32)))
+
+(declare-const x (_ BitVec 32))
+(assert (= x (_ bv10 32)))
+(assert (= (myfun x) (_ bv30 32)))
+
+(check-sat)

src/solvers/flattening/boolbv.cpp

@@ -565,6 +565,11 @@ literalt boolbvt::convert_rest(const exprt &expr)
     else if(op.type().id() == ID_fixedbv)
       return const_literal(true);
   }
+  else if(expr.id() == ID_function_application)
+  {
+    functions.record(to_function_application_expr(expr));
+    return prop.new_variable();
+  }
 
   return SUB::convert_rest(expr);
 }

src/solvers/smt2/smt2_parser.cpp

@@ -1223,19 +1223,8 @@ typet smt2_parsert::function_signature_declaration()
   mathematical_function_typet::domaint domain;
 
   while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
-  {
-    if(next_token() != smt2_tokenizert::OPEN)
-      throw error("expected '(' at beginning of parameter");
-
-    if(next_token() != smt2_tokenizert::SYMBOL)
-      throw error("expected symbol in parameter");
-
     domain.push_back(sort());
 
-    if(next_token() != smt2_tokenizert::CLOSE)
-      throw error("expected ')' at end of parameter");
-  }
-
   next_token(); // eat the ')'
 
   typet codomain = sort();

src/solvers/smt2/smt2_solver.cpp

@@ -102,18 +102,22 @@ void smt2_solvert::expand_function_applications(exprt &expr)
           domain.size() == app.arguments().size(),
           "number of parameters must match number of arguments");
 
-        replace_symbolt replace_symbol;
-
-        for(std::size_t i = 0; i < domain.size(); i++)
+        // Does it have a definition? It's otherwise uninterpreted.
+        if(!f.definition.is_nil())
         {
-          replace_symbol.insert(
-            symbol_exprt(f.parameters[i], domain[i]), app.arguments()[i]);
+          replace_symbolt replace_symbol;
+
+          for(std::size_t i = 0; i < domain.size(); i++)
+          {
+            replace_symbol.insert(
+              symbol_exprt(f.parameters[i], domain[i]), app.arguments()[i]);
+          }
+
+          exprt body = f.definition;
+          replace_symbol(body);
+          expand_function_applications(body);
+          expr = body;
         }
-
-        exprt body = f.definition;
-        replace_symbol(body);
-        expand_function_applications(body);
-        expr = body;
       }
     }
   }