GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/solver_state.cpp Lines: 272 293 92.8 %
Date: 2021-03-22 Branches: 570 1220 46.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solver_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed, Paul Meng
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of sets state object
13
 **/
14
15
#include "theory/sets/solver_state.h"
16
17
#include "expr/emptyset.h"
18
#include "options/sets_options.h"
19
#include "theory/sets/theory_sets_private.h"
20
21
using namespace std;
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace sets {
27
28
8995
SolverState::SolverState(context::Context* c,
29
                         context::UserContext* u,
30
                         Valuation val,
31
8995
                         SkolemCache& skc)
32
8995
    : TheoryState(c, u, val), d_skCache(skc), d_members(c)
33
{
34
8995
  d_true = NodeManager::currentNM()->mkConst(true);
35
8995
  d_false = NodeManager::currentNM()->mkConst(false);
36
8995
}
37
38
28371
void SolverState::reset()
39
{
40
28371
  d_set_eqc.clear();
41
28371
  d_eqc_emptyset.clear();
42
28371
  d_eqc_univset.clear();
43
28371
  d_eqc_singleton.clear();
44
28371
  d_congruent.clear();
45
28371
  d_nvar_sets.clear();
46
28371
  d_var_set.clear();
47
28371
  d_compSets.clear();
48
28371
  d_pol_mems[0].clear();
49
28371
  d_pol_mems[1].clear();
50
28371
  d_members_index.clear();
51
28371
  d_singleton_index.clear();
52
28371
  d_bop_index.clear();
53
28371
  d_op_list.clear();
54
28371
  d_allCompSets.clear();
55
28371
}
56
57
148581
void SolverState::registerEqc(TypeNode tn, Node r)
58
{
59
148581
  if (tn.isSet())
60
  {
61
53584
    d_set_eqc.push_back(r);
62
  }
63
148581
}
64
65
493176
void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
66
{
67
493176
  Kind nk = n.getKind();
68
493176
  if (nk == MEMBER)
69
  {
70
112336
    if (r.isConst())
71
    {
72
212610
      Node s = d_ee->getRepresentative(n[1]);
73
212610
      Node x = d_ee->getRepresentative(n[0]);
74
106305
      int pindex = r == d_true ? 0 : (r == d_false ? 1 : -1);
75
106305
      if (pindex != -1)
76
      {
77
106305
        if (d_pol_mems[pindex][s].find(x) == d_pol_mems[pindex][s].end())
78
        {
79
80559
          d_pol_mems[pindex][s][x] = n;
80
161118
          Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n
81
80559
                               << ", pindex = " << pindex << std::endl;
82
        }
83
106305
        if (d_members_index[s].find(x) == d_members_index[s].end())
84
        {
85
80559
          d_members_index[s][x] = n;
86
80559
          d_op_list[MEMBER].push_back(n);
87
        }
88
      }
89
      else
90
      {
91
        Assert(false);
92
      }
93
    }
94
  }
95
380840
  else if (nk == SINGLETON || nk == UNION || nk == INTERSECTION
96
343474
           || nk == SETMINUS || nk == EMPTYSET || nk == UNIVERSE_SET)
97
  {
98
62224
    if (nk == SINGLETON)
99
    {
100
23502
      Node re = d_ee->getRepresentative(n[0]);
101
11751
      if (d_singleton_index.find(re) == d_singleton_index.end())
102
      {
103
9688
        d_singleton_index[re] = n;
104
9688
        d_eqc_singleton[r] = n;
105
9688
        d_op_list[SINGLETON].push_back(n);
106
      }
107
      else
108
      {
109
2063
        d_congruent[n] = d_singleton_index[re];
110
      }
111
    }
112
50473
    else if (nk == EMPTYSET)
113
    {
114
3588
      d_eqc_emptyset[tnn] = r;
115
    }
116
46885
    else if (nk == UNIVERSE_SET)
117
    {
118
19201
      Assert(options::setsExt());
119
1748
      d_eqc_univset[tnn] = r;
120
    }
121
    else
122
    {
123
90274
      Node r1 = d_ee->getRepresentative(n[0]);
124
90274
      Node r2 = d_ee->getRepresentative(n[1]);
125
45137
      std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
126
45137
      std::map<Node, Node>::iterator itb = binr1.find(r2);
127
45137
      if (itb == binr1.end())
128
      {
129
43106
        binr1[r2] = n;
130
43106
        d_op_list[nk].push_back(n);
131
      }
132
      else
133
      {
134
2031
        d_congruent[n] = itb->second;
135
      }
136
    }
137
62224
    d_nvar_sets[r].push_back(n);
138
62224
    Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
139
  }
140
318616
  else if (nk == COMPREHENSION)
141
  {
142
124
    d_compSets[r].push_back(n);
143
124
    d_allCompSets.push_back(n);
144
124
    Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
145
  }
146
318492
  else if (n.isVar() && !d_skCache.isSkolem(n))
147
  {
148
    // it is important that we check it is a variable, but not an internally
149
    // introduced skolem, due to the semantics of the universe set.
150
28182
    if (tnn.isSet())
151
    {
152
19947
      if (d_var_set.find(r) == d_var_set.end())
153
      {
154
18495
        d_var_set[r] = n;
155
18495
        Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
156
      }
157
    }
158
  }
159
  else
160
  {
161
290310
    Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
162
  }
163
493176
}
164
165
62513
void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
166
{
167
62513
  if (a != b)
168
  {
169
18214
    Assert(areEqual(a, b));
170
18214
    exp.push_back(a.eqNode(b));
171
  }
172
62513
}
173
174
16509
Node SolverState::getEmptySetEqClass(TypeNode tn) const
175
{
176
16509
  std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
177
16509
  if (it != d_eqc_emptyset.end())
178
  {
179
15500
    return it->second;
180
  }
181
1009
  return Node::null();
182
}
183
184
3466
Node SolverState::getUnivSetEqClass(TypeNode tn) const
185
{
186
3466
  std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
187
3466
  if (it != d_eqc_univset.end())
188
  {
189
2678
    return it->second;
190
  }
191
788
  return Node::null();
192
}
193
194
7181
Node SolverState::getSingletonEqClass(Node r) const
195
{
196
7181
  std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
197
7181
  if (it != d_eqc_singleton.end())
198
  {
199
5
    return it->second;
200
  }
201
7176
  return Node::null();
202
}
203
204
231
Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
205
{
206
  std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
207
231
      d_bop_index.find(k);
208
231
  if (itk == d_bop_index.end())
209
  {
210
    return Node::null();
211
  }
212
  std::map<Node, std::map<Node, Node> >::const_iterator it1 =
213
231
      itk->second.find(r1);
214
231
  if (it1 == itk->second.end())
215
  {
216
134
    return Node::null();
217
  }
218
97
  std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
219
97
  if (it2 == it1->second.end())
220
  {
221
61
    return Node::null();
222
  }
223
36
  return it2->second;
224
}
225
226
283189
bool SolverState::isEntailed(Node n, bool polarity) const
227
{
228
283189
  if (n.getKind() == NOT)
229
  {
230
14460
    return isEntailed(n[0], !polarity);
231
  }
232
268729
  else if (n.getKind() == EQUAL)
233
  {
234
15533
    if (polarity)
235
    {
236
14835
      return areEqual(n[0], n[1]);
237
    }
238
698
    return areDisequal(n[0], n[1]);
239
  }
240
253196
  else if (n.getKind() == MEMBER)
241
  {
242
164963
    if (areEqual(n, polarity ? d_true : d_false))
243
    {
244
133900
      return true;
245
    }
246
    // check members cache
247
31063
    if (polarity && d_ee->hasTerm(n[1]))
248
    {
249
50935
      Node r = d_ee->getRepresentative(n[1]);
250
30206
      if (isMember(n[0], r))
251
      {
252
9477
        return true;
253
      }
254
    }
255
  }
256
88233
  else if (n.getKind() == AND || n.getKind() == OR)
257
  {
258
62060
    bool conj = (n.getKind() == AND) == polarity;
259
174194
    for (const Node& nc : n)
260
    {
261
125632
      bool isEnt = isEntailed(nc, polarity);
262
125632
      if (isEnt != conj)
263
      {
264
13498
        return !conj;
265
      }
266
    }
267
48562
    return conj;
268
  }
269
26173
  else if (n.isConst())
270
  {
271
14489
    return (polarity && n == d_true) || (!polarity && n == d_false);
272
  }
273
33270
  return false;
274
}
275
276
8161
bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
277
{
278
8161
  Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
279
8161
  Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
280
16322
  TypeNode tn = r1.getType();
281
16322
  Node re = getEmptySetEqClass(tn);
282
10678
  for (unsigned e = 0; e < 2; e++)
283
  {
284
12557
    Node a = e == 0 ? r1 : r2;
285
12557
    Node b = e == 0 ? r2 : r1;
286
10040
    if (isSetDisequalityEntailedInternal(a, b, re))
287
    {
288
7523
      return true;
289
    }
290
  }
291
638
  return false;
292
}
293
294
10040
bool SolverState::isSetDisequalityEntailedInternal(Node a,
295
                                                   Node b,
296
                                                   Node re) const
297
{
298
  // if there are members in a
299
  std::map<Node, std::map<Node, Node> >::const_iterator itpma =
300
10040
      d_pol_mems[0].find(a);
301
10040
  if (itpma == d_pol_mems[0].end())
302
  {
303
    // no positive members, continue
304
1586
    return false;
305
  }
306
  // if b is empty
307
8454
  if (b == re)
308
  {
309
2180
    if (!itpma->second.empty())
310
    {
311
4360
      Trace("sets-deq") << "Disequality is satisfied because members are in "
312
2180
                        << a << " and " << b << " is empty" << std::endl;
313
2180
      return true;
314
    }
315
    else
316
    {
317
      // a should not be singleton
318
      Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
319
    }
320
    return false;
321
  }
322
6274
  std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
323
  std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
324
6274
      d_pol_mems[1].find(b);
325
12548
  std::vector<Node> prev;
326
8492
  for (const std::pair<const Node, Node>& itm : itpma->second)
327
  {
328
    // if b is a singleton
329
7561
    if (itsb != d_eqc_singleton.end())
330
    {
331
5372
      if (areDisequal(itm.first, itsb->second[0]))
332
      {
333
9444
        Trace("sets-deq") << "Disequality is satisfied because of "
334
9444
                          << itm.second << ", singleton eq " << itsb->second[0]
335
4722
                          << std::endl;
336
10065
        return true;
337
      }
338
      // or disequal with another member
339
685
      for (const Node& p : prev)
340
      {
341
35
        if (areDisequal(itm.first, p))
342
        {
343
          Trace("sets-deq")
344
              << "Disequality is satisfied because of disequal members "
345
              << itm.first << " " << p << ", singleton eq " << std::endl;
346
          return true;
347
        }
348
      }
349
      // if a has positive member that is negative member in b
350
    }
351
2189
    else if (itpmb != d_pol_mems[1].end())
352
    {
353
2288
      for (const std::pair<const Node, Node>& itnm : itpmb->second)
354
      {
355
1626
        if (areEqual(itm.first, itnm.first))
356
        {
357
1242
          Trace("sets-deq") << "Disequality is satisfied because of "
358
621
                            << itm.second << " " << itnm.second << std::endl;
359
621
          return true;
360
        }
361
      }
362
    }
363
2218
    prev.push_back(itm.first);
364
  }
365
931
  return false;
366
}
367
368
Node SolverState::getCongruent(Node n) const
369
{
370
  Assert(d_ee->hasTerm(n));
371
  std::map<Node, Node>::const_iterator it = d_congruent.find(n);
372
  if (it == d_congruent.end())
373
  {
374
    return n;
375
  }
376
  return it->second;
377
}
378
79149
bool SolverState::isCongruent(Node n) const
379
{
380
79149
  return d_congruent.find(n) != d_congruent.end();
381
}
382
74593
const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
383
{
384
74593
  std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
385
74593
  if (it == d_nvar_sets.end())
386
  {
387
17413
    return d_emptyVec;
388
  }
389
57180
  return it->second;
390
}
391
392
20463
Node SolverState::getVariableSet(Node r) const
393
{
394
20463
  std::map<Node, Node>::const_iterator it = d_var_set.find(r);
395
20463
  if (it != d_var_set.end())
396
  {
397
5933
    return it->second;
398
  }
399
14530
  return Node::null();
400
}
401
402
const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
403
{
404
  std::map<Node, std::vector<Node> >::const_iterator it = d_compSets.find(r);
405
  if (it == d_compSets.end())
406
  {
407
    return d_emptyVec;
408
  }
409
  return it->second;
410
}
411
412
112433
const std::map<Node, Node>& SolverState::getMembers(Node r) const
413
{
414
112433
  return getMembersInternal(r, 0);
415
}
416
30264
const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
417
{
418
30264
  return getMembersInternal(r, 1);
419
}
420
142697
const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
421
                                                            unsigned i) const
