GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/theory_strings_preprocess.cpp Lines: 490 490 100.0 %
Date: 2021-03-23 Branches: 1447 2826 51.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_strings_preprocess.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 Strings Preprocess
13
 **
14
 ** Strings Preprocess.
15
 **/
16
17
#include "theory/strings/theory_strings_preprocess.h"
18
19
#include "expr/kind.h"
20
#include "options/smt_options.h"
21
#include "options/strings_options.h"
22
#include "proof/proof_manager.h"
23
#include "smt/logic_exception.h"
24
#include "theory/quantifiers/quantifiers_attributes.h"
25
#include "theory/strings/arith_entail.h"
26
#include "theory/strings/sequences_rewriter.h"
27
#include "theory/strings/word.h"
28
29
using namespace CVC4;
30
using namespace CVC4::kind;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace strings {
35
36
/** Mapping to a dummy node for marking an attribute on internal quantified
37
 * formulas */
38
struct QInternalVarAttributeId
39
{
40
};
41
typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
42
43
9031
StringsPreprocess::StringsPreprocess(SkolemCache* sc,
44
9031
                                     IntegralHistogramStat<Kind>* statReductions)
45
9031
    : d_sc(sc), d_statReductions(statReductions)
46
{
47
9031
}
48
49
9028
StringsPreprocess::~StringsPreprocess(){
50
51
9028
}
52
53
2826
Node StringsPreprocess::reduce(Node t,
54
                               std::vector<Node>& asserts,
55
                               SkolemCache* sc)
56
{
57
5652
  Trace("strings-preprocess-debug")
58
2826
      << "StringsPreprocess::reduce: " << t << std::endl;
59
2826
  Node retNode = t;
60
2826
  NodeManager* nm = NodeManager::currentNM();
61
5652
  Node zero = nm->mkConst(Rational(0));
62
5652
  Node one = nm->mkConst(Rational(1));
63
5652
  Node negOne = nm->mkConst(Rational(-1));
64
65
2826
  if( t.getKind() == kind::STRING_SUBSTR ) {
66
    // processing term:  substr( s, n, m )
67
2062
    Node s = t[0];
68
2062
    Node n = t[1];
69
2062
    Node m = t[2];
70
2062
    Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
71
2062
    Node t12 = nm->mkNode(PLUS, n, m);
72
2062
    Node lt0 = nm->mkNode(STRING_LENGTH, s);
73
    //start point is greater than or equal zero
74
2062
    Node c1 = nm->mkNode(GEQ, n, zero);
75
    //start point is less than end of string
76
2062
    Node c2 = nm->mkNode(GT, lt0, n);
77
    //length is positive
78
2062
    Node c3 = nm->mkNode(GT, m, zero);
79
2062
    Node cond = nm->mkNode(AND, c1, c2, c3);
80
81
2062
    Node emp = Word::mkEmptyWord(t.getType());
82
83
2062
    Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
84
2062
    Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
85
2062
    Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2));
86
    //length of first skolem is second argument
87
2062
    Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
88
2062
    Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
89
    // Length of the suffix is either 0 (in the case where m + n > len(s)) or
90
    // len(s) - n -m
91
    Node b13 = nm->mkNode(
92
        OR,
93
2062
        nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))),
94
4124
        nm->mkNode(EQUAL, lsk2, zero));
95
    // Length of the result is at most m
96
2062
    Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
97
98
2062
    Node b1 = nm->mkNode(AND, b11, b12, b13, b14);
99
2062
    Node b2 = skt.eqNode(emp);
100
2062
    Node lemma = nm->mkNode(ITE, cond, b1, b2);
101
102
    // assert:
103
    // IF    n >=0 AND len( s ) > n AND m > 0
104
    // THEN: s = sk1 ++ skt ++ sk2 AND
105
    //       len( sk1 ) = n AND
106
    //       ( len( sk2 ) = len( s )-(n+m) OR len( sk2 ) = 0 ) AND
107
    //       len( skt ) <= m
108
    // ELSE: skt = ""
109
    //
110
    // Note: The length of sk2 is either 0 (if the n + m is greater or equal to
111
    // the length of s) or len(s) - (n + m) otherwise. If n + m is greater or
112
    // equal to the length of s, then len(s) - (n + m) is negative and in
113
    // conflict with lengths always being positive, so only len(sk2) = 0 may be
114
    // satisfied. If n + m is less than the length of s, then len(sk2) = 0
115
    // cannot be satisfied because we have the constraint that len(skt) <= m,
116
    // so sk2 must be greater than 0.
117
1031
    asserts.push_back(lemma);
118
119
    // Thus, substr( s, n, m ) = skt
120
1031
    retNode = skt;
121
  }
122
1795
  else if (t.getKind() == kind::STRING_UPDATE)
123
  {
124
    // processing term:  update( s, n, r )
125
30
    Node s = t[0];
126
30
    Node n = t[1];
127
30
    Node r = t[2];
128
30
    Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
129
30
    Node ls = nm->mkNode(STRING_LENGTH, s);
130
    // start point is greater than or equal zero
131
30
    Node c1 = nm->mkNode(GEQ, n, zero);
132
    // start point is less than end of string
133
30
    Node c2 = nm->mkNode(GT, ls, n);
134
30
    Node cond = nm->mkNode(AND, c1, c2);
135
136
    // substr(r,0,|s|-n)
137
30
    Node lens = nm->mkNode(STRING_LENGTH, s);
138
30
    Node rs;
139
15
    if (r.isConst() && Word::getLength(r) == 1)
140
    {
141
      // optimization: don't need to take substring for single characters, due
142
      // to guard on where it is used in the reduction below.
143
2
      rs = r;
144
    }
145
    else
146
    {
147
13
      rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(MINUS, lens, n));
148
    }
