Some cleanup starting off from trying to understand the sharing code. Changes include

* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor

4 files changed, 12 insertions, 7 deletions

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index c6d6e3e2e..161329c06 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -48,6 +48,7 @@ class TheoryArithWhite : public CxxTest::TestSuite {
   NodeManagerScope* d_scope;
 
   TestOutputChannel d_outputChannel;
+  LogicInfo d_logicInfo;
   Theory::Effort d_level;
 
   TheoryArith* d_arith;
@@ -98,7 +99,7 @@ public:
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
-    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
+    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo);
 
     preregistered = new std::set<Node>();
 
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index a737772ed..1de3854b9 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -101,8 +101,8 @@ public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
-  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) :
-    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) {
+  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) {
   }
 
   void registerTerm(TNode n) {
@@ -149,6 +149,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   UserContext* d_uctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
+  LogicInfo* d_logicInfo;
 
   TestOutputChannel d_outputChannel;
 
@@ -164,7 +165,9 @@ public:
     d_uctxt = new UserContext();
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
-    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
+    d_logicInfo = new LogicInfo();
+
+    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);
@@ -174,6 +177,7 @@ public:
     atom1 = Node::null();
     atom0 = Node::null();
     delete d_dummy;
+    delete d_logicInfo;
     delete d_scope;
     delete d_nm;
     delete d_uctxt;
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index a158b167f..1a91364a4 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -71,7 +71,7 @@ public:
     Context* ctx = new Context();
     Bitblaster* bb = new Bitblaster(ctx); 
     
-    NodeManager* nm = NodeManager::currentNM();
+    // NodeManager* nm = NodeManager::currentNM();
     // TODO: update this
     // Node a = nm->mkVar("a", nm->mkBitVectorType(4));
     // Node b = nm->mkVar("b", nm->mkBitVectorType(4));
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 6bca0c873..ff6cba936 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -107,8 +107,8 @@ class FakeTheory : public Theory {
   // static std::deque<RewriteItem> s_expected;
 
 public:
-  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) :
-    Theory(theoryId, ctxt, uctxt, out, valuation)
+  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+    Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
   { }
 
   /** Register an expected rewrite call */