GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/extf_solver.cpp Lines: 311 340 91.5 %
Date: 2021-03-23 Branches: 788 1686 46.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file extf_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Gereon Kremer
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 solver for extended functions of theory of strings.
13
 **/
14
15
#include "theory/strings/extf_solver.h"
16
17
#include "options/strings_options.h"
18
#include "theory/strings/sequences_rewriter.h"
19
#include "theory/strings/theory_strings_preprocess.h"
20
#include "theory/strings/theory_strings_utils.h"
21
22
using namespace std;
23
using namespace CVC4::context;
24
using namespace CVC4::kind;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace strings {
29
30
8997
ExtfSolver::ExtfSolver(SolverState& s,
31
                       InferenceManager& im,
32
                       TermRegistry& tr,
33
                       StringsRewriter& rewriter,
34
                       BaseSolver& bs,
35
                       CoreSolver& cs,
36
                       ExtTheory& et,
37
8997
                       SequencesStatistics& statistics)
38
    : d_state(s),
39
      d_im(im),
40
      d_termReg(tr),
41
      d_rewriter(rewriter),
42
      d_bsolver(bs),
43
      d_csolver(cs),
44
      d_extt(et),
45
      d_statistics(statistics),
46
8997
      d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions),
47
      d_hasExtf(s.getSatContext(), false),
48
      d_extfInferCache(s.getSatContext()),
49
17994
      d_reduced(s.getUserContext())