149
30
    Node rslen = nm->mkNode(STRING_LENGTH, rs);
150
30
    Node nsuf = nm->mkNode(PLUS, n, rslen);
151
    // substr(s, n, len(substr(r,0,|s|-n))), which is used for formalizing the
152
    // purification variable sk3 below.
153
30
    Node ssubstr = nm->mkNode(STRING_SUBSTR, s, n, rslen);
154
155
30
    Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
156
    Node sk2 =
157
30
        sc->mkSkolemCached(s, nsuf, SkolemCache::SK_SUFFIX_REM, "sssufr");
158
30
    Node sk3 = sc->mkSkolemCached(ssubstr, SkolemCache::SK_PURIFY, "ssubstr");
159
30
    Node a1 = skt.eqNode(nm->mkNode(STRING_CONCAT, sk1, rs, sk2));
160
30
    Node a2 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, sk3, sk2));
161
    // length of first skolem is second argument
162
30
    Node a3 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
163
164
30
    Node b1 = nm->mkNode(AND, a1, a2, a3);
165
30
    Node b2 = skt.eqNode(s);
166
30
    Node lemma = nm->mkNode(ITE, cond, b1, b2);
167
168
    // assert:
169
    // IF    n >=0 AND n < len( s )
170
    // THEN: skt = sk1 ++ substr(r,0,len(s)-n) ++ sk2 AND
171
    //       s = sk1 ++ sk3 ++ sk2 AND
172
    //       len( sk1 ) = n
173
    // ELSE: skt = s
174
    // We use an optimization where r is used instead of substr(r,0,len(s)-n)
175
    // if r is a constant of length one.
176
15
    asserts.push_back(lemma);
177
178
    // Thus, str.update( s, n, r ) = skt
179
15
    retNode = skt;
180
  }
181
1780
  else if (t.getKind() == kind::STRING_STRIDOF)
182
  {
183
    // processing term:  indexof( x, y, n )
184
222
    Node x = t[0];
185
222
    Node y = t[1];
186
222
    Node n = t[2];
187
    Node skk = sc->mkTypedSkolemCached(
188
222
        nm->integerType(), t, SkolemCache::SK_PURIFY, "iok");
189
190
222
    Node negone = nm->mkConst(Rational(-1));
191
222
    Node krange = nm->mkNode(GEQ, skk, negone);
192
    // assert:   indexof( x, y, n ) >= -1
193
111
    asserts.push_back(krange);
194
111
    krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk);
195
    // assert:   len( x ) >= indexof( x, y, z )
196
111
    asserts.push_back(krange);
197
198
    // substr( x, n, len( x ) - n )
199
    Node st = nm->mkNode(STRING_SUBSTR,
200
                         x,
201
                         n,
202
222
                         nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
203
    Node io2 =
204
222
        sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
205
    Node io4 =
206
222
        sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
207
208
    // ~contains( substr( x, n, len( x ) - n ), y )
209
222
    Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
210
    // n > len( x )
211
222
    Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x));
212
    // 0 > n
213
222
    Node c13 = nm->mkNode(GT, zero, n);
214
222
    Node cond1 = nm->mkNode(OR, c11, c12, c13);
215
    // skk = -1
216
222
    Node cc1 = skk.eqNode(negone);
217
218
    // y = ""
219
222
    Node emp = Word::mkEmptyWord(x.getType());
220
222
    Node cond2 = y.eqNode(emp);
221
    // skk = n
222
222
    Node cc2 = skk.eqNode(t[2]);
223
224
    // substr( x, n, len( x ) - n ) = str.++( io2, y, io4 )
225
222
    Node c31 = st.eqNode(nm->mkNode(STRING_CONCAT, io2, y, io4));
226
    // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
227
    Node c32 =
228
444
        nm->mkNode(
229
              STRING_STRCTN,
230
222
              nm->mkNode(
231
                  STRING_CONCAT,
232
                  io2,
233
222
                  nm->mkNode(
234
                      STRING_SUBSTR,
235
                      y,
236
                      zero,
237
222
                      nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))),
238
              y)
239
222
            .negate();
240
    // skk = n + len( io2 )
241
222
    Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2)));
242
222
    Node cc3 = nm->mkNode(AND, c31, c32, c33);
243
244
    // assert:
245
    // IF:   ~contains( substr( x, n, len( x ) - n ), y ) OR n > len(x) OR 0 > n
246
    // THEN: skk = -1
247
    // ELIF: y = ""
248
    // THEN: skk = n
249
    // ELSE: substr( x, n, len( x ) - n ) = str.++( io2, y, io4 ) ^
250
    //       ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) ^
251
    //       skk = n + len( io2 )
252
    // for fresh io2, io4.
253
222
    Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3));
254
111
    asserts.push_back(rr);
255
256
    // Thus, indexof( x, y, n ) = skk.
257
111
    retNode = skk;
258
  }
259
1669
  else if (t.getKind() == STRING_ITOS)
260
  {
261
    // processing term:  int.to.str( n )
262
44
    Node n = t[0];
263
44
    Node itost = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
264
44
    Node leni = nm->mkNode(STRING_LENGTH, itost);
265
266
44
    std::vector<Node> conc;
267
44
    std::vector< TypeNode > argTypes;
268
22
    argTypes.push_back(nm->integerType());
269
44
    Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
270
271
44
    Node lem = nm->mkNode(GEQ, leni, one);
272
22
    conc.push_back(lem);
273
274
22
    lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni));
