diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 22:26:35 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 22:26:35 -0400 |
commit | cdd8b23c110d88008eb7c79bd55c523fe0918f47 (patch) | |
tree | 346e4934018ac914f30db5d5903c85ceaedcdab1 /test/unit/prop | |
parent | ab38090c92343c0f1b51ebe3c4bde67c19be9253 (diff) |
Unit test fix.
Diffstat (limited to 'test/unit/prop')
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 679b68a2f..0ba051aa3 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -67,7 +67,7 @@ public: return d_nextVar++; } - void addClause(SatClause& c, bool lemma) { + void addClause(SatClause& c, bool lemma, uint64_t) { d_addClauseCalled = true; } @@ -182,7 +182,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, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -199,19 +199,19 @@ public: 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 ); + d_nodeManager->mkNode(kind::XOR, e, f)))), false, false, RULE_INVALID, Node::null()); 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, RULE_INVALID, Node::null() ); 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, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -219,7 +219,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, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -227,7 +227,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, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -244,14 +244,14 @@ public: // d_nodeManager->mkVar(d_nodeManager->integerType()) // ), // d_nodeManager->mkVar(d_nodeManager->integerType()) - // ), false, false); + // ), false, false, RULE_INVALID, Node::null()); // //} 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, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -260,7 +260,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::OR, a, b, c), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -268,10 +268,10 @@ public: 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); + d_cnfStream->convertAndAssert(a, false, false, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false); + d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -279,7 +279,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::XOR, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } |