GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/base_solver.cpp Lines: 297 378 78.6 %
Date: 2021-03-23 Branches: 625 1593 39.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file base_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Tianyi Liang
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 Base solver for the theory of strings. This class implements term
13
 ** indexing and constant inference for the theory of strings.
14
 **/
15
16
#include "theory/strings/base_solver.h"
17
18
#include "expr/sequence.h"
19
#include "options/strings_options.h"
20
#include "theory/rewriter.h"
21
#include "theory/strings/theory_strings_utils.h"
22
#include "theory/strings/word.h"
23
24
using namespace std;
25
using namespace CVC4::context;
26
using namespace CVC4::kind;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace strings {
31
32
8997
BaseSolver::BaseSolver(SolverState& s, InferenceManager& im)
33
8997
    : d_state(s), d_im(im), d_congruent(s.getSatContext())
34
{
35
8997
  d_false = NodeManager::currentNM()->mkConst(false);
36
8997
  d_cardSize = utils::getAlphabetCardinality();
37
8997
}
38
39
8994
BaseSolver::~BaseSolver() {}
40
41
25158
void BaseSolver::checkInit()
42
{
43
  // build term index
44
25158
  d_eqcInfo.clear();
45
25158
  d_termIndex.clear();
46
25158
  d_stringsEqc.clear();
47
48
25158
  Trace("strings-base") << "BaseSolver::checkInit" << std::endl;
49
  // count of congruent, non-congruent per operator (independent of type),
50
  // for debugging.
51
50316
  std::map<Kind, std::pair<uint32_t, uint32_t>> congruentCount;
52
25158
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
53
25158
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
54
2254142
  while (!eqcs_i.isFinished())
55
  {
56
2228984
    Node eqc = (*eqcs_i);
57
2228984
    TypeNode tn = eqc.getType();
58
1114492
    if (!tn.isRegExp())
59
    {
60
2146692
      Node emps;
61
      // get the term index for type tn
62
1073346
      std::map<Kind, TermIndex>& tti = d_termIndex[tn];
63
1073346
      if (tn.isStringLike())
64
      {
65
456622
        d_stringsEqc.push_back(eqc);
66
456622
        emps = Word::mkEmptyWord(tn);
67
      }
68
2146692
      Node var;
69
1073346
      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
70
14365570
      while (!eqc_i.isFinished())
71
      {
72
13292224
        Node n = *eqc_i;
73
6646112
        Kind k = n.getKind();
74
6646112
        Trace("strings-base") << "initialize term: " << n << std::endl;
75
        // process constant-like terms
76
6646112
        if (utils::isConstantLike(n))
77
        {
78
692916
          Node prev = d_eqcInfo[eqc].d_bestContent;
79
346458
          if (!prev.isNull())
80
          {
81
            // we have either (seq.unit x) = C, or (seq.unit x) = (seq.unit y)
82
            // where C is a sequence constant.
83
            Node cval =
84
316
                prev.isConst() ? prev : (n.isConst() ? n : Node::null());
85
316
            std::vector<Node> exp;
86
158
            exp.push_back(prev.eqNode(n));
87
316
            Node s, t;
88
158
            if (cval.isNull())
89
            {
90
              // injectivity of seq.unit
91
32
              s = prev[0];
92
32
              t = n[0];
93
            }
94
            else
95
            {
96
              // should not have two constants in the same equivalence class
97
126
              Assert(cval.getType().isSequence());
98
252
              std::vector<Node> cchars = Word::getChars(cval);
99
126
              if (cchars.size() == 1)
100
              {
101
252
                Node oval = prev.isConst() ? n : prev;
102
126
                Assert(oval.getKind() == SEQ_UNIT);
103
126
                s = oval[0];
104
126
                t = cchars[0].getConst<Sequence>().getVec()[0];
105
                // oval is congruent (ignored) in this context
106
126
                d_congruent.insert(oval);
107
              }
108
              else
109
              {
110
                // (seq.unit x) = C => false if |C| != 1.
111
                d_im.sendInference(
112
                    exp, d_false, InferenceId::STRINGS_UNIT_CONST_CONFLICT);
113
                return;
114
              }
115
            }
116
158
            if (!d_state.areEqual(s, t))
117
            {
118
              // (seq.unit x) = (seq.unit y) => x=y, or
119
              // (seq.unit x) = (seq.unit c) => x=c
120
40
              Assert(s.getType() == t.getType());
121
40
              d_im.sendInference(exp, s.eqNode(t), InferenceId::STRINGS_UNIT_INJ);
122
            }
123
          }
124
          // update best content
125
346458
          if (prev.isNull() || n.isConst())
126
          {
127
346300
            d_eqcInfo[eqc].d_bestContent = n;
128
346300
            d_eqcInfo[eqc].d_bestScore = 0;
129
346300
            d_eqcInfo[eqc].d_base = n;
130
346300
            d_eqcInfo[eqc].d_exp = Node::null();
131
          }
132
        }
133
6646112
        if (tn.isInteger())
134
        {
135
          // do nothing
136
        }
137
        // process indexing
138
5056014
        else if (n.getNumChildren() > 0)
139
        {
140
3658858
          if (k != EQUAL)
141
          {
142
758819
            if (d_congruent.find(n) == d_congruent.end())
143
            {
144
1238722
              std::vector<Node> c;
145
1238722
              Node nc = tti[k].add(n, 0, d_state, emps, c);
146
619361
              if (nc != n)
147
              {
148
96612
                Trace("strings-base-debug")
149
48306
                    << "...found congruent term " << nc << std::endl;
150
                // check if we have inferred a new equality by removal of empty
151
                // components
152
48306
                if (k == STRING_CONCAT && !d_state.areEqual(nc, n))
153
                {
154
2144
                  std::vector<Node> exp;
155
                  // the number of empty components of n, nc
156
1072
                  size_t count[2] = {0, 0};
157
6944
                  while (count[0] < nc.getNumChildren()
158
4008
                         || count[1] < n.getNumChildren())
159
                  {
160
                    // explain empty prefixes
161
8808
                    for (unsigned t = 0; t < 2; t++)
162
                    {
163
11744
                      Node nn = t == 0 ? nc : n;
164
9006
                      while (count[t] < nn.getNumChildren()
165
23884
                             && (nn[count[t]] == emps
166
12876
                                 || d_state.areEqual(nn[count[t]], emps)))
167
                      {
168
1567
                        if (nn[count[t]] != emps)
169
                        {
170
1567
                          exp.push_back(nn[count[t]].eqNode(emps));
171
                        }
172
1567
                        count[t]++;
173
                      }
174
                    }
175
5872
                    Trace("strings-base-debug")
176
2936
                        << "  counts = " << count[0] << ", " << count[1]
177
2936
                        << std::endl;
178
                    // explain equal components
179
2936
                    if (count[0] < nc.getNumChildren())
180
                    {
181
1935
                      Assert(count[1] < n.getNumChildren());
182
1935
                      if (nc[count[0]] != n[count[1]])
183
                      {
184
79
                        exp.push_back(nc[count[0]].eqNode(n[count[1]]));
185
                      }
186
1935
                      count[0]++;
187
1935
                      count[1]++;
188
                    }
189
                  }
190
                  // infer the equality
191
1072
                  d_im.sendInference(exp, n.eqNode(nc), InferenceId::STRINGS_I_NORM);
192
                }
193
                else
194
                {
195
                  // We cannot mark one of the terms as reduced here (via
196
                  // ExtTheory::markCongruent) since extended function terms
197
                  // rely on reductions to other extended function terms. We
198
                  // may have a pair of extended function terms f(a)=f(b) where
199
                  // the reduction of argument a depends on the term b.
200
                  // Thus, marking f(b) as reduced by virtue of the fact we
201
                  // have f(a) is incorrect, since then we are effectively
202
                  // assuming that the reduction of f(a) depends on itself.
203
                }
204
                // this node is congruent to another one, we can ignore it
205
96612
                Trace("strings-base-debug")
206
48306
                    << "  congruent term : " << n << " (via " << nc << ")"
207
48306
                    << std::endl;
208
48306
                d_congruent.insert(n);
209
48306
                congruentCount[k].first++;
210
              }
211
571055
              else if (k == STRING_CONCAT && c.size() == 1)
212
              {
213
33032
                Trace("strings-base-debug")
214
16516
                    << "  congruent term by singular : " << n << " " << c[0]
215
16516
                    << std::endl;
216
                // singular case
217
16516
                if (!d_state.areEqual(c[0], n))
218
                {
219
8850
                  Node ns;
220
8850
                  std::vector<Node> exp;
221
                  // explain empty components
222
4425
                  bool foundNEmpty = false;
223
14188
                  for (const Node& nnc : n)
224
                  {
225
9763
                    if (d_state.areEqual(nnc, emps))
226
                    {
227
5338
                      if (nnc != emps)
228
                      {
229
5338
                        exp.push_back(nnc.eqNode(emps));
230
                      }
231
                    }
232
                    else
233
                    {
234
4425
                      Assert(!foundNEmpty);
235
4425
                      ns = nnc;
236
4425
                      foundNEmpty = true;
237
                    }
238
                  }
239
4425
                  AlwaysAssert(foundNEmpty);
240
                  // infer the equality
241
4425
                  d_im.sendInference(exp, n.eqNode(ns), InferenceId::STRINGS_I_NORM_S);
242
                }
243
16516
                d_congruent.insert(n);
244
16516
                congruentCount[k].first++;
245
              }
246
              else
247
              {
248
554539
                congruentCount[k].second++;
249
              }
250
            }
251
            else
252
            {
253
139458
              congruentCount[k].first++;
254
            }
255
          }
256
        }
257
1397156
        else if (!n.isConst())
258
        {
259
1180983
          if (d_congruent.find(n) == d_congruent.end())
260
          {
261
            // We mark all but the oldest variable in the equivalence class as
262
            // congruent.
263
663442
            if (var.isNull())
264
            {
265
451136
              var = n;
266
            }
267
212306
            else if (var > n)
268
            {
269
222798
              Trace("strings-base-debug")
270
111399
                  << "  congruent variable : " << var << std::endl;
271
111399
              d_congruent.insert(var);
272
111399
              var = n;
273
            }
274
            else
275
            {
276
201814
              Trace("strings-base-debug")
277
100907
                  << "  congruent variable : " << n << std::endl;
278
100907
              d_congruent.insert(n);
279
            }
280
          }
281
        }
282
6646112
        ++eqc_i;
283
      }
284
    }
285
1114492
    ++eqcs_i;
286
  }
287
25158
  if (Trace.isOn("strings-base"))
288
  {
289
    for (const std::pair<const Kind, std::pair<uint32_t, uint32_t>>& cc :
290
         congruentCount)
291
    {
292
      Trace("strings-base")
293
          << "  Terms[" << cc.first << "] = " << cc.second.second << "/"
294
          << (cc.second.first + cc.second.second) << std::endl;
295
    }
296
  }
297
25158
  Trace("strings-base") << "BaseSolver::checkInit finished" << std::endl;
298
}
299
300
22073
void BaseSolver::checkConstantEquivalenceClasses()
301
{
302
  // do fixed point
303
22073
  size_t prevSize = 0;
304
44146
  std::vector<Node> vecc;
305
  do
306
  {
307
22073
    vecc.clear();
308
44146
    Trace("strings-base-debug")
309
22073
        << "Check constant equivalence classes..." << std::endl;
310
22073
    prevSize = d_eqcInfo.size();
311
54466
    for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
312
22073
         d_termIndex)
313
    {
314
54466
      checkConstantEquivalenceClasses(
315
108932
          &tindex.second[STRING_CONCAT], vecc, true);
316
    }
317
22073
  } while (!d_im.hasProcessed() && d_eqcInfo.size() > prevSize);
318
319
22073
  if (!d_im.hasProcessed())
320
  {
321
    // now, go back and set "most content" terms
322
22073
    vecc.clear();
323
54466
    for (std::pair<const TypeNode, std::map<Kind, TermIndex>>& tindex :
324
22073
         d_termIndex)
325
    {
326
54466
      checkConstantEquivalenceClasses(
327
108932
          &tindex.second[STRING_CONCAT], vecc, false);
328
    }
329
  }
330
22073
}
331
332
637703
void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
333
                                                 std::vector<Node>& vecc,
