GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_rewriter.cpp Lines: 326 344 94.8 %
Date: 2021-03-22 Branches: 915 1885 48.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Kshitij Bansal, Paul Meng
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Sets theory rewriter.
13
 **
14
 ** Sets theory rewriter.
15
 **/
16
17
#include "theory/sets/theory_sets_rewriter.h"
18
19
#include "expr/attribute.h"
20
#include "expr/dtype_cons.h"
21
#include "options/sets_options.h"
22
#include "theory/sets/normal_form.h"
23
#include "theory/sets/rels_utils.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace sets {
30
31
2152
bool TheorySetsRewriter::checkConstantMembership(TNode elementTerm, TNode setTerm)
32
{
33
2152
  if(setTerm.getKind() == kind::EMPTYSET) {
34
71
    return false;
35
  }
36
37
2081
  if(setTerm.getKind() == kind::SINGLETON) {
38
887
    return elementTerm == setTerm[0];
39
  }
40
41
1194
  Assert(setTerm.getKind() == kind::UNION
42
         && setTerm[0].getKind() == kind::SINGLETON)
43
      << "kind was " << setTerm.getKind() << ", term: " << setTerm;
44
45
3582
  return elementTerm == setTerm[0][0]
46
3582
         || checkConstantMembership(elementTerm, setTerm[1]);
47
}
48
49
// static
50
99309
RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
51
99309
  NodeManager* nm = NodeManager::currentNM();
52
99309
  Kind kind = node.getKind();
53
99309
  Trace("sets-postrewrite") << "Process: " << node << std::endl;
54
55
99309
  if(node.isConst()) {
56
12510
    Trace("sets-rewrite-nf")
57
6255
        << "Sets::rewrite: no rewrite (constant) " << node << std::endl;
58
    // Dare you touch the const and mangle it to something else.
59
6255
    return RewriteResponse(REWRITE_DONE, node);
60
  }
61
62
93054
  switch(kind) {
63
64
38621
  case kind::MEMBER: {
65
38621
    if(node[0].isConst() && node[1].isConst()) {
66
      // both are constants
67
2440
      TNode S = preRewrite(node[1]).d_node;
68
1220
      bool isMember = checkConstantMembership(node[0], S);
69
1220
      return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
70
37401
    }else if( node[1].getKind()==kind::EMPTYSET ){
71
285
      return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
72
37116
    }else if( node[1].getKind()==kind::SINGLETON ){
73
2195
      return RewriteResponse(REWRITE_AGAIN_FULL, nm->mkNode(kind::EQUAL, node[0], node[1][0] ) );
74
34921
    }else if( node[1].getKind()==kind::UNION || node[1].getKind()==kind::INTERSECTION || node[1].getKind()==kind::SETMINUS ){
75
7882
      std::vector< Node > children;
76
11823
      for( unsigned i=0; i<node[1].getNumChildren(); i++ ){
77
15764
        Node nc = nm->mkNode(kind::MEMBER, node[0], node[1][i] );
78
7882
        if( node[1].getKind()==kind::SETMINUS && i==1 ){
79
855
          nc = nc.negate();
80
        }
81
7882
        children.push_back( nc );
82
      }
83
3941
      return RewriteResponse(REWRITE_AGAIN_FULL, nm->mkNode( node[1].getKind()==kind::UNION ? kind::OR : kind::AND, children ) );
84
    }
85
30980
    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
32263
  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
32263
    if(node[0] == node[1]) {
108
100
      Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
109
100
      return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
110
    }
111
32163
    else if (node[0].isConst() && node[1].isConst()) {
112
155
      Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
113
155
      return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
114
    }
115
32008
    else if (node[0] > node[1]) {
116
13034
      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
117
6517
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
118
6517
      return RewriteResponse(REWRITE_DONE, newNode);
119
    }
120
25491
    break;
121
  }
122
123
1637
  case kind::SETMINUS:
124
  {
125
1637
    if (node[0] == node[1])
126
    {
127
58
      Node newNode = nm->mkConst(EmptySet(node[0].getType()));
128
58
      Trace("sets-postrewrite")
129
29
          << "Sets::postRewrite returning " << newNode << std::endl;
130
29
      return RewriteResponse(REWRITE_DONE, newNode);
131
    }
132
4824
    else if (node[0].getKind() == kind::EMPTYSET
133
4824
             || node[1].getKind() == kind::EMPTYSET)
134
    {
135
18
      Trace("sets-postrewrite")
136
9
          << "Sets::postRewrite returning " << node[0] << std::endl;
137
9
      return RewriteResponse(REWRITE_AGAIN, node[0]);
138
    }
139
1599
    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
1587
    else if (node[1].getKind() == kind::UNIVERSE_SET)
146
    {
147
      return RewriteResponse(
148
          REWRITE_AGAIN,
149
          NodeManager::currentNM()->mkConst(EmptySet(node[1].getType())));
150
    }
151
1587
    else if (node[0].isConst() && node[1].isConst())
152
    {
153
120
      std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
154
120
      std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
155
120
      std::set<Node> newSet;
156
60
      std::set_difference(left.begin(),
157
                          left.end(),
158
                          right.begin(),
159
                          right.end(),
160
60
                          std::inserter(newSet, newSet.begin()));
161
120
      Node newNode = NormalForm::elementsToSet(newSet, node.getType());
162
60
      Assert(newNode.isConst());
163
120
      Trace("sets-postrewrite")
164
60
          << "Sets::postRewrite returning " << newNode << std::endl;
165
60
      return RewriteResponse(REWRITE_DONE, newNode);
166
    }
167
1527
    break;
168
  }  // kind::SETMINUS
169
170
2626
  case kind::INTERSECTION: {
171
2626
    if(node[0] == node[1]) {
172
31
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
173
31
      return RewriteResponse(REWRITE_AGAIN, node[0]);
174
2595
    } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) {
175
20
      return RewriteResponse(REWRITE_AGAIN, node[0]);
176
2575
    } else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) {
177
31
      return RewriteResponse(REWRITE_AGAIN, node[1]);
178
2544
    } else if(node[0].isConst() && node[1].isConst()) {
179
88
      std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
180
88
      std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
181
88
      std::set<Node> newSet;
182
44
      std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
183
44
                            std::inserter(newSet, newSet.begin()));
184
88
      Node newNode = NormalForm::elementsToSet(newSet, node.getType());
185
44
      Assert(newNode.isConst() && newNode.getType() == node.getType());
186
44
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
187
44
      return RewriteResponse(REWRITE_DONE, newNode);
188
    }
189
2500
    else if (node[0] > node[1])
190
    {
191
770
      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
192
385
      return RewriteResponse(REWRITE_DONE, newNode);
193
    }
194
    // we don't merge non-constant intersections
195
2115
    break;
196
  }//kind::INTERSECION
197
198
5942
  case kind::UNION: {
199
    // NOTE: case where it is CONST is taken care of at the top
200
5942
    if(node[0] == node[1]) {
201
51
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
202
51
      return RewriteResponse(REWRITE_AGAIN, node[0]);
203
5891
    } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) {
204
84
      return RewriteResponse(REWRITE_AGAIN, node[1]);
205
5807
    } else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) {
206
47
      return RewriteResponse(REWRITE_AGAIN, node[0]);
207
5760
    } else if(node[0].isConst() && node[1].isConst()) {
208
858
      std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
209
858
      std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
210
858
      std::set<Node> newSet;
211
429
      std::set_union(left.begin(), left.end(), right.begin(), right.end(),
212
429
                          std::inserter(newSet, newSet.begin()));
213
858
      Node newNode = NormalForm::elementsToSet(newSet, node.getType());
214
429
      Assert(newNode.isConst());
215
858
      Trace("sets-rewrite")
216
429
          << "Sets::rewrite: UNION_CONSTANT_MERGE: " << newNode << std::endl;
217
429
      return RewriteResponse(REWRITE_DONE, newNode);
218
    }
219
5331
    else if (node[0] > node[1])
220
    {
221
1462
      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
222
731
      return RewriteResponse(REWRITE_DONE, newNode);
223
    }
224
    // we don't merge non-constant unions
225
4600
    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
