smt2_solver: implement get-model

Author: Daniel Kroening

regression/smt2_solver/get-model/get-model1.desc

@@ -0,0 +1,8 @@
+CORE
+get-model1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+^\(\(define-fun var_x \(\) \(_ BitVec 8\) \(_ bv1 8\)\)$
+--

regression/smt2_solver/get-model/get-model1.smt2

@@ -0,0 +1,13 @@
+(set-logic QF_BV)
+(set-option :produce-models true)
+
+(declare-const var_x (_ BitVec 8)) ; nullary function
+(declare-const var_y (_ BitVec 8)) ; nullary function
+(declare-const var_z (_ BitVec 8)) ; nullary function
+
+(assert (= var_x #x01))
+(assert (= var_y #x02))
+(assert (= var_z (bvadd var_x var_y)))
+
+(check-sat)
+(get-model)

src/solvers/smt2/smt2_solver.cpp

@@ -262,6 +262,43 @@ void smt2_solvert::command(const std::string &c)
       }
       std::cout << ')' << '\n';
     }
+    else if(c == "get-model")
+    {
+      // print a model for all identifiers
+
+      if(status != SAT)
+        throw error("model is not available");
+
+      const symbol_tablet symbol_table;
+      const namespacet ns(symbol_table);
+
+      bool first = true;
+
+      std::cout << '(';
+      for(const auto &id : id_map)
+      {
+        const symbol_exprt name(id.first, id.second.type);
+        const auto value = simplify_expr(solver.get(name), ns);
+
+        if(value.is_not_nil())
+        {
+          if(first)
+            first = false;
+          else
+            std::cout << '\n' << ' ';
+
+          std::cout << "(define-fun " << smt2_format(name) << ' ';
+
+          if(id.second.type.id() == ID_mathematical_function)
+            throw error("models for functions unimplemented");
+          else
+            std::cout << "() " << smt2_format(id.second.type);
+
+          std::cout << ' ' << smt2_format(value) << ')';
+        }
+      }
+      std::cout << ')' << '\n';
+    }
     else if(c == "simplify")
     {
       // this is a command that Z3 appears to implement
@@ -287,7 +324,6 @@ void smt2_solvert::command(const std::string &c)
     | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
     | ( get-assertions )
     | ( get-info hinfo_flag i )
-    | ( get-model )
     | ( get-option hkeywordi )
     | ( get-proof )
     | ( get-unsat-assumptions )