GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/extf_solver.cpp Lines: 301 358 84.1 %
Date: 2021-09-29 Branches: 781 1758 44.4 %

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