GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_private.cpp Lines: 654 694 94.2 %
Date: 2021-03-23 Branches: 1432 3048 47.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_private.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed, Kshitij Bansal
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 implementation.
13
 **
14
 ** Sets theory implementation.
15
 **/
16
17
#include "theory/sets/theory_sets_private.h"
18
19
#include <algorithm>
20
21
#include "expr/emptyset.h"
22
#include "expr/node_algorithm.h"
23
#include "expr/skolem_manager.h"
24
#include "options/sets_options.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/sets/normal_form.h"
27
#include "theory/sets/theory_sets.h"
28
#include "theory/theory_model.h"
29
#include "util/result.h"
30
31
using namespace std;
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace sets {
37
38
8997
TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
39
                                     SolverState& state,
40
                                     InferenceManager& im,
41
8997
                                     SkolemCache& skc)
42
    : d_deq(state.getSatContext()),
43
8997
      d_termProcessed(state.getUserContext()),
44
      d_full_check_incomplete(false),
45
      d_external(external),
46
      d_state(state),
47
      d_im(im),
48
      d_skCache(skc),
49
      d_treg(state, im, skc),
50
8997
      d_rels(new TheorySetsRels(state, im, skc, d_treg)),
51
8997
      d_cardSolver(new CardinalityExtension(state, im, d_treg)),
52
      d_rels_enabled(false),
53
35988
      d_card_enabled(false)
54
{
55
8997
  d_true = NodeManager::currentNM()->mkConst(true);
56
8997
  d_false = NodeManager::currentNM()->mkConst(false);
57
8997
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
58
8997
}
59
60
17988
TheorySetsPrivate::~TheorySetsPrivate()
61
{
62
13672
  for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info)
63
  {
64
4678
    delete current_pair.second;
65
  }
66
8994
}
67
68
8997
void TheorySetsPrivate::finishInit()
69
{
70
8997
  d_equalityEngine = d_external.getEqualityEngine();
71
8997
  Assert(d_equalityEngine != nullptr);
72
8997
}
73
74
49866
void TheorySetsPrivate::eqNotifyNewClass(TNode t)
75
{
76
49866
  if (t.getKind() == kind::SINGLETON || t.getKind() == kind::EMPTYSET)
77
  {
78
2866
    EqcInfo* e = getOrMakeEqcInfo(t, true);
79
2866
    e->d_singleton = t;
80
  }
81
49866
}
82
83
114752
void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
84
{
85
114752
  if (!d_state.isInConflict())
86
  {
87
229500
    Trace("sets-prop-debug")
88
114750
        << "Merge " << t1 << " and " << t2 << "..." << std::endl;
89
229339
    Node s1, s2;
90
114750
    EqcInfo* e2 = getOrMakeEqcInfo(t2);
91
114750
    if (e2)
92
    {
93
4573
      s2 = e2->d_singleton;
94
4573
      EqcInfo* e1 = getOrMakeEqcInfo(t1);
95
4573
      Trace("sets-prop-debug") << "Merging singletons..." << std::endl;
96
4573
      if (e1)
97
      {
98
4505
        s1 = e1->d_singleton;
99
4505
        if (!s1.isNull() && !s2.isNull())
100
        {
101
2126
          if (s1.getKind() == s2.getKind())
102
          {
103
4112
            Trace("sets-prop") << "Propagate eq inference : " << s1
104
2056
                               << " == " << s2 << std::endl;
105
            // infer equality between elements of singleton
106
4112
            Node exp = s1.eqNode(s2);
107
4112
            Node eq = s1[0].eqNode(s2[0]);
108
2056
            d_im.assertInternalFact(eq, true, InferenceId::SETS_SINGLETON_EQ, exp);
109
          }
110
          else
111
          {
112
            // singleton equal to emptyset, conflict
113
140
            Trace("sets-prop")
114
70
                << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
115
70
            d_im.conflictEqConstantMerge(s1, s2);
116
70
            return;
117
          }
118
        }
119
      }
120
      else
121
      {
122
        // copy information
123
68
        e1 = getOrMakeEqcInfo(t1, true);
124
68
        e1->d_singleton.set(e2->d_singleton);
125
      }
126
    }
127
    // merge membership list
128
114680
    Trace("sets-prop-debug") << "Copying membership list..." << std::endl;
129
    // if s1 has a singleton or empty set and s2 does not, we may have new
130
    // inferences to process.
131
229269
    Node checkSingleton = s2.isNull() ? s1 : Node::null();
132
229269
    std::vector<Node> facts;
133
    // merge the membership list in the state, which may produce facts or
134
    // conflicts to propagate
135
114680
    if (!d_state.merge(t1, t2, facts, checkSingleton))
136
    {
137
      // conflict case
138
91
      Assert(facts.size() == 1);
139
182
      Trace("sets-prop") << "Propagate eq-mem conflict : " << facts[0]
140
91
                         << std::endl;
141
91
      d_im.conflict(facts[0], InferenceId::SETS_EQ_MEM_CONFLICT);
142
91
      return;
143
    }
144
114713
    for (const Node& f : facts)
145
    {
146
124
      Assert(f.getKind() == kind::IMPLIES);
147
248
      Trace("sets-prop") << "Propagate eq-mem eq inference : " << f[0] << " => "
148
124
                         << f[1] << std::endl;
149
124
      d_im.assertInternalFact(f[1], true, InferenceId::SETS_EQ_MEM, f[0]);
150
    }
151
  }
152
}
153
154
26889
void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
155
{
156
26889
  if (t1.getType().isSet())
157
  {
158
33652
    Node eq = t1.eqNode(t2);
159
16826
    if (d_deq.find(eq) == d_deq.end())
160
    {
161
16826
      d_deq[eq] = true;
162
    }
163
  }
164
26889
}
165
166
4678
TheorySetsPrivate::EqcInfo::EqcInfo(context::Context* c) : d_singleton(c) {}
167
168
151558
TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo(TNode n,
169
                                                                bool doMake)
170
{
171
151558
  std::map<Node, EqcInfo*>::iterator eqc_i = d_eqc_info.find(n);
172
151558
  if (eqc_i == d_eqc_info.end())
173
  {
174
114923
    EqcInfo* ei = NULL;
175
114923
    if (doMake)
176
    {
177
4678
      ei = new EqcInfo(d_external.getSatContext());
178
4678
      d_eqc_info[n] = ei;
179
    }
180
114923
    return ei;
181
  }
182
  else
183
  {
184
36635
    return eqc_i->second;
185
  }
186
}
187
188
49462
bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
189
{
190
148386
  if (d_equalityEngine->isTriggerTerm(a, THEORY_SETS)
191
148386
      && d_equalityEngine->isTriggerTerm(b, THEORY_SETS))
192
  {
193
    TNode a_shared =
194
48135
        d_equalityEngine->getTriggerTermRepresentative(a, THEORY_SETS);
195
    TNode b_shared =
196
48135
        d_equalityEngine->getTriggerTermRepresentative(b, THEORY_SETS);
197
    EqualityStatus eqStatus =
198
30362
        d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
199
30362
    if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
200
30362
        || eqStatus == EQUALITY_FALSE_IN_MODEL)
201
    {
202
12589
      return true;
203
    }
204
  }
205
36873
  return false;
206
}
207
208
15965
void TheorySetsPrivate::fullEffortReset()
209
{
210
15965
  Assert(d_equalityEngine->consistent());
211
15965
  d_full_check_incomplete = false;
212
15965
  d_most_common_type.clear();
213
15965
  d_most_common_type_term.clear();
214
15965
  d_card_enabled = false;
215
15965
  d_rels_enabled = false;
216
  // reset the state object
217
15965
  d_state.reset();
218
  // reset the inference manager
219
15965
  d_im.reset();
220
15965
  d_im.clearPendingLemmas();
221
  // reset the cardinality solver
222
15965
  d_cardSolver->reset();
223
15965
}
224
225
15965
void TheorySetsPrivate::fullEffortCheck()
226
{
227
15965
  Trace("sets") << "----- Full effort check ------" << std::endl;
228
  do
229
  {
230
15965
    Assert(!d_im.hasPendingLemma() || d_im.hasSent());
231
232
15965
    Trace("sets") << "...iterate full effort check..." << std::endl;
233
15965
    fullEffortReset();
234
235
15965
    Trace("sets-eqc") << "Equality Engine:" << std::endl;
236
27772
    std::map<TypeNode, unsigned> eqcTypeCount;
237
15965
    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
238
313167
    while (!eqcs_i.isFinished())
239
    {
240
297202
      Node eqc = (*eqcs_i);
241
148601
      bool isSet = false;
242
297202
      TypeNode tn = eqc.getType();
243
148601
      d_state.registerEqc(tn, eqc);
244
148601
      eqcTypeCount[tn]++;
245
      // common type node and term
246
297202
      TypeNode tnc;
247
297202
      Node tnct;
248
148601
      if (tn.isSet())
249
      {
250
53584
        isSet = true;
251
53584
        tnc = tn.getSetElementType();
252
53584
        tnct = eqc;
253
      }
254
148601
      Trace("sets-eqc") << "[" << eqc << "] : ";
255
148601
      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
256
1134993
      while (!eqc_i.isFinished())
257
      {
258
986392
        Node n = (*eqc_i);
259
493196
        if (n != eqc)
260
        {
261
344595
          Trace("sets-eqc") << n << " (" << n.isConst() << ") ";
262
        }
263
986392
        TypeNode tnn = n.getType();
264
493196
        if (isSet)
265
        {
266
136623
          Assert(tnn.isSet());
267
273246
          TypeNode tnnel = tnn.getSetElementType();
268
136623
          tnc = TypeNode::mostCommonTypeNode(tnc, tnnel);
269
136623
          Assert(!tnc.isNull());
270
          // update the common type term
271
136623
          if (tnc == tnnel)
272
          {
273
136623
            tnct = n;
274
          }
275
        }
276
        // register it with the state
277
493196
        d_state.registerTerm(eqc, tnn, n);
278
493196
        Kind nk = n.getKind();
279
493196
        if (nk == kind::SINGLETON)
280
        {
281
          // ensure the proxy has been introduced
282
11751
          d_treg.getProxy(n);
283
        }
284
481445
        else if (nk == kind::CARD)
285
        {
286
47969
          d_card_enabled = true;
287
          // register it with the cardinality solver
288
47969
          d_cardSolver->registerTerm(n);
289
          // if we do not handle the kind, set incomplete
290
47969
          Kind nk0 = n[0].getKind();
291
          // some kinds of cardinality we cannot handle
292
47969
          if (d_rels->isRelationKind(nk0))
293
          {
294
26
            d_full_check_incomplete = true;
295
52
            Trace("sets-incomplete")
296
26
                << "Sets : incomplete because of " << n << "." << std::endl;
297
            // TODO (#1124):  The issue can be divided into 4 parts
298
            // 1- Supporting the universe cardinality for finite types with
299
            // finite cardinality (done)
300
            // 2- Supporting the universe cardinality for uninterpreted sorts
301
            // with finite-model-find (pending) See the implementation of
302
            //    CardinalityExtension::checkCardinalityExtended
303
            // 3- Supporting the universe cardinality for non-finite types
304
            // (done)
305
            // 4- Supporting cardinality for relations (hard)
306
          }
307
        }
308
433476
        else if (d_rels->isRelationKind(nk))
309
        {
310
2136
          d_rels_enabled = true;
311
        }
312
493196
        ++eqc_i;
313
      }
314
148601
      if (isSet)
315
      {
316
53584
        Assert(tnct.getType().getSetElementType() == tnc);
317
53584
        d_most_common_type[eqc] = tnc;
318
53584
        d_most_common_type_term[eqc] = tnct;
319
      }
320
148601
      Trace("sets-eqc") << std::endl;
321
148601
      ++eqcs_i;
322
    }
323
324
15965
    Trace("sets-eqc") << "...finished equality engine." << std::endl;
325
326
15965
    if (Trace.isOn("sets-state"))
327
    {
328
      Trace("sets-state") << "Equivalence class counters:" << std::endl;
329
      for (std::pair<const TypeNode, unsigned>& ec : eqcTypeCount)
330
      {
331
        Trace("sets-state")
332
            << "  " << ec.first << " -> " << ec.second << std::endl;
333
      }
334
    }
335
336
    // We may have sent lemmas while registering the terms in the loop above,
337
    // e.g. the cardinality solver.
338
15965
    if (d_im.hasSent())
339
    {
340
459
      continue;
341
    }
342
15506
    if (Trace.isOn("sets-mem"))
343
    {
344
      const std::vector<Node>& sec = d_state.getSetsEqClasses();
345
      for (const Node& s : sec)
346
      {
347
        Trace("sets-mem") << "Eqc " << s << " : ";
348
        const std::map<Node, Node>& smem = d_state.getMembers(s);
349
        if (!smem.empty())
350
        {
351
          Trace("sets-mem") << "Memberships : ";
352
          for (const std::pair<const Node, Node>& it2 : smem)
353
          {
354
            Trace("sets-mem") << it2.first << " ";
355
          }
356
        }
357
        Node ss = d_state.getSingletonEqClass(s);
358
        if (!ss.isNull())
359
        {
360
          Trace("sets-mem") << " : Singleton : " << ss;
361
        }
362
        Trace("sets-mem") << std::endl;
363
      }
364
    }
365
15506
    d_im.doPendingLemmas();
366
15506
    if (d_im.hasSent())
367
    {
368
      continue;
369
    }
370
    // check downwards closure
371
15506
    checkDownwardsClosure();
372
15506
    d_im.doPendingLemmas();
373
15506
    if (d_im.hasSent())
374
    {
375
488
      continue;
376
    }
377
    // check upwards closure
378
15018
    checkUpwardsClosure();
379
15018
    d_im.doPendingLemmas();
380
15018
    if (d_im.hasSent())
381
    {
382
1119
      continue;
383
    }
384
    // check disequalities
385
13899
    checkDisequalities();
386
13899
    d_im.doPendingLemmas();
387
13899
    if (d_im.hasSent())
388
    {
389
525
      continue;
390
    }
391
    // check reduce comprehensions
392
13374
    checkReduceComprehensions();
393
394
13374
    d_im.doPendingLemmas();
395
13374
    if (d_im.hasSent())
396
    {
397
18
      continue;
398
    }
399
13356
    if (d_card_enabled)
400
    {
401
      // call the check method of the cardinality solver
402
1659
      d_cardSolver->check();
403
1658
      if (d_im.hasSent())
404
      {
405
1549
        continue;
406
      }
407
    }
408
11806
    if (d_rels_enabled)
409
    {
410
      // call the check method of the relations solver
411
689
      d_rels->check(Theory::EFFORT_FULL);
412
    }
413
27205
  } while (!d_im.hasSentLemma() && !d_state.isInConflict()
414
27205
           && d_im.hasSentFact());
415
15964
  Assert(!d_im.hasPendingLemma() || d_im.hasSent());
416
31928
  Trace("sets") << "----- End full effort check, conflict="
417
31928
                << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
418
15964
                << std::endl;
419
15964
}
420
421
15506
void TheorySetsPrivate::checkDownwardsClosure()
422
{
423
15506
  Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl;
424
  // downwards closure
425
15506
  const std::vector<Node>& sec = d_state.getSetsEqClasses();
426
64300
  for (const Node& s : sec)
427
  {
428
48794
    const std::vector<Node>& nvsets = d_state.getNonVariableSets(s);
429
48794
    if (!nvsets.empty())
430
    {
431
36797
      const std::map<Node, Node>& smem = d_state.getMembers(s);
432
95315
      for (const Node& nv : nvsets)
433
      {
434
58518
        if (!d_state.isCongruent(nv))
435
        {
436
106905
          for (const std::pair<const Node, Node>& it2 : smem)
437
          {
438
104644
            Node mem = it2.second;
439
104644
            Node eq_set = nv;
440
52322
            Assert(d_equalityEngine->areEqual(mem[1], eq_set));
441
52322
            if (mem[1] != eq_set)
442
            {
443
102128
              Trace("sets-debug") << "Downwards closure based on " << mem
444
51064
                                  << ", eq_set = " << eq_set << std::endl;
445
102128
              if (!options::setsProxyLemmas())
446
              {
447
                Node nmem = NodeManager::currentNM()->mkNode(
448
102128
                    kind::MEMBER, mem[0], eq_set);
449
51064
                nmem = Rewriter::rewrite(nmem);
450
102128
                std::vector<Node> exp;
451
51064
                exp.push_back(mem);
452
51064
                exp.push_back(mem[1].eqNode(eq_set));
453
51064
                d_im.assertInference(nmem, InferenceId::SETS_DOWN_CLOSURE, exp);
454
51064
                if (d_state.isInConflict())
455
                {
456
                  return;
457
                }
458
              }
459
              else
460
              {
461
                // use proxy set
462
                Node k = d_treg.getProxy(eq_set);
463
                Node pmem =
464
                    NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k);
465
                Node nmem = NodeManager::currentNM()->mkNode(
466
                    kind::MEMBER, mem[0], eq_set);
467
                nmem = Rewriter::rewrite(nmem);
468
                std::vector<Node> exp;
469
                if (d_state.areEqual(mem, pmem))
470
                {
471
                  exp.push_back(pmem);
472
                }
473
                else
474
                {
475
                  nmem = NodeManager::currentNM()->mkNode(
476
                      kind::OR, pmem.negate(), nmem);
477
                }
478
                d_im.assertInference(nmem, InferenceId::SETS_DOWN_CLOSURE, exp);
479
              }
480
            }
481
          }
482
        }
483
      }
484
    }
485
  }
486
}
487
488
15018
void TheorySetsPrivate::checkUpwardsClosure()
489
{
490
  // upwards closure
491
15018
  NodeManager* nm = NodeManager::currentNM();
492
  const std::map<Kind, std::map<Node, std::map<Node, Node> > >& boi =
493
15018
      d_state.getBinaryOpIndex();
494
7700
  for (const std::pair<const Kind, std::map<Node, std::map<Node, Node> > >&
495
15018
           itb : boi)
496
  {
497
7700
    Kind k = itb.first;
498
15400
    Trace("sets") << "TheorySetsPrivate: check upwards closure " << k << "..."
499
7700
                  << std::endl;
500
31888
    for (const std::pair<const Node, std::map<Node, Node> >& it : itb.second)
501
    {
502
48376
      Node r1 = it.first;
503
      // see if there are members in first argument r1
504
24188
      const std::map<Node, Node>& r1mem = d_state.getMembers(r1);
505
24188
      if (!r1mem.empty() || k == kind::UNION)
506
      {
507
48203
        for (const std::pair<const Node, Node>& it2 : it.second)
508
        {
509
56716
          Node r2 = it2.first;
510
56716
          Node term = it2.second;
511
          // see if there are members in second argument
512
28358
          const std::map<Node, Node>& r2mem = d_state.getMembers(r2);
513
28358
          const std::map<Node, Node>& r2nmem = d_state.getNegativeMembers(r2);
514
28358
          if (!r2mem.empty() || k != kind::INTERSECTION)
515
          {
516
55584
            Trace("sets-debug")
517
55584
                << "Checking " << term << ", members = " << (!r1mem.empty())
518
27792
                << ", " << (!r2mem.empty()) << std::endl;
519
            // for all members of r1
520
27792
            if (!r1mem.empty())
521
            {
522
71972
              for (const std::pair<const Node, Node>& itm1m : r1mem)
523
              {
524
92910
                Node xr = itm1m.first;
525
92910
                Node x = itm1m.second[0];
526
92910
                Trace("sets-debug") << "checking membership " << xr << " "
527
46455
                                    << itm1m.second << std::endl;
528
92910
                std::vector<Node> exp;
529
46455
                exp.push_back(itm1m.second);
530
46455
                d_state.addEqualityToExp(term[0], itm1m.second[1], exp);
531
46455
                bool valid = false;
532
46455
                int inferType = 0;
533
46455
                if (k == kind::UNION)
534
                {
535
7924
                  valid = true;
536
                }
537
38531
                else if (k == kind::INTERSECTION)
538
                {
539
                  // conclude x is in term
540
                  // if also existing in members of r2
541
12549
                  std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
542
12549
                  if (itm != r2mem.end())
543
                  {
544
7751
                    exp.push_back(itm->second);
545
7751
                    d_state.addEqualityToExp(term[1], itm->second[1], exp);
546
7751
                    d_state.addEqualityToExp(x, itm->second[0], exp);
547
7751
                    valid = true;
548
                  }
549
                  else
550
                  {
551
                    // if not, check whether it is definitely not a member, if
552
                    // unknown, split
553
4798
                    if (r2nmem.find(xr) == r2nmem.end())
554
                    {
555
873
                      exp.push_back(nm->mkNode(kind::MEMBER, x, term[1]));
556
873
                      valid = true;
557
873
                      inferType = 1;
558
                    }
559
                  }
560
                }
561
                else
562
                {
563
25982
                  Assert(k == kind::SETMINUS);
564
25982
                  std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
565
25982
                  if (itm == r2mem.end())
566
                  {
567
                    // must add lemma for set minus since non-membership in this
568
                    // case is not explained
569
11385
                    exp.push_back(
570
22770
                        nm->mkNode(kind::MEMBER, x, term[1]).negate());
571
11385
                    valid = true;
572
11385
                    inferType = 1;
573
                  }
574
                }
575
46455
                if (valid)
576
                {
577
55866
                  Node rr = d_equalityEngine->getRepresentative(term);
578
27933
                  if (!d_state.isMember(x, rr))
579
                  {
580
4862
                    Node kk = d_treg.getProxy(term);
581
4862
                    Node fact = nm->mkNode(kind::MEMBER, x, kk);
582
2431
                    d_im.assertInference(
583
                        fact, InferenceId::SETS_UP_CLOSURE, exp, inferType);
584
2431
                    if (d_state.isInConflict())
585
                    {
586
                      return;
587
                    }
588
                  }
589
                }
590
92910
                Trace("sets-debug") << "done checking membership " << xr << " "
591
46455
                                    << itm1m.second << std::endl;
592
              }
593
            }
594
27792
            if (k == kind::UNION)
595
            {
596
7681
              if (!r2mem.empty())
597
              {
598
                // for all members of r2
599
17957
                for (const std::pair<const Node, Node>& itm2m : r2mem)
600
                {
601
24028
                  Node x = itm2m.second[0];
602
24028
                  Node rr = d_equalityEngine->getRepresentative(term);
603
12014
                  if (!d_state.isMember(x, rr))
604
                  {
605
1092
                    std::vector<Node> exp;
606
546
                    exp.push_back(itm2m.second);
607
546
                    d_state.addEqualityToExp(term[1], itm2m.second[1], exp);
608
1092
                    Node r = d_treg.getProxy(term);
609
1092
                    Node fact = nm->mkNode(kind::MEMBER, x, r);
610
546
                    d_im.assertInference(fact, InferenceId::SETS_UP_CLOSURE_2, exp);
611
546
                    if (d_state.isInConflict())
612
                    {
613
                      return;
614
                    }
615
                  }
616
                }
617
              }
618
            }
619
          }
620
        }
621
      }
622
    }
623
  }
624
15018
  if (!d_im.hasSent())
625
  {
626
14572
    if (options::setsExt())
627
    {
628
      // universal sets
629
1524
      Trace("sets-debug") << "Check universe sets..." << std::endl;
630
      // all elements must be in universal set
631
1524
      const std::vector<Node>& sec = d_state.getSetsEqClasses();
632
14333
      for (const Node& s : sec)
633
      {
634
        // if equivalence class contains a variable
635
25618
        Node v = d_state.getVariableSet(s);
636
12809
        if (!v.isNull())
637
        {
638
          // the variable in the equivalence class
639
8054
          std::map<TypeNode, Node> univ_set;
640
4027
          const std::map<Node, Node>& smems = d_state.getMembers(s);
641
8805
          for (const std::pair<const Node, Node>& it2 : smems)
642
          {
643
9556
            Node e = it2.second[0];
644
9556
            TypeNode tn = NodeManager::currentNM()->mkSetType(e.getType());
645
9556
            Node u;
646
4778
            std::map<TypeNode, Node>::iterator itu = univ_set.find(tn);
647
4778
            if (itu == univ_set.end())
648
            {
649
5060
              Node ueqc = d_state.getUnivSetEqClass(tn);
650
              // if the universe does not yet exist, or is not in this
651
              // equivalence class
652
2530
              if (s != ueqc)
653
              {
654
1797
                u = d_treg.getUnivSet(tn);
655
              }
656
2530
              univ_set[tn] = u;
657
            }
658
            else
659
            {
660
2248
              u = itu->second;
661
            }
662
4778
            if (!u.isNull())
663
            {
664
2950
              Assert(it2.second.getKind() == kind::MEMBER);
665
5900
              std::vector<Node> exp;
666
2950
              exp.push_back(it2.second);
667
2950
              if (v != it2.second[1])
668
              {
669
791
                exp.push_back(v.eqNode(it2.second[1]));
670
              }
671
5900
              Node fact = nm->mkNode(kind::MEMBER, it2.second[0], u);
672
2950
              d_im.assertInference(fact, InferenceId::SETS_UP_UNIV, exp);
673
2950
              if (d_state.isInConflict())
674
              {
675
                return;
676
              }
677
            }
678
          }
679
        }
680
      }
681
    }
682
  }
683
}
684
685
13899
void TheorySetsPrivate::checkDisequalities()
686
{
687
  // disequalities
688
13899
  Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
689
13899
  NodeManager* nm = NodeManager::currentNM();
690
24925
  for (NodeBoolMap::const_iterator it = d_deq.begin(); it != d_deq.end(); ++it)
691
  {
692
11551
    if (!(*it).second)
693
    {
694
      // not active
695
14416
      continue;
696
    }
697
8161
    Node deq = (*it).first;
698
    // check if it is already satisfied
699
8161
    Assert(d_equalityEngine->hasTerm(deq[0])
700
           && d_equalityEngine->hasTerm(deq[1]));
701
8161
    Node r1 = d_equalityEngine->getRepresentative(deq[0]);
702
8161
    Node r2 = d_equalityEngine->getRepresentative(deq[1]);
703
8161
    bool is_sat = d_state.isSetDisequalityEntailed(r1, r2);
704
16322
    Trace("sets-debug") << "Check disequality " << deq
705
8161
                        << ", is_sat = " << is_sat << std::endl;
706
    // will process regardless of sat/processed/unprocessed
707
8161
    d_deq[deq] = false;
708
709
8161
    if (is_sat)
710
    {
711
      // already satisfied
712
7523
      continue;
713
    }
714
638
    if (d_termProcessed.find(deq) != d_termProcessed.end())
715
    {
716
      // already added lemma
717
113
      continue;
718
    }
719
525
    d_termProcessed.insert(deq);
720
525
    d_termProcessed.insert(deq[1].eqNode(deq[0]));
721
525
    Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
722
525
    TypeNode elementType = deq[0].getType().getSetElementType();
723
525
    Node x = d_skCache.mkTypedSkolemCached(
724
525
        elementType, deq[0], deq[1], SkolemCache::SK_DISEQUAL, "sde");
725
525
    Node mem1 = nm->mkNode(MEMBER, x, deq[0]);
726
525
    Node mem2 = nm->mkNode(MEMBER, x, deq[1]);
727
525
    Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
728
525
    lem = Rewriter::rewrite(lem);
729
525
    d_im.assertInference(lem, InferenceId::SETS_DEQ, d_true, 1);
730
525
    d_im.doPendingLemmas();
731
525
    if (d_im.hasSent())
732
    {
733
525
      return;
734
    }
735
  }
736
}
737
738
13374
void TheorySetsPrivate::checkReduceComprehensions()
739
{
740
13374
  NodeManager* nm = NodeManager::currentNM();
741
13374
  const std::vector<Node>& comps = d_state.getComprehensionSets();
742
13442
  for (const Node& n : comps)
743
  {
744
68
    if (d_termProcessed.find(n) != d_termProcessed.end())
745
    {
746
      // already reduced it
747
46
      continue;
748
    }
749
22
    d_termProcessed.insert(n);
750
44
    Node v = nm->mkBoundVar(n[2].getType());
751
44
    Node body = nm->mkNode(AND, n[1], v.eqNode(n[2]));
752
    // must do substitution
753
44
    std::vector<Node> vars;
754
44
    std::vector<Node> subs;
755
44
    for (const Node& cv : n[0])
756
    {
757
22
      vars.push_back(cv);
758
44
      Node cvs = nm->mkBoundVar(cv.getType());
759
22
      subs.push_back(cvs);
760
    }
761
22
    body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
762
44
    Node bvl = nm->mkNode(BOUND_VAR_LIST, subs);
763
22
    body = nm->mkNode(EXISTS, bvl, body);
764
44
    Node mem = nm->mkNode(MEMBER, v, n);
765
    Node lem =
766
44
        nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
767
44
    Trace("sets-comprehension")
768
22
        << "Comprehension reduction: " << lem << std::endl;
769
22
    d_im.lemma(lem, InferenceId::SETS_COMPREHENSION);
770
  }
771
13374
}
772
773
//--------------------------------- standard check
774
775
67784
void TheorySetsPrivate::postCheck(Theory::Effort level)
776
{
777
135568
  Trace("sets-check") << "Sets finished assertions effort " << level
778
67784
                      << std::endl;
779
  // invoke full effort check, relations check
780
67784
  if (!d_state.isInConflict())
781
  {
782
65146
    if (level == Theory::EFFORT_FULL)
783
    {
784
19883
      if (!d_external.d_valuation.needCheck())
785
      {
786
15965
        fullEffortCheck();
787
47892
        if (!d_state.isInConflict() && !d_im.hasSentLemma()
788
27205
            && d_full_check_incomplete)
789
        {
790
4
          d_im.setIncomplete();
791
        }
792
      }
793
    }
794
  }
795
67783
  Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
796
67783
}
797
798
107382
void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact)
799
{
800
107382
  if (d_state.isInConflict())
801
  {
802
2487
    return;
803
  }
804
104895
  if (atom.getKind() == kind::MEMBER && polarity)
805
  {
806
    // check if set has a value, if so, we can propagate
807
58602
    Node r = d_equalityEngine->getRepresentative(atom[1]);
808
29301
    EqcInfo* e = getOrMakeEqcInfo(r, true);
809
29301
    if (e)
810
    {
811
58602
      Node s = e->d_singleton;
812
29301
      if (!s.isNull())
813
      {
814
        Node pexp = NodeManager::currentNM()->mkNode(
815
5088
            kind::AND, atom, atom[1].eqNode(s));
816
2544
        if (s.getKind() == kind::SINGLETON)
817
        {
818
2393
          if (s[0] != atom[0])
819
          {
820
970
            Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl;
821
1940
            Node eq = s[0].eqNode(atom[0]);
822
            // triggers an internal inference
823
970
            d_im.assertInternalFact(eq, true, InferenceId::SETS_MEM_EQ, pexp);
824
          }
825
        }
826
        else
827
        {
828
302
          Trace("sets-prop")
829
151
              << "Propagate mem-eq conflict : " << pexp << std::endl;
830
151
          d_im.conflict(pexp, InferenceId::SETS_MEM_EQ_CONFLICT);
831
        }
832
      }
833
    }
834
    // add to membership list
835
29301
    d_state.addMember(r, atom);
836
  }
837
}
838
//--------------------------------- end standard check
839
840
/************************ Sharing ************************/
841
/************************ Sharing ************************/
842
/************************ Sharing ************************/
843
844
21011
void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
845
                                     TNodeTrie* t2,
846
                                     unsigned arity,
847
                                     unsigned depth,
848
                                     unsigned& n_pairs)
849
{
850
21011
  if (depth == arity)
851
  {
852
12130
    if (t2 != NULL)
853
    {
854
24260
      Node f1 = t1->getData();
855
24260
      Node f2 = t2->getData();
856
857
      // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or
858
      // not for the shared variables x, y in the care graph.
859
      // However, this does not apply to the membership operator since the
860
      // equality or disequality between members affects the number of elements
861
      // in a set. Therefore we need to split on (= x y) for kind MEMBER.
862
      // Example:
863
      // Suppose (= (member x S) member( y, S)) is true and there are
864
      // no other members in S. We would get S = {x} if (= x y) is true.
865
      // Otherwise we would get S = {x, y}.
866
12130
      if (f1.getKind() == MEMBER || !d_state.areEqual(f1, f2))
867
      {
868
12130
        Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
869
24260
        vector<pair<TNode, TNode> > currentPairs;
870
35938
        for (unsigned k = 0; k < f1.getNumChildren(); ++k)
871
        {
872
47616
          TNode x = f1[k];
873
47616
          TNode y = f2[k];
874
23808
          Assert(d_equalityEngine->hasTerm(x));
875
23808
          Assert(d_equalityEngine->hasTerm(y));
876
23808
          Assert(!d_state.areDisequal(x, y));
877
23808
          Assert(!areCareDisequal(x, y));
878
23808
          if (!d_equalityEngine->areEqual(x, y))
879
          {
880
31154
            Trace("sets-cg")
881
15577
                << "Arg #" << k << " is " << x << " " << y << std::endl;
882
46731
            if (d_equalityEngine->isTriggerTerm(x, THEORY_SETS)
883
46731
                && d_equalityEngine->isTriggerTerm(y, THEORY_SETS))
884
            {
885
6169
              TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
886
12338
                  x, THEORY_SETS);
887
6169
              TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
888
12338
                  y, THEORY_SETS);
889
6169
              currentPairs.push_back(make_pair(x_shared, y_shared));
890
            }
891
9408
            else if (isCareArg(f1, k) && isCareArg(f2, k))
892
            {
893
              // splitting on sets (necessary for handling set of sets properly)
894
6
              if (x.getType().isSet())
895
              {
896
6
                Assert(y.getType().isSet());
897
6
                if (!d_state.areDisequal(x, y))
898
                {
899
12
                  Trace("sets-cg-lemma")
900
6
                      << "Should split on : " << x << "==" << y << std::endl;
901
6
                  d_im.split(x.eqNode(y), InferenceId::UNKNOWN);
902
                }
903
              }
904
            }
905
          }
906
        }
907
18299
        for (unsigned c = 0; c < currentPairs.size(); ++c)
908
        {
909
12338
          Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " "
910
6169
                                << currentPairs[c].second << std::endl;
911
6169
          d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
912
6169
          n_pairs++;
913
        }
914
      }
915
    }
