From 60fae1dc65b47723c83469d1fb20a9666ddc84a2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 10 Jul 2020 21:19:01 -0500 Subject: [PATCH] (proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (#4709) We need multiple policies for generic proofs for term conversion, in particular, substitution has a "apply once" semantics which does not apply rewrite steps to a fixpoint like the rewriter. This is required for eliminating SUBS steps in the final proof. Also note that an internal method for getting proofs was generalized, which will be required for doing multiple variants of proofs in this utility in the future. --- src/expr/term_conversion_proof_generator.cpp | 123 ++++++++++++------- src/expr/term_conversion_proof_generator.h | 41 ++++++- 2 files changed, 116 insertions(+), 48 deletions(-) diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 70b429510..bad163375 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -18,9 +18,21 @@ using namespace CVC4::kind; namespace CVC4 { +std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol) +{ + switch (tcpol) + { + case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break; + case TConvPolicy::ONCE: out << "ONCE"; break; + default: out << "TConvPolicy:unknown"; break; + } + return out; +} + TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, - context::Context* c) - : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context) + context::Context* c, + TConvPolicy tpol) + : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context), d_policy(tpol) { } @@ -28,20 +40,20 @@ TConvProofGenerator::~TConvProofGenerator() {} void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofGenerator* pg) { - // should not rewrite term more than once - Assert(!hasRewriteStep(t)); - Node eq = t.eqNode(s); - d_proof.addLazyStep(eq, pg); - d_rewriteMap[t] = s; + Node eq = registerRewriteStep(t, s); + if (!eq.isNull()) + { + d_proof.addLazyStep(eq, pg); + } } void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofStep ps) { - // should not rewrite term more than once - Assert(!hasRewriteStep(t)); - Node eq = t.eqNode(s); - d_proof.addStep(eq, ps); - d_rewriteMap[t] = s; + Node eq = registerRewriteStep(t, s); + if (!eq.isNull()) + { + d_proof.addStep(eq, ps); + } } void TConvProofGenerator::addRewriteStep(Node t, @@ -50,11 +62,11 @@ void TConvProofGenerator::addRewriteStep(Node t, const std::vector& children, const std::vector& args) { - // should not rewrite term more than once - Assert(!hasRewriteStep(t)); - Node eq = t.eqNode(s); - d_proof.addStep(eq, id, children, args); - d_rewriteMap[t] = s; + Node eq = registerRewriteStep(t, s); + if (!eq.isNull()) + { + d_proof.addStep(eq, id, children, args); + } } bool TConvProofGenerator::hasRewriteStep(Node t) const @@ -62,6 +74,22 @@ bool TConvProofGenerator::hasRewriteStep(Node t) const return !getRewriteStep(t).isNull(); } +Node TConvProofGenerator::registerRewriteStep(Node t, Node s) +{ + if (t == s) + { + return Node::null(); + } + // should not rewrite term to two different things + if (!getRewriteStep(t).isNull()) + { + Assert(getRewriteStep(t) == s); + return Node::null(); + } + d_rewriteMap[t] = s; + return t.eqNode(s); +} + std::shared_ptr TConvProofGenerator::getProofFor(Node f) { Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << f @@ -72,29 +100,22 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) Assert(false); return nullptr; } - std::shared_ptr pf = getProofForRewriting(f[0]); - if (pf == nullptr) - { - // failed to generate proof - Trace("tconv-pf-gen") << "...failed to get proof" << std::endl; - Assert(false); - return pf; - } - if (pf->getResult() != f) + // we use the existing proofs + LazyCDProof lpf(d_proof.getManager(), &d_proof); + Node conc = getProofForRewriting(f[0], lpf); + if (conc != f) { Trace("tconv-pf-gen") << "...failed, mismatch: returned proof concludes " - << pf->getResult() << std::endl; + << conc << ", expected " << f << std::endl; Assert(false); return nullptr; } Trace("tconv-pf-gen") << "... success" << std::endl; - return pf; + return lpf.getProofFor(f); } -std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) +Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) { - // we use the existing proofs - LazyCDProof pf(d_proof.getManager(), &d_proof); NodeManager* nm = NodeManager::currentNM(); // Invariant: if visited[t] = s or rewritten[t] = s and t,s are distinct, // then pf is able to generate a proof of t=s. @@ -120,14 +141,23 @@ std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) Node rcur = getRewriteStep(cur); if (!rcur.isNull()) { - // d_proof should have a proof of cur = rcur. Hence there is nothing - // to do here, as pf will reference prg to get the proof from d_proof. - // It may be the case that rcur also rewrites, thus we cannot assign - // the final rewritten form for cur yet. Instead we revisit cur after - // finishing visiting rcur. - rewritten[cur] = rcur; - visit.push_back(cur); - visit.push_back(rcur); + // d_proof has a proof of cur = rcur. Hence there is nothing + // to do here, as pf will reference d_proof to get its proof. + if (d_policy == TConvPolicy::FIXPOINT) + { + // It may be the case that rcur also rewrites, thus we cannot assign + // the final rewritten form for cur yet. Instead we revisit cur after + // finishing visiting rcur. + rewritten[cur] = rcur; + visit.push_back(cur); + visit.push_back(rcur); + } + else + { + Assert(d_policy == TConvPolicy::ONCE); + // not rewriting again, rcur is final + visited[cur] = rcur; + } } else { @@ -140,6 +170,9 @@ std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) itr = rewritten.find(cur); if (itr != rewritten.end()) { + // only can generate partially rewritten nodes when rewrite again is + // true. + Assert(d_policy != TConvPolicy::ONCE); // if it was rewritten, check the status of the rewritten node, // which should be finished now Node rcur = itr->second; @@ -203,7 +236,12 @@ std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) pf.addStep(result, PfRule::CONG, pfChildren, pfArgs); } // did we rewrite ret (at post-rewrite)? - Node rret = getRewriteStep(ret); + Node rret; + // only if not ONCE policy, which only does pre-rewrite + if (d_policy != TConvPolicy::ONCE) + { + rret = getRewriteStep(ret); + } if (!rret.isNull()) { if (cur != ret) @@ -227,9 +265,8 @@ std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) } while (!visit.empty()); Assert(visited.find(t) != visited.end()); Assert(!visited.find(t)->second.isNull()); - // make the overall proof - Node teq = t.eqNode(visited[t]); - return pf.getProofFor(teq); + // return the conclusion of the overall proof + return t.eqNode(visited[t]); } Node TConvProofGenerator::getRewriteStep(Node t) const diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 56b89f65c..d7ff6e8f6 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -24,6 +24,17 @@ namespace CVC4 { +/** A policy for how rewrite steps are applied in TConvProofGenerator */ +enum class TConvPolicy : uint32_t +{ + // steps are applied to fix-point, common use case is PfRule::REWRITE + FIXPOINT, + // steps are applied once at pre-rewrite, common use case is PfRule::SUBS + ONCE, +}; +/** Writes a term conversion policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); + /** * The term conversion proof generator. * @@ -69,8 +80,12 @@ class TConvProofGenerator : public ProofGenerator * @param pnm The proof node manager for constructing ProofNode objects. * @param c The context that this class depends on. If none is provided, * this class is context-independent. + * @param tpol The policy for applying rewrite steps of this class. For + * details, see d_policy. */ - TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr); + TConvProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + TConvPolicy pol = TConvPolicy::FIXPOINT); ~TConvProofGenerator(); /** * Add rewrite step t --> s based on proof generator. @@ -96,7 +111,7 @@ class TConvProofGenerator : public ProofGenerator * t = t', where t' is the result of rewriting t based on the rewrite steps * registered to this class. * - * @param f The fact to get the proof for. + * @param f The equality fact to get the proof for. * @return The proof for f. */ std::shared_ptr getProofFor(Node f) override; @@ -112,10 +127,26 @@ class TConvProofGenerator : public ProofGenerator /** map to rewritten forms */ NodeNodeMap d_rewriteMap; /** - * Get the proof for term t. Returns a proof of t = t' where t' is the - * result of rewriting t based on the rewrite steps registered to this class. + * Policy for how rewrites are applied to terms. As a simple example, say we + * have registered the rewrite steps: + * addRewriteStep( a, f(c), p1 ) + * addRewriteStep( c, d, p2 ) + * Then getProofForRewriting(f(a,c),pf) returns a proof of: + * f(a,c) = f(f(d),d) if d_policy is FIXPOINT, + * f(a,c) = f(f(c),d) if d_policy is ONCE. + */ + TConvPolicy d_policy; + /** + * 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 + * returns the proved equality t = t'. + */ + Node getProofForRewriting(Node t, LazyCDProof& pf); + /** + * 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. */ - std::shared_ptr getProofForRewriting(Node t); + Node registerRewriteStep(Node t, Node s); }; } // namespace CVC4 -- 2.30.2