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

arrays are not necessarily unary

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-18 19:13:12 -08:00
parent a5e5a35755
commit a4a84ed083
1 changed files with 16 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -378,25 +378,27 @@ struct mbp_array_tg::impl {
mark_seen(term); mark_seen(term);
} }
} }
if (!m_use_mdl) return progress; if (!m_use_mdl)
expr *e1, *e2, *a1, *a2, *i1, *i2; return progress;
for (unsigned i = 0; i < rdTerms.size(); i++) { for (unsigned i = 0; i < rdTerms.size(); i++) {
e1 = rdTerms.get(i); app* e1 = to_app(rdTerms.get(i));
a1 = to_app(e1)->get_arg(0); expr* a1 = e1->get_arg(0);
i1 = to_app(e1)->get_arg(1);
for (unsigned j = i + 1; j < rdTerms.size(); j++) { for (unsigned j = i + 1; j < rdTerms.size(); j++) {
e2 = rdTerms.get(j); app* e2 = to_app(rdTerms.get(j));
a2 = to_app(e2)->get_arg(0); expr* a2 = e2->get_arg(0);
i2 = to_app(e2)->get_arg(1); if (!is_seen(e1, e2) && a1 == e2) {
if (!is_seen(e1, e2) && a1->get_id() == a2->get_id()) {
mark_seen(e1, e2); mark_seen(e1, e2);
progress = true; progress = true;
if (m_mdl.are_equal(i1, i2)) { for (unsigned k = 1; k < e1->get_num_args(); ++k) {
expr* i1 = e1->get_arg(k);
expr* i2 = e2->get_arg(k);
if (m_mdl.are_equal(i1, i2))
m_tg.add_eq(i1, i2); m_tg.add_eq(i1, i2);
} else { else {
SASSERT(!m_mdl.are_equal(i1, i2)); SASSERT(!m_mdl.are_equal(i1, i2));
m_tg.add_deq(i1, i2); m_tg.add_deq(i1, i2);
} }
}
continue; continue;
} }
} }