GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/core_solver.cpp Lines: 1104 1370 80.6 %
Date: 2021-03-22 Branches: 2534 6319 40.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file core_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 Implementation of the theory of strings.
13
 **
14
 ** Implementation of the theory of strings.
15
 **/
16
17
#include "theory/strings/core_solver.h"
18
19
#include "base/configuration.h"
20
#include "options/strings_options.h"
21
#include "smt/logic_exception.h"
22
#include "theory/rewriter.h"
23
#include "theory/strings/sequences_rewriter.h"
24
#include "theory/strings/strings_entail.h"
25
#include "theory/strings/theory_strings_utils.h"
26
#include "theory/strings/word.h"
27
28
using namespace std;
29
using namespace CVC4::context;
30
using namespace CVC4::kind;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace strings {
35
36
13472
CoreInferInfo::CoreInferInfo(InferenceId id) : d_infer(id), d_index(0), d_rev(false) {}
37
38
8995
CoreSolver::CoreSolver(SolverState& s,
39
                       InferenceManager& im,
40
                       TermRegistry& tr,
41
8995
                       BaseSolver& bs)
42
    : d_state(s),
43
      d_im(im),
44
      d_termReg(tr),
45
      d_bsolver(bs),
46
8995
      d_nfPairs(s.getSatContext())
47
{
48
8995
  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
49
8995
  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
50
8995
  d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
51
8995
  d_true = NodeManager::currentNM()->mkConst( true );
52
8995
  d_false = NodeManager::currentNM()->mkConst( false );
53
8995
}
54
55
8992
CoreSolver::~CoreSolver() {
56
57
8992
}
58
59
void CoreSolver::debugPrintFlatForms( const char * tc ){
60
  for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
61
    Node eqc = d_strings_eqc[k];
62
    if( d_eqc[eqc].size()>1 ){
63
      Trace( tc ) << "EQC [" << eqc << "]" << std::endl;
64
    }else{
65
      Trace( tc ) << "eqc [" << eqc << "]";
66
    }
67
    Node c = d_bsolver.getConstantEqc(eqc);
68
    if( !c.isNull() ){
69
      Trace( tc ) << "  C: " << c;
70
      if( d_eqc[eqc].size()>1 ){
71
        Trace( tc ) << std::endl;
72
      }
73
    }
74
    if( d_eqc[eqc].size()>1 ){
75
      for( unsigned i=0; i<d_eqc[eqc].size(); i++ ){
76
        Node n = d_eqc[eqc][i];
77
        Trace( tc ) << "    ";
78
        for( unsigned j=0; j<d_flat_form[n].size(); j++ ){
79
          Node fc = d_flat_form[n][j];
80
          Node fcc = d_bsolver.getConstantEqc(fc);
81
          Trace( tc ) << " ";
82
          if( !fcc.isNull() ){
83
            Trace( tc ) << fcc;
84
          }else{
85
            Trace( tc ) << fc;
86
          }
87
        }
88
        if( n!=eqc ){
89
          Trace( tc ) << ", from " << n;
90
        }
91
        Trace( tc ) << std::endl;
92
      }
93
    }else{
94
      Trace( tc ) << std::endl;
95
    }
96
  }
97
  Trace( tc ) << std::endl;
98
}
99
100
struct sortConstLength {
101
  std::map< Node, unsigned > d_const_length;
102
  bool operator() (Node i, Node j) {
103
    std::map< Node, unsigned >::iterator it_i = d_const_length.find( i );
104
    std::map< Node, unsigned >::iterator it_j = d_const_length.find( j );
105
    if( it_i==d_const_length.end() ){
106
      if( it_j==d_const_length.end() ){
107
        return i<j;
108
      }else{
109
        return false;
110
      }
111
    }else{
112
      if( it_j==d_const_length.end() ){
113
        return true;
114
      }else{
115
        return it_i->second<it_j->second;
116
      }
117
    }
118
  }
119
};
120
121
20867
void CoreSolver::checkCycles()
122
{
123
  // first check for cycles, while building ordering of equivalence classes
124
20867
  d_flat_form.clear();
125
20867
  d_flat_form_index.clear();
126
20867
  d_eqc.clear();
127
  // Rebuild strings eqc based on acyclic ordering, first copy the equivalence
128
  // classes from the base solver.
129
20867
  const std::vector<Node>& eqc = d_bsolver.getStringEqc();
130
20867
  d_strings_eqc.clear();
131
384626
  for (const Node& r : eqc)
132
  {
133
727518
    std::vector< Node > curr;
134
727518
    std::vector< Node > exp;
135
363759
    checkCycles(r, curr, exp);
136
363759
    if (d_im.hasProcessed())
137
    {
138
      return;
139
    }
140
  }
141
}
142
143
20867
void CoreSolver::checkFlatForms()
144
{
145
  // debug print flat forms
146
20867
  if (Trace.isOn("strings-ff"))
147
  {
148
    Trace("strings-ff") << "Flat forms : " << std::endl;
149
    debugPrintFlatForms("strings-ff");
150
  }
151
152
  // inferences without recursively expanding flat forms
153
154
  //(1) approximate equality by containment, infer conflicts
155
384454
  for (const Node& eqc : d_strings_eqc)
156
  {
157
727234
    Node c = d_bsolver.getConstantEqc(eqc);
158
363647
    if (!c.isNull())
159
    {
160
      // if equivalence class is constant, all component constants in flat forms
161
      // must be contained in it, in order
162
129712
      std::map<Node, std::vector<Node> >::iterator it = d_eqc.find(eqc);
163
129712
      if (it != d_eqc.end())
164
      {
165
55832
        for (const Node& n : it->second)
166
        {
167
          int firstc, lastc;
168
29538
          if (!StringsEntail::canConstantContainList(
169
29538
                  c, d_flat_form[n], firstc, lastc))
170
          {
171
120
            Trace("strings-ff-debug") << "Flat form for " << n
172
60
                                      << " cannot be contained in constant "
173
60
                                      << c << std::endl;
174
120
            Trace("strings-ff-debug") << "  indices = " << firstc << "/"
175
60
                                      << lastc << std::endl;
176
            // conflict, explanation is n = base ^ base = c ^ relevant portion
177
            // of ( n = f[n] )
178
120
            std::vector<Node> exp;
179
142
            for (int e = firstc; e <= lastc; e++)
180
            {
181
82
              if (d_flat_form[n][e].isConst())
182
              {
183
76
                Assert(e >= 0 && e < (int)d_flat_form_index[n].size());
184
76
                Assert(d_flat_form_index[n][e] >= 0
185
                       && d_flat_form_index[n][e] < (int)n.getNumChildren());
186
228
                d_im.addToExplanation(
187
152
                    n[d_flat_form_index[n][e]], d_flat_form[n][e], exp);
188
              }
189
            }
190
60
            d_bsolver.explainConstantEqc(n, eqc, exp);
191
120
            Node conc = d_false;
192
60
            d_im.sendInference(exp, conc, InferenceId::STRINGS_F_NCTN);
193
60
            return;
194
          }
195
        }
196
      }
197
    }
198
  }
199
200
  //(2) scan lists, unification to infer conflicts and equalities
201
383104
  for (const Node& eqc : d_strings_eqc)
202
  {
203
362389
    std::map<Node, std::vector<Node> >::iterator it = d_eqc.find(eqc);
204
362389
    if (it == d_eqc.end() || it->second.size() <= 1)
205
    {
206
339575
      continue;
207
    }
208
    // iterate over start index
209
84249
    for (unsigned start = 0; start < it->second.size() - 1; start++)
210
    {
211
184443
      for (unsigned r = 0; r < 2; r++)
212
      {
213
123008
        bool isRev = r == 1;
214
123008
        checkFlatForm(it->second, start, isRev);
215
123008
        if (d_state.isInConflict())
216
        {
217
184
          return;
218
        }
219
220
808862
        for (const Node& n : it->second)
221
        {
222
685946
          std::reverse(d_flat_form[n].begin(), d_flat_form[n].end());
223
685946
          std::reverse(d_flat_form_index[n].begin(),
224
685946
                       d_flat_form_index[n].end());
225
        }
226
      }
227
    }
228
  }
229
}
230
231
123008
void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
232
                                  size_t start,
233
                                  bool isRev)
234
{
235
123008
  size_t count = 0;
236
  // We check for flat form inferences involving `eqc[start]` and terms past
237
  // `start`. If there was a flat form inference involving `eqc[start]` and a
238
  // term at a smaller index `i`, we would have found it with when `start` was
239
  // `i`. Thus, we mark the preceeding terms in the equivalence class as
240
  // ineligible.
241
245924
  std::vector<Node> inelig(eqc.begin(), eqc.begin() + start + 1);
242
245924
  Node a = eqc[start];
243
246016
  Trace("strings-ff-debug")
244
123008
      << "Check flat form for a = " << a << ", whose flat form is "
245
123008
      << d_flat_form[a] << ")" << std::endl;
246
245924
  Node b;
247
  // the length explanation
248
245924
  Node lant;
249
25449
  do
250
  {
251
291563
    std::vector<Node> exp;
252
291563
    Node conc;
253
148457
    InferenceId infType = InferenceId::UNKNOWN;
254
148457
    size_t eqc_size = eqc.size();
255
148457
    size_t asize = d_flat_form[a].size();
256
148457
    if (count == asize)
257
    {
258
      for (size_t i = start + 1; i < eqc_size; i++)
259
      {
260
        b = eqc[i];
261
        if (std::find(inelig.begin(), inelig.end(), b) != inelig.end())
262
        {
263
          continue;
264
        }
265
266
        size_t bsize = d_flat_form[b].size();
267
        if (count < bsize)
268
        {
269
          Trace("strings-ff-debug")
270
              << "Found endpoint (in a) with non-empty b = " << b
271
              << ", whose flat form is " << d_flat_form[b] << std::endl;
272
          // endpoint
273
          Node emp = Word::mkEmptyWord(a.getType());
274
          std::vector<Node> conc_c;
275
          for (unsigned j = count; j < bsize; j++)
276
          {
277
            conc_c.push_back(b[d_flat_form_index[b][j]].eqNode(emp));
278
          }
279
          Assert(!conc_c.empty());
280
          conc = utils::mkAnd(conc_c);
281
          infType = InferenceId::STRINGS_F_ENDPOINT_EMP;
282
          Assert(count > 0);
283
          // swap, will enforce is empty past current
284
          a = eqc[i];
285
          b = eqc[start];
286
          break;
287
        }
288
        inelig.push_back(eqc[i]);
289
      }
290
    }
291
    else
292
    {
293
296914
      Node curr = d_flat_form[a][count];
294
296914
      Node curr_c = d_bsolver.getConstantEqc(curr);
295
296914
      Node ac = a[d_flat_form_index[a][count]];
296
296914
      std::vector<Node> lexp;
297
296914
      Node lcurr = d_state.getLength(ac, lexp);
298
547848
      for (size_t i = start + 1; i < eqc_size; i++)
299
      {
300
404742
        b = eqc[i];
301
404742
        if (std::find(inelig.begin(), inelig.end(), b) != inelig.end())
302
        {
303
36113
          continue;
304
        }
305
306
368629
        if (count == d_flat_form[b].size())
307
        {
308
          inelig.push_back(b);
309
          Trace("strings-ff-debug")
310
              << "Found endpoint in b = " << b << ", whose flat form is "
311
              << d_flat_form[b] << std::endl;
312
          // endpoint
313
          Node emp = Word::mkEmptyWord(a.getType());
314
          std::vector<Node> conc_c;
315
          for (size_t j = count; j < asize; j++)
316
          {
317
            conc_c.push_back(a[d_flat_form_index[a][j]].eqNode(emp));
318
          }
319
          Assert(!conc_c.empty());
320
          conc = utils::mkAnd(conc_c);
321
          infType = InferenceId::STRINGS_F_ENDPOINT_EMP;
322
          Assert(count > 0);
323
          break;
324
        }
325
        else
326
        {
327
731907
          Node cc = d_flat_form[b][count];
328
368629
          if (cc != curr)
329
          {
330
678725
            Node bc = b[d_flat_form_index[b][count]];
331
342038
            inelig.push_back(b);
332
342038
            Assert(!d_state.areEqual(curr, cc));
333
678725
            Node cc_c = d_bsolver.getConstantEqc(cc);
334
342038
            if (!curr_c.isNull() && !cc_c.isNull())
335
            {
336
              // check for constant conflict
337
              size_t index;
338
55270
              Node s = Word::splitConstant(cc_c, curr_c, index, isRev);
339
27681
              if (s.isNull())
340
              {
341
92
                d_bsolver.explainConstantEqc(ac,curr,exp);
342
92
                d_bsolver.explainConstantEqc(bc,cc,exp);
343
92
                conc = d_false;
344
92
                infType = InferenceId::STRINGS_F_CONST;
345
92
                break;
346
              }
347
            }
348
628714
            else if ((d_flat_form[a].size() - 1) == count
349
314357
                     && (d_flat_form[b].size() - 1) == count)
350
            {
351
2430
              conc = ac.eqNode(bc);
352
2430
              infType = InferenceId::STRINGS_F_ENDPOINT_EQ;
353
2430
              break;
354
            }
355
            else
356
            {
357
              // if lengths are the same, apply LengthEq
358
621025
              std::vector<Node> lexp2;
359
621025
              Node lcc = d_state.getLength(bc, lexp2);
360
311927
              if (d_state.areEqual(lcurr, lcc))
361
              {
362
2829
                if (Trace.isOn("strings-ff-debug"))
363
                {
364
                  Trace("strings-ff-debug")
365
                      << "Infer " << ac << " == " << bc << " since " << lcurr
366
                      << " == " << lcc << std::endl;
367
                  Trace("strings-ff-debug")
368
                      << "Explanation for " << lcurr << " is ";
369
                  for (size_t j = 0; j < lexp.size(); j++)
370
                  {
371
                    Trace("strings-ff-debug") << lexp[j] << std::endl;
372
                  }
373
                  Trace("strings-ff-debug")
374
                      << "Explanation for " << lcc << " is ";
375
                  for (size_t j = 0; j < lexp2.size(); j++)
376
                  {
377
                    Trace("strings-ff-debug") << lexp2[j] << std::endl;
378
                  }
379
                }
380
5658
                std::vector<Node> lexpc;
381
2829
                lexpc.insert(lexpc.end(), lexp.begin(), lexp.end());
382
2829
                lexpc.insert(lexpc.end(), lexp2.begin(), lexp2.end());
383
2829
                d_im.addToExplanation(lcurr, lcc, lexpc);
384
2829
                lant = utils::mkAnd(lexpc);
385
2829
                conc = ac.eqNode(bc);
386
2829
                infType = InferenceId::STRINGS_F_UNIFY;
387
2829
                break;
388
              }
389
            }
390
          }
391
        }
392
      }
393
    }
394
148457
    if (!conc.isNull())
395
    {
396
10702
      Trace("strings-ff-debug") << "Found inference (" << infType
397
5351
                                << "): " << conc << " based on equality " << a
398
5351
                                << " == " << b << ", " << isRev << std::endl;
399
      // explain why prefixes up to now were the same
400
7967
      for (size_t j = 0; j < count; j++)
401
      {
402
5232
        Trace("strings-ff-debug") << "Add at " << d_flat_form_index[a][j] << " "
403
2616
                                  << d_flat_form_index[b][j] << std::endl;
404
7848
        d_im.addToExplanation(
405
5232
            a[d_flat_form_index[a][j]], b[d_flat_form_index[b][j]], exp);
406
      }
407
      // explain why other components up to now are empty
408
16053
      for (unsigned t = 0; t < 2; t++)
409
      {
410
21404
        Node c = t == 0 ? a : b;
411
        ssize_t jj;
412
10702
        if (infType == InferenceId::STRINGS_F_ENDPOINT_EQ
413
5842
            || (t == 1 && infType == InferenceId::STRINGS_F_ENDPOINT_EMP))
414
        {
415
          // explain all the empty components for F_EndpointEq, all for
416
          // the short end for F_EndpointEmp
417
4860
          jj = isRev ? -1 : c.getNumChildren();
418
        }
419
        else
420
        {
421
8763
          jj = t == 0 ? d_flat_form_index[a][count]
422
2921
                      : d_flat_form_index[b][count];
423
        }
424
10702
        ssize_t startj = isRev ? jj + 1 : 0;
425
10702
        ssize_t endj = isRev ? c.getNumChildren() : jj;
426
21404
        Node emp = Word::mkEmptyWord(a.getType());
427
22950
        for (ssize_t j = startj; j < endj; j++)
428
        {
429
12248
          if (d_state.areEqual(c[j], emp))
430
          {
431
2156
            d_im.addToExplanation(c[j], emp, exp);
432
          }
433
        }
434
      }
435
5351
      d_im.addToExplanation(a, b, exp);
436
5351
      if (!lant.isNull())
437
      {
438
        // add the length explanation
439
2829
        exp.push_back(lant);
440
      }
441
      // Notice that F_EndpointEmp is not typically applied, since
442
      // strict prefix equality ( a.b = a ) where a,b non-empty
443
      // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
444
      // when len(b)!=0. Although if we do not infer this conflict eagerly,
445
      // it may be applied (see #3272).
446
5351
      d_im.sendInference(exp, conc, infType, isRev);
447
5351
      if (d_state.isInConflict())
448
      {
449
92
        return;
450
      }
451
5259
      break;
452
    }
453
143106
    count++;
454
143106
  } while (inelig.size() < eqc.size());
455
}
456
457
941367
Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ){
458
941367
  if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
459
    // a loop
460
    return eqc;
461
941367
  }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){
462
363759
    curr.push_back( eqc );
463
727518
    Node emp = Word::mkEmptyWord(eqc.getType());
464
    //look at all terms in this equivalence class
465
363759
    eq::EqualityEngine* ee = d_state.getEqualityEngine();
466
363759
    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee );
467
3487619
    while( !eqc_i.isFinished() ) {
468
3123860
      Node n = (*eqc_i);
469
1561930
      if( !d_bsolver.isCongruent(n) ){
470
844585
        if( n.getKind() == kind::STRING_CONCAT ){
471
251703
          Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
472
251703
          if (eqc != emp)
473
          {
474
245694
            d_eqc[eqc].push_back( n );
475
          }
476
843929
          for( unsigned i=0; i<n.getNumChildren(); i++ ){
477
1184452
            Node nr = d_state.getRepresentative(n[i]);
478
592226
            if (eqc == emp)
479
            {
480
              //for empty eqc, ensure all components are empty
481
14618
              if (nr != emp)
482
              {
483
                std::vector<Node> exps;
484
                exps.push_back(n.eqNode(emp));
485
                d_im.sendInference(
486
                    exps, n[i].eqNode(emp), InferenceId::STRINGS_I_CYCLE_E);
487
                return Node::null();
488
              }
489
            }else{
490
577608
              if (nr != emp)
491
              {
492
556121
                d_flat_form[n].push_back( nr );
493
556121
                d_flat_form_index[n].push_back( i );
494
              }
495
              //for non-empty eqc, recurse and see if we find a loop
496
1155216
              Node ncy = checkCycles( nr, curr, exp );
497
577608
              if( !ncy.isNull() ){
498
                Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
499
                d_im.addToExplanation(n, eqc, exp);
500
                d_im.addToExplanation(nr, n[i], exp);
501
                if( ncy==eqc ){
502
                  //can infer all other components must be empty
503
                  for( unsigned j=0; j<n.getNumChildren(); j++ ){
504
                    //take first non-empty
505
                    if (j != i && !d_state.areEqual(n[j], emp))
506
                    {
507
                      d_im.sendInference(
508
                          exp, n[j].eqNode(emp), InferenceId::STRINGS_I_CYCLE);
509
                      return Node::null();
510
                    }
511
                  }
512
                  Trace("strings-error") << "Looping term should be congruent : " << n << " " << eqc << " " << ncy << std::endl;
513
                  //should find a non-empty component, otherwise would have been singular congruent (I_Norm_S)
514
                  Assert(false);
515
                }else{
516
                  return ncy;
517
                }
518
              }else{
519
577608
                if (d_im.hasProcessed())
520
                {
521
                  return Node::null();
522
                }
523
              }
524
            }
525
          }
526
        }
527
      }
528
1561930
      ++eqc_i;
529
    }
530
363759
    curr.pop_back();
531
363759
    Trace("strings-eqc") << "* add string eqc: " << eqc << std::endl;
532
    //now we can add it to the list of equivalence classes
533
363759
    d_strings_eqc.push_back( eqc );
534
  }else{
535
    //already processed
536
  }
537
941367
  return Node::null();
538
}
539
540
15316
void CoreSolver::checkNormalFormsEq()
541
{
542
  // calculate normal forms for each equivalence class, possibly adding
543
  // splitting lemmas
544
15316
  d_normal_form.clear();
545
24726
  std::map<Node, Node> nf_to_eqc;
546
24726
  std::map<Node, Node> eqc_to_nf;
547
24726
  std::map<Node, Node> eqc_to_exp;
548
193264
  for (const Node& eqc : d_strings_eqc)
549
  {
550
361802
    TypeNode stype = eqc.getType();
551
367708
    Trace("strings-process-debug") << "- Verify normal forms are the same for "
552
183854
                                   << eqc << std::endl;
553
183854
    normalizeEquivalenceClass(eqc, stype);
554
183854
    Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
555
183854
    if (d_im.hasProcessed())
556
    {
557
5648
      return;
558
    }
559
178206
    NormalForm& nfe = getNormalForm(eqc);
560
356154
    Node nf_term = utils::mkNConcat(nfe.d_nf, stype);
561
178206
    std::map<Node, Node>::iterator itn = nf_to_eqc.find(nf_term);
562
178206
    if (itn != nf_to_eqc.end())
563
    {
564
258
      NormalForm& nfe_eq = getNormalForm(itn->second);
565
      // two equivalence classes have same normal form, merge
566
258
      std::vector<Node> nf_exp(nfe.d_exp.begin(), nfe.d_exp.end());
567
258
      Node eexp = eqc_to_exp[itn->second];
568
258
      if (eexp != d_true)
569
      {
570
208
        nf_exp.push_back(eexp);
571
      }
572
258
      Node eq = nfe.d_base.eqNode(nfe_eq.d_base);
573
258
      d_im.sendInference(nf_exp, eq, InferenceId::STRINGS_NORMAL_FORM);
574
258
      if (d_im.hasProcessed())
575
      {
576
258
        return;
577
      }
578
    }
579
    else
580
    {
581
177948
      nf_to_eqc[nf_term] = eqc;
582
177948
      eqc_to_nf[eqc] = nf_term;
583
177948
      eqc_to_exp[eqc] = utils::mkAnd(nfe.d_exp);
584
    }
585
355896
    Trace("strings-process-debug")
586
177948
        << "Done verifying normal forms are the same for " << eqc << std::endl;
587
  }
588
9410
  if (Trace.isOn("strings-nf"))
589
  {
590
    Trace("strings-nf") << "**** Normal forms are : " << std::endl;
591
    for (std::map<Node, Node>::iterator it = eqc_to_exp.begin();
592
         it != eqc_to_exp.end();
593
         ++it)
594
    {
595
      NormalForm& nf = getNormalForm(it->first);
596
      Trace("strings-nf") << "  N[" << it->first << "] (base " << nf.d_base
597
                          << ") = " << eqc_to_nf[it->first] << std::endl;
598
      Trace("strings-nf") << "     exp: " << it->second << std::endl;
599
    }
600
    Trace("strings-nf") << std::endl;
601
  }
602
}
603
604
//compute d_normal_forms_(base,exp,exp_depend)[eqc]
605
183854
void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype)
606
{
607
183854
  Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
608
362060
  Node emp = Word::mkEmptyWord(stype);
609
183854
  if (d_state.areEqual(eqc, emp))
610
  {
611
#ifdef CVC4_ASSERTIONS
612
9426
    for( unsigned j=0; j<d_eqc[eqc].size(); j++ ){
613
      Node n = d_eqc[eqc][j];
614
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
615
        Assert(d_state.areEqual(n[i], emp));
616
      }
617
    }
618
#endif
619
    //do nothing
620
9426
    Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
621
9426
    d_normal_form[eqc].init(emp);
622
  }
623
  else
624
  {
625
    // should not have computed the normal form of this equivalence class yet
626
174428
    Assert(d_normal_form.find(eqc) == d_normal_form.end());
627
    // Normal forms for the relevant terms in the equivalence class of eqc
628
343208
    std::vector<NormalForm> normal_forms;
629
    // map each term to its index in the above vector
630
343208
    std::map<Node, unsigned> term_to_nf_index;
631
    // get the normal forms
632
174428
    getNormalForms(eqc, normal_forms, term_to_nf_index, stype);
633
174428
    if (d_im.hasProcessed())
634
    {
635
      return;
636
    }
637
    // process the normal forms
638
174428
    processNEqc(eqc, normal_forms, stype);
639
174428
    if (d_im.hasProcessed())
640
    {
641
5648
      return;
642
    }
643
644
    //construct the normal form
645
168780
    Assert(!normal_forms.empty());
646
168780
    unsigned nf_index = 0;
647
168780
    std::map<Node, unsigned>::iterator it = term_to_nf_index.find(eqc);
648
    // we prefer taking the normal form whose base is the equivalence
649
    // class representative, since this leads to shorter explanations in
650
    // some cases.
651
168780
    if (it != term_to_nf_index.end())
652
    {
653
119111
      nf_index = it->second;
654
    }
655
168780
    d_normal_form[eqc] = normal_forms[nf_index];
656
337560
    Trace("strings-process-debug")
657
168780
        << "Return process equivalence class " << eqc
658
168780
        << " : returned = " << d_normal_form[eqc].d_nf << std::endl;
659
  }
660
}
661
662
535053
NormalForm& CoreSolver::getNormalForm(Node n)
663
{
664
535053
  std::map<Node, NormalForm>::iterator itn = d_normal_form.find(n);
665
535053
  if (itn == d_normal_form.end())
666
  {
667
    Trace("strings-warn") << "WARNING: returning empty normal form for " << n
668
                          << std::endl;
669
    // Shouln't ask for normal forms of strings that weren't computed. This
670
    // likely means that n is not a representative or not a term in the current
671
    // context. We simply return a default normal form here in this case.
672
    Assert(false);
673
    return d_normal_form[n];
674
  }
675
535053
  return itn->second;
676
}
677
678
15181
Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp)
679
{
680
15181
  if (!x.isConst())
681
  {
682
15181
    Node xr = d_state.getRepresentative(x);
683
15181
    TypeNode stype = xr.getType();
684
15181
    std::map<Node, NormalForm>::iterator it = d_normal_form.find(xr);
685
15181
    if (it != d_normal_form.end())
686
    {
687
15181
      NormalForm& nf = it->second;
688
30362
      Node ret = utils::mkNConcat(nf.d_nf, stype);
689
15181
      nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end());
690
15181
      d_im.addToExplanation(x, nf.d_base, nf_exp);
691
30362
      Trace("strings-debug")
692
15181
          << "Term: " << x << " has a normal form " << ret << std::endl;
693
15181
      return ret;
694
    }
695
    // if x does not have a normal form, then it should not occur in the
696
    // equality engine and hence should be its own representative.
697
    Assert(xr == x);
698
    if (x.getKind() == kind::STRING_CONCAT)
699
    {
700
      std::vector<Node> vec_nodes;
701
      for (unsigned i = 0; i < x.getNumChildren(); i++)
702
      {
703
        Node nc = getNormalString(x[i], nf_exp);
704
        vec_nodes.push_back(nc);
705
      }
706
      return utils::mkNConcat(vec_nodes, stype);
707
    }
708
  }
709
  return x;
710
}
711
712
8295
Node CoreSolver::getConclusion(Node x,
713
                               Node y,
714
                               PfRule rule,
715
                               bool isRev,
716
                               SkolemCache* skc,
717
                               std::vector<Node>& newSkolems)
