GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/arith_entail.cpp Lines: 344 384 89.6 %
Date: 2021-03-22 Branches: 878 1918 45.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_entail.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of arithmetic entailment computation for string terms.
13
 **/
14
15
#include "theory/strings/arith_entail.h"
16
17
#include "expr/attribute.h"
18
#include "expr/node_algorithm.h"
19
#include "theory/arith/arith_msum.h"
20
#include "theory/rewriter.h"
21
#include "theory/strings/theory_strings_utils.h"
22
#include "theory/strings/word.h"
23
#include "theory/theory.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace strings {
30
31
829
bool ArithEntail::checkEq(Node a, Node b)
32
{
33
829
  if (a == b)
34
  {
35
    return true;
36
  }
37
1658
  Node ar = Rewriter::rewrite(a);
38
1658
  Node br = Rewriter::rewrite(b);
39
829
  return ar == br;
40
}
41
42
547561
bool ArithEntail::check(Node a, Node b, bool strict)
43
{
44
547561
  if (a == b)
45
  {
46
13183
    return !strict;
47
  }
48
1068756
  Node diff = NodeManager::currentNM()->mkNode(kind::MINUS, a, b);
49
534378
  return check(diff, strict);
50
}
51
52
struct StrCheckEntailArithTag
53
{
54
};
55
struct StrCheckEntailArithComputedTag
56
{
57
};
58
/** Attribute true for expressions for which check returned true */
59
typedef expr::Attribute<StrCheckEntailArithTag, bool> StrCheckEntailArithAttr;
60
typedef expr::Attribute<StrCheckEntailArithComputedTag, bool>
61
    StrCheckEntailArithComputedAttr;
