SMT2 backend: workaround for Z3 get-value limitation

Z3 refuses to provide values for defined functions whose definition includes
a quantifier.  This commit works around this limitation by replacing
define-fun by equivalent declare-fun and assert commands.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -789,6 +789,16 @@ void smt2_convt::convert_address_of_rec(
         expr.id_string());
 }
 
+static bool has_quantifier(const exprt &expr)
+{
+  bool result = false;
+  expr.visit_post([&result](const exprt &node) {
+    if(node.id() == ID_exists || node.id() == ID_forall)
+      result = true;
+  });
+  return result;
+}
+
 literalt smt2_convt::convert(const exprt &expr)
 {
   PRECONDITION(expr.type().id() == ID_bool);
@@ -818,13 +828,28 @@ literalt smt2_convt::convert(const exprt &expr)
   // store and in future we use the literal instead of the whole expression
   // Note that here we are always converting, so we do not need to consider
   // other literal kinds, only "|B###|"
-  defined_expressions[expr] =
-    std::string{"|B"} + std::to_string(l.var_no()) + "|";
-  out << "(define-fun ";
-  convert_literal(l);
-  out << " () Bool ";
-  convert_expr(prepared_expr);
-  out << ")" << "\n";
+
+  // Z3 refuses get-value when a defined symbol contains a quantifier.
+  if(has_quantifier(prepared_expr))
+  {
+    out << "(declare-fun ";
+    convert_literal(l);
+    out << " () Bool)\n";
+    out << "(assert (= ";
+    convert_literal(l);
+    convert_expr(prepared_expr);
+    out << "))\n";
+  }
+  else
+  {
+    defined_expressions[expr] =
+      std::string{"|B"} + std::to_string(l.var_no()) + "|";
+    out << "(define-fun ";
+    convert_literal(l);
+    out << " () Bool ";
+    convert_expr(prepared_expr);
+    out << ")\n";
+  }
 
   return l;
 }

src/solvers/smt2/smt2_dec.cpp

@@ -184,24 +184,10 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
       if(res != resultt::D_UNSATISFIABLE)
       {
         const auto &message = id2string(parsed.get_sub()[1].id());
-        // Special case error handling
-        if(
-          solver == solvert::Z3 &&
-          message.find("must not contain quantifiers") != std::string::npos)
-        {
-          // We tried to "(get-value |XXXX|)" where |XXXX| is determined to
-          // include a quantified expression
-          // Nothing to do, this should be caught and value assigned by the
-          // set_to defaults later.
-        }
-        // Unhandled error, log the error and report it back up to caller
-        else
-        {
-          messaget log{message_handler};
-          log.error() << "SMT2 solver returned error message:\n"
-                      << "\t\"" << message << "\"" << messaget::eom;
-          return decision_proceduret::resultt::D_ERROR;
-        }
+        messaget log{message_handler};
+        log.error() << "SMT2 solver returned error message:\n"
+                    << "\t\"" << message << "\"" << messaget::eom;
+        return decision_proceduret::resultt::D_ERROR;
       }
     }
   }