diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
commit | 89ba584531115b7f6d47088d7614368ea05ab9d8 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/theory/theory_engine.cpp | |
parent | 324ca0376c960c75f621f0102eeaa1186589dda7 (diff) |
Merging proof branch
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 322 |
1 files changed, 303 insertions, 19 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1ab4c228b..618fda4c0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -26,6 +26,8 @@ #include "options/bv_options.h" #include "options/options.h" #include "options/quantifiers_options.h" +#include "proof/cnf_proof.h" +#include "proof/lemma_proof.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "smt/ite_removal.h" @@ -53,6 +55,104 @@ using namespace CVC4::theory; namespace CVC4 { +inline void flattenAnd(Node n, std::vector<TNode>& out){ + Assert(n.getKind() == kind::AND); + for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ + Node curr = *i; + if(curr.getKind() == kind::AND){ + flattenAnd(curr, out); + }else{ + out.push_back(curr); + } + } +} + +inline Node flattenAnd(Node n){ + std::vector<TNode> out; + flattenAnd(n, out); + return NodeManager::currentNM()->mkNode(kind::AND, out); +} + +theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, + ProofRule rule, + bool removable, + bool preprocess, + bool sendAtoms) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl; + ++ 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); + + 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); + }); + + theory::LemmaStatus result = d_engine->lemma(lemma, + rule, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST, + proofRecipe); + PROOF(delete proofRecipe;); + return result; +} + +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); + return result; +} + +bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) + throw(AssertionException, UnsafeInterruptException) { + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; + ++ d_statistics.propagations; + d_engine->d_outputChannelUsed = true; + return d_engine->propagate(literal, d_theory); +} + +void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) + throw(AssertionException, UnsafeInterruptException) { + Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + Assert (pf == NULL); // Theory shouldn't be producing proofs yet + ++ d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(conflictNode, d_theory); +} + void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); @@ -497,7 +597,10 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory); + + LemmaProofRecipe* proofRecipe = NULL; + lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe); + // 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 // if (true) { @@ -963,7 +1066,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { - Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl; + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl; Assert(toTheoryId != fromTheoryId); if(toTheoryId != THEORY_SAT_SOLVER && @@ -1176,6 +1279,23 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory); } } else { + // We could be propagating a unit-clause lemma. In this case, we need to provide a + // recipe. + // TODO: Consider putting this someplace else? This is the only refence to the proof + // manager in this class. + + PROOF({ + LemmaProofRecipe proofRecipe; + proofRecipe.addBaseAssertion(literal); + + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theory, emptyNode); + proofStep.addAssertion(literal); + proofRecipe.addStep(proofStep); + + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); + }); + // Just send off to the SAT solver Assert(d_propEngine->isSatLiteral(literal)); assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); @@ -1270,7 +1390,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { return conjunction; } -NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { +Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; bool polarity = node.getKind() != kind::NOT; @@ -1278,32 +1398,90 @@ NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) { // If we're not in shared mode, explanations are simple if (!d_logicInfo.isSharingEnabled()) { + Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. " + << " Responsible theory is: " + << theoryOf(atom)->getId() << std::endl; + Node explanation = theoryOf(atom)->explain(node); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return NodeTheoryPair(explanation, theoryOf(atom)->getId()); + PROOF({ + if(proofRecipe) { + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode); + proofStep.addAssertion(node); + proofRecipe->addBaseAssertion(node); + + if (explanation.getKind() == kind::AND) { + // If the explanation is a conjunction, the recipe for the corresponding lemma is + // the negation of its conjuncts. + Node flat = flattenAnd(explanation); + for (unsigned i = 0; i < flat.getNumChildren(); ++i) { + if (flat[i].isConst() && flat[i].getConst<bool>()) { + ++ i; + continue; + } + if (flat[i].getKind() == kind::NOT && + flat[i][0].isConst() && !flat[i][0].getConst<bool>()) { + ++ i; + continue; + } + Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: " + << flat[i].negate() << std::endl; + proofStep.addAssertion(flat[i].negate()); + proofRecipe->addBaseAssertion(flat[i].negate()); + } + } else { + // The recipe for proving it is by negating it. "True" is not an acceptable reason. + if (!((explanation.isConst() && explanation.getConst<bool>()) || + (explanation.getKind() == kind::NOT && + explanation[0].isConst() && !explanation[0].getConst<bool>()))) { + proofStep.addAssertion(explanation.negate()); + proofRecipe->addBaseAssertion(explanation.negate()); + } + } + + proofRecipe->addStep(proofStep); + } + }); + + return explanation; } + Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl; + // Initial thing to explain NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain]; + Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node " + << nodeExplainerPair.node + << " is theory: " << nodeExplainerPair.theory << std::endl; TheoryId explainer = nodeExplainerPair.theory; // Create the workplace for explanations std::vector<NodeTheoryPair> explanationVector; explanationVector.push_back(d_propagationMap[toExplain]); // Process the explanation - getExplanation(explanationVector); + if (proofRecipe) { + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode); + proofStep.addAssertion(node); + proofRecipe->addStep(proofStep); + proofRecipe->addBaseAssertion(node); + } + + getExplanation(explanationVector, proofRecipe); Node explanation = mkExplanation(explanationVector); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; - return NodeTheoryPair(explanation, explainer); + return explanation; } Node TheoryEngine::getExplanation(TNode node) { - return getExplanationAndExplainer(node).node; + LemmaProofRecipe *dontCareRecipe = NULL; + return getExplanationAndRecipe(node, dontCareRecipe); } struct AtomsCollect { @@ -1406,7 +1584,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool removable, bool preprocess, theory::TheoryId atomsTo, - theory::TheoryId ownerTheory) { + LemmaProofRecipe* proofRecipe) { // For resource-limiting (also does a time check). // spendResource(); @@ -1456,10 +1634,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. @@ -1493,22 +1671,69 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { << CheckSatCommand(conflict.toExpr()); } + LemmaProofRecipe* proofRecipe = NULL; + PROOF({ + proofRecipe = new LemmaProofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + if (conflict.getKind() == kind::AND) { + for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { + proofStep.addAssertion(conflict[i].negate()); + } + } else { + proofStep.addAssertion(conflict.negate()); + } + + proofRecipe->addStep(proofStep); + }); + // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations std::vector<NodeTheoryPair> explanationVector; explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + // Process the explanation - getExplanation(explanationVector); + getExplanation(explanationVector, 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, theoryId); + lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); + } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId); + PROOF({ + if (conflict.getKind() == kind::AND) { + // If the conflict is a conjunction, the corresponding lemma is derived by negating + // its conjuncts. + for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { + if (conflict[i].isConst() && conflict[i].getConst<bool>()) { + ++ i; + continue; + } + if (conflict[i].getKind() == kind::NOT && + conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) { + ++ i; + continue; + } + proofRecipe->getStep(0)->addAssertion(conflict[i].negate()); + proofRecipe->addBaseAssertion(conflict[i].negate()); + } + } else { + proofRecipe->getStep(0)->addAssertion(conflict.negate()); + proofRecipe->addBaseAssertion(conflict.negate()); + } + }); + + lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe); } + + PROOF({ + delete proofRecipe; + proofRecipe = NULL; + }); } void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions) { @@ -1660,19 +1885,21 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){ return result; } -void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector) -{ +void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); unsigned i = 0; // Index of the current literal we are processing unsigned j = 0; // Index of the last literal we are keeping - while (i < explanationVector.size()) { + std::set<Node> inputAssertions; + PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions();); + while (i < explanationVector.size()) { // Get the current literal to explain NodeTheoryPair toExplain = explanationVector[i]; - Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; + Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl; + // If a true constant or a negation of a false constant we can ignore it if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) { @@ -1686,6 +1913,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // If from the SAT solver, keep it if (toExplain.theory == THEORY_SAT_SOLVER) { + Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; explanationVector[j++] = explanationVector[i++]; continue; } @@ -1704,10 +1932,26 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector // See if it was sent to the theory by another theory PropagationMap::const_iterator find = d_propagationMap.find(toExplain); if (find != d_propagationMap.end()) { + Debug("theory::explain") << "\tTerm was propagated by another theory (theory = " + << theoryOf((*find).second.theory)->getId() << ")" << std::endl; // There is some propagation, check if its a timely one if ((*find).second.timestamp < toExplain.timestamp) { + Debug("theory::explain") << "\tRelevant timetsamp, pushing " + << (*find).second.node << "to index = " << explanationVector.size() << std::endl; explanationVector.push_back((*find).second); - ++ i; + ++i; + + PROOF({ + if (toExplain.node != (*find).second.node) { + Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node + << ", toExplain = " << (*find).second.node << std::endl; + + if (proofRecipe) { + proofRecipe->addRewriteRule(toExplain.node, (*find).second.node); + } + } + }) + continue; } } @@ -1716,21 +1960,61 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector Node explanation; if (toExplain.theory == THEORY_BUILTIN) { explanation = d_sharedTerms.explain(toExplain.node); + Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; } else { explanation = theoryOf(toExplain.theory)->explain(toExplain.node); + Debug("theory::explain") << "\tTerm was propagated by owner theory: " + << theoryOf(toExplain.theory)->getId() + << ". Explanation: " << explanation << std::endl; } + Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); + ++ i; + + PROOF({ + if (proofRecipe) { + // If we're expanding the target node of the explanation (this is the first expansion...), + // we don't want to add it as a separate proof step. It is already part of the assertions. + if (inputAssertions.find(toExplain.node) == inputAssertions.end()) { + LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node); + if (explanation.getKind() == kind::AND) { + Node flat = flattenAnd(explanation); + for (unsigned k = 0; k < flat.getNumChildren(); ++ k) { + // If a true constant or a negation of a false constant we can ignore it + if (! ((flat[k].isConst() && flat[k].getConst<bool>()) || + (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst<bool>()))) { + proofStep.addAssertion(flat[k].negate()); + } + } + } else { + if (! ((explanation.isConst() && explanation.getConst<bool>()) || + (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst<bool>()))) { + proofStep.addAssertion(explanation.negate()); + } + } + proofRecipe->addStep(proofStep); + } + } + }); } // Keep only the relevant literals explanationVector.resize(j); -} + PROOF({ + if (proofRecipe) { + // The remaining literals are the base of the proof + for (unsigned k = 0; k < explanationVector.size(); ++k) { + proofRecipe->addBaseAssertion(explanationVector[k].node.negate()); + } + } + }); +} void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) { |