275
22
    conc.push_back(lem);
276
277
22
    lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero));
278
22
    conc.push_back(lem);
279
280
44
    Node x = SkolemCache::mkIndexVar(t);
281
44
    Node xPlusOne = nm->mkNode(PLUS, x, one);
282
44
    Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
283
44
    Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni));
284
44
    Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one);
285
44
    Node ux = nm->mkNode(APPLY_UF, u, x);
286
44
    Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
287
44
    Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
288
44
    Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
289
290
44
    Node ten = nm->mkConst(Rational(10));
291
44
    Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
292
    Node leadingZeroPos =
293
44
        nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one));
294
    Node cb = nm->mkNode(
295
        AND,
296
44
        nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, one, zero)),
297
88
        nm->mkNode(LT, c, ten));
298
299
44
    Node ux1lem = nm->mkNode(GEQ, n, ux1);
300
301
22
    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
302
22
    lem = mkForallInternal(xbv, lem);
303
22
    conc.push_back(lem);
304
305
44
    Node nonneg = nm->mkNode(GEQ, n, zero);
306
307
44
    Node emp = Word::mkEmptyWord(t.getType());
308
22
    lem = nm->mkNode(ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(emp));
309
22
    asserts.push_back(lem);
310
    // assert:
311
    // IF n>=0
312
    // THEN:
313
    //   len( itost ) >= 1 ^
314
    //   n = U( len( itost ) ) ^ U( 0 ) = 0 ^
315
    //   forall x. (x>=0 ^ x < str.len(itost)) =>
316
    //     U( x+1 ) = (str.code( str.at(itost, x) )-48) + 10*U( x ) ^
317
    //     ite( x=0 AND str.len(itost)>1, 49, 48 ) <=
318
    //       str.code( str.at(itost, x) ) < 58 ^
319
    //     n >= U(x + 1)
320
    // ELSE
321
    //   itost = ""
322
    // thus:
323
    //   int.to.str( n ) = itost
324
    //
325
    // Note: The conjunct `n >= U(x + 1)` is not needed for correctness but is
326
    // just an optimization.
327
328
    // The function U is an accumulator, where U( x ) for x>0 is the value of
329
    // str.to.int( str.substr( int.to.str( n ), 0, x ) ). For example, for
330
    // n=345, we have that U(1), U(2), U(3) = 3, 34, 345.
331
    // Above, we use str.code to map characters to their integer value, where
332
    // note that str.code( "0" ) = 48. Further notice that
333
    //   ite( x=0 AND str.len(itost)>1, 49, 48 )
334
    // enforces that int.to.str( n ) has no leading zeroes.
335
22
    retNode = itost;
336
1647
  } else if( t.getKind() == kind::STRING_STOI ) {
337
50
    Node s = t[0];
338
    Node stoit = sc->mkTypedSkolemCached(
339
50
        nm->integerType(), t, SkolemCache::SK_PURIFY, "stoit");
340
50
    Node lens = nm->mkNode(STRING_LENGTH, s);
341
342
50
    std::vector<Node> conc1;
343
50
    Node lem = stoit.eqNode(negOne);
344
25
    conc1.push_back(lem);
345
346
50
    Node emp = Word::mkEmptyWord(s.getType());
347
50
    Node sEmpty = s.eqNode(emp);
348
50
    Node k = nm->mkSkolem("k", nm->integerType());
349
50
    Node kc1 = nm->mkNode(GEQ, k, zero);
350
50
    Node kc2 = nm->mkNode(LT, k, lens);
351
50
    Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
352
    Node codeSk = nm->mkNode(
353
        MINUS,
354
50
        nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
355
100
        c0);
356
50
    Node ten = nm->mkConst(Rational(10));
357
    Node kc3 = nm->mkNode(
358
50
        OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten));
359
25
    conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3)));
360
361
50
    std::vector<Node> conc2;
362
50
    std::vector< TypeNode > argTypes;
363
25
    argTypes.push_back(nm->integerType());
364
50
    Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
365
366
25
    lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens));
367
25
    conc2.push_back(lem);
368
369
25
    lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero));
370
25
    conc2.push_back(lem);
371
372
25
    lem = nm->mkNode(GT, lens, zero);
373
25
    conc2.push_back(lem);
374
375
50
    Node x = SkolemCache::mkIndexVar(t);
376
50
    Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
377
50
    Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens));
378
50
    Node sx = nm->mkNode(STRING_SUBSTR, s, x, one);
379
50
    Node ux = nm->mkNode(APPLY_UF, u, x);
380
50
    Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one));
381
50
    Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
382
383
50
    Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
384
50
    Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten));
385
386
50
    Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
387
388
25
    lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
389
25
    lem = mkForallInternal(xbv, lem);
390
25
    conc2.push_back(lem);
391
392
50
    Node sneg = nm->mkNode(LT, stoit, zero);
393
25
    lem = nm->mkNode(ITE, sneg, nm->mkNode(AND, conc1), nm->mkNode(AND, conc2));
394
25
    asserts.push_back(lem);
395
396
    // assert:
397
    // IF stoit < 0
398
    // THEN:
399
    //   stoit = -1 ^
400
    //   ( s = "" OR
401
    //     ( k>=0 ^ k<len( s ) ^ ( str.code( str.at(s, k) ) < 48 OR
