mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 06:01:26 +00:00
Code Activity

add delayed diseq check

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-11-07 08:03:37 -08:00
parent daf66e63c6
commit a3ec6a0f1b
1 changed files with 25 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/theory_lra.cpp
View file

@ -1012,10 +1012,30 @@ public:
return true; return true;
} }
svector<std::pair<theory_var, theory_var>> m_delayed_diseqs;
void new_diseq_eh(theory_var v1, theory_var v2) { void new_diseq_eh(theory_var v1, theory_var v2) {
TRACE(arith, tout << "v" << v1 << " != " << "v" << v2 << "\n";); TRACE(arith, tout << "v" << v1 << " != " << "v" << v2 << "\n";);
#if 1
m_delayed_diseqs.push_back({v1, v2});
ctx().push_trail(push_back_vector(m_delayed_diseqs));
#else
++m_stats.m_assert_diseq; ++m_stats.m_assert_diseq;
m_arith_eq_adapter.new_diseq_eh(v1, v2); m_arith_eq_adapter.new_diseq_eh(v1, v2);
#endif
}
bool check_delayed_diseqs() {
bool found_eq = false;
for (auto [v1, v2] : m_delayed_diseqs) {
if (is_eq(v1, v2)) {
found_eq = true;
++m_stats.m_assert_diseq;
m_arith_eq_adapter.new_diseq_eh(v1, v2);
}
}
return found_eq;
} }
void apply_sort_cnstr(enode* n, sort*) { void apply_sort_cnstr(enode* n, sort*) {
@ -1668,6 +1688,10 @@ public:
break; break;
} }
if (check_delayed_diseqs())
return FC_CONTINUE;
if (assume_eqs()) { if (assume_eqs()) {
++m_stats.m_assume_eqs; ++m_stats.m_assume_eqs;
return FC_CONTINUE; return FC_CONTINUE;