diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
commit | dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c (patch) | |
tree | 7516d3d5d43f0dadb943bb186615e0903cbd9f7f /src/prop | |
parent | 74bf9ff63f5566fbe1b5db9124f9dc1fde65cb82 (diff) | |
parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 9 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 8 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 3 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 |
5 files changed, 6 insertions, 20 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index eda736b8a..f2401041e 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -678,8 +678,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, - TNode from, - LemmaProofRecipe* proofRecipe) { + TNode from) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -689,12 +688,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - if (proofRecipe) { - Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; - proofRecipe->dump("pf::sat"); - d_cnfProof->setProofRecipe(proofRecipe); - } - if (proof_id != RULE_INVALID) { d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 6cc10d878..661108dd0 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -37,8 +37,6 @@ namespace CVC4 { -class LemmaProofRecipe; - namespace prop { class PropEngine; @@ -210,9 +208,8 @@ public: * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated - * @param proofRecipe contains the proof recipe for proving this node */ - virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -282,8 +279,7 @@ public: * @param negated true if negated */ void convertAndAssert(TNode node, bool removable, - bool negated, ProofRule rule, TNode from = TNode::null(), - LemmaProofRecipe* proofRecipe = NULL); + bool negated, ProofRule rule, TNode from = TNode::null()); /** * Constructs the stream to use the given sat solver. diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index eb607e901..6cdf17f30 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -132,13 +132,12 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, - LemmaProofRecipe* proofRecipe, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as (possibly) removable - d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe); + d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index c02015931..f966def26 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -37,7 +37,6 @@ namespace CVC4 { class ResourceManager; class DecisionEngine; class TheoryEngine; -class LemmaProofRecipe; namespace theory { class TheoryRegistrar; @@ -135,7 +134,7 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null()); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 6e8f1fbbf..5f5eac733 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -181,8 +181,7 @@ void TheoryProxy::notifyRestart() { Debug("shared") << "=) " << asNode << std::endl; } - LemmaProofRecipe* noProofRecipe = NULL; - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe); + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID); } else { Debug("shared") << "=(" << asNode << std::endl; } |