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,16 @@ 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()));
+  auto identifier =
+    convert_identifier(std::string{"B"} + std::to_string(l.var_no()));
+  // we might already have put expr in defined_expressions via
+  // prepare_for_convert_expr
+  if(defined_expressions.find(expr) == defined_expressions.end())
     defined_expressions[expr] = identifier;
-    smt2_identifiers.insert(identifier);
-    out << "(define-fun " << identifier << " () Bool ";
-    convert_expr(prepared_expr);
-    out << ")\n";
-  }
+  smt2_identifiers.insert(identifier);
+  out << "(define-fun " << identifier << " () Bool ";
+  convert_expr(prepared_expr);
+  out << ")\n";
 
   return l;
 }
@@ -2439,36 +2419,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,30 +5131,61 @@ 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
     // as 'bound symbol'
     const auto &q_expr = to_quantifier_expr(expr);
-    for(const auto &symbol : q_expr.variables())
-    {
-      const auto identifier = symbol.get_identifier();
-      auto id_entry =
-        identifier_map.insert({identifier, identifiert{symbol.type(), true}});
-      shadowed_syms.insert(
-        {identifier,
-         id_entry.second ? std::nullopt
-                         : std::optional{id_entry.first->second}});
-    }
-    find_symbols(q_expr.where());
-    for(const auto &[id, shadowed_val] : shadowed_syms)
-    {
-      auto previous_entry = identifier_map.find(id);
-      if(!shadowed_val.has_value())
-        identifier_map.erase(previous_entry);
-      else
-        previous_entry->second = std::move(*shadowed_val);
+    if(!quantifier_as_defined_expr)
+    {
+      for(const auto &symbol : q_expr.variables())
+      {
+        const auto identifier = symbol.get_identifier();
+        auto id_entry =
+          identifier_map.insert({identifier, identifiert{symbol.type(), true}});
+        shadowed_syms.insert(
+          {identifier,
+           id_entry.second ? std::nullopt
+                           : std::optional{id_entry.first->second}});
+      }
+      find_symbols(q_expr.where());
+      for(const auto &[id, shadowed_val] : shadowed_syms)
+      {
+        auto previous_entry = identifier_map.find(id);
+        if(!shadowed_val.has_value())
+          identifier_map.erase(previous_entry);
+        else
+          previous_entry->second = std::move(*shadowed_val);
+      }
+    }
+    else
+    {
+      find_symbols(q_expr.where());
+
+      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;