1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mudathir Mohamed, Gereon Kremer, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* Bags theory rewriter. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/bags/bags_rewriter.h" |
17 |
|
|
18 |
|
#include "expr/emptybag.h" |
19 |
|
#include "theory/bags/normal_form.h" |
20 |
|
#include "util/rational.h" |
21 |
|
#include "util/statistics_registry.h" |
22 |
|
|
23 |
|
using namespace cvc5::kind; |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace bags { |
28 |
|
|
29 |
2209 |
BagsRewriteResponse::BagsRewriteResponse() |
30 |
2209 |
: d_node(Node::null()), d_rewrite(Rewrite::NONE) |
31 |
|
{ |
32 |
2209 |
} |
33 |
|
|
34 |
2209 |
BagsRewriteResponse::BagsRewriteResponse(Node n, Rewrite rewrite) |
35 |
2209 |
: d_node(n), d_rewrite(rewrite) |
36 |
|
{ |
37 |
2209 |
} |
38 |
|
|
39 |
|
BagsRewriteResponse::BagsRewriteResponse(const BagsRewriteResponse& r) |
40 |
|
: d_node(r.d_node), d_rewrite(r.d_rewrite) |
41 |
|
{ |
42 |
|
} |
43 |
|
|
44 |
6335 |
BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics) |
45 |
6335 |
: d_statistics(statistics) |
46 |
|
{ |
47 |
6335 |
d_nm = NodeManager::currentNM(); |
48 |
6335 |
d_zero = d_nm->mkConst(Rational(0)); |
49 |
6335 |
d_one = d_nm->mkConst(Rational(1)); |
50 |
6335 |
} |
51 |
|
|
52 |
1440 |
RewriteResponse BagsRewriter::postRewrite(TNode n) |
53 |
|
{ |
54 |
2880 |
BagsRewriteResponse response; |
55 |
1440 |
if (n.isConst()) |
56 |
|
{ |
57 |
|
// no need to rewrite n if it is already in a normal form |
58 |
134 |
response = BagsRewriteResponse(n, Rewrite::NONE); |
59 |
|
} |
60 |
1306 |
else if (n.getKind() == EQUAL) |
61 |
|
{ |
62 |
328 |
response = postRewriteEqual(n); |
63 |
|
} |
64 |
978 |
else if (NormalForm::areChildrenConstants(n)) |
65 |
|
{ |
66 |
144 |
Node value = NormalForm::evaluate(n); |
67 |
72 |
response = BagsRewriteResponse(value, Rewrite::CONSTANT_EVALUATION); |
68 |
|
} |
69 |
|
else |
70 |
|
{ |
71 |
906 |
Kind k = n.getKind(); |
72 |
906 |
switch (k) |
73 |
|
{ |
74 |
89 |
case MK_BAG: response = rewriteMakeBag(n); break; |
75 |
610 |
case BAG_COUNT: response = rewriteBagCount(n); break; |
76 |
8 |
case DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break; |
77 |
50 |
case UNION_MAX: response = rewriteUnionMax(n); break; |
78 |
55 |
case UNION_DISJOINT: response = rewriteUnionDisjoint(n); break; |
79 |
28 |
case INTERSECTION_MIN: response = rewriteIntersectionMin(n); break; |
80 |
34 |
case DIFFERENCE_SUBTRACT: response = rewriteDifferenceSubtract(n); break; |
81 |
18 |
case DIFFERENCE_REMOVE: response = rewriteDifferenceRemove(n); break; |
82 |
2 |
case BAG_CHOOSE: response = rewriteChoose(n); break; |
83 |
4 |
case BAG_CARD: response = rewriteCard(n); break; |
84 |
2 |
case BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break; |
85 |
2 |
case BAG_FROM_SET: response = rewriteFromSet(n); break; |
86 |
2 |
case BAG_TO_SET: response = rewriteToSet(n); break; |
87 |
2 |
case BAG_MAP: response = postRewriteMap(n); break; |
88 |
|
default: response = BagsRewriteResponse(n, Rewrite::NONE); break; |
89 |
|
} |
90 |
|
} |
91 |
|
|
92 |
2880 |
Trace("bags-rewrite") << "postRewrite " << n << " to " << response.d_node |
93 |
1440 |
<< " by " << response.d_rewrite << "." << std::endl; |
94 |
|
|
95 |
1440 |
if (d_statistics != nullptr) |
96 |
|
{ |
97 |
1306 |
(*d_statistics) << response.d_rewrite; |
98 |
|
} |
99 |
1440 |
if (response.d_node != n) |
100 |
|
{ |
101 |
262 |
return RewriteResponse(RewriteStatus::REWRITE_AGAIN_FULL, response.d_node); |
102 |
|
} |
103 |
1178 |
return RewriteResponse(RewriteStatus::REWRITE_DONE, n); |
104 |
|
} |
105 |
|
|
106 |
769 |
RewriteResponse BagsRewriter::preRewrite(TNode n) |
107 |
|
{ |
108 |
1538 |
BagsRewriteResponse response; |
109 |
769 |
Kind k = n.getKind(); |
110 |
769 |
switch (k) |
111 |
|
{ |
112 |
220 |
case EQUAL: response = preRewriteEqual(n); break; |
113 |
6 |
case SUBBAG: response = rewriteSubBag(n); break; |
114 |
543 |
default: response = BagsRewriteResponse(n, Rewrite::NONE); |
115 |
|
} |
116 |
|
|
117 |
1538 |
Trace("bags-rewrite") << "preRewrite " << n << " to " << response.d_node |
118 |
769 |
<< " by " << response.d_rewrite << "." << std::endl; |
119 |
|
|
120 |
769 |
if (d_statistics != nullptr) |
121 |
|
{ |
122 |
767 |
(*d_statistics) << response.d_rewrite; |
123 |
|
} |
124 |
769 |
if (response.d_node != n) |
125 |
|
{ |
126 |
47 |
return RewriteResponse(RewriteStatus::REWRITE_AGAIN_FULL, response.d_node); |
127 |
|
} |
128 |
722 |
return RewriteResponse(RewriteStatus::REWRITE_DONE, n); |
129 |
|
} |
130 |
|
|
131 |
220 |
BagsRewriteResponse BagsRewriter::preRewriteEqual(const TNode& n) const |
132 |
|
{ |
133 |
220 |
Assert(n.getKind() == EQUAL); |
134 |
220 |
if (n[0] == n[1]) |
135 |
|
{ |
136 |
|
// (= A A) = true where A is a bag |
137 |
41 |
return BagsRewriteResponse(d_nm->mkConst(true), Rewrite::IDENTICAL_NODES); |
138 |
|
} |
139 |
179 |
return BagsRewriteResponse(n, Rewrite::NONE); |
140 |
|
} |
141 |
|
|
142 |
6 |
BagsRewriteResponse BagsRewriter::rewriteSubBag(const TNode& n) const |
143 |
|
{ |
144 |
6 |
Assert(n.getKind() == SUBBAG); |
145 |
|
|
146 |
|
// (bag.is_included A B) = ((difference_subtract A B) == emptybag) |
147 |
12 |
Node emptybag = d_nm->mkConst(EmptyBag(n[0].getType())); |
148 |
12 |
Node subtract = d_nm->mkNode(DIFFERENCE_SUBTRACT, n[0], n[1]); |
149 |
12 |
Node equal = subtract.eqNode(emptybag); |
150 |
12 |
return BagsRewriteResponse(equal, Rewrite::SUB_BAG); |
151 |
|
} |
152 |
|
|
153 |
89 |
BagsRewriteResponse BagsRewriter::rewriteMakeBag(const TNode& n) const |
154 |
|
{ |
155 |
89 |
Assert(n.getKind() == MK_BAG); |
156 |
|
// return emptybag for negative or zero multiplicity |
157 |
89 |
if (n[1].isConst() && n[1].getConst<Rational>().sgn() != 1) |
158 |
|
{ |
159 |
|
// (mkBag x c) = emptybag where c <= 0 |
160 |
18 |
Node emptybag = d_nm->mkConst(EmptyBag(n.getType())); |
161 |
9 |
return BagsRewriteResponse(emptybag, Rewrite::MK_BAG_COUNT_NEGATIVE); |
162 |
|
} |
163 |
80 |
return BagsRewriteResponse(n, Rewrite::NONE); |
164 |
|
} |
165 |
|
|
166 |
610 |
BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const |
167 |
|
{ |
168 |
610 |
Assert(n.getKind() == BAG_COUNT); |
169 |
610 |
if (n[1].isConst() && n[1].getKind() == EMPTYBAG) |
170 |
|
{ |
171 |
|
// (bag.count x emptybag) = 0 |
172 |
16 |
return BagsRewriteResponse(d_zero, Rewrite::COUNT_EMPTY); |
173 |
|
} |
174 |
594 |
if (n[1].getKind() == MK_BAG && n[0] == n[1][0]) |
175 |
|
{ |
176 |
|
// (bag.count x (mkBag x c) = c |
177 |
16 |
return BagsRewriteResponse(n[1][1], Rewrite::COUNT_MK_BAG); |
178 |
|
} |
179 |
578 |
return BagsRewriteResponse(n, Rewrite::NONE); |
180 |
|
} |
181 |
|
|
182 |
8 |
BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const |
183 |
|
{ |
184 |
8 |
Assert(n.getKind() == DUPLICATE_REMOVAL); |
185 |
26 |
if (n[0].getKind() == MK_BAG && n[0][1].isConst() |
186 |
26 |
&& n[0][1].getConst<Rational>().sgn() == 1) |
187 |
|
{ |
188 |
|
// (duplicate_removal (mkBag x n)) = (mkBag x 1) |
189 |
|
// where n is a positive constant |
190 |
4 |
Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], d_one); |
191 |
2 |
return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_MK_BAG); |
192 |
|
} |
193 |
6 |
return BagsRewriteResponse(n, Rewrite::NONE); |
194 |
|
} |
195 |
|
|
196 |
50 |
BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const |
197 |
|
{ |
198 |
50 |
Assert(n.getKind() == UNION_MAX); |
199 |
50 |
if (n[1].getKind() == EMPTYBAG || n[0] == n[1]) |
200 |
|
{ |
201 |
|
// (union_max A A) = A |
202 |
|
// (union_max A emptybag) = A |
203 |
4 |
return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_SAME_OR_EMPTY); |
204 |
|
} |
205 |
46 |
if (n[0].getKind() == EMPTYBAG) |
206 |
|
{ |
207 |
|
// (union_max emptybag A) = A |
208 |
2 |
return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_EMPTY); |
209 |
|
} |
210 |
|
|
211 |
172 |
if ((n[1].getKind() == UNION_MAX || n[1].getKind() == UNION_DISJOINT) |
212 |
140 |
&& (n[0] == n[1][0] || n[0] == n[1][1])) |
213 |
|
{ |
214 |
|
// (union_max A (union_max A B)) = (union_max A B) |
215 |
|
// (union_max A (union_max B A)) = (union_max B A) |
216 |
|
// (union_max A (union_disjoint A B)) = (union_disjoint A B) |
217 |
|
// (union_max A (union_disjoint B A)) = (union_disjoint B A) |
218 |
8 |
return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_UNION_LEFT); |
219 |
|
} |
220 |
|
|
221 |
140 |
if ((n[0].getKind() == UNION_MAX || n[0].getKind() == UNION_DISJOINT) |
222 |
116 |
&& (n[0][0] == n[1] || n[0][1] == n[1])) |
223 |
|
{ |
224 |
|
// (union_max (union_max A B) A)) = (union_max A B) |
225 |
|
// (union_max (union_max B A) A)) = (union_max B A) |
226 |
|
// (union_max (union_disjoint A B) A)) = (union_disjoint A B) |
227 |
|
// (union_max (union_disjoint B A) A)) = (union_disjoint B A) |
228 |
8 |
return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_UNION_RIGHT); |
229 |
|
} |
230 |
28 |
return BagsRewriteResponse(n, Rewrite::NONE); |
231 |
|
} |
232 |
|
|
233 |
55 |
BagsRewriteResponse BagsRewriter::rewriteUnionDisjoint(const TNode& n) const |
234 |
|
{ |
235 |
55 |
Assert(n.getKind() == UNION_DISJOINT); |
236 |
55 |
if (n[1].getKind() == EMPTYBAG) |
237 |
|
{ |
238 |
|
// (union_disjoint A emptybag) = A |
239 |
2 |
return BagsRewriteResponse(n[0], Rewrite::UNION_DISJOINT_EMPTY_RIGHT); |
240 |
|
} |
241 |
53 |
if (n[0].getKind() == EMPTYBAG) |
242 |
|
{ |
243 |
|
// (union_disjoint emptybag A) = A |
244 |
3 |
return BagsRewriteResponse(n[1], Rewrite::UNION_DISJOINT_EMPTY_LEFT); |
245 |
|
} |
246 |
156 |
if ((n[0].getKind() == UNION_MAX && n[1].getKind() == INTERSECTION_MIN) |
247 |
194 |
|| (n[1].getKind() == UNION_MAX && n[0].getKind() == INTERSECTION_MIN)) |
248 |
|
|
249 |
|
{ |
250 |
|
// (union_disjoint (union_max A B) (intersection_min A B)) = |
251 |
|
// (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) |
252 |
|
// check if the operands of union_max and intersection_min are the same |
253 |
8 |
std::set<Node> left(n[0].begin(), n[0].end()); |
254 |
8 |
std::set<Node> right(n[1].begin(), n[1].end()); |
255 |
6 |
if (left == right) |
256 |
|
{ |
257 |
8 |
Node rewritten = d_nm->mkNode(UNION_DISJOINT, n[0][0], n[0][1]); |
258 |
4 |
return BagsRewriteResponse(rewritten, Rewrite::UNION_DISJOINT_MAX_MIN); |
259 |
|
} |
260 |
|
} |
261 |
46 |
return BagsRewriteResponse(n, Rewrite::NONE); |
262 |
|
} |
263 |
|
|
264 |
28 |
BagsRewriteResponse BagsRewriter::rewriteIntersectionMin(const TNode& n) const |
265 |
|
{ |
266 |
28 |
Assert(n.getKind() == INTERSECTION_MIN); |
267 |
28 |
if (n[0].getKind() == EMPTYBAG) |
268 |
|
{ |
269 |
|
// (intersection_min emptybag A) = emptybag |
270 |
2 |
return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_EMPTY_LEFT); |
271 |
|
} |
272 |
26 |
if (n[1].getKind() == EMPTYBAG) |
273 |
|
{ |
274 |
|
// (intersection_min A emptybag) = emptybag |
275 |
2 |
return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_EMPTY_RIGHT); |
276 |
|
} |
277 |
24 |
if (n[0] == n[1]) |
278 |
|
{ |
279 |
|
// (intersection_min A A) = A |
280 |
2 |
return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SAME); |
281 |
|
} |
282 |
22 |
if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) |
283 |
|
{ |
284 |
8 |
if (n[0] == n[1][0] || n[0] == n[1][1]) |
285 |
|
{ |
286 |
|
// (intersection_min A (union_disjoint A B)) = A |
287 |
|
// (intersection_min A (union_disjoint B A)) = A |
288 |
|
// (intersection_min A (union_max A B)) = A |
289 |
|
// (intersection_min A (union_max B A)) = A |
290 |
8 |
return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SHARED_LEFT); |
291 |
|
} |
292 |
|
} |
293 |
|
|
294 |
14 |
if (n[0].getKind() == UNION_DISJOINT || n[0].getKind() == UNION_MAX) |
295 |
|
{ |
296 |
8 |
if (n[1] == n[0][0] || n[1] == n[0][1]) |
297 |
|
{ |
298 |
|
// (intersection_min (union_disjoint A B) A) = A |
299 |
|
// (intersection_min (union_disjoint B A) A) = A |
300 |
|
// (intersection_min (union_max A B) A) = A |
301 |
|
// (intersection_min (union_max B A) A) = A |
302 |
8 |
return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_SHARED_RIGHT); |
303 |
|
} |
304 |
|
} |
305 |
|
|
306 |
6 |
return BagsRewriteResponse(n, Rewrite::NONE); |
307 |
|
} |
308 |
|
|
309 |
34 |
BagsRewriteResponse BagsRewriter::rewriteDifferenceSubtract( |
310 |
|
const TNode& n) const |
311 |
|
{ |
312 |
34 |
Assert(n.getKind() == DIFFERENCE_SUBTRACT); |
313 |
34 |
if (n[0].getKind() == EMPTYBAG || n[1].getKind() == EMPTYBAG) |
314 |
|
{ |
315 |
|
// (difference_subtract A emptybag) = A |
316 |
|
// (difference_subtract emptybag A) = emptybag |
317 |
4 |
return BagsRewriteResponse(n[0], Rewrite::SUBTRACT_RETURN_LEFT); |
318 |
|
} |
319 |
30 |
if (n[0] == n[1]) |
320 |
|
{ |
321 |
|
// (difference_subtract A A) = emptybag |
322 |
4 |
Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); |
323 |
2 |
return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_SAME); |
324 |
|
} |
325 |
|
|
326 |
28 |
if (n[0].getKind() == UNION_DISJOINT) |
327 |
|
{ |
328 |
4 |
if (n[1] == n[0][0]) |
329 |
|
{ |
330 |
|
// (difference_subtract (union_disjoint A B) A) = B |
331 |
|
return BagsRewriteResponse(n[0][1], |
332 |
2 |
Rewrite::SUBTRACT_DISJOINT_SHARED_LEFT); |
333 |
|
} |
334 |
2 |
if (n[1] == n[0][1]) |
335 |
|
{ |
336 |
|
// (difference_subtract (union_disjoint B A) A) = B |
337 |
|
return BagsRewriteResponse(n[0][0], |
338 |
2 |
Rewrite::SUBTRACT_DISJOINT_SHARED_RIGHT); |
339 |
|
} |
340 |
|
} |
341 |
|
|
342 |
24 |
if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) |
343 |
|
{ |
344 |
8 |
if (n[0] == n[1][0] || n[0] == n[1][1]) |
345 |
|
{ |
346 |
|
// (difference_subtract A (union_disjoint A B)) = emptybag |
347 |
|
// (difference_subtract A (union_disjoint B A)) = emptybag |
348 |
|
// (difference_subtract A (union_max A B)) = emptybag |
349 |
|
// (difference_subtract A (union_max B A)) = emptybag |
350 |
16 |
Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); |
351 |
8 |
return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_FROM_UNION); |
352 |
|
} |
353 |
|
} |
354 |
|
|
355 |
16 |
if (n[0].getKind() == INTERSECTION_MIN) |
356 |
|
{ |
357 |
4 |
if (n[1] == n[0][0] || n[1] == n[0][1]) |
358 |
|
{ |
359 |
|
// (difference_subtract (intersection_min A B) A) = emptybag |
360 |
|
// (difference_subtract (intersection_min B A) A) = emptybag |
361 |
8 |
Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); |
362 |
4 |
return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_MIN); |
363 |
|
} |
364 |
|
} |
365 |
|
|
366 |
12 |
return BagsRewriteResponse(n, Rewrite::NONE); |
367 |
|
} |
368 |
|
|
369 |
18 |
BagsRewriteResponse BagsRewriter::rewriteDifferenceRemove(const TNode& n) const |
370 |
|
{ |
371 |
18 |
Assert(n.getKind() == DIFFERENCE_REMOVE); |
372 |
|
|
373 |
18 |
if (n[0].getKind() == EMPTYBAG || n[1].getKind() == EMPTYBAG) |
374 |
|
{ |
375 |
|
// (difference_remove A emptybag) = A |
376 |
|
// (difference_remove emptybag B) = emptybag |
377 |
4 |
return BagsRewriteResponse(n[0], Rewrite::REMOVE_RETURN_LEFT); |
378 |
|
} |
379 |
|
|
380 |
14 |
if (n[0] == n[1]) |
381 |
|
{ |
382 |
|
// (difference_remove A A) = emptybag |
383 |
4 |
Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); |
384 |
2 |
return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_SAME); |
385 |
|
} |
386 |
|
|
387 |
12 |
if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) |
388 |
|
{ |
389 |
8 |
if (n[0] == n[1][0] || n[0] == n[1][1]) |
390 |
|
{ |
391 |
|
// (difference_remove A (union_disjoint A B)) = emptybag |
392 |
|
// (difference_remove A (union_disjoint B A)) = emptybag |
393 |
|
// (difference_remove A (union_max A B)) = emptybag |
394 |
|
// (difference_remove A (union_max B A)) = emptybag |
395 |
16 |
Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); |
396 |
8 |
return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_FROM_UNION); |
397 |
|
} |
398 |
|
} |
399 |
|
|
400 |
4 |
if (n[0].getKind() == INTERSECTION_MIN) |
401 |
|
{ |
402 |
4 |
if (n[1] == n[0][0] || n[1] == n[0][1]) |
403 |
|
{ |
404 |
|
// (difference_remove (intersection_min A B) A) = emptybag |
405 |
|
// (difference_remove (intersection_min B A) A) = emptybag |
406 |
8 |
Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); |
407 |
4 |
return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_MIN); |
408 |
|
} |
409 |
|
} |
410 |
|
|
411 |
|
return BagsRewriteResponse(n, Rewrite::NONE); |
412 |
|
} |
413 |
|
|
414 |
2 |
BagsRewriteResponse BagsRewriter::rewriteChoose(const TNode& n) const |
415 |
|
{ |
416 |
2 |
Assert(n.getKind() == BAG_CHOOSE); |
417 |
2 |
if (n[0].getKind() == MK_BAG && n[0][1].isConst()) |
418 |
|
{ |
419 |
|
// (bag.choose (mkBag x c)) = x where c is a constant > 0 |
420 |
2 |
return BagsRewriteResponse(n[0][0], Rewrite::CHOOSE_MK_BAG); |
421 |
|
} |
422 |
|
return BagsRewriteResponse(n, Rewrite::NONE); |
423 |
|
} |
424 |
|
|
425 |
4 |
BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const |
426 |
|
{ |
427 |
4 |
Assert(n.getKind() == BAG_CARD); |
428 |
4 |
if (n[0].getKind() == MK_BAG && n[0][1].isConst()) |
429 |
|
{ |
430 |
|
// (bag.card (mkBag x c)) = c where c is a constant > 0 |
431 |
2 |
return BagsRewriteResponse(n[0][1], Rewrite::CARD_MK_BAG); |
432 |
|
} |
433 |
|
|
434 |
2 |
if (n[0].getKind() == UNION_DISJOINT) |
435 |
|
{ |
436 |
|
// (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B)) |
437 |
4 |
Node A = d_nm->mkNode(BAG_CARD, n[0][0]); |
438 |
4 |
Node B = d_nm->mkNode(BAG_CARD, n[0][1]); |
439 |
4 |
Node plus = d_nm->mkNode(PLUS, A, B); |
440 |
2 |
return BagsRewriteResponse(plus, Rewrite::CARD_DISJOINT); |
441 |
|
} |
442 |
|
|
443 |
|
return BagsRewriteResponse(n, Rewrite::NONE); |
444 |
|
} |
445 |
|
|
446 |
2 |
BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const |
447 |
|
{ |
448 |
2 |
Assert(n.getKind() == BAG_IS_SINGLETON); |
449 |
2 |
if (n[0].getKind() == MK_BAG) |
450 |
|
{ |
451 |
|
// (bag.is_singleton (mkBag x c)) = (c == 1) |
452 |
4 |
Node equal = n[0][1].eqNode(d_one); |
453 |
2 |
return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_MK_BAG); |
454 |
|
} |
455 |
|
return BagsRewriteResponse(n, Rewrite::NONE); |
456 |
|
} |
457 |
|
|
458 |
2 |
BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const |
459 |
|
{ |
460 |
2 |
Assert(n.getKind() == BAG_FROM_SET); |
461 |
2 |
if (n[0].getKind() == SINGLETON) |
462 |
|
{ |
463 |
|
// (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) |
464 |
4 |
TypeNode type = n[0].getType().getSetElementType(); |
465 |
4 |
Node bag = d_nm->mkBag(type, n[0][0], d_one); |
466 |
2 |
return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); |
467 |
|
} |
468 |
|
return BagsRewriteResponse(n, Rewrite::NONE); |
469 |
|
} |
470 |
|
|
471 |
2 |
BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const |
472 |
|
{ |
473 |
2 |
Assert(n.getKind() == BAG_TO_SET); |
474 |
8 |
if (n[0].getKind() == MK_BAG && n[0][1].isConst() |
475 |
8 |
&& n[0][1].getConst<Rational>().sgn() == 1) |
476 |
|
{ |
477 |
|
// (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) |
478 |
|
// where n is a positive constant and T is the type of the bag's elements |
479 |
4 |
Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]); |
480 |
2 |
return BagsRewriteResponse(set, Rewrite::TO_SINGLETON); |
481 |
|
} |
482 |
|
return BagsRewriteResponse(n, Rewrite::NONE); |
483 |
|
} |
484 |
|
|
485 |
328 |
BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const |
486 |
|
{ |
487 |
328 |
Assert(n.getKind() == kind::EQUAL); |
488 |
328 |
if (n[0] == n[1]) |
489 |
|
{ |
490 |
|
Node ret = d_nm->mkConst(true); |
491 |
|
return BagsRewriteResponse(ret, Rewrite::EQ_REFL); |
492 |
|
} |
493 |
|
|
494 |
328 |
if (n[0].isConst() && n[1].isConst()) |
495 |
|
{ |
496 |
26 |
Node ret = d_nm->mkConst(false); |
497 |
13 |
return BagsRewriteResponse(ret, Rewrite::EQ_CONST_FALSE); |
498 |
|
} |
499 |
|
|
500 |
|
// standard ordering |
501 |
315 |
if (n[0] > n[1]) |
502 |
|
{ |
503 |
54 |
Node ret = d_nm->mkNode(kind::EQUAL, n[1], n[0]); |
504 |
27 |
return BagsRewriteResponse(ret, Rewrite::EQ_SYM); |
505 |
|
} |
506 |
288 |
return BagsRewriteResponse(n, Rewrite::NONE); |
507 |
|
} |
508 |
|
|
509 |
2 |
BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const |
510 |
|
{ |
511 |
2 |
Assert(n.getKind() == kind::BAG_MAP); |
512 |
2 |
if (n[1].isConst()) |
513 |
|
{ |
514 |
|
// (bag.map f emptybag) = emptybag |
515 |
|
// (bag.map f (bag "a" 3)) = (bag (f "a") 3) |
516 |
4 |
std::map<Node, Rational> elements = NormalForm::getBagElements(n[1]); |
517 |
4 |
std::map<Node, Rational> mappedElements; |
518 |
2 |
std::map<Node, Rational>::iterator it = elements.begin(); |
519 |
2 |
while (it != elements.end()) |
520 |
|
{ |
521 |
|
Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], it->first); |
522 |
|
mappedElements[mappedElement] = it->second; |
523 |
|
++it; |
524 |
|
} |
525 |
4 |
TypeNode t = d_nm->mkBagType(n[0].getType().getRangeType()); |
526 |
4 |
Node ret = NormalForm::constructConstantBagFromElements(t, mappedElements); |
527 |
2 |
return BagsRewriteResponse(ret, Rewrite::MAP_CONST); |
528 |
|
} |
529 |
|
Kind k = n[1].getKind(); |
530 |
|
switch (k) |
531 |
|
{ |
532 |
|
case MK_BAG: |
533 |
|
{ |
534 |
|
Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], n[1][0]); |
535 |
|
Node ret = d_nm->mkNode(MK_BAG, mappedElement, n[1][0]); |
536 |
|
return BagsRewriteResponse(ret, Rewrite::MAP_MK_BAG); |
537 |
|
} |
538 |
|
|
539 |
|
case UNION_DISJOINT: |
540 |
|
{ |
541 |
|
Node a = d_nm->mkNode(BAG_MAP, n[1][0]); |
542 |
|
Node b = d_nm->mkNode(BAG_MAP, n[1][1]); |
543 |
|
Node ret = d_nm->mkNode(UNION_DISJOINT, a, b); |
544 |
|
return BagsRewriteResponse(ret, Rewrite::MAP_UNION_DISJOINT); |
545 |
|
} |
546 |
|
|
547 |
|
default: return BagsRewriteResponse(n, Rewrite::NONE); |
548 |
|
} |
549 |
|
} |
550 |
|
} // namespace bags |
551 |
|
} // namespace theory |
552 |
22746 |
} // namespace cvc5 |