50
{
51
8997
  d_extt.addFunctionKind(kind::STRING_SUBSTR);
52
8997
  d_extt.addFunctionKind(kind::STRING_UPDATE);
53
8997
  d_extt.addFunctionKind(kind::STRING_STRIDOF);
54
8997
  d_extt.addFunctionKind(kind::STRING_ITOS);
55
8997
  d_extt.addFunctionKind(kind::STRING_STOI);
56
8997
  d_extt.addFunctionKind(kind::STRING_STRREPL);
57
8997
  d_extt.addFunctionKind(kind::STRING_STRREPLALL);
58
8997
  d_extt.addFunctionKind(kind::STRING_REPLACE_RE);
59
8997
  d_extt.addFunctionKind(kind::STRING_REPLACE_RE_ALL);
60
8997
  d_extt.addFunctionKind(kind::STRING_STRCTN);
61
8997
  d_extt.addFunctionKind(kind::STRING_IN_REGEXP);
62
8997
  d_extt.addFunctionKind(kind::STRING_LEQ);
63
8997
  d_extt.addFunctionKind(kind::STRING_TO_CODE);
64
8997
  d_extt.addFunctionKind(kind::STRING_TOLOWER);
65
8997
  d_extt.addFunctionKind(kind::STRING_TOUPPER);
66
8997
  d_extt.addFunctionKind(kind::STRING_REV);
67
8997
  d_extt.addFunctionKind(kind::SEQ_UNIT);
68
8997
  d_extt.addFunctionKind(kind::SEQ_NTH);
69
70
8997
  d_true = NodeManager::currentNM()->mkConst(true);
71
8997
  d_false = NodeManager::currentNM()->mkConst(false);
72
8997
}
73
74
8994
ExtfSolver::~ExtfSolver() {}
75
76
106650
bool ExtfSolver::doReduction(int effort, Node n)
77
{
78
106650
  Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
79
106650
  if (!d_extfInfoTmp[n].d_modelActive)
80
  {
81
    // n is not active in the model, no need to reduce
82
  Trace("strings-extf-debug") << "...skip due to model active" << std::endl;
83
    return false;
84
  }
85
106650
  if (d_reduced.find(n)!=d_reduced.end())
86
  {
87
    // already sent a reduction lemma
88
71729
  Trace("strings-extf-debug") << "...skip due to reduced" << std::endl;
89
71729
    return false;
90
  }
91
  // determine the effort level to process the extf at
92
  // 0 - at assertion time, 1+ - after no other reduction is applicable
93
34921
  int r_effort = -1;
94
  // polarity : 1 true, -1 false, 0 neither
95
34921
  int pol = 0;
96
34921
  Kind k = n.getKind();
97
34921
  if (n.getType().isBoolean() && !d_extfInfoTmp[n].d_const.isNull())
98
  {
99
14467
    pol = d_extfInfoTmp[n].d_const.getConst<bool>() ? 1 : -1;
100
  }
101
34921
  if (k == STRING_STRCTN)
102
  {
103
5871
    if (pol == 1)
104
    {
105
1754
      r_effort = 1;
106
    }
107
4117
    else if (pol == -1)
108
    {
109
3851
      if (effort == 2)
110
      {
111
188
        Node x = n[0];
112
188
        Node s = n[1];
113
188
        std::vector<Node> lexp;
114
188
        Node lenx = d_state.getLength(x, lexp);
115
188
        Node lens = d_state.getLength(s, lexp);
116
97
        if (d_state.areEqual(lenx, lens))
117
        {
118
12
          Trace("strings-extf-debug")
119
6
              << "  resolve extf : " << n
120
6
              << " based on equal lengths disequality." << std::endl;
121
          // We can reduce negative contains to a disequality when lengths are
122
          // equal. In other words, len( x ) = len( s ) implies
123
          //   ~contains( x, s ) reduces to x != s.
124
6
          if (!d_state.areDisequal(x, s))
125
          {
126
            // len( x ) = len( s ) ^ ~contains( x, s ) => x != s
127
2
            lexp.push_back(lenx.eqNode(lens));
128
2
            lexp.push_back(n.negate());
129
4
            Node xneqs = x.eqNode(s).negate();
130
2
            d_im.sendInference(
131
                lexp, xneqs, InferenceId::STRINGS_CTN_NEG_EQUAL, false, true);
132
          }
133
          // this depends on the current assertions, so this
134
          // inference is context-dependent
135
6
          d_extt.markReduced(n, true);
136
6
          return true;
137
        }
138
        else
139
        {
140
91
          r_effort = 2;
141
        }
142
      }
143
    }
144
  }
145
29050
  else if (k == STRING_SUBSTR)
146
  {
147
846
    r_effort = 1;
148
  }
149
28204
  else if (k == SEQ_UNIT)
150
  {
151
    // never necessary to reduce seq.unit
152
142
    return false;
153
  }
154
28062
  else if (k != STRING_IN_REGEXP)
155
  {
156
19094
    r_effort = 2;
157
  }
158
34773
  if (effort != r_effort)
159
  {
160
161
31296
  Trace("strings-extf-debug") << "...skip due to effort" << std::endl;
162
    // not the right effort level to reduce
163
31296
    return false;
164
  }
165
6954
  Node c_n = pol == -1 ? n.negate() : n;
166
6954
  Trace("strings-process-debug")
167
3477
      << "Process reduction for " << n << ", pol = " << pol << std::endl;
168
3477
  if (k == STRING_STRCTN && pol == 1)
169
  {
170
3508
    Node x = n[0];
171
3508
    Node s = n[1];
172
    // positive contains reduces to a equality
173
1754
    SkolemCache* skc = d_termReg.getSkolemCache();
174
3508
    Node eq = d_termReg.eagerReduce(n, skc);
175
1754
    Assert(!eq.isNull());
176
1754
    Assert(eq.getKind() == ITE && eq[0] == n);
177
1754
    eq = eq[1];
178
3508
    std::vector<Node> expn;
179
1754
    expn.push_back(n);
180
1754
    d_im.sendInference(expn, expn, eq, InferenceId::STRINGS_CTN_POS, false, true);
181
3508
    Trace("strings-extf-debug")
182
1754
        << "  resolve extf : " << n << " based on positive contain reduction."
183
1754
        << std::endl;
184
3508
    Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
185
1754
                               << " => " << eq << std::endl;
186
    // context-dependent because it depends on the polarity of n itself
187
3508
    d_extt.markReduced(n, true);
188
  }
189
1723
  else if (k != kind::STRING_TO_CODE)
190
  {
191
1281
    NodeManager* nm = NodeManager::currentNM();
192
1281
    Assert(k == STRING_SUBSTR || k == STRING_UPDATE || k == STRING_STRCTN
193
           || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI
194
           || k == STRING_STRREPL || k == STRING_STRREPLALL || k == SEQ_NTH
195
           || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL
196
           || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER
197
           || k == STRING_REV);
198
2562
    std::vector<Node> new_nodes;
199
2562
    Node res = d_preproc.simplify(n, new_nodes);
200
1281
    Assert(res != n);
201
1281
    new_nodes.push_back(n.eqNode(res));
202
    Node nnlem =
203
2562
        new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(AND, new_nodes);
204
2562
    Trace("strings-red-lemma")
205
1281
        << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
206
1281
    Trace("strings-red-lemma") << "...from " << n << std::endl;
207
2562
    Trace("strings-red-lemma")
208
1281
        << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl;
209
1281
    d_im.sendInference(d_emptyVec, nnlem, InferenceId::STRINGS_REDUCTION, false, true);
210
2562
    Trace("strings-extf-debug")
211
1281
        << "  resolve extf : " << n << " based on reduction." << std::endl;
212
    // add as reduction lemma
213
1281
    d_reduced.insert(n);
214
  }
215
3477
  return true;
216
}
217
218
19487
void ExtfSolver::checkExtfReductions(int effort)
219
{
220
  // Notice we don't make a standard call to ExtTheory::doReductions here,
221
  // since certain optimizations like context-dependent reductions and
222
  // stratifying effort levels are done in doReduction below.
223
35937
  std::vector<Node> extf = d_extt.getActive();
224
38974
  Trace("strings-process") << "  checking " << extf.size() << " active extf"
225
19487
                           << std::endl;
226
123100
  for (const Node& n : extf)
227
  {
228
106650
    Assert(!d_state.isInConflict());
229
213300
    Trace("strings-process")
230
106650
        << "  check " << n
231
106650
        << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl;
232
106650
    bool ret = doReduction(effort, n);
233
106650
    if (ret)
234
    {
235
      // we do not mark as reduced, since we may want to evaluate
236
3483
      if (d_im.hasProcessed())
237
      {
238
6074
        return;
239
      }
240
    }
241
  }
242
}
243
244
31493
void ExtfSolver::checkExtfEval(int effort)
245
{
246
62986
  Trace("strings-extf-list")
247
31493
      << "Active extended functions, effort=" << effort << " : " << std::endl;
248
31493
  d_extfInfoTmp.clear();
249
31493
  NodeManager* nm = NodeManager::currentNM();
250
31493
  bool has_nreduce = false;
251
62738
  std::vector<Node> terms = d_extt.getActive();
252
  // the set of terms we have done extf inferences for
253
62738
  std::unordered_set<Node, NodeHashFunction> inferProcessed;
254
271397
  for (const Node& n : terms)
255
  {
256
    // Setup information about n, including if it is equal to a constant.
257
240152
    ExtfInfoTmp& einfo = d_extfInfoTmp[n];
258
480056
    Node r = d_state.getRepresentative(n);
259
240152
    einfo.d_const = d_bsolver.getConstantEqc(r);
260
    // Get the current values of the children of n.
261
    // Notice that we look up the value of the direct children of n, and not
262
    // their free variables. In other words, given a term:
263
    //   t = (str.replace "B" (str.replace x "A" "B") "C")
264
    // we may build the explanation that:
265
    //   ((str.replace x "A" "B") = "B") => t = (str.replace "B" "B" "C")
266
    // instead of basing this on the free variable x:
267
    //   (x = "A") => t = (str.replace "B" (str.replace "A" "A" "B") "C")
268
    // Although both allow us to infer t = "C", it is important to use the
269
    // first kind of inference since it ensures that its subterms have the
270
    // expected values. Otherwise, we may in rare cases fail to realize that
271
    // the subterm (str.replace x "A" "B") does not currently have the correct
272
    // value, say in this example that (str.replace x "A" "B") != "B".
273
480056
    std::vector<Node> exp;
274
480056
    std::vector<Node> schildren;
275
240152
    bool schanged = false;
276
792307
    for (const Node& nc : n)
277
    {
278
1104310
      Node sc = getCurrentSubstitutionFor(effort, nc, exp);
279
552155
      schildren.push_back(sc);
280
552155
      schanged = schanged || sc != nc;
281
    }
282
    // If there is information involving the children, attempt to do an
283
    // inference and/or mark n as reduced.
284
240152
    bool reduced = false;
285
480056
    Node to_reduce = n;
286
240152
    if (schanged)
287
    {
288
236052
      Node sn = nm->mkNode(n.getKind(), schildren);
289
236052
      Trace("strings-extf-debug")
290
118026
          << "Check extf " << n << " == " << sn
291
118026
          << ", constant = " << einfo.d_const << ", effort=" << effort << "..."
292
118026
          << std::endl;
293
118026
      einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
294
      // inference is rewriting the substituted node
295
236052
      Node nrc = Rewriter::rewrite(sn);
296
      // if rewrites to a constant, then do the inference and mark as reduced
297
118026
      if (nrc.isConst())
298
      {
299
69057
        if (effort < 3)
300
        {
301
69057
          d_extt.markReduced(n);
302
138114
          Trace("strings-extf-debug")
303
69057
              << "  resolvable by evaluation..." << std::endl;
304
138114
          std::vector<Node> exps;
305
          // The following optimization gets the "symbolic definition" of
306
          // an extended term. The symbolic definition of a term t is a term
307
          // t' where constants are replaced by their corresponding proxy
308
          // variables.
309
          // For example, if lsym is a proxy variable for "", then
310
          // str.replace( lsym, lsym, lsym ) is the symbolic definition for
311
          // str.replace( "", "", "" ). It is generally better to use symbolic
312
          // definitions when doing cd-rewriting for the purpose of minimizing
313
          // clauses, e.g. we infer the unit equality:
314
          //    str.replace( lsym, lsym, lsym ) == ""
315
          // instead of making this inference multiple times:
316
          //    x = "" => str.replace( x, x, x ) == ""
317
          //    y = "" => str.replace( y, y, y ) == ""
318
138114
          Trace("strings-extf-debug")
319
69057
              << "  get symbolic definition..." << std::endl;
320
138114
          Node nrs;
321
          // only use symbolic definitions if option is set
322
152133
          if (options::stringInferSym())
323
          {
324
69057
            nrs = d_termReg.getSymbolicDefinition(sn, exps);
325
          }
326
69057
          if (!nrs.isNull())
327
          {
328
113192
            Trace("strings-extf-debug")
329
56596
                << "  rewrite " << nrs << "..." << std::endl;
330
113192
            Node nrsr = Rewriter::rewrite(nrs);
331
            // ensure the symbolic form is not rewritable
332
56596
            if (nrsr != nrs)
333
            {
334
              // we cannot use the symbolic definition if it rewrites
335
2652
              Trace("strings-extf-debug")
336
1326
                  << "  symbolic definition is trivial..." << std::endl;
337
1326
              nrs = Node::null();
338
            }
339
          }
340
          else
341
          {
342
24922
            Trace("strings-extf-debug")
343
12461
                << "  could not infer symbolic definition." << std::endl;
344
          }
345
138114
          Node conc;
346
69057
          if (!nrs.isNull())
347
          {
348
110540
            Trace("strings-extf-debug")
349
55270
                << "  symbolic def : " << nrs << std::endl;
350
55270
            if (!d_state.areEqual(nrs, nrc))
351
            {
352
              // infer symbolic unit
353
1137
              if (n.getType().isBoolean())
354
              {
355
916
                conc = nrc == d_true ? nrs : nrs.negate();
356
              }
357
              else
358
              {
359
221
                conc = nrs.eqNode(nrc);
360
              }
361
1137
              einfo.d_exp.clear();
362
            }
363
          }
364
          else
365
          {
366
13787
            if (!d_state.areEqual(n, nrc))
367
            {
368
576
              if (n.getType().isBoolean())
369
              {
370
287
                if (d_state.areEqual(n, nrc == d_true ? d_false : d_true))
371
                {
372
244
                  einfo.d_exp.push_back(nrc == d_true ? n.negate() : n);
373
244
                  conc = d_false;
374
                }
375
                else
376
                {
377
43
                  conc = nrc == d_true ? n : n.negate();
378
                }
379
              }
380
              else
381
              {
382
289
                conc = n.eqNode(nrc);
383
              }
384
            }
385
          }
386
69057
          if (!conc.isNull())
387
          {
388
3426
            Trace("strings-extf")
389
1713
                << "  resolve extf : " << sn << " -> " << nrc << std::endl;
390
1713
            InferenceId inf = effort == 0 ? InferenceId::STRINGS_EXTF : InferenceId::STRINGS_EXTF_N;
391
1713
            d_im.sendInference(einfo.d_exp, conc, inf, false, true);
392
1713
            d_statistics.d_cdSimplifications << n.getKind();
393
          }
394
        }
395
        else
396
        {
397
          // check if it is already equal, if so, mark as reduced. Otherwise, do
398
          // nothing.
399
          if (d_state.areEqual(n, nrc))
400
          {
401
            Trace("strings-extf")
402
                << "  resolved extf, since satisfied by model: " << n
403
                << std::endl;
404
            einfo.d_modelActive = false;
405
          }
406
        }
407
69057
        reduced = true;
408
      }
409
      else
410
      {
411
        // if this was a predicate which changed after substitution + rewriting
412
48969
        if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n)
413
        {
414
11170
          bool pol = einfo.d_const == d_true;
415
22340
          Node nrcAssert = pol ? nrc : nrc.negate();
416
22340
          Node nAssert = pol ? n : n.negate();
417
11170
          Assert(effort < 3);
418
11170
          einfo.d_exp.push_back(nAssert);
419
11170
          Trace("strings-extf-debug") << "  decomposable..." << std::endl;
420
22340
          Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc
421
11170
                                << ", const = " << einfo.d_const << std::endl;
422
          // We send inferences internal here, which may help show unsat.
423
          // However, we do not make a determination whether n can be marked
424
          // reduced since this argument may be circular: we may infer than n
425
          // can be reduced to something else, but that thing may argue that it
426
          // can be reduced to n, in theory.
427
11170
          InferenceId infer =
428
11170
              effort == 0 ? InferenceId::STRINGS_EXTF_D : InferenceId::STRINGS_EXTF_D_N;
429
11170
          d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
430
        }
431
48969
        to_reduce = nrc;
432
      }
433
    }
434
    // We must use the original n here to avoid circular justifications for
435
    // why extended functions are reduced. In particular, n should never be a
436
    // duplicate of another term considered in the block of code for
437
    // checkExtfInference below.
438
    // if not reduced and not processed
439
651399
    if (!reduced && !n.isNull()
440
411247
        && inferProcessed.find(n) == inferProcessed.end())
441
    {
442
171095
      inferProcessed.insert(n);
443
171095
      Assert(effort < 3);
444
171095
      if (effort == 1)
445
      {
446
35476
        Trace("strings-extf")
447
17738
            << "  cannot rewrite extf : " << to_reduce << std::endl;
448
      }
449
      // we take to_reduce to be the (partially) reduced version of n, which
450
      // is justified by the explanation in einfo.
451
171095
      checkExtfInference(n, to_reduce, einfo, effort);
452
171095
      if (Trace.isOn("strings-extf-list"))
453
      {
454
        Trace("strings-extf-list") << "  * " << to_reduce;
455
        if (!einfo.d_const.isNull())
456
        {
457
          Trace("strings-extf-list") << ", const = " << einfo.d_const;
458
        }
459
        if (n != to_reduce)
460
        {
461
          Trace("strings-extf-list") << ", from " << n;
462
        }
463
        Trace("strings-extf-list") << std::endl;
464
      }
465
171095
      if (d_extt.isActive(n) && einfo.d_modelActive)
466
      {
467
171095
        has_nreduce = true;
468
      }
469
    }
470
240152
    if (d_state.isInConflict())
471
    {
472
248
      Trace("strings-extf-debug") << "  conflict, return." << std::endl;
473
248
      return;
474
    }
475
  }
476
31245
  d_hasExtf = has_nreduce;
477
}
478
479
171095
void ExtfSolver::checkExtfInference(Node n,
480
                                    Node nr,
481
                                    ExtfInfoTmp& in,
482
                                    int effort)
483
{
484
171095
  if (in.d_const.isNull())
485
  {
486
206114
    return;
487
  }
488
78218
  NodeManager* nm = NodeManager::currentNM();
489
156436
  Trace("strings-extf-infer") << "checkExtfInference: " << n << " : " << nr
490
78218
                              << " == " << in.d_const << std::endl;
491
492
  // add original to explanation
493
78218
  if (n.getType().isBoolean())
494
  {
495
    // if Boolean, it's easy
496
39203
    in.d_exp.push_back(in.d_const.getConst<bool>() ? n : n.negate());
497
  }
498
  else
499
  {
500
    // otherwise, must explain via base node
501
78030
    Node r = d_state.getRepresentative(n);
502
    // explain using the base solver
503
39015
    d_bsolver.explainConstantEqc(n, r, in.d_exp);
504
  }
505
506
  // d_extfInferCache stores whether we have made the inferences associated
507
  // with a node n,
508
  // this may need to be generalized if multiple inferences apply
509
510
78218
  if (nr.getKind() == STRING_STRCTN)
511
  {
512
20360
    Assert(in.d_const.isConst());
513
20360
    bool pol = in.d_const.getConst<bool>();
514
25219
    if ((pol && nr[1].getKind() == STRING_CONCAT)
515
40650
        || (!pol && nr[0].getKind() == STRING_CONCAT))
516
    {
517
      // If str.contains( x, str.++( y1, ..., yn ) ),
518
      //   we may infer str.contains( x, y1 ), ..., str.contains( x, yn )
519
      // The following recognizes two situations related to the above reasoning:
520
      // (1) If ~str.contains( x, yi ) holds for some i, we are in conflict,
521
      // (2) If str.contains( x, yj ) already holds for some j, then the term
522
      // str.contains( x, yj ) is irrelevant since it is satisfied by all models
523
      // for str.contains( x, str.++( y1, ..., yn ) ).
524
525
      // Notice that the dual of the above reasoning also holds, i.e.
526
      // If ~str.contains( str.++( x1, ..., xn ), y ),
527
      //   we may infer ~str.contains( x1, y ), ..., ~str.contains( xn, y )
528
      // This is also handled here.
529
1011
      if (d_extfInferCache.find(nr) == d_extfInferCache.end())
530
      {
531
391
        d_extfInferCache.insert(nr);
532
533
391
        int index = pol ? 1 : 0;
534
782
        std::vector<Node> children;
535
391
        children.push_back(nr[0]);
536
391
        children.push_back(nr[1]);
537
1505
        for (const Node& nrc : nr[index])
538
        {
539
1114
          children[index] = nrc;
540
2228
          Node conc = nm->mkNode(STRING_STRCTN, children);
541
1114
          conc = Rewriter::rewrite(pol ? conc : conc.negate());
542
          // check if it already (does not) hold
543
1114
          if (d_state.hasTerm(conc))
544
          {
545
46
            if (d_state.areEqual(conc, d_false))
546
            {
547
              // we are in conflict
548
              d_im.sendInference(in.d_exp, conc, InferenceId::STRINGS_CTN_DECOMPOSE);
549
            }
550
46
            else if (d_extt.hasFunctionKind(conc.getKind()))
551
            {
552
              // can mark as reduced, since model for n implies model for conc
553
              d_extt.markReduced(conc);
554
            }
555
          }
556
        }
557
      }
558
    }
559
    else
560
    {
561
77396
      if (std::find(d_extfInfoTmp[nr[0]].d_ctn[pol].begin(),
562
38698
                    d_extfInfoTmp[nr[0]].d_ctn[pol].end(),
563
77396
                    nr[1])
564
58047
          == d_extfInfoTmp[nr[0]].d_ctn[pol].end())
565
      {
566
38694
        Trace("strings-extf-debug") << "  store contains info : " << nr[0]
567
19347
                                    << " " << pol << " " << nr[1] << std::endl;
568
        // Store s (does not) contains t, since nr = (~)contains( s, t ) holds.
569
19347
        d_extfInfoTmp[nr[0]].d_ctn[pol].push_back(nr[1]);
570
19347
        d_extfInfoTmp[nr[0]].d_ctnFrom[pol].push_back(n);
571
        // Do transistive closure on contains, e.g.
572
        // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ).
573
574
        // The following infers new (negative) contains based on the above
575
        // reasoning, provided that ~contains( t, r ) does not
576
        // already hold in the current context. We test this by checking that
577
        // contains( t, r ) is not already asserted false in the current
578
        // context. We also handle the case where contains( t, r ) is equivalent
579
        // to t = r, in which case we check that t != r does not already hold
580
        // in the current context.
581
582
        // Notice that form of the above inference is enough to find
583
        // conflicts purely due to contains predicates. For example, if we
584
        // have only positive occurrences of contains, then no conflicts due to
585
        // contains predicates are possible and this schema does nothing. For
586
        // example, note that contains( s, t ) and contains( t, r ) implies
587
        // contains( s, r ), which we could but choose not to infer. Instead,
588
        // we prefer being lazy: only if ~contains( s, r ) appears later do we
589
        // infer ~contains( t, r ), which suffices to show a conflict.
590
19347
        bool opol = !pol;
591
22789
        for (unsigned i = 0, size = d_extfInfoTmp[nr[0]].d_ctn[opol].size();
592
22789
             i < size;
593
             i++)
594
        {
595
6884
          Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
596
          Node concOrig =
597
6884
              nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]);
598
6884
          Node conc = Rewriter::rewrite(concOrig);
599
          // For termination concerns, we only do the inference if the contains
600
          // does not rewrite (and thus does not introduce new terms).
601
3442
          if (conc == concOrig)
602
          {
603
16
            bool do_infer = false;
604
16
            conc = conc.negate();
605
16
            bool pol2 = conc.getKind() != NOT;
606
32
            Node lit = pol2 ? conc : conc[0];
607
16
            if (lit.getKind() == EQUAL)
608
            {
609
              do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1])
610
                              : !d_state.areDisequal(lit[0], lit[1]);
611
            }
612
            else
613
            {
614
16
              do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false);
615
            }
616
16
            if (do_infer)
617
            {
618
16
              std::vector<Node> exp_c;
619
8
              exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
620
16
              Node ofrom = d_extfInfoTmp[nr[0]].d_ctnFrom[opol][i];
621
8
              Assert(d_extfInfoTmp.find(ofrom) != d_extfInfoTmp.end());
622
24
              exp_c.insert(exp_c.end(),
623
8
                           d_extfInfoTmp[ofrom].d_exp.begin(),
624
32
                           d_extfInfoTmp[ofrom].d_exp.end());
625
8
              d_im.sendInference(exp_c, conc, InferenceId::STRINGS_CTN_TRANS);
626
            }
627
          }
628
        }
629
      }
630
      else
631
      {
632
        // If we already know that s (does not) contain t, then n may be
633
        // redundant. However, we do not mark n as reduced here, since strings
634
        // reductions may require dependencies between extended functions.
635
        // Marking reduced here could lead to incorrect models if an
636
        // extended function is marked reduced based on an assignment to
637
        // something that depends on n.
638
2
        Trace("strings-extf-debug") << "  redundant." << std::endl;
639
      }
640
    }
641
20360
    return;
642
  }
643
644
  // If it's not a predicate, see if we can solve the equality n = c, where c
645
  // is the constant that extended term n is equal to.
646
115716
  Node inferEq = nr.eqNode(in.d_const);
647
115716
  Node inferEqr = Rewriter::rewrite(inferEq);
648
115716
  Node inferEqrr = inferEqr;
649
57858
  if (inferEqr.getKind() == EQUAL)
650
  {
651
    // try to use the extended rewriter for equalities
652
39424
    inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr);
653
  }
654
57858
  if (inferEqrr != inferEqr)
655
  {
656
1584
    inferEqrr = Rewriter::rewrite(inferEqrr);
657
3168
    Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
658
1584
                                << " ...reduces to " << inferEqrr << std::endl;
659
1584
    d_im.sendInternalInference(in.d_exp, inferEqrr, InferenceId::STRINGS_EXTF_EQ_REW);
660
  }
