GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/cardinality_extension.cpp Lines: 514 573 89.7 %
Date: 2021-03-22 Branches: 1215 2605 46.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cardinality_extension.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed, Gereon Kremer
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 Implementation of an extension of the theory sets for handling
13
 ** cardinality constraints.
14
 **/
15
16
#include "theory/sets/cardinality_extension.h"
17
18
#include "expr/emptyset.h"
19
#include "expr/node_algorithm.h"
20
#include "options/sets_options.h"
21
#include "smt/logic_exception.h"
22
#include "theory/rewriter.h"
23
#include "theory/sets/normal_form.h"
24
#include "theory/theory_model.h"
25
#include "theory/valuation.h"
26
27
using namespace std;
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace sets {
33
34
8995
CardinalityExtension::CardinalityExtension(SolverState& s,
35
                                           InferenceManager& im,
36
8995
                                           TermRegistry& treg)
37
    : d_state(s),
38
      d_im(im),
39
      d_treg(treg),
40
8995
      d_card_processed(s.getUserContext()),
41
17990
      d_finite_type_constants_processed(false)
42
{
43
8995
  d_true = NodeManager::currentNM()->mkConst(true);
44
8995
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
45
8995
}
46
47
15955
void CardinalityExtension::reset()
48
{
49
15955
  d_eqc_to_card_term.clear();
50
15955
  d_t_card_enabled.clear();
51
15955
  d_finite_type_elements.clear();
52
15955
  d_finite_type_slack_elements.clear();
53
15955
  d_univProxy.clear();
54
15955
}
55
47969
void CardinalityExtension::registerTerm(Node n)
56
{
57
47969
  Trace("sets-card-debug") << "Register term : " << n << std::endl;
58
47969
  Assert(n.getKind() == CARD);
59
95938
  TypeNode tnc = n[0].getType().getSetElementType();
60
47969
  d_t_card_enabled[tnc] = true;
61
95938
  Node r = d_state.getRepresentative(n[0]);
62
47969
  if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
63
  {
64
29747
    d_eqc_to_card_term[r] = n;
65
29747
    registerCardinalityTerm(n[0]);
66
  }
67
47969
  Trace("sets-card-debug") << "...finished register term" << std::endl;
68
47969
}
69
70
1659
void CardinalityExtension::checkCardinalityExtended()
71
{
72
3317
  for (std::pair<const TypeNode, bool>& pair : d_t_card_enabled)
73
  {
74
3318
    TypeNode type = pair.first;
75
1659
    if (pair.second)
76
    {
77
1659
      checkCardinalityExtended(type);
78
    }
79
  }
80
1658
}
81
82
1659
void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
83
{
84
1659
  NodeManager* nm = NodeManager::currentNM();
85
2614
  TypeNode setType = nm->mkSetType(t);
86
  // skip infinite types that do not have univset terms
87
1659
  if (!t.isInterpretedFinite() && d_state.getUnivSetEqClass(setType).isNull())
88
  {
89
704
    return;
90
  }
91
92
  // get the cardinality of the finite type t
93
1910
  Cardinality card = t.getCardinality();
94
95
  // cardinality of an interpreted finite type t is infinite when t
96
  // is infinite without --fmf
97
955
  if (t.isInterpretedFinite() && card.isInfinite())
98
  {
99
    // TODO (#1123): support uninterpreted sorts with --finite-model-find
100
2
    std::stringstream message;
101
1
    message << "The cardinality " << card << " of the finite type " << t
102
1
            << " is not supported yet.";
103
1
    throw LogicException(message.str());
104
  }
105
106
  // here we call getUnivSet instead of getUnivSetEqClass to generate
107
  // a univset term for finite types even if they are not used in the input
108
1908
  Node univ = d_treg.getUnivSet(setType);
109
954
  std::map<Node, Node>::iterator it = d_univProxy.find(univ);
110
111
1908
  Node proxy;
112
113
954
  if (it == d_univProxy.end())
114
  {
115
    // Force cvc4 to build the cardinality graph for the universe set
116
954
    proxy = d_treg.getProxy(univ);
117
954
    d_univProxy[univ] = proxy;
118
  }
119
  else
120
  {
121
    proxy = it->second;
122
  }
123
124
  // get all equivalent classes of type t
125
1908
  vector<Node> representatives = d_state.getSetsEqClasses(t);
126
127
954
  if (t.isInterpretedFinite())
128
  {
129
1444
    Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));
130
1444
    Node cardUniv = nm->mkNode(kind::CARD, proxy);
131
1444
    Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality);
132
133
    // (=> true (<= (card (as univset t)) cardUniv)
134
722
    if (!d_state.isEntailed(leq, true))
135
    {
136
722
      d_im.assertInference(leq, InferenceId::SETS_CARD_UNIV_TYPE, d_true, 1);
137
    }
138
  }
139
140
  // add subset lemmas for sets and membership lemmas for negative members
141
9554
  for (Node& representative : representatives)
