From c94347913fa464b1ec6a3da2ab21e319c0c42e02 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 29 Sep 2011 05:15:30 +0000 Subject: 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 --- test/unit/prop/cnf_stream_black.h | 293 +++++++++++++++++++------------------- 1 file changed, 149 insertions(+), 144 deletions(-) (limited to 'test/unit/prop/cnf_stream_black.h') 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::THEORY_BUILTIN); - d_theoryEngine->addTheory(theory::THEORY_BOOL); - d_theoryEngine->addTheory(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::THEORY_BUILTIN); + d_theoryEngine->addTheory(theory::THEORY_BOOL); + d_theoryEngine->addTheory(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() ); + } }; -- cgit v1.2.3