Merge pull request #3550 from diffblue/smt2_constants

smt2 solver: constants

Author: Daniel Kroening

scripts/delete_failing_smt2_solver_tests

@@ -62,8 +62,6 @@ rm Quantifiers-if/test.desc
 rm Quantifiers-initialisation2/test.desc
 rm Quantifiers-invalid-var-range/test.desc
 rm Quantifiers-not/test.desc
-rm Quantifiers-not-exists/test.desc
-rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
 rm Struct_Bytewise2/test.desc
 rm Union_Initialization1/test.desc
@@ -92,6 +90,7 @@ rm equality_through_union3/test.desc
 rm gcc_bswap1/test.desc
 rm gcc_vector1/test.desc
 rm graphml_witness1/test.desc
+rm integer-assignments1/test.desc
 rm memory_allocation1/test.desc
 rm pointer-function-parameters-struct-mutual-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion/test.desc

src/solvers/smt2/smt2_format.cpp

@@ -100,6 +100,25 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
         << smt2_format(with_expr.where()) << ' '
         << smt2_format(with_expr.new_value()) << ')';
   }
+  else if(expr.id() == ID_array_list)
+  {
+    const auto &array_list_expr = to_multi_ary_expr(expr);
+
+    for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
+      out << "(store ";
+
+    out << "((as const " << smt2_format(expr.type()) << ")) "
+        << smt2_format(from_integer(0, expr.type().subtype())) << ')';
+
+    for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
+    {
+      DATA_INVARIANT(
+        i < array_list_expr.operands().size() - 1,
+        "array_list has even number of operands");
+      out << ' ' << smt2_format(array_list_expr.operands()[i]) << ' '
+          << smt2_format(array_list_expr.operands()[i + 1]) << ')';
+    }
+  }
   else
     out << "? " << expr.id();
 

src/solvers/smt2/smt2_solver.cpp

@@ -34,7 +34,7 @@ class smt2_solvert:public smt2_parsert
   decision_proceduret &solver;
 
   void command(const std::string &) override;
-  void define_constants(const exprt &);
+  void define_constants();
   void expand_function_applications(exprt &);
 
   std::set<irep_idt> constants_done;
@@ -47,36 +47,28 @@ class smt2_solvert:public smt2_parsert
   } status;
 };
 
-void smt2_solvert::define_constants(const exprt &expr)
+void smt2_solvert::define_constants()
 {
-  for(const auto &op : expr.operands())
-    define_constants(op);
-
-  if(expr.id()==ID_symbol)
+  for(const auto &id : id_map)
   {
-    irep_idt identifier=to_symbol_expr(expr).get_identifier();
+    if(id.second.type.id() == ID_mathematical_function)
+      continue;
+
+    if(id.second.definition.is_nil())
+      continue;
+
+    const irep_idt &identifier = id.first;
 
     // already done?
     if(constants_done.find(identifier)!=constants_done.end())
-      return;
+      continue;
 
     constants_done.insert(identifier);
 
-    auto f_it=id_map.find(identifier);
-
-    if(f_it!=id_map.end())
-    {
-      const auto &f=f_it->second;
-
-      if(f.type.id()!=ID_mathematical_function &&
-         f.definition.is_not_nil())
-      {
-        exprt def=f.definition;
-        expand_function_applications(def);
-        define_constants(def); // recursive!
-        solver.set_to_true(equal_exprt(expr, def));
-      }
-    }
+    exprt def = id.second.definition;
+    expand_function_applications(def);
+    solver.set_to_true(
+      equal_exprt(symbol_exprt(identifier, id.second.type), def));
   }
 }
 
@@ -135,12 +127,14 @@ void smt2_solvert::command(const std::string &c)
       if(e.is_not_nil())
       {
         expand_function_applications(e);
-        define_constants(e);
         solver.set_to_true(e);
       }
     }
     else if(c == "check-sat")
     {
+      // add constant definitions as constraints
+      define_constants();
+
       switch(solver())
       {
       case decision_proceduret::resultt::D_SATISFIABLE:
@@ -200,12 +194,7 @@ void smt2_solvert::command(const std::string &c)
         if(id_map_it == id_map.end())
           throw error("unexpected symbol " + id2string(identifier));
 
-        exprt value;
-
-        if(id_map_it->second.definition.is_nil())
-          value = solver.get(op);
-        else
-          value = solver.get(id_map_it->second.definition);
+        const exprt value = solver.get(op);
 
         if(value.is_nil())
           throw error("no value for " + id2string(identifier));