diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 | ||||
-rw-r--r-- | src/theory/combination_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/engine_output_channel.cpp | 19 | ||||
-rw-r--r-- | src/theory/shared_terms_database.cpp | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 241 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 33 |
6 files changed, 237 insertions, 64 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index d0ba4ca71..8165c5d8a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -76,7 +76,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - Node theoryExplanation = d_theoryEngine->getExplanation(lNode); + theory::TrustNode texp = d_theoryEngine->getExplanation(lNode); + Node theoryExplanation = texp.getNode(); if (options::unsatCores()) { diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index f1e977fe3..5c9e6713b 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -113,7 +113,7 @@ eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify() void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo) { - d_te.lemma(trn.getNode(), false, LemmaProperty::NONE, atomsTo); + d_te.lemma(trn, LemmaProperty::NONE, atomsTo); } void CombinationEngine::resetRound() diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 2334d3817..84a1d89a6 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -77,10 +77,10 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) TrustNode tlem = TrustNode::mkTrustLemma(lemma); theory::LemmaStatus result = d_engine->lemma( - tlem.getNode(), - false, + tlem, p, - isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST); + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, + d_theory); return result; } @@ -95,8 +95,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) << std::endl; TrustNode tlem = TrustNode::mkTrustLemma(lemma); LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE; - theory::LemmaStatus result = - d_engine->lemma(tlem.getNode(), false, p, d_theory); + theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory); return result; } @@ -117,7 +116,7 @@ void EngineOutputChannel::conflict(TNode conflictNode) ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; TrustNode tConf = TrustNode::mkTrustConflict(conflictNode); - d_engine->conflict(tConf.getNode(), d_theory); + d_engine->conflict(tConf, d_theory); } void EngineOutputChannel::demandRestart() @@ -170,7 +169,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf) } ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; - d_engine->conflict(pconf.getNode(), d_theory); + d_engine->conflict(pconf, d_theory); } LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) @@ -186,10 +185,10 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) d_engine->d_outputChannelUsed = true; // now, call the normal interface for lemma return d_engine->lemma( - plem.getNode(), - false, + plem, p, - isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST); + isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST, + d_theory); } } // namespace theory diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index a196d0ed0..b01cef377 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -251,7 +251,8 @@ void SharedTermsDatabase::checkForConflict() { std::vector<TNode> assumptions; d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions); Node conflict = mkAnd(assumptions); - d_theoryEngine->conflict(conflict, THEORY_BUILTIN); + TrustNode tconf = TrustNode::mkTrustConflict(conflict); + d_theoryEngine->conflict(tconf, THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ac06d266d..123e00bc1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -45,6 +45,7 @@ #include "theory/relevance_manager.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_engine_proof_generator.h" #include "theory/theory_id.h" #include "theory/theory_model.h" #include "theory/theory_traits.h" @@ -210,6 +211,12 @@ TheoryEngine::TheoryEngine(context::Context* context, d_userContext(userContext), d_logicInfo(logicInfo), d_pnm(nullptr), + d_lazyProof( + d_pnm != nullptr + ? new LazyCDProof( + d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") + : nullptr), + d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)), d_sharedTerms(this, context), d_tc(nullptr), d_quantEngine(nullptr), @@ -1023,8 +1030,10 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo if (!normalizedLiteral.getConst<bool>()) { // Mark the propagation for explanations if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) { + // special case, trust node has no proof generator + TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral); // Get the explanation (conflict will figure out where it came from) - conflict(normalizedLiteral, toTheoryId); + conflict(trnn, toTheoryId); } else { Unreachable(); } @@ -1283,7 +1292,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { return conjunction; } -Node TheoryEngine::getExplanation(TNode node) +TrustNode TheoryEngine::getExplanation(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " @@ -1300,10 +1309,9 @@ Node TheoryEngine::getExplanation(TNode node) << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl; TrustNode texplanation = theoryOf(atom)->explain(node); - Node explanation = texplanation.getNode(); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node - << ") => " << explanation << endl; - return explanation; + << ") => " << texplanation.getNode() << endl; + return texplanation; } Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" @@ -1323,13 +1331,10 @@ Node TheoryEngine::getExplanation(TNode node) std::vector<NodeTheoryPair> explanationVector; explanationVector.push_back(d_propagationMap[toExplain]); // Process the explanation - getExplanation(explanationVector); - Node explanation = mkExplanation(explanationVector); - + TrustNode texplanation = getExplanation(explanationVector); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " - << explanation << endl; - - return explanation; + << texplanation.getNode() << endl; + return texplanation; } struct AtomsCollect { @@ -1430,13 +1435,37 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The } } -theory::LemmaStatus TheoryEngine::lemma(TNode node, - bool negated, +theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, theory::LemmaProperty p, - theory::TheoryId atomsTo) + theory::TheoryId atomsTo, + theory::TheoryId from) { // For resource-limiting (also does a time check). // spendResource(); + Assert(tlemma.getKind() == TrustNodeKind::LEMMA + || tlemma.getKind() == TrustNodeKind::CONFLICT); + // get the node + Node node = tlemma.getNode(); + Node lemma = tlemma.getProven(); + + // when proofs are enabled, we ensure the trust node has a generator by + // adding a trust step to the lazy proof maintained by this class + if (isProofEnabled()) + { + // ensure proof: set THEORY_LEMMA if no generator is provided + if (tlemma.getGenerator() == nullptr) + { + // internal lemmas should have generators + Assert(from != THEORY_LAST); + // add theory lemma step to proof + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from); + d_lazyProof->addStep(lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn}); + // update the trust node + tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get()); + } + // ensure closed + tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial"); + } // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { @@ -1447,10 +1476,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } if(Dump.isOn("t-lemmas")) { - Node n = node; - if (!negated) { - n = node.negate(); - } + // we dump the negation of the lemma, to show validity of the lemma + Node n = lemma.negate(); Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << CheckSatCommand(n.toExpr()); } @@ -1460,18 +1487,58 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // call preprocessor std::vector<TrustNode> newLemmas; std::vector<Node> newSkolems; - TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess); - - // !!!!!!! temporary, until this method is fully updated from proof-new - if (tlemma.isNull()) + TrustNode tplemma = + d_tpp.preprocess(lemma, newLemmas, newSkolems, preprocess); + // the preprocessed lemma + Node lemmap; + if (tplemma.isNull()) { - tlemma = TrustNode::mkTrustLemma(node); + lemmap = lemma; + } + else + { + Assert(tplemma.getKind() == TrustNodeKind::REWRITE); + lemmap = tplemma.getNode(); + + // must update the trust lemma + if (lemmap != lemma) + { + // process the preprocessing + if (isProofEnabled()) + { + Assert(d_lazyProof != nullptr); + // add the original proof to the lazy proof + d_lazyProof->addLazyStep(tlemma.getProven(), tlemma.getGenerator()); + // only need to do anything if lemmap changed in a non-trivial way + if (!CDProof::isSame(lemmap, lemma)) + { + d_lazyProof->addLazyStep(tplemma.getProven(), + tplemma.getGenerator(), + true, + "TheoryEngine::lemma_pp", + false, + PfRule::PREPROCESS_LEMMA); + // ---------- from d_lazyProof -------------- from theory preprocess + // lemma lemma = lemmap + // ------------------------------------------ MACRO_SR_PRED_TRANSFORM + // lemmap + std::vector<Node> pfChildren; + pfChildren.push_back(lemma); + pfChildren.push_back(tplemma.getProven()); + std::vector<Node> pfArgs; + pfArgs.push_back(lemmap); + d_lazyProof->addStep( + lemmap, PfRule::MACRO_SR_PRED_TRANSFORM, pfChildren, pfArgs); + } + } + tlemma = TrustNode::mkTrustLemma(lemmap, d_lazyProof.get()); + } } // must use an assertion pipeline due to decision engine below AssertionPipeline lemmas; // make the assertion pipeline - lemmas.push_back(tlemma.getNode()); + lemmas.push_back(lemmap); lemmas.updateRealAssertionsEnd(); Assert(newSkolems.size() == newLemmas.size()); for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++) @@ -1490,16 +1557,25 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, d_relManager->notifyPreprocessedAssertions(lemmas.ref()); } - // assert lemmas to prop engine - for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i) + // do final checks on the lemmas we are about to send + if (isProofEnabled()) { - d_propEngine->assertLemma(lemmas[i], i == 0 && negated, removable); + Assert(tlemma.getGenerator() != nullptr); + // ensure closed, make the proof node eagerly here to debug + tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma"); + for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) + { + Assert(newLemmas[i].getGenerator() != nullptr); + newLemmas[i].debugCheckClosed("te-proof-debug", + "TheoryEngine::lemma_new"); + } } - // WARNING: Below this point don't assume lemmas[0] to be not negated. - if(negated) { - lemmas.replace(0, lemmas[0].notNode()); - negated = false; + // now, send the lemmas to the prop engine + d_propEngine->assertLemma(tlemma.getProven(), false, removable); + for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) + { + d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable); } // assert to decision engine @@ -1522,9 +1598,16 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, return theory::LemmaStatus(retLemma, d_userContext->getLevel()); } -void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { - - Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl; +void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) +{ + Assert(tconflict.getKind() == TrustNodeKind::CONFLICT); + TNode conflict = tconflict.getNode(); + Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " + << theoryId << ")" << endl; + Trace("te-proof-debug") << "Check closed conflict" << std::endl; + // doesn't require proof generator, yet, since THEORY_LEMMA is added below + tconflict.debugCheckClosed( + "te-proof-debug", "TheoryEngine::conflict_initial", false); Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl; @@ -1539,26 +1622,91 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { // 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)); + std::vector<NodeTheoryPair> vec; + vec.push_back( + NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); // Process the explanation - getExplanation(explanationVector); - Node fullConflict = mkExplanation(explanationVector); + TrustNode tncExp = getExplanation(vec); + Trace("te-proof-debug") + << "Check closed conflict explained with sharing" << std::endl; + tncExp.debugCheckClosed("te-proof-debug", + "TheoryEngine::conflict_explained_sharing"); + Node fullConflict = tncExp.getNode(); + + if (isProofEnabled()) + { + Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl; + Trace("te-proof-debug") << "Conflict " << tconflict << " from " + << tconflict.identifyGenerator() << std::endl; + Trace("te-proof-debug") << "Explanation " << tncExp << " from " + << tncExp.identifyGenerator() << std::endl; + Assert(d_lazyProof != nullptr); + if (tconflict.getGenerator() != nullptr) + { + d_lazyProof->addLazyStep(tconflict.getProven(), + tconflict.getGenerator()); + } + else + { + // add theory lemma step + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); + Node conf = tconflict.getProven(); + d_lazyProof->addStep(conf, PfRule::THEORY_LEMMA, {}, {conf, tidn}); + } + // store the explicit step, which should come from a different + // generator, e.g. d_tepg. + Node proven = tncExp.getProven(); + Assert(tncExp.getGenerator() != d_lazyProof.get()); + Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator() + << " for " << proven << std::endl; + d_lazyProof->addLazyStep(proven, tncExp.getGenerator()); + pfgEnsureClosed(proven, + d_lazyProof.get(), + "te-proof-debug", + "TheoryEngine::conflict_during"); + Node fullConflictNeg = fullConflict.notNode(); + std::vector<Node> children; + children.push_back(proven); + std::vector<Node> args; + args.push_back(fullConflictNeg); + if (conflict == d_false) + { + AlwaysAssert(proven == fullConflictNeg); + } + else + { + if (fullConflict != conflict) + { + // ------------------------- explained ---------- from theory + // fullConflict => conflict ~conflict + // -------------------------------------------- + // MACRO_SR_PRED_TRANSFORM ~fullConflict + children.push_back(conflict.notNode()); + args.push_back(mkMethodId(MethodId::SB_LITERAL)); + d_lazyProof->addStep( + fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + } + } + } + // pass the processed trust node + TrustNode tconf = + TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get()); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, - true, - LemmaProperty::REMOVABLE, - THEORY_LAST); + Trace("te-proof-debug") + << "Check closed conflict with sharing" << std::endl; + tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing"); + lemma(tconf, LemmaProperty::REMOVABLE); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, true, LemmaProperty::REMOVABLE, THEORY_LAST); + // pass the trust node that was sent from the theory + lemma(tconflict, LemmaProperty::REMOVABLE, THEORY_LAST, theoryId); } } -void TheoryEngine::getExplanation( +theory::TrustNode TheoryEngine::getExplanation( std::vector<NodeTheoryPair>& explanationVector) { Assert(explanationVector.size() > 0); @@ -1672,8 +1820,13 @@ void TheoryEngine::getExplanation( // Keep only the relevant literals explanationVector.resize(j); + + Node expNode = mkExplanation(explanationVector); + return theory::TrustNode::mkTrustLemma(expNode, nullptr); } +bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } + void TheoryEngine::setUserAttribute(const std::string& attr, Node n, const std::vector<Node>& node_values, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 30b5d9fbb..550a4f496 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -53,6 +53,7 @@ namespace CVC4 { class ResourceManager; +class TheoryEngineProofGenerator; /** * A pair of a theory and a node. This is used to mark the flow of @@ -141,6 +142,13 @@ class TheoryEngine { //--------------------------------- new proofs /** Proof node manager used by this theory engine, if proofs are enabled */ ProofNodeManager* d_pnm; + /** The lazy proof object + * + * This stores instructions for how to construct proofs for all theory lemmas. + */ + std::shared_ptr<LazyCDProof> d_lazyProof; + /** The proof generator */ + std::shared_ptr<TheoryEngineProofGenerator> d_tepg; //--------------------------------- end new proofs /** @@ -205,8 +213,12 @@ class TheoryEngine { /** * Called by the theories to notify of a conflict. + * + * @param conflict The trust node containing the conflict and its proof + * generator (if it exists), + * @param theoryId The theory that sent the conflict */ - void conflict(TNode conflict, theory::TheoryId theoryId); + void conflict(theory::TrustNode conflict, theory::TheoryId theoryId); /** * Debugging flag to ensure that shutdown() is called before the @@ -282,13 +294,16 @@ class TheoryEngine { /** * Adds a new lemma, returning its status. * @param node the lemma - * @param negated should the lemma be asserted negated * @param p the properties of the lemma. + * @param atomsTo the theory that atoms of the lemma should be sent to + * @param from the theory that sent the lemma + * @return a lemma status, containing the lemma and context information + * about when it was sent. */ - theory::LemmaStatus lemma(TNode node, - bool negated, + theory::LemmaStatus lemma(theory::TrustNode node, theory::LemmaProperty p, - theory::TheoryId atomsTo); + theory::TheoryId atomsTo = theory::THEORY_LAST, + theory::TheoryId from = theory::THEORY_LAST); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); @@ -437,7 +452,11 @@ class TheoryEngine { * where the node is the one to be explained, and the theory is the * theory that sent the literal. */ - void getExplanation(std::vector<NodeTheoryPair>& explanationVector); + theory::TrustNode getExplanation( + std::vector<NodeTheoryPair>& explanationVector); + + /** Are proofs enabled? */ + bool isProofEnabled() const; public: /** @@ -555,7 +574,7 @@ class TheoryEngine { /** * Returns an explanation of the node propagated to the SAT solver. */ - Node getExplanation(TNode node); + theory::TrustNode getExplanation(TNode node); /** * Get the pointer to the model object used by this theory engine. |