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 : : * extended rewriting class
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
16 : : #define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
17 : :
18 : : #include <unordered_map>
19 : :
20 : : #include "expr/node.h"
21 : : #include "expr/subs.h"
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : :
26 : : class Rewriter;
27 : :
28 : : namespace quantifiers {
29 : :
30 : : /** Extended rewriter
31 : : *
32 : : * This class is used for all rewriting that is not necessarily
33 : : * helpful for quantifier-free solving, but is helpful
34 : : * in other use cases. An example of this is SyGuS, where rewriting
35 : : * can be used for generalizing refinement lemmas, and hence
36 : : * should be highly aggressive.
37 : : *
38 : : * This class extended the standard techniques for rewriting
39 : : * with techniques, including but not limited to:
40 : : * - Redundant child elimination,
41 : : * - Sorting children of commutative operators,
42 : : * - Boolean constraint propagation,
43 : : * - Equality chain normalization,
44 : : * - Negation normal form,
45 : : * - Simple ITE pulling,
46 : : * - ITE conditional variable elimination,
47 : : * - ITE condition subsumption.
48 : : */
49 : : class ExtendedRewriter
50 : : {
51 : : public:
52 : : ExtendedRewriter(NodeManager* nm, Rewriter& rew, bool aggr = true);
53 : 570307 : ~ExtendedRewriter() {}
54 : : /** return the extended rewritten form of n */
55 : : Node extendedRewrite(Node n) const;
56 : :
57 : : private:
58 : : /** Pointer to the underlying node manager */
59 : : NodeManager* d_nm;
60 : : /** The underlying rewriter that we are extending */
61 : : Rewriter& d_rew;
62 : : /** cache that the extended rewritten form of n is ret */
63 : : void setCache(Node n, Node ret) const;
64 : : /** get the cache for n */
65 : : Node getCache(Node n) const;
66 : : /** add to children
67 : : *
68 : : * Adds nc to the vector of children, if dropDup is true, we do not add
69 : : * nc if it already occurs in children. This method returns false in this
70 : : * case, otherwise it returns true.
71 : : */
72 : : bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup) const;
73 : :
74 : : //--------------------------------------generic utilities
75 : : /** Rewrite ITE, for example:
76 : : *
77 : : * ite( ~C, s, t ) ---> ite( C, t, s )
78 : : * ite( A or B, s, t ) ---> ite( ~A and ~B, t, s )
79 : : * ite( x = c, x, t ) --> ite( x = c, c, t )
80 : : * t * { x -> c } = s => ite( x = c, s, t ) ---> t
81 : : *
82 : : * The parameter "full" indicates an effort level that this rewrite will
83 : : * take. If full is false, then we do only perform rewrites that
84 : : * strictly decrease the term size of n.
85 : : */
86 : : Node extendedRewriteIte(Kind itek, Node n, bool full = true) const;
87 : : /** Rewrite AND/OR
88 : : *
89 : : * This implements BCP, factoring, and equality resolution for the Boolean
90 : : * term n whose top symbolic is AND/OR.
91 : : */
92 : : Node extendedRewriteAndOr(Node n) const;
93 : : /** Pull ITE, for example:
94 : : *
95 : : * D=C2 ---> false
96 : : * implies
97 : : * D=ite( C, C1, C2 ) ---> C ^ D=C1
98 : : *
99 : : * f(t,t1) --> s and f(t,t2)---> s
100 : : * implies
101 : : * f(t,ite(C,t1,t2)) ---> s
102 : : *
103 : : * If this function returns a non-null node ret, then n ---> ret.
104 : : */
105 : : Node extendedRewritePullIte(Kind itek, Node n) const;
106 : : /** Negation Normal Form (NNF), for example:
107 : : *
108 : : * ~( A & B ) ---> ( ~ A | ~B )
109 : : * ~( ite( A, B, C ) ---> ite( A, ~B, ~C )
110 : : *
111 : : * If this function returns a non-null node ret, then n ---> ret.
112 : : */
113 : : Node extendedRewriteNnf(Node n) const;
114 : : /** (type-independent) Boolean constraint propagation, for example:
115 : : *
116 : : * ~A & ( B V A ) ---> ~A & B
117 : : * A & ( B = ( A V C ) ) ---> A & B
118 : : *
119 : : * This function takes as arguments the kinds that specify AND, OR, and NOT.
120 : : * It additionally takes as argument a map bcp_kinds. If this map is
121 : : * non-empty, then all terms that have a Kind that is *not* in this map should
122 : : * be treated as immutable. This is for instance to prevent propagation
123 : : * beneath illegal terms. As an example:
124 : : * (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but
125 : : * (bvand A (bvadd A B)) is not equivalent to (bvand A (bvadd 1..1 B)),
126 : : * hence, when using this function to do BCP for bit-vectors, we have that
127 : : * BITVECTOR_AND is a bcp_kind, but BITVECTOR_ADD is not.
128 : : *
129 : : * If this function returns a non-null node ret, then n ---> ret.
130 : : */
131 : : Node extendedRewriteBcp(Kind andk,
132 : : Kind ork,
133 : : Kind notk,
134 : : std::map<Kind, bool>& bcp_kinds,
135 : : Node n) const;
136 : : /** (type-independent) factoring, for example:
137 : : *
138 : : * ( A V B ) ^ ( A V C ) ----> A V ( B ^ C )
139 : : * ( A ^ B ) V ( A ^ C ) ----> A ^ ( B V C )
140 : : *
141 : : * This function takes as arguments the kinds that specify AND, OR.
142 : : * We assume that the children of n do not contain duplicates.
143 : : */
144 : : Node extendedRewriteFactoring(Kind andk, Kind ork, Node n) const;
145 : : /** (type-independent) equality resolution, for example:
146 : : *
147 : : * ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
148 : : * ( A V ~B ) & ( A = B ) ----> ( A = B )
149 : : * ( A V B ) & ( A xor B ) ----> ( A xor B )
150 : : * ( A & B ) V ( A xor B ) ----> B V ( A xor B )
151 : : *
152 : : * This function takes as arguments the kinds that specify AND, OR, EQUAL,
153 : : * and NOT. The equal kind eqk is interpreted as XOR if isXor is true.
154 : : * It additionally takes as argument a map bcp_kinds, which
155 : : * serves the same purpose as the above function.
156 : : * If this function returns a non-null node ret, then n ---> ret.
157 : : */
158 : : Node extendedRewriteEqRes(Kind andk,
159 : : Kind ork,
160 : : Kind eqk,
161 : : Kind notk,
162 : : std::map<Kind, bool>& bcp_kinds,
163 : : Node n,
164 : : bool isXor = false) const;
165 : : /** (type-independent) Equality chain rewriting, for example:
166 : : *
167 : : * A = ( A = B ) ---> B
168 : : * ( A = D ) = ( C = B ) ---> A = ( B = ( C = D ) )
169 : : * A = ( A & B ) ---> ~A | B
170 : : *
171 : : * If this function returns a non-null node ret, then n ---> ret.
172 : : * This function takes as arguments the kinds that specify EQUAL, AND, OR,
173 : : * and NOT. If the flag isXor is true, the eqk is treated as XOR.
174 : : */
175 : : Node extendedRewriteEqChain(Kind eqk,
176 : : Kind andk,
177 : : Kind ork,
178 : : Kind notk,
179 : : Node n,
180 : : bool isXor = false) const;
181 : : /** extended rewrite aggressive
182 : : *
183 : : * All aggressive rewriting techniques (those that should be prioritized
184 : : * at a lower level) go in this function.
185 : : */
186 : : Node extendedRewriteAggr(Node n) const;
187 : : /** Decompose right associative chain
188 : : *
189 : : * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and
190 : : * appends t1...tn to children.
191 : : */
192 : : Node decomposeRightAssocChain(Kind k,
193 : : Node n,
194 : : std::vector<Node>& children) const;
195 : : /** Make right associative chain
196 : : *
197 : : * Sorts children to obtain list { tn...t1 }, and returns the term
198 : : * f( ... f( f( base, tn ), t{n-1} ) ... t1 ).
199 : : */
200 : : Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children) const;
201 : : /** Partial substitute
202 : : *
203 : : * Applies the substitution specified by assign to n, recursing only beneath
204 : : * terms whose Kind appears in rkinds (when rkinds is empty), and additionally
205 : : * never recursing beneath WITNESS.
206 : : */
207 : : Node partialSubstitute(Node n,
208 : : const std::map<Node, Node>& assign,
209 : : const std::map<Kind, bool>& rkinds) const;
210 : : /** same as above, with the subs utility */
211 : : Node partialSubstitute(Node n,
212 : : const Subs& subs,
213 : : const std::map<Kind, bool>& rkinds) const;
214 : : /** solve equality
215 : : *
216 : : * If this function returns a non-null node n', then n' is equivalent to n
217 : : * and is of the form that can be used by inferSubstitution below.
218 : : */
219 : : Node solveEquality(Node n) const;
220 : : /** infer substitution
221 : : *
222 : : * If n is an equality of the form x = t, where t is either:
223 : : * (1) a constant, or
224 : : * (2) a variable y such that x < y based on an ordering,
225 : : * then this method adds {x -> y} to subs and return true, otherwise
226 : : * it returns false.
227 : : * If usePred is true, we may additionally add n -> true, or n[0] -> false
228 : : * is n is a negation.
229 : : */
230 : : bool inferSubstitution(Node n, Subs& subs, bool usePred = false) const;
231 : : /** extended rewrite
232 : : *
233 : : * Prints debug information, indicating the rewrite n ---> ret was found.
234 : : */
235 : : void debugExtendedRewrite(Node n, Node ret, const char* c) const;
236 : : //--------------------------------------end generic utilities
237 : :
238 : : //--------------------------------------theory-specific top-level calls
239 : : /**
240 : : * If these methods return a non-null node ret', then ret is equivalent to
241 : : * ret'.
242 : : */
243 : : Node extendedRewriteStrings(const Node& ret) const;
244 : : Node extendedRewriteSets(const Node& ret) const;
245 : : //--------------------------------------end theory-specific top-level calls
246 : :
247 : : /**
248 : : * Whether this extended rewriter applies aggressive rewriting techniques,
249 : : * which are more expensive. Examples of aggressive rewriting include:
250 : : * - conditional rewriting,
251 : : * - condition merging,
252 : : * - sorting childing of commutative operators with more than 5 children.
253 : : *
254 : : * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
255 : : * may be applied as a preprocessing step.
256 : : */
257 : : bool d_aggr;
258 : : /** Common constant nodes */
259 : : Node d_true;
260 : : Node d_false;
261 : : Node d_intZero;
262 : : };
263 : :
264 : : } // namespace quantifiers
265 : : } // namespace theory
266 : : } // namespace cvc5::internal
267 : :
268 : : #endif /* CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
|