916
  }
917
  else
918
  {
919
8881
    if (t2 == NULL)
920
    {
921
7946
      if (depth < (arity - 1))
922
      {
923
        // add care pairs internal to each child
924
7357
        for (std::pair<const TNode, TNodeTrie>& t : t1->d_data)
925
        {
926
6307
          addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs);
927
        }
928
      }
929
      // add care pairs based on each pair of non-disequal arguments
930
28304
      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
931
28304
           it != t1->d_data.end();
932
           ++it)
933
      {
934
20358
        std::map<TNode, TNodeTrie>::iterator it2 = it;
935
20358
        ++it2;
936
247336
        for (; it2 != t1->d_data.end(); ++it2)
937
        {
938
113489
          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
939
          {
940
21749
            if (!areCareDisequal(it->first, it2->first))
941
            {
942
27480
              addCarePairs(
943
18320
                  &it->second, &it2->second, arity, depth + 1, n_pairs);
944
            }
945
          }
946
        }
947
      }
948
    }
949
    else
950
    {
951
      // add care pairs based on product of indices, non-disequal arguments
952
2727
      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
953
      {
954
6138
        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
955
        {
956
4346
          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
957
          {
958
3905
            if (!areCareDisequal(tt1.first, tt2.first))
959
            {
960
3905
              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
961
            }
962
          }
963
        }
964
      }
965
    }
966
  }
967
21011
}
968
969
5917
void TheorySetsPrivate::computeCareGraph()
970
{
971
5917
  const std::map<Kind, std::vector<Node> >& ol = d_state.getOperatorList();
972
7917
  for (const std::pair<const Kind, std::vector<Node> >& it : ol)
973
  {
974
2000
    Kind k = it.first;
975
2000
    if (k == kind::SINGLETON || k == kind::MEMBER)
976
    {
977
1333
      unsigned n_pairs = 0;
978
2666
      Trace("sets-cg-summary") << "Compute graph for sets, op=" << k << "..."
979
1333
                               << it.second.size() << std::endl;
980
1333
      Trace("sets-cg") << "Build index for " << k << "..." << std::endl;
981
2666
      std::map<TypeNode, TNodeTrie> index;
982
1333
      unsigned arity = 0;
983
      // populate indices
984
15384
      for (TNode f1 : it.second)
985
      {
986
14051
        Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
987
14051
        Assert(d_equalityEngine->hasTerm(f1));
988
        // break into index based on operator, and type of first argument (since
989
        // some operators are parametric)
990
28102
        TypeNode tn = f1[0].getType();
991
28102
        std::vector<TNode> reps;
992
14051
        bool hasCareArg = false;
993
38066
        for (unsigned j = 0; j < f1.getNumChildren(); j++)
994
        {
995
24015
          reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
996
24015
          if (isCareArg(f1, j))
997
          {
998
19893
            hasCareArg = true;
999
          }
1000
        }
1001
14051
        if (hasCareArg)
1002
        {
1003
14051
          Trace("sets-cg-debug") << "......adding." << std::endl;
1004
14051
          index[tn].addTerm(f1, reps);
1005
14051
          arity = reps.size();
1006
        }
1007
        else
1008
        {
1009
          Trace("sets-cg-debug") << "......skip." << std::endl;
1010
        }
1011
      }
1012
1333
      if (arity > 0)
1013
      {
1014
        // for each index
1015
2972
        for (std::pair<const TypeNode, TNodeTrie>& tt : index)
1016
        {
1017
3278
          Trace("sets-cg") << "Process index " << tt.first << "..."
1018
1639
                           << std::endl;
1019
1639
          addCarePairs(&tt.second, nullptr, arity, 0, n_pairs);
1020
        }
1021
      }
1022
1333
      Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
1023
    }
1024
  }
1025
5917
}
1026
1027
36769
bool TheorySetsPrivate::isCareArg(Node n, unsigned a)
1028
{
1029
36769
  if (d_equalityEngine->isTriggerTerm(n[a], THEORY_SETS))
1030
  {
1031
23225
    return true;
1032
  }
1033
27088
  else if ((n.getKind() == kind::MEMBER || n.getKind() == kind::SINGLETON)
1034
40632
           && a == 0 && n[0].getType().isSet())
1035
  {
1036
20
    return true;
1037
  }
1038
  else
1039
  {
1040
13524
    return false;
1041
  }
1042
}
1043
1044
/******************** Model generation ********************/
1045
/******************** Model generation ********************/
1046
/******************** Model generation ********************/
1047
1048
namespace {
1049
/**
1050
 * This function is a helper function to print sets as
1051
 * Set A = { a0, a1, a2, }
1052
 * instead of
1053
 * (union (singleton a0) (union (singleton a1) (singleton a2)))
1054
 */
1055
7179
void traceSetElementsRecursively(stringstream& stream, const Node& set)
1056
{
1057
7179
  Assert(set.getType().isSet());
1058
7179
  if (set.getKind() == SINGLETON)
1059
  {
1060
5602
    stream << set[0] << ", ";
1061
  }
1062
7179
  if (set.getKind() == UNION)
1063
  {
1064
1122
    traceSetElementsRecursively(stream, set[0]);
1065
1122
    traceSetElementsRecursively(stream, set[1]);
1066
  }
1067
7179
}
1068
1069
4935
std::string traceElements(const Node& set)
1070
{
1071
9870
  std::stringstream stream;
1072
4935
  traceSetElementsRecursively(stream, set);
1073
9870
  return stream.str();
1074
}
1075
1076
}  // namespace
1077
1078
4580
bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
1079
                                           const std::set<Node>& termSet)
