GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/infer_proof_cons.cpp Lines: 449 536 83.8 %
Date: 2021-03-23 Branches: 888 2182 40.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_proof_cons.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 inference to proof conversion
13
 **/
14
15
#include "theory/strings/infer_proof_cons.h"
16
17
#include "expr/proof_node_manager.h"
18
#include "expr/skolem_manager.h"
19
#include "options/smt_options.h"
20
#include "options/strings_options.h"
21
#include "theory/builtin/proof_checker.h"
22
#include "theory/rewriter.h"
23
#include "theory/strings/regexp_operation.h"
24
#include "theory/strings/theory_strings_utils.h"
25
26
using namespace CVC4::kind;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace strings {
31
32
962
InferProofCons::InferProofCons(context::Context* c,
33
                               ProofNodeManager* pnm,
34
962
                               SequencesStatistics& statistics)
35
962
    : d_pnm(pnm), d_lazyFactMap(c), d_statistics(statistics)
36
{
37
962
  Assert(d_pnm != nullptr);
38
962
}
39
40
1598
void InferProofCons::notifyFact(const InferInfo& ii)
41
{
42
3174
  Node fact = ii.d_conc;
43
3196
  Trace("strings-ipc-debug")
44
1598
      << "InferProofCons::notifyFact: " << ii << std::endl;
45
1598
  if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
46
  {
47
22
    Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
48
22
    return;
49
  }
50
3152
  Node symFact = CDProof::getSymmFact(fact);
51
1576
  if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
52
  {
53
    Trace("strings-ipc-debug") << "...duplicate (sym)!" << std::endl;
54
    return;
55
  }
56
3152
  std::shared_ptr<InferInfo> iic = std::make_shared<InferInfo>(ii);
57
1576
  d_lazyFactMap.insert(ii.d_conc, iic);
58
}
59
60
1261
void InferProofCons::convert(InferenceId infer,
61
                             bool isRev,
62
                             Node conc,
63
                             const std::vector<Node>& exp,
64
                             ProofStep& ps,
65
                             TheoryProofStepBuffer& psb,
66
                             bool& useBuffer)
67
{
68
  // by default, don't use the buffer
69
1261
  useBuffer = false;
70
  // Must flatten children with respect to AND to be ready to explain.
71
  // We store the index where each flattened vector begins, since some
72
  // explanations are grouped together using AND.
73
2522
  std::vector<size_t> startExpIndex;
74
3712
  for (const Node& ec : exp)
75
  {
76
    // store the index in the flattened vector
77
2451
    startExpIndex.push_back(ps.d_children.size());
78
2451
    utils::flattenOp(AND, ec, ps.d_children);
79
  }
80
  // debug print
81
1261
  if (Trace.isOn("strings-ipc-debug"))
82
  {
83
    Trace("strings-ipc-debug") << "InferProofCons::convert: " << infer
84
                               << (isRev ? " :rev " : " ") << conc << std::endl;
85
    for (const Node& ec : exp)
86
    {
87
      Trace("strings-ipc-debug") << "    e: " << ec << std::endl;
88
    }
89
  }
90
  // try to find a set of proof steps to incorporate into the buffer
91
1261
  psb.clear();
92
1261
  NodeManager* nm = NodeManager::currentNM();
93
2522
  Node nodeIsRev = nm->mkConst(isRev);
94
1261
  switch (infer)
95
  {
96
    // ========================== equal by substitution+rewriting
97
308
    case InferenceId::STRINGS_I_NORM_S:
98
    case InferenceId::STRINGS_I_CONST_MERGE:
99
    case InferenceId::STRINGS_I_NORM:
100
    case InferenceId::STRINGS_LEN_NORM:
101
    case InferenceId::STRINGS_NORMAL_FORM:
102
    case InferenceId::STRINGS_CODE_PROXY:
103
    {
104
308
      ps.d_args.push_back(conc);
105
      // will attempt this rule
106
308
      ps.d_rule = PfRule::MACRO_SR_PRED_INTRO;
107
    }
108
308
    break;
109
    // ========================== substitution + rewriting
110
155
    case InferenceId::STRINGS_RE_NF_CONFLICT:
111
    case InferenceId::STRINGS_EXTF:
112
    case InferenceId::STRINGS_EXTF_N:
113
    case InferenceId::STRINGS_EXTF_D:
114
    case InferenceId::STRINGS_EXTF_D_N:
115
    case InferenceId::STRINGS_I_CONST_CONFLICT:
116
    case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
117
    {
118
155
      if (!ps.d_children.empty())
119
      {
120
162
        std::vector<Node> exps(ps.d_children.begin(), ps.d_children.end() - 1);
121
162
        Node src = ps.d_children[ps.d_children.size() - 1];
122
81
        if (psb.applyPredTransform(src, conc, exps))
123
        {
124
52
          useBuffer = true;
125
        }
126
      }
127
155
      if (!useBuffer)
128
      {
129
        // use the predicate version?
130
103
        ps.d_args.push_back(conc);
131
103
        ps.d_rule = PfRule::MACRO_SR_PRED_INTRO;
132
      }
133
    }
134
155
    break;
135
    // ========================== rewrite pred
136
19
    case InferenceId::STRINGS_EXTF_EQ_REW:
137
    case InferenceId::STRINGS_INFER_EMP:
138
    {
139
      // the last child is the predicate we are operating on, move to front
140
31
      Node src = ps.d_children[ps.d_children.size() - 1];
141
31
      std::vector<Node> expe(ps.d_children.begin(), ps.d_children.end() - 1);
142
      // start with a default rewrite
143
31
      Node mainEqSRew = psb.applyPredElim(src, expe);
144
19
      if (mainEqSRew == conc)
145
      {
146
        useBuffer = true;
147
        break;
148
      }
149
      // may need the "extended equality rewrite"
150
      Node mainEqSRew2 = psb.applyPredElim(
151
31
          mainEqSRew, {}, MethodId::SB_DEFAULT, MethodId::RW_REWRITE_EQ_EXT);
152
19
      if (mainEqSRew2 == conc)
153
      {
154
7
        useBuffer = true;
155
7
        break;
156
      }
157
      // rewrite again with default rewriter
158
24
      Node mainEqSRew3 = psb.applyPredElim(mainEqSRew2, {});
159
24
      useBuffer = (mainEqSRew3 == conc);
160
    }
161
12
    break;
162
    // ========================== substitution+rewriting, CONCAT_EQ, ...
163
419
    case InferenceId::STRINGS_F_CONST:
164
    case InferenceId::STRINGS_F_UNIFY:
165
    case InferenceId::STRINGS_F_ENDPOINT_EMP:
166
    case InferenceId::STRINGS_F_ENDPOINT_EQ:
167
    case InferenceId::STRINGS_F_NCTN:
168
    case InferenceId::STRINGS_N_EQ_CONF:
169
    case InferenceId::STRINGS_N_CONST:
170
    case InferenceId::STRINGS_N_UNIFY:
171
    case InferenceId::STRINGS_N_ENDPOINT_EMP:
172
    case InferenceId::STRINGS_N_ENDPOINT_EQ:
173
    case InferenceId::STRINGS_N_NCTN:
174
    case InferenceId::STRINGS_SSPLIT_CST_PROP:
175
    case InferenceId::STRINGS_SSPLIT_VAR_PROP:
176
    case InferenceId::STRINGS_SSPLIT_CST:
177
    case InferenceId::STRINGS_SSPLIT_VAR:
178
    {
179
838
      Trace("strings-ipc-core") << "Generate core rule for " << infer
180
419
                                << " (rev=" << isRev << ")" << std::endl;
181
      // All of the above inferences have the form:
182
      //   (explanation for why t and s have the same prefix/suffix) ^
183
      //   t = s ^
184
      //   (length constraint)?
185
      // We call t=s the "main equality" below. The length constraint is
186
      // optional, which we split on below.
187
419
      size_t nchild = ps.d_children.size();
188
419
      size_t mainEqIndex = 0;
189
419
      bool mainEqIndexSet = false;
190
      // the length constraint
191
764
      std::vector<Node> lenConstraint;
192
      // these inferences have a length constraint as the last explain
193
419
      if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY
194
285
          || infer == InferenceId::STRINGS_SSPLIT_CST || infer == InferenceId::STRINGS_SSPLIT_VAR
195
224
          || infer == InferenceId::STRINGS_SSPLIT_VAR_PROP
196
217
          || infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
197
      {
198
404
        if (exp.size() >= 2)
199
        {
200
202
          Assert(exp.size() <= startExpIndex.size());
201
          // The index of the "main" equality is the last equality before
202
          // the length explanation.
203
202
          mainEqIndex = startExpIndex[exp.size() - 1] - 1;
204
202
          mainEqIndexSet = true;
205
          // the remainder is the length constraint
206
606
          lenConstraint.insert(lenConstraint.end(),
207
404
                               ps.d_children.begin() + mainEqIndex + 1,
208
808
                               ps.d_children.end());
209
        }
210
      }
211
217
      else if (nchild >= 1)
212
      {
213
        // The index of the main equality is the last child.
214
217
        mainEqIndex = nchild - 1;
215
217
        mainEqIndexSet = true;
216
      }
217
764
      Node mainEq;
218
419
      if (mainEqIndexSet)
219
      {
220
419
        mainEq = ps.d_children[mainEqIndex];
221
838
        Trace("strings-ipc-core") << "Main equality " << mainEq << " at index "
222
419
                                  << mainEqIndex << std::endl;
223
      }
224
419
      if (mainEq.isNull() || mainEq.getKind() != EQUAL)
225
      {
226
        Trace("strings-ipc-core")
227
            << "...failed to find main equality" << std::endl;
228
        break;
229
      }
230
      // apply MACRO_SR_PRED_ELIM using equalities up to the main eq
231
764
      std::vector<Node> childrenSRew;
232
419
      childrenSRew.push_back(mainEq);
233
1257
      childrenSRew.insert(childrenSRew.end(),
234
                          ps.d_children.begin(),
235
1676
                          ps.d_children.begin() + mainEqIndex);
236
      Node mainEqSRew =
237
764
          psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {});
238
419
      if (CDProof::isSame(mainEqSRew, mainEq))
239
      {
240
67
        Trace("strings-ipc-core") << "...undo step" << std::endl;
241
        // the rule added above was not necessary
242
67
        psb.popStep();
243
      }
244
352
      else if (mainEqSRew == conc)
245
      {
246
73
        Trace("strings-ipc-core") << "...success after rewrite!" << std::endl;
247
73
        useBuffer = true;
248
73
        break;
249
      }
250
692
      Trace("strings-ipc-core")
251
346
          << "Main equality after subs+rewrite " << mainEqSRew << std::endl;
252
      // now, apply CONCAT_EQ to get the remainder
253
691
      std::vector<Node> childrenCeq;
254
346
      childrenCeq.push_back(mainEqSRew);
255
691
      std::vector<Node> argsCeq;
256
346
      argsCeq.push_back(nodeIsRev);
257
691
      Node mainEqCeq = psb.tryStep(PfRule::CONCAT_EQ, childrenCeq, argsCeq);
258
692
      Trace("strings-ipc-core")
259
346
          << "Main equality after CONCAT_EQ " << mainEqCeq << std::endl;
260
346
      if (mainEqCeq.isNull() || mainEqCeq.getKind() != EQUAL)
261
      {
262
        // fail
263
        break;
264
      }
265
346
      else if (mainEqCeq == mainEqSRew)
266
      {
267
87
        Trace("strings-ipc-core") << "...undo step" << std::endl;
268
        // not necessary, probably first component of equality
269
87
        psb.popStep();
270
      }
271
      // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
272
      // inference involved t and s.
273
346
      if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ
274
259
          || infer == InferenceId::STRINGS_N_ENDPOINT_EMP
275
259
          || infer == InferenceId::STRINGS_F_ENDPOINT_EQ
276
202
          || infer == InferenceId::STRINGS_F_ENDPOINT_EMP)
277
      {
278
        // Should be equal to conclusion already, or rewrite to it.
279
        // Notice that this step is necessary to handle the "rproc"
280
        // optimization in processSimpleNEq. Alternatively, this could
281
        // possibly be done by CONCAT_EQ with !isRev.
282
288
        std::vector<Node> cexp;
283
144
        if (psb.applyPredTransform(mainEqCeq,
284
                                   conc,
285
                                   cexp,
286
                                   MethodId::SB_DEFAULT,
287
                                   MethodId::RW_REWRITE_EQ_EXT))
288
        {
289
284
          Trace("strings-ipc-core") << "Transformed to " << conc
290
142
                                    << " via pred transform" << std::endl;
291
          // success
292
142
          useBuffer = true;
293
142
          Trace("strings-ipc-core") << "...success!" << std::endl;
294
144
        }
295
        // Otherwise, note that EMP rules conclude ti = "" where
296
        // t1 ++ ... ++ tn == "". However, these are very rarely applied, let
297
        // alone for 2+ children. This case is intentionally unhandled here.
298
      }
299
202
      else if (infer == InferenceId::STRINGS_N_CONST || infer == InferenceId::STRINGS_F_CONST
300
202
               || infer == InferenceId::STRINGS_N_EQ_CONF)
301
      {
302
        // should be a constant conflict
303
        std::vector<Node> childrenC;
304
        childrenC.push_back(mainEqCeq);
305
        std::vector<Node> argsC;
306
        argsC.push_back(nodeIsRev);
307
        Node mainEqC = psb.tryStep(PfRule::CONCAT_CONFLICT, childrenC, argsC);
308
        if (mainEqC == conc)
309
        {
310
          useBuffer = true;
311
          Trace("strings-ipc-core") << "...success!" << std::endl;
312
        }
313
      }
314
      else
315
      {
316
403
        std::vector<Node> tvec;
317
403
        std::vector<Node> svec;
318
202
        utils::getConcat(mainEqCeq[0], tvec);
319
202
        utils::getConcat(mainEqCeq[1], svec);
320
403
        Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
321
403
        Node s0 = svec[isRev ? svec.size() - 1 : 0];
322
202
        bool applySym = false;
323
        // may need to apply symmetry
324
404
        if ((infer == InferenceId::STRINGS_SSPLIT_CST
325
142
             || infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
326
262
            && t0.isConst())
327
        {
328
26
          Assert(!s0.isConst());
329
26
          applySym = true;
330
26
          std::swap(t0, s0);
331
        }
332
202
        if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY)
333
        {
334
134
          if (conc.getKind() != EQUAL)
335
          {
336
            break;
337
          }
338
          // one side should match, the other side could be a split constant
339
134
          if (conc[0] != t0 && conc[1] != s0)
340
          {
341
51
            applySym = true;
342
51
            std::swap(t0, s0);
343
          }
344
134
          Assert(conc[0].isConst() == t0.isConst());
345
134
          Assert(conc[1].isConst() == s0.isConst());
346
        }
347
202
        PfRule rule = PfRule::UNKNOWN;
348
        // the form of the required length constraint expected by the proof
349
403
        Node lenReq;
350
202
        bool lenSuccess = false;
351
202
        if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY)
352
        {
353
          // the required premise for unify is always len(x) = len(y),
354
          // however the explanation may not be literally this. Thus, we
355
          // need to reconstruct a proof from the given explanation.
356
          // it should be the case that lenConstraint => lenReq.
357
          // We use terms in the conclusion equality, not t0, s0 here.
358
402
          lenReq = nm->mkNode(STRING_LENGTH, conc[0])
359
268
                       .eqNode(nm->mkNode(STRING_LENGTH, conc[1]));
360
134
          lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
361
134
          rule = PfRule::CONCAT_UNIFY;
362
        }
363
68
        else if (infer == InferenceId::STRINGS_SSPLIT_VAR)
364
        {
365
          // it should be the case that lenConstraint => lenReq
366
3
          lenReq = nm->mkNode(STRING_LENGTH, t0)
367
2
                       .eqNode(nm->mkNode(STRING_LENGTH, s0))
368
2
                       .notNode();
369
1
          lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
370
1
          rule = PfRule::CONCAT_SPLIT;
371
        }
372
67
        else if (infer == InferenceId::STRINGS_SSPLIT_CST)
373
        {
374
          // it should be the case that lenConstraint => lenReq
375
180
          lenReq = nm->mkNode(STRING_LENGTH, t0)
376
120
                       .eqNode(nm->mkConst(Rational(0)))
377
120
                       .notNode();
378
60
          lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
379
60
          rule = PfRule::CONCAT_CSPLIT;
380
        }
381
7
        else if (infer == InferenceId::STRINGS_SSPLIT_VAR_PROP)
382
        {
383
          // it should be the case that lenConstraint => lenReq
384
11
          for (unsigned r = 0; r < 2; r++)
385
          {
386
30
            lenReq = nm->mkNode(GT,
387
20
                                nm->mkNode(STRING_LENGTH, t0),
388
20
                                nm->mkNode(STRING_LENGTH, s0));
389
10
            if (convertLengthPf(lenReq, lenConstraint, psb))
390
            {
391
6
              lenSuccess = true;
392
6
              break;
393
            }
394
4
            if (r == 0)
395
            {
396
              // may be the other direction
397
3
              applySym = true;
398
3
              std::swap(t0, s0);
399
            }
400
          }
401
7
          rule = PfRule::CONCAT_LPROP;
402
        }
403
        else if (infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
404
        {
405
          // it should be the case that lenConstraint => lenReq
406
          lenReq = nm->mkNode(STRING_LENGTH, t0)
407
                       .eqNode(nm->mkConst(Rational(0)))
408
                       .notNode();
409
          lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
410
          rule = PfRule::CONCAT_CPROP;
411
        }
412
202
        if (!lenSuccess)
413
        {
414
2
          Trace("strings-ipc-core")
415
1
              << "...failed due to length constraint" << std::endl;
416
1
          break;
417
        }
418
        // apply symmetry if necessary
419
201
        if (applySym)
420
        {
421
158
          std::vector<Node> childrenSymm;
422
79
          childrenSymm.push_back(mainEqCeq);
423
          // note this explicit step may not be necessary
424
79
          mainEqCeq = psb.tryStep(PfRule::SYMM, childrenSymm, {});
425
158
          Trace("strings-ipc-core")
426
79
              << "Main equality after SYMM " << mainEqCeq << std::endl;
427
        }
428
201
        if (rule != PfRule::UNKNOWN)
429
        {
430
402
          Trace("strings-ipc-core")
431
201
              << "Core rule length requirement is " << lenReq << std::endl;
432
          // apply the given rule
433
402
          std::vector<Node> childrenMain;
434
201
          childrenMain.push_back(mainEqCeq);
435
201
          childrenMain.push_back(lenReq);
436
402
          std::vector<Node> argsMain;
437
201
          argsMain.push_back(nodeIsRev);
438
402
          Node mainEqMain = psb.tryStep(rule, childrenMain, argsMain);
439
402
          Trace("strings-ipc-core") << "Main equality after " << rule << " "
440
201
                                    << mainEqMain << std::endl;
441
201
          if (mainEqMain == mainEqCeq)
442
          {
443
10
            Trace("strings-ipc-core") << "...undo step" << std::endl;
444
            // not necessary, probably first component of equality
445
10
            psb.popStep();
446
          }
447
          // either equal or rewrites to it
448
402
          std::vector<Node> cexp;
449
201
          if (psb.applyPredTransform(mainEqMain, conc, cexp))
450
          {
451
            // requires that length success is also true
452
199
            useBuffer = true;
453
199
            Trace("strings-ipc-core") << "...success" << std::endl;
454
          }
455
          else
456
          {
457
2
            Trace("strings-ipc-core") << "...fail" << std::endl;
458
          }
459
        }
460
        else
461
        {
462
          // should always have given a rule to try above
463
          Assert(false) << "No reconstruction rule given for " << infer;
464
        }
465
345
      }
466
    }
467
345
    break;
468
    // ========================== Disequalities
469
1
    case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
470
    case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
471
    {
472
3
      if (conc.getKind() != AND || conc.getNumChildren() != 2
473
2
          || conc[0].getKind() != EQUAL || !conc[0][0].getType().isStringLike()
474
2
          || conc[1].getKind() != EQUAL
475
3
          || conc[1][0].getKind() != STRING_LENGTH)
476
      {
477
        Trace("strings-ipc-deq") << "malformed application" << std::endl;
478
        Assert(false) << "unexpected conclusion " << conc << " for " << infer;
479
      }
480
      else
481
      {
482
        Node lenReq =
483
2
            nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, conc[0][0]), conc[1][1]);
484
2
        Trace("strings-ipc-deq")
485
1
            << "length requirement is " << lenReq << std::endl;
486
1
        if (convertLengthPf(lenReq, ps.d_children, psb))
487
        {
488
1
          Trace("strings-ipc-deq") << "...success length" << std::endl;
489
          // make the proof
490
2
          std::vector<Node> childrenMain;
491
1
          childrenMain.push_back(lenReq);
492
2
          std::vector<Node> argsMain;
493
1
          argsMain.push_back(nodeIsRev);
494
          Node mainConc =
495
2
              psb.tryStep(PfRule::STRING_DECOMPOSE, childrenMain, argsMain);
496
2
          Trace("strings-ipc-deq")
497
1
              << "...main conclusion is " << mainConc << std::endl;
498
1
          useBuffer = (mainConc == conc);
499
2
          Trace("strings-ipc-deq")
500
1
              << "...success is " << useBuffer << std::endl;
501
        }
502
        else
503
        {
504
          Trace("strings-ipc-deq") << "...fail length" << std::endl;
505
        }
506
      }
507
    }
508
1
    break;
509
    // ========================== Boolean split
510
55
    case InferenceId::STRINGS_CARD_SP:
511
    case InferenceId::STRINGS_LEN_SPLIT:
512
    case InferenceId::STRINGS_LEN_SPLIT_EMP:
513
    case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
514
    case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
515
    case InferenceId::STRINGS_DEQ_STRINGS_EQ:
516
    case InferenceId::STRINGS_DEQ_LENS_EQ:
517
    case InferenceId::STRINGS_DEQ_LENGTH_SP:
518
    {
519
55
      if (conc.getKind() != OR)
520
      {
521
        // This should never happen. If it does, we resort to using
522
        // STRING_TRUST below (in production mode).
523
        Assert(false) << "Expected OR conclusion for " << infer;
524
      }
525
      else
526
      {
527
55
        ps.d_rule = PfRule::SPLIT;
528
55
        Assert(ps.d_children.empty());
529
55
        ps.d_args.push_back(conc[0]);
530
      }
531
    }
532
55
    break;
533
    // ========================== Regular expression unfolding
534
28
    case InferenceId::STRINGS_RE_UNFOLD_POS:
535
    case InferenceId::STRINGS_RE_UNFOLD_NEG:
536
    {
537
28
      Assert (!ps.d_children.empty());
538
28
      size_t nchild = ps.d_children.size();
539
56
      Node mem = ps.d_children[nchild-1];
540
28
      if (nchild>1)
541
      {
542
        // if more than one, apply MACRO_SR_PRED_ELIM
543
        std::vector<Node> tcs;
544
        tcs.insert(tcs.end(),
545
                          ps.d_children.begin(),
546
                          ps.d_children.begin() + (nchild-1));
547
        mem = psb.applyPredElim(mem, tcs);
548
        useBuffer = true;
549
      }
550
28
      PfRule r = PfRule::UNKNOWN;
551
28
      if (mem.isNull())
552
      {
553
        // failed to eliminate above
554
        Assert(false) << "Failed to apply MACRO_SR_PRED_ELIM for RE unfold";
555
        useBuffer = false;
556
      }
557
28
      else if (infer == InferenceId::STRINGS_RE_UNFOLD_POS)
558
      {
559
23
        r = PfRule::RE_UNFOLD_POS;
560
      }
561
      else
562
      {
563
5
        r = PfRule::RE_UNFOLD_NEG;
564
        // it may be an optimized form of concat simplification
565
5
        Assert(mem.getKind() == NOT && mem[0].getKind() == STRING_IN_REGEXP);
566
5
        if (mem[0][1].getKind() == REGEXP_CONCAT)
567
        {
568
          size_t index;
569
10
          Node reLen = RegExpOpr::getRegExpConcatFixed(mem[0][1], index);
570
          // if we can find a fixed length for a component, use the optimized
571
          // version
572
5
          if (!reLen.isNull())
573
          {
574
3
            r = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED;
575
          }
576
        }
577
      }
578
28
      if (useBuffer)
579
      {
580
        mem = psb.tryStep(r, {mem}, {});
581
        // should match the conclusion
582
        useBuffer = (mem==conc);
583
      }
584
      else
585
      {
586
28
        ps.d_rule = r;
587
28
      }
588
    }
589
28
    break;
590
    // ========================== Reduction
591
77
    case InferenceId::STRINGS_CTN_POS:
592
    case InferenceId::STRINGS_CTN_NEG_EQUAL:
593
    {
594
77
      if (ps.d_children.size() != 1)
595
      {
596
        break;
597
      }
598
77
      bool polarity = ps.d_children[0].getKind() != NOT;
599
154
      Node atom = polarity ? ps.d_children[0] : ps.d_children[0][0];
600
154
      std::vector<Node> args;
601
77
      args.push_back(atom);
602
154
      Node res = psb.tryStep(PfRule::STRING_EAGER_REDUCTION, {}, args);
603
77
      if (res.isNull())
604
      {
605
        break;
606
      }
607
      // ite( contains(x,t), x = k1 ++ t ++ k2, x != t )
608
154
      std::vector<Node> tiChildren;
609
77
      tiChildren.push_back(ps.d_children[0]);
610
      Node ctnt = psb.tryStep(
611
154
          polarity ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO, tiChildren, {});
612
77
      if (ctnt.isNull() || ctnt.getKind() != EQUAL)
613
      {
614
        break;
615
      }
616
154
      std::vector<Node> tchildren;
617
77
      tchildren.push_back(ctnt);
618
      // apply substitution { contains(x,t) -> true|false } and rewrite to get
619
      // conclusion x = k1 ++ t ++ k2 or x != t.
620
77
      if (psb.applyPredTransform(res, conc, tchildren))
621
      {
622
77
        useBuffer = true;
623
77
      }
624
    }
625
77
    break;
626
627
104
    case InferenceId::STRINGS_REDUCTION:
628
    {
629
104
      size_t nchild = conc.getNumChildren();
630
208
      Node mainEq;
631
104
      if (conc.getKind() == EQUAL)
632
      {
633
3
        mainEq = conc;
634
      }
635
101
      else if (conc.getKind() == AND && conc[nchild - 1].getKind() == EQUAL)
636
      {
637
101
        mainEq = conc[nchild - 1];
638
      }
639
104
      if (mainEq.isNull())
640
      {
641
        Trace("strings-ipc-red") << "Bad Reduction: " << conc << std::endl;
642
        Assert(false) << "Unexpected reduction " << conc;
643
        break;
644
      }
645
208
      std::vector<Node> argsRed;
646
      // the left hand side of the last conjunct is the term we are reducing
647
104
      argsRed.push_back(mainEq[0]);
648
208
      Node red = psb.tryStep(PfRule::STRING_REDUCTION, {}, argsRed);
649
104
      Trace("strings-ipc-red") << "Reduction : " << red << std::endl;
650
104
      if (!red.isNull())
651
      {
652
        // either equal or rewrites to it
653
208
        std::vector<Node> cexp;
654
104
        if (psb.applyPredTransform(red, conc, cexp))
655
        {
656
93
          Trace("strings-ipc-red") << "...success!" << std::endl;
657
93
          useBuffer = true;
658
        }
659
        else
660
        {
661
11
          Trace("strings-ipc-red") << "...failed to reduce" << std::endl;
662
        }
663
104
      }
664
    }
665
104
    break;
666
    // ========================== code injectivity
667
44
    case InferenceId::STRINGS_CODE_INJ:
668
    {
669
44
      ps.d_rule = PfRule::STRING_CODE_INJ;
670
44
      Assert(conc.getKind() == OR && conc.getNumChildren() == 3
671
             && conc[2].getKind() == EQUAL);
672
44
      ps.d_args.push_back(conc[2][0]);
673
44
      ps.d_args.push_back(conc[2][1]);
674
    }
675
44
    break;
676
    // ========================== unit injectivity
677
10
    case InferenceId::STRINGS_UNIT_INJ: { ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ;
678
    }
679
10
    break;
680
    // ========================== prefix conflict
681
32
    case InferenceId::STRINGS_PREFIX_CONFLICT:
682
    {
683
32
      Trace("strings-ipc-prefix") << "Prefix conflict..." << std::endl;
684
64
      std::vector<Node> eqs;
685
74
      for (const Node& e : ps.d_children)
686
      {
687
42
        Kind ek = e.getKind();
688
42
        if (ek == EQUAL)
689
        {
690
32
          Trace("strings-ipc-prefix") << "- equality : " << e << std::endl;
691
32
          eqs.push_back(e);
692
        }
693
10
        else if (ek == STRING_IN_REGEXP)
694
        {
695
          // unfold it and extract the equality
696
20
          std::vector<Node> children;
697
10
          children.push_back(e);
698
20
          std::vector<Node> args;
699
20
          Node eunf = psb.tryStep(PfRule::RE_UNFOLD_POS, children, args);
700
20
          Trace("strings-ipc-prefix")
701
10
              << "--- " << e << " unfolds to " << eunf << std::endl;
702
10
          if (eunf.isNull())
703
          {
704
            continue;
705
          }
706
10
          else if (eunf.getKind() == AND)
707
          {
708
            // equality is the last conjunct
709
20
            std::vector<Node> childrenAE;
710
10
            childrenAE.push_back(eunf);
711
20
            std::vector<Node> argsAE;
712
10
            argsAE.push_back(nm->mkConst(Rational(eunf.getNumChildren() - 1)));
713
20
            Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE);
714
20
            Trace("strings-ipc-prefix")
715
10
                << "--- and elim to " << eunfAE << std::endl;
716
10
            if (eunfAE.isNull() || eunfAE.getKind() != EQUAL)
717
            {
718
              Assert(false)
719
                  << "Unexpected unfolded premise " << eunf << " for " << infer;
720
              continue;
721
            }
722
20
            Trace("strings-ipc-prefix")
723
10
                << "- equality : " << eunfAE << std::endl;
724
10
            eqs.push_back(eunfAE);
725
          }
726
          else if (eunf.getKind() == EQUAL)
727
          {
728
            Trace("strings-ipc-prefix") << "- equality : " << eunf << std::endl;
729
            eqs.push_back(eunf);
730
          }
731
        }
732
        else
733
        {
734
          // not sure how to use this assumption
735
          Assert(false) << "Unexpected premise " << e << " for " << infer;
736
        }
737
      }
738
32
      if (eqs.empty())
739
      {
740
        break;
741
      }
742
      // connect via transitivity
743
64
      Node curr = eqs[0];
744
42
      for (size_t i = 1, esize = eqs.size(); i < esize; i++)
745
      {
746
20
        Node prev = curr;
747
10
        curr = convertTrans(curr, eqs[1], psb);
748
10
        if (curr.isNull())
749
        {
750
          break;
751
        }
752
10
        Trace("strings-ipc-prefix") << "- Via trans: " << curr << std::endl;
753
      }
754
32
      if (curr.isNull())
755
      {
756
        break;
757
      }
758
64
      Trace("strings-ipc-prefix")
759
32
          << "- Possible conflicting equality : " << curr << std::endl;
760
64
      std::vector<Node> emp;
761
64
      Node concE = psb.applyPredElim(curr, emp);
762
64
      Trace("strings-ipc-prefix")
763
32
          << "- After pred elim: " << concE << std::endl;
764
32
      if (concE == conc)
765
      {
766
32
        Trace("strings-ipc-prefix") << "...success!" << std::endl;
767
32
        useBuffer = true;
768
32
      }
769
    }
770
32
    break;
771
    // ========================== regular expressions
772
7
    case InferenceId::STRINGS_RE_INTER_INCLUDE:
773
    case InferenceId::STRINGS_RE_INTER_CONF:
774
    case InferenceId::STRINGS_RE_INTER_INFER:
775
    {
776
14
      std::vector<Node> reiExp;
777
14
      std::vector<Node> reis;
778
14
      std::vector<Node> reiChildren;
779
14
      std::vector<Node> reiChildrenOrig;
780
14
      Node x;
781
      // make the regular expression intersection that summarizes all
782
      // memberships in the explanation
783
23
      for (const Node& c : ps.d_children)
784
      {
785
16
        bool polarity = c.getKind() != NOT;
786
30
        Node catom = polarity ? c : c[0];
787
18
        if (catom.getKind() != STRING_IN_REGEXP)
788
        {
789
2
          Assert(c.getKind() == EQUAL);
790
2
          if (c.getKind() == EQUAL)
791
          {
792
2
            reiExp.push_back(c);
793
          }
794
2
          continue;
795
        }
796
14
        if (x.isNull())
797
        {
798
          // just take the first LHS; others should be equated to it by exp
799
7
          x = catom[0];
800
        }
801
        Node rcurr =
802
28
            polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]);
803
14
        reis.push_back(rcurr);
804
28
        Node mem = nm->mkNode(STRING_IN_REGEXP, catom[0], rcurr);
805
14
        reiChildren.push_back(mem);
806
14
        reiChildrenOrig.push_back(c);
807
      }
808
      // go back and justify each premise
809
7
      bool successChildren = true;
810
21
      for (size_t i = 0, nchild = reiChildren.size(); i < nchild; i++)
811
      {
812
14
        if (!psb.applyPredTransform(reiChildrenOrig[i], reiChildren[i], reiExp))
813
        {
814
          Trace("strings-ipc-re")
815
              << "... failed to justify child " << reiChildren[i] << " from "
816
              << reiChildrenOrig[i] << std::endl;
817
          successChildren = false;
818
          break;
819
        }
820
      }
821
7
      if (!successChildren)
822
      {
823
        break;
824
      }
825
14
      Node mem = psb.tryStep(PfRule::RE_INTER, reiChildren, {});
826
14
      Trace("strings-ipc-re")
827
7
          << "Regular expression summary: " << mem << std::endl;
828
      // the conclusion is rewritable to the premises via rewriting?
829
7
      if (psb.applyPredTransform(mem, conc, {}))
830
      {
831
2
        Trace("strings-ipc-re") << "... success!" << std::endl;
832
2
        useBuffer = true;
833
      }
834
      else
835
      {
836
10
        Trace("strings-ipc-re")
837
5
            << "...failed to rewrite to conclusion" << std::endl;
838
7
      }
839
    }
840
7
    break;
841
    // ========================== unknown and currently unsupported
842
2
    case InferenceId::STRINGS_CARDINALITY:
843
    case InferenceId::STRINGS_I_CYCLE_E:
844
    case InferenceId::STRINGS_I_CYCLE:
845
    case InferenceId::STRINGS_RE_DELTA:
846
    case InferenceId::STRINGS_RE_DELTA_CONF:
847
    case InferenceId::STRINGS_RE_DERIVE:
848
    case InferenceId::STRINGS_FLOOP:
849
    case InferenceId::STRINGS_FLOOP_CONFLICT:
850
    case InferenceId::STRINGS_DEQ_NORM_EMP:
851
    case InferenceId::STRINGS_CTN_TRANS:
852
    case InferenceId::STRINGS_CTN_DECOMPOSE:
853
    default:
854
      // do nothing, these will be converted to STRING_TRUST below since the
855
      // rule is unknown.
856
2
      break;
857
  }
858
859
  // now see if we would succeed with the checker-to-try
860
1261
  bool success = false;
861
1261
  if (ps.d_rule != PfRule::UNKNOWN)
862
  {
863
1096
    Trace("strings-ipc") << "For " << infer << ", try proof rule " << ps.d_rule
864
548
                         << "...";
865
548
    Assert(ps.d_rule != PfRule::UNKNOWN);
866
1096
    Node pconc = psb.tryStep(ps.d_rule, ps.d_children, ps.d_args);
867
548
    if (pconc.isNull() || pconc != conc)
868
    {
869
8
      Trace("strings-ipc") << "failed, pconc is " << pconc << " (expected "
870
4
                           << conc << ")" << std::endl;
871
4
      ps.d_rule = PfRule::UNKNOWN;
872
    }
873
    else
874
    {
875
      // successfully set up a single step proof in ps
876
544
      success = true;
877
544
      Trace("strings-ipc") << "success!" << std::endl;
878
    }
879
  }
880
713
  else if (useBuffer)
881
  {
882
    // successfully set up a multi step proof in psb
883
684
    success = true;
884
  }
885
  else
886
  {
887
58
    Trace("strings-ipc") << "For " << infer << " " << conc
888
29
                         << ", no proof rule, failed" << std::endl;
889
  }
890
1261
  if (!success)
891
  {
892
    // debug print
893
33
    if (Trace.isOn("strings-ipc-fail"))
894
    {
895
      Trace("strings-ipc-fail")
896
          << "InferProofCons::convert: Failed " << infer
897
          << (isRev ? " :rev " : " ") << conc << std::endl;
898
      for (const Node& ec : exp)
899
      {
900
        Trace("strings-ipc-fail") << "    e: " << ec << std::endl;
901
      }
902
    }
903
    // untrustworthy conversion, the argument of STRING_TRUST is its conclusion
904
33
    ps.d_args.clear();
905
33
    ps.d_args.push_back(conc);
906
    // use the trust rule
907
33
    ps.d_rule = PfRule::STRING_TRUST;
908
    // add to stats
909
33
    d_statistics.d_inferencesNoPf << infer;
910
  }