4966
  case kind::CARD: {
236
4966
    if(node[0].isConst()) {
237
318
      std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]);
238
159
      return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(elements.size())));
239
4807
    }else if( node[0].getKind()==kind::SINGLETON ){
240
11
      return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(1)));
241
4796
    }else if( node[0].getKind()==kind::UNION ){
242
      Node ret = NodeManager::currentNM()->mkNode( kind::MINUS,
243
501
                   NodeManager::currentNM()->mkNode( kind::PLUS, NodeManager::currentNM()->mkNode( kind::CARD, node[0][0] ),
244
334
                                                                 NodeManager::currentNM()->mkNode( kind::CARD, node[0][1] ) ),
245
668
                   NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) );
246
167
      return RewriteResponse(REWRITE_DONE, ret );
247
4629
    }else if( node[0].getKind()==kind::SETMINUS ){
248
      Node ret = NodeManager::currentNM()->mkNode( kind::MINUS,
249
1206
                   NodeManager::currentNM()->mkNode( kind::CARD, node[0][0] ),
250
2412
                   NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) );
251
603
      return RewriteResponse(REWRITE_DONE, ret );
252
    }
253
4026
    break;
254
  }
255
256
22
  case kind::CHOOSE:
257
  {
258
22
    if (node[0].getKind() == SINGLETON)
259
    {
260
      //(= (choose (singleton x)) x) is a tautology
261
      // we return x for (choose (singleton x))
262
4
      return RewriteResponse(REWRITE_AGAIN, node[0][0]);
263
    }
264
18
    break;
265
  }  // kind::CHOOSE
266
36
  case kind::IS_SINGLETON:
267
  {
268
36
    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
4
                             NodeManager::currentNM()->mkConst(true));
274
    }
275
32
    break;
276
  } // kind::IS_SINGLETON
277
278
235
  case kind::TRANSPOSE: {
279
235
    if(node[0].getKind() == kind::TRANSPOSE) {
280
      return RewriteResponse(REWRITE_AGAIN, node[0][0]);
281
    }
282
283
235
    if(node[0].getKind() == kind::EMPTYSET) {
284
      return RewriteResponse(REWRITE_DONE,
285
                             nm->mkConst(EmptySet(node.getType())));
286
235
    } 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
226
    if(node[0].getKind() != kind::TRANSPOSE) {
302
226
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl;
303
226
      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
344
    if( node[0].getKind() == kind::EMPTYSET ||
311
258
        node[1].getKind() == kind::EMPTYSET) {
312
      return RewriteResponse(REWRITE_DONE,
313
                             nm->mkConst(EmptySet(node.getType())));
314
86
    } else if( node[0].isConst() && node[1].isConst() ) {
315
10
      Trace("sets-rels-postrewrite") << "Sets::postRewrite processing **** " <<  node << std::endl;
316
20
      std::set<Node> new_tuple_set;
317
20
      std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
318
20
      std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
319
10
      std::set<Node>::iterator left_it = left.begin();
320
10
      int left_len = (*left_it).getType().getTupleLength();
321
20
      TypeNode tn = node.getType().getSetElementType();
322
54
      while(left_it != left.end()) {
323
22
        Trace("rels-debug") << "Sets::postRewrite processing left_it = " <<  *left_it << std::endl;
324
44
        std::vector<Node> left_tuple;
325
22
        left_tuple.push_back(tn.getDType()[0].getConstructor());
326
61
        for(int i = 0; i < left_len; i++) {
327
39
          left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
328
        }
329
22
        std::set<Node>::iterator right_it = right.begin();
330
22
        int right_len = (*right_it).getType().getTupleLength();
331
150
        while(right_it != right.end()) {
332
64
          Trace("rels-debug") << "Sets::postRewrite processing right_it = " <<  *right_it << std::endl;
333
128
          std::vector<Node> right_tuple;
334
177
          for(int j = 0; j < right_len; j++) {
335
113
            right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
336
          }
337
128
          std::vector<Node> new_tuple;
338
64
          new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
339
64
          new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end());
340
128
          Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple);
341
64
          new_tuple_set.insert(composed_tuple);
342
64
          ++right_it;
343
        }
344
22
        ++left_it;
345
      }
346
20
      Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType());
