mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix types and incompleteness for feature #6104

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-06 01:08:54 -07:00
parent bda86726af
commit 580ed31afd
2 changed files with 18 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -211,30 +211,20 @@ namespace bv {
return; return;
} }
euf::enode* n1 = var2enode(eq.v1()); euf::enode* n1 = var2enode(eq.v1());
euf::enode* int2bv = nullptr; for (euf::enode* bv2int : euf::enode_class(n1)) {
for (euf::enode* sib : euf::enode_class(n1)) { if (!bv.is_bv2int(bv2int->get_expr()))
if (bv.is_bv2int(sib->get_expr())) { continue;
int2bv = sib; euf::enode* bv2int_arg = bv2int->get_arg(0);
break; for (euf::enode* p : euf::enode_parents(n1->get_root())) {
} if (bv.is_int2bv(p->get_expr()) && p->get_sort() == bv2int_arg->get_sort() && p->get_root() != bv2int_arg->get_root()) {
}
if (!int2bv)
return;
for (euf::enode* p : euf::enode_parents(n1->get_root())) {
if (bv.is_int2bv(p->get_expr())) {
euf::enode* int2bv_arg = int2bv->get_arg(0);
if (p->get_root() != int2bv_arg->get_root()) {
euf::enode_pair_vector eqs; euf::enode_pair_vector eqs;
eqs.push_back({ n1, p->get_arg(0) }); eqs.push_back({ n1, p->get_arg(0) });
eqs.push_back({ n1, int2bv }); eqs.push_back({ n1, bv2int });
ctx.propagate(p, int2bv_arg, euf::th_explain::propagate(*this, eqs, p, int2bv_arg)); ctx.propagate(p, bv2int_arg, euf::th_explain::propagate(*this, eqs, p, bv2int_arg));
break; break;
} }
} }
} }
} }
void solver::new_diseq_eh(euf::th_eq const& ne) { void solver::new_diseq_eh(euf::th_eq const& ne) {

28
src/smt/theory_bv.cpp
View file

@ -1497,32 +1497,24 @@ namespace smt {
bool changed = true; bool changed = true;
TRACE("bv", tout << "bits size: " << sz << "\n";); TRACE("bv", tout << "bits size: " << sz << "\n";);
if (sz == 0) { if (sz == 0) {
// int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
enode* n1 = get_enode(r1); enode* n1 = get_enode(r1);
enode* int2bv = nullptr; for (enode* bv2int : *n1) {
for (enode* sib : *n1) { if (!m_util.is_bv2int(bv2int->get_expr()))
if (m_util.is_bv2int(sib->get_expr())) { continue;
int2bv = sib; enode* bv2int_arg = bv2int->get_arg(0);
break; for (enode* p : enode::parents(n1->get_root())) {
} if (m_util.is_int2bv(p->get_expr()) && p->get_root() != bv2int_arg->get_root() && p->get_sort() == bv2int_arg->get_sort()) {
}
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; enode_pair_vector eqs;
eqs.push_back({n1, p->get_arg(0) }); eqs.push_back({n1, p->get_arg(0) });
eqs.push_back({n1, int2bv}); eqs.push_back({n1, bv2int});
justification * js = ctx.mk_justification( justification * js = ctx.mk_justification(
ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, int2bv_arg)); ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));
ctx.assign_eq(p, int2bv_arg, eq_justification(js)); ctx.assign_eq(p, bv2int_arg, eq_justification(js));
break; break;
} }
} }
} }
} }
do { do {
// This outerloop is necessary to avoid missing propagation steps. // This outerloop is necessary to avoid missing propagation steps.