334
                                                 bool ensureConst,
335
                                                 bool isConst)
336
{
337
1275406
  Node n = ti->d_data;
338
637703
  if (!n.isNull())
339
  {
340
    // construct the constant if applicable
341
601068
    Node c;
342
300534
    if (isConst)
343
    {
344
76822
      c = utils::mkNConcat(vecc, n.getType());
345
    }
346
300534
    if (!isConst || !d_state.areEqual(n, c))
347
    {
348
223712
      if (Trace.isOn("strings-debug"))
349
      {
350
        Trace("strings-debug")
351
            << "Constant eqc : " << c << " for " << n << std::endl;
352
        Trace("strings-debug") << "  ";
353
        for (const Node& v : vecc)
354
        {
355
          Trace("strings-debug") << v << " ";
356
        }
357
        Trace("strings-debug") << std::endl;
358
      }
359
223712
      size_t count = 0;
360
223712
      size_t countc = 0;
361
447424
      std::vector<Node> exp;
362
      // non-constant vector
363
447424
      std::vector<Node> vecnc;
364
223712
      size_t contentSize = 0;
365
1266440
      while (count < n.getNumChildren())
366
      {
367
        // Add explanations for the empty children
368
1042728
        Node emps;
369
557838
        while (count < n.getNumChildren()
370
1079202
               && d_state.isEqualEmptyWord(n[count], emps))
371
        {
372
18237
          d_im.addToExplanation(n[count], emps, exp);
373
18237
          count++;
374
        }
375
521364
        if (count < n.getNumChildren())
376
        {
377
509604
          if (vecc[countc].isNull())
378
          {
379
464942
            Assert(!isConst);
380
            // no constant for this component, leave it as is
381
464942
            vecnc.push_back(n[count]);
382
          }
383
          else
384
          {
385
44662
            if (!isConst)
386
            {
387
              // use the constant
388
44662
              vecnc.push_back(vecc[countc]);
389
44662
              Assert(vecc[countc].isConst());
390
44662
              contentSize += Word::getLength(vecc[countc]);
391
            }
392
89324
            Trace("strings-debug") << "...explain " << n[count] << " "
393
44662
                                   << vecc[countc] << std::endl;
394
44662
            if (!d_state.areEqual(n[count], vecc[countc]))
395
            {
396
              Node nrr = d_state.getRepresentative(n[count]);
397
              Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
398
                     && d_eqcInfo[nrr].d_bestContent.isConst());
399
              // must flatten to avoid nested AND in explanations
400
              utils::flattenOp(AND, d_eqcInfo[nrr].d_exp, exp);
401
              // now explain equality to base
402
              d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
403
            }
404
            else
405
            {
406
44662
              d_im.addToExplanation(n[count], vecc[countc], exp);
407
            }
408
44662
            countc++;
409
          }
410
509604
          count++;
411
        }
412
      }
413
      // exp contains an explanation of n==c
414
223712
      Assert(!isConst || countc == vecc.size());
415
223712
      if (!isConst)
416
      {
417
        // no use storing something with no content
418
223712
        if (contentSize > 0)
419
        {
420
83082
          Node nr = d_state.getRepresentative(n);
421
41541
          BaseEqcInfo& bei = d_eqcInfo[nr];
422
83082
          if (!bei.d_bestContent.isConst()
423
41541
              && (bei.d_bestContent.isNull() || contentSize > bei.d_bestScore))
424
          {
425
            // The equivalence class is not entailed to be equal to a constant
426
            // and we found a better concatenation
427
66666
            Node nct = utils::mkNConcat(vecnc, n.getType());
428
33333
            Assert(!nct.isConst());
429
33333
            bei.d_bestContent = nct;
430
33333
            bei.d_bestScore = contentSize;
431
33333
            bei.d_base = n;
432
33333
            if (!exp.empty())
433
            {
434
11807
              bei.d_exp = utils::mkAnd(exp);
435
            }
436
66666
            Trace("strings-debug")
437
33333
                << "Set eqc best content " << n << " to " << nct
438
33333
                << ", explanation = " << bei.d_exp << std::endl;
439
          }
440
        }
441
      }
442
      else if (d_state.hasTerm(c))
443
      {
444
        d_im.sendInference(exp, n.eqNode(c), InferenceId::STRINGS_I_CONST_MERGE);
445
        return;
446
      }
447
      else if (!d_im.hasProcessed())
448
      {
449
        Node nr = d_state.getRepresentative(n);
450
        BaseEqcInfo& bei = d_eqcInfo[nr];
451
        if (!bei.d_bestContent.isConst())
452
        {
453
          bei.d_bestContent = c;
454
          bei.d_base = n;
455
          bei.d_exp = utils::mkAnd(exp);
456
          Trace("strings-debug")
457
              << "Set eqc const " << n << " to " << c
458
              << ", explanation = " << bei.d_exp << std::endl;
459
        }
460
        else if (c != bei.d_bestContent)
461
        {
462
          // conflict
463
          Trace("strings-debug")
464
              << "Conflict, other constant was " << bei.d_bestContent
465
              << ", this constant was " << c << std::endl;
466
          if (bei.d_exp.isNull())
467
          {
468
            // n==c ^ n == c' => false
469
            d_im.addToExplanation(n, bei.d_bestContent, exp);
470
          }
471
          else
472
          {
473
            // n==c ^ n == d_base == c' => false
474
            exp.push_back(bei.d_exp);
475
            d_im.addToExplanation(n, bei.d_base, exp);
476
          }
477
          d_im.sendInference(exp, d_false, InferenceId::STRINGS_I_CONST_CONFLICT);
478
          return;
479
        }
480
        else
481
        {
482
          Trace("strings-debug") << "Duplicate constant." << std::endl;
483
        }
484
      }
485
    }
486
  }
