From 1ed892170cf31cee928cb6f6db140ea99d456a48 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sun, 2 Dec 2018 19:35:40 +0000
Subject: [PATCH] smt2_solver: implement get-model

---
 .../smt2_solver/get-model/get-model1.desc     |  8 ++++
 .../smt2_solver/get-model/get-model1.smt2     | 13 +++++++
 src/solvers/smt2/smt2_solver.cpp              | 38 ++++++++++++++++++-
 3 files changed, 58 insertions(+), 1 deletion(-)
 create mode 100644 regression/smt2_solver/get-model/get-model1.desc
 create mode 100644 regression/smt2_solver/get-model/get-model1.smt2

diff --git a/regression/smt2_solver/get-model/get-model1.desc b/regression/smt2_solver/get-model/get-model1.desc
new file mode 100644
index 00000000000..c0385c81f4f
--- /dev/null
+++ b/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\)\)$
+--
diff --git a/regression/smt2_solver/get-model/get-model1.smt2 b/regression/smt2_solver/get-model/get-model1.smt2
new file mode 100644
index 00000000000..dde77550c3e
--- /dev/null
+++ b/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)
diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp
index f9d46a78b8f..e1051de5fd6 100644
--- a/src/solvers/smt2/smt2_solver.cpp
+++ b/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 )