From: Andrew Reynolds Date: Fri, 29 Jan 2021 19:27:44 +0000 (-0600) Subject: (proof-new) Distinguish pre vs post rewrites in term conversion proof generator ... X-Git-Tag: cvc5-1.0.0~2340 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce1b2f2fb06150599c231bf0d59b52a07e74c3f5;p=cvc5.git (proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833) This is work towards resolving two kinds of failures on proof-new: (1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things, (2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected. A followup PR will simplify and fix proofs for theory-preprocessing. --- diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index d351d88b6..d37ccf914 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -51,7 +51,8 @@ TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, TermContext* tccb, bool rewriteOps) : d_proof(pnm, nullptr, c, name + "::LazyCDProof"), - d_rewriteMap(c ? c : &d_context), + d_preRewriteMap(c ? c : &d_context), + d_postRewriteMap(c ? c : &d_context), d_policy(pol), d_cpolicy(cpol), d_name(name), @@ -65,23 +66,22 @@ TConvProofGenerator::~TConvProofGenerator() {} void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofGenerator* pg, + bool isPre, PfRule trustId, bool isClosed, uint32_t tctx) { - Node eq = registerRewriteStep(t, s, tctx); + Node eq = registerRewriteStep(t, s, tctx, isPre); if (!eq.isNull()) { d_proof.addLazyStep(eq, pg, trustId, isClosed); } } -void TConvProofGenerator::addRewriteStep(Node t, - Node s, - ProofStep ps, - uint32_t tctx) +void TConvProofGenerator::addRewriteStep( + Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx) { - Node eq = registerRewriteStep(t, s, tctx); + Node eq = registerRewriteStep(t, s, tctx, isPre); if (!eq.isNull()) { d_proof.addStep(eq, ps); @@ -93,31 +93,39 @@ void TConvProofGenerator::addRewriteStep(Node t, PfRule id, const std::vector& children, const std::vector& args, + bool isPre, uint32_t tctx) { - Node eq = registerRewriteStep(t, s, tctx); + Node eq = registerRewriteStep(t, s, tctx, isPre); if (!eq.isNull()) { d_proof.addStep(eq, id, children, args); } } -bool TConvProofGenerator::hasRewriteStep(Node t, uint32_t tctx) const +bool TConvProofGenerator::hasRewriteStep(Node t, + uint32_t tctx, + bool isPre) const { - return !getRewriteStep(t, tctx).isNull(); + return !getRewriteStep(t, tctx, isPre).isNull(); } -Node TConvProofGenerator::getRewriteStep(Node t, uint32_t tctx) const +Node TConvProofGenerator::getRewriteStep(Node t, + uint32_t tctx, + bool isPre) const { Node thash = t; if (d_tcontext != nullptr) { thash = TCtxNode::computeNodeHash(t, tctx); } - return getRewriteStepInternal(thash); + return getRewriteStepInternal(thash, isPre); } -Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx) +Node TConvProofGenerator::registerRewriteStep(Node t, + Node s, + uint32_t tctx, + bool isPre) { if (t == s) { @@ -134,14 +142,15 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx) Assert(tctx == 0); } // should not rewrite term to two different things - if (!getRewriteStepInternal(thash).isNull()) + if (!getRewriteStepInternal(thash, isPre).isNull()) { - Assert(getRewriteStepInternal(thash) == s) + Assert(getRewriteStepInternal(thash, isPre) == s) << identify() << " rewriting " << t << " to both " << s << " and " - << getRewriteStepInternal(thash); + << getRewriteStepInternal(thash, isPre); return Node::null(); } - d_rewriteMap[thash] = s; + NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap; + rm[thash] = s; if (d_cpolicy == TConvCachePolicy::DYNAMIC) { // clear the cache @@ -188,19 +197,23 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) serr << " (see -t tconv-pf-gen-debug for details)"; } serr << std::endl; - serr << " source: " << f[0] << std::endl; - serr << "expected after rewriting: " << f[1] << std::endl; - serr << " actual after rewriting: " << conc[1] << std::endl; + serr << " source: " << f[0] << std::endl; + serr << " requested conclusion: " << f[1] << std::endl; + serr << "conclusion from generator: " << conc[1] << std::endl; if (debugTraceEnabled) { Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl; - serr << "Rewrite steps: " << std::endl; - for (NodeNodeMap::const_iterator it = d_rewriteMap.begin(); - it != d_rewriteMap.end(); - ++it) + for (size_t r = 0; r < 2; r++) { - serr << (*it).first << " -> " << (*it).second << std::endl; + const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap; + serr << "Rewrite steps (" << (r == 0 ? "pre" : "post") + << "):" << std::endl; + for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end(); + ++it) + { + serr << (*it).first << " -> " << (*it).second << std::endl; + } } } Unhandled() << serr.str(); @@ -288,8 +301,8 @@ Node TConvProofGenerator::getProofForRewriting(Node t, { Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl; visited[curHash] = Node::null(); - // did we rewrite the current node (possibly at pre-rewrite)? - Node rcur = getRewriteStepInternal(curHash); + // did we rewrite the current node (at pre-rewrite)? + Node rcur = getRewriteStepInternal(curHash, true); if (!rcur.isNull()) { Trace("tconv-pf-gen-rewrite") @@ -484,13 +497,8 @@ Node TConvProofGenerator::getProofForRewriting(Node t, retHash = TCtxNode::computeNodeHash(cur, curCVal); } // did we rewrite ret (at post-rewrite)? - Node rret; - // only if not ONCE policy, which only does pre-rewrite - if (d_policy != TConvPolicy::ONCE) - { - rret = getRewriteStepInternal(retHash); - } - if (!rret.isNull()) + Node rret = getRewriteStepInternal(retHash, false); + if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT) { Trace("tconv-pf-gen-rewrite") << "*** " << retHash << " postrewrites to " << rret << std::endl; @@ -519,6 +527,8 @@ Node TConvProofGenerator::getProofForRewriting(Node t, } else { + // take its rewrite if it rewrote and we have ONCE rewriting policy + ret = rret.isNull() ? ret : rret; Trace("tconv-pf-gen-rewrite") << "-> (postrewrite) " << curHash << " = " << ret << std::endl; // it is final @@ -553,10 +563,11 @@ void TConvProofGenerator::doCache(Node curHash, } } -Node TConvProofGenerator::getRewriteStepInternal(Node t) const +Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const { - NodeNodeMap::const_iterator it = d_rewriteMap.find(t); - if (it == d_rewriteMap.end()) + const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap; + NodeNodeMap::const_iterator it = rm.find(t); + if (it == rm.end()) { return Node::null(); } diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 0a1f4e70a..dcf8b3fa4 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -144,6 +144,8 @@ class TConvProofGenerator : public ProofGenerator /** * Add rewrite step t --> s based on proof generator. * + * @param isPre Whether the rewrite is applied at prerewrite (pre-order + * traversal). * @param trustId If a null proof generator is provided, we add a step to * the proof that has trustId as the rule and expected as the sole argument. * @param isClosed whether to expect that pg can provide a closed proof for @@ -156,25 +158,28 @@ class TConvProofGenerator : public ProofGenerator void addRewriteStep(Node t, Node s, ProofGenerator* pg, + bool isPre = false, PfRule trustId = PfRule::ASSUME, bool isClosed = false, uint32_t tctx = 0); /** Same as above, for a single step */ - void addRewriteStep(Node t, Node s, ProofStep ps, uint32_t tctx = 0); + void addRewriteStep( + Node t, Node s, ProofStep ps, bool isPre = false, uint32_t tctx = 0); /** Same as above, with explicit arguments */ void addRewriteStep(Node t, Node s, PfRule id, const std::vector& children, const std::vector& args, + bool isPre = false, uint32_t tctx = 0); /** Has rewrite step for term t */ - bool hasRewriteStep(Node t, uint32_t tctx = 0) const; + bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; /** * Get rewrite step for term t, returns the s provided in a call to * addRewriteStep if one exists, or null otherwise. */ - Node getRewriteStep(Node t, uint32_t tctx = 0) const; + Node getRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; /** * Get the proof for formula f. It should be the case that f is of the form * t = t', where t' is the result of rewriting t based on the rewrite steps @@ -194,7 +199,8 @@ class TConvProofGenerator : public ProofGenerator /** The (lazy) context dependent proof object. */ LazyCDProof d_proof; /** map to rewritten forms */ - NodeNodeMap d_rewriteMap; + NodeNodeMap d_preRewriteMap; + NodeNodeMap d_postRewriteMap; /** * Policy for how rewrites are applied to terms. As a simple example, say we * have registered the rewrite steps: @@ -220,7 +226,7 @@ class TConvProofGenerator : public ProofGenerator */ bool d_rewriteOps; /** Get rewrite step for (hash value of) term. */ - Node getRewriteStepInternal(Node thash) const; + Node getRewriteStepInternal(Node thash, bool isPre) const; /** * Adds a proof of t = t' to the proof pf where t' is the result of rewriting * t based on the rewrite steps registered to this class. This method then @@ -231,7 +237,7 @@ class TConvProofGenerator : public ProofGenerator * Register rewrite step, returns the equality t=s if t is distinct from s * and a rewrite step has not already been registered for t. */ - Node registerRewriteStep(Node t, Node s, uint32_t tctx); + Node registerRewriteStep(Node t, Node s, uint32_t tctx, bool isPre); /** cache that r is the rewritten form of cur, pf can provide a proof */ void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf); /** get debug information on this generator */ diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 4f49e1bbe..c2c4b6fd2 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -99,7 +99,7 @@ TrustNode ExpandDefs::expandDefinitions( // ------- ASSUME // n = f Node conc = n.eqNode(f); - tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}); + tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc}, true); } // must recursively expand its definition TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg); @@ -236,7 +236,8 @@ TrustNode ExpandDefs::expandDefinitions( instance, PfRule::MACRO_SR_PRED_INTRO, pfExpChildren, - {conc}); + {conc}, + true); } } // now, call expand definitions again on the result @@ -260,7 +261,7 @@ TrustNode ExpandDefs::expandDefinitions( if (tpg != nullptr) { tpg->addRewriteStep( - n, node, trn.getGenerator(), PfRule::THEORY_EXPAND_DEF); + n, node, trn.getGenerator(), true, PfRule::THEORY_EXPAND_DEF); } } else diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a620a4d22..a57a6d920 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -806,7 +806,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // add previous rewrite steps for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - tcg.addRewriteStep(vvec[j], svec[j], pgs[j]); + // substitutions are pre-rewrites + tcg.addRewriteStep(vvec[j], svec[j], pgs[j], true); } // get the proof for the update to the current substitution Node seqss = subs.eqNode(ss); @@ -851,7 +852,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, true); for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]); + // substitutions are pre-rewrites + tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], true); } // add the proof constructed by the term conversion utility std::shared_ptr pfn = tcpg.getProofFor(eq); diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 9a856fc14..0df521c0b 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -462,6 +462,7 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, PfRule::MACRO_SR_PRED_INTRO, {}, {node.eqNode(skolem)}, + true, cval); } diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 9c2c035a8..cba3bd340 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -118,7 +118,8 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) true, "WitnessFormGenerator::convertToWitnessForm:witness_axiom"); d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); - d_tcpg.addRewriteStep(cur, curw, &d_wintroPf, PfRule::ASSUME, true); + d_tcpg.addRewriteStep( + cur, curw, &d_wintroPf, true, PfRule::ASSUME, true); } else { diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 725fa5cd8..be26510c6 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -382,11 +382,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, << "with proofs: " << rewriteStackTop.d_node << std::endl; Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl; Node eq = rewriteStackTop.d_node.eqNode(cached); + // we make this a post-rewrite, since we are processing a node that + // has finished post-rewriting above tcpg->addRewriteStep(rewriteStackTop.d_node, cached, PfRule::TRUST_REWRITE, {}, - {eq}); + {eq}, + false); // don't overwrite the cache, should be the same rewriteStackTop.d_node = cached; } @@ -485,12 +488,13 @@ RewriteResponse Rewriter::processTrustRewriteResponse( proven[1], PfRule::THEORY_REWRITE, {}, - {proven, tidn, rid}); + {proven, tidn, rid}, + isPre); } else { // store proven rewrite step - tcpg->addRewriteStep(proven[0], proven[1], pg); + tcpg->addRewriteStep(proven[0], proven[1], pg, isPre); } } return RewriteResponse(tresponse.d_status, trn.getNode()); diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 7c01eda0f..3b5e9cee4 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -421,6 +421,7 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) Node TheoryPreprocessor::rewriteWithProof(Node term) { + // FIXME (project #37): should properly distinguish pre vs post rewrite Node termr = Rewriter::rewrite(term); // store rewrite step if tracking proofs and it rewrites if (isProofEnabled()) @@ -431,7 +432,7 @@ Node TheoryPreprocessor::rewriteWithProof(Node term) Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> " << termr << std::endl; // always use term context hash 0 (default) - d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}); + d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, false); } } return termr; @@ -470,6 +471,7 @@ Node TheoryPreprocessor::preprocessWithProof(Node term) } Node termr = trn.getNode(); Assert(term != termr); + // FIXME (project #37): should properly distinguish pre vs post rewrite if (isProofEnabled()) { if (trn.getGenerator() != nullptr) @@ -480,15 +482,19 @@ Node TheoryPreprocessor::preprocessWithProof(Node term) "TheoryPreprocessor::preprocessWithProof"); // always use term context hash 0 (default) d_tpg->addRewriteStep( - term, termr, trn.getGenerator(), PfRule::ASSUME, true); + term, termr, trn.getGenerator(), false, PfRule::ASSUME, true); } else { Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) " << term << " -> " << termr << std::endl; // small step trust - d_tpg->addRewriteStep( - term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)}); + d_tpg->addRewriteStep(term, + termr, + PfRule::THEORY_PREPROCESS, + {}, + {term.eqNode(termr)}, + false); } } termr = rewriteWithProof(termr);