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

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

4 files changed, 4 insertions, 4 deletions

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index d8c41bf3a..ea1ee698f 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -70,7 +70,7 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
-    d_arith = new TheoryArith(d_ctxt, d_outputChannel);
+    d_arith = new TheoryArith(0, d_ctxt, d_outputChannel);
 
     preregistered = new std::set<Node>();
 
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 967a53462..0c6a38d0b 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -95,7 +95,7 @@ public:
   vector<Node> d_getSequence;
 
   DummyTheory(Context* ctxt, OutputChannel& out) :
-    Theory(ctxt, out) {
+    Theory(0, ctxt, out) {
   }
 
   void registerTerm(TNode n) {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index addf15af3..570fa74a4 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -80,7 +80,7 @@ class FakeTheory : public Theory {
 
 public:
   FakeTheory(context::Context* ctxt, OutputChannel& out, std::string id) :
-    Theory(ctxt, out),
+    Theory(0, ctxt, out),
     d_id(id) {
   }
 
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index a959d01ba..8e72c428f 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -59,7 +59,7 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
-    d_euf = new TheoryUF(d_ctxt, d_outputChannel);
+    d_euf = new TheoryUF(0, d_ctxt, d_outputChannel);
 
     d_booleanType = new TypeNode(d_nm->booleanType());
   }