62
63
803618
bool ArithEntail::check(Node a, bool strict)
64
{
65
803618
  if (a.isConst())
66
  {
67
88624
    return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
68
  }
69
70
  Node ar = strict ? NodeManager::currentNM()->mkNode(
71
954100
                kind::MINUS, a, NodeManager::currentNM()->mkConst(Rational(1)))
72
1669094
                   : a;
73
714994
  ar = Rewriter::rewrite(ar);
74
75
714994
  if (ar.getAttribute(StrCheckEntailArithComputedAttr()))
76
  {
77
552135
    return ar.getAttribute(StrCheckEntailArithAttr());
78
  }
79
80
162859
  bool ret = checkInternal(ar);
81
162859
  if (!ret)
82
  {
83
    // try with approximations
84
152540
    ret = checkApprox(ar);
85
  }
86
  // cache the result
87
162859
  ar.setAttribute(StrCheckEntailArithAttr(), ret);
88
162859
  ar.setAttribute(StrCheckEntailArithComputedAttr(), true);
89
162859
  return ret;
90
}
91
92
152540
bool ArithEntail::checkApprox(Node ar)
93
{
94
152540
  Assert(Rewriter::rewrite(ar) == ar);
95
152540
  NodeManager* nm = NodeManager::currentNM();
96
305080
  std::map<Node, Node> msum;
97
305080
  Trace("strings-ent-approx-debug")
98
152540
      << "Setup arithmetic approximations for " << ar << std::endl;
99
152540
  if (!ArithMSum::getMonomialSum(ar, msum))
100
  {
101
    Trace("strings-ent-approx-debug")
102
        << "...failed to get monomial sum!" << std::endl;
103
    return false;
104
  }
105
  // for each monomial v*c, mApprox[v] a list of
106
  // possibilities for how the term can be soundly approximated, that is,
107
  // if mApprox[v] contains av, then v*c > av*c. Notice that if c
108
  // is positive, then v > av, otherwise if c is negative, then v < av.
109
  // In other words, av is an under-approximation if c is positive, and an
110
  // over-approximation if c is negative.
111
152540
  bool changed = false;
112
305080
  std::map<Node, std::vector<Node> > mApprox;
113
  // map from approximations to their monomial sums
114
305080
  std::map<Node, std::map<Node, Node> > approxMsums;
115
  // aarSum stores each monomial that does not have multiple approximations
116
305080
  std::vector<Node> aarSum;
117
553022
  for (std::pair<const Node, Node>& m : msum)
118
  {
119
800964
    Node v = m.first;
120
800964
    Node c = m.second;
121
800964
    Trace("strings-ent-approx-debug")
122
400482
        << "Get approximations " << v << "..." << std::endl;
123
400482
    if (v.isNull())
124
    {
125
230920
      Node mn = c.isNull() ? nm->mkConst(Rational(1)) : c;
126
115460
      aarSum.push_back(mn);
127
    }
128
    else
129
    {
130
      // c.isNull() means c = 1
131
285022
      bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1;
132
285022
      std::vector<Node>& approx = mApprox[v];
133
570044
      std::unordered_set<Node, NodeHashFunction> visited;
134
570044
      std::vector<Node> toProcess;
135
285022
      toProcess.push_back(v);
136
49095
      do
137
      {
138
668234
        Node curr = toProcess.back();
139
334117
        Trace("strings-ent-approx-debug") << "  process " << curr << std::endl;
140
334117
        curr = Rewriter::rewrite(curr);
141
334117
        toProcess.pop_back();
142
334117
        if (visited.find(curr) == visited.end())
143
        {
144
330537
          visited.insert(curr);
145
661074
          std::vector<Node> currApprox;
146
330537
          getArithApproximations(curr, currApprox, isOverApprox);
147
330537
          if (currApprox.empty())
148
          {
149
594558
            Trace("strings-ent-approx-debug")
150
297279
                << "...approximation: " << curr << std::endl;
151
            // no approximations, thus curr is a possibility
152
297279
            approx.push_back(curr);
153
          }
154
          else
155
          {
156
33258
            toProcess.insert(
157
66516
                toProcess.end(), currApprox.begin(), currApprox.end());
158
          }
159
        }
160
334117
      } while (!toProcess.empty());
161
285022
      Assert(!approx.empty());
162
      // if we have only one approximation, move it to final
163
285022
      if (approx.size() == 1)
164
      {
165
272777
        changed = v != approx[0];
166
545554
        Node mn = ArithMSum::mkCoeffTerm(c, approx[0]);
167
272777
        aarSum.push_back(mn);
168
272777
        mApprox.erase(v);
169
      }
170
      else
171
      {
172
        // compute monomial sum form for each approximation, used below
173
36747
        for (const Node& aa : approx)
174
        {
175
24502
          if (approxMsums.find(aa) == approxMsums.end())
176
          {
177
            CVC4_UNUSED bool ret =
178
23486
                ArithMSum::getMonomialSum(aa, approxMsums[aa]);
179
23486
            Assert(ret);
180
          }
181
        }
182
12245
        changed = true;
183
      }
184
    }
185
  }
186
152540
  if (!changed)
187
  {
188
    // approximations had no effect, return
189
134397
    Trace("strings-ent-approx-debug") << "...no approximations" << std::endl;
190
134397
    return false;
191
  }
192
  // get the current "fixed" sum for the abstraction of ar
193
18143
  Node aar = aarSum.empty()
194
19646
                 ? nm->mkConst(Rational(0))
195
37789
                 : (aarSum.size() == 1 ? aarSum[0] : nm->mkNode(PLUS, aarSum));
196
18143
  aar = Rewriter::rewrite(aar);
197
36286
  Trace("strings-ent-approx-debug")
198
36286
      << "...processed fixed sum " << aar << " with " << mApprox.size()
199
18143
      << " approximated monomials." << std::endl;
200
  // if we have a choice of how to approximate
201
18143
  if (!mApprox.empty())
202
  {
203
    // convert aar back to monomial sum
204
17158
    std::map<Node, Node> msumAar;
205
8579
    if (!ArithMSum::getMonomialSum(aar, msumAar))
206
    {
207
      return false;
208
    }
209
8579
    if (Trace.isOn("strings-ent-approx"))
210
    {
211
      Trace("strings-ent-approx")
212
          << "---- Check arithmetic entailment by under-approximation " << ar
213
          << " >= 0" << std::endl;
214
      Trace("strings-ent-approx") << "FIXED:" << std::endl;
215
      ArithMSum::debugPrintMonomialSum(msumAar, "strings-ent-approx");
216
      Trace("strings-ent-approx") << "APPROX:" << std::endl;
217
      for (std::pair<const Node, std::vector<Node> >& a : mApprox)
218
      {
219
        Node c = msum[a.first];
220
        Trace("strings-ent-approx") << "  ";
221
        if (!c.isNull())
222
        {
223
          Trace("strings-ent-approx") << c << " * ";
224
        }
225
        Trace("strings-ent-approx")
226
            << a.second << " ...from " << a.first << std::endl;
227
      }
228
      Trace("strings-ent-approx") << std::endl;
229
    }
230
17158
    Rational one(1);
231
    // incorporate monomials one at a time that have a choice of approximations
232
25895
    while (!mApprox.empty())
233
    {
234
17316
      Node v;
235
17316
      Node vapprox;
236
8658
      int maxScore = -1;
237
      // Look at each approximation, take the one with the best score.
238
      // Notice that we are in the process of trying to prove
239
      // ( c1*t1 + .. + cn*tn ) + ( approx_1 | ... | approx_m ) >= 0,
240
      // where c1*t1 + .. + cn*tn is the "fixed" component of our sum (aar)
241
      // and approx_1 ... approx_m are possible approximations. The
242
      // intution here is that we want coefficients c1...cn to be positive.
243
      // This is because arithmetic string terms t1...tn (which may be
244
      // applications of len, indexof, str.to.int) are never entailed to be
245
      // negative. Hence, we add the approx_i that contributes the "most"
246
      // towards making all constants c1...cn positive and cancelling negative
247
      // monomials in approx_i itself.
248
8658
      for (std::pair<const Node, std::vector<Node> >& nam : mApprox)
249
      {
250
8658
        Node cr = msum[nam.first];
251
25986
        for (const Node& aa : nam.second)
252
        {
253
17328
          unsigned helpsCancelCount = 0;
254
17328
          unsigned addsObligationCount = 0;
255
17328
          std::map<Node, Node>::iterator it;
256
          // we are processing an approximation cr*( c1*t1 + ... + cn*tn )
257
37722
          for (std::pair<const Node, Node>& aam : approxMsums[aa])
258
          {
259
            // Say aar is of the form t + c*ti, and aam is the monomial ci*ti
260
            // where ci != 0. We say aam:
261
            // (1) helps cancel if c != 0 and c>0 != ci>0
262
            // (2) adds obligation if c>=0 and c+ci<0
263
40788
            Node ti = aam.first;
264
40788
            Node ci = aam.second;
265
20394
            if (!cr.isNull())
266
            {
267
32941
              ci = ci.isNull() ? cr
268
32941
                               : Rewriter::rewrite(nm->mkNode(MULT, ci, cr));
269
            }
270
20394
            Trace("strings-ent-approx-debug") << ci << "*" << ti << " ";
271
20394
            int ciSgn = ci.isNull() ? 1 : ci.getConst<Rational>().sgn();
272
20394
            it = msumAar.find(ti);
273
20394
            if (it != msumAar.end())
274
            {
275
25508
              Node c = it->second;
276
12754
              int cSgn = c.isNull() ? 1 : c.getConst<Rational>().sgn();
277
12754
              if (cSgn == 0)
278
              {
279
2038
                addsObligationCount += (ciSgn == -1 ? 1 : 0);
280
              }
281
10716
              else if (cSgn != ciSgn)
282
              {
283
9578
                helpsCancelCount++;
284
19156
                Rational r1 = c.isNull() ? one : c.getConst<Rational>();
285
19156
                Rational r2 = ci.isNull() ? one : ci.getConst<Rational>();
286
19156
                Rational r12 = r1 + r2;
287
9578
                if (r12.sgn() == -1)
288
                {
289
7311
                  addsObligationCount++;
290
                }
291
              }
292
            }
293
            else
294
            {
295
7640
              addsObligationCount += (ciSgn == -1 ? 1 : 0);
296
            }
297
          }
298
34656
          Trace("strings-ent-approx-debug")
299
17328
              << "counts=" << helpsCancelCount << "," << addsObligationCount
300
17328
              << " for " << aa << " into " << aar << std::endl;
301
34656
          int score = (addsObligationCount > 0 ? 0 : 2)
302
17328
                      + (helpsCancelCount > 0 ? 1 : 0);
303
          // if its the best, update v and vapprox
304
17328
          if (v.isNull() || score > maxScore)
305
          {
306
11254
            v = nam.first;
307
11254
            vapprox = aa;
308
11254
            maxScore = score;
309
          }
310
        }
311
8658
        if (!v.isNull())
312
        {
313
8658
          break;
314
        }
315
      }
316
17316
      Trace("strings-ent-approx")
317
8658
          << "- Decide " << v << " = " << vapprox << std::endl;
318
      // we incorporate v approximated by vapprox into the overall approximation
319
      // for ar
320
8658
      Assert(!v.isNull() && !vapprox.isNull());
321
8658
      Assert(msum.find(v) != msum.end());
322
17316
      Node mn = ArithMSum::mkCoeffTerm(msum[v], vapprox);
323
8658
      aar = nm->mkNode(PLUS, aar, mn);
324
      // update the msumAar map
325
8658
      aar = Rewriter::rewrite(aar);
326
8658
      msumAar.clear();
327
8658
      if (!ArithMSum::getMonomialSum(aar, msumAar))
328
      {
329
        Assert(false);
330
        Trace("strings-ent-approx")
331
            << "...failed to get monomial sum!" << std::endl;
332
        return false;
333
      }
334
      // we have processed the approximation for v
335
8658
      mApprox.erase(v);
336
    }
337
8579
    Trace("strings-ent-approx") << "-----------------" << std::endl;
338
  }
339
18143
  if (aar == ar)
340
  {
341
    Trace("strings-ent-approx-debug")
342
        << "...approximation had no effect" << std::endl;
343
    // this should never happen, but we avoid the infinite loop for sanity here
344
    Assert(false);
345
    return false;
346
  }
347
  // Check entailment on the approximation of ar.
348
  // Notice that this may trigger further reasoning by approximation. For
349
  // example, len( replace( x ++ y, substr( x, 0, n ), z ) ) may be
350
  // under-approximated as len( x ) + len( y ) - len( substr( x, 0, n ) ) on
351
  // this call, where in the recursive call we may over-approximate
352
  // len( substr( x, 0, n ) ) as len( x ). In this example, we can infer
353
  // that len( replace( x ++ y, substr( x, 0, n ), z ) ) >= len( y ) in two
354
  // steps.
355
18143
  if (check(aar))
356
  {
357
3288
    Trace("strings-ent-approx")
358
1644
        << "*** StrArithApprox: showed " << ar
359
1644
        << " >= 0 using under-approximation!" << std::endl;
360
3288
    Trace("strings-ent-approx")
361
1644
        << "*** StrArithApprox: under-approximation was " << aar << std::endl;
362
1644
    return true;
363
  }
364
16499
  return false;
365
}
366
367
331017
void ArithEntail::getArithApproximations(Node a,
368
                                         std::vector<Node>& approx,
369
                                         bool isOverApprox)
