Remove mergePredicates from EqualityEngine interface (#4305)

This function was equivalent to asserting an equality. Removing it for the sake of simplicity.

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index dae7261e500d2937c7369b7583752e7bdd9e8e50..e96bee4103569c88bc3207f527346f48efa2eec9 100644 (file)
--- 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 b6896e45d6510259ea6bd91fac9556b020eb5102..e3d0021387acdb50d8107f8a41b9760f0b134b0e 100644 (file)
--- 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 041625568d27868e4d5b54abe2277f4c047b9bf1..0ae95b34a0670c6b3a1cfb59514a86970337fb0a 100644 (file)
--- 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.
    *