1 /********************* */
2 /*! \file term_conversion_proof_generator.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Term conversion proof generator utility
15 #include "cvc4_private.h"
17 #ifndef CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
18 #define CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
20 #include "context/cdhashmap.h"
21 #include "expr/lazy_proof.h"
22 #include "expr/proof_generator.h"
23 #include "expr/proof_node_manager.h"
24 #include "expr/term_context.h"
28 /** A policy for how rewrite steps are applied in TConvProofGenerator */
29 enum class TConvPolicy
: uint32_t
31 // steps are applied to fix-point, common use case is PfRule::REWRITE
33 // steps are applied once at pre-rewrite, common use case is PfRule::SUBS
36 /** Writes a term conversion policy name to a stream. */
37 std::ostream
& operator<<(std::ostream
& out
, TConvPolicy tcpol
);
39 /** A policy for how proofs are cached in TConvProofGenerator */
40 enum class TConvCachePolicy
: uint32_t
42 // proofs are statically cached
44 // proofs are dynamically cached, cleared when a new rewrite is added
46 // proofs are never cached
49 /** Writes a term conversion cache policy name to a stream. */
50 std::ostream
& operator<<(std::ostream
& out
, TConvCachePolicy tcpol
);
53 * The term conversion proof generator.
55 * This class is used for proofs of t = t', where t' is obtained from t by
56 * applying (context-free) small step rewrites on subterms of t. Its main
57 * interface functions are:
58 * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
59 * rewrites to s, where justification is either a proof generator or proof
61 * (2) getProofFor(f) where f is any equality that can be justified by the
62 * rewrite steps given above.
64 * For example, say we make the following calls:
65 * addRewriteStep(a,b,P1)
66 * addRewriteStep(f(a),c,P2)
67 * addRewriteStep(c,d,P3)
68 * where P1 and P2 are proof steps. Afterwards, this class may justify any
69 * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
70 * c->d, based on the strategy outlined below [***]. For example, the call to:
71 * getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
72 * will return the proof:
74 * TRANS(P2,P3), ; f(a)=d
75 * CONG(P1 :args h), ; h(a)=h(b)
76 * REFL(:args f(e)) ; f(e)=f(e)
79 * [***] This class traverses the left hand side of a given equality-to-prove
80 * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
81 * steps to obtain its rewritten form. To do so, it applies any available
82 * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
83 * (post-order traversal). It thus does not require the user of this class to
84 * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
85 * addRewriteStep. In particular, notice that in the above example, we realize
86 * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
87 * ending with f(a)=f(b).
89 * This class may additionally be used for term-context-sensitive rewrite
90 * systems. An example is the term formula removal pass which rewrites
91 * terms dependending on whether they occur in a "term position", for details
92 * see RtfTermContext in expr/term_context.h. To use this class in a way
93 * that takes into account term contexts, the user of the term conversion
94 * proof generator should:
95 * (1) Provide a term context callback to the constructor of this class (tccb),
96 * (2) Register rewrite steps that indicate the term context identifier of
97 * the rewrite, which is a uint32_t.
99 * For example, RtfTermContext uses hash value 2 to indicate we are in a "term
100 * position". Say the user of this class calls:
101 * addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2)
102 * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if
103 * (and A B) occurs in a term position, where pg is a proof generator that can
104 * provide a closed proof of:
105 * (= (and A B) BOOLEAN_TERM_VARIABLE_1)
106 * Subsequently, this class may respond to a call to getProofFor on:
108 * (or (and A B) (P (and A B)))
109 * (or (and A B) (P BOOLEAN_TERM_VARIABLE_1)))
110 * where P is a predicate Bool -> Bool. The proof returned by this class
111 * involves congruence and pg's proof of the equivalence above. In particular,
112 * assuming its proof of the equivalence is P1, this proof is:
113 * (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1)))
114 * Notice the callback provided to this class ensures that the rewrite is
115 * replayed in the expected way, e.g. the occurrence of (and A B) that is not
116 * in term position is not rewritten.
118 class TConvProofGenerator
: public ProofGenerator
122 * Constructor, which notice does fixpoint rewriting (since this is the
123 * most common use case) and never caches.
125 * @param pnm The proof node manager for constructing ProofNode objects.
126 * @param c The context that this class depends on. If none is provided,
127 * this class is context-independent.
128 * @param tpol The policy for applying rewrite steps of this class. For
129 * details, see d_policy.
130 * @param cpol The caching policy for this generator.
131 * @param name The name of this generator (for debugging).
132 * @param tccb The term context callback that this class depends on. If this
133 * is non-null, then this class stores a term-context-sensitive rewrite
134 * system. The rewrite steps should be given term context identifiers.
136 TConvProofGenerator(ProofNodeManager
* pnm
,
137 context::Context
* c
= nullptr,
138 TConvPolicy pol
= TConvPolicy::FIXPOINT
,
139 TConvCachePolicy cpol
= TConvCachePolicy::NEVER
,
140 std::string name
= "TConvProofGenerator",
141 TermContext
* tccb
= nullptr,
142 bool rewriteOps
= false);
143 ~TConvProofGenerator();
145 * Add rewrite step t --> s based on proof generator.
147 * @param trustId If a null proof generator is provided, we add a step to
148 * the proof that has trustId as the rule and expected as the sole argument.
149 * @param isClosed whether to expect that pg can provide a closed proof for
151 * @param tctx The term context identifier for the rewrite step. This
152 * value should correspond to one generated by the term context callback
153 * class provided in the argument tccb provided to the constructor of this
156 void addRewriteStep(Node t
,
159 PfRule trustId
= PfRule::ASSUME
,
160 bool isClosed
= false,
162 /** Same as above, for a single step */
163 void addRewriteStep(Node t
, Node s
, ProofStep ps
, uint32_t tctx
= 0);
164 /** Same as above, with explicit arguments */
165 void addRewriteStep(Node t
,
168 const std::vector
<Node
>& children
,
169 const std::vector
<Node
>& args
,
171 /** Has rewrite step for term t */
172 bool hasRewriteStep(Node t
, uint32_t tctx
= 0) const;
174 * Get rewrite step for term t, returns the s provided in a call to
175 * addRewriteStep if one exists, or null otherwise.
177 Node
getRewriteStep(Node t
, uint32_t tctx
= 0) const;
179 * Get the proof for formula f. It should be the case that f is of the form
180 * t = t', where t' is the result of rewriting t based on the rewrite steps
181 * registered to this class.
183 * @param f The equality fact to get the proof for.
184 * @return The proof for f.
186 std::shared_ptr
<ProofNode
> getProofFor(Node f
) override
;
187 /** Identify this generator (for debugging, etc..) */
188 std::string
identify() const override
;
191 typedef context::CDHashMap
<Node
, Node
, NodeHashFunction
> NodeNodeMap
;
192 /** A dummy context used by this class if none is provided */
193 context::Context d_context
;
194 /** The (lazy) context dependent proof object. */
196 /** map to rewritten forms */
197 NodeNodeMap d_rewriteMap
;
199 * Policy for how rewrites are applied to terms. As a simple example, say we
200 * have registered the rewrite steps:
201 * addRewriteStep( a, f(c), p1 )
202 * addRewriteStep( c, d, p2 )
203 * Then getProofForRewriting(f(a,c),pf) returns a proof of:
204 * f(a,c) = f(f(d),d) if d_policy is FIXPOINT,
205 * f(a,c) = f(f(c),d) if d_policy is ONCE.
207 TConvPolicy d_policy
;
208 /** The cache policy */
209 TConvCachePolicy d_cpolicy
;
210 /** Name identifier */
212 /** The cache for terms */
213 std::map
<Node
, std::shared_ptr
<ProofNode
> > d_cache
;
214 /** An (optional) term context object */
215 TermContext
* d_tcontext
;
217 * Whether we rewrite operators. If this flag is true, then the main
218 * traversal algorithm of this proof generator traverses operators of
219 * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary.
222 /** Get rewrite step for (hash value of) term. */
223 Node
getRewriteStepInternal(Node thash
) const;
225 * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
226 * t based on the rewrite steps registered to this class. This method then
227 * returns the proved equality t = t'.
229 Node
getProofForRewriting(Node t
, LazyCDProof
& pf
, TermContext
* tc
= nullptr);
231 * Register rewrite step, returns the equality t=s if t is distinct from s
232 * and a rewrite step has not already been registered for t.
234 Node
registerRewriteStep(Node t
, Node s
, uint32_t tctx
);
235 /** cache that r is the rewritten form of cur, pf can provide a proof */
236 void doCache(Node curHash
, Node cur
, Node r
, LazyCDProof
& pf
);
237 /** get debug information on this generator */
238 std::string
toStringDebug() const;
243 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */