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, 11 insertions, 1 deletions

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)
@@ -515,6 +520,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.
    */