370
{
371
331017
  NodeManager* nm = NodeManager::currentNM();
372
  // We do not handle PLUS here since this leads to exponential behavior.
373
  // Instead, this is managed, e.g. during checkApprox, where
374
  // PLUS terms are expanded "on-demand" during the reasoning.
375
662034
  Trace("strings-ent-approx-debug")
376
331017
      << "Get arith approximations " << a << std::endl;
377
331017
  Kind ak = a.getKind();
378
331017
  if (ak == MULT)
379
  {
380
960
    Node c;
381
960
    Node v;
382
480
    if (ArithMSum::getMonomial(a, c, v))
383
    {
384
480
      bool isNeg = c.getConst<Rational>().sgn() == -1;
385
480
      getArithApproximations(v, approx, isNeg ? !isOverApprox : isOverApprox);
386
504
      for (unsigned i = 0, size = approx.size(); i < size; i++)
387
      {
388
24
        approx[i] = nm->mkNode(MULT, c, approx[i]);
389
      }
390
    }
391
  }
392
330537
  else if (ak == STRING_LENGTH)
393
  {
394
293785
    Kind aak = a[0].getKind();
395
293785
    if (aak == STRING_SUBSTR)
396
    {
397
      // over,under-approximations for len( substr( x, n, m ) )
398
81422
      Node lenx = nm->mkNode(STRING_LENGTH, a[0][0]);
399
40711
      if (isOverApprox)
400
      {
401
        // m >= 0 implies
402
        //  m >= len( substr( x, n, m ) )
403
22794
        if (check(a[0][2]))
404
        {
405
14408
          approx.push_back(a[0][2]);
406
        }
407
22794
        if (check(lenx, a[0][1]))
408
        {
409
          // n <= len( x ) implies
410
          //   len( x ) - n >= len( substr( x, n, m ) )
411
7839
          approx.push_back(nm->mkNode(MINUS, lenx, a[0][1]));
412
        }
413
        else
414
        {
415
          // len( x ) >= len( substr( x, n, m ) )
416
14955
          approx.push_back(lenx);
417
        }
418
      }
419
      else
420
      {
421
        // 0 <= n and n+m <= len( x ) implies
422
        //   m <= len( substr( x, n, m ) )
423
35834
        Node npm = nm->mkNode(PLUS, a[0][1], a[0][2]);
424
17917
        if (check(a[0][1]) && check(lenx, npm))
425
        {
426
2373
          approx.push_back(a[0][2]);
427
        }
428
        // 0 <= n and n+m >= len( x ) implies
429
        //   len(x)-n <= len( substr( x, n, m ) )
430
17917
        if (check(a[0][1]) && check(npm, lenx))
431
        {
432
1573
          approx.push_back(nm->mkNode(MINUS, lenx, a[0][1]));
433
        }
434
      }
435
    }
436
253074
    else if (aak == STRING_STRREPL)
437
    {
438
      // over,under-approximations for len( replace( x, y, z ) )
439
      // notice this is either len( x ) or ( len( x ) + len( z ) - len( y ) )
440
7446
      Node lenx = nm->mkNode(STRING_LENGTH, a[0][0]);
441
7446
      Node leny = nm->mkNode(STRING_LENGTH, a[0][1]);
442
7446
      Node lenz = nm->mkNode(STRING_LENGTH, a[0][2]);
443
3723
      if (isOverApprox)
444
      {
445
2023
        if (check(leny, lenz))
446
        {
447
          // len( y ) >= len( z ) implies
448
          //   len( x ) >= len( replace( x, y, z ) )
449
592
          approx.push_back(lenx);
450
        }
451
        else
452
        {
453
          // len( x ) + len( z ) >= len( replace( x, y, z ) )
454
1431
          approx.push_back(nm->mkNode(PLUS, lenx, lenz));
455
        }
456
      }
457
      else
458
      {
459
1700
        if (check(lenz, leny) || check(lenz, lenx))
460
        {
461
          // len( y ) <= len( z ) or len( x ) <= len( z ) implies
462
          //   len( x ) <= len( replace( x, y, z ) )
463
788
          approx.push_back(lenx);
464
        }
465
        else
466
        {
467
          // len( x ) - len( y ) <= len( replace( x, y, z ) )
468
912
          approx.push_back(nm->mkNode(MINUS, lenx, leny));
469
        }
470
      }
471
    }
472
249351
    else if (aak == STRING_ITOS)
473
    {
474
      // over,under-approximations for len( int.to.str( x ) )
475
375
      if (isOverApprox)
476
      {
477
191
        if (check(a[0][0], false))
478
        {
479
81
          if (check(a[0][0], true))
480
          {
481
            // x > 0 implies
482
            //   x >= len( int.to.str( x ) )
483
7
            approx.push_back(a[0][0]);
484
          }
485
          else
486
          {
487
            // x >= 0 implies
488
            //   x+1 >= len( int.to.str( x ) )
489
74
            approx.push_back(
490
148
                nm->mkNode(PLUS, nm->mkConst(Rational(1)), a[0][0]));
491
          }
492
        }
493
      }
494
      else
495
      {
496
184
        if (check(a[0][0]))
497
        {
498
          // x >= 0 implies
499
          //   len( int.to.str( x ) ) >= 1
500
60
          approx.push_back(nm->mkConst(Rational(1)));
501
        }
502
        // other crazy things are possible here, e.g.
503
        // len( int.to.str( len( y ) + 10 ) ) >= 2
504
      }
505
    }
506
  }
507
36752
  else if (ak == STRING_STRIDOF)
508
  {
509
    // over,under-approximations for indexof( x, y, n )
510
4083
    if (isOverApprox)
511
    {
512
4352
      Node lenx = nm->mkNode(STRING_LENGTH, a[0]);
513
4352
      Node leny = nm->mkNode(STRING_LENGTH, a[1]);
514
2176
      if (check(lenx, leny))
515
      {
516
        // len( x ) >= len( y ) implies
517
        //   len( x ) - len( y ) >= indexof( x, y, n )
518
8
        approx.push_back(nm->mkNode(MINUS, lenx, leny));
519
      }
520
      else
521
      {
522
        // len( x ) >= indexof( x, y, n )
523
2168
        approx.push_back(lenx);
524
      }
525
    }
526
    else
527
    {
528
      // TODO?:
529
      // contains( substr( x, n, len( x ) ), y ) implies
530
      //   n <= indexof( x, y, n )
531
      // ...hard to test, runs risk of non-termination
532
533
      // -1 <= indexof( x, y, n )
534
1907
      approx.push_back(nm->mkConst(Rational(-1)));
535
    }
536
  }
537
32669
  else if (ak == STRING_STOI)
538
  {
539
    // over,under-approximations for str.to.int( x )
540
    if (isOverApprox)
541
    {
542
      // TODO?:
543
      // y >= 0 implies
544
      //   y >= str.to.int( int.to.str( y ) )
545
    }
546
    else
547
    {
548
      // -1 <= str.to.int( x )
549
      approx.push_back(nm->mkConst(Rational(-1)));
550
    }
551
  }
552
331017
  Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl;
553
331017
}
554
555
54455
bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
556
{
557
54455
  Assert(assumption.getKind() == kind::EQUAL);
558
54455
  Assert(Rewriter::rewrite(assumption) == assumption);
559
108910
  Trace("strings-entail") << "checkWithEqAssumption: " << assumption << " " << a
560
54455
                          << ", strict=" << strict << std::endl;
561
562
  // Find candidates variables to compute substitutions for
563
108910
  std::unordered_set<Node, NodeHashFunction> candVars;
564
108910
  std::vector<Node> toVisit = {assumption};
565
669789
  while (!toVisit.empty())
566
  {
567
615334
    Node curr = toVisit.back();
568
307667
    toVisit.pop_back();
569
570
878061
    if (curr.getKind() == kind::PLUS || curr.getKind() == kind::MULT
571
552946
        || curr.getKind() == kind::MINUS || curr.getKind() == kind::EQUAL)
572
    {
573
370055
      for (const auto& currChild : curr)
574
      {
575
253212
        toVisit.push_back(currChild);
576
      }
577
    }
578
190824
    else if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH)
579
    {
580
10706
      candVars.insert(curr);
581
    }
582
180118
    else if (curr.getKind() == kind::STRING_LENGTH)
583
    {
584
110702
      candVars.insert(curr);
585
    }
586
  }