661
}
662
663
552155
Node ExtfSolver::getCurrentSubstitutionFor(int effort,
664
                                           Node n,
665
                                           std::vector<Node>& exp)
666
{
667
552155
  if (effort >= 3)
668
  {
669
    // model values
670
    Node mv = d_state.getModel()->getRepresentative(n);
671
    Trace("strings-subs") << "   model val : " << mv << std::endl;
672
    return mv;
673
  }
674
1104310
  Node nr = d_state.getRepresentative(n);
675
1104310
  Node c = d_bsolver.explainBestContentEqc(n, nr, exp);
676
552155
  if (!c.isNull())
677
  {
678
316033
    return c;
679
  }
680
236122
  else if (effort >= 1 && n.getType().isStringLike())
681
  {
682
14825
    Assert(effort < 3);
683
    // normal forms
684
14825
    NormalForm& nfnr = d_csolver.getNormalForm(nr);
685
29650
    Node ns = d_csolver.getNormalString(nfnr.d_base, exp);
686
29650
    Trace("strings-subs") << "   normal eqc : " << ns << " " << nfnr.d_base
687
14825
                          << " " << nr << std::endl;
688
14825
    if (!nfnr.d_base.isNull())
689
    {
690
14825
      d_im.addToExplanation(n, nfnr.d_base, exp);
691
    }
692
14825
    return ns;
693
  }
694
221297
  return n;
695
}
696
697
7346
const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const
698
{
699
7346
  return d_extfInfoTmp;
700
}
701
bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
702
703
7346
std::vector<Node> ExtfSolver::getActive(Kind k) const
704
{
705
7346
  return d_extt.getActive(k);
706
}
707
708
bool StringsExtfCallback::getCurrentSubstitution(
709
    int effort,
710
    const std::vector<Node>& vars,
711
    std::vector<Node>& subs,
712
    std::map<Node, std::vector<Node> >& exp)
713
{
714
  Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort
715
                        << std::endl;
716
  for (const Node& v : vars)
717
  {
718
    Trace("strings-subs") << "  get subs for " << v << "..." << std::endl;
719
    Node s = d_esolver->getCurrentSubstitutionFor(effort, v, exp[v]);
720
    subs.push_back(s);
721
  }
722
  return true;
723
}
724
725
}  // namespace strings
726
}  // namespace theory
727
109761
}  // namespace CVC4