422
{
423
  std::map<Node, std::map<Node, Node> >::const_iterator itp =
424
142697
      d_pol_mems[i].find(r);
425
142697
  if (itp == d_pol_mems[i].end())
426
  {
427
43621
    return d_emptyMap;
428
  }
429
99076
  return itp->second;
430
}
431
432
1043
bool SolverState::hasMembers(Node r) const
433
{
434
  std::map<Node, std::map<Node, Node> >::const_iterator it =
435
1043
      d_pol_mems[0].find(r);
436
1043
  if (it == d_pol_mems[0].end())
437
  {
438
356
    return false;
439
  }
440
687
  return !it->second.empty();
441
}
442
const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
443
15008
SolverState::getBinaryOpIndex() const
444
{
445
15008
  return d_bop_index;
446
}
447
448
const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
449
    Kind k)
450
{
451
  return d_bop_index[k];
452
}
453
454
5913
const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
455
{
456
5913
  return d_op_list;
457
}
458
459
13364
const std::vector<Node>& SolverState::getComprehensionSets() const
460
{
461
13364
  return d_allCompSets;
462
}
463
464
954
const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
465
{
466
954
  vector<Node> representatives;
467
9554
  for (const Node& eqc : getSetsEqClasses())
468
  {
469
8600
    if (eqc.getType().getSetElementType() == t)
470
    {
471
8600
      representatives.push_back(eqc);
472
    }
473
  }
474
954
  return representatives;
475
}
476
477
70153
bool SolverState::isMember(TNode x, TNode s) const
478
{
479
70153
  Assert(hasTerm(s) && getRepresentative(s) == s);
480
70153
  NodeIntMap::const_iterator mem_i = d_members.find(s);
481
70153
  if (mem_i != d_members.end())
482
  {
483
    std::map<Node, std::vector<Node> >::const_iterator itd =
484
53374
        d_members_data.find(s);
485
53374
    Assert(itd != d_members_data.end());
486
53374
    const std::vector<Node>& members = itd->second;
487
53374
    Assert((*mem_i).second <= members.size());
488
111144
    for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
489
    {
490
104217
      if (areEqual(members[i][0], x))
491
      {
492
46447
        return true;
493
      }
494
    }
495
  }
496
23706
  return false;
497
}
498
499
29301
void SolverState::addMember(TNode r, TNode atom)
500
{
501
29301
  NodeIntMap::iterator mem_i = d_members.find(r);
502
29301
  size_t n_members = 0;
503
29301
  if (mem_i != d_members.end())
504
  {
505
18711
    n_members = (*mem_i).second;
506
  }
507
29301
  d_members[r] = n_members + 1;
508
29301
  if (n_members < d_members_data[r].size())
509
  {
510
19549
    d_members_data[r][n_members] = atom;
511
  }
512
  else
513
  {
514
9752
    d_members_data[r].push_back(atom);
515
  }
516
29301
}
517
518
114680
bool SolverState::merge(TNode t1,
519
                        TNode t2,
520
                        std::vector<Node>& facts,
521
                        TNode cset)