487
1306753
  for (std::pair<const TNode, TermIndex>& p : ti->d_children)
488
  {
489
669050
    std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(p.first);
490
669050
    if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst())
491
    {
492
228739
      vecc.push_back(it->second.d_bestContent);
493
228739
      checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, isConst);
494
228739
      vecc.pop_back();
495
    }
496
440311
    else if (!ensureConst)
497
    {
498
      // can still proceed, with null
499
300032
      vecc.push_back(Node::null());
500
300032
      checkConstantEquivalenceClasses(&p.second, vecc, ensureConst, false);
501
300032
      vecc.pop_back();
502
    }
503
669050
    if (d_im.hasProcessed())
504
    {
505
      break;
506
    }
507
  }
508
}
509
510
7109
void BaseSolver::checkCardinality()
511
{
512
  // This will create a partition of eqc, where each collection has length that
513
  // are pairwise propagated to be equal. We do not require disequalities
514
  // between the lengths of each collection, since we split on disequalities
515
  // between lengths of string terms that are disequal (DEQ-LENGTH-SP).
516
14218
  std::map<TypeNode, std::vector<std::vector<Node> > > cols;
517
14218
  std::map<TypeNode, std::vector<Node> > lts;
518
7109
  d_state.separateByLength(d_stringsEqc, cols, lts);
519
8330
  for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols)
