1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Kshitij Bansal, Paul Meng |
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 |
|
* Sets theory rewriter. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/sets/theory_sets_rewriter.h" |
17 |
|
|
18 |
|
#include "expr/attribute.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "options/sets_options.h" |
21 |
|
#include "theory/sets/normal_form.h" |
22 |
|
#include "theory/sets/rels_utils.h" |
23 |
|
|
24 |
|
using namespace cvc5::kind; |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace sets { |
29 |
|
|
30 |
1987 |
bool TheorySetsRewriter::checkConstantMembership(TNode elementTerm, TNode setTerm) |
31 |
|
{ |
32 |
1987 |
if(setTerm.getKind() == kind::EMPTYSET) { |
33 |
65 |
return false; |
34 |
|
} |
35 |
|
|
36 |
1922 |
if(setTerm.getKind() == kind::SINGLETON) { |
37 |
727 |
return elementTerm == setTerm[0]; |
38 |
|
} |
39 |
|
|
40 |
1195 |
Assert(setTerm.getKind() == kind::UNION |
41 |
|
&& setTerm[0].getKind() == kind::SINGLETON) |
42 |
|
<< "kind was " << setTerm.getKind() << ", term: " << setTerm; |
43 |
|
|
44 |
3585 |
return elementTerm == setTerm[0][0] |
45 |
3585 |
|| checkConstantMembership(elementTerm, setTerm[1]); |
46 |
|
} |
47 |
|
|
48 |
|
// static |
49 |
96424 |
RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { |
50 |
96424 |
NodeManager* nm = NodeManager::currentNM(); |
51 |
96424 |
Kind kind = node.getKind(); |
52 |
96424 |
Trace("sets-postrewrite") << "Process: " << node << std::endl; |
53 |
|
|
54 |
96424 |
if(node.isConst()) { |
55 |
11970 |
Trace("sets-rewrite-nf") |
56 |
5985 |
<< "Sets::rewrite: no rewrite (constant) " << node << std::endl; |
57 |
|
// Dare you touch the const and mangle it to something else. |
58 |
5985 |
return RewriteResponse(REWRITE_DONE, node); |
59 |
|
} |
60 |
|
|
61 |
90439 |
switch(kind) { |
62 |
|
|
63 |
38534 |
case kind::MEMBER: { |
64 |
38534 |
if(node[0].isConst() && node[1].isConst()) { |
65 |
|
// both are constants |
66 |
2096 |
TNode S = preRewrite(node[1]).d_node; |
67 |
1048 |
bool isMember = checkConstantMembership(node[0], S); |
68 |
1048 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember)); |
69 |
37486 |
}else if( node[1].getKind()==kind::EMPTYSET ){ |
70 |
295 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(false)); |
71 |
37191 |
}else if( node[1].getKind()==kind::SINGLETON ){ |
72 |
2241 |
return RewriteResponse(REWRITE_AGAIN_FULL, nm->mkNode(kind::EQUAL, node[0], node[1][0] ) ); |
73 |
34950 |
}else if( node[1].getKind()==kind::UNION || node[1].getKind()==kind::INTERSECTION || node[1].getKind()==kind::SETMINUS ){ |
74 |
8168 |
std::vector< Node > children; |
75 |
12252 |
for( unsigned i=0; i<node[1].getNumChildren(); i++ ){ |
76 |
16336 |
Node nc = nm->mkNode(kind::MEMBER, node[0], node[1][i] ); |
77 |
8168 |
if( node[1].getKind()==kind::SETMINUS && i==1 ){ |
78 |
871 |
nc = nc.negate(); |
79 |
|
} |
80 |
8168 |
children.push_back( nc ); |
81 |
|
} |
82 |
4084 |
return RewriteResponse(REWRITE_AGAIN_FULL, nm->mkNode( node[1].getKind()==kind::UNION ? kind::OR : kind::AND, children ) ); |
83 |
|
} |
84 |
30866 |
break; |
85 |
|
}//kind::MEMBER |
86 |
|
|
87 |
|
case kind::SUBSET: { |
88 |
|
Assert(false) |
89 |
|
<< "TheorySets::postRrewrite(): Subset is handled in preRewrite."; |
90 |
|
|
91 |
|
// but in off-chance we do end up here, let us do our best |
92 |
|
|
93 |
|
// rewrite (A subset-or-equal B) as (A union B = B) |
94 |
|
TNode A = node[0]; |
95 |
|
TNode B = node[1]; |
96 |
|
return RewriteResponse(REWRITE_AGAIN_FULL, |
97 |
|
nm->mkNode(kind::EQUAL, |
98 |
|
nm->mkNode(kind::UNION, A, B), |
99 |
|
B) ); |
100 |
|
}//kind::SUBSET |
101 |
|
|
102 |
30364 |
case kind::EQUAL: { |
103 |
|
//rewrite: t = t with true (t term) |
104 |
|
//rewrite: c = c' with c different from c' false (c, c' constants) |
105 |
|
//otherwise: sort them |
106 |
30364 |
if(node[0] == node[1]) { |
107 |
110 |
Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl; |
108 |
110 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); |
109 |
|
} |
110 |
30254 |
else if (node[0].isConst() && node[1].isConst()) { |
111 |
146 |
Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl; |
112 |
146 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(false)); |
113 |
|
} |
114 |
30108 |
else if (node[0] > node[1]) { |
115 |
12206 |
Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); |
116 |
6103 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; |
117 |
6103 |
return RewriteResponse(REWRITE_DONE, newNode); |
118 |
|
} |
119 |
24005 |
break; |
120 |
|
} |
121 |
|
|
122 |
1662 |
case kind::SETMINUS: |
123 |
|
{ |
124 |
1662 |
if (node[0] == node[1]) |
125 |
|
{ |
126 |
56 |
Node newNode = nm->mkConst(EmptySet(node[0].getType())); |
127 |
56 |
Trace("sets-postrewrite") |
128 |
28 |
<< "Sets::postRewrite returning " << newNode << std::endl; |
129 |
28 |
return RewriteResponse(REWRITE_DONE, newNode); |
130 |
|
} |
131 |
4902 |
else if (node[0].getKind() == kind::EMPTYSET |
132 |
4902 |
|| node[1].getKind() == kind::EMPTYSET) |
133 |
|
{ |
134 |
12 |
Trace("sets-postrewrite") |
135 |
6 |
<< "Sets::postRewrite returning " << node[0] << std::endl; |
136 |
6 |
return RewriteResponse(REWRITE_AGAIN, node[0]); |
137 |
|
} |
138 |
1628 |
else if (node[1].getKind() == kind::SETMINUS && node[1][0] == node[0]) |
139 |
|
{ |
140 |
|
// (setminus A (setminus A B)) = (intersection A B) |
141 |
24 |
Node intersection = nm->mkNode(INTERSECTION, node[0], node[1][1]); |
142 |
12 |
return RewriteResponse(REWRITE_AGAIN, intersection); |
143 |
|
} |
144 |
1616 |
else if (node[1].getKind() == kind::UNIVERSE_SET) |
145 |
|
{ |
146 |
|
return RewriteResponse( |
147 |
|
REWRITE_AGAIN, |
148 |
4 |
NodeManager::currentNM()->mkConst(EmptySet(node[1].getType()))); |
149 |
|
} |
150 |
1612 |
else if (node[0].isConst() && node[1].isConst()) |
151 |
|
{ |
152 |
122 |
std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); |
153 |
122 |
std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); |
154 |
122 |
std::set<Node> newSet; |
155 |
61 |
std::set_difference(left.begin(), |
156 |
|
left.end(), |
157 |
|
right.begin(), |
158 |
|
right.end(), |
159 |
61 |
std::inserter(newSet, newSet.begin())); |
160 |
122 |
Node newNode = NormalForm::elementsToSet(newSet, node.getType()); |
161 |
61 |
Assert(newNode.isConst()); |
162 |
122 |
Trace("sets-postrewrite") |
163 |
61 |
<< "Sets::postRewrite returning " << newNode << std::endl; |
164 |
61 |
return RewriteResponse(REWRITE_DONE, newNode); |
165 |
|
} |
166 |
1551 |
break; |
167 |
|
} // kind::SETMINUS |
168 |
|
|
169 |
2633 |
case kind::INTERSECTION: { |
170 |
2633 |
if(node[0] == node[1]) { |
171 |
29 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; |
172 |
29 |
return RewriteResponse(REWRITE_AGAIN, node[0]); |
173 |
2604 |
} else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) { |
174 |
42 |
return RewriteResponse(REWRITE_AGAIN, node[0]); |
175 |
2562 |
} else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) { |
176 |
52 |
return RewriteResponse(REWRITE_AGAIN, node[1]); |
177 |
2510 |
} else if(node[0].isConst() && node[1].isConst()) { |
178 |
76 |
std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); |
179 |
76 |
std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); |
180 |
76 |
std::set<Node> newSet; |
181 |
38 |
std::set_intersection(left.begin(), left.end(), right.begin(), right.end(), |
182 |
38 |
std::inserter(newSet, newSet.begin())); |
183 |
76 |
Node newNode = NormalForm::elementsToSet(newSet, node.getType()); |
184 |
38 |
Assert(newNode.isConst() && newNode.getType() == node.getType()); |
185 |
38 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl; |
186 |
38 |
return RewriteResponse(REWRITE_DONE, newNode); |
187 |
|
} |
188 |
2472 |
else if (node[0] > node[1]) |
189 |
|
{ |
190 |
754 |
Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); |
191 |
377 |
return RewriteResponse(REWRITE_DONE, newNode); |
192 |
|
} |
193 |
|
// we don't merge non-constant intersections |
194 |
2095 |
break; |
195 |
|
}//kind::INTERSECION |
196 |
|
|
197 |
5814 |
case kind::UNION: { |
198 |
|
// NOTE: case where it is CONST is taken care of at the top |
199 |
5814 |
if(node[0] == node[1]) { |
200 |
45 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; |
201 |
45 |
return RewriteResponse(REWRITE_AGAIN, node[0]); |
202 |
5769 |
} else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) { |
203 |
101 |
return RewriteResponse(REWRITE_AGAIN, node[1]); |
204 |
5668 |
} else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) { |
205 |
39 |
return RewriteResponse(REWRITE_AGAIN, node[0]); |
206 |
5629 |
} else if(node[0].isConst() && node[1].isConst()) { |
207 |
880 |
std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); |
208 |
880 |
std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); |
209 |
880 |
std::set<Node> newSet; |
210 |
440 |
std::set_union(left.begin(), left.end(), right.begin(), right.end(), |
211 |
440 |
std::inserter(newSet, newSet.begin())); |
212 |
880 |
Node newNode = NormalForm::elementsToSet(newSet, node.getType()); |
213 |
440 |
Assert(newNode.isConst()); |
214 |
880 |
Trace("sets-rewrite") |
215 |
440 |
<< "Sets::rewrite: UNION_CONSTANT_MERGE: " << newNode << std::endl; |
216 |
440 |
return RewriteResponse(REWRITE_DONE, newNode); |
217 |
|
} |
218 |
5189 |
else if (node[0] > node[1]) |
219 |
|
{ |
220 |
1394 |
Node newNode = nm->mkNode(node.getKind(), node[1], node[0]); |
221 |
697 |
return RewriteResponse(REWRITE_DONE, newNode); |
222 |
|
} |
223 |
|
// we don't merge non-constant unions |
224 |
4492 |
break; |
225 |
|
}//kind::UNION |
226 |
23 |
case kind::COMPLEMENT: |
227 |
|
{ |
228 |
46 |
Node univ = NodeManager::currentNM()->mkNullaryOperator(node[0].getType(), |
229 |
69 |
kind::UNIVERSE_SET); |
230 |
|
return RewriteResponse( |
231 |
|
REWRITE_AGAIN, |
232 |
23 |
NodeManager::currentNM()->mkNode(kind::SETMINUS, univ, node[0])); |
233 |
|
} |
234 |
4876 |
case kind::CARD: { |
235 |
4876 |
if(node[0].isConst()) { |
236 |
336 |
std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]); |
237 |
168 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(elements.size()))); |
238 |
4708 |
}else if( node[0].getKind()==kind::SINGLETON ){ |
239 |
17 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(1))); |
240 |
4691 |
}else if( node[0].getKind()==kind::UNION ){ |
241 |
|
Node ret = NodeManager::currentNM()->mkNode( kind::MINUS, |
242 |
462 |
NodeManager::currentNM()->mkNode( kind::PLUS, NodeManager::currentNM()->mkNode( kind::CARD, node[0][0] ), |
243 |
308 |
NodeManager::currentNM()->mkNode( kind::CARD, node[0][1] ) ), |
244 |
616 |
NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) ); |
245 |
154 |
return RewriteResponse(REWRITE_DONE, ret ); |
246 |
4537 |
}else if( node[0].getKind()==kind::SETMINUS ){ |
247 |
|
Node ret = NodeManager::currentNM()->mkNode( kind::MINUS, |
248 |
1238 |
NodeManager::currentNM()->mkNode( kind::CARD, node[0][0] ), |
249 |
2476 |
NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) ); |
250 |
619 |
return RewriteResponse(REWRITE_DONE, ret ); |
251 |
|
} |
252 |
3918 |
break; |
253 |
|
} |
254 |
|
|
255 |
25 |
case kind::CHOOSE: |
256 |
|
{ |
257 |
25 |
if (node[0].getKind() == SINGLETON) |
258 |
|
{ |
259 |
|
//(= (choose (singleton x)) x) is a tautology |
260 |
|
// we return x for (choose (singleton x)) |
261 |
5 |
return RewriteResponse(REWRITE_AGAIN, node[0][0]); |
262 |
|
} |
263 |
20 |
break; |
264 |
|
} // kind::CHOOSE |
265 |
57 |
case kind::IS_SINGLETON: |
266 |
|
{ |
267 |
57 |
if (node[0].getKind() == SINGLETON) |
268 |
|
{ |
269 |
|
//(= (is_singleton (singleton x)) is a tautology |
270 |
|
// we return true for (is_singleton (singleton x)) |
271 |
|
return RewriteResponse(REWRITE_AGAIN, |
272 |
5 |
NodeManager::currentNM()->mkConst(true)); |
273 |
|
} |
274 |
52 |
break; |
275 |
|
} // kind::IS_SINGLETON |
276 |
|
|
277 |
237 |
case kind::TRANSPOSE: { |
278 |
237 |
if(node[0].getKind() == kind::TRANSPOSE) { |
279 |
|
return RewriteResponse(REWRITE_AGAIN, node[0][0]); |
280 |
|
} |
281 |
|
|
282 |
237 |
if(node[0].getKind() == kind::EMPTYSET) { |
283 |
|
return RewriteResponse(REWRITE_DONE, |
284 |
|
nm->mkConst(EmptySet(node.getType()))); |
285 |
237 |
} else if(node[0].isConst()) { |
286 |
18 |
std::set<Node> new_tuple_set; |
287 |
18 |
std::set<Node> tuple_set = NormalForm::getElementsFromNormalConstant(node[0]); |
288 |
9 |
std::set<Node>::iterator tuple_it = tuple_set.begin(); |
289 |
|
|
290 |
45 |
while(tuple_it != tuple_set.end()) { |
291 |
18 |
new_tuple_set.insert(RelsUtils::reverseTuple(*tuple_it)); |
292 |
18 |
++tuple_it; |
293 |
|
} |
294 |
18 |
Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); |
295 |
9 |
Assert(new_node.isConst()); |
296 |
9 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; |
297 |
9 |
return RewriteResponse(REWRITE_DONE, new_node); |
298 |
|
|
299 |
|
} |
300 |
228 |
if(node[0].getKind() != kind::TRANSPOSE) { |
301 |
228 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl; |
302 |
228 |
return RewriteResponse(REWRITE_DONE, node); |
303 |
|
} |
304 |
|
break; |
305 |
|
} |
306 |
|
|
307 |
86 |
case kind::PRODUCT: { |
308 |
86 |
Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " << node << std::endl; |
309 |
344 |
if( node[0].getKind() == kind::EMPTYSET || |
310 |
258 |
node[1].getKind() == kind::EMPTYSET) { |
311 |
|
return RewriteResponse(REWRITE_DONE, |
312 |
|
nm->mkConst(EmptySet(node.getType()))); |
313 |
86 |
} else if( node[0].isConst() && node[1].isConst() ) { |
314 |
10 |
Trace("sets-rels-postrewrite") << "Sets::postRewrite processing **** " << node << std::endl; |
315 |
20 |
std::set<Node> new_tuple_set; |
316 |
20 |
std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); |
317 |
20 |
std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); |
318 |
10 |
std::set<Node>::iterator left_it = left.begin(); |
319 |
10 |
int left_len = (*left_it).getType().getTupleLength(); |
320 |
20 |
TypeNode tn = node.getType().getSetElementType(); |
321 |
54 |
while(left_it != left.end()) { |
322 |
22 |
Trace("rels-debug") << "Sets::postRewrite processing left_it = " << *left_it << std::endl; |
323 |
44 |
std::vector<Node> left_tuple; |
324 |
22 |
left_tuple.push_back(tn.getDType()[0].getConstructor()); |
325 |
61 |
for(int i = 0; i < left_len; i++) { |
326 |
39 |
left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); |
327 |
|
} |
328 |
22 |
std::set<Node>::iterator right_it = right.begin(); |
329 |
22 |
int right_len = (*right_it).getType().getTupleLength(); |
330 |
150 |
while(right_it != right.end()) { |
331 |
64 |
Trace("rels-debug") << "Sets::postRewrite processing right_it = " << *right_it << std::endl; |
332 |
128 |
std::vector<Node> right_tuple; |
333 |
177 |
for(int j = 0; j < right_len; j++) { |
334 |
113 |
right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); |
335 |
|
} |
336 |
128 |
std::vector<Node> new_tuple; |
337 |
64 |
new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end()); |
338 |
64 |
new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); |
339 |
128 |
Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); |
340 |
64 |
new_tuple_set.insert(composed_tuple); |
341 |
64 |
++right_it; |
342 |
|
} |
343 |
22 |
++left_it; |
344 |
|
} |
345 |
20 |
Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); |
346 |
10 |
Assert(new_node.isConst()); |
347 |
10 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; |
348 |
10 |
return RewriteResponse(REWRITE_DONE, new_node); |
349 |
|
} |
350 |
76 |
break; |
351 |
|
} |
352 |
|
|
353 |
660 |
case kind::JOIN: { |
354 |
2638 |
if( node[0].getKind() == kind::EMPTYSET || |
355 |
1978 |
node[1].getKind() == kind::EMPTYSET) { |
356 |
|
return RewriteResponse(REWRITE_DONE, |
357 |
3 |
nm->mkConst(EmptySet(node.getType()))); |
358 |
657 |
} else if( node[0].isConst() && node[1].isConst() ) { |
359 |
29 |
Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " << node << std::endl; |
360 |
58 |
std::set<Node> new_tuple_set; |
361 |
58 |
std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); |
362 |
58 |
std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); |
363 |
29 |
std::set<Node>::iterator left_it = left.begin(); |
364 |
29 |
int left_len = (*left_it).getType().getTupleLength(); |
365 |
58 |
TypeNode tn = node.getType().getSetElementType(); |
366 |
139 |
while(left_it != left.end()) { |
367 |
110 |
std::vector<Node> left_tuple; |
368 |
55 |
left_tuple.push_back(tn.getDType()[0].getConstructor()); |
369 |
107 |
for(int i = 0; i < left_len - 1; i++) { |
370 |
52 |
left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i)); |
371 |
|
} |
372 |
55 |
std::set<Node>::iterator right_it = right.begin(); |
373 |
55 |
int right_len = (*right_it).getType().getTupleLength(); |
374 |
327 |
while(right_it != right.end()) { |
375 |
136 |
if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) { |
376 |
80 |
std::vector<Node> right_tuple; |
377 |
82 |
for(int j = 1; j < right_len; j++) { |
378 |
42 |
right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j)); |
379 |
|
} |
380 |
80 |
std::vector<Node> new_tuple; |
381 |
40 |
new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end()); |
382 |
40 |
new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); |
383 |
80 |
Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); |
384 |
40 |
new_tuple_set.insert(composed_tuple); |
385 |
|
} |
386 |
136 |
++right_it; |
387 |
|
} |
388 |
55 |
++left_it; |
389 |
|
} |
390 |
58 |
Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); |
391 |
29 |
Assert(new_node.isConst()); |
392 |
29 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; |
393 |
29 |
return RewriteResponse(REWRITE_DONE, new_node); |
394 |
|
} |
395 |
|
|
396 |
628 |
break; |
397 |
|
} |
398 |
|
|
399 |
83 |
case kind::TCLOSURE: { |
400 |
83 |
if(node[0].getKind() == kind::EMPTYSET) { |
401 |
|
return RewriteResponse(REWRITE_DONE, |
402 |
4 |
nm->mkConst(EmptySet(node.getType()))); |
403 |
79 |
} else if (node[0].isConst()) { |
404 |
14 |
std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); |
405 |
14 |
std::set<Node> tc_rel_mems = RelsUtils::computeTC(rel_mems, node); |
406 |
14 |
Node new_node = NormalForm::elementsToSet(tc_rel_mems, node.getType()); |
407 |
7 |
Assert(new_node.isConst()); |
408 |
7 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl; |
409 |
7 |
return RewriteResponse(REWRITE_DONE, new_node); |
410 |
|
|
411 |
72 |
} else if(node[0].getKind() == kind::TCLOSURE) { |
412 |
|
return RewriteResponse(REWRITE_AGAIN, node[0]); |
413 |
72 |
} else if(node[0].getKind() != kind::TCLOSURE) { |
414 |
72 |
Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl; |
415 |
72 |
return RewriteResponse(REWRITE_DONE, node); |
416 |
|
} |
417 |
|
break; |
418 |
|
} |
419 |
|
|
420 |
17 |
case kind::IDEN: { |
421 |
17 |
if(node[0].getKind() == kind::EMPTYSET) { |
422 |
|
return RewriteResponse(REWRITE_DONE, |
423 |
|
nm->mkConst(EmptySet(node.getType()))); |
424 |
17 |
} else if (node[0].isConst()) { |
425 |
2 |
std::set<Node> iden_rel_mems; |
426 |
2 |
std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); |
427 |
1 |
std::set<Node>::iterator rel_mems_it = rel_mems.begin(); |
428 |
|
|
429 |
9 |
while( rel_mems_it != rel_mems.end() ) { |
430 |
8 |
Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0); |
431 |
4 |
iden_rel_mems.insert(RelsUtils::constructPair(node, fst_mem, fst_mem)); |
432 |
4 |
++rel_mems_it; |
433 |
|
} |
434 |
|
|
435 |
2 |
Node new_node = NormalForm::elementsToSet(iden_rel_mems, node.getType()); |
436 |
1 |
Assert(new_node.isConst()); |
437 |
1 |
Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl; |
438 |
1 |
return RewriteResponse(REWRITE_DONE, new_node); |
439 |
|
|
440 |
|
} else { |
441 |
16 |
Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl; |
442 |
|
} |
443 |
16 |
break; |
444 |
|
} |
445 |
|
|
446 |
73 |
case kind::JOIN_IMAGE: { |
447 |
73 |
unsigned int min_card = node[1].getConst<Rational>().getNumerator().getUnsignedInt(); |
448 |
73 |
Trace("rels-postrewrite") << "Rels::postRewrite " << node << " with min_card = " << min_card << std::endl; |
449 |
|
|
450 |
73 |
if( min_card == 0) { |
451 |
2 |
return RewriteResponse(REWRITE_DONE, nm->mkNullaryOperator( node.getType(), kind::UNIVERSE_SET )); |
452 |
71 |
} else if(node[0].getKind() == kind::EMPTYSET) { |
453 |
|
return RewriteResponse(REWRITE_DONE, |
454 |
|
nm->mkConst(EmptySet(node.getType()))); |
455 |
71 |
} else if (node[0].isConst()) { |
456 |
14 |
std::set<Node> has_checked; |
457 |
14 |
std::set<Node> join_img_mems; |
458 |
14 |
std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]); |
459 |
7 |
std::set<Node>::iterator rel_mems_it = rel_mems.begin(); |
460 |
|
|
461 |
85 |
while( rel_mems_it != rel_mems.end() ) { |
462 |
63 |
Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0); |
463 |
54 |
if( has_checked.find( fst_mem ) != has_checked.end() ) { |
464 |
15 |
++rel_mems_it; |
465 |
15 |
continue; |
466 |
|
} |
467 |
24 |
has_checked.insert( fst_mem ); |
468 |
48 |
std::set<Node> existing_mems; |
469 |
24 |
std::set<Node>::iterator rel_mems_it_snd = rel_mems.begin(); |
470 |
308 |
while( rel_mems_it_snd != rel_mems.end() ) { |
471 |
284 |
Node fst_mem_snd = RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 0); |
472 |
142 |
if( fst_mem == fst_mem_snd ) { |
473 |
39 |
existing_mems.insert( RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 1) ); |
474 |
|
} |
475 |
142 |
++rel_mems_it_snd; |
476 |
|
} |
477 |
24 |
if( existing_mems.size() >= min_card ) { |
478 |
19 |
const DType& dt = node.getType().getSetElementType().getDType(); |
479 |
19 |
join_img_mems.insert( |
480 |
38 |
nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem)); |
481 |
|
} |
482 |
24 |
++rel_mems_it; |
483 |
|
} |
484 |
14 |
Node new_node = NormalForm::elementsToSet(join_img_mems, node.getType()); |
485 |
7 |
Assert(new_node.isConst()); |
486 |
7 |
Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl; |
487 |
7 |
return RewriteResponse(REWRITE_DONE, new_node); |
488 |
|
} else { |
489 |
64 |
Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl; |
490 |
|
} |
491 |
64 |
break; |
492 |
|
} |
493 |
|
|
494 |
5295 |
default: |
495 |
5295 |
break; |
496 |
|
} |
497 |
|
|
498 |
73078 |
return RewriteResponse(REWRITE_DONE, node); |
499 |
|
} |
500 |
|
|
501 |
|
|
502 |
|
// static |
503 |
55670 |
RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { |
504 |
55670 |
NodeManager* nm = NodeManager::currentNM(); |
505 |
55670 |
Kind k = node.getKind(); |
506 |
55670 |
if (k == kind::EQUAL) |
507 |
|
{ |
508 |
16704 |
if(node[0] == node[1]) { |
509 |
1349 |
return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); |
510 |
|
} |
511 |
|
} |
512 |
38966 |
else if (k == kind::INSERT) |
513 |
|
{ |
514 |
32 |
size_t setNodeIndex = node.getNumChildren()-1; |
515 |
64 |
TypeNode elementType = node[setNodeIndex].getType().getSetElementType(); |
516 |
64 |
Node insertedElements = nm->mkSingleton(elementType, node[0]); |
517 |
|
|
518 |
83 |
for (size_t i = 1; i < setNodeIndex; ++i) |
519 |
|
{ |
520 |
102 |
Node singleton = nm->mkSingleton(elementType, node[i]); |
521 |
51 |
insertedElements = nm->mkNode(kind::UNION, insertedElements, singleton); |
522 |
|
} |
523 |
|
return RewriteResponse(REWRITE_AGAIN, |
524 |
64 |
nm->mkNode(kind::UNION, |
525 |
|
insertedElements, |
526 |
32 |
node[setNodeIndex])); |
527 |
|
} |
528 |
38934 |
else if (k == kind::SUBSET) |
529 |
|
{ |
530 |
|
// rewrite (A subset-or-equal B) as (A union B = B) |
531 |
|
return RewriteResponse(REWRITE_AGAIN, |
532 |
1396 |
nm->mkNode(kind::EQUAL, |
533 |
698 |
nm->mkNode(kind::UNION, node[0], node[1]), |
534 |
349 |
node[1]) ); |
535 |
|
} |
536 |
|
|
537 |
|
// could have an efficient normalizer for union here |
538 |
|
|
539 |
53940 |
return RewriteResponse(REWRITE_DONE, node); |
540 |
|
} |
541 |
|
|
542 |
|
} // namespace sets |
543 |
|
} // namespace theory |
544 |
28194 |
} // namespace cvc5 |