Work around Z3 not producing models for some quantified expressions

Until the Z3 bug-fix (see Z3Prover/z3#7743) is available widely work
around the problem that Z3's preprocessing introduces by adding extra
symbols. This may cause solving to take longer, to be determined
empirically.

Fixes: #8679

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -67,6 +67,7 @@ smt2_convt::smt2_convt(
     use_datatypes(false),
     use_lambda_for_array(false),
     emit_set_logic(true),
+    quantifier_as_defined_expr(false),
     ns(_ns),
     out(_out),
     benchmark(_benchmark),
@@ -136,6 +137,7 @@ smt2_convt::smt2_convt(
     use_lambda_for_array = true;
     emit_set_logic = false;
     use_datatypes = true;
+    quantifier_as_defined_expr = true;
     break;
   }
 
@@ -888,16 +890,6 @@ 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.is_boolean());
@@ -928,28 +920,13 @@ literalt smt2_convt::convert(const exprt &expr)
   // Note that here we are always converting, so we do not need to consider
   // other literal kinds, only "|B###|"
 
-  // 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);
-    out << ' ';
-    convert_expr(prepared_expr);
-    out << "))\n";
-  }
-  else
-  {
-    auto identifier =
-      convert_identifier(std::string{"B"} + std::to_string(l.var_no()));
-    defined_expressions[expr] = identifier;
-    smt2_identifiers.insert(identifier);
-    out << "(define-fun " << identifier << " () Bool ";
-    convert_expr(prepared_expr);
-    out << ")\n";
-  }
+  auto identifier =
+    convert_identifier(std::string{"B"} + std::to_string(l.var_no()));
+  defined_expressions[expr] = identifier;
+  smt2_identifiers.insert(identifier);
+  out << "(define-fun " << identifier << " () Bool ";
+  convert_expr(prepared_expr);
+  out << ")\n";
 
   return l;
 }
@@ -2439,36 +2416,50 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_forall ||
           expr.id()==ID_exists)
   {
-    const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr);
+    bool already_converted = false;
+    if(quantifier_as_defined_expr)
+    {
+      defined_expressionst::const_iterator it = defined_expressions.find(expr);
+      if(it != defined_expressions.end())
+      {
+        already_converted = true;
+        out << it->second;
+      }
+    }
 
-    if(solver==solvert::MATHSAT)
-      // NOLINTNEXTLINE(readability/throw)
-      throw "MathSAT does not support quantifiers";
+    if(!already_converted)
+    {
+      const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr);
 
-    if(quantifier_expr.id() == ID_forall)
-      out << "(forall ";
-    else if(quantifier_expr.id() == ID_exists)
-      out << "(exists ";
+      if(solver == solvert::MATHSAT)
+        // NOLINTNEXTLINE(readability/throw)
+        throw "MathSAT does not support quantifiers";
+
+      if(quantifier_expr.id() == ID_forall)
+        out << "(forall ";
+      else if(quantifier_expr.id() == ID_exists)
+        out << "(exists ";
 
-    out << '(';
-    bool first = true;
-    for(const auto &bound : quantifier_expr.variables())
-    {
-      if(first)
-        first = false;
-      else
-        out << ' ';
       out << '(';
-      convert_expr(bound);
-      out << ' ';
-      convert_type(bound.type());
-      out << ')';
-    }
-    out << ") ";
+      bool first = true;
+      for(const auto &bound : quantifier_expr.variables())
+      {
+        if(first)
+          first = false;
+        else
+          out << ' ';
+        out << '(';
+        convert_expr(bound);
+        out << ' ';
+        convert_type(bound.type());
+        out << ')';
+      }
+      out << ") ";
 
-    convert_expr(quantifier_expr.where());
+      convert_expr(quantifier_expr.where());
 
-    out << ')';
+      out << ')';
+    }
   }
   else if(
     const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
@@ -5137,6 +5128,13 @@ void smt2_convt::find_symbols(const exprt &expr)
 
   if(expr.id() == ID_exists || expr.id() == ID_forall)
   {
+    if(
+      quantifier_as_defined_expr &&
+      defined_expressions.find(expr) != defined_expressions.end())
+    {
+      return;
+    }
+
     std::unordered_map<irep_idt, std::optional<identifiert>> shadowed_syms;
 
     // do not declare the quantified symbol, but record
@@ -5161,6 +5159,26 @@ void smt2_convt::find_symbols(const exprt &expr)
       else
         previous_entry->second = std::move(*shadowed_val);
     }
+
+    if(quantifier_as_defined_expr)
+    {
+      const irep_idt id =
+        "quantified_expr." + std::to_string(defined_expressions.size());
+
+      out << "; the following is a workaround for solvers removing quantified "
+             "expression during preprocessing\n";
+      out << "(declare-fun " << id << " () Bool)\n";
+
+      out << "(assert (=> " << id << ' ';
+      convert_expr(expr);
+      out << "))\n";
+      out << "(assert (=> ";
+      convert_expr(expr);
+      out << ' ' << id << "))\n";
+
+      defined_expressions[expr] = id;
+    }
+
     return;
   }
 

src/solvers/smt2/smt2_conv.h

@@ -71,6 +71,7 @@ class smt2_convt : public stack_decision_proceduret
   bool use_datatypes;
   bool use_lambda_for_array;
   bool emit_set_logic;
+  bool quantifier_as_defined_expr;
 
   exprt handle(const exprt &expr) override;
   void set_to(const exprt &expr, bool value) override;