GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/theory_strings.cpp Lines: 468 571 82.0 %
Date: 2021-03-22 Branches: 995 2361 42.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_strings.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Andres Noetzli
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 the theory of strings.
13
 **/
14
15
#include "theory/strings/theory_strings.h"
16
17
#include "expr/kind.h"
18
#include "options/smt_options.h"
19
#include "options/strings_options.h"
20
#include "options/theory_options.h"
21
#include "smt/logic_exception.h"
22
#include "theory/decision_manager.h"
23
#include "theory/ext_theory.h"
24
#include "theory/rewriter.h"
25
#include "theory/strings/theory_strings_utils.h"
26
#include "theory/strings/type_enumerator.h"
27
#include "theory/strings/word.h"
28
#include "theory/theory_model.h"
29
#include "theory/valuation.h"
30
31
using namespace std;
32
using namespace CVC4::context;
33
using namespace CVC4::kind;
34
35
namespace CVC4 {
36
namespace theory {
37
namespace strings {
38
39
8995
TheoryStrings::TheoryStrings(context::Context* c,
40
                             context::UserContext* u,
41
                             OutputChannel& out,
42
                             Valuation valuation,
43
                             const LogicInfo& logicInfo,
44
8995
                             ProofNodeManager* pnm)
45
    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
46
      d_notify(*this),
47
      d_statistics(),
48
      d_state(c, u, d_valuation),
49
      d_eagerSolver(d_state),
50
      d_termReg(d_state, d_statistics, pnm),
51
      d_extTheoryCb(),
52
      d_extTheory(d_extTheoryCb, c, u, out),
53
      d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
54
      d_rewriter(&d_statistics.d_rewrites),
55
      d_bsolver(d_state, d_im),
56
      d_csolver(d_state, d_im, d_termReg, d_bsolver),
57
      d_esolver(d_state,
58
                d_im,
59
                d_termReg,
60
                d_rewriter,
61
                d_bsolver,
62
                d_csolver,
63
                d_extTheory,
64
                d_statistics),
65
      d_rsolver(d_state,
66
                d_im,
67
                d_termReg.getSkolemCache(),
68
                d_csolver,
69
                d_esolver,
70
                d_statistics),
71
18008
      d_regexp_elim(options::regExpElimAgg(), pnm, u),
72
17990
      d_stringsFmf(c, u, valuation, d_termReg)
73
{
74
8995
  d_termReg.finishInit(&d_im);
75
76
8995
  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
77
8995
  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
78
8995
  d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
79
8995
  d_true = NodeManager::currentNM()->mkConst( true );
80
8995
  d_false = NodeManager::currentNM()->mkConst( false );
81
82
8995
  d_cardSize = utils::getAlphabetCardinality();
83
84
  // set up the extended function callback
85
8995
  d_extTheoryCb.d_esolver = &d_esolver;
86
87
8995
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
88
8995
  if (pc != nullptr)
89
  {
90
    // add checkers
91
962
    d_sProofChecker.registerTo(pc);
92
  }
93
  // use the state object as the official theory state
94
8995
  d_theoryState = &d_state;
95
  // use the inference manager as the official inference manager
96
8995
  d_inferManager = &d_im;
97
8995
}
98
99
17984
TheoryStrings::~TheoryStrings() {
100
101
17984
}
102
103
8995
TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
104
105
8995
bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
106
{
107
8995
  esi.d_notify = &d_notify;
108
8995
  esi.d_name = "theory::strings::ee";
109
8995
  return true;
110
}
111
112
8995
void TheoryStrings::finishInit()
113
{
114
8995
  Assert(d_equalityEngine != nullptr);
115
116
  // witness is used to eliminate str.from_code
117
8995
  d_valuation.setUnevaluatedKind(WITNESS);
118
119
17990
  bool eagerEval = options::stringEagerEval();
120
  // The kinds we are treating as function application in congruence
121
8995
  d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval);
122
8995
  d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval);
123
8995
  d_equalityEngine->addFunctionKind(kind::STRING_IN_REGEXP, eagerEval);
124
8995
  d_equalityEngine->addFunctionKind(kind::STRING_TO_CODE, eagerEval);
125
8995
  d_equalityEngine->addFunctionKind(kind::SEQ_UNIT, eagerEval);
126
  // `seq.nth` is not always defined, and so we do not evaluate it eagerly.
127
8995
  d_equalityEngine->addFunctionKind(kind::SEQ_NTH, false);
128
  // extended functions
129
8995
  d_equalityEngine->addFunctionKind(kind::STRING_STRCTN, eagerEval);
130
8995
  d_equalityEngine->addFunctionKind(kind::STRING_LEQ, eagerEval);
131
8995
  d_equalityEngine->addFunctionKind(kind::STRING_SUBSTR, eagerEval);
132
8995
  d_equalityEngine->addFunctionKind(kind::STRING_UPDATE, eagerEval);
133
8995
  d_equalityEngine->addFunctionKind(kind::STRING_ITOS, eagerEval);
134
8995
  d_equalityEngine->addFunctionKind(kind::STRING_STOI, eagerEval);
135
8995
  d_equalityEngine->addFunctionKind(kind::STRING_STRIDOF, eagerEval);
136
8995
  d_equalityEngine->addFunctionKind(kind::STRING_STRREPL, eagerEval);
137
8995
  d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
138
8995
  d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
139
8995
  d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
140
8995
  d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
141
8995
  d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval);
142
8995
  d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval);
143
8995
  d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval);
144
8995
}
145
146
std::string TheoryStrings::identify() const
147
{
148
  return std::string("TheoryStrings");
149
}
150
151
2711
bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
152
2711
  Assert(d_equalityEngine->hasTerm(x));
153
2711
  Assert(d_equalityEngine->hasTerm(y));
154
8133
  if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
155
8133
      && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
156
  {
157
    TNode x_shared =
158
3080
        d_equalityEngine->getTriggerTermRepresentative(x, THEORY_STRINGS);
159
    TNode y_shared =
160
3080
        d_equalityEngine->getTriggerTermRepresentative(y, THEORY_STRINGS);
161
2051
    EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
162
2051
    if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
163
1022
      return true;
164
    }
165
  }
166
1689
  return false;
167
}
168
169
614828
bool TheoryStrings::propagateLit(TNode literal)
170
{
171
614828
  return d_im.propagateLit(literal);
172
}
173
174
37721
TrustNode TheoryStrings::explain(TNode literal)
175
{
176
37721
  Debug("strings-explain") << "explain called on " << literal << std::endl;
177
37721
  return d_im.explainLit(literal);
178
}
179
180
12416
void TheoryStrings::presolve() {
181
12416
  Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
182
12416
  d_strat.initializeStrategy();
183
184
  // if strings fmf is enabled, register the strategy
185
12416
  if (options::stringFMF())
186
  {
187
61
    d_stringsFmf.presolve();
188
    // This strategy is local to a check-sat call, since we refresh the strategy
189
    // on every call to presolve.
190
61
    getDecisionManager()->registerStrategy(
191
        DecisionManager::STRAT_STRINGS_SUM_LENGTHS,
192
        d_stringsFmf.getDecisionStrategy(),
193
        DecisionManager::STRAT_SCOPE_LOCAL_SOLVE);
194
  }
195
12416
  Debug("strings-presolve") << "Finished presolve" << std::endl;
196
12416
}
197
198
199
/////////////////////////////////////////////////////////////////////////////
200
// MODEL GENERATION
201
/////////////////////////////////////////////////////////////////////////////
202
203
5076
bool TheoryStrings::collectModelValues(TheoryModel* m,
204
                                       const std::set<Node>& termSet)
205
{
206
5076
  if (Trace.isOn("strings-model"))
207
  {
208
    Trace("strings-model") << "TheoryStrings : Collect model values"
209
                           << std::endl;
210
    Trace("strings-model") << "Equivalence classes are:" << std::endl;
211
    Trace("strings-model") << debugPrintStringsEqc() << std::endl;
212
  }
213
10152
  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
214
  // Generate model
215
  // get the relevant string equivalence classes
216
73834
  for (const Node& s : termSet)
217
  {
218
137516
    TypeNode tn = s.getType();
219
68758
    if (tn.isStringLike())
220
    {
221
68642
      Node r = d_state.getRepresentative(s);
222
34321
      repSet[tn].insert(r);
223
    }
224
  }
225
792
  for (const std::pair<const TypeNode,
226
                       std::unordered_set<Node, NodeHashFunction> >& rst :
227
5076
       repSet)
228
  {
229
    // get partition of strings of equal lengths, per type
230
1586
    std::map<TypeNode, std::vector<std::vector<Node> > > colT;
231
1586
    std::map<TypeNode, std::vector<Node> > ltsT;
232
1586
    std::vector<Node> repVec(rst.second.begin(), rst.second.end());
233
793
    d_state.separateByLength(repVec, colT, ltsT);
234
    // now collect model info for the type
235
1586
    TypeNode st = rst.first;
236
794
    if (!collectModelInfoType(st, rst.second, colT[st], ltsT[st], m))
237
    {
238
      return false;
239
    }
240
  }
241
5075
  return true;
242
}
243
244
793
bool TheoryStrings::collectModelInfoType(
245
    TypeNode tn,
246
    const std::unordered_set<Node, NodeHashFunction>& repSet,
247
    std::vector<std::vector<Node> >& col,
248
    std::vector<Node>& lts,
249
    TheoryModel* m)
