Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The TheoryRewriter class.
11 : : *
12 : : * The interface that theory rewriters implement.
13 : : */
14 : :
15 : : #include "cvc5_private.h"
16 : :
17 : : #ifndef CVC5__THEORY__THEORY_REWRITER_H
18 : : #define CVC5__THEORY__THEORY_REWRITER_H
19 : :
20 : : #include <cvc5/cvc5_proof_rule.h>
21 : :
22 : : #include "expr/node.h"
23 : : #include "proof/trust_node.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : :
28 : : class Rewriter;
29 : :
30 : : /**
31 : : * A context for when to try theory rewrites.
32 : : */
33 : : enum class TheoryRewriteCtx
34 : : {
35 : : // Attempt to use the theory rewrite prior to DSL rewrite reconstruction.
36 : : PRE_DSL,
37 : : // Attempt to use the theory rewrite during subcalls in DSL rewrite
38 : : // reconstruction.
39 : : DSL_SUBCALL,
40 : : // Attempt to use the theory rewrite only after DSL rewrite reconstruction
41 : : // fails.
42 : : POST_DSL,
43 : : };
44 : :
45 : : /** Print a TheoryRewriteCtx to an output stream */
46 : : std::ostream& operator<<(std::ostream& os, TheoryRewriteCtx trc);
47 : :
48 : : /**
49 : : * Theory rewriters signal whether more rewriting is needed (or not)
50 : : * by using a member of this enumeration. See RewriteResponse, below.
51 : : */
52 : : enum RewriteStatus
53 : : {
54 : : /**
55 : : * The node is fully rewritten (no more rewrites apply for the original
56 : : * kind). If the rewrite changes the kind, the rewriter will apply another
57 : : * round of rewrites.
58 : : */
59 : : REWRITE_DONE,
60 : : /** The node may be rewritten further */
61 : : REWRITE_AGAIN,
62 : : /** Subnodes of the node may be rewritten further */
63 : : REWRITE_AGAIN_FULL
64 : : }; /* enum RewriteStatus */
65 : :
66 : : /** Print a RewriteStatus to an output stream */
67 : : std::ostream& operator<<(std::ostream& os, RewriteStatus rs);
68 : :
69 : : /**
70 : : * Instances of this class serve as response codes from
71 : : * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
72 : : * consists of the rewritten node as well as a status that indicates whether
73 : : * more rewriting is needed or not.
74 : : */
75 : : struct RewriteResponse
76 : : {
77 : : const RewriteStatus d_status;
78 : : const Node d_node;
79 : 87646753 : RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
80 : : }; /* struct RewriteResponse */
81 : :
82 : : /** Same as above, with trust node instead of node. */
83 : : struct TrustRewriteResponse
84 : : {
85 : : TrustRewriteResponse(RewriteStatus status,
86 : : Node n,
87 : : Node nr,
88 : : ProofGenerator* pg);
89 : : /** The status of the rewrite */
90 : : const RewriteStatus d_status;
91 : : /**
92 : : * The trust node corresponding to the rewrite.
93 : : */
94 : : TrustNode d_node;
95 : : };
96 : :
97 : : /**
98 : : * The interface that a theory rewriter has to implement.
99 : : *
100 : : * Note: A theory rewriter is expected to handle all kinds of a theory, even
101 : : * the ones that are removed by `Theory::expandDefinition()` since it may be
102 : : * called on terms before the definitions have been expanded.
103 : : */
104 : : class TheoryRewriter
105 : : {
106 : : public:
107 : 804041 : TheoryRewriter(NodeManager* nm) : d_nm(nm) {}
108 : 798866 : virtual ~TheoryRewriter() = default;
109 : :
110 : : /**
111 : : * Registers the rewrites of a given theory with the rewriter.
112 : : *
113 : : * @param rewriter The rewriter to register the rewrites with.
114 : : */
115 : 0 : virtual void registerRewrites(CVC5_UNUSED Rewriter* rewriter) {}
116 : :
117 : : /**
118 : : * Performs a post-rewrite step.
119 : : *
120 : : * @param node The node to rewrite
121 : : */
122 : : virtual RewriteResponse postRewrite(TNode node) = 0;
123 : :
124 : : /**
125 : : * Performs a post-rewrite step, with proofs.
126 : : *
127 : : * @param node The node to rewrite
128 : : */
129 : : virtual TrustRewriteResponse postRewriteWithProof(TNode node);
130 : :
131 : : /**
132 : : * Performs a pre-rewrite step.
133 : : *
134 : : * @param node The node to rewrite
135 : : */
136 : : virtual RewriteResponse preRewrite(TNode node) = 0;
137 : :
138 : : /**
139 : : * Performs a pre-rewrite step, with proofs.
140 : : *
141 : : * @param node The node to rewrite
142 : : */
143 : : virtual TrustRewriteResponse preRewriteWithProof(TNode node);
144 : :
145 : : /** rewrite equality extended
146 : : *
147 : : * This method returns a formula that is equivalent to the equality between
148 : : * two terms s = t, given by node.
149 : : *
150 : : * Specifically, this method performs rewrites whose conclusion is not
151 : : * necessarily one of { s = t, t = s, true, false }. This is in constrast
152 : : * to postRewrite and preRewrite above, where the rewritten form of an
153 : : * equality must be one of these.
154 : : *
155 : : * @param node The node to rewrite
156 : : */
157 : : virtual Node rewriteEqualityExt(Node node);
158 : :
159 : : /** rewrite equality extended, with proofs
160 : : *
161 : : * @param node The node to rewrite
162 : : * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
163 : : * node if no rewrites are applied.
164 : : */
165 : : virtual TrustNode rewriteEqualityExtWithProof(Node node);
166 : :
167 : : /**
168 : : * Expand definitions in the term node. This returns a term that is
169 : : * equivalent to node. If node is unchanged by this method, the
170 : : * null Node may be returned.
171 : : *
172 : : * The purpose of this method is typically to eliminate the operators in node
173 : : * that are syntax sugar that cannot otherwise be eliminated during rewriting.
174 : : * For example, division relies on the introduction of an uninterpreted
175 : : * function for the divide-by-zero case, which we do not introduce with
176 : : * the standard rewrite methods.
177 : : *
178 : : * Some theories have kinds that are effectively definitions and should be
179 : : * expanded before they are handled. Definitions allow a much wider range of
180 : : * actions than the normal forms given by the rewriter. However no
181 : : * assumptions can be made about subterms having been expanded or rewritten.
182 : : * Where possible rewrite rules should be used, definitions should only be
183 : : * used when rewrites are not possible, for example in handling
184 : : * under-specified operations using partially defined functions.
185 : : *
186 : : * @param node The node to expand.
187 : : * @return the expanded form of node.
188 : : */
189 : : virtual Node expandDefinition(Node node);
190 : :
191 : : /**
192 : : * Rewrite n based on the proof rewrite rule id.
193 : : * @param id The rewrite rule.
194 : : * @param n The node to rewrite.
195 : : * @return The rewritten version of n based on id, or Node::null() if n
196 : : * cannot be rewritten.
197 : : */
198 : : virtual Node rewriteViaRule(ProofRewriteRule id, const Node& n);
199 : : /**
200 : : * Find the rewrite that proves a == b, if one exists.
201 : : * If none can be found, return ProofRewriteRule::NONE.
202 : : * @param a The left hand side of the rewrite.
203 : : * @param b The right hand side of the rewrite.
204 : : * @param ctx The context under which we are finding the rewrites.
205 : : * @return An identifier, if one exists, that rewrites a to b. In particular,
206 : : * the returned rule is either ProofRewriteRule::NONE or is a rule id such
207 : : * that rewriteViaRule(id, a) returns b.
208 : : */
209 : : ProofRewriteRule findRule(const Node& a, const Node& b, TheoryRewriteCtx ctx);
210 : :
211 : : protected:
212 : : /**
213 : : * Register proof rewrite rule. This method is called to notify the RARE
214 : : * DSL rewrite rule reconstruction algorithm that the rewrite rule id
215 : : * should be tried during proof reconstruction. This method should be
216 : : * called in the constructor of the theory rewriter.
217 : : *
218 : : * @param id The rewrite rule this theory rewriter implements via
219 : : * rewriteViaRule.
220 : : * @param ctx The context for the rewrite, which indicates when the RARE
221 : : * proof reconstruction should attempt this rule.
222 : : */
223 : : void registerProofRewriteRule(ProofRewriteRule id, TheoryRewriteCtx ctx);
224 : : /** The underlying node manager */
225 : : NodeManager* d_nm;
226 : : /**
227 : : * The proof rewrite rules implemented by this rewriter, for each context.
228 : : * This caches the calls to registerProofRewriteRule.
229 : : */
230 : : std::map<TheoryRewriteCtx, std::vector<ProofRewriteRule>> d_pfTheoryRewrites;
231 : : /** Get a pointer to the node manager */
232 : : NodeManager* nodeManager() const;
233 : : };
234 : :
235 : : /**
236 : : * The null theory rewriter, which does not perform any rewrites. This is used
237 : : * if a theory does not have an (active) rewriter.
238 : : */
239 : : class NoOpTheoryRewriter : public TheoryRewriter
240 : : {
241 : : public:
242 : : NoOpTheoryRewriter(NodeManager* nm, TheoryId tid);
243 : : /** Performs a post-rewrite step. */
244 : : RewriteResponse postRewrite(TNode node) override;
245 : : /** Performs a pre-rewrite step. */
246 : : RewriteResponse preRewrite(TNode node) override;
247 : :
248 : : private:
249 : : /** The theory id */
250 : : TheoryId d_tid;
251 : : };
252 : :
253 : : } // namespace theory
254 : : } // namespace cvc5::internal
255 : :
256 : : #endif /* CVC5__THEORY__THEORY_REWRITER_H */
|
