diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /test/unit/theory | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 7 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 13 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 13 |
3 files changed, 21 insertions, 12 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index ded7cee97..f0073cc0b 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -43,6 +43,7 @@ using namespace std; class TheoryArithWhite : public CxxTest::TestSuite { Context* d_ctxt; + UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -92,11 +93,12 @@ public: } void setUp() { - d_ctxt = new Context; + d_ctxt = new Context(); + d_uctxt = new UserContext(); d_nm = new NodeManager(d_ctxt, NULL); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL)); + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL)); preregistered = new std::set<Node>(); @@ -115,6 +117,7 @@ public: d_outputChannel.clear(); delete d_scope; delete d_nm; + delete d_uctxt; delete d_ctxt; } diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 2c3ff0bb1..63900c19c 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -95,8 +95,8 @@ public: set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) : - Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) { + DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) : + Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) { } void registerTerm(TNode n) { @@ -135,11 +135,12 @@ public: void explain(TNode n, Effort level) {} Node getValue(TNode n) { return Node::null(); } string identify() const { return "DummyTheory"; } -}; +};/* class DummyTheory */ class TheoryBlack : public CxxTest::TestSuite { Context* d_ctxt; + UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -153,10 +154,11 @@ class TheoryBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; + d_ctxt = new Context(); + d_uctxt = new UserContext(); d_nm = new NodeManager(d_ctxt, NULL); d_scope = new NodeManagerScope(d_nm); - d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL)); + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL)); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); @@ -168,6 +170,7 @@ public: delete d_dummy; delete d_scope; delete d_nm; + delete d_uctxt; delete d_ctxt; } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index e33efb597..7132d9b17 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -104,8 +104,8 @@ class FakeTheory : public Theory { // static std::deque<RewriteItem> s_expected; public: - FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) : - Theory(theoryId, ctxt, out, valuation) + FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) : + Theory(theoryId, ctxt, uctxt, out, valuation) { } /** Register an expected rewrite call */ @@ -222,6 +222,7 @@ public: */ class TheoryEngineWhite : public CxxTest::TestSuite { Context* d_ctxt; + UserContext* d_uctxt; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -231,15 +232,16 @@ class TheoryEngineWhite : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; + d_ctxt = new Context(); + d_uctxt = new UserContext(); d_nm = new NodeManager(d_ctxt, NULL); d_scope = new NodeManagerScope(d_nm); - d_nullChannel = new FakeOutputChannel; + d_nullChannel = new FakeOutputChannel(); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt); + d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt); d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN); d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL); @@ -260,6 +262,7 @@ public: delete d_scope; delete d_nm; + delete d_uctxt; delete d_ctxt; } |