Adding support for a master equality engine. Each theory gets the master equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().

4 files changed, 12 insertions, 0 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 09410f15b..5ee250c09 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -65,6 +65,10 @@ ArithCongruenceManager::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_conflicts);
 }
 
+void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_ee.setMasterEqualityEngine(eq);
+}
+
 void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){
   Assert(lb->isLowerBound());
   Assert(ub->isUpperBound());
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 502ea5cf0..5e2c80a63 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -144,6 +144,8 @@ public:
     return d_explanationMap.find(n) != d_explanationMap.end();
   }
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
 private:
   Node externalToInternal(TNode n) const{
     Assert(canExplain(n));
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 141b22dc6..6ec6c7090 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -91,6 +91,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
 
 TheoryArith::~TheoryArith(){}
 
+void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_congruenceManager.setMasterEqualityEngine(eq);
+}
+
 Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
   NodeManager* currNM = NodeManager::currentNM();
   TypeNode functionType = currNM->mkFunctionType(dom, range);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0773ab7ba..ad041208d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -341,6 +341,8 @@ public:
    */
   void preRegisterTerm(TNode n);
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void check(Effort e);
   void propagate(Effort e);
   Node explain(TNode n);