250
{
251
793
  NodeManager* nm = NodeManager::currentNM();
252
1586
  std::map< Node, Node > processed;
253
  //step 1 : get all values for known lengths
254
1586
  std::vector< Node > lts_values;
255
1586
  std::map<std::size_t, Node> values_used;
256
1586
  std::vector<Node> len_splits;
257
5651
  for( unsigned i=0; i<col.size(); i++ ) {
258
4859
    Trace("strings-model") << "Checking length for {";
259
13394
    for( unsigned j=0; j<col[i].size(); j++ ) {
260
8535
      if( j>0 ) {
261
3676
        Trace("strings-model") << ", ";
262
      }
263
8535
      Trace("strings-model") << col[i][j];
264
    }
265
4859
    Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
266
9718
    Node len_value;
267
4859
    if( lts[i].isConst() ) {
268
3547
      len_value = lts[i];
269
    }
270
1312
    else if (!lts[i].isNull())
271
    {
272
      // get the model value for lts[i]
273
1312
      len_value = d_valuation.getModelValue(lts[i]);
274
    }
275
4859
    if (len_value.isNull())
276
    {
277
      lts_values.push_back(Node::null());
278
    }
279
    else
280
    {
281
      // must throw logic exception if we cannot construct the string
282
4859
      if (len_value.getConst<Rational>() > String::maxSize())
283
      {
284
2
        std::stringstream ss;
285
2
        ss << "The model was computed to have strings of length " << len_value
286
1
           << ". We only allow strings up to length " << String::maxSize();
287
1
        throw LogicException(ss.str());
288
      }
289
      std::size_t lvalue =
290
4858
          len_value.getConst<Rational>().getNumerator().toUnsignedInt();
291
4858
      auto itvu = values_used.find(lvalue);
292
4858
      if (itvu == values_used.end())
293
      {
294
3867
        values_used[lvalue] = lts[i];
295
      }
296
      else
297
      {
298
991
        len_splits.push_back(lts[i].eqNode(itvu->second));
299
      }
300
4858
      lts_values.push_back(len_value);
301
    }
302
  }
303
  ////step 2 : assign arbitrary values for unknown lengths?
304
  // confirmed by calculus invariant, see paper
305
792
  Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
306
1584
  std::map<Node, Node> pure_eq_assign;
307
  //step 3 : assign values to equivalence classes that are pure variables
308
5649
  for( unsigned i=0; i<col.size(); i++ ){
309
9714
    std::vector< Node > pure_eq;
310
9714
    Trace("strings-model") << "The (" << col[i].size()
311
4857
                           << ") equivalence classes ";
312
13390
    for (const Node& eqc : col[i])
313
    {
314
8533
      Trace("strings-model") << eqc << " ";
315
      //check if col[i][j] has only variables
316
8533
      if (!eqc.isConst())
317
      {
318
2489
        NormalForm& nfe = d_csolver.getNormalForm(eqc);
319
2489
        if (nfe.d_nf.size() == 1)
320
        {
321
          // is it an equivalence class with a seq.unit term?
322
777
          if (nfe.d_nf[0].getKind() == SEQ_UNIT)
323
          {
324
16
            Node argVal;
325
8
            if (nfe.d_nf[0][0].getType().isStringLike())
326
            {
327
1
              argVal = d_state.getRepresentative(nfe.d_nf[0][0]);
328
            }
329
            else
330
            {
331
              // otherwise, it is a shared term
332
7
              argVal = d_valuation.getModelValue(nfe.d_nf[0][0]);
333
            }
334
16
            Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal));
335
8
            pure_eq_assign[eqc] = c;
336
8
            Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") ";
337
8
            m->getEqualityEngine()->addTerm(c);
338
          }
339
          // does it have a code and the length of these equivalence classes are
340
          // one?
341
769
          else if (d_termReg.hasStringCode() && lts_values[i] == d_one)
342
          {
343
291
            EqcInfo* eip = d_state.getOrMakeEqcInfo(eqc, false);
344
291
            if (eip && !eip->d_codeTerm.get().isNull())
345
            {
346
              // its value must be equal to its code
347
310
              Node ct = nm->mkNode(kind::STRING_TO_CODE, eip->d_codeTerm.get());
348
310
              Node ctv = d_valuation.getModelValue(ct);
349
              unsigned cvalue =
350
155
                  ctv.getConst<Rational>().getNumerator().toUnsignedInt();
351
155
              Trace("strings-model") << "(code: " << cvalue << ") ";
352
310
              std::vector<unsigned> vec;
353
155
              vec.push_back(cvalue);
354
310
              Node mv = nm->mkConst(String(vec));
355
155
              pure_eq_assign[eqc] = mv;
356
155
              m->getEqualityEngine()->addTerm(mv);
357
            }
358
          }
359
777
          pure_eq.push_back(eqc);
360
        }
361
      }
362
      else
363
      {
364
6044
        processed[eqc] = eqc;
365
        // Make sure that constants are asserted to the theory model that we
366
        // are building. It is possible that new constants were introduced by
367
        // the eager evaluation in the equality engine. These terms are missing
368
        // in the term set and, as a result, are skipped when the equality
369
        // engine is asserted to the theory model.
370
6044
        m->getEqualityEngine()->addTerm(eqc);
371
      }
372
    }
373
4857
    Trace("strings-model") << "have length " << lts_values[i] << std::endl;
374
375
    //assign a new length if necessary
376
4857
    if( !pure_eq.empty() ){
377
556
      if( lts_values[i].isNull() ){
378
        // start with length two (other lengths have special precendence)
379
        std::size_t lvalue = 2;
380
        while( values_used.find( lvalue )!=values_used.end() ){
381
          lvalue++;
382
        }
383
        Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
384
        lts_values[i] = nm->mkConst(Rational(lvalue));
385
        values_used[lvalue] = Node::null();
386
      }
387
556
      Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
388
1333
      for( unsigned j=0; j<pure_eq.size(); j++ ){
389
777
        Trace("strings-model") << pure_eq[j] << " ";
390
      }
391
556
      Trace("strings-model") << std::endl;
392
393
      //use type enumerator
394
556
      Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()))
395
          << "Exceeded UINT32_MAX in string model";
396
      uint32_t currLen =
397
556
          lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt();
398
1112
      std::unique_ptr<SEnumLen> sel;
399
1112
      Trace("strings-model") << "Cardinality of alphabet is "
400
556
                             << utils::getAlphabetCardinality() << std::endl;
401
556
      if (tn.isString())  // string-only
402
      {
403
542
        sel.reset(new StringEnumLen(
404
542
            currLen, currLen, utils::getAlphabetCardinality()));
405
      }
406
      else
407
      {
408
14
        sel.reset(new SeqEnumLen(tn, nullptr, currLen, currLen));
409
      }
410
1333
      for (const Node& eqc : pure_eq)
