From 8849cef4b7ece99d83cb1f353149743270f4626c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jun 2020 15:33:52 -0700 Subject: [PATCH] add stub for equality propagation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 541e90397..8775785b3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2357,6 +2357,10 @@ public: return m_imp.bound_is_interesting(j, kind, v); } + void add_eq(lpvar u, lpvar v, lp::explanation const& e) { + m_imp.add_eq(u, v, e); + } + void consume(rational const& v, lp::constraint_index j) override { m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs); m_imp.m_explanation.add_pair(j, v); @@ -2419,6 +2423,26 @@ public: } } + void add_eq(lpvar u, lpvar v, lp::explanation const& e) { + theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations + 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 == n2) + return; + reset_evidence(); + for (auto const& ev : e) + set_evidence(ev.ci(), m_core, m_eqs); + justification* js = ctx().mk_justification( + 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()); }; + scoped_trace_stream _sts(th, fn); + ctx().assign_eq(n1, n2, eq_justification(js)); + } + + literal_vector m_core2; void assign(literal lit, literal_vector const& core, svector const& eqs, vector const& params) {