520
  {
521
1221
    checkCardinalityType(c.first, c.second, lts[c.first]);
522
  }
523
7109
}
524
525
1221
void BaseSolver::checkCardinalityType(TypeNode tn,
526
                                      std::vector<std::vector<Node> >& cols,
527
                                      std::vector<Node>& lts)
528
{
529
2442
  Trace("strings-card") << "Check cardinality (type " << tn << ")..."
530
1221
                        << std::endl;
531
1221
  NodeManager* nm = NodeManager::currentNM();
532
  uint32_t typeCardSize;
533
1221
  if (tn.isString())  // string-only
534
  {
535
1153
    typeCardSize = d_cardSize;
536
  }
537
  else
538
  {
539
68
    Assert(tn.isSequence());
540
136
    TypeNode etn = tn.getSequenceElementType();
541
68
    if (etn.isInterpretedFinite())
542
    {
543
      // infinite cardinality, we are fine
544
6
      return;
545
    }
546
    // TODO (cvc4-projects #23): how to handle sequence for finite types?
547
62
    return;
548
  }
549
  // for each collection
550
7761
  for (unsigned i = 0, csize = cols.size(); i < csize; ++i)
551
  {
552
6608
    Node lr = lts[i];
553
13216
    Trace("strings-card") << "Number of strings with length equal to " << lr
554
6608
                          << " is " << cols[i].size() << std::endl;
555
6608
    if (cols[i].size() <= 1)
556
    {
557
      // no restriction on sets in the partition of size 1
558
4966
      continue;
559
    }
560
    // size > c^k
561
1642
    unsigned card_need = 1;
562
1642
    double curr = static_cast<double>(cols[i].size());
563
1642
    while (curr > typeCardSize)
564
    {
565
      curr = curr / static_cast<double>(typeCardSize);
566
      card_need++;
567
    }
568
3284
    Trace("strings-card")
569
1642
        << "Need length " << card_need
570
1642
        << " for this number of strings (where alphabet size is "
571
1642
        << typeCardSize << ") given type " << tn << "." << std::endl;
572
    // check if we need to split
573
1642
    bool needsSplit = true;
574
1642
    if (lr.isConst())
575
    {
576
      // if constant, compare
577
3100
      Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need)));
