From 95d98ea8ced65d9c9e34b034a7a8f3ac4c6bd400 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Jan 2021 04:51:00 -0800 Subject: [PATCH] throttle equality propagation to shared expressions --- src/sat/smt/arith_solver.cpp | 8 +++++++- src/smt/theory_lra.cpp | 13 ++++++++++--- 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index a99c00b6377..6960fe44425 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -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) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 06114d6de85..5abef0480c2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2289,8 +2289,15 @@ class theory_lra::imp { 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 @@ class theory_lra::imp { 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 fn = [&]() { return m.mk_eq(n1->get_owner(), n2->get_owner()); }; + std::function fn = [&]() { return m.mk_eq(e1, e2); }; scoped_trace_stream _sts(th, fn); ctx().assign_eq(n1, n2, eq_justification(js)); }