From 706d542eeb8e5b333710f96babcf01a4ae484636 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Feb 2023 17:52:34 -0800 Subject: [PATCH] add propagation justification to bv antecedents --- src/sat/smt/bv_polysat.cpp | 2 +- src/sat/smt/bv_solver.cpp | 43 ++++++++++++++++++++++++++++++++++++++ src/sat/smt/bv_solver.h | 42 ++++++++++++++++++++++++++++--------- 3 files changed, 76 insertions(+), 11 deletions(-) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index e1ec7e73f..d7a2012e2 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -268,7 +268,7 @@ namespace bv { eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2))); } } - auto* ex = euf::th_explain::conflict(*this, core, eqs); + auto ex = mk_bv2ext_justification(core, eqs); ctx.set_conflict(ex); } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index f660b1a77..ab4f2b22e 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -388,6 +388,13 @@ namespace bv { ctx.add_antecedent(probing, c.a, c.c); break; } + case bv_justification::kind_t::bvext: { + for (unsigned i = 0; i < c.m_num_literals; ++i) + r.push_back(c.m_literals[i]); + for (unsigned i = 0; i < c.m_num_eqs; ++i) + ctx.add_antecedent(probing, c.m_eqs[i].first, c.m_eqs[i].second); + break; + } default: UNREACHABLE(); break; @@ -465,6 +472,14 @@ namespace bv { lits.push_back(leq1); lits.push_back(leq2); break; + case bv_justification::kind_t::bvext: + for (unsigned i = 0; i < c.m_num_literals; ++i) + lits.push_back(~c.m_literals[i]); + for (unsigned i = 0; i < c.m_num_eqs; ++i) { + IF_VERBOSE(0, verbose_stream() << "proof hints for bvext equalities is TBD\n"); + } + break; + } m_lit_head = m_lit_tail; @@ -505,6 +520,8 @@ namespace bv { th = "bit2ne"; break; case bv_justification::kind_t::bv2int: th = "bv2int"; break; + case bv_justification::kind_t::bvext: + th = "bvext"; break; } func_decl* f = m.mk_func_decl(th, sorts.size(), sorts.data(), proof); return m.mk_app(f, args); @@ -962,6 +979,14 @@ namespace bv { return jst; } + sat::ext_constraint_idx solver::mk_bv2ext_justification(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) { + void* mem = get_region().allocate(bv_justification::get_obj_size(lits.size(), eqs.size())); + sat::constraint_base::initialize(mem, this); + auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(lits, eqs); + auto jst = constraint->to_index(); + return jst; + } + bool solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) { m_stats.m_num_eq2bit++; SASSERT(ctx.s().value(antecedent) == l_true); @@ -1055,4 +1080,22 @@ namespace bv { return m_power2[i]; } + solver::bv_justification::bv_justification(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs): + m_kind(bv_justification::kind_t::bvext), + //m_consequent(sat::null_literal), + //m_eq(euf::enode_pair()), + m_num_literals(lits.size()), + m_num_eqs(eqs.size()) + { + char* base_ptr = reinterpret_cast(this) + sizeof(bv_justification); + m_literals = reinterpret_cast(base_ptr); + unsigned i; + for (i = 0; i < lits.size(); ++i) + m_literals[i] = lits[i]; + base_ptr += sizeof(literal) * lits.size(); + m_eqs = reinterpret_cast(base_ptr); + for (i = 0; i < eqs.size(); ++i) + m_eqs[i] = eqs[i]; + } + } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index d6deae7c5..f9097cb32 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -64,25 +64,41 @@ namespace bv { }; struct bv_justification { - enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne, bv2int }; + enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne, bv2int, bvext }; kind_t m_kind; - unsigned m_idx = UINT_MAX; - theory_var m_v1 = euf::null_theory_var; - theory_var m_v2 = euf::null_theory_var; - sat::literal m_consequent; - sat::literal m_antecedent; - euf::enode* a, *b, *c; + union { + // for eq2bit, ne2bit, bit2eq, bit2ne, bv2int: + struct { + unsigned m_idx; + theory_var m_v1; + theory_var m_v2; + sat::literal m_consequent; + sat::literal m_antecedent; + euf::enode* a, *b, *c; + }; + // for bvext: + struct { + // sat::literal m_consequent; // literal consequent for propagations + // euf::enode_pair m_eq; // equality consequent for propagations + unsigned m_num_literals; + unsigned m_num_eqs; + sat::literal* m_literals; + euf::enode_pair* m_eqs; + }; + }; + bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) : - m_kind(bv_justification::kind_t::eq2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {} + m_kind(bv_justification::kind_t::eq2bit), m_idx(UINT_MAX), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {} bv_justification(theory_var v1, theory_var v2): - m_kind(bv_justification::kind_t::bit2eq), m_v1(v1), m_v2(v2) {} + m_kind(bv_justification::kind_t::bit2eq), m_idx(UINT_MAX), m_v1(v1), m_v2(v2) {} bv_justification(unsigned idx, sat::literal c) : m_kind(bv_justification::kind_t::bit2ne), m_idx(idx), m_consequent(c) {} bv_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a) : m_kind(bv_justification::kind_t::ne2bit), m_idx(idx), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {} bv_justification(theory_var v1, theory_var v2, euf::enode* a, euf::enode* b, euf::enode* c): - m_kind(bv_justification::kind_t::bv2int), m_v1(v1), m_v2(v2), a(a), b(b), c(c) {} + m_kind(bv_justification::kind_t::bv2int), m_idx(UINT_MAX), m_v1(v1), m_v2(v2), a(a), b(b), c(c) {} + bv_justification(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs); sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } @@ -90,6 +106,11 @@ namespace bv { return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); } static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(bv_justification)); } + + static size_t get_obj_size(unsigned num_lits, unsigned num_eqs) { + return sat::constraint_base::obj_size(sizeof(bv_justification) + sizeof(sat::literal) * num_lits + sizeof(euf::enode_pair) * num_eqs); + } + }; sat::justification mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a); @@ -97,6 +118,7 @@ namespace bv { sat::justification mk_bit2ne_justification(unsigned idx, sat::literal c); sat::justification mk_ne2bit_justification(unsigned idx, theory_var v1, theory_var v2, sat::literal c, sat::literal a); sat::ext_constraint_idx mk_bv2int_justification(theory_var v1, theory_var v2, euf::enode* a, euf::enode* b, euf::enode* c); + sat::ext_constraint_idx mk_bv2ext_justification(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs); void log_drat(bv_justification const& c); class proof_hint : public euf::th_proof_hint { bv_justification::kind_t m_kind;