/****************************************************************************** * Top contributors (to current version): * Andrew Reynolds, Gereon Kremer * * This file is part of the cvc5 project. * * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. * **************************************************************************** * * Term conversion proof generator utility. */ #include "cvc5_private.h" #ifndef CVC5__PROOF__CONV_PROOF_GENERATOR_H #define CVC5__PROOF__CONV_PROOF_GENERATOR_H #include "context/cdhashmap.h" #include "proof/lazy_proof.h" #include "proof/proof_generator.h" namespace cvc5 { class ProofNodeManager; class TermContext; /** 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); /** A policy for how proofs are cached in TConvProofGenerator */ enum class TConvCachePolicy : uint32_t { // proofs are statically cached STATIC, // proofs are dynamically cached, cleared when a new rewrite is added DYNAMIC, // proofs are never cached NEVER, }; /** Writes a term conversion cache policy name to a stream. */ std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); /** * The term conversion proof generator. * * This class is used for proofs of t = t', where t' is obtained from t by * applying (context-free) small step rewrites on subterms of t. Its main * interface functions are: * (1) addRewriteStep(t,s,) which notifies this class that t * rewrites to s, where justification is either a proof generator or proof * step, * (2) getProofFor(f) where f is any equality that can be justified by the * rewrite steps given above. * * For example, say we make the following calls: * addRewriteStep(a,b,P1) * addRewriteStep(f(a),c,P2) * addRewriteStep(c,d,P3) * where P1 and P2 are proof steps. Afterwards, this class may justify any * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c, * c->d, based on the strategy outlined below [***]. For example, the call to: * getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e))) * will return the proof: * CONG( * TRANS(P2,P3), ; f(a)=d * CONG(P1 :args h), ; h(a)=h(b) * REFL(:args f(e)) ; f(e)=f(e) * :args g) * * [***] This class traverses the left hand side of a given equality-to-prove * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite * steps to obtain its rewritten form. To do so, it applies any available * rewrite step at pre-rewrite (pre-order traversal) and post-rewrite * (post-order traversal) based on whether the user specified pre-rewrite or a * post-rewrite during addRewriteStep. * * This class may additionally be used for term-context-sensitive rewrite * systems. An example is the term formula removal pass which rewrites * terms dependending on whether they occur in a "term position", for details * see RtfTermContext in expr/term_context.h. To use this class in a way * that takes into account term contexts, the user of the term conversion * proof generator should: * (1) Provide a term context callback to the constructor of this class (tccb), * (2) Register rewrite steps that indicate the term context identifier of * the rewrite, which is a uint32_t. * * For example, RtfTermContext uses hash value 2 to indicate we are in a "term * position". Say the user of this class calls: * addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2) * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if * (and A B) occurs in a term position, where pg is a proof generator that can * provide a closed proof of: * (= (and A B) BOOLEAN_TERM_VARIABLE_1) * Subsequently, this class may respond to a call to getProofFor on: * (= * (or (and A B) (P (and A B))) * (or (and A B) (P BOOLEAN_TERM_VARIABLE_1))) * where P is a predicate Bool -> Bool. The proof returned by this class * involves congruence and pg's proof of the equivalence above. In particular, * assuming its proof of the equivalence is P1, this proof is: * (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1))) * Notice the callback provided to this class ensures that the rewrite is * replayed in the expected way, e.g. the occurrence of (and A B) that is not * in term position is not rewritten. */ class TConvProofGenerator : public ProofGenerator { public: /** * Constructor, which notice does fixpoint rewriting (since this is the * most common use case) and never caches. * * @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. * @param cpol The caching policy for this generator. * @param name The name of this generator (for debugging). * @param tccb The term context callback that this class depends on. If this * is non-null, then this class stores a term-context-sensitive rewrite * system. The rewrite steps should be given term context identifiers. */ TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr, TConvPolicy pol = TConvPolicy::FIXPOINT, TConvCachePolicy cpol = TConvCachePolicy::NEVER, std::string name = "TConvProofGenerator", TermContext* tccb = nullptr, bool rewriteOps = false); ~TConvProofGenerator(); /** * 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 * this fact. * @param tctx The term context identifier for the rewrite step. This * value should correspond to one generated by the term context callback * class provided in the argument tccb provided to the constructor of this * class. */ 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, 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, 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, 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 * registered to this class. * * @param f The equality fact to get the proof for. * @return The proof for f. */ std::shared_ptr getProofFor(Node f) override; /** Identify this generator (for debugging, etc..) */ std::string identify() const override; /** * Get the proof for how term n would rewrite. This is in contrast to the * above method where the user provides an equality (= n n'). The motivation * for this method is when it may be expensive to compute n', and hence it * is preferred that the proof checker computes the rewritten form of * n, instead of verifying that n has rewritten form n'. */ std::shared_ptr getProofForRewriting(Node n); protected: typedef context::CDHashMap NodeNodeMap; /** A dummy context used by this class if none is provided */ context::Context d_context; /** The (lazy) context dependent proof object. */ LazyCDProof d_proof; /** map to rewritten forms */ 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: * 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; /** The cache policy */ TConvCachePolicy d_cpolicy; /** Name identifier */ std::string d_name; /** The cache for terms */ std::map > d_cache; /** An (optional) term context object */ TermContext* d_tcontext; /** * Whether we rewrite operators. If this flag is true, then the main * traversal algorithm of this proof generator traverses operators of * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary. */ bool d_rewriteOps; /** Get rewrite step for (hash value of) term. */ 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 * returns the proved equality t = t'. */ Node getProofForRewriting(Node t, LazyCDProof& pf, TermContext* tc = nullptr); /** * 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, 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 */ std::string toStringDebug() const; }; } // namespace cvc5 #endif /* CVC5__PROOF__CONV_PROOF_GENERATOR_H */