Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

RELEASE_NOTES

@@ -26,6 +26,8 @@ Version 4.3.2
 
 - Fixed crash reported at http://z3.codeplex.com/workitem/10
 
+- Removed auxiliary constants created by the nnf tactic from Z3 models.
+  
 Version 4.3.1
 =============
 

src/ast/normal_forms/defined_names.cpp

@@ -67,6 +67,9 @@ struct defined_names::impl {
     void push_scope();
     void pop_scope(unsigned num_scopes);
     void reset();
+
+    unsigned get_num_names() const { return m_names.size(); }
+    func_decl * get_name_decl(unsigned i) const { return to_app(m_names.get(i))->get_decl(); }
 };
 
 struct defined_names::pos_impl : public defined_names::impl {
@@ -308,6 +311,16 @@ void defined_names::reset() {
     m_pos_impl->reset();
 }
 
+unsigned defined_names::get_num_names() const { 
+    return m_impl->get_num_names() + m_pos_impl->get_num_names();
+}
+
+func_decl * defined_names::get_name_decl(unsigned i) const { 
+    SASSERT(i < get_num_names());
+    unsigned n1 = m_impl->get_num_names();
+    return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1);
+}
+
 
 
 

src/ast/normal_forms/defined_names.h

@@ -80,6 +80,9 @@ public:
     void push();
     void pop(unsigned num_scopes);
     void reset();
+
+    unsigned get_num_names() const;
+    func_decl * get_name_decl(unsigned i) const;
 };
 
 #endif /* _DEFINED_NAMES_H_ */

src/smt/params/smt_params.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include"smt_params.h"
 #include"smt_params_helper.hpp"
+#include"model_params.hpp"
 
 void smt_params::updt_local_params(params_ref const & _p) {
     smt_params_helper p(_p);
@@ -33,6 +34,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
     m_soft_timeout = p.soft_timeout();
+    model_params mp(_p);
+    m_model_compact = mp.compact();
     if (_p.get_bool("arith.greatest_error_pivot", false))
         m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
     else if (_p.get_bool("arith.least_error_pivot", false))
@@ -50,5 +53,4 @@ void smt_params::updt_params(params_ref const & p) {
 void smt_params::updt_params(context_params const & p) {
     m_auto_config    = p.m_auto_config;
     m_model          = p.m_model;
-    m_model_validate = p.m_model_validate;
 }

src/smt/params/smt_params.h

@@ -177,7 +177,6 @@ struct smt_params : public preprocessor_params,
     // -----------------------------------
     bool             m_model; 
     bool             m_model_compact;
-    bool             m_model_validate;
     bool             m_model_on_timeout;
     bool             m_model_on_final_check;
 
@@ -264,7 +263,6 @@ struct smt_params : public preprocessor_params,
         m_abort_after_preproc(false),
         m_model(true),
         m_model_compact(false),
-        m_model_validate(false),
         m_model_on_timeout(false),
         m_model_on_final_check(false),
         m_progress_sampling_freq(0),

src/tactic/core/nnf_tactic.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include"nnf.h"
 #include"tactical.h"
+#include"filter_model_converter.h"
 
 class nnf_tactic : public tactic {
     params_ref    m_params;
@@ -100,6 +101,13 @@ public:
         }
         g->inc_depth();
         result.push_back(g.get());
+        unsigned num_extra_names = dnames.get_num_names();
+        if (num_extra_names > 0) {
+            filter_model_converter * fmc = alloc(filter_model_converter, m);
+            mc = fmc;
+            for (unsigned i = 0; i < num_extra_names; i++)
+                fmc->insert(dnames.get_name_decl(i));
+        }
         TRACE("nnf", g->display(tout););
         SASSERT(g->is_well_sorted());
     }