diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
commit | 1433806056059339dd16ae8e431feaae23553150 (patch) | |
tree | cf678baa687b1a19e479c28a1c01470bb2f120c7 /test/unit | |
parent | 8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (diff) |
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
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 3 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 10 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_white.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 4 |
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 */ |