From 77fdb2327ae969a7d97b6eb67ad3526d78867b3a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 18 Aug 2020 16:42:22 -0500 Subject: [PATCH] (proof-new) Theory preprocessor proof producing (#4807) This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places. --- src/expr/proof_rule.cpp | 6 +- src/expr/proof_rule.h | 30 ++-- src/theory/builtin/proof_checker.cpp | 13 +- src/theory/theory_engine.cpp | 14 +- src/theory/theory_preprocessor.cpp | 206 +++++++++++++++++++++++---- src/theory/theory_preprocessor.h | 31 +++- 6 files changed, 251 insertions(+), 49 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index be8aaea9b..0a45c6790 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -32,9 +32,13 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; + case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; + //================================================= Trusted rules case PfRule::PREPROCESS: return "PREPROCESS"; + case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; + case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; + case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; - case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index a83e043bf..59c406d28 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -174,29 +174,35 @@ enum class PfRule : uint32_t THEORY_REWRITE, //================================================= Processing rules - // ======== Preprocess (trusted) + // ======== Remove Term Formulas Axiom + // Children: none + // Arguments: (t) + // --------------------------------------------------------------- + // Conclusion: RemoveTermFormulas::getAxiomFor(t). + REMOVE_TERM_FORMULA_AXIOM, + + //================================================= Trusted rules + // The rules in this section have the signature of a "trusted rule": + // // Children: none // Arguments: (F) // --------------------------------------------------------------- // Conclusion: F + // // where F is an equality of the form t = t' where t was replaced by t' // based on some preprocessing pass, or otherwise F was added as a new // assertion by some preprocessing pass. PREPROCESS, - // ======== Witness axiom (trusted) - // Children: none - // Arguments: (F) - // --------------------------------------------------------------- - // Conclusion: F + // where F was added as a new assertion by some preprocessing pass. + PREPROCESS_LEMMA, + // where F is an equality of the form t = Theory::ppRewrite(t) for some + // theory. Notice this is a "trusted" rule. + THEORY_PREPROCESS, + // where F was added as a new assertion by theory preprocessing. + THEORY_PREPROCESS_LEMMA, // where F is an existential (exists ((x T)) (P x)) used for introducing // a witness term (witness ((x T)) (P x)). WITNESS_AXIOM, - // ======== Remove Term Formulas Axiom - // Children: none - // Arguments: (t) - // --------------------------------------------------------------- - // Conclusion: RemoveTermFormulas::getAxiomFor(t). - REMOVE_TERM_FORMULA_AXIOM, //================================================= Boolean rules // ======== Split diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 05c17dedf..7521d116e 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -61,9 +61,13 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); pc->registerChecker(PfRule::THEORY_REWRITE, this); - pc->registerChecker(PfRule::PREPROCESS, this); - pc->registerChecker(PfRule::WITNESS_AXIOM, this); pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); + // trusted rules + pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2); + pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2); + pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2); + pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2); + pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2); } Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite) @@ -330,7 +334,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args.size() == 1); return RemoveTermFormulas::getAxiomFor(args[0]); } - else if (id == PfRule::PREPROCESS || id == PfRule::WITNESS_AXIOM) + else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA + || id == PfRule::THEORY_PREPROCESS + || id == PfRule::THEORY_PREPROCESS_LEMMA + || id == PfRule::WITNESS_AXIOM) { Assert(children.empty()); Assert(args.size() == 1); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e86a09112..f8694e760 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -980,7 +980,13 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa void TheoryEngine::preprocessStart() { d_tpp.clearCache(); } Node TheoryEngine::preprocess(TNode assertion) { - return d_tpp.theoryPreprocess(assertion); + TrustNode trn = d_tpp.theoryPreprocess(assertion); + if (trn.isNull()) + { + // no change + return assertion; + } + return trn.getNode(); } void TheoryEngine::notifyPreprocessedAssertions( @@ -1633,6 +1639,12 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, 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()) + { + tlemma = TrustNode::mkTrustLemma(node); + } + // must use an assertion pipeline due to decision engine below AssertionPipeline lemmas; // make the assertion pipeline diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 328c65fcb..6e569508b 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -14,6 +14,8 @@ #include "theory/theory_preprocessor.h" +#include "expr/lazy_proof.h" +#include "expr/skolem_manager.h" #include "theory/logic_info.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -24,31 +26,90 @@ namespace CVC4 { namespace theory { TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine, - RemoveTermFormulas& tfr) + RemoveTermFormulas& tfr, + ProofNodeManager* pnm) : d_engine(engine), d_logicInfo(engine.getLogicInfo()), d_ppCache(), - d_tfr(tfr) + d_tfr(tfr), + d_pfContext(), + d_tpg(pnm ? new TConvProofGenerator( + pnm, + &d_pfContext, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "TheoryPreprocessor::TConvProofGenerator") + : nullptr), + d_lp(pnm ? new LazyCDProof(pnm, + nullptr, + &d_pfContext, + "TheoryPreprocessor::LazyCDProof") + : nullptr) { + if (isProofEnabled()) + { + // enable proofs in the term formula remover + d_tfr.setProofNodeManager(pnm); + // push the proof context, since proof steps may be cleared on calls to + // clearCache() below. + d_pfContext.push(); + } } TheoryPreprocessor::~TheoryPreprocessor() {} -void TheoryPreprocessor::clearCache() { d_ppCache.clear(); } +void TheoryPreprocessor::clearCache() +{ + d_ppCache.clear(); + // clear proofs from d_tpg and d_lp using internal push/pop context + if (isProofEnabled()) + { + d_pfContext.pop(); + d_pfContext.push(); + } +} TrustNode TheoryPreprocessor::preprocess(TNode node, std::vector& newLemmas, std::vector& newSkolems, bool doTheoryPreprocess) { + // In this method, all rewriting steps of node are stored in d_tpg. + + Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node + << std::endl; // Run theory preprocessing, maybe - Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node); + Node ppNode = node; + if (doTheoryPreprocess) + { + // run theory preprocessing + TrustNode tpp = theoryPreprocess(node); + ppNode = tpp.getNode(); + } + Trace("tpp-proof-debug") + << "TheoryPreprocessor::preprocess: after preprocessing " << ppNode + << std::endl; // Remove the ITEs Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl; TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false); Trace("te-tform-rm") << "..done " << ttfr.getNode() << std::endl; Node retNode = ttfr.getNode(); + if (isProofEnabled()) + { + // if we rewrote + if (retNode != ppNode) + { + // should always have provided a proof generator, or else term formula + // removal and this class do not agree on whether proofs are enabled. + Assert(ttfr.getGenerator() != nullptr); + Trace("tpp-proof-debug") + << "TheoryPreprocessor: addRewriteStep (term formula removal) " + << ppNode << " -> " << retNode << std::endl; + // store as a rewrite in d_tpg + d_tpg->addRewriteStep(ppNode, retNode, ttfr.getGenerator()); + } + } if (Debug.isOn("lemma-ites")) { @@ -62,14 +123,25 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, } Debug("lemma-ites") << endl; } - - retNode = Rewriter::rewrite(retNode); + // Rewrite the main node, we rewrite and store the proof step, if necessary, + // in d_tpg, which maintains the fact that d_tpg can prove the rewrite. + Trace("tpp-proof-debug") + << "TheoryPreprocessor::preprocess: rewrite returned node " << retNode + << std::endl; + retNode = rewriteWithProof(retNode); + Trace("tpp-proof-debug") + << "TheoryPreprocessor::preprocess: after rewriting is " << retNode + << std::endl; // now, rewrite the lemmas + Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas" + << std::endl; for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) { // get the trust node to process TrustNode trn = newLemmas[i]; + trn.debugCheckClosed( + "tpp-proof-debug", "TheoryPreprocessor::lemma_new_initial", false); Assert(trn.getKind() == TrustNodeKind::LEMMA); Node assertion = trn.getNode(); // rewrite, which is independent of d_tpg, since additional lemmas @@ -77,11 +149,37 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, Node rewritten = Rewriter::rewrite(assertion); if (assertion != rewritten) { - // not tracking proofs, just make new - newLemmas[i] = TrustNode::mkTrustLemma(rewritten, nullptr); + if (isProofEnabled()) + { + Assert(d_lp != nullptr); + // store in the lazy proof + d_lp->addLazyStep(assertion, + trn.getGenerator(), + true, + "TheoryPreprocessor::rewrite_lemma_new", + false, + PfRule::THEORY_PREPROCESS_LEMMA); + d_lp->addStep(rewritten, + PfRule::MACRO_SR_PRED_TRANSFORM, + {assertion}, + {rewritten}); + } + newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get()); } + Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr); + newLemmas[i].debugCheckClosed("tpp-proof-debug", + "TheoryPreprocessor::lemma_new"); } - return TrustNode::mkTrustRewrite(node, retNode, nullptr); + if (node == retNode) + { + // no change + return TrustNode::null(); + } + Trace("tpp-proof-debug") << "Preprocessed: " << node << " " << retNode + << std::endl; + TrustNode tret = TrustNode::mkTrustRewrite(node, retNode, d_tpg.get()); + tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret"); + return tret; } struct preprocess_stack_element @@ -91,7 +189,7 @@ struct preprocess_stack_element preprocess_stack_element(TNode n) : node(n), children_added(false) {} }; -Node TheoryPreprocessor::theoryPreprocess(TNode assertion) +TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion) { Trace("theory::preprocess") << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl; @@ -158,7 +256,7 @@ Node TheoryPreprocessor::theoryPreprocess(TNode assertion) Node result = builder; if (result != current) { - result = Rewriter::rewrite(result); + result = rewriteWithProof(result); } Debug("theory::internal") << "TheoryPreprocessor::theoryPreprocess(" << assertion @@ -196,9 +294,9 @@ Node TheoryPreprocessor::theoryPreprocess(TNode assertion) } } } - // Return the substituted version - return d_ppCache[assertion]; + Node res = d_ppCache[assertion]; + return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get()); } // Recursively traverse a term and call the theory rewriter on its sub-terms @@ -212,18 +310,13 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) unsigned nc = term.getNumChildren(); if (nc == 0) { - TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term); - return trn.isNull() ? Node(term) : trn.getNode(); + return preprocessWithProof(term); } Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; - Node newTerm; + Node newTerm = term; // do not rewrite inside quantifiers - if (term.isClosure()) - { - newTerm = Rewriter::rewrite(term); - } - else + if (!term.isClosure()) { NodeBuilder<> newNode(term.getKind()); if (term.getMetaKind() == kind::metakind::PARAMETERIZED) @@ -235,18 +328,75 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) { newNode << ppTheoryRewrite(term[i]); } - newTerm = Rewriter::rewrite(Node(newNode)); - } - TrustNode trn = d_engine.theoryOf(newTerm)->ppRewrite(newTerm); - Node newTerm2 = trn.isNull() ? newTerm : trn.getNode(); - if (newTerm != newTerm2) - { - newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2)); + newTerm = Node(newNode); } + newTerm = rewriteWithProof(newTerm); + newTerm = preprocessWithProof(newTerm); d_ppCache[term] = newTerm; Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl; return newTerm; } +Node TheoryPreprocessor::rewriteWithProof(Node term) +{ + Node termr = Rewriter::rewrite(term); + // store rewrite step if tracking proofs and it rewrites + if (isProofEnabled()) + { + // may rewrite the same term more than once, thus check hasRewriteStep + if (termr != term) + { + Trace("tpp-proof-debug") + << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> " + << termr << std::endl; + d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}); + } + } + return termr; +} + +Node TheoryPreprocessor::preprocessWithProof(Node term) +{ + // Important that it is in rewritten form, to ensure that the rewrite steps + // recorded in d_tpg are functional. In other words, there should not + // be steps from the same term to multiple rewritten forms, which would be + // the case if we registered a preprocessing step for a non-rewritten term. + Assert(term == Rewriter::rewrite(term)); + // call ppRewrite for the given theory + TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term); + if (trn.isNull()) + { + // no change, return original term + return term; + } + Node termr = trn.getNode(); + Assert(term != termr); + if (isProofEnabled()) + { + if (trn.getGenerator() != nullptr) + { + Trace("tpp-proof-debug") + << "TheoryPreprocessor: addRewriteStep (generator) " << term << " -> " + << termr << std::endl; + trn.debugCheckClosed("tpp-proof-debug", + "TheoryPreprocessor::preprocessWithProof"); + d_tpg->addRewriteStep(term, termr, trn.getGenerator()); + } + else + { + Trace("tpp-proof-debug") + << "TheoryPreprocessor: addRewriteStep (trusted) " << term << " -> " + << termr << std::endl; + // small step trust + d_tpg->addRewriteStep( + term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)}); + } + } + termr = rewriteWithProof(termr); + return ppTheoryRewrite(termr); +} + +bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; } + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 2f3813e68..95236ded3 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -19,15 +19,16 @@ #include +#include "expr/lazy_proof.h" #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" +#include "expr/term_conversion_proof_generator.h" +#include "theory/trust_node.h" namespace CVC4 { class LogicInfo; class TheoryEngine; class RemoveTermFormulas; -class LazyCDProof; namespace theory { @@ -40,7 +41,9 @@ class TheoryPreprocessor public: /** Constructs a theory preprocessor */ - TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr); + TheoryPreprocessor(TheoryEngine& engine, + RemoveTermFormulas& tfr, + ProofNodeManager* pnm = nullptr); /** Destroys a theory preprocessor */ ~TheoryPreprocessor(); /** Clear the cache of this class */ @@ -69,7 +72,7 @@ class TheoryPreprocessor * the formula. This is only called on input assertions, after ITEs * have been removed. */ - Node theoryPreprocess(TNode node); + TrustNode theoryPreprocess(TNode node); private: /** Reference to owning theory engine */ @@ -80,8 +83,28 @@ class TheoryPreprocessor NodeMap d_ppCache; /** The term formula remover */ RemoveTermFormulas& d_tfr; + /** The context for the proof generator below */ + context::Context d_pfContext; + /** A term conversion proof generator */ + std::unique_ptr d_tpg; + /** A lazy proof, for additional lemmas. */ + std::unique_ptr d_lp; /** Helper for theoryPreprocess */ Node ppTheoryRewrite(TNode term); + /** + * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary + * and returns the rewritten form of term. + */ + Node rewriteWithProof(Node term); + /** + * Preprocess with proof, which calls the appropriate ppRewrite method, + * stores the corresponding rewrite step in d_tpg if necessary and returns + * the preprocessed and rewritten form of term. It should be the case that + * term is already in rewritten form. + */ + Node preprocessWithProof(Node term); + /** Proofs enabled */ + bool isProofEnabled() const; }; } // namespace theory -- 2.30.2