411
      {
412
1554
        Node c;
413
777
        std::map<Node, Node>::iterator itp = pure_eq_assign.find(eqc);
414
777
        if (itp == pure_eq_assign.end())
415
        {
416
629
          do
417
          {
418
1243
            if (sel->isFinished())
419
            {
420
              // We are in a case where model construction is impossible due to
421
              // an insufficient number of constants of a given length.
422
423
              // Consider an integer equivalence class E whose value is assigned
424
              // n in the model. Let { S_1, ..., S_m } be the set of string
425
              // equivalence classes such that len( x ) is a member of E for
426
              // some member x of each class S1, ...,Sm. Since our calculus is
427
              // saturated with respect to cardinality inference (see Liang
428
              // et al, Figure 6, CAV 2014), we have that m <= A^n, where A is
429
              // the cardinality of our alphabet.
430
431
              // Now, consider the case where there exists two integer
432
              // equivalence classes E1 and E2 that are assigned n, and moreover
433
              // we did not received notification from arithmetic that E1 = E2.
434
              // This typically should never happen, but assume in the following
435
              // that it does.
436
437
              // Now, it may be the case that there are string equivalence
438
              // classes { S_1, ..., S_m1 } whose lengths are in E1,
439
              // and classes { S'_1, ..., S'_m2 } whose lengths are in E2, where
440
              // m1 + m2 > A^n. In this case, we have insufficient strings to
441
              // assign to { S_1, ..., S_m1, S'_1, ..., S'_m2 }. If this
442
              // happens, we add a split on len( u1 ) = len( u2 ) for some
443
              // len( u1 ) in E1, len( u2 ) in E2. We do this for each pair of
444
              // integer equivalence classes that are assigned to the same value
445
              // in the model.
446
              AlwaysAssert(!len_splits.empty());
447
              for (const Node& sl : len_splits)
448
              {
449
                Node spl = nm->mkNode(OR, sl, sl.negate());
450
                d_im.lemma(spl, InferenceId::STRINGS_CMI_SPLIT);
451
                Trace("strings-lemma")
452
                    << "Strings::CollectModelInfoSplit: " << spl << std::endl;
453
              }
454
              // we added a lemma, so can return here
455
              return false;
456
            }
457
1243
            c = sel->getCurrent();
458
            // increment
459
1243
            sel->increment();
460
1243
          } while (m->hasTerm(c));
461
        }
462
        else
463
        {
464
163
          c = itp->second;
465
        }
466
1554
        Trace("strings-model") << "*** Assigned constant " << c << " for "
467
777
                               << eqc << std::endl;
468
777
        processed[eqc] = c;
469
777
        if (!m->assertEquality(eqc, c, true))
470
        {
471
          // this should never happen due to the model soundness argument
472
          // for strings
473
          Unreachable()
474
              << "TheoryStrings::collectModelInfoType: Inconsistent equality"
475
              << std::endl;
476
          return false;
477
        }
478
      }
479
    }
480
  }
481
792
  Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
482
  //step 4 : assign constants to all other equivalence classes
483
9325
  for (const Node& rn : repSet)
484
  {
485
8533
    if (processed.find(rn) == processed.end())
486
    {
487
1712
      NormalForm& nf = d_csolver.getNormalForm(rn);
488
1712
      if (Trace.isOn("strings-model"))
489
      {
490
        Trace("strings-model")
491
            << "Construct model for " << rn << " based on normal form ";
492
        for (unsigned j = 0, size = nf.d_nf.size(); j < size; j++)
493
        {
494
          Node n = nf.d_nf[j];
495
          if (j > 0)
496
          {
497
            Trace("strings-model") << " ++ ";
498
          }
499
          Trace("strings-model") << n;
500
          Node r = d_state.getRepresentative(n);
501
          if (!r.isConst() && processed.find(r) == processed.end())
502
          {
503
            Trace("strings-model") << "(UNPROCESSED)";
504
          }
505
        }
506
      }
507
1712
      Trace("strings-model") << std::endl;
508
3424
      std::vector< Node > nc;
509
8414
      for (const Node& n : nf.d_nf)
510
      {
511
13404
        Node r = d_state.getRepresentative(n);
512
6702
        Assert(r.isConst() || processed.find(r) != processed.end());
513
6702
        nc.push_back(r.isConst() ? r : processed[r]);
514
      }
515
3424
      Node cc = utils::mkNConcat(nc, tn);
516
3424
      Trace("strings-model")
517
1712
          << "*** Determined constant " << cc << " for " << rn << std::endl;
518
1712
      processed[rn] = cc;
519
1712
      if (!m->assertEquality(rn, cc, true))
520
      {
521
        // this should never happen due to the model soundness argument
522
        // for strings
523
        Unreachable() << "TheoryStrings::collectModelInfoType: "
524
                         "Inconsistent equality (unprocessed eqc)"
525
                      << std::endl;
526
        return false;
527
      }
528
1712
      else if (!cc.isConst())
529
      {
530
        // the value may be specified by seq.unit components, ensure this
531
        // is marked as the skeleton for constructing values in this class.
532
        m->assertSkeleton(cc);
533
      }
534
    }
535
  }
536
  //Trace("strings-model") << "String Model : Assigned." << std::endl;
537
792
  Trace("strings-model") << "String Model : Finished." << std::endl;
538
792
  return true;
