diff options
| -rw-r--r-- | test/unit/prop/cnf_stream_black.h | 103 |
1 files changed, 98 insertions, 5 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 25a7cce6c..9c8560783 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -93,14 +93,63 @@ 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. In some cases, - * we'll check to make sure a certain number of assertions are generated. + * 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 testTrue() { +void testAnd() { NodeManagerScope nms(d_nodeManager); - d_satSolver->reset(); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) ); + 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) ); + 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)))) ); + TS_ASSERT( d_satSolver->addClauseCalled() ); +} + +void testFalse() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(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) ); + 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) ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -119,4 +168,48 @@ void testIte() { )); } + +void testNot() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::NOT, a) ); + 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) ); + TS_ASSERT( d_satSolver->addClauseCalled() ); +} + +void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) ); + 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); + TS_ASSERT( d_satSolver->addClauseCalled() ); + d_satSolver->reset(); + d_cnfStream->convertAndAssert(b); + 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) ); + TS_ASSERT( d_satSolver->addClauseCalled() ); +} }; |