From e0f4d870fd120f0429a557d583035963a0a6cc08 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Dec 2012 14:03:58 -0800 Subject: [PATCH] Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem. Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/ast/normal_forms/defined_names.cpp | 13 +++++++++++++ src/ast/normal_forms/defined_names.h | 3 +++ src/smt/params/smt_params.cpp | 4 +++- src/smt/params/smt_params.h | 2 -- src/tactic/core/nnf_tactic.cpp | 8 ++++++++ 6 files changed, 29 insertions(+), 3 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 7ac026673..19b361acc 100644 --- a/RELEASE_NOTES +++ b/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 ============= diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index 91acacf61..16e9098fc 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/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); +} + diff --git a/src/ast/normal_forms/defined_names.h b/src/ast/normal_forms/defined_names.h index d720a2fa3..0b9f04569 100644 --- a/src/ast/normal_forms/defined_names.h +++ b/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_ */ diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index e62a3de21..519302c19 100644 --- a/src/smt/params/smt_params.cpp +++ b/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; } diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 3d823cb51..256c5a646 100644 --- a/src/smt/params/smt_params.h +++ b/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), diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index a79a4ed06..19190c299 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/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()); }