From bc5056c8927e8fbffbe9e9d103f0a81f8ab49480 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 8 Oct 2020 19:07:52 -0500 Subject: [PATCH] (proof-new) Theory engine proof producing (#5195) This completes proof support in TheoryEngine. The main addition in this PR is to make its getExplanation method proof producing. --- src/smt/smt_solver.cpp | 3 +- src/theory/theory_engine.cpp | 325 +++++++++++++++++++++++++++-------- src/theory/theory_engine.h | 14 +- 3 files changed, 267 insertions(+), 75 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 298706339..8ff022556 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -52,7 +52,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) d_rm, d_pp.getTermFormulaRemover(), logicInfo, - d_smt.getOutputManager())); + d_smt.getOutputManager(), + d_pnm)); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4722251a3..863c67a2b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -22,6 +22,7 @@ #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" +#include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/node_algorithm.h" #include "expr/node_builder.h" @@ -130,7 +131,8 @@ std::string getTheoryString(theory::TheoryId id) } } -void TheoryEngine::finishInit() { +void TheoryEngine::finishInit() +{ // NOTE: This seems to be required since // theory::TheoryTraits::isParametric cannot be accessed without // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR @@ -212,18 +214,21 @@ void TheoryEngine::finishInit() { } } +ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; } + TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, ResourceManager* rm, RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo, - OutputManager& outMgr) + OutputManager& outMgr, + ProofNodeManager* pnm) : d_propEngine(nullptr), d_context(context), d_userContext(userContext), d_logicInfo(logicInfo), d_outMgr(outMgr), - d_pnm(nullptr), + d_pnm(pnm), d_lazyProof( d_pnm != nullptr ? new LazyCDProof( @@ -246,7 +251,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_tpp(*this, iteRemover), + d_tpp(*this, iteRemover, d_pnm), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), d_false(), @@ -852,13 +857,15 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( void TheoryEngine::preprocessStart() { d_tpp.clearCache(); } -Node TheoryEngine::preprocess(TNode assertion) { +Node TheoryEngine::preprocess(TNode assertion) +{ TrustNode trn = d_tpp.theoryPreprocess(assertion); if (trn.isNull()) { // no change return assertion; } + // notice that we could alternatively return the trust node here. return trn.getNode(); } @@ -951,18 +958,16 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo return; } - // Polarity of the assertion - bool polarity = assertion.getKind() != kind::NOT; - - // Atom of the assertion - TNode atom = polarity ? assertion : assertion[0]; - // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { - Assert(atom.getKind() == kind::EQUAL) - << "atom should be an EQUALity, not `" << atom << "'"; + Assert(assertion.getKind() == kind::EQUAL + || (assertion.getKind() == kind::NOT + && assertion[0].getKind() == kind::EQUAL)) + << "atom should be an EQUALity, not `" << assertion << "'"; if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // assert to the shared solver + bool polarity = assertion.getKind() != kind::NOT; + TNode atom = polarity ? assertion : assertion[0]; d_sharedSolver->assertSharedEquality(atom, polarity, assertion); } return; @@ -1004,7 +1009,9 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo return; } - Assert(atom.getKind() == kind::EQUAL); + Assert(assertion.getKind() == kind::EQUAL + || (assertion.getKind() == kind::NOT + && assertion[0].getKind() == kind::EQUAL)); // Normalize Node normalizedLiteral = Rewriter::rewrite(assertion); @@ -1214,42 +1221,11 @@ Node TheoryEngine::getInstantiatedConjunction( Node q ) { } } - -static Node mkExplanation(const std::vector& explanation) { - - std::set all; - for (unsigned i = 0; i < explanation.size(); ++ i) { - Assert(explanation[i].d_theory == THEORY_SAT_SOLVER); - all.insert(explanation[i].d_node); - } - - if (all.size() == 0) { - // Normalize to true - return NodeManager::currentNM()->mkConst(true); - } - - if (all.size() == 1) { - // All the same, or just one - return explanation[0].d_node; - } - - NodeBuilder<> conjunction(kind::AND); - std::set::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} - TrustNode TheoryEngine::getExplanation(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl; - bool polarity = node.getKind() != kind::NOT; TNode atom = polarity ? node : node[0]; @@ -1261,8 +1237,24 @@ TrustNode 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 - << ") => " << texplanation.getNode() << endl; + << ") => " << explanation << endl; + if (isProofEnabled()) + { + texplanation.debugCheckClosed( + "te-proof-exp", "texplanation no share", false); + // check if no generator, if so, add THEORY_LEMMA + if (texplanation.getGenerator() == nullptr) + { + Node proven = texplanation.getProven(); + TheoryId tid = theoryOf(atom)->getId(); + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid); + d_lazyProof->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn}); + texplanation = + TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get()); + } + } return texplanation; } @@ -1280,10 +1272,9 @@ TrustNode TheoryEngine::getExplanation(TNode node) << " is theory: " << nodeExplainerPair.d_theory << std::endl; // Create the workplace for explanations - std::vector explanationVector; - explanationVector.push_back(d_propagationMap[toExplain]); + std::vector vec{d_propagationMap[toExplain]}; // Process the explanation - TrustNode texplanation = getExplanation(explanationVector); + TrustNode texplanation = getExplanation(vec); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << texplanation.getNode() << endl; return texplanation; @@ -1438,6 +1429,9 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, bool removable = isLemmaPropertyRemovable(p); bool preprocess = isLemmaPropertyPreprocess(p); + // ensure closed + tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial"); + // call preprocessor std::vector newLemmas; std::vector newSkolems; @@ -1665,11 +1659,23 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) theory::TrustNode TheoryEngine::getExplanation( std::vector& explanationVector) { - Assert(explanationVector.size() > 0); - + Assert(explanationVector.size() == 1); + Node conclusion = explanationVector[0].d_node; + std::shared_ptr lcp; + if (isProofEnabled()) + { + Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion + << std::endl; + lcp.reset(new LazyCDProof( + d_pnm, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation")); + } unsigned i = 0; // Index of the current literal we are processing - unsigned j = 0; // Index of the last literal we are keeping + std::unique_ptr> inputAssertions = nullptr; + // the overall explanation + std::set exp; + // vector of trust nodes to explain at the end + std::vector> texplains; // cache of nodes we have already explained by some theory std::unordered_map cache; @@ -1691,15 +1697,25 @@ theory::TrustNode TheoryEngine::getExplanation( cache[toExplain.d_node] = toExplain.d_timestamp; // If a true constant or a negation of a false constant we can ignore it - if (toExplain.d_node.isConst() && toExplain.d_node.getConst()) - { - ++ i; - continue; - } - if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst() - && !toExplain.d_node[0].getConst()) + if ((toExplain.d_node.isConst() && toExplain.d_node.getConst()) + || (toExplain.d_node.getKind() == kind::NOT + && toExplain.d_node[0].isConst() + && !toExplain.d_node[0].getConst())) { ++ i; + // if we are building a proof + if (lcp != nullptr) + { + Trace("te-proof-exp") + << "- explain " << toExplain.d_node << " trivially..." << std::endl; + // ------------------MACRO_SR_PRED_INTRO + // toExplain.d_node + std::vector children; + std::vector args; + args.push_back(toExplain.d_node); + lcp->addStep( + toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args); + } continue; } @@ -1707,7 +1723,9 @@ theory::TrustNode TheoryEngine::getExplanation( if (toExplain.d_theory == THEORY_SAT_SOLVER) { Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl; - explanationVector[j++] = explanationVector[i++]; + exp.insert(explanationVector[i++].d_node); + // it will be a free assumption in the proof + Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl; continue; } @@ -1717,12 +1735,23 @@ theory::TrustNode TheoryEngine::getExplanation( Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.d_node << " got from " << toExplain.d_theory << endl; - for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k) + size_t nchild = toExplain.d_node.getNumChildren(); + for (size_t k = 0; k < nchild; ++k) { NodeTheoryPair newExplain( toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp); explanationVector.push_back(newExplain); } + if (lcp != nullptr) + { + Trace("te-proof-exp") + << "- AND expand " << toExplain.d_node << std::endl; + // delay explanation, use a dummy trust node + TrustNode tnAndExp = TrustNode::mkTrustPropExp( + toExplain.d_node, toExplain.d_node, nullptr); + texplains.push_back( + std::pair(THEORY_LAST, tnAndExp)); + } ++ i; continue; } @@ -1742,13 +1771,46 @@ theory::TrustNode TheoryEngine::getExplanation( explanationVector.push_back((*find).second); ++i; + if (lcp != nullptr) + { + if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node)) + { + Trace("te-proof-exp") + << "- t-explained cached: " << toExplain.d_node << " by " + << (*find).second.d_node << std::endl; + // delay explanation, use a dummy trust node that says that + // (*find).second.d_node explains toExplain.d_node. + TrustNode tnRewExp = TrustNode::mkTrustPropExp( + toExplain.d_node, (*find).second.d_node, nullptr); + texplains.push_back( + std::pair(THEORY_LAST, tnRewExp)); + } + } continue; } } - - TrustNode texp = + // It was produced by the theory, so ask for an explanation + TrustNode texplanation = d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory); - Node explanation = texp.getNode(); + if (lcp != nullptr) + { + texplanation.debugCheckClosed("te-proof-exp", "texplanation", false); + Trace("te-proof-exp") + << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node + << " by " << texplanation.getNode() << std::endl; + // if not a trivial explanation + if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node)) + { + // We add it to the list of theory explanations, to be processed at + // the end of this method. We wait to explain here because it may + // be that a later explanation may preempt the need for proving this + // step. For instance, if the conclusion lit is later added as an + // assumption in the final explanation. This avoids cyclic proofs. + texplains.push_back( + std::pair(toExplain.d_theory, texplanation)); + } + } + Node explanation = texplanation.getNode(); Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation @@ -1763,10 +1825,139 @@ theory::TrustNode TheoryEngine::getExplanation( ++ i; } - // Keep only the relevant literals - explanationVector.resize(j); + // make the explanation node + Node expNode; + if (exp.size() == 0) + { + // Normalize to true + expNode = NodeManager::currentNM()->mkConst(true); + } + else if (exp.size() == 1) + { + // All the same, or just one + expNode = *exp.begin(); + } + else + { + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = exp.begin(); + std::set::const_iterator it_end = exp.end(); + while (it != it_end) + { + conjunction << *it; + ++it; + } + expNode = conjunction; + } + // if we are building a proof, go back through the explanations and + // build the proof + if (lcp != nullptr) + { + if (Trace.isOn("te-proof-exp")) + { + Trace("te-proof-exp") << "Explanation is:" << std::endl; + for (const Node& e : exp) + { + Trace("te-proof-exp") << " " << e << std::endl; + } + Trace("te-proof-exp") << "=== Replay explanations..." << std::endl; + } + // Now, go back and add the necessary steps of theory explanations, i.e. + // add those that prove things that aren't in the final explanation. We + // iterate in reverse order so that most recent steps take priority. This + // avoids cyclic proofs in the lazy proof we are building (lcp). + for (std::vector>::reverse_iterator + it = texplains.rbegin(), + itEnd = texplains.rend(); + it != itEnd; + ++it) + { + TrustNode trn = it->second; + Assert(trn.getKind() == TrustNodeKind::PROP_EXP); + Node proven = trn.getProven(); + Assert(proven.getKind() == kind::IMPLIES); + Node tConc = proven[1]; + Trace("te-proof-exp") << "- Process " << trn << std::endl; + if (exp.find(tConc) != exp.end()) + { + // already added to proof + Trace("te-proof-exp") << "...already added" << std::endl; + continue; + } + Node symTConc = CDProof::getSymmFact(tConc); + if (!symTConc.isNull()) + { + if (exp.find(symTConc) != exp.end()) + { + // symmetric direction + Trace("te-proof-exp") << "...already added (SYMM)" << std::endl; + continue; + } + } + // remember that we've explained this formula, to avoid cycles in lcp + exp.insert(tConc); + TheoryId ttid = it->first; + Node tExp = proven[0]; + if (ttid == THEORY_LAST) + { + if (tConc == tExp) + { + // dummy trust node, do AND expansion + Assert(tConc.getKind() == kind::AND); + // tConc[0] ... tConc[n] + // ---------------------- AND_INTRO + // tConc + std::vector pfChildren; + pfChildren.insert(pfChildren.end(), tConc.begin(), tConc.end()); + lcp->addStep(tConc, PfRule::AND_INTRO, pfChildren, {}); + Trace("te-proof-exp") << "...via AND_INTRO" << std::endl; + continue; + } + // otherwise should hold by rewriting + Assert(Rewriter::rewrite(tConc) == Rewriter::rewrite(tExp)); + // tExp + // ---- MACRO_SR_PRED_TRANSFORM + // tConc + lcp->addStep(tConc, PfRule::MACRO_SR_PRED_TRANSFORM, {tExp}, {tConc}); + Trace("te-proof-exp") << "...via MACRO_SR_PRED_TRANSFORM" << std::endl; + continue; + } + if (tExp == tConc) + { + // trivial + Trace("te-proof-exp") << "...trivial" << std::endl; + continue; + } + // ------------- Via theory + // tExp => tConc tExp + // ---------------------------------MACRO_SR_PRED_TRANSFORM + // tConc + if (trn.getGenerator() != nullptr) + { + Trace("te-proof-exp") << "...via theory generator" << std::endl; + lcp->addLazyStep(proven, trn.getGenerator()); + } + else + { + Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl; + // otherwise, trusted theory lemma + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(it->first); + lcp->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn}); + } + std::vector pfChildren; + pfChildren.push_back(proven); + pfChildren.push_back(trn.getNode()); + std::vector pfArgs; + pfArgs.push_back(tConc); + pfArgs.push_back(mkMethodId(MethodId::SB_FORMULA)); + lcp->addStep(tConc, PfRule::MACRO_SR_PRED_TRANSFORM, pfChildren, pfArgs); + } + // store in the proof generator + TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp); + // return the trust node + return trn; + } - Node expNode = mkExplanation(explanationVector); return theory::TrustNode::mkTrustLemma(expNode, nullptr); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e410bddd5..fd6d1af27 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -42,6 +42,7 @@ #include "theory/term_registration_visitor.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" +#include "theory/trust_node.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" @@ -111,7 +112,6 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; - friend class theory::CombinationEngine; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; friend class theory::SharedSolver; @@ -175,9 +175,6 @@ class TheoryEngine { /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; - typedef std::unordered_map NodeMap; - typedef std::unordered_map TNodeMap; - /** * Output channels for individual theories. */ @@ -315,7 +312,8 @@ class TheoryEngine { ResourceManager* rm, RemoveTermFormulas& iteRemover, const LogicInfo& logic, - OutputManager& outMgr); + OutputManager& outMgr, + ProofNodeManager* pnm); /** Destroys a theory engine */ ~TheoryEngine(); @@ -339,7 +337,7 @@ class TheoryEngine { *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo, - nullptr); + d_pnm); theory::Rewriter::registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } @@ -365,6 +363,9 @@ class TheoryEngine { return d_propEngine; } + /** Get the proof node manager */ + ProofNodeManager* getProofNodeManager() const; + /** * Get a pointer to the underlying sat context. */ @@ -740,7 +741,6 @@ private: private: IntStat d_arithSubstitutionsAdded; - };/* class TheoryEngine */ }/* CVC4 namespace */ -- 2.30.2