From 56d3718cde7260d54c34e1420ef11a3436671139 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Jan 2022 03:41:21 -0800 Subject: [PATCH] add simplification with qe-lite as an option #5767 Signed-off-by: Nikolaj Bjorner --- src/qe/lite/qe_lite.h | 2 + src/sat/smt/pb_solver.cpp | 6 ++- src/smt/params/qi_params.cpp | 1 + src/smt/params/qi_params.h | 60 ++++++++------------- src/smt/params/smt_params_helper.pyg | 1 + src/solver/assertions/CMakeLists.txt | 1 + src/solver/assertions/asserted_formulas.cpp | 2 + src/solver/assertions/asserted_formulas.h | 4 ++ 8 files changed, 36 insertions(+), 41 deletions(-) diff --git a/src/qe/lite/qe_lite.h b/src/qe/lite/qe_lite.h index 3251fa3f8..691879753 100644 --- a/src/qe/lite/qe_lite.h +++ b/src/qe/lite/qe_lite.h @@ -60,6 +60,8 @@ public: \brief full rewriting based light-weight quantifier elimination round. */ void operator()(expr_ref& fml, proof_ref& pr); + + void operator()(expr* fml, expr_ref& result, proof_ref& pr) { result = fml; (*this)(result, pr); } }; tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 0eebd5247..b88ba7715 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -1403,8 +1403,10 @@ namespace pb { if (m_solver) m_solver->set_external(lit.var()); c->watch_literal(*this, lit); c->watch_literal(*this, ~lit); - } - SASSERT(c->well_formed()); + } + if (!c->well_formed()) + std::cout << *c << "\n"; + VERIFY(c->well_formed()); if (m_solver && m_solver->get_config().m_drat) { std::function fn = [&](std::ostream& out) { out << "c ba constraint " << *c << " 0\n"; diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index 91f354eda..387df4dd5 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -28,6 +28,7 @@ void qi_params::updt_params(params_ref const & _p) { m_mbqi_trace = p.mbqi_trace(); m_mbqi_force_template = p.mbqi_force_template(); m_mbqi_id = p.mbqi_id(); + m_qe_lite = p.q_lite(); m_qi_profile = p.qi_profile(); m_qi_profile_freq = p.qi_profile_freq(); m_qi_max_instances = p.qi_max_instances(); diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 8ad7a8a90..8f59667a0 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -30,26 +30,27 @@ enum quick_checker_mode { struct qi_params { std::string m_qi_cost; std::string m_qi_new_gen; - double m_qi_eager_threshold; - double m_qi_lazy_threshold; - unsigned m_qi_max_eager_multipatterns; - unsigned m_qi_max_lazy_multipattern_matching; - bool m_qi_profile; - unsigned m_qi_profile_freq; - quick_checker_mode m_qi_quick_checker; - bool m_qi_lazy_quick_checker; - bool m_qi_promote_unsat; - unsigned m_qi_max_instances; - bool m_qi_lazy_instantiation; - bool m_qi_conservative_final_check; + double m_qi_eager_threshold = 10.0; + double m_qi_lazy_threshold = 20.0; + unsigned m_qi_max_eager_multipatterns = 0; + unsigned m_qi_max_lazy_multipattern_matching = 2; + bool m_qi_profile = false; + unsigned m_qi_profile_freq = UINT_MAX; + quick_checker_mode m_qi_quick_checker = MC_NO; + bool m_qi_lazy_quick_checker = true; + bool m_qi_promote_unsat = true; + unsigned m_qi_max_instances = UINT_MAX; + bool m_qi_lazy_instantiation = false; + bool m_qi_conservative_final_check = false; + bool m_qe_lite = false; - bool m_mbqi; - unsigned m_mbqi_max_cexs; - unsigned m_mbqi_max_cexs_incr; - unsigned m_mbqi_max_iterations; - bool m_mbqi_trace; - unsigned m_mbqi_force_template; - const char * m_mbqi_id; + bool m_mbqi = true; + unsigned m_mbqi_max_cexs = 1; + unsigned m_mbqi_max_cexs_incr = 1; + unsigned m_mbqi_max_iterations = 1000; + bool m_mbqi_trace = false; + unsigned m_mbqi_force_template = 10; + const char * m_mbqi_id = nullptr; qi_params(params_ref const & p = params_ref()): /* @@ -78,26 +79,7 @@ struct qi_params { matching loop detection. */ m_qi_cost("(+ weight generation)"), - m_qi_new_gen("cost"), - m_qi_eager_threshold(10.0), - m_qi_lazy_threshold(20.0), // reduced to give a chance to MBQI - m_qi_max_eager_multipatterns(0), - m_qi_max_lazy_multipattern_matching(2), - m_qi_profile(false), - m_qi_profile_freq(UINT_MAX), - m_qi_quick_checker(MC_NO), - m_qi_lazy_quick_checker(true), - m_qi_promote_unsat(true), - m_qi_max_instances(UINT_MAX), - m_qi_lazy_instantiation(false), - m_qi_conservative_final_check(false), - m_mbqi(true), // enabled by default - m_mbqi_max_cexs(1), - m_mbqi_max_cexs_incr(1), - m_mbqi_max_iterations(1000), - m_mbqi_trace(false), - m_mbqi_force_template(10), - m_mbqi_id(nullptr) + m_qi_new_gen("cost") { updt_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 20839ea8a..295b12f80 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -35,6 +35,7 @@ def_module_params(module_name='smt', ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'), ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'), ('q.lift_ite', UINT, 0, '0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers'), + ('q.lite', BOOL, False, 'Use cheap quantifier elimination during pre-processing'), ('qi.profile', BOOL, False, 'profile quantifier instantiation'), ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'), ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'), diff --git a/src/solver/assertions/CMakeLists.txt b/src/solver/assertions/CMakeLists.txt index 7cc320458..6deffd3a5 100644 --- a/src/solver/assertions/CMakeLists.txt +++ b/src/solver/assertions/CMakeLists.txt @@ -4,4 +4,5 @@ z3_add_component(solver_assertions COMPONENT_DEPENDENCIES smt2parser smt_params + qe_lite ) diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 1b8bfe9dd..d852d9383 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -49,6 +49,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re m_refine_inj_axiom(*this), m_max_bv_sharing_fn(*this), m_elim_term_ite(*this), + m_qe_lite(*this), m_pull_nested_quantifiers(*this), m_elim_bvs_from_quantifiers(*this), m_cheap_quant_fourier_motzkin(*this), @@ -285,6 +286,7 @@ void asserted_formulas::reduce() { m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE); if (!invoke(m_ng_lift_ite)) return; if (!invoke(m_elim_term_ite)) return; + if (!invoke(m_qe_lite)) return; if (!invoke(m_refine_inj_axiom)) return; if (!invoke(m_distribute_forall)) return; if (!invoke(m_find_macros)) return; diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 23a4f5a0a..77c670f78 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -37,6 +37,7 @@ Revision History: #include "ast/normal_forms/elim_term_ite.h" #include "ast/pattern/pattern_inference.h" #include "smt/params/smt_params.h" +#include "qe/lite/qe_lite.h" class asserted_formulas { @@ -190,6 +191,8 @@ class asserted_formulas { MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != lift_ite_kind::LI_NONE, true); MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != lift_ite_kind::LI_NONE, true); + MK_SIMPLIFIERA(qe_lite_fn, qe_lite, "qe-lite", af.m_smt_params.m_qe_lite && af.has_quantifiers(), (af.m, af.m_params), true); + reduce_asserted_formulas_fn m_reduce_asserted_formulas; distribute_forall_fn m_distribute_forall; @@ -197,6 +200,7 @@ class asserted_formulas { refine_inj_axiom_fn m_refine_inj_axiom; max_bv_sharing_fn m_max_bv_sharing_fn; elim_term_ite_fn m_elim_term_ite; + qe_lite_fn m_qe_lite; pull_nested_quantifiers m_pull_nested_quantifiers; elim_bvs_from_quantifiers m_elim_bvs_from_quantifiers; cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;