402
    //                             str.code( str.at(s, k) ) >= 58 )))
403
    // ELSE:
404
    //   stoit = U( len( s ) ) ^ U( 0 ) = 0 ^
405
    //   str.len( s ) > 0 ^
406
    //   forall x. (x>=0 ^ x < str.len(s)) =>
407
    //     U( x+1 ) = ( str.code( str.at(s, x) ) - 48 ) + 10*U( x ) ^
408
    //     48 <= str.code( str.at(s, x) ) < 58 ^
409
    //     stoit >= U( x+1 )
410
    // Thus, str.to.int( s ) = stoit
411
    //
412
    // Note: The conjunct `stoit >= U( x+1 )` is not needed for correctness but
413
    // is just an optimization.
414
415
25
    retNode = stoit;
416
  }
417
1622
  else if (t.getKind() == kind::SEQ_NTH)
418
  {
419
    // processing term:  str.nth( s, n)
420
    // similar to substr.
421
58
    Node s = t[0];
422
58
    Node n = t[1];
423
58
    Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
424
58
    Node t12 = nm->mkNode(PLUS, n, one);
425
58
    Node lt0 = nm->mkNode(STRING_LENGTH, s);
426
    // start point is greater than or equal zero
427
58
    Node c1 = nm->mkNode(GEQ, n, zero);
428
    // start point is less than end of string
429
58
    Node c2 = nm->mkNode(GT, lt0, n);
430
    // check whether this application of seq.nth is defined.
431
58
    Node cond = nm->mkNode(AND, c1, c2);
432
433
    // nodes for the case where `seq.nth` is defined.
434
58
    Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
435
58
    Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
436
58
    Node unit = nm->mkNode(SEQ_UNIT, skt);
437
58
    Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, unit, sk2));
438
    // length of first skolem is second argument
439
58
    Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
440
58
    Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
441
58
    Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, t12));
442
58
    Node b1 = nm->mkNode(AND, b11, b12, b13);
443
444
    // nodes for the case where `seq.nth` is undefined.
445
58
    Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
446
58
    Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n));
447
448
    // the full ite, split on definedness of `seq.nth`
449
58
    Node lemma = nm->mkNode(ITE, cond, b1, b2);
450
451
    // assert:
452
    // IF    n >=0 AND n < len( s )
453
    // THEN: s = sk1 ++ unit(skt) ++ sk2 AND
454
    //       len( sk1 ) = n AND
455
    //       ( len( sk2 ) = len( s )- (n+1)
456
    // ELSE: skt = Uf(s, n), where Uf is a cached skolem function.
457
29
    asserts.push_back(lemma);
458
29
    retNode = skt;
459
  }
460
1593
  else if (t.getKind() == kind::STRING_STRREPL)
461
  {
462
    // processing term: replace( x, y, z )
463
332
    Node x = t[0];
464
332
    Node y = t[1];
465
332
    Node z = t[2];
466
332
    TypeNode tn = t[0].getType();
467
    Node rp1 =
468
332
        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre");
469
    Node rp2 =
470
332
        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
471
332
    Node rpw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
472
473
    // y = ""
474
332
    Node emp = Word::mkEmptyWord(tn);
475
332
    Node cond1 = y.eqNode(emp);
476
    // rpw = str.++( z, x )
477
332
    Node c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x));
478
479
    // contains( x, y )
480
332
    Node cond2 = nm->mkNode(kind::STRING_STRCTN, x, y);
481
    // x = str.++( rp1, y, rp2 )
482
332
    Node c21 = x.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, y, rp2));
483
    // rpw = str.++( rp1, z, rp2 )
484
332
    Node c22 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, z, rp2));
485
    // ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y )
486
    Node c23 =
487
664
        nm->mkNode(kind::STRING_STRCTN,
488
332
                   nm->mkNode(
489
                       kind::STRING_CONCAT,
490
                       rp1,
491
332
                       nm->mkNode(kind::STRING_SUBSTR,
492
                                  y,
493
                                  zero,
494
664
                                  nm->mkNode(kind::MINUS,
495
332
                                             nm->mkNode(kind::STRING_LENGTH, y),
496
                                             one))),
497
                   y)
498
332
            .negate();
499
500
    // assert:
501
    //   IF    y=""
502
    //   THEN: rpw = str.++( z, x )
503
    //   ELIF: contains( x, y )
504
    //   THEN: x = str.++( rp1, y, rp2 ) ^
505
    //         rpw = str.++( rp1, z, rp2 ) ^
506
    //         ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y ),
507
    //   ELSE: rpw = x
508
    // for fresh rp1, rp2, rpw
509
    Node rr = nm->mkNode(kind::ITE,
510
                         cond1,
511
                         c1,
512
664
                         nm->mkNode(kind::ITE,
513
                                    cond2,
514
332
                                    nm->mkNode(kind::AND, c21, c22, c23),
515
664
                                    rpw.eqNode(x)));
516
166
    asserts.push_back(rr);
517
518
    // Thus, replace( x, y, z ) = rpw.
519
166
    retNode = rpw;
520
  }
521
1427
  else if (t.getKind() == kind::STRING_STRREPLALL)
