diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-06-01 01:26:24 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-06-01 01:26:24 +0000 |
commit | eee91ecc512e94358a02d2aa155764e4cda2e5fa (patch) | |
tree | 7611e3305463978cb9a957a75d218083fe6fb677 /test/unit | |
parent | cfb3b789e26fdab73e733825950b24492c6c5e4c (diff) |
In order for splitting on demand to be able to retract clauses every translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 9c8560783..bbae46df7 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -104,7 +104,7 @@ void testAnd() { 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) ); + d_nodeManager->mkNode(kind::AND, a, b, c), false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -125,13 +125,13 @@ void testComplexExpr() { d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode( kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))) ); + d_nodeManager->mkNode(kind::XOR, e, f)))), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false) ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -140,7 +140,7 @@ void testIff() { 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) ); + d_nodeManager->mkNode(kind::IFF, a, b), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -149,7 +149,7 @@ void testImplies() { 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) ); + d_nodeManager->mkNode(kind::IMPLIES, a, b), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -165,7 +165,7 @@ void testIte() { d_nodeManager->mkVar(d_nodeManager->integerType()) ), d_nodeManager->mkVar(d_nodeManager->integerType()) - )); + ), false); } @@ -173,7 +173,7 @@ void testNot() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a) ); + d_nodeManager->mkNode(kind::NOT, a), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -183,13 +183,13 @@ void testOr() { 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) ); + d_nodeManager->mkNode(kind::OR, a, b, c), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -197,10 +197,10 @@ 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); + d_cnfStream->convertAndAssert(a, false); TS_ASSERT( d_satSolver->addClauseCalled() ); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b); + d_cnfStream->convertAndAssert(b, false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -209,7 +209,7 @@ void testXor() { 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) ); + d_nodeManager->mkNode(kind::XOR, a, b), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } }; |