Added shared term manager. Basic mechanism for identifying shared terms is

working.  Still need to implement theory-specific shared term propagation.

1 files changed, 37 insertions, 8 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index bcb2d011b..6da47fbd8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -136,6 +136,11 @@ private:
   Theory();
 
   /**
+   * A unique integer identifying the theory
+   */
+  int d_id;
+
+  /**
    * The context for the Theory.
    */
   context::Context* d_context;
@@ -175,7 +180,8 @@ protected:
   /**
    * Construct a Theory.
    */
-  Theory(context::Context* ctxt, OutputChannel& out) throw() :
+  Theory(int id, context::Context* ctxt, OutputChannel& out) throw() :
+    d_id(id),
     d_context(ctxt),
     d_facts(),
     d_factsResetter(*this),
@@ -196,13 +202,6 @@ protected:
   }
 
   /**
-   * Get the context associated to this Theory.
-   */
-  context::Context* getContext() const {
-    return d_context;
-  }
-
-  /**
    * The output channel for the Theory.
    */
   OutputChannel* d_out;
@@ -269,6 +268,20 @@ public:
   static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
 
   /**
+   * Get the id for this Theory.
+   */
+  int getId() const {
+    return d_id;
+  }
+
+  /**
+   * Get the context associated to this Theory.
+   */
+  context::Context* getContext() const {
+    return d_context;
+  }
+
+  /**
    * Set the output channel associated to this theory.
    */
   void setOutputChannel(OutputChannel& out) {
@@ -340,6 +353,22 @@ public:
   }
 
   /**
+   * This method is called to notify a theory that the node n should be considered a "shared term" by this theory
+   */
+  virtual void addSharedTerm(TNode n) { }
+
+  /**
+   * This method is called by the shared term manager when a shared term t
+   * which this theory cares about (either because it received a previous
+   * addSharedTerm call with t or because it received a previous notifyEq call
+   * with t as the second argument) becomes equal to another shared term u.
+   * This call also serves as notice to the theory that the shared term manager
+   * now considers u the representative for this equivalence class of shared
+   * terms, so future notifications for this class will be based on u not t.
+   */
+  virtual void notifyEq(TNode t, TNode u) { }
+
+  /**
    * Check the current assignment's consistency.
    *
    * An implementation of check() is required to either: