From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 26 Nov 2012 17:07:46 +0000 (+0000)
Subject: Adding support for a master equality engine. Each theory gets the master equality... 
X-Git-Tag: cvc5-1.0.0~7559
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a731b9164bb178f1232a9af0babc7dd84450cea;p=cvc5.git

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().
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7c913578b..03834825d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -554,6 +554,7 @@ void SmtEngine::finishInit() {
 
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
+  d_theoryEngine->finishInit();
 
   // [MGD 10/20/2011] keep around in incremental mode, due to a
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
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);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f40fea0ba..b8c1ace4b 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -111,7 +111,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   }
 }
 
-
 TheoryArrays::~TheoryArrays() {
 
   StatisticsRegistry::unregisterStat(&d_numRow);
@@ -124,6 +123,10 @@ TheoryArrays::~TheoryArrays() {
 
 }
 
+void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 
 /////////////////////////////////////////////////////////////////////////////
 // PREPROCESSING
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index eaa3ca431..240cfad9a 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -123,6 +123,8 @@ class TheoryArrays : public Theory {
   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryArrays();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   std::string identify() const { return std::string("TheoryArrays"); }
 
   /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 17ea7034b..ca3e3e35c 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -67,6 +67,10 @@ EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   }
 }
 
+void EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 void EqualitySolver::preRegister(TNode node) {
   if (!d_useEqualityEngine)
     return;
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index 64fe12706..2b024cfd4 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -63,7 +63,7 @@ class EqualitySolver : public SubtheorySolver {
 public:
 
   EqualitySolver(context::Context* c, TheoryBV* bv);
-
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
   void  preRegister(TNode node);
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a37ed59c8..7acb93cc2 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -50,6 +50,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
 
 TheoryBV::~TheoryBV() {}
 
+
+void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalitySolver.setMasterEqualityEngine(eq);
+}
+
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 933fd8700..0c8df3fca 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -50,6 +50,8 @@ public:
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryBV();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void preRegisterTerm(TNode n);
 
   void check(Effort e);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6b576cba8..8ec45efb9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -56,6 +56,10 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 TheoryDatatypes::~TheoryDatatypes() {
 }
 
+void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake ){
   std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
   if( !hasEqcInfo( n ) ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 16e403e95..5cda9eeae 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -179,6 +179,9 @@ public:
   TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation,
                   const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryDatatypes();
+
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   /** propagate */
   void propagate(Effort effort);
   /** propagate */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6e704ba1c..446c9285e 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -36,17 +36,22 @@ using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
-  d_numRestarts(0){
+  d_numRestarts(0),
+  d_masterEqualityEngine(0)
+{
   d_numInstantiations = 0;
   d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
 }
 
-
 TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
+void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_masterEqualityEngine = eq;
+}
+
 void TheoryQuantifiers::addSharedTerm(TNode t) {
   Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
                      << t << endl;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 7b050bb1c..12b735497 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -31,6 +31,7 @@ namespace CVC4 {
 class TheoryEngine;
 
 namespace theory {
+
 namespace quantifiers {
 
 class ModelEngine;
@@ -49,10 +50,14 @@ private:
 
   KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime");
 
+  eq::EqualityEngine* d_masterEqualityEngine;
+
 public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryQuantifiers();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void preRegisterTerm(TNode n);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 95fe03c82..4d535a8af 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -54,6 +54,10 @@ namespace rrinst{
 class CandidateGenerator;
 }
 
+namespace eq {
+class EqualityEngine;
+}
+
 /**
  * Information about an assertion for the theories.
  */
@@ -246,7 +250,8 @@ protected:
    * Construct a Theory.
    */
   Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
-         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) throw()
+         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
+         QuantifiersEngine* qe, eq::EqualityEngine* master = 0) throw()
   : d_id(id)
   , d_satContext(satContext)
   , d_userContext(userContext)
@@ -514,6 +519,11 @@ public:
    */
   virtual void addSharedTerm(TNode n) { }
 
+  /**
+   * Called to set the master equality engine.
+   */
+  virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { }
+
   /**
    * Return the current theory care graph. Theories should overload computeCareGraph to do
    * the actual computation, and use addCarePair to add pairs to the care graph.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4b4316db1..cd3b34879 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,12 +42,26 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 
+#include "theory/uf/equality_engine.h"
 
 using namespace std;
 
 using namespace CVC4;
 using namespace CVC4::theory;
 
+void TheoryEngine::finishInit() {
+  if (d_logicInfo.isQuantified()) {
+    Assert(d_masterEqualityEngine == 0);
+    d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master");
+
+    for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+      if (d_theoryTable[theoryId]) {
+        d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
+      }
+    }
+  }
+}
+
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveITE& iteRemover,
@@ -58,6 +72,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_userContext(userContext),
   d_logicInfo(logicInfo),
   d_sharedTerms(this, context),
+  d_masterEqualityEngine(NULL),
   d_quantEngine(NULL),
   d_curr_model(NULL),
   d_curr_model_builder(NULL),
@@ -114,6 +129,8 @@ TheoryEngine::~TheoryEngine() {
 
   delete d_quantEngine;
 
+  delete d_masterEqualityEngine;
+
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 }
 
@@ -229,21 +246,6 @@ void TheoryEngine::dumpAssertions(const char* tag) {
   }
 }
 
-
-template<typename T, bool doAssert>
-class scoped_vector_clear {
-  vector<T>& d_v;
-public:
-  scoped_vector_clear(vector<T>& v)
-  : d_v(v) {
-    Assert(!doAssert || d_v.empty());
-  }
-  ~scoped_vector_clear() {
-    d_v.clear();
-  }
-
-};
-
 /**
  * Check all (currently-active) theories for conflicts.
  * @param effort the effort level to use
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d6e984f8f..de872db42 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -76,8 +76,13 @@ namespace theory {
   class Instantiator;
   class TheoryModel;
   class TheoryEngineModelBuilder;
+
+  namespace eq {
+    class EqualityEngine;
+  }
 }/* CVC4::theory namespace */
 
+
 class DecisionEngine;
 
 /**
@@ -123,6 +128,11 @@ class TheoryEngine {
    */
   SharedTermsDatabase d_sharedTerms;
 
+  /**
+   * Master equality engine, to share with theories.
+   */
+  theory::eq::EqualityEngine* d_masterEqualityEngine;
+
   /**
    * The quantifiers engine
    */
@@ -428,6 +438,9 @@ public:
     d_decisionEngine = decisionEngine;
   }
 
+  /** Called when all initialization of options/logic is done */
+  void finishInit();
+
   /**
    * Get a pointer to the underlying propositional engine.
    */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 90de8d0d2..636427ed1 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -79,8 +79,9 @@ EqualityEngine::~EqualityEngine() throw(AssertionException) {
 }
 
 
-EqualityEngine::EqualityEngine(context::Context* context, std::string name) 
+EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 : ContextNotifyObj(context)
+, d_masterEqualityEngine(0)
 , d_context(context)
 , d_done(context, false)
 , d_performNotify(true)
@@ -102,6 +103,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 
 EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name)
 : ContextNotifyObj(context)
+, d_masterEqualityEngine(0)
 , d_context(context)
 , d_done(context, false)
 , d_performNotify(true)
@@ -121,6 +123,11 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
   init();
 }
 
+void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
+  Assert(d_masterEqualityEngine == 0);
+  d_masterEqualityEngine = master;
+}
+
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
   Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
   if (back) {
@@ -294,6 +301,11 @@ void EqualityEngine::addTerm(TNode t) {
     d_nodeIndividualTrigger[tId] = newTriggerTermSet();
   }
 
+  // If this is not an internal node, add it to the master
+  if (d_masterEqualityEngine && !d_isInternal[result]) {
+    d_masterEqualityEngine->addTerm(t);
+  }
+
   propagate();
 
   Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl;
@@ -1213,9 +1225,34 @@ void EqualityEngine::propagate() {
       continue;
     }
 
-    // Depending on the merge preference (such as size, or being a constant), merge them
+    // Vector to collect the triggered events
     std::vector<TriggerId> triggers;
-    if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) {
+
+    // Figure out the merge preference
+    EqualityNodeId mergeInto = t1classId;
+    if (d_isInternal[t2classId] != d_isInternal[t1classId]) {
+      // We always keep non-internal nodes as representatives: if any node in
+      // the class is non-internal, then the representative will be non-internal
+      if (d_isInternal[t1classId]) {
+        mergeInto = t2classId;
+      } else {
+        mergeInto = t1classId;
+      }
+    } else if (d_isConstant[t2classId] != d_isConstant[t1classId]) {
+      // We always keep constants as representatives: if any (at most one) node
+      // in the class in a constant, then the representative will be a constant
+      if (d_isConstant[t2classId]) {
+        mergeInto = t2classId;
+      } else {
+        mergeInto = t1classId;
+      }
+    } else if (node2.getSize() > node1.getSize()) {
+      // We always merge into the bigger class to reduce the amount of traversing
+      // we need to do
+      mergeInto = t2classId;
+    }
+
+    if (mergeInto == t2classId) {
       Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
       d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
@@ -1231,6 +1268,12 @@ void EqualityEngine::propagate() {
       }
     }
 
+    // If not merging internal nodes, notify the master
+    if (d_masterEqualityEngine && !d_isInternal[mergeInto]) {
+      d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null());
+      d_masterEqualityEngine->propagate();
+    }
+
     // Notify the triggers
     if (d_performNotify && !d_done) {
       for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 166362951..9bc2cb61c 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -151,8 +151,35 @@ class EqualityEngine : public context::ContextNotifyObj {
   /** Default implementation of the notification object */
   static EqualityEngineNotifyNone s_notifyNone;
 
+  /**
+   * Master equality engine that gets all the equality information from
+   * this one, or null if none.
+   */
+  EqualityEngine* d_masterEqualityEngine;
+
 public:
 
+  /**
+   * Initialize the equality engine, given the notification class.
+   */
+  EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
+
+  /**
+   * Initialize the equality engine with no notification class.
+   */
+  EqualityEngine(context::Context* context, std::string name);
+
+  /**
+   * Just a destructor.
+   */
+  virtual ~EqualityEngine() throw(AssertionException);
+
+  /**
+   * Set the master equality engine for this one. Master engine will get copies of all
+   * the terms and equalities from this engine.
+   */
+  void setMasterEqualityEngine(EqualityEngine* master);
+
   /** Statistics about the equality engine instance */
   struct Statistics {
     /** Total number of merges */
@@ -639,21 +666,6 @@ private:
 
 public:
 
-  /**
-   * Initialize the equality engine, given the notification class.
-   */
-  EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
-
-  /**
-   * Initialize the equality engine with no notification class.
-   */
-  EqualityEngine(context::Context* context, std::string name);
-
-  /**
-   * Just a destructor.
-   */
-  virtual ~EqualityEngine() throw(AssertionException);
-
   /**
    * Adds a term to the term database.
    */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d76d95adb..e6ae3747c 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -45,6 +45,10 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
 
+void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
   Assert(conjunctions.size() > 0);
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f30619e2e..46a17a5e0 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -187,6 +187,8 @@ public:
     }
   }
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void check(Effort);
   void preRegisterTerm(TNode term);
   Node explain(TNode n);