578
1550
      cmp = Rewriter::rewrite(cmp);
579
1550
      needsSplit = !cmp.getConst<bool>();
580
    }
581
    else
582
    {
583
      // find the minimimum constant that we are unknown to be disequal from, or
584
      // otherwise stop if we increment such that cardinality does not apply.
585
      // We always start with r=1 since by the invariants of our term registry,
586
      // a term is either equal to the empty string, or has length >= 1.
587
92
      unsigned r = 1;
588
92
      bool success = true;
589
92
      while (r < card_need && success)
590
      {
591
        Node rr = nm->mkConst(Rational(r));
592
        if (d_state.areDisequal(rr, lr))
593
        {
594
          r++;
595
        }
596
        else
597
        {
598
          success = false;
599
        }
600
      }
601
92
      if (r > 0)
602
      {
603
184
        Trace("strings-card")
604
92
            << "Symbolic length " << lr << " must be at least " << r
605
92
            << " due to constant disequalities." << std::endl;
606
      }
607
92
      needsSplit = r < card_need;
608
    }
609
610
1642
    if (!needsSplit)
611
    {
612
      // don't need to split
613
1642
      continue;
614
    }
615
    // first, try to split to merge equivalence classes
616
    for (std::vector<Node>::iterator itr1 = cols[i].begin();
617
         itr1 != cols[i].end();
618
         ++itr1)
