From a895506dac7513de516068a7ead80b871096a7e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Jan 2013 09:29:03 -0800
Subject: [PATCH] Fix issue reported at
 http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 RELEASE_NOTES                        |  2 ++
 src/api/api_model.cpp                |  3 ++-
 src/model/model_evaluator.cpp        | 17 ++++++++---------
 src/model/model_evaluator_params.pyg |  8 ++++++++
 src/model/model_params.pyg           |  2 +-
 5 files changed, 21 insertions(+), 11 deletions(-)
 create mode 100644 src/model/model_evaluator_params.pyg

diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 3145d3b62..27c52140f 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -57,6 +57,8 @@ Version 4.3.2
 
 - Relax check_logic procedure. Now, it accepts coercions (to_real) automatically introduced by Z3. (Thanks to Paul Jackson). This is a fix for http://z3.codeplex.com/workitem/19.
 
+- Fixed http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model.
+
 Version 4.3.1
 =============
 
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index f26ffeeba..f17f7a586 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include"model_v2_pp.h"
 #include"model_smt2_pp.h"
 #include"model_params.hpp"
+#include"model_evaluator_params.hpp"
 
 extern "C" {
 
@@ -489,7 +490,7 @@ extern "C" {
                            Z3_model m,
                            Z3_ast t,
                            Z3_ast * v) {
-        model_params p;
+        model_evaluator_params p;
         return Z3_model_eval(c, m, t, p.completion(), v);
     }
 
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index dc4c20aa8..41bca940d 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include"model.h"
+#include"model_evaluator_params.hpp"
 #include"rewriter_types.h"
 #include"model_evaluator.h"
 #include"bool_rewriter.h"
@@ -59,11 +60,12 @@ struct evaluator_cfg : public default_rewriter_cfg {
         updt_params(p);
     }
 
-    void updt_params(params_ref const & p) {
-        m_max_memory       = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-        m_max_steps        = p.get_uint("max_steps", UINT_MAX);
-        m_model_completion = p.get_bool("model_completion", false);
-        m_cache            = p.get_bool("cache", true);
+    void updt_params(params_ref const & _p) {
+        model_evaluator_params p(_p);
+        m_max_memory       = megabytes_to_bytes(p.max_memory());
+        m_max_steps        = p.max_steps();
+        m_model_completion = p.completion();
+        m_cache            = p.cache();
     }
         
     ast_manager & m() const { return m_model.get_manager(); }
@@ -230,10 +232,7 @@ void model_evaluator::updt_params(params_ref const & p) {
 }
 
 void model_evaluator::get_param_descrs(param_descrs & r) {
-    insert_max_memory(r);
-    insert_max_steps(r);
-    r.insert("model_completion", CPK_BOOL, "(default: false) assigns an interpretation to symbols that are not intepreted by the model.");
-    r.insert("cache", CPK_BOOL, "(default: true) cache intermediate results.");
+    model_evaluator_params::collect_param_descrs(r);
 }
 
 void model_evaluator::set_model_completion(bool f) {
diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg
new file mode 100644
index 000000000..b68d5c3ad
--- /dev/null
+++ b/src/model/model_evaluator_params.pyg
@@ -0,0 +1,8 @@
+def_module_params('model_evaluator', 
+                  export=True,
+                  params=(max_memory_param(),
+                          max_steps_param(),
+                          ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
+                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator')
+                          ))
+
diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg
index 977538163..14e83952c 100644
--- a/src/model/model_params.pyg
+++ b/src/model/model_params.pyg
@@ -4,5 +4,5 @@ def_module_params('model',
                           ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
                           ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
                           ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
-                          ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model')))
+                          ))