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 | |
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')
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 293 | ||||
-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 |
4 files changed, 170 insertions, 156 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index c9a2196a5..62117d4c1 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -99,154 +99,159 @@ class CnfStreamBlack : public CxxTest::TestSuite { /** The context */ Context* d_context; + /** The user context */ + UserContext* d_userContext; + /** The node manager */ NodeManager* d_nodeManager; -void setUp() { - d_context = new Context; - d_nodeManager = new NodeManager(d_context, NULL); - NodeManagerScope nms(d_nodeManager); - d_satSolver = new FakeSatSolver; - d_theoryEngine = new TheoryEngine(d_context); - d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); - d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); - d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH); - theory::Registrar registrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); -} - -void tearDown() { - NodeManagerScope nms(d_nodeManager); - delete d_cnfStream; - d_theoryEngine->shutdown(); - delete d_theoryEngine; - delete d_satSolver; - delete d_nodeManager; - delete d_context; -} + void setUp() { + d_context = new Context(); + d_userContext = new UserContext(); + d_nodeManager = new NodeManager(d_context, NULL); + NodeManagerScope nms(d_nodeManager); + d_satSolver = new FakeSatSolver(); + d_theoryEngine = new TheoryEngine(d_context, d_userContext); + d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); + d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); + d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH); + theory::Registrar registrar(d_theoryEngine); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); + } + + void tearDown() { + NodeManagerScope nms(d_nodeManager); + delete d_cnfStream; + d_theoryEngine->shutdown(); + delete d_theoryEngine; + delete d_satSolver; + delete d_nodeManager; + delete d_userContext; + delete d_context; + } public: -/* [chris 5/26/2010] In the tests below, we don't attempt to delve into the - * deep structure of the CNF conversion. Firstly, we just want to make sure - * that the conversion doesn't choke on any boolean Exprs. We'll also check - * that addClause got called. We won't check that it gets called a particular - * number of times, or with what. - */ - -void testAnd() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::AND, a, b, c), false, false); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testComplexExpr() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode( - kind::IMPLIES, - d_nodeManager->mkNode(kind::AND, a, b), - d_nodeManager->mkNode( - kind::IFF, - d_nodeManager->mkNode(kind::OR, c, d), - d_nodeManager->mkNode( - kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testFalse() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testIff() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IFF, a, b), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testImplies() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -// ITEs should be removed before going to CNF -//void testIte() { -// NodeManagerScope nms(d_nodeManager); -// d_cnfStream->convertAndAssert( -// d_nodeManager->mkNode( -// kind::EQUAL, -// d_nodeManager->mkNode( -// kind::ITE, -// d_nodeManager->mkVar(d_nodeManager->booleanType()), -// d_nodeManager->mkVar(d_nodeManager->integerType()), -// d_nodeManager->mkVar(d_nodeManager->integerType()) -// ), -// d_nodeManager->mkVar(d_nodeManager->integerType()) -// ), false, false); -// -//} - -void testNot() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testOr() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testTrue() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testVar() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a, false, false); - TS_ASSERT( d_satSolver->addClauseCalled() ); - d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} - -void testXor() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::XOR, a, b), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); -} + /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the + * deep structure of the CNF conversion. Firstly, we just want to make sure + * that the conversion doesn't choke on any boolean Exprs. We'll also check + * that addClause got called. We won't check that it gets called a particular + * number of times, or with what. + */ + + void testAnd() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::AND, a, b, c), false, false); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testComplexExpr() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode( + kind::IMPLIES, + d_nodeManager->mkNode(kind::AND, a, b), + d_nodeManager->mkNode( + kind::IFF, + d_nodeManager->mkNode(kind::OR, c, d), + d_nodeManager->mkNode( + kind::NOT, + d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testFalse() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testIff() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::IFF, a, b), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testImplies() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + // ITEs should be removed before going to CNF + //void testIte() { + // NodeManagerScope nms(d_nodeManager); + // d_cnfStream->convertAndAssert( + // d_nodeManager->mkNode( + // kind::EQUAL, + // d_nodeManager->mkNode( + // kind::ITE, + // d_nodeManager->mkVar(d_nodeManager->booleanType()), + // d_nodeManager->mkVar(d_nodeManager->integerType()), + // d_nodeManager->mkVar(d_nodeManager->integerType()) + // ), + // d_nodeManager->mkVar(d_nodeManager->integerType()) + // ), false, false); + // + //} + + void testNot() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::NOT, a), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testOr() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testVar() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert(a, false, false); + TS_ASSERT( d_satSolver->addClauseCalled() ); + d_satSolver->reset(); + d_cnfStream->convertAndAssert(b, false, false); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + + void testXor() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::XOR, a, b), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } }; 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; } |