1080
{
1081
4580
  Trace("sets-model") << "Set collect model values" << std::endl;
1082
1083
4580
  NodeManager* nm = NodeManager::currentNM();
1084
9160
  std::map<Node, Node> mvals;
1085
  // If cardinality is enabled, we need to use the ordered equivalence class
1086
  // list computed by the cardinality solver, where sets equivalence classes
1087
  // are assigned model values based on their position in the cardinality
1088
  // graph.
1089
4580
  const std::vector<Node>& sec = d_card_enabled
1090
9098
                                     ? d_cardSolver->getOrderedSetsEqClasses()
1091
9098
                                     : d_state.getSetsEqClasses();
1092
4580
  Valuation& val = getValuation();
1093
9556
  for (int i = (int)(sec.size() - 1); i >= 0; i--)
1094
  {
1095
9952
    Node eqc = sec[i];
1096
4976
    if (termSet.find(eqc) == termSet.end())
1097
    {
1098
82
      Trace("sets-model") << "* Do not assign value for " << eqc
1099
41
                          << " since is not relevant." << std::endl;
1100
    }
1101
    else
1102
    {
1103
9870
      std::vector<Node> els;
1104
4935
      bool is_base = !d_card_enabled || d_cardSolver->isModelValueBasic(eqc);
1105
4935
      if (is_base)
1106
      {
1107
9760
        Trace("sets-model")
1108
4880
            << "Collect elements of base eqc " << eqc << std::endl;
1109
        // members that must be in eqc
1110
4880
        const std::map<Node, Node>& emems = d_state.getMembers(eqc);
1111
4880
        if (!emems.empty())
1112
        {
1113
8918
          TypeNode elementType = eqc.getType().getSetElementType();
1114
9857
          for (const std::pair<const Node, Node>& itmm : emems)
1115
          {
1116
10796
            Trace("sets-model")
1117
5398
                << "m->getRepresentative(" << itmm.first
1118
5398
                << ")= " << m->getRepresentative(itmm.first) << std::endl;
1119
10796
            Node t = nm->mkSingleton(elementType, itmm.first);
1120
5398
            els.push_back(t);
1121
          }
1122
        }
1123
      }
1124
4935
      if (d_card_enabled)
1125
      {
1126
        // make the slack elements for the equivalence class based on set
1127
        // cardinality
1128
167
        d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals, m);
1129
      }
1130
1131
9870
      Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType());
1132
4935
      rep = Rewriter::rewrite(rep);
1133
9870
      Trace("sets-model") << "* Assign representative of " << eqc << " to "
1134
4935
                          << rep << std::endl;
1135
4935
      mvals[eqc] = rep;
1136
4935
      if (!m->assertEquality(eqc, rep, true))
1137
      {
1138
        return false;
1139
      }
1140
4935
      m->assertSkeleton(rep);
1141
1142
      // we add the element terms (singletons) as representatives to tell the
1143
      // model builder to evaluate them along with their union (rep).
1144
      // This is needed to account for cases when members and rep are not enough
1145
      // for the model builder to evaluate set terms.
1146
      // e.g.
1147
      // eqc(rep) = [(union (singleton skolem) (singleton 0))]
1148
      // eqc(skolem) = [0]
1149
      // The model builder would fail to evaluate rep as (singleton 0)
1150
      // if (singleton skolem) is not registered as a representative in the
1151
      // model
1152
10459
      for (const Node& el : els)
1153
      {
1154
5524
        m->assertSkeleton(el);
1155
      }
1156
1157
9870
      Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep)
1158
4935
                          << " }" << std::endl;
1159
    }
1160
  }
1161
1162
  // handle slack elements constraints for finite types
1163
4580
  if (d_card_enabled)
1164
  {
1165
    const std::map<TypeNode, std::vector<TNode> >& slackElements =
1166
62
        d_cardSolver->getFiniteTypeSlackElements();
1167
70
    for (const auto& pair : slackElements)
1168
    {
1169
      const std::vector<Node>& members =
1170
8
          d_cardSolver->getFiniteTypeMembers(pair.first);
1171
8
      m->setAssignmentExclusionSetGroup(pair.second, members);
1172
16
      Trace("sets-model") << "ExclusionSet: Group " << pair.second
1173
8
                          << " is excluded from set" << members << std::endl;
1174
    }
1175
  }
1176
4580
  return true;