142
  {
143
    // the universe set is a subset of itself
144
8600
    if (representative != d_state.getRepresentative(univ))
145
    {
146
      // here we only add representatives with variables to avoid adding
147
      // infinite equivalent generated terms to the cardinality graph
148
9560
      Node variable = d_state.getVariableSet(representative);
149
7654
      if (variable.isNull())
150
      {
151
5748
        continue;
152
      }
153
154
      // (=> true (subset representative (as univset t))
155
3812
      Node subset = nm->mkNode(kind::SUBSET, variable, proxy);
156
      // subset terms are rewritten as union terms: (subset A B) implies (=
157
      // (union A B) B)
158
1906
      subset = Rewriter::rewrite(subset);
159
1906
      if (!d_state.isEntailed(subset, true))
160
      {
161
120
        d_im.assertInference(
162
            subset, InferenceId::SETS_CARD_UNIV_SUPERSET, d_true, 1);
163
      }
164
165
      // negative members are members in the universe set
166
      const std::map<Node, Node>& negativeMembers =
167
1906
          d_state.getNegativeMembers(representative);
168
169
4039
      for (const auto& negativeMember : negativeMembers)
170
      {
171
4266
        Node member = nm->mkNode(MEMBER, negativeMember.first, univ);
172
        // negativeMember.second is the reason for the negative membership and
173
        // has kind MEMBER. So we specify the negation as the reason for the
174
        // negative membership lemma
175
4266
        Node notMember = nm->mkNode(NOT, negativeMember.second);
176
        // (=>
177
        //    (not (member negativeMember representative)))
178
        //    (member negativeMember (as univset t)))
179
2133
        d_im.assertInference(
180
            member, InferenceId::SETS_CARD_NEGATIVE_MEMBER, notMember, 1);
181
      }
182
    }
183
  }
184
}
185
186
1659
void CardinalityExtension::check()
187
{
188
1659
  checkCardinalityExtended();
189
1658
  checkRegister();
190
1658
  if (d_im.hasSent())
191
  {
192
1865
    return;
193
  }
194
1363
  checkMinCard();
195
1363
  if (d_im.hasSent())
196
  {
197
411
    return;
198
  }
199
952
  checkCardCycles();
200
952
  if (d_im.hasSent())
201
  {
202
399
    return;
203
  }
204
  // The last step will either do nothing (in which case we are SAT), or request
205
  // that a new set term is introduced.
206
641
  std::vector<Node> intro_sets;
207
553
  checkNormalForms(intro_sets);
208
553
  if (intro_sets.empty())
209
  {
210
465
    return;
211
  }
212
88
  Assert(intro_sets.size() == 1);
213
88
  Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
214
88
  Trace("sets-intro") << "  Actual Intro : ";
215
88
  d_treg.debugPrintSet(intro_sets[0], "sets-nf");
216
88
  Trace("sets-nf") << std::endl;
217
176
  Node k = d_treg.getProxy(intro_sets[0]);
218
88
  AlwaysAssert(!k.isNull());
219
}
220
221
1658
void CardinalityExtension::checkRegister()
222
{
223
1658
  Trace("sets") << "Cardinality graph..." << std::endl;
224
1658
  NodeManager* nm = NodeManager::currentNM();
225
  // first, ensure cardinality relationships are added as lemmas for all
226
  // non-basic set terms
227
1658
  const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
228
18319
  for (const Node& eqc : setEqc)
229
  {
230
16661
    const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
231
37292
    for (Node n : nvsets)
232
    {
233
20631
      if (!d_state.isCongruent(n))
234
      {
235
        // if setminus, do for intersection instead
236
20365
        if (n.getKind() == SETMINUS)
237
        {
238
10162
          n = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
239
        }
240
20365
        registerCardinalityTerm(n);
241
      }
242
    }
243
  }
244
1658
  Trace("sets") << "Done cardinality graph" << std::endl;
245
1658
}
246
247
50112
void CardinalityExtension::registerCardinalityTerm(Node n)
248
{
249
51782
  TypeNode tnc = n.getType().getSetElementType();
250
50112
  if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
251
  {
252
    // if no cardinality constraints for sets of this type, we can ignore
253
144
    return;
254
  }
255
49968
  if (d_card_processed.find(n) != d_card_processed.end())
256
  {
257
    // already processed
258
48298
    return;
259
  }
260
1670
  d_card_processed.insert(n);
261
1670
  NodeManager* nm = NodeManager::currentNM();
262
1670
  Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
263
3340
  std::vector<Node> cterms;
264
1670
  if (n.getKind() == INTERSECTION)
265
  {
266
966
    for (unsigned e = 0; e < 2; e++)
267
    {
268
1288
      Node s = nm->mkNode(SETMINUS, n[e], n[1 - e]);
269
644
      cterms.push_back(s);
270
    }
271
644
    Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, n), d_zero);
272
322
    d_im.assertInference(
273
        pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
274
  }
275
  else
276
  {
277
1348
    cterms.push_back(n);
278
  }
279
3662
  for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
280
  {
281
3984
    Node nn = cterms[k];
282
3984
    Node nk = d_treg.getProxy(nn);
283
3984
    Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, nk), d_zero);
284
1992
    d_im.assertInference(
285
        pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
286
1992
    if (nn != nk)
287
    {
288
1886
      Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn));
289
943
      lem = Rewriter::rewrite(lem);
290
943
      Trace("sets-card") << "  " << k << " : " << lem << std::endl;
291
943
      d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1);
292
    }
293
  }
294
1670
  d_im.doPendingLemmas();
295
}
296
297
952
void CardinalityExtension::checkCardCycles()
298
{
299
952
  Trace("sets") << "Check cardinality cycles..." << std::endl;
300
  // build order of equivalence classes, also build cardinality graph
301
952
  const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
302
952
  d_oSetEqc.clear();
303
952
  d_card_parent.clear();
304
8083
  for (const Node& s : setEqc)
305
  {
306
14661
    std::vector<Node> curr;
307
14661
    std::vector<Node> exp;
308
7530
    checkCardCyclesRec(s, curr, exp);
309
7530
    if (d_im.hasSent())
310
    {
311
399
      return;
312
    }
313
  }
314
315
553
  Trace("sets") << "d_card_parent: " << d_card_parent << std::endl;
316
553
  Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
317
553
  Trace("sets") << "Done check cardinality cycles" << std::endl;
318
}
319
320
12833
void CardinalityExtension::checkCardCyclesRec(Node eqc,
321
                                              std::vector<Node>& curr,
322
                                              std::vector<Node>& exp)
323
{
324
12833
  Trace("sets-cycle-debug") << "Traverse eqc " << eqc << std::endl;
325
12833
  NodeManager* nm = NodeManager::currentNM();
326
12833
  if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
327
  {
328
    Trace("sets-debug") << "Found venn region loop..." << std::endl;
329
    if (curr.size() > 1)
330
    {
331
      // all regions must be equal
332
      std::vector<Node> conc;
333
      bool foundLoopStart = false;
334
      for (const Node& cc : curr)
335
      {
336
        if (cc == eqc)
337
        {
338
          foundLoopStart = true;
339
        }
340
        else if (foundLoopStart && eqc != cc)
341
        {
342
          conc.push_back(eqc.eqNode(cc));
343
        }
344
      }
345
      Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(AND, conc);
346
      Trace("sets-cycle-debug")
347
          << "CYCLE: " << fact << " from " << exp << std::endl;
348
      d_im.assertInference(fact, InferenceId::SETS_CARD_CYCLE, exp);
349
      d_im.doPendingLemmas();
350
    }
351
    else
352
    {
353
      // should be guaranteed based on not exploring equal parents
354
      Assert(false);
355
    }
356
7277
    return;
357
  }
358
12833
  if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
359
  {
360
    // already processed
361
5289
    return;
362
  }
363
7544
  const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
364
7544
  if (nvsets.empty())
365
  {
366
    // no non-variable sets, trivial
367
1582
    d_oSetEqc.push_back(eqc);
368
1582
    return;
369
  }
370
5962
  curr.push_back(eqc);
371
11518
  TypeNode tn = eqc.getType();
372
5962
  bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
373
11518
  Node emp_set = d_treg.getEmptySet(tn);
374
15360
  for (const Node& n : nvsets)
375
  {
376
9804
    Kind nk = n.getKind();
377
9804
    if (nk != INTERSECTION && nk != SETMINUS)
378
    {
379
6911
      continue;
380
    }
381
14152
    Trace("sets-debug") << "Build cardinality parents for " << n << "..."
382
7076
                        << std::endl;
383
12291
    std::vector<Node> sib;
384
7076
    unsigned true_sib = 0;
385
7076
    if (n.getKind() == INTERSECTION)
386
    {
387
2648
      d_localBase[n] = n;
388
7944
      for (unsigned e = 0; e < 2; e++)
389
      {
390
10592
        Node sm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
391
5296
        sib.push_back(sm);
392
      }
393
2648
      true_sib = 2;
394
    }
395
    else
396
    {
397
8856
      Node si = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
398
4428
      sib.push_back(si);
399
4428
      d_localBase[n] = si;
400
8856
      Node osm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
401
4428
      sib.push_back(osm);
402
4428
      true_sib = 1;
403
    }
404
12291
    Node u = Rewriter::rewrite(nm->mkNode(UNION, n[0], n[1]));
405
7076
    if (!d_state.hasTerm(u))
406
    {
407
4494
      u = Node::null();
408
    }
409
7076
    unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
410
    // if this set is empty
411
7076
    if (is_empty)
412
    {
413
1632
      Assert(d_state.areEqual(n, emp_set));
414
1632
      Trace("sets-debug") << "  empty, parents equal siblings" << std::endl;
415
1632
      std::vector<Node> conc;
416
      // parent equal siblings
417
3625
      for (unsigned e = 0; e < true_sib; e++)
418
      {
419
1993
        if (d_state.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
420
        {
421
227
          conc.push_back(n[e].eqNode(sib[e]));
422
        }
423
      }
424
1632
      d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EMP, n.eqNode(emp_set));
425
1632
      d_im.doPendingLemmas();
426
1632
      if (d_im.hasSent())
427
      {
428
177
        return;
429
      }
430
      else
431
      {
432
        // justify why there is no edge to parents (necessary?)
433
3861
        for (unsigned e = 0; e < n_parents; e++)
434
        {
435
2406
          Node p = (e == true_sib) ? u : n[e];
436
        }
437
      }
438
1455
      continue;
439
    }
440
10659
    std::vector<Node> card_parents;
441
10659
    std::vector<int> card_parent_ids;
442
    // check if equal to a parent
443
14764
    for (unsigned e = 0; e < n_parents; e++)
444
    {
445
18862
      Trace("sets-debug") << "  check parent " << e << "/" << n_parents
446
9431
                          << std::endl;
447
9431
      bool is_union = e == true_sib;
448
18751
      Node p = (e == true_sib) ? u : n[e];
449
18862
      Trace("sets-debug") << "  check relation to parent " << p
450
9431
                          << ", isu=" << is_union << "..." << std::endl;
451
      // if parent is empty
452
9431
      if (d_state.areEqual(p, emp_set))
453
      {
454
        Trace("sets-debug") << "  it is empty..." << std::endl;
455
        Assert(!d_state.areEqual(n, emp_set));
456
        d_im.assertInference(
457
            n.eqNode(emp_set), InferenceId::SETS_CARD_GRAPH_EMP_PARENT, p.eqNode(emp_set));
458
        d_im.doPendingLemmas();
459
        if (d_im.hasSent())
460
        {
461
          return;
462
        }
463
        // if we are equal to a parent
464
      }
465
9431
      else if (d_state.areEqual(p, n))
466
      {
467
2245
        Trace("sets-debug") << "  it is equal to this..." << std::endl;
468
4379
        std::vector<Node> conc;
469
4379
        std::vector<int> sib_emp_indices;
470
2245
        if (is_union)
471
        {
472
90
          for (unsigned s = 0; s < sib.size(); s++)
473
          {
474
60
            sib_emp_indices.push_back(s);
475
          }
476
        }
477
        else
478
        {
479
2215
          sib_emp_indices.push_back(e);
480
        }
481
        // sibling(s) are empty
482
4520
        for (unsigned si : sib_emp_indices)
483
        {
484
2275
          if (!d_state.areEqual(sib[si], emp_set))
485
          {
486
111
            conc.push_back(sib[si].eqNode(emp_set));
487
          }
488
          else
489
          {
490
4328
            Trace("sets-debug")
491
2164
                << "Sibling " << sib[si] << " is already empty." << std::endl;
492
          }
493
        }
494
2245
        if (!is_union && nk == INTERSECTION && !u.isNull())
495
        {
496
          // union is equal to other parent
497
976
          if (!d_state.areEqual(u, n[1 - e]))
498
          {
499
            conc.push_back(u.eqNode(n[1 - e]));
500
          }
501
        }
502
4490
        Trace("sets-debug")
503
2245
            << "...derived " << conc.size() << " conclusions" << std::endl;
504
2245
        d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT, n.eqNode(p));
505
2245
        d_im.doPendingLemmas();
506
2245
        if (d_im.hasSent())
507
        {
508
111
          return;
509
        }
510
      }
511
      else
512
      {
513
7186
        Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
514
        // otherwise, we a syntactic subset of p
515
7186
        card_parents.push_back(p);
516
7186
        card_parent_ids.push_back(is_union ? 2 : e);
517
      }
518
    }
519
5333
    Assert(d_card_parent[n].empty());
520
5333
    Trace("sets-debug") << "get parent representatives..." << std::endl;
521
    // for each parent, take their representatives
522
12403
    for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
523
    {
524
14251
      Node cpk = card_parents[k];
525
14251
      Node eqcc = d_state.getRepresentative(cpk);
526
14362
      Trace("sets-debug") << "Check card parent " << k << "/"
527
7181
                          << card_parents.size() << std::endl;
528
529
      // if parent is singleton, then we should either be empty to equal to it
530
14251
      Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
531
7181
      if (!eqccSingleton.isNull())
532
      {
533
5
        bool eq_parent = false;
534
10
        std::vector<Node> exps;
535
5
        d_state.addEqualityToExp(cpk, eqccSingleton, exps);
536
5
        if (d_state.areDisequal(n, emp_set))
537
        {
538
          exps.push_back(n.eqNode(emp_set).negate());
539
          eq_parent = true;
540
        }
541
        else
542
        {
543
5
          const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
544
5
          if (!pmemsE.empty())
545
          {
546
10
            Node pmem = pmemsE.begin()->second;
547
5
            exps.push_back(pmem);
548
5
            d_state.addEqualityToExp(n, pmem[1], exps);
549
5
            eq_parent = true;
550
          }
551
        }
552
        // must be equal to parent
553
5
        if (eq_parent)
554
        {
555
10
          Node conc = n.eqNode(cpk);
556
5
          d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON, exps);
557
5
          d_im.doPendingLemmas();
558
        }
559
        else
560
        {
561
          // split on empty
562
          Trace("sets-nf") << "Split empty : " << n << std::endl;
563
          d_im.split(n.eqNode(emp_set), InferenceId::UNKNOWN, 1);
564
        }
565
5
        Assert(d_im.hasSent());
566
5
        return;
567
      }
568
      else
569
      {
570
7176
        bool dup = false;
571
9838
        for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++)
572
        {
573
3582
          Node cpnl = d_card_parent[n][l];
574
2768
          if (eqcc != cpnl)
575
          {
576
1112
            continue;
577
          }
578
3312
          Trace("sets-debug") << "  parents " << l << " and " << k
579
1656
                              << " are equal, ids = " << card_parent_ids[l]
580
1656
                              << " " << card_parent_ids[k] << std::endl;
581
1656
          dup = true;
582
1656
          if (n.getKind() != INTERSECTION)
583
          {
584
736
            continue;
585
          }
586
920
          Assert(card_parent_ids[l] != 2);
587
1734
          std::vector<Node> conc;
588
920
          if (card_parent_ids[k] == 2)
589
          {
590
            // intersection is equal to other parent
591
920
            unsigned pid = 1 - card_parent_ids[l];
592
920
            if (!d_state.areEqual(n[pid], n))
593
            {
594
212
              Trace("sets-debug")
595
106
                  << "  one of them is union, make equal to other..."
596
106
                  << std::endl;
597
106
              conc.push_back(n[pid].eqNode(n));
598
            }
599
          }
600
          else
601
          {
602
            if (!d_state.areEqual(cpk, n))
603
            {
604
              Trace("sets-debug")
605
                  << "  neither is union, make equal to one parent..."
606
                  << std::endl;
607
              // intersection is equal to one of the parents
608
              conc.push_back(cpk.eqNode(n));
609
            }
610
          }
611
920
          d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2, cpk.eqNode(cpnl));
612
920
          d_im.doPendingLemmas();
613
920
          if (d_im.hasSent())
614
          {
615
106
            return;
616
          }
617
        }
618
7070
        if (!dup)
619
        {
620
5520
          d_card_parent[n].push_back(eqcc);
621
        }
622
      }
623
    }
624
    // now recurse on parents (to ensure their normal will be computed after
625
    // this eqc)
626
5222
    exp.push_back(eqc.eqNode(n));
627
10518
    for (const Node& cpnc : d_card_parent[n])
628
    {
629
10606
      Trace("sets-cycle-debug")
630
5303
          << "Traverse card parent " << eqc << " -> " << cpnc << std::endl;
631
5303
      checkCardCyclesRec(cpnc, curr, exp);
632
5303
      if (d_im.hasSent())
633
      {
634
7
        return;
635
      }
636
    }
637
5215
    exp.pop_back();
638
  }
639
5556
  curr.pop_back();
640
  // parents now processed, can add to ordered list
641
5556
  d_oSetEqc.push_back(eqc);
642
}
643
644
553
void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
645
{
646
553
  Trace("sets") << "Check normal forms..." << std::endl;
647
  // now, build normal form for each equivalence class
648
  // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
649
  // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
650
553
  d_ff.clear();
651
553
  d_nf.clear();
652
2495
  for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
653
  {
654
2386
    checkNormalForm(d_oSetEqc[i], intro_sets);
655
2386
    if (d_im.hasSent() || !intro_sets.empty())
656
    {
657
444
      return;
658
    }
659
  }
660
109
  Trace("sets") << "Done check normal forms" << std::endl;
661
}
662
663
2386
void CardinalityExtension::checkNormalForm(Node eqc,
664
                                           std::vector<Node>& intro_sets)
