From 79d47eb3029e01635ac12d71bd47a06bfc67e330 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Feb 2023 17:39:00 -0800 Subject: [PATCH] add preprocessor parameter whether to use bound simplifier --- src/smt/params/preprocessor_params.cpp | 2 ++ src/smt/params/preprocessor_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + src/solver/solver_preprocess.cpp | 2 ++ 4 files changed, 6 insertions(+) diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 180242f85..b6b80a34e 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -30,6 +30,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) { m_elim_unconstrained = p.elim_unconstrained(); m_solve_eqs = p.solve_eqs(); m_ng_lift_ite = static_cast(p.q_lift_ite()); + m_bound_simplifier = p.bound_simplifier(); } void preprocessor_params::updt_params(params_ref const & p) { @@ -63,4 +64,5 @@ void preprocessor_params::display(std::ostream & out) const { DISPLAY_PARAM(m_max_bv_sharing); DISPLAY_PARAM(m_pre_simplifier); DISPLAY_PARAM(m_nlquant_elim); + DISPLAY_PARAM(m_bound_simplifier); } diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index 55a55980b..d53cbbe8f 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -49,6 +49,7 @@ struct preprocessor_params : public pattern_inference_params, bool m_max_bv_sharing = true; bool m_pre_simplifier = true; bool m_nlquant_elim = false; + bool m_bound_simplifier = true; public: preprocessor_params(params_ref const & p = params_ref()): diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 86a0371f2..4b4a453c8 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -21,6 +21,7 @@ def_module_params(module_name='smt', ('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'), + ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'), ('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'), diff --git a/src/solver/solver_preprocess.cpp b/src/solver/solver_preprocess.cpp index 38b0584b5..7fd9d1dba 100644 --- a/src/solver/solver_preprocess.cpp +++ b/src/solver/solver_preprocess.cpp @@ -39,6 +39,7 @@ Notes: #include "ast/simplifiers/push_ite.h" #include "ast/simplifiers/elim_term_ite.h" #include "ast/simplifiers/flatten_clauses.h" +#include "ast/simplifiers/bound_simplifier.h" #include "ast/simplifiers/cnf_nnf.h" #include "smt/params/smt_params.h" #include "solver/solver_preprocess.h" @@ -59,6 +60,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st)); if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st)); if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st)); + if (smtp.m_bound_simplifier) s.add_simplifier(alloc(bound_simplifier, m, p, st)); if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st)); if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st)); if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st));