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/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 )