From b870ed192ada7f98d3a98c8140a2b1899ef09449 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Nov 2024 09:26:32 -0800 Subject: [PATCH] include disequality expansion for non-unit case. Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster.cpp | 6 ++-- src/ast/rewriter/bit_blaster/bit_blaster.h | 22 +++++++----- src/sat/smt/bv_solver.cpp | 36 +++++++++++--------- src/sat/smt/bv_solver.h | 2 -- src/sat/smt/euf_internalize.cpp | 5 +-- 5 files changed, 36 insertions(+), 35 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.cpp b/src/ast/rewriter/bit_blaster/bit_blaster.cpp index 8f5fc2a53..7d26fe47e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster.cpp @@ -28,7 +28,7 @@ bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool m_rw(rw) { } -static void sort_args(expr * & l1, expr * & l2, expr * & l3) { +void bit_blaster_cfg::sort_args(expr * & l1, expr * & l2, expr * & l3) { expr * args[3] = {l1, l2, l3}; // ast_lt_proc is based on the AST ids. So, it is a total order on AST nodes. // No need for stable_sort @@ -41,7 +41,7 @@ void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) { TRACE("xor3", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id();); sort_args(l1, l2, l3); TRACE("xor3_sorted", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id();); - if (m_params.m_bb_ext_gates) { + if (m_ext_gates || m_params.m_bb_ext_gates) { if (l1 == l2) r = l3; else if (l1 == l3) @@ -80,7 +80,7 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) { TRACE("carry", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id();); sort_args(l1, l2, l3); TRACE("carry_sorted", tout << "#" << l1->get_id() << " #" << l2->get_id() << " #" << l3->get_id();); - if (m_params.m_bb_ext_gates) { + if (m_ext_gates || m_params.m_bb_ext_gates) { if ((m().is_false(l1) && m().is_false(l2)) || (m().is_false(l1) && m().is_false(l3)) || (m().is_false(l2) && m().is_false(l3))) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h index 39b6de673..5969e9fc9 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster.h @@ -31,35 +31,39 @@ protected: bv_util & m_util; bit_blaster_params const & m_params; bool_rewriter & m_rw; + bool m_ext_gates = false; + void sort(expr*& a, expr*& b) { if (a->get_id() > b->get_id()) std::swap(a, b); } + void sort_args(expr*& l1, expr*& l2, expr*& l3); public: bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw); ast_manager & m() const { return m_util.get_manager(); } numeral power(unsigned n) const { return rational::power_of_two(n); } - void mk_xor(expr * a, expr * b, expr_ref & r) { m_rw.mk_xor(a, b, r); } + void mk_xor(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_xor(a, b, r); } void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r); void mk_carry(expr * a, expr * b, expr * c, expr_ref & r); - void mk_iff(expr * a, expr * b, expr_ref & r) { m_rw.mk_iff(a, b, r); } - void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); } - void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); } + void mk_iff(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_iff(a, b, r); } + void mk_and(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_and(a, b, r); } + void mk_and(expr* a, expr* b, expr* c, expr_ref& r) { sort_args(a, b, c); m_rw.mk_and(a, b, c, r); } void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); } void mk_ge2(expr* a, expr* b, expr* c, expr_ref& r) { m_rw.mk_ge2(a, b, c, r); } - void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); } - void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); } + void mk_or(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_or(a, b, r); } + void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { sort_args(a, b, c); m_rw.mk_or(a, b, c, r); } void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); } void mk_not(expr * a, expr_ref & r) { m_rw.mk_not(a, r); } void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); } - void mk_nand(expr * a, expr * b, expr_ref & r) { m_rw.mk_nand(a, b, r); } - void mk_nor(expr * a, expr * b, expr_ref & r) { m_rw.mk_nor(a, b, r); } + void mk_nand(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_nand(a, b, r); } + void mk_nor(expr * a, expr * b, expr_ref & r) { sort(a, b); m_rw.mk_nor(a, b, r); } }; -class bit_blaster : public bit_blaster_tpl { +class bit_blaster : public bit_blaster_tpl { bv_util m_util; bool_rewriter m_rw; public: bit_blaster(ast_manager & m, bit_blaster_params const & params); bit_blaster_params const & get_params() const { return this->m_params; } void set_flat_and_or(bool f) { m_rw.set_flat_and_or(f); } + void set_ext_gates(bool f) { m_ext_gates = f; } }; diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index e879ba30c..238533841 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -56,6 +56,7 @@ namespace bv { m_bb(m, get_config()), m_find(*this) { m_bb.set_flat_and_or(false); + m_bb.set_ext_gates(true); } bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) { @@ -267,7 +268,7 @@ namespace bv { ++num_undef; undef_idx = -static_cast(i + 1); } - if (num_undef > 1) + if (num_undef > 1 && false) return; } if (num_undef == 0) @@ -533,12 +534,10 @@ namespace bv { } bool solver::unit_propagate() { - if (m_prop_queue_head == m_prop_queue.size()) + if (m_prop_queue.empty()) return false; - force_push(); - ctx.push(value_trail(m_prop_queue_head)); - for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) { - auto const p = m_prop_queue[m_prop_queue_head]; + for (unsigned i = 0; i < m_prop_queue.size() && !s().inconsistent(); ++i) { + auto const p = m_prop_queue[i]; if (p.m_atom) { for (auto vp : *p.m_atom) propagate_bits(vp); @@ -548,6 +547,7 @@ namespace bv { else propagate_bits(p.m_vp); } + m_prop_queue.reset(); // check_missing_propagation(); return true; } @@ -587,6 +587,8 @@ namespace bv { if (m_wpos[v1] == idx) find_wpos(v1); + bool is_fixed = s().value(m_bits[v1][m_wpos[v1]]) != l_undef; + literal bit1 = m_bits[v1][idx]; lbool val = s().value(bit1); TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_expr_id() << "[" << idx << "] = " << val << "\n";); @@ -613,7 +615,7 @@ namespace bv { if (!assign_bit(bit2, v1, v2, idx, bit1, false)) break; } - if (s().value(m_bits[v1][m_wpos[v1]]) != l_undef) + if (!is_fixed && s().value(m_bits[v1][m_wpos[v1]]) != l_undef) find_wpos(v1); return num_assigned > 0; @@ -626,7 +628,7 @@ namespace bv { */ sat::check_result solver::check() { force_push(); - SASSERT(m_prop_queue.size() == m_prop_queue_head); + SASSERT(m_prop_queue.empty()); bool ok = true; svector> delay; for (auto kv : m_delay_internalize) @@ -651,22 +653,19 @@ namespace bv { } void solver::push_core() { - TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue_lim.size() << "\n";); + TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue.size() << "\n";); th_euf_solver::push_core(); - m_prop_queue_lim.push_back(m_prop_queue.size()); } void solver::pop_core(unsigned n) { SASSERT(m_num_scopes == 0); - unsigned old_sz = m_prop_queue_lim.size() - n; - m_prop_queue.shrink(m_prop_queue_lim[old_sz]); - m_prop_queue_lim.shrink(old_sz); th_euf_solver::pop_core(n); - old_sz = get_num_vars(); + unsigned old_sz = get_num_vars(); m_bits.shrink(old_sz); m_wpos.shrink(old_sz); m_zero_one_bits.shrink(old_sz); - TRACE("bv", tout << "num vars " << old_sz << "@" << m_prop_queue_lim.size() << "\n";); + m_prop_queue.reset(); + TRACE("bv", tout << "num vars " << old_sz << "\n";); } void solver::simplify() { @@ -886,12 +885,14 @@ namespace bv { void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { + TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";); if (!merge_zero_one_bits(r1, r2)) { TRACE("bv", tout << "conflict detected\n";); return; // conflict was detected } + m_prop_queue.reset(); SASSERT(m_bits[v1].size() == m_bits[v2].size()); unsigned sz = m_bits[v1].size(); if (sz == 1) @@ -982,8 +983,9 @@ namespace bv { force_push(); if (a) for (auto curr : *a) - if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) - m_prop_queue.push_back(propagation_item(curr)); + if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) { + m_prop_queue.push_back(propagation_item(curr)); + } return true; } } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 9cbee87f9..3783d4a37 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -234,8 +234,6 @@ namespace bv { mutable vector m_power2; literal_vector m_tmp_literals; svector m_prop_queue; - unsigned_vector m_prop_queue_lim; - unsigned m_prop_queue_head = 0; sat::literal m_true = sat::null_literal; euf::enode_vector m_bv2ints; obj_map m_lazymul; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 602364e7d..8a1937f02 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -155,9 +155,7 @@ namespace euf { if (lit.sign()) { v = si.add_bool_var(e); s().set_external(v); - s().set_eliminated(v, false); - set_bool_var2expr(v, e); - m_var_trail.push_back(v); + s().set_eliminated(v, false); sat::literal lit2 = literal(v, false); th_proof_hint* ph1 = nullptr, * ph2 = nullptr; if (use_drat()) { @@ -185,7 +183,6 @@ namespace euf { return lit; } - set_bool_var2expr(v, e); enode* n = m_egraph.find(e); if (!n)