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