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"
26 class ProofNodeManager
;
29 /** A policy for how rewrite steps are applied in TConvProofGenerator */
30 enum class TConvPolicy
: uint32_t
32 // steps are applied to fix-point, common use case is PfRule::REWRITE
34 // steps are applied once at pre-rewrite, common use case is PfRule::SUBS
37 /** Writes a term conversion policy name to a stream. */
38 std::ostream
& operator<<(std::ostream
& out
, TConvPolicy tcpol
);
40 /** A policy for how proofs are cached in TConvProofGenerator */
41 enum class TConvCachePolicy
: uint32_t
43 // proofs are statically cached
45 // proofs are dynamically cached, cleared when a new rewrite is added
47 // proofs are never cached
50 /** Writes a term conversion cache policy name to a stream. */
51 std::ostream
& operator<<(std::ostream
& out
, TConvCachePolicy tcpol
);
54 * The term conversion proof generator.
56 * This class is used for proofs of t = t', where t' is obtained from t by
57 * applying (context-free) small step rewrites on subterms of t. Its main
58 * interface functions are:
59 * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
60 * rewrites to s, where justification is either a proof generator or proof
62 * (2) getProofFor(f) where f is any equality that can be justified by the
63 * rewrite steps given above.
65 * For example, say we make the following calls:
66 * addRewriteStep(a,b,P1)
67 * addRewriteStep(f(a),c,P2)
68 * addRewriteStep(c,d,P3)
69 * where P1 and P2 are proof steps. Afterwards, this class may justify any
70 * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
71 * c->d, based on the strategy outlined below [***]. For example, the call to:
72 * getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
73 * will return the proof:
75 * TRANS(P2,P3), ; f(a)=d
76 * CONG(P1 :args h), ; h(a)=h(b)
77 * REFL(:args f(e)) ; f(e)=f(e)
80 * [***] This class traverses the left hand side of a given equality-to-prove
81 * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
82 * steps to obtain its rewritten form. To do so, it applies any available
83 * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
84 * (post-order traversal). It thus does not require the user of this class to
85 * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
86 * addRewriteStep. In particular, notice that in the above example, we realize
87 * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
88 * ending with f(a)=f(b).
90 * This class may additionally be used for term-context-sensitive rewrite
91 * systems. An example is the term formula removal pass which rewrites
92 * terms dependending on whether they occur in a "term position", for details
93 * see RtfTermContext in expr/term_context.h. To use this class in a way
94 * that takes into account term contexts, the user of the term conversion
95 * proof generator should:
96 * (1) Provide a term context callback to the constructor of this class (tccb),
97 * (2) Register rewrite steps that indicate the term context identifier of
98 * the rewrite, which is a uint32_t.
100 * For example, RtfTermContext uses hash value 2 to indicate we are in a "term
101 * position". Say the user of this class calls:
102 * addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2)
103 * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if
104 * (and A B) occurs in a term position, where pg is a proof generator that can
105 * provide a closed proof of:
106 * (= (and A B) BOOLEAN_TERM_VARIABLE_1)
107 * Subsequently, this class may respond to a call to getProofFor on:
109 * (or (and A B) (P (and A B)))
110 * (or (and A B) (P BOOLEAN_TERM_VARIABLE_1)))
111 * where P is a predicate Bool -> Bool. The proof returned by this class
112 * involves congruence and pg's proof of the equivalence above. In particular,
113 * assuming its proof of the equivalence is P1, this proof is:
114 * (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1)))
115 * Notice the callback provided to this class ensures that the rewrite is
116 * replayed in the expected way, e.g. the occurrence of (and A B) that is not
117 * in term position is not rewritten.
119 class TConvProofGenerator
: public ProofGenerator
123 * Constructor, which notice does fixpoint rewriting (since this is the
124 * most common use case) and never caches.
126 * @param pnm The proof node manager for constructing ProofNode objects.
127 * @param c The context that this class depends on. If none is provided,
128 * this class is context-independent.
129 * @param tpol The policy for applying rewrite steps of this class. For
130 * details, see d_policy.
131 * @param cpol The caching policy for this generator.
132 * @param name The name of this generator (for debugging).
133 * @param tccb The term context callback that this class depends on. If this
134 * is non-null, then this class stores a term-context-sensitive rewrite
135 * system. The rewrite steps should be given term context identifiers.
137 TConvProofGenerator(ProofNodeManager
* pnm
,
138 context::Context
* c
= nullptr,
139 TConvPolicy pol
= TConvPolicy::FIXPOINT
,
140 TConvCachePolicy cpol
= TConvCachePolicy::NEVER
,
141 std::string name
= "TConvProofGenerator",
142 TermContext
* tccb
= nullptr,
143 bool rewriteOps
= false);
144 ~TConvProofGenerator();
146 * Add rewrite step t --> s based on proof generator.
148 * @param isPre Whether the rewrite is applied at prerewrite (pre-order
150 * @param trustId If a null proof generator is provided, we add a step to
151 * the proof that has trustId as the rule and expected as the sole argument.
152 * @param isClosed whether to expect that pg can provide a closed proof for
154 * @param tctx The term context identifier for the rewrite step. This
155 * value should correspond to one generated by the term context callback
156 * class provided in the argument tccb provided to the constructor of this
159 void addRewriteStep(Node t
,
163 PfRule trustId
= PfRule::ASSUME
,
164 bool isClosed
= false,
166 /** Same as above, for a single step */
168 Node t
, Node s
, ProofStep ps
, bool isPre
= false, uint32_t tctx
= 0);
169 /** Same as above, with explicit arguments */
170 void addRewriteStep(Node t
,
173 const std::vector
<Node
>& children
,
174 const std::vector
<Node
>& args
,
177 /** Has rewrite step for term t */
178 bool hasRewriteStep(Node t
, uint32_t tctx
= 0, bool isPre
= false) const;
180 * Get rewrite step for term t, returns the s provided in a call to
181 * addRewriteStep if one exists, or null otherwise.
183 Node
getRewriteStep(Node t
, uint32_t tctx
= 0, bool isPre
= false) const;
185 * Get the proof for formula f. It should be the case that f is of the form
186 * t = t', where t' is the result of rewriting t based on the rewrite steps
187 * registered to this class.
189 * @param f The equality fact to get the proof for.
190 * @return The proof for f.
192 std::shared_ptr
<ProofNode
> getProofFor(Node f
) override
;
193 /** Identify this generator (for debugging, etc..) */
194 std::string
identify() const override
;
197 typedef context::CDHashMap
<Node
, Node
, NodeHashFunction
> NodeNodeMap
;
198 /** A dummy context used by this class if none is provided */
199 context::Context d_context
;
200 /** The (lazy) context dependent proof object. */
202 /** map to rewritten forms */
203 NodeNodeMap d_preRewriteMap
;
204 NodeNodeMap d_postRewriteMap
;
206 * Policy for how rewrites are applied to terms. As a simple example, say we
207 * have registered the rewrite steps:
208 * addRewriteStep( a, f(c), p1 )
209 * addRewriteStep( c, d, p2 )
210 * Then getProofForRewriting(f(a,c),pf) returns a proof of:
211 * f(a,c) = f(f(d),d) if d_policy is FIXPOINT,
212 * f(a,c) = f(f(c),d) if d_policy is ONCE.
214 TConvPolicy d_policy
;
215 /** The cache policy */
216 TConvCachePolicy d_cpolicy
;
217 /** Name identifier */
219 /** The cache for terms */
220 std::map
<Node
, std::shared_ptr
<ProofNode
> > d_cache
;
221 /** An (optional) term context object */
222 TermContext
* d_tcontext
;
224 * Whether we rewrite operators. If this flag is true, then the main
225 * traversal algorithm of this proof generator traverses operators of
226 * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary.
229 /** Get rewrite step for (hash value of) term. */
230 Node
getRewriteStepInternal(Node thash
, bool isPre
) const;
232 * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
233 * t based on the rewrite steps registered to this class. This method then
234 * returns the proved equality t = t'.
236 Node
getProofForRewriting(Node t
, LazyCDProof
& pf
, TermContext
* tc
= nullptr);
238 * Register rewrite step, returns the equality t=s if t is distinct from s
239 * and a rewrite step has not already been registered for t.
241 Node
registerRewriteStep(Node t
, Node s
, uint32_t tctx
, bool isPre
);
242 /** cache that r is the rewritten form of cur, pf can provide a proof */
243 void doCache(Node curHash
, Node cur
, Node r
, LazyCDProof
& pf
);
244 /** get debug information on this generator */
245 std::string
toStringDebug() const;
250 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */