GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/proof_checker.cpp Lines: 238 296 80.4 %
Date: 2021-03-23 Branches: 573 1846 31.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 strings proof checker
13
 **/
14
15
#include "theory/strings/proof_checker.h"
16
17
#include "expr/sequence.h"
18
#include "options/strings_options.h"
19
#include "theory/rewriter.h"
20
#include "theory/strings/core_solver.h"
21
#include "theory/strings/regexp_elim.h"
22
#include "theory/strings/regexp_operation.h"
23
#include "theory/strings/term_registry.h"
24
#include "theory/strings/theory_strings_preprocess.h"
25
#include "theory/strings/theory_strings_utils.h"
26
#include "theory/strings/word.h"
27
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace strings {
33
34
962
void StringProofRuleChecker::registerTo(ProofChecker* pc)
35
{
36
962
  pc->registerChecker(PfRule::CONCAT_EQ, this);
37
962
  pc->registerChecker(PfRule::CONCAT_UNIFY, this);
38
962
  pc->registerChecker(PfRule::CONCAT_CONFLICT, this);
39
962
  pc->registerChecker(PfRule::CONCAT_SPLIT, this);
40
962
  pc->registerChecker(PfRule::CONCAT_CSPLIT, this);
41
962
  pc->registerChecker(PfRule::CONCAT_LPROP, this);
42
962
  pc->registerChecker(PfRule::CONCAT_CPROP, this);
43
962
  pc->registerChecker(PfRule::STRING_DECOMPOSE, this);
44
962
  pc->registerChecker(PfRule::STRING_LENGTH_POS, this);
45
962
  pc->registerChecker(PfRule::STRING_LENGTH_NON_EMPTY, this);
46
962
  pc->registerChecker(PfRule::STRING_REDUCTION, this);
47
962
  pc->registerChecker(PfRule::STRING_EAGER_REDUCTION, this);
48
962
  pc->registerChecker(PfRule::RE_INTER, this);
49
962
  pc->registerChecker(PfRule::RE_UNFOLD_POS, this);
50
962
  pc->registerChecker(PfRule::RE_UNFOLD_NEG, this);
51
962
  pc->registerChecker(PfRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
52
962
  pc->registerChecker(PfRule::RE_ELIM, this);
53
962
  pc->registerChecker(PfRule::STRING_CODE_INJ, this);
54
962
  pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
55
  // trusted rules
56
962
  pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2);
57
962
}
58
59
2494
Node StringProofRuleChecker::checkInternal(PfRule id,
60
                                           const std::vector<Node>& children,
61
                                           const std::vector<Node>& args)
62
{
63
2494
  NodeManager* nm = NodeManager::currentNM();
64
  // core rules for word equations
65
2494
  if (id == PfRule::CONCAT_EQ || id == PfRule::CONCAT_UNIFY
66
1633
      || id == PfRule::CONCAT_CONFLICT || id == PfRule::CONCAT_SPLIT
67
1630
      || id == PfRule::CONCAT_CSPLIT || id == PfRule::CONCAT_LPROP
68
1456
      || id == PfRule::CONCAT_CPROP)
69
  {
70
1038
    Trace("strings-pfcheck") << "Checking id " << id << std::endl;
71
1038
    Assert(children.size() >= 1);
72
1038
    Assert(args.size() == 1);
73
    // all rules have an equality
74
1038
    if (children[0].getKind() != EQUAL)
75
    {
76
      return Node::null();
77
    }
78
    // convert to concatenation form
79
2076
    std::vector<Node> tvec;
80
2076
    std::vector<Node> svec;
81
1038
    utils::getConcat(children[0][0], tvec);
82
1038
    utils::getConcat(children[0][1], svec);
83
1038
    size_t nchildt = tvec.size();
84
1038
    size_t nchilds = svec.size();
85
2076
    TypeNode stringType = children[0][0].getType();
86
    // extract the Boolean corresponding to whether the rule is reversed
87
    bool isRev;
88
1038
    if (!getBool(args[0], isRev))
89
    {
90
      return Node::null();
91
    }
92
1038
    if (id == PfRule::CONCAT_EQ)
93
    {
94
605
      Assert(children.size() == 1);
95
605
      size_t index = 0;
96
1210
      std::vector<Node> tremVec;
97
1210
      std::vector<Node> sremVec;
98
      // scan the concatenation until we exhaust child proofs
99
1211
      while (index < nchilds && index < nchildt)
100
      {
101
1211
        Node currT = tvec[isRev ? (nchildt - 1 - index) : index];
102
1211
        Node currS = svec[isRev ? (nchilds - 1 - index) : index];
103
908
        if (currT != currS)
104
        {
105
605
          if (currT.isConst() && currS.isConst())
106
          {
107
            size_t sindex;
108
            // get the equal prefix/suffix, strip and add the remainders
109
550
            Node currR = Word::splitConstant(currT, currS, sindex, isRev);
110
275
            if (!currR.isNull())
111
            {
112
              // add the constant to remainder vec
113
275
              std::vector<Node>& rem = sindex == 0 ? tremVec : sremVec;
114
275
              rem.push_back(currR);
115
              // ignore the current component
116
275
              index++;
117
              // In other words, if we have (currS,currT) = ("ab","abc"), then
118
              // we proceed to the next component and add currR = "c" to
119
              // tremVec.
120
            }
121
            // otherwise if we are not the same prefix, then both will be added
122
            // Notice that we do not add maximal prefixes, in other words,
123
            // ("abc", "abd") may be added to the remainder vectors, and not
124
            // ("c", "d").
125
          }
126
605
          break;
127
        }
128
303
        index++;
129
      }
130
605
      Assert(index <= nchildt);
131
605
      Assert(index <= nchilds);
132
      // the remainders are equal
133
1815
      tremVec.insert(isRev ? tremVec.begin() : tremVec.end(),
134
1210
                     tvec.begin() + (isRev ? 0 : index),
135
3025
                     tvec.begin() + nchildt - (isRev ? index : 0));
136
1815
      sremVec.insert(isRev ? sremVec.begin() : sremVec.end(),
137
1210
                     svec.begin() + (isRev ? 0 : index),
138
3025
                     svec.begin() + nchilds - (isRev ? index : 0));
139
      // convert back to node
140
1210
      Node trem = utils::mkConcat(tremVec, stringType);
141
1210
      Node srem = utils::mkConcat(sremVec, stringType);
142
605
      return trem.eqNode(srem);
143
    }
144
    // all remaining rules do something with the first child of each side
145
866
    Node t0 = tvec[isRev ? nchildt - 1 : 0];
146
866
    Node s0 = svec[isRev ? nchilds - 1 : 0];
147
433
    if (id == PfRule::CONCAT_UNIFY)
148
    {
149
256
      Assert(children.size() == 2);
150
256
      if (children[1].getKind() != EQUAL)
151
      {
152
        return Node::null();
153
      }
154
766
      for (size_t i = 0; i < 2; i++)
155
      {
156
530
        Node l = children[1][i];
157
512
        if (l.getKind() != STRING_LENGTH)
158
        {
159
          return Node::null();
160
        }
161
530
        Node term = i == 0 ? t0 : s0;
162
512
        if (l[0] == term)
163
        {
164
492
          continue;
165
        }
166
        // could be a spliced constant
167
20
        bool success = false;
168
20
        if (term.isConst() && l[0].isConst())
169
        {
170
18
          size_t lenL = Word::getLength(l[0]);
171
36
          success = (isRev && l[0] == Word::suffix(term, lenL))
172
54
                    || (!isRev && l[0] == Word::prefix(term, lenL));
173
        }
174
20
        if (!success)
175
        {
176
2
          return Node::null();
177
        }
178
      }
179
254
      return children[1][0][0].eqNode(children[1][1][0]);
180
    }
181
177
    else if (id == PfRule::CONCAT_CONFLICT)
182
    {
183
      Assert(children.size() == 1);
184
      if (!t0.isConst() || !s0.isConst())
185
      {
186
        // not constants
187
        return Node::null();
188
      }
189
      size_t sindex;
190
      Node r0 = Word::splitConstant(t0, s0, sindex, isRev);
191
      if (!r0.isNull())
192
      {
193
        // Not a conflict due to constants, i.e. s0 is a prefix of t0 or vice
194
        // versa.
195
        return Node::null();
196
      }
197
      return nm->mkConst(false);
198
    }
199
177
    else if (id == PfRule::CONCAT_SPLIT)
200
    {
201
3
      Assert(children.size() == 2);
202
9
      if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
203
6
          || children[1][0][0].getKind() != STRING_LENGTH
204
6
          || children[1][0][0][0] != t0
205
6
          || children[1][0][1].getKind() != STRING_LENGTH
206
9
          || children[1][0][1][0] != s0)
207
      {
208
        return Node::null();
209
      }
210
    }
211
174
    else if (id == PfRule::CONCAT_CSPLIT)
212
    {
213
157
      Assert(children.size() == 2);
214
314
      Node zero = nm->mkConst(Rational(0));
215
314
      Node one = nm->mkConst(Rational(1));
216
471
      if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
217
314
          || children[1][0][0].getKind() != STRING_LENGTH
218
471
          || children[1][0][0][0] != t0 || children[1][0][1] != zero)
219
      {
220
        return Node::null();
221
      }
222
157
      if (!s0.isConst() || !s0.getType().isStringLike() || Word::isEmpty(s0))
223
      {
224
        return Node::null();
225
      }
226
    }
227
17
    else if (id == PfRule::CONCAT_LPROP)
228
    {
229
17
      Assert(children.size() == 2);
230
34
      if (children[1].getKind() != GT
231
34
          || children[1][0].getKind() != STRING_LENGTH
232
34
          || children[1][0][0] != t0
233
34
          || children[1][1].getKind() != STRING_LENGTH
234
51
          || children[1][1][0] != s0)
235
      {
236
        return Node::null();
237
      }
238
    }
239
    else if (id == PfRule::CONCAT_CPROP)
240
    {
241
      Assert(children.size() == 2);
242
      Node zero = nm->mkConst(Rational(0));
243
244
      Trace("pfcheck-strings-cprop")
245
          << "CONCAT_PROP, isRev=" << isRev << std::endl;
246
      if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
247
          || children[1][0][0].getKind() != STRING_LENGTH
248
          || children[1][0][0][0] != t0 || children[1][0][1] != zero)
249
      {
250
        Trace("pfcheck-strings-cprop")
251
            << "...failed pattern match" << std::endl;
252
        return Node::null();
253
      }
254
      if (tvec.size() <= 1)
255
      {
256
        Trace("pfcheck-strings-cprop")
257
            << "...failed adjacent constant" << std::endl;
258
        return Node::null();
259
      }
260
      Node w1 = tvec[isRev ? nchildt - 2 : 1];
261
      if (!w1.isConst() || !w1.getType().isStringLike() || Word::isEmpty(w1))
262
      {
263
        Trace("pfcheck-strings-cprop")
264
            << "...failed adjacent constant content" << std::endl;
265
        return Node::null();
266
      }
267
      Node w2 = s0;
268
      if (!w2.isConst() || !w2.getType().isStringLike() || Word::isEmpty(w2))
269
      {
270
        Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl;
271
        return Node::null();
272
      }
273
      // getConclusion expects the adjacent constant to be included
274
      t0 = nm->mkNode(STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1);
275
    }
276
    // use skolem cache
277
354
    SkolemCache skc(false);
278
354
    std::vector<Node> newSkolems;
279
354
    Node conc = CoreSolver::getConclusion(t0, s0, id, isRev, &skc, newSkolems);
280
177
    return conc;
281
  }
282
1456
  else if (id == PfRule::STRING_DECOMPOSE)
283
  {
284
1
    Assert(children.size() == 1);
285
1
    Assert(args.size() == 1);
286
    bool isRev;
287
1
    if (!getBool(args[0], isRev))
288
    {
289
      return Node::null();
290
    }
291
2
    Node atom = children[0];
292
1
    if (atom.getKind() != GEQ || atom[0].getKind() != STRING_LENGTH)
293
    {
294
      return Node::null();
295
    }
296
2
    SkolemCache sc(false);
297
2
    std::vector<Node> newSkolems;
298
    Node conc = CoreSolver::getConclusion(
299
2
        atom[0][0], atom[1], id, isRev, &sc, newSkolems);
300
1
    return conc;
301
  }
302
1455
  else if (id == PfRule::STRING_REDUCTION
303
1204
           || id == PfRule::STRING_EAGER_REDUCTION
304
952
           || id == PfRule::STRING_LENGTH_POS)
305
  {
306
1102
    Assert(children.empty());
307
1102
    Assert(args.size() >= 1);
308
    // These rules are based on calling a C++ method for returning a valid
309
    // lemma involving a single argument term.
310
    // Must convert to skolem form.
311
2204
    Node t = args[0];
312
2204
    Node ret;
313
1102
    if (id == PfRule::STRING_REDUCTION)
314
    {
315
251
      Assert(args.size() == 1);
316
      // we do not use optimizations
317
502
      SkolemCache skc(false);
318
502
      std::vector<Node> conj;
319
251
      ret = StringsPreprocess::reduce(t, conj, &skc);
320
251
      conj.push_back(t.eqNode(ret));
321
251
      ret = nm->mkAnd(conj);
322
    }
323
851
    else if (id == PfRule::STRING_EAGER_REDUCTION)
324
    {
325
252
      Assert(args.size() == 1);
326
504
      SkolemCache skc(false);
327
252
      ret = TermRegistry::eagerReduce(t, &skc);
328
    }
329
599
    else if (id == PfRule::STRING_LENGTH_POS)
330
    {
331
599
      Assert(args.size() == 1);
332
599
      ret = TermRegistry::lengthPositive(t);
333
    }
334
1102
    if (ret.isNull())
335
    {
336
      return Node::null();
337
    }
338
1102
    return ret;
339
  }
340
353
  else if (id == PfRule::STRING_LENGTH_NON_EMPTY)
341
  {
342
82
    Assert(children.size() == 1);
343
82
    Assert(args.empty());
344
164
    Node nemp = children[0];
345
246
    if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL
346
242
        || !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike())
347
    {
348
10
      return Node::null();
349
    }
350
72
    if (!Word::isEmpty(nemp[0][1]))
351
    {
352
      return Node::null();
353
    }
354
144
    Node zero = nm->mkConst(Rational(0));
355
144
    Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]);
356
72
    return clen.eqNode(zero).notNode();
357
  }
358
271
  else if (id == PfRule::RE_INTER)
359
  {
360
11
    Assert(children.size() >= 1);
361
11
    Assert(args.empty());
362
22
    std::vector<Node> reis;
363
22
    Node x;
364
    // make the regular expression intersection that summarizes all
365
    // memberships in the explanation
366
31
    for (const Node& c : children)
367
    {
368
22
      bool polarity = c.getKind() != NOT;
369
42
      Node catom = polarity ? c : c[0];
370
22
      if (catom.getKind() != STRING_IN_REGEXP)
371
      {
372
        return Node::null();
373
      }
374
22
      if (x.isNull())
375
      {
376
11
        x = catom[0];
377
      }
378
11
      else if (x != catom[0])
379
      {
380
        // different LHS
381
2
        return Node::null();
382
      }
383
40
      Node xcurr = catom[0];
384
      Node rcurr =
385
40
          polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]);
