Merge pull request #3461 from diffblue/smt2_solver_get-value

SMT2 solver: implement get-value

Author: Daniel Kroening

scripts/delete_failing_smt2_solver_tests

@@ -39,7 +39,6 @@ rm Float4/test.desc
 rm Float5/test.desc
 rm Float6/test.desc
 rm Float8/test.desc
-rm Free2/test.desc
 rm Function1/test.desc
 rm Initialization6/test.desc
 rm Linking4/test.desc
@@ -51,14 +50,12 @@ rm Malloc19/test.desc
 rm Malloc21/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
-rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
 rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
 rm Multi_Dimensional_Array3/test.desc
 rm Multi_Dimensional_Array4/test.desc
 rm Multi_Dimensional_Array6/test.desc
-rm Multiple_Properties1/test.desc
 rm Overflow_Leftshift1/test.desc
 rm Overflow_Multiplication1/test.desc
 rm Overflow_Subtraction1/test.desc
@@ -92,14 +89,12 @@ rm Quantifiers-not-exists/test.desc
 rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
 rm Quantifiers1/test.desc
-rm Recursion5/test.desc
 rm String2/test.desc
 rm Struct_Bytewise1/test.desc
 rm Struct_Bytewise2/test.desc
 rm Struct_Initialization2/test.desc
 rm Struct_Padding1/test.desc
 rm Typecast1/test.desc
-rm Undefined_Shift1/test.desc
 rm Union_Initialization1/test.desc
 rm Unwinding_Locality1/test.desc
 rm address_space_size_limit1/test.desc
@@ -117,7 +112,6 @@ rm byte_update6/test.desc
 rm byte_update7/test.desc
 rm byte_update8/test.desc
 rm byte_update9/test.desc
-rm compact-trace/test.desc
 rm dynamic_size1/stack_object.desc
 rm equality_through_array1/test.desc
 rm equality_through_array2/test.desc
@@ -134,19 +128,14 @@ rm equality_through_struct_containing_arrays2/test.desc
 rm equality_through_union1/test.desc
 rm equality_through_union2/test.desc
 rm equality_through_union3/test.desc
-rm full_slice1/test.desc
-rm full_slice2/test.desc
 rm gcc_bswap1/test.desc
 rm gcc_c99-bool-1/test.desc
 rm gcc_statement_expression4/test.desc
-rm gcc_switch_case_range1/test.desc
-rm gcc_switch_case_range2/test.desc
 rm gcc_vector1/test.desc
 rm gcc_vector2/test.desc
 rm graphml_witness1/test.desc
 rm havoc_object1/test.desc
 rm hex_trace/test.desc
-rm if2/test.desc
 rm integer-assignments1/test.desc
 rm little-endian-array1/test.desc
 rm memory_allocation1/test.desc

src/solvers/Makefile

@@ -185,6 +185,7 @@ SRC = $(BOOLEFORCE_SRC) \
       sat/resolution_proof.cpp \
       smt2/smt2_conv.cpp \
       smt2/smt2_dec.cpp \
+      smt2/smt2_format.cpp \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \

src/solvers/smt2/smt2_format.cpp

@@ -0,0 +1,71 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "smt2_format.h"
+
+#include <util/arith_tools.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
+{
+  if(type.id() == ID_unsignedbv)
+    out << "(_ BitVec " << to_unsignedbv_type(type).get_width() << ')';
+  else if(type.id() == ID_bool)
+    out << "Bool";
+  else if(type.id() == ID_integer)
+    out << "Int";
+  else if(type.id() == ID_real)
+    out << "Real";
+  else
+    out << "? " << type.id();
+
+  return out;
+}
+
+std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
+{
+  if(expr.id() == ID_constant)
+  {
+    const auto &value = to_constant_expr(expr).get_value();
+
+    const typet &expr_type = expr.type();
+
+    if(expr_type.id() == ID_unsignedbv)
+    {
+      const std::size_t width = to_unsignedbv_type(expr_type).get_width();
+
+      const auto value = numeric_cast_v<mp_integer>(expr);
+
+      out << "(_ bv" << value << " " << width << ")";
+    }
+    else if(expr_type.id() == ID_bool)
+    {
+      if(expr.is_true())
+        out << "true";
+      else if(expr.is_false())
+        out << "false";
+      else
+        DATA_INVARIANT(false, "unknown Boolean constant");
+    }
+    else if(expr_type.id() == ID_integer)
+    {
+      out << value;
+    }
+    else
+      DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    out << to_symbol_expr(expr).get_identifier();
+  }
+  else
+    out << "? " << expr.id();
+
+  return out;
+}

src/solvers/smt2/smt2_format.h

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
+#define CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H
+
+#include <util/expr.h>
+
+template <typename T>
+struct smt2_format_containert
+{
+  explicit smt2_format_containert(const T &_o) : o(_o)
+  {
+  }
+
+  const T &o;
+};
+
+template <typename T>
+static inline smt2_format_containert<T> smt2_format(const T &_o)
+{
+  return smt2_format_containert<T>(_o);
+}
+
+template <typename T>
+static inline std::ostream &
+operator<<(std::ostream &out, const smt2_format_containert<T> &c)
+{
+  return smt2_format_rec(out, c.o);
+}
+
+std::ostream &smt2_format_rec(std::ostream &, const exprt &);
+std::ostream &smt2_format_rec(std::ostream &, const typet &);
+
+#endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H

