diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/prop/theory_proxy.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 33 |
1 files changed, 13 insertions, 20 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 6e8f1fbbf..4a4515eb9 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -99,34 +99,29 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - LemmaProofRecipe* proofRecipe = NULL; - PROOF(proofRecipe = new LemmaProofRecipe;); - - Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); + NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode); + Node explanationNode = theoryExplanation.node; + theory::TheoryId explainerTheory = theoryExplanation.theory; PROOF({ - ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); - ProofManager::getCnfProof()->setProofRecipe(proofRecipe); - - Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " - << std::endl; - proofRecipe->dump("pf::sat"); + ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode); + ProofManager::getCnfProof()->setExplainerTheory(explainerTheory); - delete proofRecipe; - proofRecipe = NULL; + Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: " + << explainerTheory << std::endl; }); - Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; - if (theoryExplanation.getKind() == kind::AND) { - Node::const_iterator it = theoryExplanation.begin(); - Node::const_iterator it_end = theoryExplanation.end(); + Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl; + if (explanationNode.getKind() == kind::AND) { + Node::const_iterator it = explanationNode.begin(); + Node::const_iterator it_end = explanationNode.end(); explanation.push_back(l); for (; it != it_end; ++ it) { explanation.push_back(~d_cnfStream->getLiteral(*it)); } } else { explanation.push_back(l); - explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation)); + explanation.push_back(~d_cnfStream->getLiteral(explanationNode)); } } @@ -180,9 +175,7 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { 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, theory::THEORY_LAST); } else { Debug("shared") << "=(" << asNode << std::endl; } |