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