diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-01 19:08:23 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-01 19:08:23 -0300 |
commit | 8ad308b23c705e73507a42d2425289e999d47f86 (patch) | |
tree | 29e3ac78844bc57171e0d122d758a8371a292a93 /test/unit/prop | |
parent | 62ec0666dd4d409ee85603ae94d7ab1a2b4c9dcc (diff) |
Removes old proof code (#4964)
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
Diffstat (limited to 'test/unit/prop')
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 60 |
1 files changed, 22 insertions, 38 deletions
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index f0253fdbf..33fc15674 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -174,8 +174,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::AND, a, b, c), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -189,26 +189,27 @@ class CnfStreamWhite : public CxxTest::TestSuite { Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( d_nodeManager->mkNode( - kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b), + kind::IMPLIES, + d_nodeManager->mkNode(kind::AND, a, b), d_nodeManager->mkNode( - kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d), + kind::EQUAL, + d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode(kind::NOT, d_nodeManager->mkNode(kind::XOR, e, f)))), - false, false, RULE_INVALID, Node::null()); + false, + false); TS_ASSERT(d_satSolver->addClauseCalled()); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false, - RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false, - RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -216,8 +217,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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::EQUAL, a, b), false, - false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::EQUAL, a, b), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -225,33 +226,16 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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, RULE_INVALID, Node::null()); + 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, 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, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::NOT, a), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -260,8 +244,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::OR, a, b, c), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -269,10 +253,10 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(a, false, false); TS_ASSERT(d_satSolver->addClauseCalled()); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert(b, false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } @@ -280,8 +264,8 @@ class CnfStreamWhite : public CxxTest::TestSuite { 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, RULE_INVALID, Node::null()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::XOR, a, b), false, false); TS_ASSERT(d_satSolver->addClauseCalled()); } |