665
{
666
3465
  TypeNode tn = eqc.getType();
667
2386
  Trace("sets") << "Compute normal form for " << eqc << std::endl;
668
2386
  Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
669
2386
  if (eqc == d_state.getEmptySetEqClass(tn))
670
  {
671
348
    d_nf[eqc].clear();
672
348
    Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
673
348
    return;
674
  }
675
  // flat/normal forms are sets of equivalence classes
676
3117
  Node base;
677
3117
  std::vector<Node> comps;
678
  std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
679
2038
      d_ff.find(eqc);
680
2038
  if (it != d_ff.end())
681
  {
682
650
    for (std::pair<const Node, std::vector<Node> >& itf : it->second)
683
    {
684
379
      std::sort(itf.second.begin(), itf.second.end());
685
379
      if (base.isNull())
686
      {
687
271
        base = itf.first;
688
      }
689
      else
690
      {
691
108
        comps.push_back(itf.first);
692
      }
693
758
      Trace("sets-nf") << "  F " << itf.first << " : " << itf.second
694
379
                       << std::endl;
695
379
      Trace("sets-nf-debug") << " ...";
696
379
      d_treg.debugPrintSet(itf.first, "sets-nf-debug");
697
379
      Trace("sets-nf-debug") << std::endl;
698
    }
699
  }
700
  else
701
  {
702
1767
    Trace("sets-nf") << "(no flat forms)" << std::endl;
703
  }
704
2038
  std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
705
2038
  Assert(d_nf.find(eqc) == d_nf.end());
706
2038
  std::vector<Node>& nfeqc = d_nf[eqc];
707
2038
  NodeManager* nm = NodeManager::currentNM();
708
2038
  bool success = true;
709
3117
  Node emp_set = d_treg.getEmptySet(tn);
710
2038
  if (!base.isNull())
711
  {
712
291
    for (unsigned j = 0, csize = comps.size(); j < csize; j++)
713
    {
714
      // compare if equal
715
128
      std::vector<Node> c;
716
108
      c.push_back(base);
717
108
      c.push_back(comps[j]);
718
324
      std::vector<Node> only[2];
719
128
      std::vector<Node> common;
720
216
      Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
721
108
                             << comps[j] << std::endl;
722
108
      unsigned k[2] = {0, 0};
723
1010
      while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
724
      {
725
451
        bool proc = true;
726
1353
        for (unsigned e = 0; e < 2; e++)
727
        {
728
902
          if (k[e] == ffeqc[c[e]].size())
729
          {
730
324
            for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
731
            {
732
92
              only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
733
            }
734
140
            proc = false;
735
          }
736
        }
737
451
        if (proc)
738
        {
739
363
          if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
740
          {
741
137
            common.push_back(ffeqc[c[0]][k[0]]);
742
137
            k[0]++;
743
137
            k[1]++;
744
          }
745
226
          else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
746
          {
747
121
            only[0].push_back(ffeqc[c[0]][k[0]]);
748
121
            k[0]++;
749
          }
750
          else
751
          {
752
105
            only[1].push_back(ffeqc[c[1]][k[1]]);
753
105
            k[1]++;
754
          }
755
        }
756
      }
757
108
      if (!only[0].empty() || !only[1].empty())
758
      {
759
88
        if (Trace.isOn("sets-nf-debug"))
760
        {
761
          Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
762
          for (unsigned e = 0; e < 2; e++)
763
          {
764
            Trace("sets-nf-debug") << "  " << c[e] << " : { ";
765
            for (unsigned l = 0; l < only[e].size(); l++)
766
            {
767
              if (l > 0)
768
              {
769
                Trace("sets-nf-debug") << ", ";
770
              }
771
              Trace("sets-nf-debug") << "[" << only[e][l] << "]";
772
            }
773
            Trace("sets-nf-debug") << " }" << std::endl;
774
          }
775
        }
776
        // try to make one empty, prefer the unique ones first
777
352
        for (unsigned e = 0; e < 3; e++)
778
        {
779
264
          unsigned sz = e == 2 ? common.size() : only[e].size();
780
661
          for (unsigned l = 0; l < sz; l++)
781
          {
782
794
            Node r = e == 2 ? common[l] : only[e][l];
783
397
            Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
784
397
            Trace("sets-nf-debug") << "         actual : ";
785
397
            d_treg.debugPrintSet(r, "sets-nf-debug");
786
397
            Trace("sets-nf-debug") << std::endl;
787
397
            Assert(!d_state.areEqual(r, emp_set));
788
397
            if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r))
789
            {
790
              // guess that its equal empty if it has no explicit members
791
              Trace("sets-nf") << " Split empty : " << r << std::endl;
792
              Trace("sets-nf") << "Actual Split : ";
793
              d_treg.debugPrintSet(r, "sets-nf");
794
              Trace("sets-nf") << std::endl;
795
              d_im.split(r.eqNode(emp_set), InferenceId::UNKNOWN, 1);
796
              Assert(d_im.hasSent());
797
              return;
798
            }
799
          }
800
        }
801
88
        for (const Node& o0 : only[0])
802
        {
803
124
          for (const Node& o1 : only[1])
804
          {
805
124
            bool disjoint = false;
806
248
            Trace("sets-nf-debug")
807
124
                << "Try split " << o0 << " against " << o1 << std::endl;
808
            // split them
809
319
            for (unsigned e = 0; e < 2; e++)
810
            {
811
426
              Node r1 = e == 0 ? o0 : o1;
812
426
              Node r2 = e == 0 ? o1 : o0;
813
              // check if their intersection exists modulo equality
814
426
              Node r1r2i = d_state.getBinaryOpTerm(INTERSECTION, r1, r2);
815
231
              if (!r1r2i.isNull())
816
              {
817
72
                Trace("sets-nf-debug")
818
                    << "Split term already exists, but not in cardinality "
819
36
                       "graph : "
820
36
                    << r1r2i << ", should be empty." << std::endl;
821
                // their intersection is empty (probably?)
822
                // e.g. these are two disjoint venn regions, proceed to next
823
                // pair
824
36
                Assert(d_state.areEqual(emp_set, r1r2i));
825
36
                disjoint = true;
826
36
                break;
827
              }
828
            }
829
124
            if (!disjoint)
830
            {
831
              // simply introduce their intersection
832
88
              Assert(o0 != o1);
833
176
              Node kca = d_treg.getProxy(o0);
834
176
              Node kcb = d_treg.getProxy(o1);
835
              Node intro =
836
176
                  Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
837
176
              Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
838
88
                               << ", term is " << intro << std::endl;
839
88
              intro_sets.push_back(intro);
840
88
              Assert(!d_state.hasTerm(intro));
841
88
              return;
842
            }
843
          }
844
        }
845
        // should never get here
846
        success = false;
847
      }
848
    }
