mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 09:50:23 +00:00
Code Activity

fix #6104

Browse source 
add equality reasoning to bit-vector solver to instantiate int2bv(bv2int(x)) = x identity on demand.
This commit is contained in:
Nikolaj Bjorner 2022-07-05 12:23:24 -07:00
parent 282c786f1c
commit de41cfd277
1 changed files with 33 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/smt/theory_bv.cpp
View file

@ -52,9 +52,8 @@ namespace smt {
bits.reset(); bits.reset();
m_bits_expr.reset(); m_bits_expr.reset();
for (unsigned i = 0; i < bv_size; i++) { for (unsigned i = 0; i < bv_size; i++)
m_bits_expr.push_back(mk_bit2bool(owner, i)); m_bits_expr.push_back(mk_bit2bool(owner, i));
}
ctx.internalize(m_bits_expr.data(), bv_size, true); ctx.internalize(m_bits_expr.data(), bv_size, true);
for (unsigned i = 0; i < bv_size; i++) { for (unsigned i = 0; i < bv_size; i++) {
@ -601,9 +600,8 @@ namespace smt {
TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";); TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";);
process_args(n); process_args(n);
mk_enode(n); mk_enode(n);
if (!ctx.relevancy()) { if (!ctx.relevancy())
assert_bv2int_axiom(n); assert_bv2int_axiom(n);
}
} }
@ -669,10 +667,11 @@ namespace smt {
mk_enode(n); mk_enode(n);
theory_var v = ctx.get_enode(n)->get_th_var(get_id()); theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v); mk_bits(v);
mk_var(ctx.get_enode(n->get_arg(0)));
if (!ctx.relevancy()) {
if (!ctx.relevancy())
assert_int2bv_axiom(n); assert_int2bv_axiom(n);
}
} }
void theory_bv::assert_int2bv_axiom(app* n) { void theory_bv::assert_int2bv_axiom(app* n) {
@ -1497,6 +1496,34 @@ namespace smt {
unsigned sz = m_bits[v1].size(); unsigned sz = m_bits[v1].size();
bool changed = true; bool changed = true;
TRACE("bv", tout << "bits size: " << sz << "\n";); TRACE("bv", tout << "bits size: " << sz << "\n";);
if (sz == 0) {
enode* n1 = get_enode(r1);
enode* int2bv = nullptr;
for (enode* sib : *n1) {
if (m_util.is_bv2int(sib->get_expr())) {
int2bv = sib;
break;
}
}
if (!int2bv)
return;
for (enode* p : enode::parents(n1->get_root())) {
if (m_util.is_int2bv(p->get_expr())) {
enode* int2bv_arg = int2bv->get_arg(0);
if (p->get_root() != int2bv_arg->get_root()) {
enode_pair_vector eqs;
eqs.push_back({n1, p->get_arg(0) });
eqs.push_back({n1, int2bv});
justification * js = ctx.mk_justification(
ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, int2bv_arg));
ctx.assign_eq(p, int2bv_arg, eq_justification(js));
break;
}
}
}
}
do { do {
// This outerloop is necessary to avoid missing propagation steps. // This outerloop is necessary to avoid missing propagation steps.
// For example, let's assume that bits1 and bits2 contains the following // For example, let's assume that bits1 and bits2 contains the following