619
    {
620
      for (std::vector<Node>::iterator itr2 = itr1 + 1; itr2 != cols[i].end();
621
           ++itr2)
622
      {
623
        if (!d_state.areDisequal(*itr1, *itr2))
624
        {
625
          // add split lemma
626
          if (d_im.sendSplit(*itr1, *itr2, InferenceId::STRINGS_CARD_SP))
627
          {
628
            return;
629
          }
630
        }
631
      }
632
    }
633
    // otherwise, we need a length constraint
634
    uint32_t int_k = static_cast<uint32_t>(card_need);
635
    EqcInfo* ei = d_state.getOrMakeEqcInfo(lr, true);
636
    Trace("strings-card") << "Previous cardinality used for " << lr << " is "
637
                          << ((int)ei->d_cardinalityLemK.get() - 1)
638
                          << std::endl;
639
    if (int_k + 1 > ei->d_cardinalityLemK.get())
640
    {
641
      Node k_node = nm->mkConst(Rational(int_k));
642
      // add cardinality lemma
643
      Node dist = nm->mkNode(DISTINCT, cols[i]);
644
      std::vector<Node> expn;
645
      expn.push_back(dist);
646
      for (std::vector<Node>::iterator itr1 = cols[i].begin();
647
           itr1 != cols[i].end();
648
           ++itr1)
649
      {
650
        Node len = nm->mkNode(STRING_LENGTH, *itr1);
651
        if (len != lr)
652
        {
653
          Node len_eq_lr = len.eqNode(lr);
654
          expn.push_back(len_eq_lr);
655
        }
656
      }
657
      Node len = nm->mkNode(STRING_LENGTH, cols[i][0]);
658
      Node cons = nm->mkNode(GEQ, len, k_node);
659
      cons = Rewriter::rewrite(cons);
660
      ei->d_cardinalityLemK.set(int_k + 1);
661
      if (!cons.isConst() || !cons.getConst<bool>())
662
      {
663
        d_im.sendInference(
664
            expn, expn, cons, InferenceId::STRINGS_CARDINALITY, false, true);
665
        return;
666
      }
667
    }