386
20
      reis.push_back(rcurr);
387
    }
388
18
    Node rei = reis.size() == 1 ? reis[0] : nm->mkNode(REGEXP_INTER, reis);
389
9
    return nm->mkNode(STRING_IN_REGEXP, x, rei);
390
  }
391
260
  else if (id == PfRule::RE_UNFOLD_POS || id == PfRule::RE_UNFOLD_NEG
392
190
           || id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
393
  {
394
76
    Assert(children.size() == 1);
395
76
    Assert(args.empty());
396
152
    Node skChild = children[0];
397
76
    if (id == PfRule::RE_UNFOLD_NEG || id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
398
    {
399
20
      if (skChild.getKind() != NOT || skChild[0].getKind() != STRING_IN_REGEXP)
400
      {
401
        Trace("strings-pfcheck") << "...fail, non-neg member" << std::endl;
402
        return Node::null();
403
      }
404
    }
405
66
    else if (skChild.getKind() != STRING_IN_REGEXP)
406
    {
407
      Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl;
408
      return Node::null();
409
    }
410
152
    Node conc;
411
76
    if (id == PfRule::RE_UNFOLD_POS)
412
    {
413
132
      std::vector<Node> newSkolems;
414
132
      SkolemCache sc;
415
66
      conc = RegExpOpr::reduceRegExpPos(skChild, &sc, newSkolems);
416
    }
417
10
    else if (id == PfRule::RE_UNFOLD_NEG)
418
    {
419
4
      conc = RegExpOpr::reduceRegExpNeg(skChild);
420
    }
421
6
    else if (id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
422
    {
423
6
      if (skChild[0][1].getKind() != REGEXP_CONCAT)
424
      {
425
        Trace("strings-pfcheck") << "...fail, no concat regexp" << std::endl;
426
        return Node::null();
427
      }
428
      size_t index;
429
12
      Node reLen = RegExpOpr::getRegExpConcatFixed(skChild[0][1], index);
430
6
      if (reLen.isNull())
431
      {
432
        Trace("strings-pfcheck") << "...fail, non-fixed lengths" << std::endl;
433
        return Node::null();
434
      }
435
6
      conc = RegExpOpr::reduceRegExpNegConcatFixed(skChild, reLen, index);
436
    }
437
76
    return conc;
438
  }
439
184
  else if (id == PfRule::RE_ELIM)
440
  {
441
2
    Assert(children.empty());
442
2
    Assert(args.size() == 2);
443
    bool isAgg;
444
2
    if (!getBool(args[1], isAgg))
445
    {
446
      return Node::null();
447
    }
448
4
    Node ea = RegExpElimination::eliminate(args[0], isAgg);
449
    // if we didn't eliminate, then this trivially proves the reflexive equality
450
2
    if (ea.isNull())
451
    {
452
      ea = args[0];
453
    }
454
2
    return args[0].eqNode(ea);
455
  }
456
182
  else if (id == PfRule::STRING_CODE_INJ)
457
  {
458
133
    Assert(children.empty());
459
133
    Assert(args.size() == 2);
460
133
    Assert(args[0].getType().isStringLike()
461
           && args[1].getType().isStringLike());
462
266
    Node c1 = nm->mkNode(STRING_TO_CODE, args[0]);
463
266
    Node c2 = nm->mkNode(STRING_TO_CODE, args[1]);
464
266
    Node eqNegOne = c1.eqNode(nm->mkConst(Rational(-1)));
465
266
    Node deq = c1.eqNode(c2).negate();
466
266
    Node eqn = args[0].eqNode(args[1]);
467
133
    return nm->mkNode(kind::OR, eqNegOne, deq, eqn);
468
  }
469
49
  else if (id == PfRule::STRING_SEQ_UNIT_INJ)
470
  {
471
16
    Assert(children.size() == 1);
472
16
    Assert(args.empty());
473
16
    if (children[0].getKind() != EQUAL)
474
    {
475
      return Node::null();
476
    }
477
32
    Node t[2];
478
48
    for (size_t i = 0; i < 2; i++)
479
    {
480
32
      if (children[0][i].getKind() == SEQ_UNIT)
481
      {
482
28
        t[i] = children[0][i][0];
483
      }
484
4
      else if (children[0][i].isConst())
485
      {
486
        // notice that Word::getChars is not the right call here, since it
487
        // gets a vector of sequences of length one. We actually need to
488
        // extract the character, which is a sequence-specific operation.
489
4
        const Sequence& sx = children[0][i].getConst<Sequence>();
490
4
        const std::vector<Node>& vec = sx.getVec();
491
4
        if (vec.size() == 1)
492
        {
493
          // the character of the single character sequence
494
4
          t[i] = vec[0];
495
        }
496
      }
497
32
      if (t[i].isNull())
498
      {
499
        return Node::null();
500
      }
501
    }
502
32
    Trace("strings-pfcheck-debug")
503
16
        << "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0]
504
16
        << " == " << t[1] << std::endl;
505
16
    AlwaysAssert(t[0].getType() == t[1].getType());
506
16
    return t[0].eqNode(t[1]);
507
  }
508
33
  else if (id == PfRule::STRING_TRUST)
509
  {
510
    // "trusted" rules
511
33
    Assert(!args.empty());
512
33
    Assert(args[0].getType().isBoolean());
513
33
    return args[0];
514
  }
515
  return Node::null();
516
}
517
518
}  // namespace strings
519
}  // namespace theory
520
26685
}  // namespace CVC4