522
  {
523
    // processing term: replaceall( x, y, z )
524
20
    Node x = t[0];
525
20
    Node y = t[1];
526
20
    Node z = t[2];
527
20
    Node rpaw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
528
529
    Node numOcc = sc->mkTypedSkolemCached(
530
20
        nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
531
20
    std::vector<TypeNode> argTypes;
532
10
    argTypes.push_back(nm->integerType());
533
    Node us =
534
20
        nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
535
20
    TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
536
    Node uf = sc->mkTypedSkolemCached(
537
20
        ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
538
539
20
    Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
540
20
    Node usno = nm->mkNode(APPLY_UF, us, numOcc);
541
20
    Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x));
542
543
20
    std::vector<Node> lem;
544
10
    lem.push_back(nm->mkNode(GEQ, numOcc, zero));
545
10
    lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, zero)));
546
10
    lem.push_back(usno.eqNode(rem));
547
10
    lem.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero));
548
10
    lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(negOne));
549
550
20
    Node i = SkolemCache::mkIndexVar(t);
551
20
    Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
552
    Node bound =
553
20
        nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
554
20
    Node ufi = nm->mkNode(APPLY_UF, uf, i);
555
20
    Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one));
556
20
    Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi);
557
    Node cc = nm->mkNode(
558
        STRING_CONCAT,
559
20
        nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)),
560
        z,
561
40
        nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
562
563
20
    std::vector<Node> flem;
564
10
    flem.push_back(ii.eqNode(negOne).negate());
565
10
    flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc));
566
10
    flem.push_back(
567
20
        ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
568
569
20
    Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
570
20
    Node q = mkForallInternal(bvli, body);
571
10
    lem.push_back(q);
572
573
    // assert:
574
    //   IF y=""
575
    //   THEN: rpaw = x
576
    //   ELSE:
577
    //     numOcc >= 0 ^
578
    //     rpaw = Us(0) ^ Us(numOcc) = substr(x, Uf(numOcc), len(x)) ^
579
    //     Uf(0) = 0 ^ indexof( x, y, Uf(numOcc) ) = -1 ^
580
    //     forall i. 0 <= i < numOcc =>
581
    //        ii != -1 ^
582
    //        Us( i ) = str.substr( x, Uf(i), ii - Uf(i) ) ++ z ++ Us(i+1) ^
583
    //        Uf( i+1 ) = ii + len(y)
584
    //        where ii == indexof( x, y, Uf(i) )
585
586
    // Conceptually, numOcc is the number of occurrences of y in x, Uf( i ) is
587
    // the index to begin searching in x for y after the i^th occurrence of y in
588
    // x, and Us( i ) is the result of processing the remainder after processing
589
    // the i^th occurrence of y in x.
590
20
    Node emp = Word::mkEmptyWord(t.getType());
591
    Node assert =
592
20
        nm->mkNode(ITE, y.eqNode(emp), rpaw.eqNode(x), nm->mkNode(AND, lem));
593
10
    asserts.push_back(assert);
594
595
    // Thus, replaceall( x, y, z ) = rpaw
596
10
    retNode = rpaw;
597
  }
598
1417
  else if (t.getKind() == STRING_REPLACE_RE)
599
  {
600
32
    Node x = t[0];
601
32
    Node y = t[1];
602
32
    Node z = t[2];
603
32
    Node k = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "k");
604
605
32
    std::vector<Node> emptyVec;
606
    Node sigmaStar =
607
32
        nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
608
32
    Node re = nm->mkNode(REGEXP_CONCAT, sigmaStar, y, sigmaStar);
609
    // in_re(x, re.++(_*, y, _*))
610
32
    Node hasMatch = nm->mkNode(STRING_IN_REGEXP, x, re);
611
612
    // in_re("", y)
613
    Node matchesEmpty =
614
32
        nm->mkNode(STRING_IN_REGEXP, nm->mkConst(String("")), y);
615
    // k = z ++ x
616
32
    Node res1 = k.eqNode(nm->mkNode(STRING_CONCAT, z, x));
617
618
    Node k1 =
619
32
        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_MATCH_PRE, "rre_pre");
620
    Node k2 =
621
32
        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_MATCH, "rre_match");
622
    Node k3 =
623
32
        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_MATCH_POST, "rre_post");
624
    // x = k1 ++ k2 ++ k3
625
32
    Node splitX = x.eqNode(nm->mkNode(STRING_CONCAT, k1, k2, k3));
626
    // ~in_re(k1 ++ str.substr(k2, 0, str.len(k2) - 1), re.++(_*, y, _*))
627
32
    Node k2len = nm->mkNode(STRING_LENGTH, k2);
628
    Node firstMatch =
629
64
        nm->mkNode(
630
              STRING_IN_REGEXP,
631
32
              nm->mkNode(
632
                  STRING_CONCAT,
633
                  k1,
634
32
                  nm->mkNode(
635
32
                      STRING_SUBSTR, k2, zero, nm->mkNode(MINUS, k2len, one))),
636
              re)
637
32
            .negate();
638
    // in_re(k2, y)
639
32
    Node k2Match = nm->mkNode(STRING_IN_REGEXP, k2, y);
640
    // k = k1 ++ z ++ k3
641
32
    Node res2 = k.eqNode(nm->mkNode(STRING_CONCAT, k1, z, k3));
642
643
    // IF in_re(x, re.++(_*, y, _*))
644
    // THEN:
645
    //   IF in_re("", y)
646
    //   THEN: k = z ++ x
647
    //   ELSE:
648
    //     x = k1 ++ k2 ++ k3 ^
649
    //     ~in_re(k1 ++ substr(k2, 0, str.len(k2) - 1), re.++(_*, y, _*)) ^
650
    //     in_re(k2, y) ^ k = k1 ++ z ++ k3