522
{
523
114680
  NodeIntMap::iterator mem_i2 = d_members.find(t2);
524
114680
  if (mem_i2 == d_members.end())
525
  {
526
    // no members in t2, we are done
527
111510
    return true;
528
  }
529
3170
  NodeIntMap::iterator mem_i1 = d_members.find(t1);
530
3170
  size_t n_members = 0;
531
3170
  if (mem_i1 != d_members.end())
532
  {
533
2868
    n_members = (*mem_i1).second;
534
  }
535
7139
  for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
536
  {
537
4060
    Assert(i < d_members_data[t2].size()
538
           && d_members_data[t2][i].getKind() == MEMBER);
539
8029
    Node m2 = d_members_data[t2][i];
540
    // check if redundant
541
4060
    bool add = true;
542
6341
    for (size_t j = 0; j < n_members; j++)
543
    {
544
5679
      Assert(j < d_members_data[t1].size()
545
             && d_members_data[t1][j].getKind() == MEMBER);
546
5679
      if (areEqual(m2[0], d_members_data[t1][j][0]))
547
      {
548
3398
        add = false;
549
3398
        break;
550
      }
551
    }
552
4060
    if (add)
553
    {
554
      // if there is a concrete set in t1, propagate new facts or conflicts
555
662
      if (!cset.isNull())
556
      {
557
215
        NodeManager* nm = NodeManager::currentNM();
558
215
        Assert(areEqual(m2[1], cset));
559
339
        Node exp = nm->mkNode(AND, m2[1].eqNode(cset), m2);
560
215
        if (cset.getKind() == SINGLETON)
561
        {
562
124
          if (cset[0] != m2[0])
563
          {
564
248
            Node eq = cset[0].eqNode(m2[0]);
565
248
            Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
566
124
                               << " => " << eq << std::endl;
567
248
            Node fact = nm->mkNode(IMPLIES, exp, eq);
568
124
            facts.push_back(fact);
569
          }
570
        }
571
        else
572
        {
573
          // conflict
574
91
          Assert(facts.empty());
575
182
          Trace("sets-prop")
576
91
              << "Propagate eq-mem conflict : " << exp << std::endl;
577
91
          facts.push_back(exp);
578
91
          return false;
579
        }
580
      }
581
571
      if (n_members < d_members_data[t1].size())
582
      {
583
439
        d_members_data[t1][n_members] = m2;
584
      }
585
      else
586
      {
587
132
        d_members_data[t1].push_back(m2);
588
      }
589
571
      n_members++;
590
    }
591
  }
592
3079
  d_members[t1] = n_members;
593
3079
  return true;
594
}
595
596
}  // namespace sets
597
}  // namespace theory
598
26676
}  // namespace CVC4