src/solvers/smt2/smt2_parser.cpp

@@ -8,23 +8,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_parser.h"
 
-#include <util/arith_tools.h>
-
-std::ostream &operator<<(std::ostream &out, const smt2_parsert::smt2_format &f)
-{
-  if(f.type.id() == ID_unsignedbv)
-    out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')';
-  else if(f.type.id() == ID_bool)
-    out << "Bool";
-  else if(f.type.id() == ID_integer)
-    out << "Int";
-  else if(f.type.id() == ID_real)
-    out << "Real";
-  else
-    out << "? " << f.type.id();
+#include "smt2_format.h"
 
-  return out;
-}
+#include <util/arith_tools.h>
 
 void smt2_parsert::command_sequence()
 {

src/solvers/smt2/smt2_parser.h

@@ -43,15 +43,6 @@ class smt2_parsert:public smt2_tokenizert
   using id_mapt=std::map<irep_idt, idt>;
   id_mapt id_map;
 
-  struct smt2_format
-  {
-    explicit smt2_format(const typet &_type) : type(_type)
-    {
-    }
-
-    const typet type;
-  };
-
 protected:
   bool exit;
   void command_sequence();
@@ -91,6 +82,4 @@ class smt2_parsert:public smt2_tokenizert
   exprt cast_bv_to_unsigned(const exprt &);
 };
 
-std::ostream &operator<<(std::ostream &, const smt2_parsert::smt2_format &);
-
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H

src/solvers/smt2/smt2_solver.cpp

@@ -6,11 +6,13 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include "smt2_parser.h"
+
+#include "smt2_format.h"
+
 #include <fstream>
 #include <iostream>
 
-#include "smt2_parser.h"
-
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_symbol.h>
@@ -23,11 +25,8 @@ Author: Daniel Kroening, [email protected]
 class smt2_solvert:public smt2_parsert
 {
 public:
-  smt2_solvert(
-    std::istream &_in,
-    decision_proceduret &_solver):
-    smt2_parsert(_in),
-    solver(_solver)
+  smt2_solvert(std::istream &_in, decision_proceduret &_solver)
+    : smt2_parsert(_in), solver(_solver), status(NOT_SOLVED)
   {
   }
 
@@ -39,6 +38,13 @@ class smt2_solvert:public smt2_parsert
   void expand_function_applications(exprt &);
 
   std::set<irep_idt> constants_done;
+
+  enum
+  {
+    NOT_SOLVED,
+    SAT,
+    UNSAT
+  } status;
 };
 
 void smt2_solvert::define_constants(const exprt &expr)
@@ -139,14 +145,17 @@ void smt2_solvert::command(const std::string &c)
       {
       case decision_proceduret::resultt::D_SATISFIABLE:
         std::cout << "sat\n";
+        status = SAT;
         break;
 
       case decision_proceduret::resultt::D_UNSATISFIABLE:
         std::cout << "unsat\n";
+        status = UNSAT;
         break;
 
       case decision_proceduret::resultt::D_ERROR:
         std::cout << "error\n";
+        status = NOT_SOLVED;
       }
     }
     else if(c=="check-sat-assuming")
@@ -162,6 +171,63 @@ void smt2_solvert::command(const std::string &c)
         std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
       }
     }
+    else if(c == "get-value")
+    {
+      std::vector<exprt> ops;
+
+      if(next_token() != OPEN)
+        throw "get-value expects list as argument";
+
+      while(peek() != CLOSE && peek() != END_OF_FILE)
+        ops.push_back(expression()); // any term
+
+      if(next_token() != CLOSE)
+        throw "get-value expects ')' at end of list";
+
+      if(status != SAT)
+        throw "model is not available";
+
+      std::vector<exprt> values;
+      values.reserve(ops.size());
+
+      for(const auto &op : ops)
+      {
+        if(op.id() != ID_symbol)
+          throw "get-value expects symbol";
+
+        const auto &identifier = to_symbol_expr(op).get_identifier();
+
+        const auto id_map_it = id_map.find(identifier);
+
+        if(id_map_it == id_map.end())
+          throw "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);
+
+        if(value.is_nil())
+          throw "no value for " + id2string(identifier);
+
+        values.push_back(value);
+      }
+
+      std::cout << '(';
+
+      for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++)
+      {
+        if(op_nr != 0)
+          std::cout << "\n ";
+
+        std::cout << '(' << smt2_format(ops[op_nr]) << ' '
+                  << smt2_format(values[op_nr]) << ')';
+      }
+
+      std::cout << ")\n";
+    }
     else if(c=="simplify")
     {
       // this is a command that Z3 appears to implement
@@ -195,7 +261,6 @@ void smt2_solvert::command(const std::string &c)
     | ( get-proof )
     | ( get-unsat-assumptions )
     | ( get-unsat-core )
-    | ( get-value ( htermi + ) )
     | ( pop hnumerali )
     | ( push hnumerali )
     | ( reset )