diff options
Diffstat (limited to 'src/proof/conv_proof_generator.h')
| -rw-r--r-- | src/proof/conv_proof_generator.h | 256 |
1 files changed, 256 insertions, 0 deletions
diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h new file mode 100644 index 000000000..f23a661ae --- /dev/null +++ b/src/proof/conv_proof_generator.h @@ -0,0 +1,256 @@ +/****************************************************************************** + * 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,<justification>) 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<Node>& children, + const std::vector<Node>& 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<ProofNode> 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<ProofNode> getProofForRewriting(Node n); + + protected: + typedef context::CDHashMap<Node, Node> 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<Node, std::shared_ptr<ProofNode> > 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 */ |