smt2: implemented get-assignment

get-assignment returns the satisfying assignment for a given set of named
terms.

Author: Daniel Kroening

regression/smt2_solver/get-assignment/get-assignment1.desc

@@ -0,0 +1,8 @@
+CORE
+get-assignment1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+^\(\(y_equality true\)\)$
+--

regression/smt2_solver/get-assignment/get-assignment1.smt2

@@ -0,0 +1,13 @@
+(set-logic QF_BV)
+(set-option :produce-assignments 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) :named y_equality))
+(assert (= var_z (bvadd var_x var_y)))
+
+(check-sat)
+(get-assignment)

src/solvers/smt2/smt2_solver.cpp

@@ -232,6 +232,36 @@ void smt2_solvert::command(const std::string &c)
 
       std::cout << smt2_format(constant_exprt(buffer, string_typet())) << '\n';
     }
+    else if(c == "get-assignment")
+    {
+      // print satisfying assignment for all named expressions
+
+      if(status != SAT)
+        throw error("model is not available");
+
+      bool first = true;
+
+      std::cout << '(';
+      for(const auto &named_term : named_terms)
+      {
+        const symbol_tablet symbol_table;
+        const namespacet ns(symbol_table);
+        const auto value =
+          simplify_expr(solver.get(named_term.second.term), ns);
+
+        if(value.is_constant())
+        {
+          if(first)
+            first = false;
+          else
+            std::cout << '\n' << ' ';
+
+          std::cout << '(' << smt2_format(named_term.second.name) << ' '
+                    << smt2_format(value) << ')';
+        }
+      }
+      std::cout << ')' << '\n';
+    }
     else if(c == "simplify")
     {
       // this is a command that Z3 appears to implement
@@ -256,7 +286,6 @@ void smt2_solvert::command(const std::string &c)
     | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
     | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
     | ( get-assertions )
-    | ( get-assignment )
     | ( get-info hinfo_flag i )
     | ( get-model )
     | ( get-option hkeywordi )