718
{
719
16590
  Trace("strings-csolver") << "CoreSolver::getConclusion: " << x << " " << y
720
8295
                           << " " << rule << " " << isRev << std::endl;
721
8295
  NodeManager* nm = NodeManager::currentNM();
722
8295
  Node conc;
723
8295
  if (rule == PfRule::CONCAT_SPLIT || rule == PfRule::CONCAT_LPROP)
724
  {
725
5534
    Node sk1;
726
5534
    Node sk2;
727
8301
    if (options::stringUnifiedVSpt())
728
    {
729
      // must compare so that we are agnostic to order of x/y
730
5534
      Node ux = x < y ? x : y;
731
5534
      Node uy = x < y ? y : x;
732
      Node sk = skc->mkSkolemCached(ux,
733
                                    uy,
734
                                    isRev ? SkolemCache::SK_ID_V_UNIFIED_SPT_REV
735
                                          : SkolemCache::SK_ID_V_UNIFIED_SPT,
736
5534
                                    "v_spt");
737
2767
      newSkolems.push_back(sk);
738
2767
      sk1 = sk;
739
2767
      sk2 = sk;
740
    }
741
    else
742
    {
743
      sk1 = skc->mkSkolemCached(
744
          x,
745
          y,
746
          isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT,
747
          "v_spt1");
748
      sk2 = skc->mkSkolemCached(
749
          y,
750
          x,
751
          isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT,
752
          "v_spt2");
753
      newSkolems.push_back(sk1);
754
      newSkolems.push_back(sk2);
755
    }
756
5534
    Node eq1 = x.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk1, y)
757
5534
                              : nm->mkNode(STRING_CONCAT, y, sk1));
758
759
2767
    if (rule == PfRule::CONCAT_LPROP)
760
    {
761
1060
      conc = eq1;
762
    }
763
    else
764
    {
765
3414
      Node eq2 = y.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk2, x)
766
3414
                                : nm->mkNode(STRING_CONCAT, x, sk2));
767
      // make agnostic to x/y
768
1707
      conc = x < y ? nm->mkNode(OR, eq1, eq2) : nm->mkNode(OR, eq2, eq1);
769
    }
770
2767
    if (options::stringUnifiedVSpt())
771
    {
772
      // we can assume its length is greater than zero
773
5534
      Node emp = Word::mkEmptyWord(sk1.getType());
774
8301
      conc = nm->mkNode(
775
          AND,
776
          conc,
777
5534
          sk1.eqNode(emp).negate(),
778
11068
          nm->mkNode(
779
11068
              GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConst(Rational(0))));
780
2767
    }
781
  }
782
5528
  else if (rule == PfRule::CONCAT_CSPLIT)
783
  {
784
4707
    Assert(y.isConst());
785
4707
    size_t yLen = Word::getLength(y);
786
    Node firstChar =
787
9414
        yLen == 1 ? y : (isRev ? Word::suffix(y, 1) : Word::prefix(y, 1));
788
    Node sk = skc->mkSkolemCached(
789
        x,
790
        isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
791
9414
        "c_spt");
792
4707
    newSkolems.push_back(sk);
793
4707
    conc = x.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk, firstChar)
794
                          : nm->mkNode(STRING_CONCAT, firstChar, sk));
795
  }
796
821
  else if (rule == PfRule::CONCAT_CPROP)
797
  {
798
    // expect (str.++ z d) and c
799
820
    Assert(x.getKind() == STRING_CONCAT && x.getNumChildren() == 2);
800
1640
    Node z = x[isRev ? 1 : 0];
801
1640
    Node d = x[isRev ? 0 : 1];
802
820
    Assert(d.isConst());
803
1640
    Node c = y;
804
820
    Assert(c.isConst());
805
820
    size_t cLen = Word::getLength(c);
806
820
    size_t p = getSufficientNonEmptyOverlap(c, d, isRev);
807
    Node preC =
808
1640
        p == cLen ? c : (isRev ? Word::suffix(c, p) : Word::prefix(c, p));
809
    Node sk = skc->mkSkolemCached(
810
        z,
811
        preC,
812
        isRev ? SkolemCache::SK_ID_C_SPT_REV : SkolemCache::SK_ID_C_SPT,
813
1640
        "c_spt");
814
820
    newSkolems.push_back(sk);
815
820
    conc = z.eqNode(isRev ? nm->mkNode(STRING_CONCAT, sk, preC)
816
                          : nm->mkNode(STRING_CONCAT, preC, sk));
817
  }
818
819
8295
  return conc;
820
}
821
822
3450
size_t CoreSolver::getSufficientNonEmptyOverlap(Node c, Node d, bool isRev)
823
{
824
3450
  Assert(c.isConst() && c.getType().isStringLike());
825
3450
  Assert(d.isConst() && d.getType().isStringLike());
826
  size_t p;
827
  size_t p2;
828
3450
  size_t cLen = Word::getLength(c);
829
3450
  if (isRev)
830
  {
831
    // Since non-empty, we start with character 1
832
3938
    Node c1 = Word::prefix(c, cLen - 1);
833
1969
    p = cLen - Word::roverlap(c1, d);
834
1969
    p2 = Word::rfind(c1, d);
835
  }
836
  else
837
  {
838
2962
    Node c1 = Word::substr(c, 1);
839
1481
    p = cLen - Word::overlap(c1, d);
840
1481
    p2 = Word::find(c1, d);
841
  }
842
3450
  return p2 == std::string::npos ? p : (p > p2 + 1 ? p2 + 1 : p);
843
}
844
845
30
Node CoreSolver::getDecomposeConclusion(Node x,
846
                                        Node l,
847
                                        bool isRev,
848
                                        SkolemCache* skc,
849
                                        std::vector<Node>& newSkolems)
850
{
851
30
  Assert(l.getType().isInteger());
852
30
  NodeManager* nm = NodeManager::currentNM();
853
60
  Node n = isRev ? nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), l) : l;
854
60
  Node sk1 = skc->mkSkolemCached(x, n, SkolemCache::SK_PREFIX, "dc_spt1");
855
30
  newSkolems.push_back(sk1);
856
60
  Node sk2 = skc->mkSkolemCached(x, n, SkolemCache::SK_SUFFIX_REM, "dc_spt2");
857
30
  newSkolems.push_back(sk2);
858
60
  Node conc = x.eqNode(nm->mkNode(STRING_CONCAT, sk1, sk2));
859
  // add the length constraint to the conclusion
860
60
  Node lc = nm->mkNode(STRING_LENGTH, isRev ? sk2 : sk1).eqNode(l);
861
60
  return nm->mkNode(AND, conc, lc);
862
}
863
864
174428
void CoreSolver::getNormalForms(Node eqc,
865
                                std::vector<NormalForm>& normal_forms,
866
                                std::map<Node, unsigned>& term_to_nf_index,
867
                                TypeNode stype)
868
{
869
348856
  Node emp = Word::mkEmptyWord(stype);
870
  //constant for equivalence class
871
348856
  Node eqc_non_c = eqc;
872
174428
  Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
873
174428
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
874
174428
  eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee );
875
1560986
  while( !eqc_i.isFinished() ){
876
1386558
    Node n = (*eqc_i);
877
693279
    if( !d_bsolver.isCongruent(n) ){
878
392489
      Kind nk = n.getKind();
879
392489
      bool isCLike = utils::isConstantLike(n);
880
392489
      if (isCLike || nk == STRING_CONCAT)
881
      {
882
175631
        Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
883
351262
        NormalForm nf_curr;
884
175631
        if (isCLike)
885
        {
886
53743
          nf_curr.init(n);
887
        }
888
121888
        else if (nk == STRING_CONCAT)
889
        {
890
          // set the base to n, we construct the other portions of nf_curr in
891
          // the following.
892
121888
          nf_curr.d_base = n;
893
407537
          for( unsigned i=0; i<n.getNumChildren(); i++ ) {
894
571298
            Node nr = ee->getRepresentative( n[i] );
895
            // get the normal form for the component
896
285649
            NormalForm& nfr = getNormalForm(nr);
897
285649
            std::vector<Node>& nfrv = nfr.d_nf;
898
571298
            Trace("strings-process-debug")
899
571298
                << "Normalizing subterm " << n[i] << " = " << nr
900
285649
                << ", which is " << nfrv << std::endl;
901
285649
            unsigned orig_size = nf_curr.d_nf.size();
902
285649
            unsigned add_size = nfrv.size();
903
            //if not the empty string, add to current normal form
904
285649
            if (!nfrv.empty())
905
            {
906
              // if in a build with assertions, we run the following block,
907
              // which checks that normal forms do not have concat terms.
908
276440
              if (Configuration::isAssertionBuild())
909
              {
910
786537
                for (const Node& nn : nfrv)
911
                {
912
510097
                  if (Trace.isOn("strings-error"))
913
                  {
914
                    if (nn.getKind() == STRING_CONCAT)
915
                    {
916
                      Trace("strings-error")
917
                          << "Strings::Error: From eqc = " << eqc << ", " << n
918
                          << " index " << i << ", bad normal form : ";
919
                      for (unsigned rr = 0; rr < nfrv.size(); rr++)
920
                      {
921
                        Trace("strings-error") << nfrv[rr] << " ";
922
                      }
923
                      Trace("strings-error") << std::endl;
924
                    }
925
                  }
926
510097
                  Assert(nn.getKind() != kind::STRING_CONCAT);
927
                }
928
              }
929
276440
              nf_curr.d_nf.insert(nf_curr.d_nf.end(), nfrv.begin(), nfrv.end());
930
            }
931
            // Track explanation for the normal form. This is in two parts.
932
            // First, we must carry the explanation of the normal form computed
933
            // for the representative nr.
934
462675
            for (const Node& exp : nfr.d_exp)
935
            {
936
              // The explanation is only relevant for the subsegment it was
937
              // previously relevant for, shifted now based on its relative
938
              // placement in the normal form of n.
939
354052
              nf_curr.addToExplanation(
940
                  exp,
941
354052
                  orig_size + nfr.d_expDep[exp][false],
942
354052
                  orig_size + (add_size - nfr.d_expDep[exp][true]));
943
            }
944
            // Second, must explain that the component n[i] is equal to the
945
            // base of the normal form for nr.
946
571298
            Node base = nfr.d_base;
947
285649
            if (base != n[i])
948
            {
949
303618
              Node eq = n[i].eqNode(base);
950
              // The equality is relevant for the entire current segment
951
151809
              nf_curr.addToExplanation(eq, orig_size, orig_size + add_size);
952
            }
953
          }
954
          // Now that we are finished with the loop, we convert forward indices
955
          // to reverse indices in the explanation dependency information
956
121888
          int total_size = nf_curr.d_nf.size();
957
327637
          for (std::pair<const Node, std::map<bool, unsigned> >& ed :
958
121888
               nf_curr.d_expDep)
959
          {
960
327637
            ed.second[true] = total_size - ed.second[true];
961
327637
            Assert(ed.second[true] >= 0);
962
          }
963
        }
964
        //if not equal to self
965
175631
        std::vector<Node>& currv = nf_curr.d_nf;
966
351262
        if (currv.size() > 1
967
351262
            || (currv.size() == 1 && utils::isConstantLike(currv[0])))
968
        {
969
          // if in a build with assertions, check that normal form is acyclic
970
175631
          if (Configuration::isAssertionBuild())
971
          {
972
175631
            if (currv.size() > 1)
973
            {
974
631985
              for (unsigned i = 0; i < currv.size(); i++)
975
              {
976
510097
                if (Trace.isOn("strings-error"))
977
                {
978
                  Trace("strings-error") << "Cycle for normal form ";
979
                  utils::printConcatTrace(currv, "strings-error");
980
                  Trace("strings-error") << "..." << currv[i] << std::endl;
981
                }
982
510097
                Assert(!d_state.areEqual(currv[i], n));
983
              }
984
            }
985
          }
986
175631
          term_to_nf_index[n] = normal_forms.size();
987
175631
          normal_forms.push_back(nf_curr);
988
        }else{
989
          //this was redundant: combination of self + empty string(s)
990
          Node nn = currv.size() == 0 ? emp : currv[0];
991
          Assert(d_state.areEqual(nn, eqc));
992
175631
        }
993
      }else{
994
216858
        eqc_non_c = n;
995
      }
996
    }
997
    else
998
    {
999
601580
      Trace("strings-process-debug")
1000
300790
          << "Get Normal Form : term " << n << " in eqc " << eqc
1001
300790
          << " is congruent" << std::endl;
1002
    }
1003
693279
    ++eqc_i;
1004
  }
1005
1006
174428
  if( normal_forms.empty() ) {
1007
40163
    Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
1008
    // This case happens when there are no non-trivial normal forms for this
1009
    // equivalence class. For example, given assertions:
1010
    //   { x = y ++ z, x = y, z = "" }
1011
    // The equivalence class of { x, y, y ++ z } is such that the normal form
1012
    // of all terms is a variable (either x or y) in the equivalence class
1013
    // itself. Thus, the normal form of this equivalence class can be assigned
1014
    // to one of these variables.
1015
    // We use a non-concatenation term among the terms in this equivalence
1016
    // class, which is stored in eqc_non_c. The reason is this does not require
1017
    // an explanation, whereas e.g. y ++ z would require the explanation z = ""
1018
    // to justify its normal form is y.
1019
40163
    Assert(eqc_non_c.getKind() != STRING_CONCAT);
1020
80326
    NormalForm nf_triv;
1021
40163
    nf_triv.init(eqc_non_c);
1022
40163
    normal_forms.push_back(nf_triv);
1023
  }else{
1024
134265
    if(Trace.isOn("strings-solve")) {
1025
      Trace("strings-solve") << "--- Normal forms for equivalance class " << eqc << " : " << std::endl;
1026
      for (unsigned i = 0, size = normal_forms.size(); i < size; i++)
1027
      {
1028
        NormalForm& nf = normal_forms[i];
1029
        Trace("strings-solve") << "#" << i << " (from " << nf.d_base << ") : ";
1030
        for (unsigned j = 0, sizej = nf.d_nf.size(); j < sizej; j++)
1031
        {
1032
          if(j>0) {
1033
            Trace("strings-solve") << ", ";
1034
          }
1035
          Trace("strings-solve") << nf.d_nf[j];
1036
        }
1037
        Trace("strings-solve") << std::endl;
1038
        Trace("strings-solve") << "   Explanation is : ";
1039
        if (nf.d_exp.size() == 0)
1040
        {
1041
          Trace("strings-solve") << "NONE";
1042
        } else {
1043
          for (unsigned j = 0, sizej = nf.d_exp.size(); j < sizej; j++)
1044
          {
1045
            if(j>0) {
1046
              Trace("strings-solve") << " AND ";
1047
            }
1048
            Trace("strings-solve") << nf.d_exp[j];
1049
          }
1050
          Trace("strings-solve") << std::endl;
1051
          Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl;
1052
          for (unsigned j = 0, sizej = nf.d_exp.size(); j < sizej; j++)
1053
          {
1054
            Node exp = nf.d_exp[j];
1055
            Trace("strings-solve") << "   " << exp << " -> ";
1056
            Trace("strings-solve") << nf.d_expDep[exp][false] << ",";
1057
            Trace("strings-solve") << nf.d_expDep[exp][true] << std::endl;
1058
          }
1059
        }
1060
        Trace("strings-solve") << std::endl;
1061
      }
1062
    } else {
1063
134265
      Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
1064
    }
1065
  }
