adding mergePredicates method to the equality engine to be able to

assert equalities betweeen predicates

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 6cef3dff51e4538a5536983a96a3ba9c88905dec..97dcbad86ab55d40f0fd05a9712aae11426959a6 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -353,6 +353,14 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) {
   propagate();
 }
 
+void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
+  Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl;
+  Assert(p.getKind() != kind::EQUAL, "Use assertEquality instead");
+  Assert(q.getKind() != kind::EQUAL, "Use assertEquality instead");
+  assertEqualityInternal(p, q, reason);
+  propagate();
+}
+
 void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
   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 e32a347072ebd442547b8f9e0222ddd2cbb18b01..5d5e0f1f321a658428a056251684f1d7012ab6da 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -696,6 +696,11 @@ public:
    */
   void assertPredicate(TNode p, bool polarity, TNode reason);
 
+  /**
+   * 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.
    *