587
588
  // Check if any of the candidate variables are in n
589
108910
  Node v;
590
54455
  Assert(toVisit.empty());
591
54455
  toVisit.push_back(a);
592
532545
  while (!toVisit.empty())
593
  {
594
500884
    Node curr = toVisit.back();
595
261839
    toVisit.pop_back();
596
597
532435
    for (const auto& currChild : curr)
598
    {
599
270596
      toVisit.push_back(currChild);
600
    }
601
602
261839
    if (candVars.find(curr) != candVars.end())
603
    {
604
22794
      v = curr;
605
22794
      break;
606
    }
607
  }
608
609
54455
  if (v.isNull())
610
  {
611
    // No suitable candidate found
612
31661
    return false;
613
  }
614
615
45588
  Node solution = ArithMSum::solveEqualityFor(assumption, v);
616
22794
  if (solution.isNull())
617
  {
618
    // Could not solve for v
619
96
    return false;
620
  }
621
45396
  Trace("strings-entail") << "checkWithEqAssumption: subs " << v << " -> "
622
22698
                          << solution << std::endl;
623
624
  // use capture avoiding substitution
625
22698
  a = expr::substituteCaptureAvoiding(a, v, solution);
626
22698
  return check(a, strict);
627
}
628
629
81608
bool ArithEntail::checkWithAssumption(Node assumption,
630
                                      Node a,
631
                                      Node b,
632
                                      bool strict)
