Support E-matching/QCF for Set operators.

4 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 3a5b61390..c230b9ac5 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,6 +34,10 @@ TheorySets::~TheorySets() {
   delete d_internal;
 }
 
+void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_internal->setMasterEqualityEngine(eq);
+}
+
 void TheorySets::addSharedTerm(TNode n) {
   d_internal->addSharedTerm(n);
 }
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 9f74064cb..6ff41d5f5 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -48,6 +48,8 @@ public:
 
   ~TheorySets();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  
   void addSharedTerm(TNode);
 
   void check(Effort);
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index af96b50d0..8c9441483 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -880,6 +880,10 @@ bool TheorySetsPrivate::propagate(TNode literal) {
 }/* TheorySetsPropagate::propagate(TNode) */
 
 
+void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 void TheorySetsPrivate::addSharedTerm(TNode n) {
   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 73c0c419e..90dec7c0b 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -47,6 +47,8 @@ public:
                     context::UserContext* u);
 
   ~TheorySetsPrivate();
+  
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
   void addSharedTerm(TNode);