651
    // ELSE: k = x
652
48
    asserts.push_back(nm->mkNode(
653
        ITE,
654
        hasMatch,
655
32
        nm->mkNode(ITE,
656
                   matchesEmpty,
657
                   res1,
658
32
                   nm->mkNode(AND, splitX, firstMatch, k2Match, res2)),
659
32
        k.eqNode(x)));
660
16
    retNode = k;
661
  }
662
1401
  else if (t.getKind() == STRING_REPLACE_RE_ALL)
663
  {
664
16
    Node x = t[0];
665
16
    Node y = t[1];
666
16
    Node z = t[2];
667
16
    Node k = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "k");
668
669
    Node numOcc = sc->mkTypedSkolemCached(
670
16
        nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
671
16
    std::vector<TypeNode> argTypes;
672
8
    argTypes.push_back(nm->integerType());
673
16
    Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, t.getType()));
674
16
    TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
675
    Node uf = sc->mkTypedSkolemCached(
676
16
        ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
677
    Node ul =
678
16
        sc->mkTypedSkolemCached(ufType, x, y, SkolemCache::SK_OCCUR_LEN, "Ul");
679
680
16
    Node emp = Word::mkEmptyWord(t.getType());
681
682
16
    std::vector<Node> emptyVec;
683
    Node sigmaStar =
684
16
        nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
685
16
    Node yp = nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp));
686
16
    Node re = nm->mkNode(REGEXP_CONCAT, sigmaStar, yp, sigmaStar);
687
    // in_re(x, _* ++ y' ++ _*)
688
16
    Node hasMatch = nm->mkNode(STRING_IN_REGEXP, x, re);
689
690
16
    Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
691
16
    Node usno = nm->mkNode(APPLY_UF, us, numOcc);
692
16
    Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x));
693
694
16
    std::vector<Node> lemmas;
695
    // numOcc > 0
696
8
    lemmas.push_back(nm->mkNode(GT, numOcc, zero));
697
    // k = Us(0)
698
8
    lemmas.push_back(k.eqNode(nm->mkNode(APPLY_UF, us, zero)));
699
    // Us(numOcc) = substr(x, Uf(numOcc))
700
8
    lemmas.push_back(usno.eqNode(rem));
701
    // Uf(0) = 0
702
8
    lemmas.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero));
703
    // not(in_re(substr(x, Uf(numOcc)), re.++(_*, y', _*)))
704
8
    lemmas.push_back(nm->mkNode(STRING_IN_REGEXP, rem, re).negate());
705
706
16
    Node i = SkolemCache::mkIndexVar(t);
707
16
    Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
708
    Node bound =
709
16
        nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
710
16
    Node ip1 = nm->mkNode(PLUS, i, one);
711
16
    Node ufi = nm->mkNode(APPLY_UF, uf, i);
712
16
    Node uli = nm->mkNode(APPLY_UF, ul, i);
713
16
    Node ufip1 = nm->mkNode(APPLY_UF, uf, ip1);
714
16
    Node ii = nm->mkNode(MINUS, ufip1, uli);
715
16
    Node match = nm->mkNode(STRING_SUBSTR, x, ii, uli);
716
    Node pfxMatch =
717
16
        nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi));
718
    Node nonMatch =
719
        nm->mkNode(STRING_SUBSTR,
720
                   x,
721
                   ufi,
722
16
                   nm->mkNode(MINUS, nm->mkNode(MINUS, ufip1, one), ufi));
723
724
16
    std::vector<Node> flem;
725
    // Ul(i) > 0
726
8
    flem.push_back(nm->mkNode(GT, uli, zero));
727
    // Uf(i + 1) >= Uf(i) + Ul(i)
728
8
    flem.push_back(nm->mkNode(GEQ, ufip1, nm->mkNode(PLUS, ufi, uli)));
729
    // in_re(substr(x, ii, Ul(i)), y')
730
8
    flem.push_back(nm->mkNode(STRING_IN_REGEXP, match, yp));
731
    // ~in_re(substr(x, Uf(i), Uf(i + 1) - 1 - Uf(i)), re.++(_*, y', _*))
732
8
    flem.push_back(nm->mkNode(STRING_IN_REGEXP, nonMatch, re).negate());
733
    // Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
734
8
    flem.push_back(
735
16
        nm->mkNode(APPLY_UF, us, i)
736
16
            .eqNode(nm->mkNode(
737
16
                STRING_CONCAT, pfxMatch, z, nm->mkNode(APPLY_UF, us, ip1))));
738
739
16
    Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
740
16
    Node forall = mkForallInternal(bvli, body);
741
8
    lemmas.push_back(forall);
742
743
    // IF in_re(x, re.++(_*, y', _*))
744
    // THEN:
745
    //   numOcc > 0 ^
746
    //   k = Us(0) ^ Us(numOcc) = substr(x, Uf(numOcc)) ^
747
    //   Uf(0) = 0 ^ not(in_re(substr(x, Uf(numOcc)), re.++(_*, y', _*)))
748
    //   forall i. 0 <= i < nummOcc =>
749
    //     Ul(i) > 0 ^
750
    //     Uf(i + 1) >= Uf(i) + Ul(i) ^
751
    //     in_re(substr(x, ii, Ul(i)), y') ^
752
    //     ~in_re(substr(x, Uf(i), Uf(i + 1) - 1 - Uf(i)), re.++(_*, y', _*)) ^
753
    //     Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
754
    //     where ii = Uf(i + 1) - Ul(i)
