From cf8d103b11261d3b4425dab74008dffd903b8121 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Apr 2020 11:42:00 -0500 Subject: [PATCH] Remove mergePredicates from EqualityEngine interface (#4305) This function was equivalent to asserting an equality. Removing it for the sake of simplicity. --- src/theory/theory_model.cpp | 6 ++++-- src/theory/uf/equality_engine.cpp | 6 ------ src/theory/uf/equality_engine.h | 5 ----- 3 files changed, 4 insertions(+), 13 deletions(-) diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index dae7261e5..e96bee410 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -483,8 +483,10 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, first = false; } else { - Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; - d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null()); + Node eq = (*eqc_i).eqNode(rep); + Trace("model-builder-assertions") + << "(assert " << eq << ");" << std::endl; + d_equalityEngine->assertEquality(eq, true, Node::null()); if (!d_equalityEngine->consistent()) { return false; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index b6896e45d..e3d002138 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -449,12 +449,6 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig propagate(); } -void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { - Debug("equality") << d_name << "::eq::mergePredicates(" << p << "," << q << ")" << std::endl; - assertEqualityInternal(p, q, reason); - propagate(); -} - void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 041625568..0ae95b34a 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -803,11 +803,6 @@ public: */ void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); - /** - * Adds predicate p and q and makes them equal. - */ - void mergePredicates(TNode p, TNode q, TNode reason); - /** * Adds an equality eq with the given polarity to the database. * -- 2.30.2