1066
174428
}
1067
1068
174428
void CoreSolver::processNEqc(Node eqc,
1069
                             std::vector<NormalForm>& normal_forms,
1070
                             TypeNode stype)
1071
{
1072
174428
  if (normal_forms.size() <= 1)
1073
  {
1074
325191
    return;
1075
  }
1076
  // if equivalence class is constant, approximate as containment, infer
1077
  // conflicts
1078
23665
  Node c = d_bsolver.getConstantEqc(eqc);
1079
  // the possible inferences
1080
23665
  std::vector<CoreInferInfo> pinfer;
1081
  // compute normal forms that are effectively unique
1082
23665
  std::unordered_map<Node, size_t, NodeHashFunction> nfCache;
1083
23665
  std::vector<size_t> nfIndices;
1084
21540
  bool hasConstIndex = false;
1085
84046
  for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++)
1086
  {
1087
62714
    NormalForm& nfi = normal_forms[i];
1088
125220
    Node ni = utils::mkNConcat(nfi.d_nf, stype);
1089
62714
    if (nfCache.find(ni) == nfCache.end())
1090
    {
1091
      // If the equivalence class is entailed to be constant, check
1092
      // if the normal form cannot be contained in that constant.
1093
30790
      if (!c.isNull())
1094
      {
1095
        int firstc, lastc;
1096
13890
        if (!StringsEntail::canConstantContainList(c, nfi.d_nf, firstc, lastc))
1097
        {
1098
416
          Node n = nfi.d_base;
1099
416
          std::vector<Node> exp(nfi.d_exp.begin(), nfi.d_exp.end());
1100
          //conflict
1101
208
          Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl;
1102
          // conflict, explanation is:
1103
          //  n = base ^ base = c ^ relevant porition of ( n = N[n] )
1104
          // Notice although not implemented, this can be minimized based on
1105
          // firstc/lastc, normal_forms_exp_depend.
1106
208
          d_bsolver.explainConstantEqc(n, eqc, exp);
1107
208
          d_im.sendInference(exp, d_false, InferenceId::STRINGS_N_NCTN);
1108
          // conflict, finished
1109
208
          return;
1110
        }
1111
      }
1112
1113
30582
      nfCache[ni] = i;
1114
30582
      if (ni.isConst())
1115
      {
1116
12665
        hasConstIndex = true;
1117
12665
        nfIndices.insert(nfIndices.begin(), i);
1118
      }
1119
      else
1120
      {
1121
17917
        nfIndices.push_back(i);
1122
      }
1123
    }
1124
  }
1125
21332
  size_t nnfs = nfIndices.size();
1126
42664
  Trace("strings-solve") << "CoreSolver::processNEqc: " << nnfs << "/"
1127
42664
                         << normal_forms.size() << " normal forms are unique."
1128
21332
                         << std::endl;
1129
1130
  // loop over all pairs
1131
24061
  for (unsigned i = 0; i < nnfs - 1; i++)
1132
  {
1133
    //unify each normalform[j] with normal_forms[i]
1134
12788
    for (unsigned j = i + 1; j < nnfs; j++)
1135
    {
1136
9553
      NormalForm& nfi = normal_forms[nfIndices[i]];
1137
9553
      NormalForm& nfj = normal_forms[nfIndices[j]];
1138
      //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality, add to pinfer if not
1139
9553
      Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
1140
9553
      if (isNormalFormPair(nfi.d_base, nfj.d_base))
1141
      {
1142
        Trace("strings-solve") << "Strings: Already cached." << std::endl;
1143
        continue;
1144
      }
1145
      // process the reverse direction first (check for easy conflicts and
1146
      // inferences)
1147
9553
      unsigned rindex = 0;
1148
9553
      nfi.reverse();
1149
9553
      nfj.reverse();
1150
9553
      processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
1151
9553
      nfi.reverse();
1152
9553
      nfj.reverse();
1153
9553
      if (d_im.hasProcessed())
1154
      {
1155
5634
        break;
1156
      }
1157
      // AJR: for less aggressive endpoint inference
1158
      // rindex = 0;
1159
1160
7196
      unsigned index = 0;
1161
7196
      processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
1162
7196
      if (d_im.hasProcessed())
1163
      {
1164
920
        break;
1165
      }
1166
    }
1167
6512
    if (hasConstIndex || d_im.hasProcessed())
1168
    {
1169
3783
      break;
1170
    }
1171
  }
1172
21332
  if (d_state.isInConflict())
1173
  {
1174
    // conflict, we are done
1175
75
    return;
1176
  }
1177
  // Go back and check for normal form equality conflicts. These take
1178
  // precedence over any facts and lemmas.
1179
42345
  for (const std::pair<const Node, size_t>& ni : nfCache)
1180
  {
1181
64250
    for (const std::pair<const Node, size_t>& nj : nfCache)
1182
    {
1183
39960
      if (ni.first >= nj.first)
1184
      {
1185
        // avoid duplicate comparisons
1186
33088
        continue;
1187
      }
1188
13706
      Node eq = ni.first.eqNode(nj.first);
1189
6872
      eq = Rewriter::rewrite(eq);
1190
6872
      if (eq == d_false)
1191
      {
1192
76
        std::vector<Node> exp;
1193
38
        NormalForm& nfi = normal_forms[ni.second];
1194
38
        NormalForm& nfj = normal_forms[nj.second];
1195
38
        exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
1196
38
        exp.insert(exp.end(), nfj.d_exp.begin(), nfj.d_exp.end());
1197
38
        exp.push_back(nfi.d_base.eqNode(nfj.d_base));
1198
38
        d_im.sendInference(exp, d_false, InferenceId::STRINGS_N_EQ_CONF);
1199
38
        return;
1200
      }
1201
    }
1202
24290
    if (d_im.hasProcessed())
1203
    {
1204
3202
      break;
1205
    }
1206
  }
1207
21219
  if (d_im.hasProcessed() || pinfer.empty())
1208
  {
1209
    // either already sent a lemma or fact, or there are no possible inferences
1210
19094
    return;
1211
  }
1212
  // now, determine which of the possible inferences we want to add
1213
2125
  unsigned use_index = 0;
1214
2125
  bool set_use_index = false;
1215
4250
  Trace("strings-solve") << "Possible inferences (" << pinfer.size()
1216
2125
                         << ") : " << std::endl;
1217
2125
  InferenceId min_id = InferenceId::UNKNOWN;
1218
2125
  unsigned max_index = 0;
1219
11831
  for (unsigned i = 0, psize = pinfer.size(); i < psize; i++)
1220
  {
1221
9706
    CoreInferInfo& ipii = pinfer[i];
1222
9706
    InferInfo& ii = ipii.d_infer;
1223
19412
    Trace("strings-solve") << "#" << i << ": From " << ipii.d_i << " / "
1224
9706
                           << ipii.d_j << " (rev=" << ipii.d_rev << ") : ";
1225
9706
    Trace("strings-solve") << ii.d_conc << " by " << ii.getId() << std::endl;
1226
26993
    if (!set_use_index || ii.getId() < min_id
1227
16451
        || (ii.getId() == min_id && ipii.d_index > max_index))
1228
    {
1229
3381
      min_id = ii.getId();
1230
3381
      max_index = ipii.d_index;
1231
3381
      use_index = i;
1232
3381
      set_use_index = true;
1233
    }
1234
  }
1235
2125
  Trace("strings-solve") << "...choose #" << use_index << std::endl;
1236
2125
  if (!processInferInfo(pinfer[use_index]))
1237
  {
1238
    Unhandled() << "Failed to process infer info " << pinfer[use_index].d_infer
1239
                << std::endl;
1240
  }
1241
}
1242
1243
16749
void CoreSolver::processSimpleNEq(NormalForm& nfi,
1244
                                  NormalForm& nfj,
1245
                                  unsigned& index,
1246
                                  bool isRev,
1247
                                  unsigned rproc,
1248
                                  std::vector<CoreInferInfo>& pinfer,
1249
                                  TypeNode stype)
1250
{
1251
16749
  NodeManager* nm = NodeManager::currentNM();
1252
33468
  Node emp = Word::mkEmptyWord(stype);
1253
1254
16749
  const std::vector<Node>& nfiv = nfi.d_nf;
1255
16749
  const std::vector<Node>& nfjv = nfj.d_nf;
1256
16749
  Assert(rproc <= nfiv.size() && rproc <= nfjv.size());
1257
  while (true)
1258
  {
1259
38533
    bool lhsDone = (index == (nfiv.size() - rproc));
1260
38533
    bool rhsDone = (index == (nfjv.size() - rproc));
1261
38533
    if (lhsDone && rhsDone)
1262
    {
1263
      // We are done with both normal forms
1264
      break;
1265
    }
1266
38533
    else if (lhsDone || rhsDone)
1267
    {
1268
      // Only one side is done so the remainder of the other side must be empty
1269
      NormalForm& nfk = index == (nfiv.size() - rproc) ? nfj : nfi;
1270
      std::vector<Node>& nfkv = nfk.d_nf;
1271
      unsigned index_k = index;
1272
      std::vector<Node> curr_exp;
1273
      NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, curr_exp);
1274
      while (!d_state.isInConflict() && index_k < (nfkv.size() - rproc))
1275
      {
1276
        // can infer that this string must be empty
1277
        Node eq = nfkv[index_k].eqNode(emp);
1278
        Assert(!d_state.areEqual(emp, nfkv[index_k]));
1279
        d_im.sendInference(curr_exp, eq, InferenceId::STRINGS_N_ENDPOINT_EMP, isRev);
1280
        index_k++;
1281
      }
1282
      break;
1283
    }
1284
1285
    // We have inferred that the normal forms up to position `index` are
1286
    // equivalent. Below, we refer to the components at the current position of
1287
    // the normal form as `x` and `y`.
1288
    //
1289
    // E.g. x ++ ... = y ++ ...
1290
38533
    Node x = nfiv[index];
1291
38533
    Node y = nfjv[index];
1292
77066
    Trace("strings-solve-debug")
1293
38533
        << "Process " << x << " ... " << y << std::endl;
1294
1295
55605
    if (x == y)
1296
    {
1297
      // The normal forms have the same term at the current position. We just
1298
      // continue with the next index. By construction of the normal forms, we
1299
      // end up in this case if the two components are equal according to the
1300
      // equality engine (i.e. we cannot have different x and y terms that are
1301
      // equal in the equality engine).
1302
      //
1303
      // E.g. x ++ x' ++ ... = x ++ y' ++ ... ---> x' ++ ... = y' ++ ...
1304
34144
      Trace("strings-solve-debug")
1305
17072
          << "Simple Case 1 : strings are equal" << std::endl;
1306
17072
      index++;
1307
17072
      continue;
1308
    }
1309
21461
    Assert(!d_state.areEqual(x, y));
1310
1311
21461
    std::vector<Node> lenExp;
1312
21461
    Node xLenTerm = d_state.getLength(x, lenExp);
1313
21461
    Node yLenTerm = d_state.getLength(y, lenExp);
1314
1315
21461
    if (d_state.areEqual(xLenTerm, yLenTerm))
1316
    {
1317
2365
      std::vector<Node> ant;
1318
2365
      NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, ant);
1319
2365
      if (x.isConst() && y.isConst())
1320
      {
1321
        // if both are constant, it's just a constant conflict
1322
30
        d_im.sendInference(ant, d_false, InferenceId::STRINGS_N_CONST, isRev, true);
1323
30
        return;
1324
      }
1325
      // `x` and `y` have the same length. We infer that the two components
1326
      // have to be the same.
1327
      //
1328
      // E.g. x ++ ... = y ++ ... ^ len(x) = len(y) ---> x = y
1329
4670
      Trace("strings-solve-debug")
1330
2335
          << "Simple Case 2 : string lengths are equal" << std::endl;
1331
4670
      Node eq = x.eqNode(y);
1332
4670
      Node leneq = xLenTerm.eqNode(yLenTerm);
1333
2335
      lenExp.push_back(leneq);
1334
      // set the explanation for length
1335
4670
      Node lant = utils::mkAnd(lenExp);
1336
2335
      ant.push_back(lant);
1337
2335
      d_im.sendInference(ant, eq, InferenceId::STRINGS_N_UNIFY, isRev);
1338
2335
      break;
1339
    }
1340
47723
    else if ((!x.isConst() && index == nfiv.size() - rproc - 1)
1341
37832
             || (!y.isConst() && index == nfjv.size() - rproc - 1))
1342
    {
1343
      // We have reached the last component in one of the normal forms and it
1344
      // is not a constant. Thus, the last component must be equal to the
1345
      // remainder of the other normal form.
1346
      //
1347
      // E.g. x = y ++ y' ---> x = y ++ y'
1348
1734
      Trace("strings-solve-debug")
1349
867
          << "Simple Case 3 : at endpoint" << std::endl;
1350
1734
      Node eqn[2];
1351
2601
      for (unsigned r = 0; r < 2; r++)
1352
      {
1353
1734
        const NormalForm& nfk = r == 0 ? nfi : nfj;
1354
1734
        const std::vector<Node>& nfkv = nfk.d_nf;
1355
3468
        std::vector<Node> eqnc;
1356
4332
        for (unsigned i = index, size = (nfkv.size() - rproc); i < size; i++)
1357
        {
1358
2598
          if (isRev)
1359
          {
1360
1412
            eqnc.insert(eqnc.begin(), nfkv[i]);
1361
          }
1362
          else
1363
          {
1364
1186
            eqnc.push_back(nfkv[i]);
1365
          }
1366
        }
1367
1734
        eqn[r] = utils::mkNConcat(eqnc, stype);
1368
      }
1369
1734
      Trace("strings-solve-debug")
1370
867
          << "Endpoint eq check: " << eqn[0] << " " << eqn[1] << std::endl;
1371
867
      if (!d_state.areEqual(eqn[0], eqn[1]))
1372
      {
1373
1734
        std::vector<Node> antec;
1374
867
        NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, antec);
1375
1734
        d_im.sendInference(antec,
1376
1734
                           eqn[0].eqNode(eqn[1]),
1377
                           InferenceId::STRINGS_N_ENDPOINT_EQ,
1378
                           isRev,
1379
                           true);
1380
      }
1381
      else
1382
      {
1383
        Assert(nfiv.size() == nfjv.size());
1384
        index = nfiv.size() - rproc;
1385
      }
1386
867
      break;
1387
    }
1388
18229
    else if (x.isConst() && y.isConst())
1389
    {
1390
      // Constants in both normal forms.
1391
      //
1392
      // E.g. "abc" ++ ... = "ab" ++ ...
1393
4757
      size_t lenX = Word::getLength(x);
1394
4757
      size_t lenY = Word::getLength(y);
1395
9514
      Trace("strings-solve-debug")
1396
4757
          << "Simple Case 4 : Const Split : " << x << " vs " << y
1397
4757
          << " at index " << index << ", isRev = " << isRev << std::endl;
1398
4757
      size_t minLen = std::min(lenX, lenY);
1399
      bool isSameFix =
1400
4757
          isRev ? Word::rstrncmp(x, y, minLen) : Word::strncmp(x, y, minLen);
1401
4757
      if (isSameFix)
1402
      {
1403
        // The shorter constant is a prefix/suffix of the longer constant. We
1404
        // split the longer constant into the shared part and the remainder and
1405
        // continue from there.
1406
        //
1407
        // E.g. "abc" ++ x' ++ ... = "ab" ++ y' ++ ... --->
1408
        //      "c" ++ x' ++ ... = y' ++ ...
1409
4712
        bool xShorter = lenX < lenY;
1410
4712
        NormalForm& nfl = xShorter ? nfj : nfi;
1411
9424
        Node cl = xShorter ? y : x;
1412
9424
        Node ns = xShorter ? x : y;
1413
1414
9424
        Node remainderStr;
1415
4712
        if (isRev)
1416
        {
1417
3333
          size_t newlen = std::max(lenX, lenY) - minLen;
1418
3333
          remainderStr = Word::substr(cl, 0, newlen);
1419
        }
1420
        else
1421
        {
1422
1379
          remainderStr = Word::substr(cl, minLen);
1423
        }
1424
9424
        Trace("strings-solve-debug-test")
1425
4712
            << "Break normal form of " << cl << " into " << ns << ", "
1426
4712
            << remainderStr << std::endl;
1427
4712
        nfl.splitConstant(index, ns, remainderStr);
1428
4712
        index++;
1429
4712
        continue;
1430
      }
1431
      else
1432
      {
1433
        // Conflict because the shorter constant is not a prefix/suffix of the
1434
        // other.
1435
        //
1436
        // E.g. "abc" ++ ... = "bc" ++ ... ---> conflict
1437
90
        std::vector<Node> antec;
1438
45
        NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, antec);
1439
45
        d_im.sendInference(antec, d_false, InferenceId::STRINGS_N_CONST, isRev, true);
1440
45
        break;
1441
      }
1442
    }
1443
1444
    // The candidate inference "info"
1445
26944
    CoreInferInfo info(InferenceId::UNKNOWN);
1446
13472
    InferInfo& iinfo = info.d_infer;
1447
13472
    info.d_index = index;
1448
    // for debugging
1449
13472
    info.d_i = nfi.d_base;
1450
13472
    info.d_j = nfj.d_base;
1451
13472
    info.d_rev = isRev;
1452
13472
    Assert(index < nfiv.size() - rproc && index < nfjv.size() - rproc);
1453
63100
    if (!d_state.areDisequal(xLenTerm, yLenTerm) && !d_state.areEqual(xLenTerm, yLenTerm)
1454
9212
        && !x.isConst()
1455
59722
        && !y.isConst())  // AJR: remove the latter 2 conditions?
1456
    {
1457
      // We don't know whether `x` and `y` have the same length or not. We
1458
      // split on whether they are equal or not (note that splitting on
1459
      // equality between strings is worse since it is harder to process).
1460
      //
1461
      // E.g. x ++ ... = y ++ ... ---> (len(x) = len(y)) v (len(x) != len(y))
1462
9870
      Trace("strings-solve-debug")
1463
4935
          << "Non-simple Case 1 : string lengths neither equal nor disequal"
1464
4935
          << std::endl;
1465
9870
      Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm);
1466
4935
      lenEq = Rewriter::rewrite(lenEq);
1467
4935
      iinfo.d_conc = nm->mkNode(OR, lenEq, lenEq.negate());
1468
4935
      iinfo.setId(InferenceId::STRINGS_LEN_SPLIT);
1469
4935
      info.d_pendingPhase[lenEq] = true;
1470
4935
      pinfer.push_back(info);
1471
4935
      break;
1472
    }
1473
1474
17074
    Trace("strings-solve-debug")
1475
8537
        << "Non-simple Case 2 : must compare strings" << std::endl;
1476
8537
    int lhsLoopIdx = -1;
1477
8537
    int rhsLoopIdx = -1;
1478
8537
    if (detectLoop(nfi, nfj, index, lhsLoopIdx, rhsLoopIdx, rproc))
1479
    {
1480
      // We are dealing with a looping word equation.
1481
      // Note we could make this code also run in the reverse direction, but
1482
      // this is not implemented currently.
1483
482
      if (!isRev)
1484
      {
1485
        // add temporarily to the antecedant of iinfo.
1486
420
        NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, iinfo.d_premises);
1487
        ProcessLoopResult plr =
1488
1260
            processLoop(lhsLoopIdx != -1 ? nfi : nfj,
1489
420
                        lhsLoopIdx != -1 ? nfj : nfi,
1490
420
                        lhsLoopIdx != -1 ? lhsLoopIdx : rhsLoopIdx,
1491
420
                        index,
1492
420
                        info);
1493
420
        if (plr == ProcessLoopResult::INFERENCE)
1494
        {
1495
420
          pinfer.push_back(info);
1496
420
          break;
1497
        }
1498
        else if (plr == ProcessLoopResult::CONFLICT)
1499
        {
1500
          break;
1501
        }
1502
        Assert(plr == ProcessLoopResult::SKIPPED);
1503
        // not processing an inference here, undo changes to ant
1504
        iinfo.d_premises.clear();
1505
      }
1506
    }
1507
1508
    // AJR: length entailment here?
1509
8117
    if (x.isConst() || y.isConst())
1510
    {
1511
      // Below, we deal with the case where `x` or `y` is a constant string. We
1512
      // refer to the non-constant component as `nc` below.
1513
      //
1514
      // E.g. "abc" ++ ... = nc ++ ...
1515
5370
      Assert(!x.isConst() || !y.isConst());
1516
5370
      NormalForm& nfc = x.isConst() ? nfi : nfj;
1517
5370
      const std::vector<Node>& nfcv = nfc.d_nf;
1518
5370
      NormalForm& nfnc = x.isConst() ? nfj : nfi;
1519
5370
      const std::vector<Node>& nfncv = nfnc.d_nf;
1520
10740
      Node nc = nfncv[index];
1521
5370
      Assert(!nc.isConst()) << "Other string is not constant.";
1522
5370
      Assert(nc.getKind() != STRING_CONCAT) << "Other string is not CONCAT.";
1523
      // explanation for why nc is non-empty
1524
10740
      Node expNonEmpty = d_state.explainNonEmpty(nc);
1525
5370
      if (expNonEmpty.isNull())
1526
      {
1527
        // The non-constant side may be equal to the empty string. Split on
1528
        // whether it is.
1529
        //
1530
        // E.g. "abc" ++ ... = nc ++ ... ---> (nc = "") v (nc != "")
1531
        Node eq = nc.eqNode(emp);
1532
        eq = Rewriter::rewrite(eq);
1533
        if (eq.isConst())
1534
        {
1535
          // If the equality rewrites to a constant, we must use the
1536
          // purify variable for this string to communicate that
1537
          // we have inferred whether it is empty.
1538
          SkolemCache* skc = d_termReg.getSkolemCache();
1539
          Node p = skc->mkSkolemCached(nc, SkolemCache::SK_PURIFY, "lsym");
1540
          Node pEq = p.eqNode(emp);
1541
          // should not be constant
1542
          Assert(!Rewriter::rewrite(pEq).isConst());
1543
          // infer the purification equality, and the (dis)equality
1544
          // with the empty string in the direction that the rewriter
1545
          // inferred
1546
          iinfo.d_conc = nm->mkNode(
1547
              AND, p.eqNode(nc), !eq.getConst<bool>() ? pEq.negate() : pEq);
1548
          iinfo.setId(InferenceId::STRINGS_INFER_EMP);
1549
        }
1550
        else
1551
        {
1552
          iinfo.d_conc = nm->mkNode(OR, eq, eq.negate());
1553
          iinfo.setId(InferenceId::STRINGS_LEN_SPLIT_EMP);
1554
        }
1555
        pinfer.push_back(info);
1556
        break;
1557
      }
1558
1559
      // At this point, we know that `nc` is non-empty, so we add expNonEmpty
1560
      // to our explanation below. We do this after adding other parts of the
1561
      // explanation for consistency with other inferences.
1562
1563
5370
      size_t ncIndex = index + 1;
1564
10740
      Node nextConstStr = nfnc.collectConstantStringAt(ncIndex);
1565
5370
      if (!nextConstStr.isNull())
1566
      {
1567
        // We are in the case where we have a constant after `nc`, so we
1568
        // split `nc`.
1569
        //
1570
        // E.g. "abc" ++ ... = nc ++ "b" ++ ... ---> nc = "a" ++ k
1571
2630
        size_t cIndex = index;
1572
4440
        Node stra = nfc.collectConstantStringAt(cIndex);
1573
2630
        Assert(!stra.isNull());
1574
4440
        Node strb = nextConstStr;
1575
1576
        // Since `nc` is non-empty, we use the non-empty overlap
1577
2630
        size_t p = getSufficientNonEmptyOverlap(stra, strb, isRev);
1578
1579
        // If we can't split off more than a single character from the
1580
        // constant, we might as well do regular constant/non-constant
1581
        // inference (see below).
1582
2630
        if (p > 1)
1583
        {
1584
820
          NormalForm::getExplanationForPrefixEq(
1585
              nfc, nfnc, cIndex, ncIndex, iinfo.d_premises);
1586
820
          iinfo.d_premises.push_back(expNonEmpty);
1587
          // make the conclusion
1588
820
          SkolemCache* skc = d_termReg.getSkolemCache();
1589
          Node xcv =
1590
1640
              nm->mkNode(STRING_CONCAT, isRev ? strb : nc, isRev ? nc : strb);
1591
1640
          std::vector<Node> newSkolems;
1592
1640
          iinfo.d_conc = getConclusion(
1593
820
              xcv, stra, PfRule::CONCAT_CPROP, isRev, skc, newSkolems);
1594
820
          Assert(newSkolems.size() == 1);
1595
820
          iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
1596
820
          iinfo.setId(InferenceId::STRINGS_SSPLIT_CST_PROP);
1597
820
          iinfo.d_idRev = isRev;
1598
820
          pinfer.push_back(info);
1599
820
          break;
1600
        }
1601
      }
1602
1603
      // Since none of the other inferences apply, we just infer that `nc` has
1604
      // to start with the first character of the constant.
1605
      //
1606
      // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
1607
4550
      SkolemCache* skc = d_termReg.getSkolemCache();
1608
9100
      std::vector<Node> newSkolems;
1609
13650
      iinfo.d_conc = getConclusion(
1610
9100
          nc, nfcv[index], PfRule::CONCAT_CSPLIT, isRev, skc, newSkolems);
1611
13650
      NormalForm::getExplanationForPrefixEq(
1612
9100
          nfi, nfj, index, index, iinfo.d_premises);
1613
4550
      iinfo.d_premises.push_back(expNonEmpty);
1614
4550
      Assert(newSkolems.size() == 1);
1615
4550
      iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
1616
4550
      iinfo.setId(InferenceId::STRINGS_SSPLIT_CST);
1617
4550
      iinfo.d_idRev = isRev;
1618
4550
      pinfer.push_back(info);
1619
4550
      break;
1620
    }
1621
1622
    // Below, we deal with the case where `x` and `y` are two non-constant
1623
    // terms of different lengths. In this case, we have to split on which term
1624
    // is a prefix/suffix of the other.
1625
    //
1626
    // E.g. x ++ ... = y ++ ... ---> (x = y ++ k) v (y = x ++ k)
1627
2747
    Assert(d_state.areDisequal(xLenTerm, yLenTerm));
1628
2747
    Assert(!x.isConst());
1629
2747
    Assert(!y.isConst());
1630
1631
2747
    int32_t lentTestSuccess = -1;
1632
5494
    Node lenConstraint;
1633
5494
    if (options::stringCheckEntailLen())
1634
    {
1635
      // If length entailment checks are enabled, we can save the case split by
1636
      // inferring that `x` has to be longer than `y` or vice-versa.
1637
6912
      for (size_t e = 0; e < 2; e++)
1638
      {
1639
9373
        Node t = e == 0 ? x : y;
1640
        // do not infer constants are larger than variables
1641
5208
        if (!t.isConst())
1642
        {
1643
9373
          Node lt1 = e == 0 ? xLenTerm : yLenTerm;
1644
9373
          Node lt2 = e == 0 ? yLenTerm : xLenTerm;
1645
9373
          Node entLit = Rewriter::rewrite(nm->mkNode(GT, lt1, lt2));
1646
5208
          std::pair<bool, Node> et = d_state.entailmentCheck(
1647
9373
              options::TheoryOfMode::THEORY_OF_TYPE_BASED, entLit);
1648
5208
          if (et.first)
1649
          {
1650
2086
            Trace("strings-entail")
1651
1043
                << "Strings entailment : " << entLit
1652
1043
                << " is entailed in the current context." << std::endl;
1653
2086
            Trace("strings-entail")
1654
1043
                << "  explanation was : " << et.second << std::endl;
1655
1043
            lentTestSuccess = e;
1656
1043
            lenConstraint = entLit;
1657
            // Its not explained by the equality engine of this class, so its
1658
            // marked as not being explained. The length constraint is
1659
            // additionally being saved and added to the length constraint
1660
            // vector lcVec below, which is added to iinfo.d_ant below. Length
1661
            // constraints are being added as the last antecedant for the sake
1662
            // of proof reconstruction, which expect length constraints to come
1663
            // last.
1664
1043
            iinfo.d_noExplain.push_back(lenConstraint);
1665
1043
            break;
1666
          }
1667
        }
1668
      }
1669
    }