539
}
540
541
/////////////////////////////////////////////////////////////////////////////
542
// MAIN SOLVER
543
/////////////////////////////////////////////////////////////////////////////
544
545
104368
void TheoryStrings::preRegisterTerm(TNode n)
546
{
547
208736
  Trace("strings-preregister")
548
104368
      << "TheoryStrings::preRegisterTerm: " << n << std::endl;
549
104368
  d_termReg.preRegisterTerm(n);
550
  // Register the term with the extended theory. Notice we do not recurse on
551
  // this term here since preRegisterTerm is already called recursively on all
552
  // subterms in preregistered literals.
553
104368
  d_extTheory.registerTerm(n);
554
104368
}
555
556
544
TrustNode TheoryStrings::expandDefinition(Node node)
557
{
558
544
  Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
559
560
544
  if (node.getKind() == kind::SEQ_NTH)
561
  {
562
2
    NodeManager* nm = NodeManager::currentNM();
563
2
    SkolemCache* sc = d_termReg.getSkolemCache();
564
4
    Node s = node[0];
565
4
    Node n = node[1];
566
    // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
567
    Node cond = nm->mkNode(AND,
568
4
                           nm->mkNode(LEQ, d_zero, n),
569
8
                           nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
570
4
    Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
571
4
    Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
572
4
    Node u = nm->mkNode(APPLY_UF, uf, s, n);
573
4
    Node ret = nm->mkNode(ITE, cond, ss, u);
574
2
    Trace("strings-exp-def") << "...return " << ret << std::endl;
575
2
    return TrustNode::mkTrustRewrite(node, ret, nullptr);
576
  }
577
542
  return TrustNode::null();
578
}
579
580
606809
bool TheoryStrings::preNotifyFact(
581
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
582
{
583
  // this is only required for internal facts, others are already registered
584
606809
  if (isInternal && atom.getKind() == EQUAL)
585
  {
586
    // We must ensure these terms are registered. We register eagerly here for
587
    // performance reasons. Alternatively, terms could be registered at full
588
    // effort in e.g. BaseSolver::init.
589
40023
    for (const Node& t : atom)
590
    {
591
26682
      d_termReg.registerTerm(t, 0);
592
    }
593
  }
594
606809
  return false;
595
}
596
597
606809
void TheoryStrings::notifyFact(TNode atom,
598
                               bool polarity,
599
                               TNode fact,
600
                               bool isInternal)
601
{
602
606809
  d_eagerSolver.notifyFact(atom, polarity, fact, isInternal);
603
  // process pending conflicts due to reasoning about endpoints
604
606809
  if (!d_state.isInConflict() && d_state.hasPendingConflict())
605
  {
606
570
    InferInfo iiPendingConf(InferenceId::UNKNOWN);
607
285
    d_state.getPendingConflict(iiPendingConf);
608
570
    Trace("strings-pending")
609
285
        << "Process pending conflict " << iiPendingConf.d_premises << std::endl;
610
570
    Trace("strings-conflict")
611
285
        << "CONFLICT: Eager : " << iiPendingConf.d_premises << std::endl;
612
285
    ++(d_statistics.d_conflictsEager);
613
    // call the inference manager to send the conflict
614
285
    d_im.processConflict(iiPendingConf);
615
285
    return;
616
  }
617
606524
  Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
618
606524
  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
619
}
620
621
261321
void TheoryStrings::postCheck(Effort e)
622
{
623
261321
  d_im.doPendingFacts();
624
625
261321
  Assert(d_strat.isStrategyInit());
626
782585
  if (!d_state.isInConflict() && !d_valuation.needCheck()
627
327175
      && d_strat.hasStrategyEffort(e))
628
  {
629
34674
    Trace("strings-check-debug")
630
17337
        << "Theory of strings " << e << " effort check " << std::endl;
631
17337
    if (Trace.isOn("strings-eqc"))
632
    {
633
      Trace("strings-eqc") << debugPrintStringsEqc() << std::endl;
634
    }
635
17337
    ++(d_statistics.d_checkRuns);
636
17337
    bool sentLemma = false;
637
17337
    bool hadPending = false;
638
17337
    Trace("strings-check") << "Full effort check..." << std::endl;
639
7811
    do{
640
25148
      d_im.reset();
641
25148
      ++(d_statistics.d_strategyRuns);
642
25148
      Trace("strings-check") << "  * Run strategy..." << std::endl;
643
25148
      runStrategy(e);
644
      // remember if we had pending facts or lemmas
645
25148
      hadPending = d_im.hasPending();
646
      // Send the facts *and* the lemmas. We send lemmas regardless of whether
647
      // we send facts since some lemmas cannot be dropped. Other lemmas are
648
      // otherwise avoided by aborting the strategy when a fact is ready.
649
25148
      d_im.doPending();
650
      // Did we successfully send a lemma? Notice that if hasPending = true
651
      // and sentLemma = false, then the above call may have:
652
      // (1) had no pending lemmas, but successfully processed pending facts,
653
      // (2) unsuccessfully processed pending lemmas.
654
      // In either case, we repeat the strategy if we are not in conflict.
655
25148
      sentLemma = d_im.hasSentLemma();
656
25148
      if (Trace.isOn("strings-check"))
657
      {
658
        Trace("strings-check") << "  ...finish run strategy: ";
659
        Trace("strings-check") << (hadPending ? "hadPending " : "");
660
        Trace("strings-check") << (sentLemma ? "sentLemma " : "");
661
        Trace("strings-check") << (d_state.isInConflict() ? "conflict " : "");
662
        if (!hadPending && !sentLemma && !d_state.isInConflict())
663
        {
664
          Trace("strings-check") << "(none)";
665
        }
666
        Trace("strings-check") << std::endl;
667
      }
668
      // repeat if we did not add a lemma or conflict, and we had pending
669
      // facts or lemmas.
670
25148
    } while (!d_state.isInConflict() && !sentLemma && hadPending);
671
  }
672
261321
  Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
673
261321
  Assert(!d_im.hasPendingFact());
674
261321
  Assert(!d_im.hasPendingLemma());
675
261321
}
676
677
6030
bool TheoryStrings::needsCheckLastEffort() {
678
6030
  if( options::stringGuessModel() ){
679
    return d_esolver.hasExtendedFunctions();
680
  }
681
6030
  return false;
682
}
683
684
/** Conflict when merging two constants */
685
645
void TheoryStrings::conflict(TNode a, TNode b){
686
645
  if (d_state.isInConflict())
687
  {
688
    // already in conflict
689
    return;
690
  }
691
645
  d_im.conflictEqConstantMerge(a, b);
692
645
  Trace("strings-conflict") << "CONFLICT: Eq engine conflict" << std::endl;
693
645
  ++(d_statistics.d_conflictsEqEngine);
694
}
695
696
83762
void TheoryStrings::eqNotifyNewClass(TNode t){
697
83762
  Kind k = t.getKind();
698
83762
  if (k == STRING_LENGTH || k == STRING_TO_CODE)
699
  {
700
24508
    Trace("strings-debug") << "New length eqc : " << t << std::endl;
701
    //we care about the length of this string
702
24508
    d_termReg.registerTerm(t[0], 1);
703
  }
704
83762
  d_eagerSolver.eqNotifyNewClass(t);
705
83762
}
706
707
8450
void TheoryStrings::addCarePairs(TNodeTrie* t1,
708
                                 TNodeTrie* t2,
709
                                 unsigned arity,
710
                                 unsigned depth)
711
{
712
8450
  if( depth==arity ){
713
374
    if( t2!=NULL ){
714
748
      Node f1 = t1->getData();
715
748
      Node f2 = t2->getData();
716
374
      if (!d_equalityEngine->areEqual(f1, f2))
717
      {
718
239
        Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
719
478
        vector< pair<TNode, TNode> > currentPairs;
720
674
        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
721
870
          TNode x = f1[k];
722
870
          TNode y = f2[k];
723
435
          Assert(d_equalityEngine->hasTerm(x));
724
435
          Assert(d_equalityEngine->hasTerm(y));
725
435
          Assert(!d_equalityEngine->areDisequal(x, y, false));
726
435
          Assert(!areCareDisequal(x, y));
727
435
          if (!d_equalityEngine->areEqual(x, y))
728
          {
729
753
            if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS)
730
753
                && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS))
731
            {
732
119
              TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
733
238
                  x, THEORY_STRINGS);
734
119
              TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
735
238
                  y, THEORY_STRINGS);
736
119
              currentPairs.push_back(make_pair(x_shared, y_shared));
737
            }
738
          }
739
        }