1177
}
1178
1179
/********************** Helper functions ***************************/
1180
/********************** Helper functions ***************************/
1181
/********************** Helper functions ***************************/
1182
1183
1896
Node mkAnd(const std::vector<TNode>& conjunctions)
1184
{
1185
1896
  Assert(conjunctions.size() > 0);
1186
1187
3792
  std::set<TNode> all;
1188
8402
  for (unsigned i = 0; i < conjunctions.size(); ++i)
1189
  {
1190
13012
    TNode t = conjunctions[i];
1191
6506
    if (t.getKind() == kind::AND)
1192
    {
1193
357
      for (TNode::iterator child_it = t.begin(); child_it != t.end();
1194
           ++child_it)
1195
      {
1196
238
        Assert((*child_it).getKind() != kind::AND);
1197
238
        all.insert(*child_it);
1198
      }
1199
    }
1200
    else
1201
    {
1202
6387
      all.insert(t);
1203
    }
1204
  }
1205
1206
1896
  Assert(all.size() > 0);
1207
1896
  if (all.size() == 1)
1208
  {
1209
    // All the same, or just one
1210
309
    return conjunctions[0];
1211
  }
1212
1213
3174
  NodeBuilder<> conjunction(kind::AND);
1214
1587
  std::set<TNode>::const_iterator it = all.begin();
1215
1587
  std::set<TNode>::const_iterator it_end = all.end();
1216
13225
  while (it != it_end)
1217
  {
1218
5819
    conjunction << *it;
1219
5819
    ++it;
1220
  }
1221
1587
  return conjunction;
1222
} /* mkAnd() */
1223
1224
4580
Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
1225
1226
1896
Node TheorySetsPrivate::explain(TNode literal)
1227
{
1228
1896
  Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;
1229
1230
1896
  bool polarity = literal.getKind() != kind::NOT;
1231
3792
  TNode atom = polarity ? literal : literal[0];
1232
3792
  std::vector<TNode> assumptions;
1233
1234
1896
  if (atom.getKind() == kind::EQUAL)
1235
  {
1236
1443
    d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
1237
  }
1238
453
  else if (atom.getKind() == kind::MEMBER)
1239
  {
1240
453
    d_equalityEngine->explainPredicate(atom, polarity, assumptions);
1241
  }
1242
  else
1243
  {
1244
    Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
1245
                  << polarity << "); kind" << atom.getKind() << std::endl;
1246
    Unhandled();
1247
  }
1248
1249
3792
  return mkAnd(assumptions);
1250
}
1251
1252
58456
void TheorySetsPrivate::preRegisterTerm(TNode node)
1253
{
1254
116912
  Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
1255
58456
                << std::endl;
1256
58456
  switch (node.getKind())
1257
  {
1258
32647
    case kind::EQUAL:
1259
    case kind::MEMBER:
1260
    {
1261
      // add trigger predicate for equality and membership
1262
32647
      d_equalityEngine->addTriggerPredicate(node);
1263
    }
1264
32647
    break;
1265
25809
    default: d_equalityEngine->addTerm(node); break;
1266
  }
1267
58456
}
1268
1269
44541
TrustNode TheorySetsPrivate::ppRewrite(Node node,
1270
                                       std::vector<SkolemLemma>& lems)
1271
{
1272
44541
  Debug("sets-proc") << "ppRewrite : " << node << std::endl;
1273
1274
44541
  switch (node.getKind())
1275
  {
1276
5
    case kind::CHOOSE: return expandChooseOperator(node, lems);
1277
8
    case kind::IS_SINGLETON: return expandIsSingletonOperator(node);
1278
44528
    default: return TrustNode::null();
1279
  }
1280
}
1281
1282
5
TrustNode TheorySetsPrivate::expandChooseOperator(
1283
    const Node& node, std::vector<SkolemLemma>& lems)
1284
{
1285
5
  Assert(node.getKind() == CHOOSE);
1286
1287
  // (choose A) is expanded as
1288
  // (witness ((x elementType))
1289
  //    (ite
1290
  //      (= A (as emptyset setType))
1291
  //      (= x chooseUf(A))
1292
  //      (and (member x A) (= x chooseUf(A)))
1293
1294
5
  NodeManager* nm = NodeManager::currentNM();
1295
10
  Node set = node[0];
1296
10
  TypeNode setType = set.getType();
1297
10
  Node chooseSkolem = getChooseFunction(setType);
1298
10
  Node apply = NodeManager::currentNM()->mkNode(APPLY_UF, chooseSkolem, set);
1299
1300
10
  Node witnessVariable = nm->mkBoundVar(setType.getSetElementType());
1301
1302
10
  Node equal = witnessVariable.eqNode(apply);
1303
10
  Node emptySet = nm->mkConst(EmptySet(setType));
1304
10
  Node isEmpty = set.eqNode(emptySet);
1305
10
  Node member = nm->mkNode(MEMBER, witnessVariable, set);
1306
10
  Node memberAndEqual = member.andNode(equal);
1307
10
  Node ite = nm->mkNode(ITE, isEmpty, equal, memberAndEqual);
1308
5
  SkolemManager* sm = nm->getSkolemManager();
1309
10
  Node ret = sm->mkSkolem(witnessVariable, ite, "kSetChoose");
1310
5
  lems.push_back(SkolemLemma(ret, nullptr));
1311
10
  return TrustNode::mkTrustRewrite(node, ret, nullptr);
1312
}
1313
1314
8
TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
1315
{
1316
8
  Assert(node.getKind() == IS_SINGLETON);
1317
1318
  // we call the rewriter here to handle the pattern
1319
  // (is_singleton (singleton x)) because the rewriter is called after expansion
1320
16
  Node rewritten = Rewriter::rewrite(node);
1321
8
  if (rewritten.getKind() != IS_SINGLETON)
1322
  {
1323
    return TrustNode::mkTrustRewrite(node, rewritten, nullptr);
1324
  }
1325
1326
  // (is_singleton A) is expanded as
1327
  // (exists ((x: T)) (= A (singleton x)))
1328
  // where T is the sort of elements of A
1329
1330
8
  NodeManager* nm = NodeManager::currentNM();
1331
16
  Node set = rewritten[0];
1332
1333
8
  std::map<Node, Node>::iterator it = d_isSingletonNodes.find(rewritten);
1334
1335
8
  if (it != d_isSingletonNodes.end())
1336
  {
1337
    return TrustNode::mkTrustRewrite(rewritten, it->second, nullptr);
1338
  }
1339
1340
16
  TypeNode setType = set.getType();
1341
16
  Node boundVar = nm->mkBoundVar(setType.getSetElementType());
1342
16
  Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar);
1343
16
  Node equal = set.eqNode(singleton);
1344
16
  std::vector<Node> variables = {boundVar};
1345
16
  Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables);
1346
16
  Node exists = nm->mkNode(kind::EXISTS, boundVars, equal);
1347
8
  d_isSingletonNodes[rewritten] = exists;
1348
1349
8
  return TrustNode::mkTrustRewrite(node, exists, nullptr);
1350
}
1351
1352
5
Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
1353
{
1354
5
  std::map<TypeNode, Node>::iterator it = d_chooseFunctions.find(setType);
1355
5
  if (it != d_chooseFunctions.end())
1356
  {
1357
    return it->second;
1358
  }
1359
1360
5
  NodeManager* nm = NodeManager::currentNM();
1361
10
  TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType());
1362
10
  stringstream stream;
1363
5
  stream << "chooseUf" << setType.getId();
1364
10
  string name = stream.str();
1365
  Node chooseSkolem = nm->mkSkolem(
1366
10
      name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
1367
5
  d_chooseFunctions[setType] = chooseSkolem;
1368
5
  return chooseSkolem;
1369
}
1370
1371
12418
void TheorySetsPrivate::presolve() { d_state.reset(); }
1372
1373
}  // namespace sets
1374
}  // namespace theory
1375
26685
}  // namespace CVC4