1670
    // lcVec stores the length constraint portion of the antecedant.
1671
5494
    std::vector<Node> lcVec;
1672
2747
    if (lenConstraint.isNull())
1673
    {
1674
      // will do split on length
1675
1704
      lenConstraint = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate();
1676
1704
      lcVec.push_back(lenConstraint);
1677
    }
1678
    else
1679
    {
1680
1043
      utils::flattenOp(AND, lenConstraint, lcVec);
1681
    }
1682
1683
2747
    NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_premises);
1684
    // Add premises for x != "" ^ y != ""
1685
8241
    for (unsigned xory = 0; xory < 2; xory++)
1686
    {
1687
10988
      Node t = xory == 0 ? x : y;
1688
10988
      Node tnz = d_state.explainNonEmpty(t);
1689
5494
      if (!tnz.isNull())
1690
      {
1691
5494
        lcVec.push_back(tnz);
1692
      }
1693
      else
1694
      {
1695
        tnz = x.eqNode(emp).negate();
1696
        lcVec.push_back(tnz);
1697
        iinfo.d_noExplain.push_back(tnz);
1698
      }
1699
    }
1700
2747
    SkolemCache* skc = d_termReg.getSkolemCache();
1701
5494
    std::vector<Node> newSkolems;
1702
    // make the conclusion
1703
2747
    if (lentTestSuccess == -1)
1704
    {
1705
1704
      iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR);
1706
1704
      iinfo.d_conc =
1707
3408
          getConclusion(x, y, PfRule::CONCAT_SPLIT, isRev, skc, newSkolems);
1708
    }
1709
1043
    else if (lentTestSuccess == 0)
1710
    {
1711
286
      iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR_PROP);
1712
286
      iinfo.d_conc =
1713
572
          getConclusion(x, y, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
1714
    }
1715
    else
1716
    {
1717
757
      Assert(lentTestSuccess == 1);
1718
757
      iinfo.setId(InferenceId::STRINGS_SSPLIT_VAR_PROP);
1719
757
      iinfo.d_conc =
1720
1514
          getConclusion(y, x, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
1721
    }
1722
    // add the length constraint(s) as the last antecedant
1723
5494
    Node lc = utils::mkAnd(lcVec);
1724
2747
    iinfo.d_premises.push_back(lc);
1725
2747
    iinfo.d_idRev = isRev;
1726
2747
    pinfer.push_back(info);
1727
2747
    break;
1728
21784
  }
1729
}
1730
1731
8537
bool CoreSolver::detectLoop(NormalForm& nfi,
1732
                               NormalForm& nfj,
1733
                               int index,
1734
                               int& loop_in_i,
1735
                               int& loop_in_j,
1736
                               unsigned rproc)
1737
{
1738
8537
  int has_loop[2] = { -1, -1 };
1739
25611
  for (unsigned r = 0; r < 2; r++)
1740
  {
1741
17074
    NormalForm& nf = r == 0 ? nfi : nfj;
1742
17074
    NormalForm& nfo = r == 0 ? nfj : nfi;
1743
17074
    std::vector<Node>& nfv = nf.d_nf;
1744
17074
    std::vector<Node>& nfov = nfo.d_nf;
1745
17074
    if (nfov[index].isConst())
1746
    {
1747
5424
      continue;
1748
    }
1749
41336
    for (unsigned lp = index + 1, lpEnd = nfv.size() - rproc; lp < lpEnd; lp++)
1750
    {
1751
30168
      if (nfv[lp] == nfov[index])
1752
      {
1753
482
        has_loop[r] = lp;
1754
482
        break;
1755
      }
1756
    }
1757
  }
1758
8537
  if( has_loop[0]!=-1 || has_loop[1]!=-1 ) {
1759
482
    loop_in_i = has_loop[0];
1760
482
    loop_in_j = has_loop[1];
1761
482
    return true;
1762
  } else {
1763
8055
    Trace("strings-solve-debug") << "No loops detected." << std::endl;
1764
8055
    return false;
1765
  }
1766
}
1767
1768
//xs(zy)=t(yz)xr
1769
420
CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
1770
                                                      NormalForm& nfj,
1771
                                                      int loop_index,
1772
                                                      int index,
1773
                                                      CoreInferInfo& info)
1774
{
1775
420
  if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT)
1776
  {
1777
    throw LogicException("Looping word equation encountered.");
1778
  }
1779
420
  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE)
1780
  {
1781
    d_im.setIncomplete();
1782
    return ProcessLoopResult::SKIPPED;
1783
  }
1784
1785
420
  NodeManager* nm = NodeManager::currentNM();
1786
840
  Node conc;
1787
420
  const std::vector<Node>& veci = nfi.d_nf;
1788
420
  const std::vector<Node>& vecoi = nfj.d_nf;
1789
1790
840
  TypeNode stype = veci[loop_index].getType();
1791
1792
840
  Trace("strings-loop") << "Detected possible loop for " << veci[loop_index]
1793
420
                        << std::endl;
1794
420
  Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl;
1795
420
  Trace("strings-loop") << " ... T(Y.Z)= ";
1796
840
  std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index);
1797
840
  Node t_yz = utils::mkNConcat(vec_t, stype);
1798
420
  Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
1799
420
  Trace("strings-loop") << " ... S(Z.Y)= ";
1800
840
  std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end());
1801
840
  Node s_zy = utils::mkNConcat(vec_s, stype);
1802
420
  Trace("strings-loop") << s_zy << std::endl;
1803
420
  Trace("strings-loop") << " ... R= ";
1804
840
  std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end());
1805
840
  Node r = utils::mkNConcat(vec_r, stype);
1806
420
  Trace("strings-loop") << r << std::endl;
1807
1808
840
  Node emp = Word::mkEmptyWord(stype);
1809
1810
420
  InferInfo& iinfo = info.d_infer;
1811
420
  if (s_zy.isConst() && r.isConst() && r != emp)
1812
  {
1813
    int c;
1814
18
    bool flag = true;
1815
18
    if (s_zy.getConst<String>().tailcmp(r.getConst<String>(), c))
1816
    {
1817
18
      if (c >= 0)
1818
      {
1819
18
        s_zy = Word::substr(s_zy, 0, c);
1820
18
        r = emp;
1821
18
        vec_r.clear();
1822
36
        Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
1823
18
                              << ", c=" << c << std::endl;
1824
18
        flag = false;
1825
      }
1826
    }
1827
18
    if (flag)
1828
    {
1829
      Trace("strings-loop") << "Strings::Loop: tails are different."
1830
                            << std::endl;
1831
      d_im.sendInference(
1832
          iinfo.d_premises, conc, InferenceId::STRINGS_FLOOP_CONFLICT, false, true);
1833
      return ProcessLoopResult::CONFLICT;
1834
    }
1835
  }
1836
1837
840
  Node split_eq;
1838
1260
  for (unsigned i = 0; i < 2; i++)
1839
  {
1840
1680
    Node t = i == 0 ? veci[loop_index] : t_yz;
1841
840
    split_eq = t.eqNode(emp);
1842
1680
    Node split_eqr = Rewriter::rewrite(split_eq);
1843
    // the equality could rewrite to false
1844
840
    if (!split_eqr.isConst())
1845
    {
1846
1572
      Node expNonEmpty = d_state.explainNonEmpty(t);
1847
786
      if (expNonEmpty.isNull())
1848
      {
1849
        // no antecedants necessary
1850
        iinfo.d_premises.clear();
1851
        // try to make t equal to empty to avoid loop
1852
        iinfo.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
1853
        iinfo.setId(InferenceId::STRINGS_LEN_SPLIT_EMP);
1854
        return ProcessLoopResult::INFERENCE;
1855
      }
1856
      else
1857
      {
1858
786
        iinfo.d_premises.push_back(expNonEmpty);
1859
      }
1860
    }
1861
    else
1862
    {
1863
54
      Assert(!split_eqr.getConst<bool>());
1864
    }
1865
  }
1866
1867
840
  Node str_in_re;
1868
860
  if (s_zy == t_yz && r == emp && s_zy.isConst()
1869
440
      && s_zy.getConst<String>().isRepeated())
1870
  {
1871
28
    Node rep_c = Word::substr(s_zy, 0, 1);
1872
28
    Trace("strings-loop") << "Special case (X)=" << vecoi[index] << " "
1873
14
                          << std::endl;
1874
14
    Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
1875
    // special case
1876
28
    str_in_re = nm->mkNode(
1877
        STRING_IN_REGEXP,
1878
14
        vecoi[index],
1879
28
        nm->mkNode(REGEXP_STAR, nm->mkNode(STRING_TO_REGEXP, rep_c)));
1880
14
    conc = str_in_re;
1881
  }
1882
406
  else if (t_yz.isConst())
1883
  {
1884
72
    Trace("strings-loop") << "Strings::Loop: Const Normal Breaking."
1885
36
                          << std::endl;
1886
36
    unsigned size = Word::getLength(t_yz);
1887
72
    std::vector<Node> vconc;
1888
132
    for (unsigned len = 1; len <= size; len++)
1889
    {
1890
112
      Node y = Word::substr(t_yz, 0, len);
1891
112
      Node z = Word::substr(t_yz, len, size - len);
1892
112
      Node restr = s_zy;
1893
112
      Node cc;
1894
96
      if (r != emp)
1895
      {
1896
72
        std::vector<Node> v2(vec_r);
1897
36
        v2.insert(v2.begin(), y);
1898
36
        v2.insert(v2.begin(), z);
1899
36
        restr = utils::mkNConcat(z, y);
1900
36
        cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype)));
1901
      }
1902
      else
1903
      {
1904
60
        cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(z, y)));
1905
      }
1906
96
      if (cc == d_false)
1907
      {
1908
80
        continue;
1909
      }
1910
      Node conc2 = nm->mkNode(
1911
          STRING_IN_REGEXP,
1912
16
          vecoi[index],
1913
64
          nm->mkNode(
1914
              REGEXP_CONCAT,
1915
32
              nm->mkNode(STRING_TO_REGEXP, y),
1916
80
              nm->mkNode(REGEXP_STAR, nm->mkNode(STRING_TO_REGEXP, restr))));
1917
16
      cc = cc == d_true ? conc2 : nm->mkNode(kind::AND, cc, conc2);
1918
16
      vconc.push_back(cc);
1919
    }
1920
52
    conc = vconc.size() == 0 ? Node::null() : vconc.size() == 1
1921
16
                                                  ? vconc[0]
1922
                                                  : nm->mkNode(kind::OR, vconc);
1923
  }
1924
  else
1925
  {
1926
740
    if (options::stringProcessLoopMode()
1927
370
        == options::ProcessLoopMode::SIMPLE_ABORT)
1928
    {
1929
      throw LogicException("Normal looping word equation encountered.");
1930
    }
1931
740
    else if (options::stringProcessLoopMode()
1932
370
             == options::ProcessLoopMode::SIMPLE)
1933
    {
1934
      d_im.setIncomplete();
1935
      return ProcessLoopResult::SKIPPED;
1936
    }
1937
1938
740
    Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking."
1939
370
                          << std::endl;
1940
    // right
1941
370
    SkolemCache* skc = d_termReg.getSkolemCache();
1942
740
    Node sk_w = skc->mkSkolem("w_loop");
1943
740
    Node sk_y = skc->mkSkolem("y_loop");
1944
370
    iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y);
1945
740
    Node sk_z = skc->mkSkolem("z_loop");
1946
    // t1 * ... * tn = y * z
1947
740
    Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
1948
    // s1 * ... * sk = z * y * r
1949
370
    vec_r.insert(vec_r.begin(), sk_y);
1950
370
    vec_r.insert(vec_r.begin(), sk_z);
1951
740
    Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, stype));
1952
740
    Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w));
1953
740
    Node restr = r == emp ? s_zy : utils::mkNConcat(sk_z, sk_y);
1954
370
    str_in_re =
1955
740
        nm->mkNode(kind::STRING_IN_REGEXP,
1956
                   sk_w,
1957
740
                   nm->mkNode(kind::REGEXP_STAR,
1958
740
                              nm->mkNode(kind::STRING_TO_REGEXP, restr)));
1959
1960
740
    std::vector<Node> vec_conc;
1961
370
    vec_conc.push_back(conc1);
1962
370
    vec_conc.push_back(conc2);
1963
370
    vec_conc.push_back(conc3);
1964
370
    vec_conc.push_back(str_in_re);
1965
370
    conc = nm->mkNode(kind::AND, vec_conc);
1966
  }  // normal case
1967
1968
  // we will be done
1969
420
  iinfo.d_conc = conc;
1970
420
  iinfo.setId(InferenceId::STRINGS_FLOOP);
1971
420
  info.d_nfPair[0] = nfi.d_base;
1972
420
  info.d_nfPair[1] = nfj.d_base;
1973
420
  return ProcessLoopResult::INFERENCE;
