From 8970a54eaa5241d76a5b3699d0c644110b42c7f1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Jan 2023 22:06:19 -0800 Subject: [PATCH] expose parameters to control behavior for #5660 --- src/sat/sat_solver/sat_smt_preprocess.cpp | 6 +-- src/sat/smt/euf_solver.cpp | 1 + src/sat/smt/q_ematch.cpp | 9 ++-- src/smt/params/preprocessor_params.cpp | 5 +++ src/smt/params/preprocessor_params.h | 52 +++++++++-------------- src/smt/params/smt_params_helper.pyg | 9 ++-- 6 files changed, 40 insertions(+), 42 deletions(-) diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp index 31888251c89..c1a4acc9e95 100644 --- a/src/sat/sat_solver/sat_smt_preprocess.cpp +++ b/src/sat/sat_solver/sat_smt_preprocess.cpp @@ -46,9 +46,9 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep smt_params smtp(p); if (sp.euf() || sp.smt()) { s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); - s.add_simplifier(alloc(propagate_values, m, p, st)); - s.add_simplifier(alloc(euf::solve_eqs, m, st)); - s.add_simplifier(alloc(elim_unconstrained, m, st)); + if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st)); + if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st)); + if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st)); if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st)); if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st)); if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st)); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index b56093eb0ff..c9b0430b584 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -540,6 +540,7 @@ namespace euf { sat::check_result solver::check() { ++m_stats.m_final_checks; TRACE("euf", s().display(tout);); + TRACE("final_check", s().display(tout);); bool give_up = false; bool cont = false; diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 573003305f7..df832a675f7 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -69,9 +69,12 @@ namespace q { [&](euf::enode* n) { m_mam->add_node(n, false); }; - ctx.get_egraph().set_on_merge(_on_merge); - if (!ctx.relevancy_enabled()) - ctx.get_egraph().set_on_make(_on_make); + + if (ctx.get_config().m_ematching) { + ctx.get_egraph().set_on_merge(_on_merge); + if (!ctx.relevancy_enabled()) + ctx.get_egraph().set_on_make(_on_make); + } m_mam = mam::mk(ctx, *this); } diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index f3c46f95c98..180242f858a 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -26,6 +26,9 @@ void preprocessor_params::updt_local_params(params_ref const & _p) { m_restricted_quasi_macros = p.restricted_quasi_macros(); m_pull_nested_quantifiers = p.pull_nested_quantifiers(); m_refine_inj_axiom = p.refine_inj_axioms(); + m_propagate_values = p.propagate_values(); + m_elim_unconstrained = p.elim_unconstrained(); + m_solve_eqs = p.solve_eqs(); m_ng_lift_ite = static_cast(p.q_lift_ite()); } @@ -47,6 +50,8 @@ void preprocessor_params::display(std::ostream & out) const { DISPLAY_PARAM(m_eliminate_term_ite); DISPLAY_PARAM(m_macro_finder); DISPLAY_PARAM(m_propagate_values); + DISPLAY_PARAM(m_solve_eqs); + DISPLAY_PARAM(m_elim_unconstrained); DISPLAY_PARAM(m_refine_inj_axiom); DISPLAY_PARAM(m_eliminate_bounds); DISPLAY_PARAM(m_simplify_bit2int); diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index 53568c36684..55a55980b2b 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -31,43 +31,29 @@ struct preprocessor_params : public pattern_inference_params, public bit_blaster_params { lift_ite_kind m_lift_ite; lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms - bool m_pull_cheap_ite; - bool m_pull_nested_quantifiers; - bool m_eliminate_term_ite; - bool m_macro_finder; - bool m_propagate_values; - bool m_refine_inj_axiom; - bool m_eliminate_bounds; - bool m_simplify_bit2int; - bool m_nnf_cnf; - bool m_distribute_forall; - bool m_reduce_args; - bool m_quasi_macros; - bool m_restricted_quasi_macros; - bool m_max_bv_sharing; - bool m_pre_simplifier; - bool m_nlquant_elim; + bool m_pull_cheap_ite = false; + bool m_pull_nested_quantifiers = false; + bool m_eliminate_term_ite = false; + bool m_macro_finder = false; + bool m_propagate_values = true; + bool m_elim_unconstrained = true; + bool m_solve_eqs = true; + bool m_refine_inj_axiom = true; + bool m_eliminate_bounds = false; + bool m_simplify_bit2int = false; + bool m_nnf_cnf = true; + bool m_distribute_forall = false; + bool m_reduce_args = false; + bool m_quasi_macros = false; + bool m_restricted_quasi_macros = false; + bool m_max_bv_sharing = true; + bool m_pre_simplifier = true; + bool m_nlquant_elim = false; public: preprocessor_params(params_ref const & p = params_ref()): m_lift_ite(lift_ite_kind::LI_NONE), - m_ng_lift_ite(lift_ite_kind::LI_NONE), - m_pull_cheap_ite(false), - m_pull_nested_quantifiers(false), - m_eliminate_term_ite(false), - m_macro_finder(false), - m_propagate_values(true), - m_refine_inj_axiom(true), - m_eliminate_bounds(false), - m_simplify_bit2int(false), - m_nnf_cnf(true), - m_distribute_forall(false), - m_reduce_args(false), - m_quasi_macros(false), - m_restricted_quasi_macros(false), - m_max_bv_sharing(true), - m_pre_simplifier(true), - m_nlquant_elim(false) { + m_ng_lift_ite(lift_ite_kind::LI_NONE) { updt_local_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 8dfcf5d3b6e..86a0371f24e 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -18,8 +18,11 @@ def_module_params(module_name='smt', ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'), ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'), ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), - ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), - ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), + ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'), + ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'), + ('propagate_values', BOOL, True, 'pre-processing: propagate values'), + ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'), + ('refine_inj_axioms', BOOL, True, 'pre-processing: refine injectivity axioms'), ('candidate_models', BOOL, False, 'create candidate models even when quantifier or theory reasoning is incomplete'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), @@ -50,7 +53,7 @@ def_module_params(module_name='smt', ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'), ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'), ('bv.eq_axioms', BOOL, True, 'enable redundant equality axioms for bit-vectors'), - ('bv.size_reduce', BOOL, False, 'turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'), + ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),