633
{
634
81608
  Assert(Rewriter::rewrite(assumption) == assumption);
635
636
81608
  NodeManager* nm = NodeManager::currentNM();
637
638
81608
  if (!assumption.isConst() && assumption.getKind() != kind::EQUAL)
639
  {
640
    // We rewrite inequality assumptions from x <= y to x + (str.len s) = y
641
    // where s is some fresh string variable. We use (str.len s) because
642
    // (str.len s) must be non-negative for the equation to hold.
643
108894
    Node x, y;
644
54447
    if (assumption.getKind() == kind::GEQ)
645
    {
646
44575
      x = assumption[0];
647
44575
      y = assumption[1];
648
    }
649
    else
650
    {
651
      // (not (>= s t)) --> (>= (t - 1) s)
652
9872
      Assert(assumption.getKind() == kind::NOT
653
             && assumption[0].getKind() == kind::GEQ);
654
9872
      x = nm->mkNode(kind::MINUS, assumption[0][1], nm->mkConst(Rational(1)));
655
9872
      y = assumption[0][0];
656
    }
657
658
108894
    Node s = nm->mkBoundVar("slackVal", nm->stringType());
659
108894
    Node slen = nm->mkNode(kind::STRING_LENGTH, s);
660
54447
    assumption = Rewriter::rewrite(
661
108894
        nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen)));
