From 1d07595a25267066a77ffce8216a759be5fbbdde Mon Sep 17 00:00:00 2001 From: Guy Date: Sun, 24 Jul 2016 20:56:08 -0700 Subject: [PATCH] Proper handling for lemmas that are conjuncts: Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked. Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them. --- src/prop/cnf_stream.cpp | 9 +--- src/prop/cnf_stream.h | 8 +-- src/prop/prop_engine.cpp | 3 +- src/prop/prop_engine.h | 3 +- src/prop/theory_proxy.cpp | 3 +- src/theory/theory_engine.cpp | 95 ++++++++++++++++++++---------------- 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& atoms, theory::TheoryId theory); -- 2.30.2