668
  }
669
1153
  Trace("strings-card") << "...end check cardinality" << std::endl;
670
}
671
672
2255319
bool BaseSolver::isCongruent(Node n)
673
{
674
2255319
  return d_congruent.find(n) != d_congruent.end();
675
}
676
677
1118668
Node BaseSolver::getConstantEqc(Node eqc)
678
{
679
1118668
  std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
680
1118668
  if (it != d_eqcInfo.end() && it->second.d_bestContent.isConst())
681
  {
682
400138
    return it->second.d_bestContent;
683
  }
684
718530
  return Node::null();
685
}
686
687
39467
Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
688
{
689
39467
  std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
690
39467
  if (it != d_eqcInfo.end())
691
  {
692
39467
    BaseEqcInfo& bei = d_eqcInfo[eqc];
693
39467
    if (!bei.d_bestContent.isConst())
694
    {
695
      return Node::null();
696
    }
697
39467
    if (!bei.d_exp.isNull())
698
    {
699
      utils::flattenOp(AND, bei.d_exp, exp);
700
    }
701
39467
    if (!bei.d_base.isNull())
702
    {
703
39467
      d_im.addToExplanation(n, bei.d_base, exp);
704
    }
705
39467
    return bei.d_bestContent;
706
  }
707
  return Node::null();
708
}
709
710
552155
Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp)
711
{
712
552155
  std::map<Node, BaseEqcInfo>::const_iterator it = d_eqcInfo.find(eqc);
713
552155
  if (it != d_eqcInfo.end())
714
  {
715
316033
    BaseEqcInfo& bei = d_eqcInfo[eqc];
716
316033
    Assert(!bei.d_bestContent.isNull());
717
316033
    if (!bei.d_exp.isNull())
718
    {
719
31800
      utils::flattenOp(AND, bei.d_exp, exp);
720
    }
721
316033
    if (!bei.d_base.isNull())
722
    {
723
316033
      d_im.addToExplanation(n, bei.d_base, exp);
724
    }
725
316033
    return bei.d_bestContent;
726
  }
727
728
236122
  return Node::null();
729
}
730
731
21706
const std::vector<Node>& BaseSolver::getStringEqc() const
732
{
733
21706
  return d_stringsEqc;
734
}
735
736
2077330
Node BaseSolver::TermIndex::add(TNode n,
737
                                unsigned index,
738
                                const SolverState& s,
739
                                Node er,
740
                                std::vector<Node>& c)
741
{
742
2077330
  if (index == n.getNumChildren())
743
  {
744
619361
    if (d_data.isNull())
745
    {
746
571055
      d_data = n;
747
    }
748
619361
    return d_data;
749
  }
750
1457969
  Assert(index < n.getNumChildren());
751
2915938
  TNode nir = s.getRepresentative(n[index]);
752
  // if it is empty, and doing CONCAT, ignore
753
1457969
  if (nir == er && n.getKind() == STRING_CONCAT)
754
  {
755
102632
    return add(n, index + 1, s, er, c);
756
  }
757
1355337
  c.push_back(nir);
758
1355337
  return d_children[nir].add(n, index + 1, s, er, c);
759
}
760
761
}  // namespace strings
762
}  // namespace theory
763
26685
}  // namespace CVC4