mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity

create proper extract terms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-14 10:37:55 -08:00
parent 60ac9388c8
commit 8f3e8bd0bb
2 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_bv_plugin.cpp
View file

@ -171,7 +171,9 @@ namespace euf {
if (is_extract(p, lo, hi)) {
auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
push_merge(mk_extract(x->get_interpreted(), lo, hi), mk_value(val_p, width(p)));
auto ix = x->get_interpreted();
auto ex = mk(bv.mk_extract(hi, lo, ix->get_expr()), 1, &ix);
push_merge(ex, mk_value(val_p, width(p)));
}
}

14
src/ast/euf/euf_egraph.cpp
View file

@ -69,7 +69,7 @@ namespace euf {
}
enode_bool_pair egraph::insert_table(enode* p) {
TRACE("euf", tout << "insert_table " << bpp(p) << "\n");
TRACE("euf_verbose", tout << "insert_table " << bpp(p) << "\n");
//SASSERT(!m_table.contains_ptr(p));
auto rc = m_table.insert(p);
p->m_cg = rc.first;
@ -522,7 +522,7 @@ namespace euf {
}
void egraph::remove_parents(enode* r) {
TRACE("euf", tout << bpp(r) << "\n");
TRACE("euf_verbose", tout << bpp(r) << "\n");
SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
for (enode* p : enode_parents(r)) {
if (p->is_marked1())
@ -533,7 +533,7 @@ namespace euf {
SASSERT(m_table.contains_ptr(p));
p->mark1();
erase_from_table(p);
CTRACE("euf", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
CTRACE("euf_verbose", m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
SASSERT(!m_table.contains_ptr(p));
}
else if (p->is_equality())
@ -546,11 +546,11 @@ namespace euf {
if (!p->is_marked1())
continue;
p->unmark1();
TRACE("euf", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
TRACE("euf_verbose", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
if (p->cgc_enabled()) {
auto [p_other, comm] = insert_table(p);
SASSERT(m_table.contains_ptr(p) == (p_other == p));
CTRACE("euf", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
CTRACE("euf_verbose", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
if (p_other != p)
m_to_merge.push_back(to_merge(p_other, p, comm));
else
@ -584,14 +584,14 @@ namespace euf {
void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
enode* r2 = r1->get_root();
TRACE("euf", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
TRACE("euf_verbose", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
r2->dec_class_size(r1->class_size());
r2->set_is_shared(l_undef);
std::swap(r1->m_next, r2->m_next);
auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents();
for (auto it = begin; it != end; ++it) {
enode* p = *it;
TRACE("euf", tout << "erase " << bpp(p) << "\n";);
TRACE("euf_verbose", tout << "erase " << bpp(p) << "\n";);
SASSERT(!p->cgc_enabled() || m_table.contains_ptr(p));
SASSERT(!p->cgc_enabled() || p->is_cgr());
if (p->cgc_enabled())