From 383d061be2bc8162d3379c98ad106555d21e5f86 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Sep 2020 20:02:33 -0500 Subject: (proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056) This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node. This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR. --- src/theory/theory_engine.cpp | 241 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 197 insertions(+), 44 deletions(-) (limited to 'src/theory/theory_engine.cpp') 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()) { // 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& 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 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& 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 newLemmas; std::vector 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 pfChildren; + pfChildren.push_back(lemma); + pfChildren.push_back(tplemma.getProven()); + std::vector 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 explanationVector; - explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + std::vector 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 children; + children.push_back(proven); + std::vector 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& 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_values, -- cgit v1.2.3