Merge pull request diffblue#15 from thomasspriggs/tas/no_values_of_quantifiers

Fix errors from issue 5970

Author: thomasspriggs

src/solvers/smt2/smt2_conv.cpp

@@ -319,6 +319,15 @@ exprt smt2_convt::get(const exprt &expr) const
   }
   else if(expr.is_constant())
     return expr;
+  else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
+  {
+    exprt array_copy = *array;
+    for(auto &element : array_copy.operands())
+    {
+      element = get(element);
+    }
+    return array_copy;
+  }
 
   return nil_exprt();
 }
@@ -745,6 +754,14 @@ literalt smt2_convt::convert(const exprt &expr)
   no_boolean_variables++;
 
   out << "; convert\n";
+  out << "; Converting var_no " << l.var_no() << " with expr ID of "
+      << expr.id_string() << "\n";
+  // We're converting the expression, so store it in the defined_expressions
+  // 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 ";
@@ -4314,18 +4331,27 @@ void smt2_convt::set_to(const exprt &expr, bool value)
 
   out << "; set_to " << (value?"true":"false") << "\n"
       << "(assert ";
-
   if(!value)
   {
     out << "(not ";
-    convert_expr(prepared_expr);
-    out << ")";
+  }
+  const auto found_literal = defined_expressions.find(expr);
+  if(!(found_literal == defined_expressions.end()))
+  {
+    // This is a converted expression, we can just assert the literal name
+    // since the expression is already defined
+    out << found_literal->second;
+    set_values[found_literal->second] = value;
   }
   else
+  {
     convert_expr(prepared_expr);
-
-  out << ")" << "\n"; // assert
-
+  }
+  if(!value)
+  {
+    out << ")";
+  }
+  out << ")\n";
   return;
 }
 

src/solvers/smt2/smt2_conv.h

@@ -225,6 +225,10 @@ class smt2_convt : public stack_decision_proceduret
 
   typedef std::map<exprt, irep_idt> defined_expressionst;
   defined_expressionst defined_expressions;
+  /// The values which boolean identifiers have been `smt2_convt::set_to` or
+  /// in other words those which are asserted as true / false in the output
+  /// smt2 formula.
+  std::unordered_map<irep_idt, bool> set_values;
 
   defined_expressionst object_sizes;
 

src/solvers/smt2/smt2_dec.cpp

@@ -139,7 +139,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
   boolean_assignment.resize(no_boolean_variables, false);
 
   typedef std::unordered_map<irep_idt, irept> valuest;
-  valuest values;
+  valuest parsed_values;
 
   while(in)
   {
@@ -167,37 +167,54 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
       // ( (|some_integer| 0) )
       // ( (|some_integer| (- 10)) )
 
-      values[s0.id()] = s1;
+      parsed_values[s0.id()] = s1;
     }
     else if(
       parsed.id().empty() && parsed.get_sub().size() == 2 &&
       parsed.get_sub().front().id() == "error")
     {
+      const auto &message = id2string(parsed.get_sub()[1].id());
+
       // We ignore errors after UNSAT because get-value after check-sat
       // returns unsat will give an error.
-      if(res != resultt::D_UNSATISFIABLE)
+      if(
+        res != resultt::D_UNSATISFIABLE &&
+        !(solver == solvert::Z3 &&
+          message.find("must not contain quantifiers") != std::string::npos))
       {
         messaget log{message_handler};
         log.error() << "SMT2 solver returned error message:\n"
-                    << "\t\"" << parsed.get_sub()[1].id() << "\""
-                    << messaget::eom;
+                    << "\t\"" << message << "\"" << messaget::eom;
         return decision_proceduret::resultt::D_ERROR;
       }
     }
   }
 
+  if(res != resultt::D_SATISFIABLE)
+    return res;
+
   for(auto &assignment : identifier_map)
   {
     std::string conv_id = convert_identifier(assignment.first);
-    const irept &value = values[conv_id];
+    const irept &value = parsed_values[conv_id];
     assignment.second.value = parse_rec(value, assignment.second.type);
   }
 
   // Booleans
   for(unsigned v = 0; v < no_boolean_variables; v++)
   {
-    const irept &value = values["B" + std::to_string(v)];
-    boolean_assignment[v] = (value.id() == ID_true);
+    const std::string boolean_identifier = "B" + std::to_string(v);
+    boolean_assignment[v] = [&]() {
+      const auto found_parsed_value = parsed_values.find(boolean_identifier);
+      if(found_parsed_value != parsed_values.end())
+        return found_parsed_value->second.id() == ID_true;
+      // Work out the value based on what set_to was called with.
+      const auto found_set_value =
+        set_values.find('|' + boolean_identifier + '|');
+      if(found_set_value != set_values.end())
+        return found_set_value->second;
+      UNREACHABLE;
+    }();
   }
 
   return res;