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

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

2 files changed, 22 insertions, 3 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ab72a0a8c..b84b1e507 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -16,9 +16,11 @@
  ** Implementation of the theory of arrays.
  **/
 
+
 #include "theory/arrays/theory_arrays.h"
 #include "expr/kind.h"
 
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -26,14 +28,29 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arrays;
 
-TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) :
-  Theory(c, out)
+
+TheoryArrays::TheoryArrays(int id, Context* c, OutputChannel& out) :
+  Theory(id, c, out)
 {
 }
 
+
 TheoryArrays::~TheoryArrays() {
 }
 
+
+void TheoryArrays::addSharedTerm(TNode t) {
+  Debug("arrays") << "TheoryArrays::addSharedTerm(): "
+                  << t << endl;
+}
+
+
+void TheoryArrays::notifyEq(TNode eq) {
+  Debug("arrays") << "TheoryArrays::notifyEq(): "
+                  << eq << endl;
+}
+
+
 void TheoryArrays::check(Effort e) {
   while(!done()) {
     Node assertion = get();
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index cf7f16f52..3cb050287 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -31,7 +31,7 @@ namespace arrays {
 
 class TheoryArrays : public Theory {
 public:
-  TheoryArrays(context::Context* c, OutputChannel& out);
+  TheoryArrays(int id, context::Context* c, OutputChannel& out);
   ~TheoryArrays();
   void preRegisterTerm(TNode n) { }
   void registerTerm(TNode n) { }
@@ -48,6 +48,8 @@ public:
     return RewriteComplete(in);
   }
 
+  void addSharedTerm(TNode t);
+  void notifyEq(TNode eq);
   void check(Effort e);
   void propagate(Effort e) { }
   void explain(TNode n, Effort e) { }