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

1 files changed, 5 insertions, 0 deletions

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);