662
  }
663
664
163216
  Node diff = nm->mkNode(kind::MINUS, a, b);
665
81608
  bool res = false;
666
81608
  if (assumption.isConst())
667
  {
668
27153
    bool assumptionBool = assumption.getConst<bool>();
669
27153
    if (assumptionBool)
670
    {
671
27153
      res = check(diff, strict);
672
    }
673
    else
674
    {
675
      res = true;
676
    }
677
  }
678
  else
679
  {
680
54455
    res = checkWithEqAssumption(assumption, diff, strict);
681
  }
682
163216
  return res;
683
}
684
685
bool ArithEntail::checkWithAssumptions(std::vector<Node> assumptions,
686
                                       Node a,
687
                                       Node b,
688
                                       bool strict)
689
{
690
  // TODO: We currently try to show the entailment with each assumption
691
  // independently. In the future, we should make better use of multiple
692
  // assumptions.
693
  bool res = false;
694
  for (const auto& assumption : assumptions)
695
  {
696
    Assert(Rewriter::rewrite(assumption) == assumption);
697
698
    if (checkWithAssumption(assumption, a, b, strict))
699
    {
700
      res = true;
701
      break;
702
    }
703
  }
704
  return res;
705
}
706
707
34992
Node ArithEntail::getConstantBound(Node a, bool isLower)
708
{
709
34992
  Assert(Rewriter::rewrite(a) == a);
710
34992
  Node ret;
711
34992
  if (a.isConst())
712
  {
713
14448
    ret = a;
714
  }
715
20544
  else if (a.getKind() == kind::STRING_LENGTH)
716
  {
717
2900
    if (isLower)
718
    {
719
2900
      ret = NodeManager::currentNM()->mkConst(Rational(0));
720
    }
721
  }
722
17644
  else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
723
  {
724
24684
    std::vector<Node> children;
725
12342
    bool success = true;
726
21618
    for (unsigned i = 0; i < a.getNumChildren(); i++)
727
    {
728
29782
      Node ac = getConstantBound(a[i], isLower);
729
20506
      if (ac.isNull())
730
      {
731
6010
        ret = ac;
732
6010
        success = false;
733
6010
        break;
734
      }
735
      else
736
      {
737
14496
        if (ac.getConst<Rational>().sgn() == 0)
738
        {
739
2616
          if (a.getKind() == kind::MULT)
740
          {
741
4
            ret = ac;
742
4
            success = false;
743
4
            break;
744
          }
745
        }
746
        else
747
        {
748
11880
          if (a.getKind() == kind::MULT)
749
          {
750
5224
            if ((ac.getConst<Rational>().sgn() > 0) != isLower)
751
            {
752
5216
              ret = Node::null();
753
5216
              success = false;
754
5216
              break;
755
            }
756
          }
757
6664
          children.push_back(ac);
758
        }
759
      }
760
    }
761
12342
    if (success)
762
    {
763
1112
      if (children.empty())
764
      {
765
198
        ret = NodeManager::currentNM()->mkConst(Rational(0));
766
      }
767
914
      else if (children.size() == 1)
768
      {
769
914
        ret = children[0];
770
      }
771
      else
772
      {
773
        ret = NodeManager::currentNM()->mkNode(a.getKind(), children);
774
        ret = Rewriter::rewrite(ret);
775
      }
776
    }
777
  }
778
69984
  Trace("strings-rewrite-cbound")
779
34992
      << "Constant " << (isLower ? "lower" : "upper") << " bound for " << a
780
34992
      << " is " << ret << std::endl;
781
34992
  Assert(ret.isNull() || ret.isConst());
782
  // entailment check should be at least as powerful as computing a lower bound
783
34992
  Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() < 0
784
         || check(a, false));
