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

throttle equality propagation to shared expressions

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-19 04:51:00 -08:00
parent 7c34a54e8a
commit 95d98ea8ce
2 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/arith_solver.cpp
View file

@ -307,7 +307,13 @@ namespace arith {
return;
enode* n1 = var2enode(uv);
enode* n2 = var2enode(vv);
if (m.get_sort(n1->get_expr()) != m.get_sort(n2->get_expr()))
if (!ctx.is_shared(n1) || !ctx.is_shared(n2))
return;
expr* e1 = n1->get_expr();
expr* e2 = n2->get_expr();
if (m.is_ite(e1) || m.is_ite(e2))
return;
if (m.get_sort(e1) != m.get_sort(e2))
return;
reset_evidence();
for (auto const& ev : e)

13
src/smt/theory_lra.cpp
View file

@ -2289,8 +2289,15 @@ public:
theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
enode* n1 = get_enode(uv);
enode* n2 = get_enode(vv);
if (n1->get_root() == n2->get_root() ||
m.get_sort(n1->get_owner()) != m.get_sort(n2->get_owner()))
if (n1->get_root() == n2->get_root())
return;
if (!ctx().is_shared(n1) || !ctx().is_shared(n2))
return;
expr* e1 = n1->get_owner();
expr* e2 = n2->get_owner();
if (m.get_sort(e1) != m.get_sort(e2))
return;
if (m.is_ite(e1) || m.is_ite(e2))
return;
reset_evidence();
for (auto const& ev : e)
@ -2299,7 +2306,7 @@ public:
ext_theory_eq_propagation_justification(
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), n1, n2));
std::function<expr*(void)> fn = [&]() { return m.mk_eq(n1->get_owner(), n2->get_owner()); };
std::function<expr*(void)> fn = [&]() { return m.mk_eq(e1, e2); };
scoped_trace_stream _sts(th, fn);
ctx().assign_eq(n1, n2, eq_justification(js));
}