911
1261
  if (Trace.isOn("strings-ipc-debug"))
912
  {
913
    if (useBuffer)
914
    {
915
      Trace("strings-ipc-debug")
916
          << "InferProofCons::convert returned buffer with "
917
          << psb.getNumSteps() << " steps:" << std::endl;
918
      const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
919
      for (const std::pair<Node, ProofStep>& step : steps)
920
      {
921
        Trace("strings-ipc-debug")
922
            << "- " << step.first << " via " << step.second << std::endl;
923
      }
924
    }
925
    else
926
    {
927
      Trace("strings-ipc-debug")
928
          << "InferProofCons::convert returned " << ps << std::endl;
929
    }
930
  }
931
1261
}
932
933
206
bool InferProofCons::convertLengthPf(Node lenReq,
934
                                     const std::vector<Node>& lenExp,
935
                                     TheoryProofStepBuffer& psb)
936
{
937
343
  for (const Node& le : lenExp)
938
  {
939
226
    if (lenReq == le)
940
    {
941
89
      return true;
942
    }
943
  }
944
234
  Trace("strings-ipc-len") << "Must explain " << lenReq << " by " << lenExp
945
117
                           << std::endl;
946
129
  for (const Node& le : lenExp)
947
  {
948
    // probably rewrites to it?
949
137
    std::vector<Node> exp;
950
125
    if (psb.applyPredTransform(le, lenReq, exp))
951
    {
952
78
      Trace("strings-ipc-len") << "...success by rewrite" << std::endl;
953
78
      return true;
954
    }
955
    // maybe x != "" => len(x) != 0
956
59
    std::vector<Node> children;
957
47
    children.push_back(le);
958
59
    std::vector<Node> args;
959
59
    Node res = psb.tryStep(PfRule::STRING_LENGTH_NON_EMPTY, children, args);
960
47
    if (res == lenReq)
961
    {
962
35
      Trace("strings-ipc-len") << "...success by LENGTH_NON_EMPTY" << std::endl;
963
35
      return true;
964
    }
965
  }
966
4
  Trace("strings-ipc-len") << "...failed" << std::endl;
967
4
  return false;
968
}
969
970
10
Node InferProofCons::convertTrans(Node eqa,
971
                                  Node eqb,
972
                                  TheoryProofStepBuffer& psb)
973
{
974
10
  if (eqa.getKind() != EQUAL || eqb.getKind() != EQUAL)
975
  {
976
    return Node::null();
977
  }
978
10
  for (uint32_t i = 0; i < 2; i++)
979
  {
980
10
    Node eqaSym = i == 0 ? eqa[1].eqNode(eqa[0]) : eqa;
981
10
    for (uint32_t j = 0; j < 2; j++)
982
    {
983
10
      Node eqbSym = j == 0 ? eqb : eqb[1].eqNode(eqb[1]);
984
10
      if (eqa[i] == eqb[j])
985
      {
986
20
        std::vector<Node> children;
987
10
        children.push_back(eqaSym);
988
10
        children.push_back(eqbSym);
989
10
        return psb.tryStep(PfRule::TRANS, children, {});
990
      }
991
    }
992
  }
993
  return Node::null();
994
}
995
996
1261
std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
997
{
998
  // temporary proof
999
2522
  CDProof pf(d_pnm);
1000
  // get the inference
1001
1261
  NodeInferInfoMap::iterator it = d_lazyFactMap.find(fact);
1002
1261
  if (it == d_lazyFactMap.end())
1003
  {
1004
    Node factSym = CDProof::getSymmFact(fact);
1005
    if (!factSym.isNull())
1006
    {
1007
      // Use the symmetric fact. There is no need to explictly make a
1008
      // SYMM proof, as this is handled by CDProof::getProofFor below.
1009
      it = d_lazyFactMap.find(factSym);
1010
    }
1011
  }
1012
1261
  AlwaysAssert(it != d_lazyFactMap.end());
1013
  // now go back and convert it to proof steps and add to proof
1014
1261
  bool useBuffer = false;
1015
2522
  ProofStep ps;
1016
2522
  TheoryProofStepBuffer psb(d_pnm->getChecker());
1017
2522
  std::shared_ptr<InferInfo> ii = (*it).second;
1018
  // run the conversion
1019
1261
  convert(ii->getId(), ii->d_idRev, ii->d_conc, ii->d_premises, ps, psb, useBuffer);
1020
  // make the proof based on the step or the buffer
1021
1261
  if (useBuffer)
1022
  {
1023
684
    if (!pf.addSteps(psb))
1024
    {
1025
      return nullptr;
1026
    }
1027
  }
1028
  else
1029
  {
1030
577
    if (!pf.addStep(fact, ps))
1031
    {
1032
      return nullptr;
1033
    }
1034
  }
1035
1261
  return pf.getProofFor(fact);
1036
}
1037
1038
2827
std::string InferProofCons::identify() const
1039
{
1040
2827
  return "strings::InferProofCons";
1041
}
1042
1043
}  // namespace strings
1044
}  // namespace theory
1045
26685
}  // namespace CVC4