785
34992
  Assert(!isLower || ret.isNull() || ret.getConst<Rational>().sgn() <= 0
786
         || check(a, true));
787
34992
  return ret;
788
}
789
790
428465
bool ArithEntail::checkInternal(Node a)
791
{
792
428465
  Assert(Rewriter::rewrite(a) == a);
793
  // check whether a >= 0
794
428465
  if (a.isConst())
795
  {
796
183503
    return a.getConst<Rational>().sgn() >= 0;
797
  }
798
244962
  else if (a.getKind() == kind::STRING_LENGTH)
799
  {
800
    // str.len( t ) >= 0
801
33168
    return true;
802
  }
803
211794
  else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)
804
  {
805
267258
    for (unsigned i = 0; i < a.getNumChildren(); i++)
806
    {
807
265606
      if (!checkInternal(a[i]))
808
      {
809
207638
        return false;
810
      }
811
    }
812
    // t1 >= 0 ^ ... ^ tn >= 0 => t1 op ... op tn >= 0
813
1652
    return true;
814
  }
815
816
2504
  return false;
817
}
818
819
1301
bool ArithEntail::inferZerosInSumGeq(Node x,
820
                                     std::vector<Node>& ys,
821
                                     std::vector<Node>& zeroYs)
822
{
823
1301
  Assert(zeroYs.empty());
824
825
1301
  NodeManager* nm = NodeManager::currentNM();
826
827
  // Check if we can show that y1 + ... + yn >= x
828
2602
  Node sum = (ys.size() > 1) ? nm->mkNode(PLUS, ys) : ys[0];
829
1301
  if (!check(sum, x))
830
  {
831
433
    return false;
832
  }
833
834
  // Try to remove yi one-by-one and check if we can still show:
835
  //
836
  // y1 + ... + yi-1 +  yi+1 + ... + yn >= x
837
  //
838
  // If that's the case, we know that yi can be zero and the inequality still
839
  // holds.
840
868
  size_t i = 0;
841
5454
  while (i < ys.size())
842
  {
843
4586
    Node yi = ys[i];
844
2293
    std::vector<Node>::iterator pos = ys.erase(ys.begin() + i);
845
2293
    if (ys.size() > 1)
846
    {
847
829
      sum = nm->mkNode(PLUS, ys);
848
    }
849
    else
850
    {
851
1464
      sum = ys.size() == 1 ? ys[0] : nm->mkConst(Rational(0));
852
    }
853
854
2293
    if (check(sum, x))
855
    {
856
828
      zeroYs.push_back(yi);
857
    }
858
    else
859
    {
860
1465
      ys.insert(pos, yi);
861
1465
      i++;
862
    }
863
  }
864
868
  return true;
865
}
866
867
}  // namespace strings
868
}  // namespace theory
869
26676
}  // namespace CVC4