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

@@ -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
 =============
 

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);
     }
 

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

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')
+                          ))
+

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')))
+                          ))