diff options
Diffstat (limited to 'src')
-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 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 95 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 10 |
7 files changed, 67 insertions, 64 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; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0ec55a5e6..0aaf602e3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -83,35 +83,8 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - LemmaProofRecipe* proofRecipe = NULL; PROOF({ - // Theory lemmas have one step that proves the empty clause - proofRecipe = new LemmaProofRecipe; - - Node emptyNode; - LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode); - - proofRecipe->setOriginalLemma(lemma); - - Node rewritten; - if (lemma.getKind() == kind::OR) { - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { - rewritten = theory::Rewriter::rewrite(lemma[i]); - if (rewritten != lemma[i]) { - proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma[i]); - proofRecipe->addBaseAssertion(rewritten); - } - } else { - rewritten = theory::Rewriter::rewrite(lemma); - if (rewritten != lemma) { - proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma); - proofRecipe->addBaseAssertion(rewritten); - } - proofRecipe->addStep(proofStep); + registerLemmaRecipe(lemma, lemma, d_theory); }); theory::LemmaStatus result = d_engine->lemma(lemma, @@ -119,22 +92,59 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, false, removable, preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST, - proofRecipe); - PROOF(delete proofRecipe;); + sendAtoms ? d_theory : theory::THEORY_LAST); + // PROOF(delete proofRecipe;); return result; } +void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId) { + // During CNF conversion, conjunctions will be broken down into + // multiple lemmas. In order for the recipes to match, we have to do + // the same here. + if (lemma.getKind() == kind::AND) { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) + registerLemmaRecipe(lemma[i], originalLemma, theoryId); + } + + // Theory lemmas have one step that proves the empty clause + LemmaProofRecipe proofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + // Remember the original lemma, so we can report this later when asked to + proofRecipe.setOriginalLemma(originalLemma); + + // Record the assertions and rewrites + Node rewritten; + if (lemma.getKind() == kind::OR) { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { + rewritten = theory::Rewriter::rewrite(lemma[i]); + if (rewritten != lemma[i]) { + proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma[i]); + proofRecipe.addBaseAssertion(rewritten); + } + } else { + rewritten = theory::Rewriter::rewrite(lemma); + if (rewritten != lemma) { + proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma); + proofRecipe.addBaseAssertion(rewritten); + } + proofRecipe.addStep(proofStep); + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); +} + theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - - LemmaProofRecipe* proofRecipe = NULL; Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; - theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe); + theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); return result; } @@ -629,8 +639,7 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - LemmaProofRecipe* proofRecipe = NULL; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe); + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory); // This code is supposed to force preference to follow what the theory models already have // but it doesn't seem to make a big difference - need to explore more -Clark @@ -1616,8 +1625,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, - theory::TheoryId atomsTo, - LemmaProofRecipe* proofRecipe) { + theory::TheoryId atomsTo) { // For resource-limiting (also does a time check). // spendResource(); @@ -1667,10 +1675,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1729,10 +1737,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // Process the explanation getExplanation(explanationVector, proofRecipe); + PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); } else { // When only one theory, the conflict should need no processing @@ -1758,9 +1767,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { proofRecipe->getStep(0)->addAssertion(conflict.negate()); proofRecipe->addBaseAssertion(conflict.negate()); } + + ProofManager::getCnfProof()->setProofRecipe(proofRecipe); }); - lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST); } PROOF({ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index eed58864a..ea8628f9c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -322,6 +322,13 @@ class TheoryEngine { void handleUserAttribute( const char* attr, theory::Theory* t ){ d_engine->handleUserAttribute( attr, t ); } + + private: + + /** + * A helper function for registering lemma recipes with the proof engine + */ + void registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId); };/* class TheoryEngine::EngineOutputChannel */ /** @@ -429,8 +436,7 @@ class TheoryEngine { bool negated, bool removable, bool preprocess, - theory::TheoryId atomsTo, - LemmaProofRecipe* proofRecipe); + theory::TheoryId atomsTo); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); |