347
10
      Assert(new_node.isConst());
348
10
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl;
349
10
      return RewriteResponse(REWRITE_DONE, new_node);
350
    }
351
76
    break;
352
  }
353
354
659
  case kind::JOIN: {
355
2634
    if( node[0].getKind() == kind::EMPTYSET ||
356
1975
        node[1].getKind() == kind::EMPTYSET) {
357
      return RewriteResponse(REWRITE_DONE,
358
3
                             nm->mkConst(EmptySet(node.getType())));
359
656
    } else if( node[0].isConst() && node[1].isConst() ) {
360
30
      Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " <<  node << std::endl;
361
60
      std::set<Node> new_tuple_set;
362
60
      std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
363
60
      std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
364
30
      std::set<Node>::iterator left_it = left.begin();
365
30
      int left_len = (*left_it).getType().getTupleLength();
366
60
      TypeNode tn = node.getType().getSetElementType();
367
148
      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
363
        while(right_it != right.end()) {
376
152
          if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) {
377
88
            std::vector<Node> right_tuple;
378
90
            for(int j = 1; j < right_len; j++) {
379
46
              right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
380
            }
381
88
            std::vector<Node> new_tuple;
382
44
            new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
383
44
            new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end());
384
88
            Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple);
385
44
            new_tuple_set.insert(composed_tuple);
386
          }
387
152
          ++right_it;
388
        }
389
59
        ++left_it;
390
      }
391
60
      Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType());
392
30
      Assert(new_node.isConst());
393
30
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl;
394
30
      return RewriteResponse(REWRITE_DONE, new_node);
395
    }
396
397
626
    break;
398
  }
399
400
82
  case kind::TCLOSURE: {
401
82
    if(node[0].getKind() == kind::EMPTYSET) {
402
      return RewriteResponse(REWRITE_DONE,
403
4
                             nm->mkConst(EmptySet(node.getType())));
404
78
    } 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
70
    } else if(node[0].getKind() == kind::TCLOSURE) {
413
      return RewriteResponse(REWRITE_AGAIN, node[0]);
414
70
    } else if(node[0].getKind() != kind::TCLOSURE) {
415
70
      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl;
416
70
      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
5766
  default:
496
5766
    break;
497
  }
498
499
75337
  return RewriteResponse(REWRITE_DONE, node);
500
}
501
502
503
// static
504
56587
RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
505
56587
  NodeManager* nm = NodeManager::currentNM();
506
56587
  Kind k = node.getKind();
507
56587
  if (k == kind::EQUAL)
508
  {
509
17010
    if(node[0] == node[1]) {
510
695
      return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
511
    }
512
  }
513
39577
  else if (k == kind::INSERT)
514
  {
515
32
    size_t setNodeIndex =  node.getNumChildren()-1;
516
64
    TypeNode elementType = node[setNodeIndex].getType().getSetElementType();
517
64
    Node insertedElements = nm->mkSingleton(elementType, node[0]);
518
519
79
    for (size_t i = 1; i < setNodeIndex; ++i)
520
    {
521
94
      Node singleton = nm->mkSingleton(elementType, node[i]);
522
47
      insertedElements = nm->mkNode(kind::UNION, insertedElements, singleton);
523
    }
524
    return RewriteResponse(REWRITE_AGAIN,
525
64
                           nm->mkNode(kind::UNION,
526
                                      insertedElements,
527
32
                                      node[setNodeIndex]));
528
  }
529
39545
  else if (k == kind::SUBSET)
530
  {
531
    // rewrite (A subset-or-equal B) as (A union B = B)
532
    return RewriteResponse(REWRITE_AGAIN,
533
1420
                           nm->mkNode(kind::EQUAL,
534
710
                                      nm->mkNode(kind::UNION, node[0], node[1]),
535
355
                                      node[1]) );
536
  }
537
538
  // could have an efficient normalizer for union here
539
540
55505
  return RewriteResponse(REWRITE_DONE, node);
541
}
542
543
}/* CVC4::theory::sets namespace */
544
}/* CVC4::theory namespace */
545
26676
}/* CVC4 namespace */