849
183
    if (success)
850
    {
851
      // normal form is flat form of base
852
183
      nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
853
183
      Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
854
    }
855
    else
856
    {
857
      Trace("sets-nf") << "failed to build N " << eqc << std::endl;
858
    }
859
  }
860
  else
861
  {
862
    // must ensure disequal from empty
863
5258
    if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
864
4369
        && !d_state.hasMembers(eqc))
865
    {
866
356
      Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
867
356
      d_im.split(eqc.eqNode(emp_set), InferenceId::UNKNOWN);
868
356
      success = false;
869
    }
870
    else
871
    {
872
      // normal form is this equivalence class
873
1411
      nfeqc.push_back(eqc);
874
2822
      Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
875
1411
                       << std::endl;
876
    }
877
  }
878
1950
  if (!success)
879
  {
880
356
    Assert(d_im.hasSent());
881
356
    return;
882
  }
883
  // Send to parents (a parent is a set that contains a term in this equivalence
884
  // class as a direct child).
885
1594
  const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
886
1594
  if (nvsets.empty())
887
  {
888
    // no non-variable sets
889
515
    return;
890
  }
891
2158
  std::map<Node, std::map<Node, bool> > parents_proc;
892
2518
  for (const Node& n : nvsets)
893
  {
894
1439
    Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
895
1439
    if (d_card_parent[n].empty())
896
    {
897
      // nothing to do
898
366
      continue;
899
    }
900
1073
    Assert(d_localBase.find(n) != d_localBase.end());
901
2146
    Node cbase = d_localBase[n];
902
1073
    Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
903
2241
    for (const Node& p : d_card_parent[n])
904
    {
905
1168
      Trace("sets-nf-debug") << "Check parent " << p << std::endl;
906
1168
      if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
907
      {
908
        Trace("sets-nf-debug") << "..already processed parent " << p << " for "
909
                               << cbase << std::endl;
910
        continue;
911
      }
912
1168
      parents_proc[cbase][p] = true;
913
2336
      Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
914
1168
                             << "] ), from " << n << "..." << std::endl;
915
916
1168
      std::vector<Node>& ffpc = d_ff[p][cbase];
917
2505
      for (const Node& nfeqci : nfeqc)
918
      {
919
1337
        if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
920
        {
921
1168
          ffpc.insert(ffpc.end(), nfeqc.begin(), nfeqc.end());
922
        }
923
        else
924
        {
925
          // if it is a duplicate venn region, it must be empty since it is
926
          // coming from syntactically disjoint siblings
927
        }
928
      }
929
    }
930
  }
931
}
932
933
1363
void CardinalityExtension::checkMinCard()
934
{
935
1363
  NodeManager* nm = NodeManager::currentNM();
936
1363
  const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
937
15641
  for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
938
  {
939
22188
    Node eqc = setEqc[i];
940
22188
    TypeNode tn = eqc.getType().getSetElementType();
941
14278
    if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
942
    {
943
      // cardinality is not enabled for this type, skip
944
120
      continue;
945
    }
946
    // get members in class
947
14158
    const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
948
14158
    if (pmemsE.empty())
949
    {
950
      // no members, trivial
951
6248
      continue;
952
    }
953
15820
    std::vector<Node> exp;
954
15820
    std::vector<Node> members;
955
15820
    Node cardTerm;
956
7910
    std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
957
7910
    if (it != d_eqc_to_card_term.end())
958
    {
959
7908
      cardTerm = it->second;
960
    }
961
    else
962
    {
963
2
      cardTerm = nm->mkNode(CARD, eqc);
964
    }
965
20448
    for (const std::pair<const Node, Node>& itmm : pmemsE)
966
    {
967
12538
      members.push_back(itmm.first);
968
12538
      exp.push_back(nm->mkNode(MEMBER, itmm.first, cardTerm[0]));
969
    }
970
7910
    if (members.size() > 1)
971
    {
972
2820
      exp.push_back(nm->mkNode(DISTINCT, members));
973
    }
974
7910
    if (!members.empty())
975
    {
976
      Node conc =
977
15820
          nm->mkNode(GEQ, cardTerm, nm->mkConst(Rational(members.size())));
978
15820
      Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
979
7910
      d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1);
980
    }
981
  }