740
358
        for (unsigned c = 0; c < currentPairs.size(); ++ c) {
741
119
          Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
742
119
          addCarePair(currentPairs[c].first, currentPairs[c].second);
743
        }
744
      }
745
    }
746
  }else{
747
8076
    if( t2==NULL ){
748
7196
      if( depth<(arity-1) ){
749
        //add care pairs internal to each child
750
7181
        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
751
        {
752
4813
          addCarePairs(&tt.second, nullptr, arity, depth + 1);
753
        }
754
      }
755
      //add care pairs based on each pair of non-disequal arguments
756
25207
      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
757
25207
           it != t1->d_data.end();
758
           ++it)
759
      {
760
18011
        std::map<TNode, TNodeTrie>::iterator it2 = it;
761
18011
        ++it2;
762
174173
        for( ; it2 != t1->d_data.end(); ++it2 ){
763
78081
          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
764
          {
765
1318
            if( !areCareDisequal(it->first, it2->first) ){
766
710
              addCarePairs( &it->second, &it2->second, arity, depth+1 );
767
            }
768
          }
769
        }
770
      }
771
    }else{
772
      //add care pairs based on product of indices, non-disequal arguments
773
2344
      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
774
      {
775
4080
        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
776
        {
777
2616
          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
778
          {
779
958
            if (!areCareDisequal(tt1.first, tt2.first))
780
            {
781
544
              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
782
            }
783
          }
784
        }
785
      }
786
    }
787
  }
788
8450
}
789
790
6475
void TheoryStrings::computeCareGraph(){
791
  //computing the care graph here is probably still necessary, due to operators that take non-string arguments  TODO: verify
792
6475
  Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
793
  // Term index for each (type, operator) pair. We require the operator here
794
  // since operators are polymorphic, taking strings/sequences.
795
12950
  std::map<std::pair<TypeNode, Node>, TNodeTrie> index;
796
12950
  std::map< Node, unsigned > arity;
797
6475
  const context::CDList<TNode>& fterms = d_termReg.getFunctionTerms();
798
6475
  size_t functionTerms = fterms.size();
799
41996
  for (unsigned i = 0; i < functionTerms; ++ i) {
800
71042
    TNode f1 = fterms[i];
801
35521
    Trace("strings-cg") << "...build for " << f1 << std::endl;
802
71042
    Node op = f1.getOperator();
803
71042
    std::vector< TNode > reps;
804
35521
    bool has_trigger_arg = false;
805
81379
    for( unsigned j=0; j<f1.getNumChildren(); j++ ){
806
45858
      reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
807
45858
      if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_STRINGS))
808
      {
809
34547
        has_trigger_arg = true;
810
      }
811
    }
812
35521
    if( has_trigger_arg ){
813
53150
      TypeNode ft = utils::getOwnerStringType(f1);
814
53150
      std::pair<TypeNode, Node> ikey = std::pair<TypeNode, Node>(ft, op);
815
26575
      index[ikey].addTerm(f1, reps);
816
26575
      arity[op] = reps.size();
817
    }
818
  }
