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, 13 insertions, 0 deletions

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;
 
 /**
@@ -124,6 +129,11 @@ class TheoryEngine {
   SharedTermsDatabase d_sharedTerms;
 
   /**
+   * Master equality engine, to share with theories.
+   */
+  theory::eq::EqualityEngine* d_masterEqualityEngine;
+
+  /**
    * The quantifiers engine
    */
   theory::QuantifiersEngine* d_quantEngine;
@@ -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.
    */