adding mergePredicates method to the equality engine to be able to

assert equalities betweeen predicates 

2 files changed, 13 insertions, 0 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 6cef3dff5..97dcbad86 100644
--- 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 e32a34707..5d5e0f1f3 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -697,6 +697,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.
    *
    * @param eq the (non-negated) equality