From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Apr 2020 16:42:00 +0000 (-0500)
Subject: Remove mergePredicates from EqualityEngine interface (#4305)
X-Git-Tag: cvc5-1.0.0~3380
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf8d103b11261d3b4425dab74008dffd903b8121;p=cvc5.git

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 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.
    *