755
    // ELSE: k = x
756
    // where y' = re.diff(y, "")
757
    //
758
    // Conceptually, y' is the regex y but excluding the empty string (because
759
    // we do not want to match empty strings), numOcc is the number of shortest
760
    // matches of y' in x, Uf(i) is the end position of the i-th match, Ul(i)
761
    // is the length of the i^th match, and Us(i) is the result of processing
762
    // the remainder after processing the i^th occurrence of y in x.
763
8
    asserts.push_back(
764
16
        nm->mkNode(ITE, hasMatch, nm->mkNode(AND, lemmas), k.eqNode(x)));
765
8
    retNode = k;
766
  }
767
1393
  else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER)
768
  {
769
12
    Node x = t[0];
770
12
    Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
771
772
12
    Node lenx = nm->mkNode(STRING_LENGTH, x);
773
12
    Node lenr = nm->mkNode(STRING_LENGTH, r);
774
12
    Node eqLenA = lenx.eqNode(lenr);
775
776
12
    Node i = SkolemCache::mkIndexVar(t);
777
12
    Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
778
779
12
    Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one));
780
12
    Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one));
781
782
12
    Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
783
12
    Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
784
    Node offset =
785
12
        nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? -32 : 32));
786
787
    Node res = nm->mkNode(
788
        ITE,
789
12
        nm->mkNode(AND, nm->mkNode(LEQ, lb, ci), nm->mkNode(LEQ, ci, ub)),
790
12
        nm->mkNode(PLUS, ci, offset),
791
36
        ci);
792
793
    Node bound =
794
12
        nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
795
12
    Node body = nm->mkNode(OR, bound.negate(), ri.eqNode(res));
796
12
    Node rangeA = mkForallInternal(bvi, body);
797
798
    // upper 65 ... 90
799
    // lower 97 ... 122
800
    // assert:
801
    //   len(r) = len(x) ^
802
    //   forall i. 0 <= i < len(r) =>
803
    //     str.code( str.substr(r,i,1) ) = ite( 97 <= ci <= 122, ci-32, ci)
804
    // where ci = str.code( str.substr(x,i,1) )
805
12
    Node assert = nm->mkNode(AND, eqLenA, rangeA);
806
6
    asserts.push_back(assert);
807
808
    // Thus, toLower( x ) = r
809
6
    retNode = r;
810
  }
811
1387
  else if (t.getKind() == STRING_REV)
812
  {
813
36
    Node x = t[0];
814
36
    Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
815
816
36
    Node lenx = nm->mkNode(STRING_LENGTH, x);
817
36
    Node lenr = nm->mkNode(STRING_LENGTH, r);
818
36
    Node eqLenA = lenx.eqNode(lenr);
819
820
36
    Node i = SkolemCache::mkIndexVar(t);
821
36
    Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
822
823
    Node revi = nm->mkNode(
824
36
        MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
825
36
    Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one);
826
36
    Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one);
827
828
    Node bound =
829
36
        nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
830
36
    Node body = nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx));
831
36
    Node rangeA = mkForallInternal(bvi, body);
832
    // assert:
833
    //   len(r) = len(x) ^
834
    //   forall i. 0 <= i < len(r) =>
835
    //     substr(r,i,1) = substr(x,len(x)-(i+1),1)
836
36
    Node assert = nm->mkNode(AND, eqLenA, rangeA);
837
18
    asserts.push_back(assert);
838
839
    // Thus, (str.rev x) = r
840
18
    retNode = r;
841
  }
842
1369
  else if (t.getKind() == kind::STRING_STRCTN)
843
  {
844
246
    Node x = t[0];
845
246
    Node s = t[1];
846
    //negative contains reduces to existential
847
246
    Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
848
246
    Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
849
246
    Node b1 = SkolemCache::mkIndexVar(t);
850
246
    Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
851
    Node body = NodeManager::currentNM()->mkNode(
852
        kind::AND,
853
246
        NodeManager::currentNM()->mkNode(kind::LEQ, zero, b1),
854
369
        NodeManager::currentNM()->mkNode(
855
            kind::LEQ,
856
            b1,
857
246
            NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)),
858
492
        NodeManager::currentNM()->mkNode(
859
            kind::EQUAL,
860
246
            NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
861
861
            s));
862
123
    retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
863
  }
864
1246
  else if (t.getKind() == kind::STRING_LEQ)
865
  {
866
    Node ltp = sc->mkTypedSkolemCached(
867
44
        nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp");
868
44
    Node k = SkolemCache::mkIndexVar(t);
869
870
44
    std::vector<Node> conj;
871
22
    conj.push_back(nm->mkNode(GEQ, k, zero));
872
44
    Node substr[2];
873
44
    Node code[2];
874
66
    for (unsigned r = 0; r < 2; r++)
875
    {
876
88
      Node ta = t[r];
877
88
      Node tb = t[1 - r];
878
44
      substr[r] = nm->mkNode(STRING_SUBSTR, ta, zero, k);
879
44
      code[r] =
880
88
          nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, one));
881
44
      conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta)));
882
    }
883
22
    conj.push_back(substr[0].eqNode(substr[1]));
884
44
    std::vector<Node> ite_ch;
885
22
    ite_ch.push_back(ltp);
886
66
    for (unsigned r = 0; r < 2; r++)
887
    {
888
44
      ite_ch.push_back(nm->mkNode(LT, code[r], code[1 - r]));
889
    }
890
22
    conj.push_back(nm->mkNode(ITE, ite_ch));