819
  //for each index
820
8858
  for (std::pair<const std::pair<TypeNode, Node>, TNodeTrie>& ti : index)
821
  {
822
4766
    Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
823
2383
                        << ti.first << "..." << std::endl;
824
4766
    Node op = ti.first.second;
825
2383
    addCarePairs(&ti.second, nullptr, arity[op], 0);
826
  }
827
6475
}
828
829
void TheoryStrings::checkRegisterTermsPreNormalForm()
830
{
831
  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
832
  for (const Node& eqc : seqc)
833
  {
834
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
835
    while (!eqc_i.isFinished())
836
    {
837
      Node n = (*eqc_i);
838
      if (!d_bsolver.isCongruent(n))
839
      {
840
        d_termReg.registerTerm(n, 2);
841
      }
842
      ++eqc_i;
843
    }
844
  }
845
}
846
847
8957
void TheoryStrings::checkCodes()
848
{
849
  // ensure that lemmas regarding str.code been added for each constant string
850
  // of length one
851
8957
  if (d_termReg.hasStringCode())
852
  {
853
821
    NodeManager* nm = NodeManager::currentNM();
854
    // str.code applied to the code term for each equivalence class that has a
855
    // code term but is not a constant
856
1487
    std::vector<Node> nconst_codes;
857
    // str.code applied to the proxy variables for each equivalence classes that
858
    // are constants of size one
859
1487
    std::vector<Node> const_codes;
860
821
    const std::vector<Node>& seqc = d_bsolver.getStringEqc();
861
10739
    for (const Node& eqc : seqc)
862
    {
863
9918
      NormalForm& nfe = d_csolver.getNormalForm(eqc);
864
9918
      if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst())
865
      {
866
7856
        Node c = nfe.d_nf[0];
867
7856
        Trace("strings-code-debug") << "Get proxy variable for " << c
868
3928
                                    << std::endl;
869
7856
        Node cc = nm->mkNode(kind::STRING_TO_CODE, c);
870
3928
        cc = Rewriter::rewrite(cc);
871
3928
        Assert(cc.isConst());
872
7856
        Node cp = d_termReg.ensureProxyVariableFor(c);
873
7856
        Node vc = nm->mkNode(STRING_TO_CODE, cp);
874
3928
        if (!d_state.areEqual(cc, vc))
875
        {
876
776
          std::vector<Node> emptyVec;
877
388
          d_im.sendInference(emptyVec, cc.eqNode(vc), InferenceId::STRINGS_CODE_PROXY);
878
        }
879
3928
        const_codes.push_back(vc);
880
      }
881
      else
882
      {
883
5990
        EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
884
5990
        if (ei && !ei->d_codeTerm.get().isNull())
885
        {
886
3160
          Node vc = nm->mkNode(kind::STRING_TO_CODE, ei->d_codeTerm.get());
887
1580
          nconst_codes.push_back(vc);
888
        }
889
      }
890
    }
891
821
    if (d_im.hasProcessed())
892
    {
893
155
      return;
894
    }
895
    // now, ensure that str.code is injective
896
1332
    std::vector<Node> cmps;
897
666
    cmps.insert(cmps.end(), const_codes.rbegin(), const_codes.rend());
898
666
    cmps.insert(cmps.end(), nconst_codes.rbegin(), nconst_codes.rend());
899
1977
    for (unsigned i = 0, num_ncc = nconst_codes.size(); i < num_ncc; i++)
900
    {
901
2622
      Node c1 = nconst_codes[i];
902
1311
      cmps.pop_back();
903
7975
      for (const Node& c2 : cmps)
904
      {
905
13328
        Trace("strings-code-debug")
906
6664
            << "Compare codes : " << c1 << " " << c2 << std::endl;
907
6664
        if (!d_state.areDisequal(c1, c2) && !d_state.areEqual(c1, d_neg_one))
908
        {
909
1924
          Node eq_no = c1.eqNode(d_neg_one);
910
1924
          Node deq = c1.eqNode(c2).negate();
911
1924
          Node eqn = c1[0].eqNode(c2[0]);
912
          // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
913
1924
          Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
914
962
          deq = Rewriter::rewrite(deq);
915
962
          d_im.addPendingPhaseRequirement(deq, false);
916
1924
          std::vector<Node> emptyVec;
917
962
          d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ);
918
        }
919
      }
920
    }
921
  }
922
}
923
924
void TheoryStrings::checkRegisterTermsNormalForms()
925
{
926
  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
927
  for (const Node& eqc : seqc)
928
  {
929
    NormalForm& nfi = d_csolver.getNormalForm(eqc);
930
    // check if there is a length term for this equivalence class
931
    EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
932
    Node lt = ei ? ei->d_lengthTerm : Node::null();
933
    if (lt.isNull())
934
    {
935
      Node c = utils::mkNConcat(nfi.d_nf, eqc.getType());
936
      d_termReg.registerTerm(c, 3);
937
    }
938
  }
939
}
940
941
87923
TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
942
{
943
87923
  Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
944
87923
  if (atom.getKind() == STRING_FROM_CODE)
945
  {
946
    // str.from_code(t) --->
947
    //   witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "")
948
49
    NodeManager* nm = NodeManager::currentNM();
949
98
    Node t = atom[0];
950
98
    Node card = nm->mkConst(Rational(utils::getAlphabetCardinality()));
951
    Node cond =
952
98
        nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
953
98
    Node v = nm->mkBoundVar(nm->stringType());
954
98
    Node emp = Word::mkEmptyWord(atom.getType());
955
    Node pred = nm->mkNode(
956
98
        ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, v)), v.eqNode(emp));
