uninterpreted functions with Boolean codomain

This adds support for uninterpreted functions that have a Boolean codomain.

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)

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);
 }