1974
}
1975
1976
4304
void CoreSolver::processDeq(Node ni, Node nj)
1977
{
1978
4304
  NodeManager* nm = NodeManager::currentNM();
1979
4304
  NormalForm& nfni = getNormalForm(ni);
1980
4304
  NormalForm& nfnj = getNormalForm(nj);
1981
1982
4304
  if (nfni.d_nf.size() <= 1 && nfnj.d_nf.size() <= 1)
1983
  {
1984
    // If normal forms have size <=1, then we are comparing either:
1985
    // (1) variable to variable,
1986
    // (2) variable to constant-like (empty, constant string/seq or SEQ_UNIT),
1987
    // (3) SEQ_UNIT to constant-like.
1988
    // We only have to process (3) here, since disequalities of the form of (1)
1989
    // and (2) are satisfied by construction.
1990
8529
    for (size_t i = 0; i < 2; i++)
1991
    {
1992
5694
      NormalForm& nfc = i == 0 ? nfni : nfnj;
1993
5694
      if (nfc.d_nf.size() == 0 || nfc.d_nf[0].getKind() != SEQ_UNIT)
1994
      {
1995
        // may need to look at the other side
1996
5680
        continue;
1997
      }
1998
14
      Node u = nfc.d_nf[0];
1999
      // if the other side is constant like
2000
14
      NormalForm& nfo = i == 0 ? nfnj : nfni;
2001
14
      if (nfo.d_nf.size() == 0 || !utils::isConstantLike(nfo.d_nf[0]))
2002
      {
2003
2
        break;
2004
      }
2005
      // v is the other side (a possibly constant seq.unit term)
2006
12
      Node v = nfo.d_nf[0];
2007
12
      Node vc;
2008
12
      if (v.isConst())
2009
      {
2010
        // get the list of characters (strings of length 1)
2011
24
        std::vector<Node> vchars = Word::getChars(v);
2012
12
        if (vchars.size() != 1)
2013
        {
2014
          // constant of size != 1, disequality is satisfied
2015
          break;
2016
        }
2017
        // get the element of the character
2018
12
        vc = vchars[0].getConst<Sequence>().getVec()[0];
2019
      }
2020
      else
2021
      {
2022
        Assert(v.getKind() == SEQ_UNIT);
2023
        vc = v[0];
2024
      }
2025
12
      Assert(u[0].getType() == vc.getType());
2026
      // if already disequal, we are done
2027
12
      if (d_state.areDisequal(u[0], vc))
2028
      {
2029
8
        break;
2030
      }
2031
      // seq.unit(x) != seq.unit(y) => x != y
2032
      // Notice this is a special case, since the code below would justify this
2033
      // disequality by reasoning that a component is disequal. However, the
2034
      // disequality components are the entire disequality.
2035
8
      Node deq = u.eqNode(v).notNode();
2036
8
      std::vector<Node> premises;
2037
4
      premises.push_back(deq);
2038
8
      Node conc = u[0].eqNode(vc).notNode();
2039
4
      d_im.sendInference(premises, conc, InferenceId::STRINGS_UNIT_INJ_DEQ, false, true);
2040
4
      return;
2041
    }
2042
2845
    Trace("strings-solve-debug") << "...trivial" << std::endl;
2043
2845
    return;
2044
  }
2045
2046
2910
  std::vector<Node> nfi = nfni.d_nf;
2047
2910
  std::vector<Node> nfj = nfnj.d_nf;
2048
2049
  // See if one side is constant, if so, the disequality ni != nj is satisfied
2050
  // if it cannot contain the other side.
2051
  //
2052
  // E.g. "abc" != x ++ "d" ++ y
2053
3967
  for (uint32_t i = 0; i < 2; i++)
2054
  {
2055
5312
    Node c = d_bsolver.getConstantEqc(i == 0 ? ni : nj);
2056
2800
    if (!c.isNull())
2057
    {
2058
      int findex, lindex;
2059
1026
      if (!StringsEntail::canConstantContainList(
2060
              c, i == 0 ? nfj : nfi, findex, lindex))
2061
      {
2062
576
        Trace("strings-solve-debug")
2063
288
            << "Disequality: constant cannot contain list" << std::endl;
2064
288
        return;
2065
      }
2066
    }
2067
  }
2068
2069
1167
  if (processReverseDeq(nfi, nfj, ni, nj))
2070
  {
2071
295
    Trace("strings-solve-debug") << "...processed reverse" << std::endl;
2072
295
    return;
2073
  }
2074
2075
872
  nfi = nfni.d_nf;
2076
872
  nfj = nfnj.d_nf;
2077
2078
872
  size_t index = 0;
2079
872
  while (index < nfi.size() || index < nfj.size())
2080
  {
2081
872
    if (processSimpleDeq(nfi, nfj, ni, nj, index, false))
2082
    {
2083
92
      Trace("strings-solve-debug") << "...processed simple" << std::endl;
2084
964
      return;
2085
    }
2086
2087
    // We have inferred that the normal forms up to position `index` are
2088
    // equivalent. Below, we refer to the components at the current position of
2089
    // the normal form as `x` and `y`.
2090
    //
2091
    // E.g. x ++ ... = y ++ ...
2092
780
    Assert(index < nfi.size() && index < nfj.size());
2093
780
    Node x = nfi[index];
2094
780
    Node y = nfj[index];
2095
1560
    Trace("strings-solve-debug")
2096
780
        << "...Processing(DEQ) " << x << " " << y << std::endl;
2097
780
    if (d_state.areEqual(x, y))
2098
    {
2099
      // The normal forms have an equivalent term at `index` in the current
2100
      // context. We move to the next `index`.
2101
      //
2102
      // E.g. x ++ x' ++ ... != z ++ y' ++ ... ^ x = z
2103
      index++;
2104
      continue;
2105
    }
2106
2107
780
    Assert(!x.isConst() || !y.isConst());
2108
780
    std::vector<Node> lenExp;
2109
780
    Node xLenTerm = d_state.getLength(x, lenExp);
2110
780
    Node yLenTerm = d_state.getLength(y, lenExp);
2111
780
    if (d_state.areDisequal(xLenTerm, yLenTerm))
2112
    {
2113
      // Below, we deal with the cases where the components at the current
2114
      // index are of different lengths in the current context.
2115
      //
2116
      // E.g. x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) != len(y)
2117
706
      if (x.isConst() || y.isConst())
2118
      {
2119
702
        Node ck = x.isConst() ? x : y;
2120
702
        Node nck = x.isConst() ? y : x;
2121
702
        Node nckLenTerm = x.isConst() ? yLenTerm : xLenTerm;
2122
702
        Node expNonEmpty = d_state.explainNonEmpty(nck);
2123
702
        if (expNonEmpty.isNull())
2124
        {
2125
          // Either `x` or `y` is a constant and the other may be equal to the
2126
          // empty string in the current context. We split on whether it
2127
          // actually is empty in that case.
2128
          //
2129
          // E.g. x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y) --->
2130
          //      x = "" v x != ""
2131
          Node emp = Word::mkEmptyWord(nck.getType());
2132
          d_im.sendSplit(nck, emp, InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT);
2133
          return;
2134
        }
2135
2136
702
        Node firstChar = Word::getLength(ck) == 1 ? ck : Word::prefix(ck, 1);
2137
702
        if (d_state.areEqual(nckLenTerm, d_one))
2138
        {
2139
680
          if (d_state.areDisequal(firstChar, nck))
2140
          {
2141
            // Either `x` or `y` is a constant and the other is a string of
2142
            // length one. If the non-constant is disequal to the first
2143
            // character of the constant in the current context, we satisfy the
2144
            // disequality and there is nothing else to do.
2145
            //
2146
            // E.g. "d" ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1
2147
638
            return;
2148
          }
2149
42
          else if (!d_state.areEqual(firstChar, nck))
2150
          {
2151
            // Either `x` or `y` is a constant and the other is a string of
2152
            // length one. If we do not know whether the non-constant is equal
2153
            // or disequal to the first character in the constant, we split on
2154
            // whether it is.
2155
            //
2156
            // E.g. x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1 --->
2157
            //      x = "a" v x != "a"
2158
42
            if (d_im.sendSplit(firstChar,
2159
                               nck,
2160
                               InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT,
2161
                               false))
2162
            {
2163
42
              return;
2164
            }
2165
          }
2166
        }
2167
        else
2168
        {
2169
          // Either `x` or `y` is a constant and it is not know whether the
2170
          // non-empty non-constant is of length one. We split the non-constant
2171
          // into a string of length one and the remainder.
2172
          //
2173
          // len(x)>=1 => x = k1 ++ k2 ^ len(k1) = 1
2174
22
          SkolemCache* skc = d_termReg.getSkolemCache();
2175
44
          std::vector<Node> newSkolems;
2176
          Node conc = getDecomposeConclusion(
2177
44
              nck, d_one, false, skc, newSkolems);
2178
22
          Assert(newSkolems.size() == 2);
2179
44
          std::vector<Node> antecLen;
2180
22
          antecLen.push_back(nm->mkNode(GEQ, nckLenTerm, d_one));
2181
22
          d_im.sendInference(antecLen,
2182
                             antecLen,
2183
                             conc,
2184
                             InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT,
2185
                             false,
2186
                             true);
2187
22
          return;
2188
        }
2189
      }
2190
      else
2191
      {
2192
        // `x` and `y` have different lengths in the current context and they
2193
        // are both non-constants. We split them into parts that have the same
2194
        // lengths.
2195
        //
2196
        // len(x) > len(y) => x = k1 ++ k2 ^ len(k1) = len(y)
2197
        // len(y) > len(x) => y = k3 ++ k4 ^ len(k3) = len(x)
2198
8
        Trace("strings-solve")
2199
4
            << "Non-Simple Case 1 : add lemmas " << std::endl;
2200
4
        SkolemCache* skc = d_termReg.getSkolemCache();
2201
2202
12
        for (unsigned r = 0; r < 2; r++)
2203
        {
2204
16
          Node ux = r == 0 ? x : y;
2205
16
          Node uy = r == 0 ? y : x;
2206
16
          Node uxLen = nm->mkNode(STRING_LENGTH, ux);
2207
16
          Node uyLen = nm->mkNode(STRING_LENGTH, uy);
2208
          // We always add the length constraint in the conclusion here
2209
          // because the skolem needs to have length `uyLen`. If we only assert
2210
          // that the skolem's length is greater or equal to one, we can end up
2211
          // in a loop:
2212
          //
2213
          // 1. Split: x = k1 ++ k2 ^ len(k1) >= 1
2214
          // 2. Assume: k2 = ""
2215
          // 3. Deduce: x = k1
2216
          //
2217
          // After step 3, `k1` is marked congruent because `x` is the older
2218
          // variable. So we get `x` in the normal form again.
2219
16
          std::vector<Node> newSkolems;
2220
          Node conc =
2221
16
              getDecomposeConclusion(ux, uyLen, false, skc, newSkolems);
2222
8
          Assert(newSkolems.size() == 2);
2223
8
          d_termReg.registerTermAtomic(newSkolems[1], LENGTH_GEQ_ONE);
2224
16
          std::vector<Node> antecLen;
2225
8
          antecLen.push_back(nm->mkNode(GT, uxLen, uyLen));
2226
8
          d_im.sendInference(antecLen,
2227
                             antecLen,
2228
                             conc,
2229
                             InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT,
2230
                             false,
2231
                             true);
2232
        }
2233
2234
4
        return;
2235
      }
2236
    }
2237
74
    else if (d_state.areEqual(xLenTerm, yLenTerm))
2238
    {
2239
      // `x` and `y` have the same length in the current context. We split on
2240
      // whether they are actually equal.
2241
      //
2242
      // E.g. x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y) --->
2243
      //      x = y v x != y
2244
40
      Assert(!d_state.areDisequal(x, y));
2245
40
      if (d_im.sendSplit(x, y, InferenceId::STRINGS_DEQ_STRINGS_EQ, false))
2246
      {
2247
40
        return;
2248
      }
2249
    }
2250
    else
2251
    {
2252
      // It is not known whether `x` and `y` have the same length in the
2253
      // current context. We split on whether they do.
2254
      //
2255
      // E.g. x ++ x' ++ ... != y ++ y' ++ ... --->
2256
      //      len(x) = len(y) v len(x) != len(y)
2257
34
      if (d_im.sendSplit(xLenTerm, yLenTerm, InferenceId::STRINGS_DEQ_LENS_EQ))
2258
      {
2259
34
        return;
2260
      }
2261
    }
2262
  }
2263
  Unreachable();
2264
}
2265
2266
1167
bool CoreSolver::processReverseDeq(std::vector<Node>& nfi,
2267
                                   std::vector<Node>& nfj,
2268
                                   Node ni,
2269
                                   Node nj)
2270
{
2271
  // reverse normal form of i, j
2272
1167
  std::reverse(nfi.begin(), nfi.end());
2273
1167
  std::reverse(nfj.begin(), nfj.end());
2274
2275
1167
  size_t index = 0;
2276
1167
  bool ret = processSimpleDeq(nfi, nfj, ni, nj, index, true);
2277
2278
  // reverse normal form of i, j
2279
1167
  std::reverse(nfi.begin(), nfi.end());
2280
1167
  std::reverse(nfj.begin(), nfj.end());
2281
2282
1167
  return ret;
2283
}
2284
2285
2039
bool CoreSolver::processSimpleDeq(std::vector<Node>& nfi,
2286
                                  std::vector<Node>& nfj,
2287
                                  Node ni,
2288
                                  Node nj,
2289
                                  size_t& index,
2290
                                  bool isRev)