891
892
    Node conjn = nm->mkNode(
893
44
        EXISTS, nm->mkNode(BOUND_VAR_LIST, k), nm->mkNode(AND, conj));
894
    // Intuitively, the reduction says either x and y are equal, or they have
895
    // some (maximal) common prefix after which their characters at position k
896
    // are distinct, and the comparison of their code matches the return value
897
    // of the overall term.
898
    // Notice the below reduction relies on the semantics of str.code being -1
899
    // for the empty string. In particular, say x = "a" and y = "ab", then the
900
    // reduction below is satisfied for k = 1, since
901
    //   str.code(substr( "a", 1, 1 )) = str.code( "" ) = -1 <
902
    //   str.code(substr( "ab", 1, 1 )) = str.code( "b" ) = 66
903
904
    // assert:
905
    //  IF x=y
906
    //  THEN: ltp
907
    //  ELSE: exists k.
908
    //        k >= 0 AND k <= len( x ) AND k <= len( y ) AND
909
    //        substr( x, 0, k ) = substr( y, 0, k ) AND
910
    //        IF    ltp
911
    //        THEN: str.code(substr( x, k, 1 )) < str.code(substr( y, k, 1 ))
912
    //        ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 ))
913
44
    Node assert = nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, conjn);
914
22
    asserts.push_back(assert);
915
916
    // Thus, str.<=( x, y ) = ltp
917
22
    retNode = ltp;
918
  }
919
5652
  return retNode;
920
}
921
922
2575
Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts)
923
{
924
2575
  size_t prev_asserts = asserts.size();
925
  // call the static reduce routine
926
2575
  Node retNode = reduce(t, asserts, d_sc);
927
2575
  if( t!=retNode ){
928
1351
    Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
929
1351
    if (!asserts.empty())
930
    {
931
2498
      Trace("strings-preprocess")
932
2498
          << " ... new nodes (" << (asserts.size() - prev_asserts)
933
1249
          << "):" << std::endl;
934
2663
      for (size_t i = prev_asserts; i < asserts.size(); ++i)
935
      {
936
1414
        Trace("strings-preprocess") << "   " << asserts[i] << std::endl;
937
      }
938
    }
939
1351
    if (d_statReductions != nullptr)
940
    {
941
1281
      (*d_statReductions) << t.getKind();
942
    }
943
  }
944
  else
945
  {
946
2448
    Trace("strings-preprocess-debug")
947
1224
        << "Return " << retNode << " unchanged" << std::endl;
948
  }
949
2575
  return retNode;
950
}
951
952
2148
Node StringsPreprocess::simplifyRec(Node t, std::vector<Node>& asserts)
953
{
954
2148
  std::map<Node, Node>::iterator it = d_visited.find(t);
955
2148
  if (it != d_visited.end())
956
  {
957
850
    return it->second;
958
  }else{
959
2596
    Node retNode = t;
960
1298
    if( t.getNumChildren()==0 ){
961
336
      retNode = simplify(t, asserts);
962
    }
963
962
    else if (!t.isClosure())
964
    {
965
958
      bool changed = false;
966
1916
      std::vector< Node > cc;
967
958
      if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){
968
4
        cc.push_back( t.getOperator() );
969
      }
970
2977
      for(unsigned i=0; i<t.getNumChildren(); i++) {
971
4038
        Node s = simplifyRec(t[i], asserts);
972
2019
        cc.push_back( s );
973
2019
        if( s!=t[i] ) {
974
175
          changed = true;
975
        }
976
      }
977
1916
      Node tmp = t;
978
958
      if( changed ){
979
154
        tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
980
      }
981
958
      retNode = simplify(tmp, asserts);
982
    }
983
1298
    d_visited[t] = retNode;
984
1298
    return retNode;
985
  }
986
}
987
988
81
Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
989
{
990
162
  std::vector<Node> asserts_curr;
991
81
  Node ret = simplifyRec(n, asserts_curr);
992
177
  while (!asserts_curr.empty())
993
  {
994
96
    Node curr = asserts_curr.back();
995
48
    asserts_curr.pop_back();
996
96
    std::vector<Node> asserts_tmp;
997
48
    curr = simplifyRec(curr, asserts_tmp);
998
48
    asserts_curr.insert(
999
96
        asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
1000
48
    asserts.push_back(curr);
1001
  }
1002
162
  return ret;
1003
}
1004
1005
89
Node StringsPreprocess::mkForallInternal(Node bvl, Node body)
1006
{
1007
89
  NodeManager* nm = NodeManager::currentNM();
1008
  QInternalVarAttribute qiva;
1009
178
  Node qvar;
1010
89
  if (bvl.hasAttribute(qiva))
1011
  {
1012
12
    qvar = bvl.getAttribute(qiva);
1013
  }
1014
  else
1015
  {
1016
77
    qvar = nm->mkSkolem("qinternal", nm->booleanType());
1017
    // this dummy variable marks that the quantified formula is internal
1018
77
    qvar.setAttribute(InternalQuantAttribute(), true);
1019
    // remember the dummy variable
1020
77
    bvl.setAttribute(qiva, qvar);
1021
  }
1022
  // make the internal attribute, and put it in a singleton list
1023
178
  Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
1024
178
  Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
1025
  // make the overall formula
1026
178
  return nm->mkNode(FORALL, bvl, body, ipl);
1027
}
1028
1029
}/* CVC4::theory::strings namespace */
1030
}/* CVC4::theory namespace */
1031
26685
}/* CVC4 namespace */