From 4ea3ed7e273a0c9170541b43902d2d8723f881f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Oct 2014 11:00:45 -0700 Subject: [PATCH] ensure parameters are updated and ensure that global use of auto-config is not obscured by smt.auto-config scoping Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 25 ++++++++++++++----------- src/qe/qe.h | 7 +++++-- src/qe/qe_sat_tactic.cpp | 9 ++++++--- src/qe/qe_tactic.cpp | 1 + src/smt/params/smt_params.cpp | 3 ++- 5 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 192d97c3b..d229d8735 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -2238,8 +2238,7 @@ namespace qe { m_params(p), m_trail(m), m_qe(0), - m_assumption(m.mk_true()), - m_use_new_qe(true) + m_assumption(m.mk_true()) { } @@ -2261,12 +2260,6 @@ namespace qe { } void expr_quant_elim::updt_params(params_ref const& p) { - bool r = p.get_bool("use_neq_qe", m_use_new_qe); - if (r != m_use_new_qe) { - dealloc(m_qe); - m_qe = 0; - m_use_new_qe = r; - } init_qe(); m_qe->updt_params(p); } @@ -2274,7 +2267,6 @@ namespace qe { void expr_quant_elim::collect_param_descrs(param_descrs& r) { r.insert("eliminate_variables_as_block", CPK_BOOL, "(default: true) eliminate variables as a block (true) or one at a time (false)"); - // r.insert("use_new_qe", CPK_BOOL, "(default: true) invoke quantifier engine based on abstracted solver"); } void expr_quant_elim::init_qe() { @@ -2504,7 +2496,7 @@ namespace qe { class simplify_solver_context : public i_solver_context { ast_manager& m; - smt_params m_fparams; + smt_params m_fparams; app_ref_vector* m_vars; expr_ref* m_fml; ptr_vector m_contains; @@ -2520,6 +2512,10 @@ namespace qe { add_plugin(mk_arith_plugin(*this, false, m_fparams)); } + void updt_params(params_ref const& p) { + m_fparams.updt_params(p); + } + virtual ~simplify_solver_context() { reset(); } void solve(expr_ref& fml, app_ref_vector& vars) { @@ -2610,6 +2606,10 @@ namespace qe { public: impl(ast_manager& m) : m(m), m_ctx(m) {} + void updt_params(params_ref const& p) { + m_ctx.updt_params(p); + } + bool reduce_quantifier( quantifier * old_q, expr * new_body, @@ -2673,6 +2673,10 @@ namespace qe { return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr); } + void simplify_rewriter_cfg::updt_params(params_ref const& p) { + imp->updt_params(p); + } + bool simplify_rewriter_cfg::pre_visit(expr* e) { if (!is_quantifier(e)) return true; quantifier * q = to_quantifier(e); @@ -2680,7 +2684,6 @@ namespace qe { } void simplify_exists(app_ref_vector& vars, expr_ref& fml) { - smt_params params; ast_manager& m = fml.get_manager(); simplify_solver_context ctx(m); ctx.solve(fml, vars); diff --git a/src/qe/qe.h b/src/qe/qe.h index 1697a5cbd..0fd2ff60c 100644 --- a/src/qe/qe.h +++ b/src/qe/qe.h @@ -275,13 +275,12 @@ namespace qe { class expr_quant_elim { ast_manager& m; - smt_params const& m_fparams; + smt_params const& m_fparams; params_ref m_params; expr_ref_vector m_trail; obj_map m_visited; quant_elim* m_qe; expr* m_assumption; - bool m_use_new_qe; public: expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p = params_ref()); ~expr_quant_elim(); @@ -372,6 +371,8 @@ namespace qe { bool pre_visit(expr* e); + void updt_params(params_ref const& p); + }; class simplify_rewriter_star : public rewriter_tpl { @@ -380,6 +381,8 @@ namespace qe { simplify_rewriter_star(ast_manager& m): rewriter_tpl(m, false, m_cfg), m_cfg(m) {} + + void updt_params(params_ref const& p) { m_cfg.updt_params(p); } }; }; diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index b4a1a6a8b..2be32c02d 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -74,6 +74,7 @@ namespace qe { is_relevant_default m_is_relevant; mk_atom_default m_mk_atom; th_rewriter m_rewriter; + simplify_rewriter_star m_qe_rw; expr_strong_context_simplifier m_ctx_rewriter; class solver_context : public i_solver_context { @@ -218,6 +219,7 @@ namespace qe { m_Ms(m), m_assignments(m), m_rewriter(m), + m_qe_rw(m), m_ctx_rewriter(m_fparams, m) { m_fparams.m_model = true; } @@ -256,10 +258,9 @@ namespace qe { ptr_vector fmls; goal->get_formulas(fmls); m_fml = m.mk_and(fmls.size(), fmls.c_ptr()); - TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";); - simplify_rewriter_star rw(m); + TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";); expr_ref tmp(m); - rw(m_fml, tmp); + m_qe_rw(m_fml, tmp); m_fml = tmp; TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";); skolemize_existential_prefix(); @@ -305,6 +306,8 @@ namespace qe { m_projection_mode_param = p.get_bool("projection_mode", m_projection_mode_param); m_strong_context_simplify_param = p.get_bool("strong_context_simplify", m_strong_context_simplify_param); m_ctx_simplify_local_param = p.get_bool("strong_context_simplify_local", m_ctx_simplify_local_param); + m_fparams.updt_params(p); + m_qe_rw.updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index 5b522e041..8819d704b 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -36,6 +36,7 @@ class qe_tactic : public tactic { } void updt_params(params_ref const & p) { + m_fparams.updt_params(p); m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false); m_qe.updt_params(p); } diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index f1c407dc7..18619c8ec 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -19,10 +19,11 @@ Revision History: #include"smt_params.h" #include"smt_params_helper.hpp" #include"model_params.hpp" +#include"gparams.h" void smt_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); - m_auto_config = p.auto_config(); + m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams. m_random_seed = p.random_seed(); m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching();