mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

add propagation justification to bv antecedents

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-23 17:52:34 -08:00
parent 9b274f349b
commit 706d542eeb
3 changed files with 76 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/bv_polysat.cpp
View file

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

43
src/sat/smt/bv_solver.cpp
View file

@ -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<char*>(this) + sizeof(bv_justification);
m_literals = reinterpret_cast<literal*>(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<euf::enode_pair*>(base_ptr);
for (i = 0; i < eqs.size(); ++i)
m_eqs[i] = eqs[i];
}
}

42
src/sat/smt/bv_solver.h
View file

@ -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<bv_justification*>(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;