diff options
Diffstat (limited to 'test/unit/prop/cnf_stream_black.h')
| -rw-r--r-- | test/unit/prop/cnf_stream_black.h | 44 |
1 files changed, 23 insertions, 21 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 62117d4c1..26b490d2d 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -144,8 +144,7 @@ public: 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); + d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -157,22 +156,18 @@ public: 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_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b), - d_nodeManager->mkNode( - kind::IFF, + d_nodeManager->mkNode(kind::IFF, d_nodeManager->mkNode(kind::OR, c, d), - d_nodeManager->mkNode( - kind::NOT, + 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 ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -180,8 +175,7 @@ public: 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 ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -189,8 +183,7 @@ public: 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 ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -214,8 +207,7 @@ public: 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 ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -224,14 +216,13 @@ public: 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 ); + 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 ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -250,8 +241,19 @@ public: 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 ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } + + void testEnsureLiteral() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b); + d_cnfStream->ensureLiteral(a_and_b); + // Clauses are necessary to "literal-ize" a_and_b; this perhaps + // doesn't belong in a black-box test though... + TS_ASSERT( d_satSolver->addClauseCalled() ); + TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) ); + } }; |