diff options
| -rw-r--r-- | src/theory/theory_model.cpp | 6 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 6 | ||||
| -rw-r--r-- | 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 @@ -804,11 +804,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. * * @param eq the (non-negated) equality |