2291
{
2292
4078
  TypeNode stype = ni.getType();
2293
4078
  Node emp = Word::mkEmptyWord(stype);
2294
2295
2039
  NormalForm& nfni = getNormalForm(ni);
2296
2039
  NormalForm& nfnj = getNormalForm(nj);
2297
3003
  while (index < nfi.size() || index < nfj.size())
2298
  {
2299
2521
    if (index >= nfi.size() || index >= nfj.size())
2300
    {
2301
      // We have reached the end of one of the normal forms. Note that this
2302
      // function only deals with two normal forms that have the same length,
2303
      // so the remainder of the longer normal form needs to be empty. This
2304
      // will lead to a conflict.
2305
      //
2306
      // E.g. px ++ x ++ ... != py ^
2307
      //        len(px ++ x ++ ...) = len(py) --->
2308
      //      x = "" ^ ...
2309
8
      Trace("strings-solve-debug")
2310
4
          << "Disequality normalize empty" << std::endl;
2311
      // the antecedant
2312
8
      std::vector<Node> ant;
2313
      // the antecedant that is not explainable in this context
2314
8
      std::vector<Node> antn;
2315
8
      Node niLenTerm = d_state.getLengthExp(ni, ant, nfni.d_base);
2316
8
      Node njLenTerm = d_state.getLengthExp(nj, ant, nfnj.d_base);
2317
      // length is not guaranteed to hold
2318
8
      Node leq = niLenTerm.eqNode(njLenTerm);
2319
4
      ant.push_back(leq);
2320
4
      antn.push_back(leq);
2321
4
      ant.insert(ant.end(), nfni.d_exp.begin(), nfni.d_exp.end());
2322
4
      ant.insert(ant.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
2323
8
      std::vector<Node> cc;
2324
4
      std::vector<Node>& nfk = index >= nfi.size() ? nfj : nfi;
2325
8
      for (size_t k = index; k < nfk.size(); k++)
2326
      {
2327
4
        cc.push_back(nfk[k].eqNode(emp));
2328
      }
2329
4
      Node conc = cc.size() == 1
2330
4
                      ? cc[0]
2331
12
                      : NodeManager::currentNM()->mkNode(kind::AND, cc);
2332
4
      d_im.sendInference(ant, antn, conc, InferenceId::STRINGS_DEQ_NORM_EMP, isRev, true);
2333
4
      return true;
2334
    }
2335
2336
    // We have inferred that the normal forms up to position `index` are
2337
    // equivalent. Below, we refer to the components at the current position of
2338
    // the normal form as `x` and `y`.
2339
    //
2340
    // E.g. x ++ ... = y ++ ...
2341
2637
    Node x = nfi[index];
2342
2637
    Node y = nfj[index];
2343
5034
    Trace("strings-solve-debug")
2344
2517
        << "...Processing(QED) " << x << " " << y << std::endl;
2345
2879
    if (d_state.areEqual(x, y))
2346
    {
2347
      // The normal forms have an equivalent term at `index` in the current
2348
      // context. We move to the next `index`.
2349
      //
2350
      // E.g. x ++ x' ++ ... != z ++ y' ++ ... ^ x = z
2351
362
      index++;
2352
362
      continue;
2353
    }
2354
2355
2155
    if (!x.isConst() || !y.isConst())
2356
    {
2357
3792
      std::vector<Node> lenExp;
2358
3792
      Node xLenTerm = d_state.getLength(x, lenExp);
2359
3792
      Node yLenTerm = d_state.getLength(y, lenExp);
2360
1896
      if (d_state.areEqual(xLenTerm, yLenTerm) && d_state.areDisequal(x, y))
2361
      {
2362
        // Either `x` or `y` is non-constant, the lengths are equal, and `x`
2363
        // and `y` are disequal in the current context. The disequality is
2364
        // satisfied and there is nothing else to do.
2365
        //
2366
        // E.g. x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y) ^ x != y
2367
488
        Trace("strings-solve")
2368
244
            << "Simple Case 2 : found equal length disequal sub strings " << x
2369
244
            << " " << y << std::endl;
2370
244
        return true;
2371
      }
2372
      else
2373
      {
2374
        // Either `x` or `y` is non-constant but it is not known whether they
2375
        // have the same length or are disequal. We bail out.
2376
        //
2377
        // E.g. x ++ x' ++ ... != y ++ y' ++ ...
2378
1652
        return false;
2379
      }
2380
    }
2381
2382
    // Below, we deal with the cases where both `x` and `y` are constant.
2383
259
    Assert(x.isConst() && y.isConst());
2384
259
    size_t xLen = Word::getLength(x);
2385
259
    size_t yLen = Word::getLength(y);
2386
259
    size_t shortLen = std::min(xLen, yLen);
2387
    bool isSameFix =
2388
259
        isRev ? Word::rstrncmp(x, y, shortLen) : Word::strncmp(x, y, shortLen);
2389
259
    if (!isSameFix)
2390
    {
2391
      // `x` and `y` are constants but do not share a prefix/suffix, thus
2392
      // satisfying the disequality. There is nothing else to do.
2393
      //
2394
      // E.g. "abc" ++ x' ++ ... != "d" ++ y' ++ ...
2395
139
      return true;
2396
    }
2397
2398
    // `x` and `y` are constants and share a prefix/suffix. We move the common
2399
    // prefix/suffix to a separate component in the normal form.
2400
    //
2401
    // E.g. "abc" ++ x' ++ ... != "ab" ++ y' ++ ... --->
2402
    //      "ab" ++ "c" ++ x' ++ ... != "ab" ++ y' ++ ...
2403
240
    Node nk = xLen < yLen ? x : y;
2404
240
    Node nl = xLen < yLen ? y : x;
2405
240
    Node remainderStr;
2406
120
    if (isRev)
2407
    {
2408
44
      remainderStr = Word::substr(nl, 0, Word::getLength(nl) - shortLen);
2409
88
      Trace("strings-solve-debug-test")
2410
44
          << "Rev. Break normal form of " << nl << " into " << nk << ", "
2411
44
          << remainderStr << std::endl;
2412
    }
2413
    else
2414
    {
2415
76
      remainderStr = Word::substr(nl, shortLen);
2416
152
      Trace("strings-solve-debug-test")
2417
76
          << "Break normal form of " << nl << " into " << nk << ", "
2418
76
          << remainderStr << std::endl;
2419
    }
2420
120
    if (xLen < yLen)
2421
    {
2422
      nfj.insert(nfj.begin() + index + 1, remainderStr);
2423
      nfj[index] = nfi[index];
2424
    }
2425
    else
2426
    {
2427
120
      nfi.insert(nfi.begin() + index + 1, remainderStr);
2428
120
      nfi[index] = nfj[index];
2429
    }
2430
2431
120
    index++;
2432
  }
2433
  return false;
2434
}
2435
2436
void CoreSolver::addNormalFormPair( Node n1, Node n2 ){
2437
  if (n1>n2)
2438
  {
2439
    addNormalFormPair(n2,n1);
2440
    return;
2441
  }
2442
  if( !isNormalFormPair( n1, n2 ) ){
2443
    int index = 0;
2444
    NodeIntMap::const_iterator it = d_nfPairs.find(n1);
2445
    if (it != d_nfPairs.end())
2446
    {
2447
      index = (*it).second;
2448
    }
2449
    d_nfPairs[n1] = index + 1;
2450
    if( index<(int)d_nf_pairs_data[n1].size() ){
2451
      d_nf_pairs_data[n1][index] = n2;
2452
    }else{
2453
      d_nf_pairs_data[n1].push_back( n2 );
2454
    }
2455
    Assert(isNormalFormPair(n1, n2));
2456
  } else {
2457
    Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl;
2458
  }
2459
}
2460
2461
13286
bool CoreSolver::isNormalFormPair( Node n1, Node n2 ) {
2462
13286
  if (n1>n2)
2463
  {
2464
3733
    return isNormalFormPair(n2,n1);
2465
  }
2466
  //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl;
2467
9553
  NodeIntMap::const_iterator it = d_nfPairs.find(n1);
2468
9553
  if (it != d_nfPairs.end())
2469
  {
2470
    Assert(d_nf_pairs_data.find(n1) != d_nf_pairs_data.end());
2471
    for( int i=0; i<(*it).second; i++ ){
2472
      Assert(i < (int)d_nf_pairs_data[n1].size());
2473
      if( d_nf_pairs_data[n1][i]==n2 ){
2474
        return true;
2475
      }
2476
    }
2477
  }
2478
9553
  return false;
2479
}
2480
2481
9299
void CoreSolver::checkNormalFormsDeq()
2482
{
2483
9299
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
2484
18256
  std::map< Node, std::map< Node, bool > > processed;
2485
2486
9299
  const context::CDList<Node>& deqs = d_state.getDisequalityList();
2487
2488
  //for each pair of disequal strings, must determine whether their lengths are equal or disequal
2489
37006
  for (const Node& eq : deqs)
2490
  {
2491
55414
    Node n[2];
2492
83121
    for( unsigned i=0; i<2; i++ ){
2493
55414
      n[i] = ee->getRepresentative( eq[i] );
2494
    }
2495
27707
    if( processed[n[0]].find( n[1] )==processed[n[0]].end() ){
2496
23638
      processed[n[0]][n[1]] = true;
2497
47276
      Node lt[2];
2498
70914
      for( unsigned i=0; i<2; i++ ){
2499
47276
        EqcInfo* ei = d_state.getOrMakeEqcInfo(n[i], false);
2500
47276
        lt[i] = ei ? ei->d_lengthTerm : Node::null();
2501
47276
        if( lt[i].isNull() ){
2502
          lt[i] = eq[i];
2503
        }
2504
47276
        lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] );
2505
      }
2506
23638
      if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1]))
2507
      {
2508
313
        d_im.sendSplit(lt[0], lt[1], InferenceId::STRINGS_DEQ_LENGTH_SP);
2509
      }
2510
    }
2511
  }
2512
2513
9299
  if (d_im.hasProcessed())
2514
  {
2515
    // added splitting lemma above
2516
192
    return;
2517
  }
2518
  // otherwise, look at pairs of equivalence classes with equal lengths
2519
18064
  std::map<TypeNode, std::vector<std::vector<Node> > > colsT;
2520
18064
  std::map<TypeNode, std::vector<Node> > ltsT;
2521
9107
  d_state.separateByLength(d_strings_eqc, colsT, ltsT);
2522
12177
  for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& ct : colsT)
2523
  {
2524
3220
    std::vector<std::vector<Node> >& cols = ct.second;
2525
23462
    for( unsigned i=0; i<cols.size(); i++ ){
2526
20392
      if (cols[i].size() > 1 && !d_im.hasPendingLemma())
2527
      {
2528
4891
        if (Trace.isOn("strings-solve"))
2529
        {
2530
          Trace("strings-solve") << "- Verify disequalities are processed for "
2531
                                 << cols[i][0] << ", normal form : ";
2532
          utils::printConcatTrace(getNormalForm(cols[i][0]).d_nf, "strings-solve");
2533
          Trace("strings-solve")
2534
              << "... #eql = " << cols[i].size() << std::endl;
2535
        }
2536
        //must ensure that normal forms are disequal
2537
22582
        for( unsigned j=0; j<cols[i].size(); j++ ){
2538
62778
          for( unsigned k=(j+1); k<cols[i].size(); k++ ){
2539
            //for strings that are disequal, but have the same length
2540
45087
            if (cols[i][j].isConst() && cols[i][k].isConst())
2541
            {
2542
              // if both are constants, they should be distinct, and its trivial
2543
31552
              Assert(cols[i][j] != cols[i][k]);
2544
            }
2545
13535
            else if (d_state.areDisequal(cols[i][j], cols[i][k]))
2546
            {
2547
4304
              Assert(!d_state.isInConflict());
2548
4304
              if (Trace.isOn("strings-solve"))
2549
              {
2550
                Trace("strings-solve") << "- Compare " << cols[i][j] << ", nf ";
2551
                utils::printConcatTrace(getNormalForm(cols[i][j]).d_nf,
2552
                                        "strings-solve");
2553
                Trace("strings-solve") << " against " << cols[i][k] << ", nf ";
2554
                utils::printConcatTrace(getNormalForm(cols[i][k]).d_nf,
2555
                                        "strings-solve");
2556
                Trace("strings-solve") << "..." << std::endl;
2557
              }
2558
4304
              processDeq(cols[i][j], cols[i][k]);
2559
4304
              if (d_im.hasProcessed())
2560
              {
2561
300
                return;
2562
              }
2563
            }
2564
          }
2565
        }
2566
      }
2567
    }
2568
  }
2569
}
2570
2571
8653
void CoreSolver::checkLengthsEqc() {
2572
37973
  for (unsigned i = 0; i < d_strings_eqc.size(); i++)
2573
  {
2574
58640
    TypeNode stype = d_strings_eqc[i].getType();
2575
29320
    NormalForm& nfi = getNormalForm(d_strings_eqc[i]);
2576
58640
    Trace("strings-process-debug")
2577
29320
        << "Process length constraints for " << d_strings_eqc[i] << std::endl;
2578
    // check if there is a length term for this equivalence class
2579
29320
    EqcInfo* ei = d_state.getOrMakeEqcInfo(d_strings_eqc[i], false);
2580
58640
    Node lt = ei ? ei->d_lengthTerm : Node::null();
2581
29320
    if (lt.isNull())
2582
    {
2583
      Trace("strings-process-debug")
2584
          << "No length term for eqc " << d_strings_eqc[i] << std::endl;
2585
      continue;
2586
    }
2587
58640
    Node llt = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, lt);
2588
    // now, check if length normalization has occurred
2589
29320
    if (ei->d_normalizedLength.get().isNull())
2590
    {
2591
53096
      Node nf = utils::mkNConcat(nfi.d_nf, stype);
2592
26548
      if (Trace.isOn("strings-process-debug"))
2593
      {
2594
        Trace("strings-process-debug")
2595
            << "  normal form is " << nf << " from base " << nfi.d_base
2596
            << std::endl;
2597
        Trace("strings-process-debug") << "  normal form exp is: " << std::endl;
2598
        for (const Node& exp : nfi.d_exp)
2599
        {
2600
          Trace("strings-process-debug") << "   " << exp << std::endl;
2601
        }
2602
      }
2603
2604
      // if not, add the lemma
2605
53096
      std::vector<Node> ant;
2606
26548
      ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end());
2607
26548
      ant.push_back(lt.eqNode(nfi.d_base));
2608
53096
      Node lc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nf);
2609
53096
      Node lcr = Rewriter::rewrite(lc);
2610
53096
      Trace("strings-process-debug")
2611
26548
          << "Rewrote length " << lc << " to " << lcr << std::endl;
2612
26548
      if (!d_state.areEqual(llt, lcr))
2613
      {
2614
10564
        Node eq = llt.eqNode(lc);
2615
5282
        ei->d_normalizedLength.set(eq);
2616
5282
        d_im.sendInference(ant, eq, InferenceId::STRINGS_LEN_NORM, false, true);
2617
      }
2618
    }
2619
  }
2620
8653
}
2621
2622
2125
bool CoreSolver::processInferInfo(CoreInferInfo& cii)
2623
{
2624
2125
  InferInfo& ii = cii.d_infer;
2625
  // rewrite the conclusion, ensure non-trivial
2626
4250
  Node concr = Rewriter::rewrite(ii.d_conc);
2627
2628
2125
  if (concr == d_true)
2629
  {
2630
    // conclusion rewrote to true
2631
    return false;
2632
  }
2633
  // process the state change to this solver
2634
2125
  if (!cii.d_nfPair[0].isNull())
2635
  {
2636
    Assert(!cii.d_nfPair[1].isNull());
2637
    addNormalFormPair(cii.d_nfPair[0], cii.d_nfPair[1]);
2638
  }
2639
  // send phase requirements
2640
2801
  for (const std::pair<const Node, bool>& pp : cii.d_pendingPhase)
2641
  {
2642
1352
    Node ppr = Rewriter::rewrite(pp.first);
2643
676
    d_im.addPendingPhaseRequirement(ppr, pp.second);
2644
  }
2645
2646
  // send the inference, which is a lemma
2647
2125
  d_im.sendInference(ii, true);
2648
2649
2125
  return true;
2650
}
2651
2652
}/* CVC4::theory::strings namespace */
2653
}/* CVC4::theory namespace */
2654
26676
}/* CVC4 namespace */