982
  // flush the lemmas
983
1363
  d_im.doPendingLemmas();
984
1363
}
985
986
379
bool CardinalityExtension::isModelValueBasic(Node eqc)
987
{
988
379
  return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
989
}
990
991
167
void CardinalityExtension::mkModelValueElementsFor(
992
    Valuation& val,
993
    Node eqc,
994
    std::vector<Node>& els,
995
    const std::map<Node, Node>& mvals,
996
    TheoryModel* model)
997
{
998
334
  TypeNode elementType = eqc.getType().getSetElementType();
999
167
  if (isModelValueBasic(eqc))
1000
  {
1001
112
    std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
1002
112
    if (it != d_eqc_to_card_term.end())
1003
    {
1004
      // slack elements from cardinality value
1005
202
      Node v = val.getModelValue(it->second);
1006
202
      Trace("sets-model") << "Cardinality of " << eqc << " is " << v
1007
101
                          << std::endl;
1008
101
      if (v.getConst<Rational>() > UINT32_MAX)
1009
      {
1010
        std::stringstream ss;
1011
        ss << "The model for " << eqc << " was computed to have cardinality "
1012
           << v << ". We only allow sets up to cardinality " << UINT32_MAX;
1013
        throw LogicException(ss.str());
1014
      }
1015
101
      std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
1016
101
      Assert(els.size() <= vu);
1017
101
      NodeManager* nm = NodeManager::currentNM();
1018
101
      if (elementType.isInterpretedFinite())
1019
      {
1020
        // get all members of this finite type
1021
20
        collectFiniteTypeSetElements(model);
1022
      }
1023
259
      while (els.size() < vu)
1024
      {
1025
79
        if (elementType.isInterpretedFinite())
1026
        {
1027
          // At this point we are sure the formula is satisfiable and all
1028
          // cardinality constraints are satisfied. Since this type is finite,
1029
          // there is only one single cardinality graph for all sets of this
1030
          // type because the universe cardinality constraint has been added by
1031
          // CardinalityExtension::checkCardinalityExtended. This means we have
1032
          // enough slack elements of this finite type for all disjoint leaves
1033
          // in the cardinality graph. Therefore we can safely add new distinct
1034
          // slack elements for the leaves without worrying about conflicts with
1035
          // the current members of this finite type.
1036
1037
86
          Node slack = nm->mkSkolem("slack", elementType);
1038
86
          Node singleton = nm->mkSingleton(elementType, slack);
1039
43
          els.push_back(singleton);
1040
43
          d_finite_type_slack_elements[elementType].push_back(slack);
1041
86
          Trace("sets-model") << "Added slack element " << slack << " to set "
1042
43
                              << eqc << std::endl;
1043
        }
1044
        else
1045
        {
1046
36
          els.push_back(
1047
72
              nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
1048
        }
1049
      }
1050
    }
1051
    else
1052
    {
1053
11
      Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1054
    }
1055
  }
1056
  else
1057
  {
1058
110
    Trace("sets-model") << "Build value for " << eqc
1059
110
                        << " based on normal form, size = " << d_nf[eqc].size()
1060
55
                        << std::endl;
1061
    // it is union of venn regions
1062
102
    for (unsigned j = 0; j < d_nf[eqc].size(); j++)
1063
    {
1064
47
      std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
1065
47
      if (itm != mvals.end())
1066
      {
1067
47
        els.push_back(itm->second);
1068
      }
1069
      else
1070
      {
1071
        Assert(false);
1072
      }
1073
    }
1074
  }
1075
167
}
1076
1077
20
void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
1078
{
1079
20
  if (d_finite_type_constants_processed)
1080
  {
1081
10
    return;
1082
  }
1083
55
  for (const Node& set : getOrderedSetsEqClasses())
1084
  {
1085
45
    if (!set.getType().isInterpretedFinite())
1086
    {
1087
      continue;
1088
    }
1089
45
    if (!isModelValueBasic(set))
1090
    {
1091
      // only consider leaves in the cardinality graph
1092
25
      continue;
1093
    }
1094
42
    for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
1095
    {
1096
44
      Node member = pair.first;
1097
44
      Node modelRepresentative = model->getRepresentative(member);
1098
22
      std::vector<Node>& elements = d_finite_type_elements[member.getType()];
1099
66
      if (std::find(elements.begin(), elements.end(), modelRepresentative)
1100
66
          == elements.end())
1101
      {
1102
22
        elements.push_back(modelRepresentative);
1103
      }
1104
    }
1105
  }
1106
10
  d_finite_type_constants_processed = true;
1107
}
1108
1109
8
const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
1110
    TypeNode typeNode)
1111
{
1112
8
  return d_finite_type_elements[typeNode];
1113
}
1114
1115
}  // namespace sets
1116
}  // namespace theory
1117
26676
}  // namespace CVC4