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

@@ -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
 ==============

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);
+}

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<expr> m_todo, m_args;
     expr_ref_vector m_refs;
     std::unordered_map<expr*,expr*> m_cache;
@@ -48,5 +49,9 @@ public:
     void reset();
 
     bool empty() const { return m_src.empty(); }
+
+    void push_scope();
+
+    void pop_scope(unsigned n);
 };
 

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'),

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);
 }

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);
     }

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;

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;