957
49
    SkolemManager* sm = nm->getSkolemManager();
958
98
    Node ret = sm->mkSkolem(v, pred, "kFromCode");
959
49
    lems.push_back(SkolemLemma(ret, nullptr));
960
49
    return TrustNode::mkTrustRewrite(atom, ret, nullptr);
961
  }
962
175748
  TrustNode ret;
963
175748
  Node atomRet = atom;
964
175810
  if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
965
  {
966
    // aggressive elimination of regular expression membership
967
58
    ret = d_regexp_elim.eliminateTrusted(atomRet);
968
58
    if (!ret.isNull())
969
    {
970
96
      Trace("strings-ppr") << "  rewrote " << atom << " -> " << ret.getNode()
971
48
                           << " via regular expression elimination."
972
48
                           << std::endl;
973
48
      atomRet = ret.getNode();
974
    }
975
  }
976
87874
  return ret;
977
}
978
979
/** run the given inference step */
980
196561
void TheoryStrings::runInferStep(InferStep s, int effort)
981
{
982
196561
  Trace("strings-process") << "Run " << s;
983
196561
  if (effort > 0)
984
  {
985
28881
    Trace("strings-process") << ", effort = " << effort;
986
  }
987
196561
  Trace("strings-process") << "..." << std::endl;
988
196561
  switch (s)
989
  {
990
25148
    case CHECK_INIT: d_bsolver.checkInit(); break;
991
22063
    case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break;
992
31473
    case CHECK_EXTF_EVAL: d_esolver.checkExtfEval(effort); break;
993
20867
    case CHECK_CYCLES: d_csolver.checkCycles(); break;
994
20867
    case CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break;
995
    case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break;
996
15316
    case CHECK_NORMAL_FORMS_EQ: d_csolver.checkNormalFormsEq(); break;
997
9299
    case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break;
998
8957
    case CHECK_CODES: checkCodes(); break;
999
8653
    case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
1000
    case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
1001
19471
    case CHECK_EXTF_REDUCTION: d_esolver.checkExtfReductions(effort); break;
1002
7342
    case CHECK_MEMBERSHIP: d_rsolver.checkMemberships(); break;
1003
7105
    case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
1004
    default: Unreachable(); break;
1005
  }
1006
393122
  Trace("strings-process") << "Done " << s
1007
393122
                           << ", addedFact = " << d_im.hasPendingFact()
1008
393122
                           << ", addedLemma = " << d_im.hasPendingLemma()
1009
393122
                           << ", conflict = " << d_state.isInConflict()
1010
196561
                           << std::endl;
1011
196561
}
1012
1013
25148
void TheoryStrings::runStrategy(Theory::Effort e)
1014
{
1015
25148
  std::vector<std::pair<InferStep, int> >::iterator it = d_strat.stepBegin(e);
1016
  std::vector<std::pair<InferStep, int> >::iterator stepEnd =
1017
25148
      d_strat.stepEnd(e);
1018
1019
25148
  Trace("strings-process") << "----check, next round---" << std::endl;
1020
759610
  while (it != stepEnd)
1021
  {
1022
385274
    InferStep curr = it->first;
1023
385274
    if (curr == BREAK)
1024
    {
1025
188713
      if (d_im.hasProcessed())
1026
      {
1027
17300
        break;
1028
      }
1029
    }
1030
    else
1031
    {
1032
196561
      runInferStep(curr, it->second);
1033
196561
      if (d_state.isInConflict())
1034
      {
1035
743
        break;
1036
      }
1037
    }
1038
367231
    ++it;
1039
  }
1040
25148
  Trace("strings-process") << "----finished round---" << std::endl;
1041
25148
}
1042
1043
std::string TheoryStrings::debugPrintStringsEqc()
1044
{
1045
  std::stringstream ss;
1046
  for (unsigned t = 0; t < 2; t++)
1047
  {
1048
    eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
1049
    ss << (t == 0 ? "STRINGS:" : "OTHER:") << std::endl;
1050
    while (!eqcs2_i.isFinished())
1051
    {
1052
      Node eqc = (*eqcs2_i);
1053
      bool print = (t == 0 && eqc.getType().isStringLike())
1054
                   || (t == 1 && !eqc.getType().isStringLike());
1055
      if (print)
1056
      {
1057
        eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, d_equalityEngine);
1058
        ss << "Eqc( " << eqc << " ) : { ";
1059
        while (!eqc2_i.isFinished())
1060
        {
1061
          if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != kind::EQUAL)
1062
          {
1063
            ss << (*eqc2_i) << " ";
1064
          }
1065
          ++eqc2_i;
1066
        }
1067
        ss << " } " << std::endl;
1068
        EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
1069
        if (ei)
1070
        {
1071
          Trace("strings-eqc-debug")
1072
              << "* Length term : " << ei->d_lengthTerm.get() << std::endl;
1073
          Trace("strings-eqc-debug")
1074
              << "* Cardinality lemma k : " << ei->d_cardinalityLemK.get()
1075
              << std::endl;
1076
          Trace("strings-eqc-debug")
1077
              << "* Normalization length lemma : "
1078
              << ei->d_normalizedLength.get() << std::endl;
1079
        }
1080
      }
1081
      ++eqcs2_i;
1082
    }
1083
    ss << std::endl;
1084
  }
1085
  ss << std::endl;
1086
  return ss.str();
1087
}
1088
1089
}/* CVC4::theory::strings namespace */
1090
}/* CVC4::theory namespace */
1091
26676
}/* CVC4 namespace */