From 48b13291d1fc1707ec1f839f98bbba28c6990c9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Aug 2022 16:35:14 -0700 Subject: [PATCH] add bv-size reduce #6137 - add option smt.bv.reduce_size. - it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant. This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0. --- RELEASE_NOTES.md | 4 +++ src/ast/rewriter/expr_safe_replace.cpp | 14 ++++++++ src/ast/rewriter/expr_safe_replace.h | 5 +++ src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_bv_params.cpp | 2 ++ src/smt/params/theory_bv_params.h | 1 + src/solver/assertions/asserted_formulas.cpp | 39 +++++++++++++++++++++ src/solver/assertions/asserted_formulas.h | 12 +++++++ 8 files changed, 78 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 48b97583e..783e92e4b 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -19,6 +19,10 @@ Version 4.11.0 - add solver.lemmas2console - prints lemmas to the console. - remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files +- add option smt.bv.reduce_size. + - it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant. + This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0. +- add feature to model-based projection for arithmetic to handle integer division. Version 4.10.2 ============== diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 300e82707..2ca3b5e24 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -190,3 +190,17 @@ void expr_safe_replace::apply_substitution(expr* s, expr* def, expr_ref& t) { (*this)(t, t); reset(); } + +void expr_safe_replace::push_scope() { + m_limit.push_back(m_src.size()); +} + +void expr_safe_replace::pop_scope(unsigned n) { + unsigned old_sz = m_limit[m_limit.size() - n]; + if (old_sz != m_src.size()) { + m_cache.clear(); + m_src.shrink(old_sz); + m_dst.shrink(old_sz); + } + m_limit.shrink(m_limit.size() - n); +} diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h index 4e8b64232..7f5a3a100 100644 --- a/src/ast/rewriter/expr_safe_replace.h +++ b/src/ast/rewriter/expr_safe_replace.h @@ -28,6 +28,7 @@ class expr_safe_replace { ast_manager& m; expr_ref_vector m_src; expr_ref_vector m_dst; + unsigned_vector m_limit = 0; ptr_vector m_todo, m_args; expr_ref_vector m_refs; std::unordered_map m_cache; @@ -48,5 +49,9 @@ public: void reset(); bool empty() const { return m_src.empty(); } + + void push_scope(); + + void pop_scope(unsigned n); }; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 3b32d7602..d32517a23 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -50,6 +50,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, True, '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'), ('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'), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 61b4d967a..35a62e7fc 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -28,6 +28,7 @@ void theory_bv_params::updt_params(params_ref const & _p) { m_bv_enable_int2bv2int = p.bv_enable_int2bv(); m_bv_delay = p.bv_delay(); m_bv_eq_axioms = p.bv_eq_axioms(); + m_bv_size_reduce = p.bv_size_reduce(); } #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; @@ -42,4 +43,5 @@ void theory_bv_params::display(std::ostream & out) const { DISPLAY_PARAM(m_bv_blast_max_size); DISPLAY_PARAM(m_bv_enable_int2bv2int); DISPLAY_PARAM(m_bv_delay); + DISPLAY_PARAM(m_bv_size_reduce); } diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 57ec16b6a..e83b0b5db 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -36,6 +36,7 @@ struct theory_bv_params { bool m_bv_enable_int2bv2int = true; bool m_bv_watch_diseq = false; bool m_bv_delay = true; + bool m_bv_size_reduce = false; theory_bv_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index e1345fe92..5780ef227 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -26,6 +26,7 @@ Revision History: #include "ast/pattern/pattern_inference.h" #include "ast/macros/quasi_macros.h" #include "ast/occurs.h" +#include "ast/bv_decl_plugin.h" #include "solver/assertions/asserted_formulas.h" @@ -54,6 +55,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re m_elim_bvs_from_quantifiers(*this), m_cheap_quant_fourier_motzkin(*this), m_apply_bit2int(*this), + m_bv_size_reduce(*this), m_lift_ite(*this), m_ng_lift_ite(*this), m_find_macros(*this), @@ -205,6 +207,7 @@ void asserted_formulas::push_scope_core() { m_elim_term_ite.push(); m_bv_sharing.push_scope(); m_macro_manager.push_scope(); + m_bv_size_reduce.push_scope(); commit(); TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n"); } @@ -225,6 +228,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";); m_bv_sharing.pop_scope(num_scopes); m_macro_manager.pop_scope(num_scopes); + m_bv_size_reduce.pop_scope(num_scopes); unsigned new_lvl = m_scopes.size() - num_scopes; scope & s = m_scopes[new_lvl]; m_inconsistent = s.m_inconsistent_old; @@ -293,6 +297,7 @@ void asserted_formulas::reduce() { if (!invoke(m_find_macros)) return; if (!invoke(m_apply_quasi_macros)) return; if (!invoke(m_apply_bit2int)) return; + if (!invoke(m_bv_size_reduce)) return; if (!invoke(m_cheap_quant_fourier_motzkin)) return; if (!invoke(m_pattern_inference)) return; if (!invoke(m_max_bv_sharing_fn)) return; @@ -717,6 +722,40 @@ void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, e } +void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { + bv_util bv(m); + expr* f = j.get_fml(); + expr* a, *b, *x; + unsigned lo, hi; + rational r; + expr_ref new_term(m); + auto check_reduce = [&](expr* a, expr* b) { + if (bv.is_extract(a, lo, hi, x) && lo > 0 && hi + 1 == bv.get_bv_size(x) && bv.is_numeral(b, r) && r == 0) { + // insert x -> x[0,lo-1] ++ n into sub + new_term = bv.mk_concat(bv.mk_extract(lo - 1, 0, x), b); + m_sub.insert(x, new_term); + n = j.get_fml(); + return true; + } + return false; + }; + if (m.is_eq(f, a, b) && (check_reduce(a, b) || check_reduce(b, a))) { + // done + } + else { + n = j.get_fml(); + m_sub(n); + } +} + +void asserted_formulas::bv_size_reduce_fn::push_scope() { + m_sub.push_scope(); +} + +void asserted_formulas::bv_size_reduce_fn::pop_scope(unsigned n) { + m_sub.pop_scope(n); +} + unsigned asserted_formulas::get_total_size() const { expr_mark visited; unsigned r = 0; diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 77c670f78..c4da97704 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -30,6 +30,7 @@ Revision History: #include "ast/rewriter/bv_elim.h" #include "ast/rewriter/der.h" #include "ast/rewriter/elim_bounds.h" +#include "ast/rewriter/expr_safe_replace.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "ast/normal_forms/defined_names.h" @@ -150,6 +151,16 @@ class asserted_formulas { void post_op() override { af.m_reduce_asserted_formulas(); } }; + class bv_size_reduce_fn : public simplify_fmls { + expr_safe_replace m_sub; + public: + bv_size_reduce_fn(asserted_formulas& af): simplify_fmls(af, "bv-size-reduce"), m_sub(af.m) {} + bool should_apply() const override { return af.m_smt_params.m_bv_size_reduce; } + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override; + void push_scope(); + void pop_scope(unsigned n); + }; + class elim_term_ite_fn : public simplify_fmls { elim_term_ite_rw m_elim; public: @@ -205,6 +216,7 @@ class asserted_formulas { elim_bvs_from_quantifiers m_elim_bvs_from_quantifiers; cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin; apply_bit2int m_apply_bit2int; + bv_size_reduce_fn m_bv_size_reduce; lift_ite m_lift_ite; ng_lift_ite m_ng_lift_ite; find_macros_fn m_find_macros;