GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/proof_post_processor.cpp Lines: 504 549 91.8 %
Date: 2021-03-22 Branches: 941 2448 38.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_post_processor.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 module for processing proof nodes
13
 **/
14
15
#include "smt/proof_post_processor.h"
16
17
#include "expr/proof_node_manager.h"
18
#include "expr/skolem_manager.h"
19
#include "options/proof_options.h"
20
#include "options/smt_options.h"
21
#include "preprocessing/assertion_pipeline.h"
22
#include "smt/smt_engine.h"
23
#include "smt/smt_statistics_registry.h"
24
#include "theory/builtin/proof_checker.h"
25
#include "theory/rewriter.h"
26
#include "theory/theory.h"
27
28
using namespace CVC4::kind;
29
using namespace CVC4::theory;
30
31
namespace CVC4 {
32
namespace smt {
33
34
962
ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm,
35
                                                   SmtEngine* smte,
36
962
                                                   ProofGenerator* pppg)
37
962
    : d_pnm(pnm), d_smte(smte), d_pppg(pppg), d_wfpm(pnm)
38
{
39
962
  d_true = NodeManager::currentNM()->mkConst(true);
40
  // always check whether to update ASSUME
41
962
  d_elimRules.insert(PfRule::ASSUME);
42
962
}
43
44
1146
void ProofPostprocessCallback::initializeUpdate()
45
{
46
1146
  d_assumpToProof.clear();
47
1146
  d_wfAssumptions.clear();
48
1146
}
49
50
6734
void ProofPostprocessCallback::setEliminateRule(PfRule rule)
51
{
52
6734
  d_elimRules.insert(rule);
53
6734
}
54
55
1825555
bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
56
                                            bool& continueUpdate)
57
{
58
1825555
  return d_elimRules.find(pn->getRule()) != d_elimRules.end();
59
}
60
61
390267
bool ProofPostprocessCallback::update(Node res,
62
                                      PfRule id,
63
                                      const std::vector<Node>& children,
64
                                      const std::vector<Node>& args,
65
                                      CDProof* cdp,
66
                                      bool& continueUpdate)
67
{
68
780534
  Trace("smt-proof-pp-debug") << "- Post process " << id << " " << children
69
390267
                              << " / " << args << std::endl;
70
71
390267
  if (id == PfRule::ASSUME)
72
  {
73
    // we cache based on the assumption node, not the proof node, since there
74
    // may be multiple occurrences of the same node.
75
529676
    Node f = args[0];
76
529676
    std::shared_ptr<ProofNode> pfn;
77
    std::map<Node, std::shared_ptr<ProofNode>>::iterator it =
78
264838
        d_assumpToProof.find(f);
79
264838
    if (it != d_assumpToProof.end())
80
    {
81
243342
      Trace("smt-proof-pp-debug") << "...already computed" << std::endl;
82
243342
      pfn = it->second;
83
    }
84
    else
85
    {
86
21496
      Trace("smt-proof-pp-debug") << "...get proof" << std::endl;
87
21496
      Assert(d_pppg != nullptr);
88
      // get proof from preprocess proof generator
89
21496
      pfn = d_pppg->getProofFor(f);
90
21496
      Trace("smt-proof-pp-debug") << "...finished get proof" << std::endl;
91
      // print for debugging
92
21496
      if (pfn == nullptr)
93
      {
94
29238
        Trace("smt-proof-pp-debug")
95
14619
            << "...no proof, possibly an input assumption" << std::endl;
96
      }
97
      else
98
      {
99
6877
        Assert(pfn->getResult() == f);
100
6877
        if (Trace.isOn("smt-proof-pp"))
101
        {
102
          Trace("smt-proof-pp")
103
              << "=== Connect proof for preprocessing: " << f << std::endl;
104
          Trace("smt-proof-pp") << *pfn.get() << std::endl;
105
        }
106
      }
107
21496
      d_assumpToProof[f] = pfn;
108
    }
109
264838
    if (pfn == nullptr || pfn->getRule() == PfRule::ASSUME)
110
    {
111
258114
      Trace("smt-proof-pp-debug") << "...do not add proof" << std::endl;
112
      // no update
113
258114
      return false;
114
    }
115
6724
    Trace("smt-proof-pp-debug") << "...add proof" << std::endl;
116
    // connect the proof
117
6724
    cdp->addProof(pfn);
118
6724
    return true;
119
  }
120
250858
  Node ret = expandMacros(id, children, args, cdp);
121
125429
  Trace("smt-proof-pp-debug") << "...expanded = " << !ret.isNull() << std::endl;
122
125429
  return !ret.isNull();
123
}
124
125
55356
bool ProofPostprocessCallback::updateInternal(Node res,
126
                                              PfRule id,
127
                                              const std::vector<Node>& children,
128
                                              const std::vector<Node>& args,
129
                                              CDProof* cdp)
130
{
131
55356
  bool continueUpdate = true;
132
55356
  return update(res, id, children, args, cdp, continueUpdate);
133
}
134
135
6996
Node ProofPostprocessCallback::eliminateCrowdingLits(
136
    const std::vector<Node>& clauseLits,
137
    const std::vector<Node>& targetClauseLits,
138
    const std::vector<Node>& children,
139
    const std::vector<Node>& args,
140
    CDProof* cdp)
141
{
142
6996
  Trace("smt-proof-pp-debug2") << push;
143
6996
  NodeManager* nm = NodeManager::currentNM();
144
13992
  Node trueNode = nm->mkConst(true);
145
  // get crowding lits and the position of the last clause that includes
146
  // them. The factoring step must be added after the last inclusion and before
147
  // its elimination.
148
13992
  std::unordered_set<TNode, TNodeHashFunction> crowding;
149
13992
  std::vector<std::pair<Node, size_t>> lastInclusion;
150
  // positions of eliminators of crowding literals, which are the positions of
151
  // the clauses that eliminate crowding literals *after* their last inclusion
152
13992
  std::vector<size_t> eliminators;
153
251831
  for (size_t i = 0, size = clauseLits.size(); i < size; ++i)
154
  {
155
734505
    if (!crowding.count(clauseLits[i])
156
1160801
        && std::find(
157
213148
               targetClauseLits.begin(), targetClauseLits.end(), clauseLits[i])
158
671131
               == targetClauseLits.end())
159
    {
160
85424
      Node crowdLit = clauseLits[i];
161
42712
      crowding.insert(crowdLit);
162
42712
      Trace("smt-proof-pp-debug2") << "crowding lit " << crowdLit << "\n";
163
      // found crowding lit, now get its last inclusion position, which is the
164
      // position of the last resolution link that introduces the crowding
165
      // literal. Note that this position has to be *before* the last link, as a
166
      // link *after* the last inclusion must eliminate the crowding literal.
167
      size_t j;
168
1167339
      for (j = children.size() - 1; j > 0; --j)
169
      {
170
        // notice that only non-singleton clauses may be introducing the
171
        // crowding literal, so we only care about non-singleton OR nodes. We
172
        // check then against the kind and whether the whole OR node occurs as a
173
        // pivot of the respective resolution
174
1167339
        if (children[j - 1].getKind() != kind::OR)
175
        {
176
340605
          continue;
177
        }
178
826734
        uint64_t pivotIndex = 2 * (j - 1);
179
1653468
        if (args[pivotIndex] == children[j - 1]
180
1653468
            || args[pivotIndex].notNode() == children[j - 1])
181
        {
182
578
          continue;
183
        }
184
2478468
        if (std::find(children[j - 1].begin(), children[j - 1].end(), crowdLit)
185
2478468
            != children[j - 1].end())
186
        {
187
42712
          break;
188
        }
189
      }
190
42712
      Assert(j > 0);
191
42712
      lastInclusion.emplace_back(crowdLit, j - 1);
192
193
42712
      Trace("smt-proof-pp-debug2") << "last inc " << j - 1 << "\n";
194
      // get elimination position, starting from the following link as the last
195
      // inclusion one. The result is the last (in the chain, but first from
196
      // this point on) resolution link that eliminates the crowding literal. A
197
      // literal l is eliminated by a link if it contains a literal l' with
198
      // opposite polarity to l.
199
636310
      for (; j < children.size(); ++j)
200
      {
201
339511
        bool posFirst = args[(2 * j) - 1] == trueNode;
202
636310
        Node pivot = args[(2 * j)];
203
679022
        Trace("smt-proof-pp-debug2")
204
339511
            << "\tcheck w/ args " << posFirst << " / " << pivot << "\n";
205
        // To eliminate the crowding literal (crowdLit), the clause must contain
206
        // it with opposite polarity. There are three successful cases,
207
        // according to the pivot and its sign
208
        //
209
        // - crowdLit is the same as the pivot and posFirst is true, which means
210
        //   that the clause contains its negation and eliminates it
211
        //
212
        // - crowdLit is the negation of the pivot and posFirst is false, so the
213
        //   clause contains the node whose negation is crowdLit. Note that this
214
        //   case may either be crowdLit.notNode() == pivot or crowdLit ==
215
        //   pivot.notNode().
216
690163
        if ((crowdLit == pivot && posFirst)
217
667881
            || (crowdLit.notNode() == pivot && !posFirst)
218
1007392
            || (pivot.notNode() == crowdLit && !posFirst))
219
        {
220
42712
          Trace("smt-proof-pp-debug2") << "\t\tfound it!\n";
221
42712
          eliminators.push_back(j);
222
42712
          break;
223
        }
224
      }
225
42712
      AlwaysAssert(j < children.size());
226
    }
227
  }
228
6996
  Assert(!lastInclusion.empty());
229
  // order map so that we process crowding literals in the order of the clauses
230
  // that last introduce them
231
105684
  auto cmp = [](std::pair<Node, size_t>& a, std::pair<Node, size_t>& b) {
232
105684
    return a.second < b.second;
233
105684
  };
234
6996
  std::sort(lastInclusion.begin(), lastInclusion.end(), cmp);
235
  // order eliminators
236
6996
  std::sort(eliminators.begin(), eliminators.end());
237
6996
  if (Trace.isOn("smt-proof-pp-debug"))
238
  {
239
    Trace("smt-proof-pp-debug") << "crowding lits last inclusion:\n";
240
    for (const auto& pair : lastInclusion)
241
    {
242
      Trace("smt-proof-pp-debug")
243
          << "\t- [" << pair.second << "] : " << pair.first << "\n";
244
    }
245
    Trace("smt-proof-pp-debug") << "eliminators:";
246
    for (size_t elim : eliminators)
247
    {
248
      Trace("smt-proof-pp-debug") << " " << elim;
249
    }
250
    Trace("smt-proof-pp-debug") << "\n";
251
  }
252
  // TODO (cvc4-wishues/issues/77): implement also simpler version and compare
253
  //
254
  // We now start to break the chain, one step at a time. Naively this breaking
255
  // down would be one resolution/factoring to each crowding literal, but we can
256
  // merge some of the cases. Effectively we do the following:
257
  //
258
  //
259
  // lastClause   children[start] ... children[end]
260
  // ---------------------------------------------- CHAIN_RES
261
  //         C
262
  //    ----------- FACTORING
263
  //    lastClause'                children[start'] ... children[end']
264
  //    -------------------------------------------------------------- CHAIN_RES
265
  //                                    ...
266
  //
267
  // where
268
  //   lastClause_0 = children[0]
269
  //   start_0 = 1
270
  //   end_0 = eliminators[0] - 1
271
  //   start_i+1 = nextGuardedElimPos - 1
272
  //
273
  // The important point is how end_i+1 is computed. It is based on what we call
274
  // the "nextGuardedElimPos", i.e., the next elimination position that requires
275
  // removal of duplicates. The intuition is that a factoring step may eliminate
276
  // the duplicates of crowding literals l1 and l2. If the last inclusion of l2
277
  // is before the elimination of l1, then we can go ahead and also perform the
278
  // elimination of l2 without another factoring. However if another literal l3
279
  // has its last inclusion after the elimination of l2, then the elimination of
280
  // l3 is the next guarded elimination.
281
  //
282
  // To do the above computation then we determine, after a resolution/factoring
283
  // step, the first crowded literal to have its last inclusion after "end". The
284
  // first elimination position to be bigger than the position of that crowded
285
  // literal is the next guarded elimination position.
286
6996
  size_t lastElim = 0;
287
6996
  Node lastClause = children[0];
288
13992
  std::vector<Node> childrenRes;
289
13992
  std::vector<Node> childrenResArgs;
290
13992
  Node resPlaceHolder;
291
6996
  size_t nextGuardedElimPos = eliminators[0];
292
  do
293
  {
294
34110
    size_t start = lastElim + 1;
295
34110
    size_t end = nextGuardedElimPos - 1;
296
68220
    Trace("smt-proof-pp-debug2")
297
34110
        << "res with:\n\tlastClause: " << lastClause << "\n\tstart: " << start
298
34110
        << "\n\tend: " << end << "\n";
299
34110
    childrenRes.push_back(lastClause);
300
    // note that the interval of insert is exclusive in the end, so we add 1
301
102330
    childrenRes.insert(childrenRes.end(),
302
68220
                       children.begin() + start,
303
170550
                       children.begin() + end + 1);
304
102330
    childrenResArgs.insert(childrenResArgs.end(),
305
68220
                           args.begin() + (2 * start) - 1,
306
170550
                           args.begin() + (2 * end) + 1);
307
34110
    Trace("smt-proof-pp-debug2") << "res children: " << childrenRes << "\n";
308
34110
    Trace("smt-proof-pp-debug2") << "res args: " << childrenResArgs << "\n";
309
68220
    resPlaceHolder = d_pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION,
310
                                                     childrenRes,
311
                                                     childrenResArgs,
312
68220
                                                     Node::null(),
313
                                                     "");
314
68220
    Trace("smt-proof-pp-debug2")
315
34110
        << "resPlaceHorder: " << resPlaceHolder << "\n";
316
34110
    cdp->addStep(
317
        resPlaceHolder, PfRule::CHAIN_RESOLUTION, childrenRes, childrenResArgs);
318
    // I need to add factoring if end < children.size(). Otherwise, this is
319
    // to be handled by the caller
320
34110
    if (end < children.size() - 1)
321
    {
322
81342
      lastClause = d_pnm->getChecker()->checkDebug(
323
81342
          PfRule::FACTORING, {resPlaceHolder}, {}, Node::null(), "");
324
27114
      if (!lastClause.isNull())
325
      {
326
27114
        cdp->addStep(lastClause, PfRule::FACTORING, {resPlaceHolder}, {});
327
      }
328
      else
329
      {
330
        lastClause = resPlaceHolder;
331
      }
332
27114
      Trace("smt-proof-pp-debug2") << "lastClause: " << lastClause << "\n";
333
    }
334
    else
335
    {
336
6996
      lastClause = resPlaceHolder;
337
6996
      break;
338
    }
339
    // update for next round
340
27114
    childrenRes.clear();
341
27114
    childrenResArgs.clear();
342
27114
    lastElim = end;
343
344
    // find the position of the last inclusion of the next crowded literal
345
27114
    size_t nextCrowdedInclusionPos = lastInclusion.size();
346
212111
    for (size_t i = 0, size = lastInclusion.size(); i < size; ++i)
347
    {
348
205115
      if (lastInclusion[i].second > lastElim)
349
      {
350
20118
        nextCrowdedInclusionPos = i;
351
20118
        break;
352
      }
353
    }
354
54228
    Trace("smt-proof-pp-debug2")
355
27114
        << "nextCrowdedInclusion/Pos: "
356
27114
        << lastInclusion[nextCrowdedInclusionPos].second << "/"
357
27114
        << nextCrowdedInclusionPos << "\n";
358
    // if there is none, then the remaining literals will be used in the next
359
    // round
360
27114
    if (nextCrowdedInclusionPos == lastInclusion.size())
361
    {
362
6996
      nextGuardedElimPos = children.size();
363
    }
364
    else
365
    {
366
20118
      nextGuardedElimPos = children.size();
367
141908
      for (size_t i = 0, size = eliminators.size(); i < size; ++i)
368
      {
369
        //  nextGuardedElimPos is the largest element of
370
        // eliminators bigger the next crowded literal's last inclusion
371
141908
        if (eliminators[i] > lastInclusion[nextCrowdedInclusionPos].second)
372
        {
373
20118
          nextGuardedElimPos = eliminators[i];
374
20118
          break;
375
        }
376
      }
377
20118
      Assert(nextGuardedElimPos < children.size());
378
    }
379
54228
    Trace("smt-proof-pp-debug2")
380
54228
        << "nextGuardedElimPos: " << nextGuardedElimPos << "\n";
381
  } while (true);
382
13992
  Trace("smt-proof-pp-debug2") << pop;
383
13992
  return lastClause;
384
}
385
386
202256
Node ProofPostprocessCallback::expandMacros(PfRule id,
387
                                            const std::vector<Node>& children,
388
                                            const std::vector<Node>& args,
389
                                            CDProof* cdp)
390
{
391
202256
  if (d_elimRules.find(id) == d_elimRules.end())
392
  {
393
    // not eliminated
394
    return Node::null();
395
  }
396
  // macro elimination
397
202256
  if (id == PfRule::MACRO_SR_EQ_INTRO)
398
  {
399
    // (TRANS
400
    //   (SUBS <children> :args args[0:1])
401
    //   (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
402
159318
    std::vector<Node> tchildren;
403
159318
    Node t = args[0];
404
159318
    Node ts;
405
79659
    if (!children.empty())
406
    {
407
24934
      std::vector<Node> sargs;
408
12467
      sargs.push_back(t);
409
12467
      MethodId sid = MethodId::SB_DEFAULT;
410
12467
      if (args.size() >= 2)
411
      {
412
8412
        if (builtin::BuiltinProofRuleChecker::getMethodId(args[1], sid))
413
        {
414
8412
          sargs.push_back(args[1]);
415
        }
416
      }
417
12467
      ts =
418
24934
          builtin::BuiltinProofRuleChecker::applySubstitution(t, children, sid);
419
24934
      Trace("smt-proof-pp-debug")
420
12467
          << "...eq intro subs equality is " << t << " == " << ts << ", from "
421
12467
          << sid << std::endl;
422
12467
      if (ts != t)
423
      {
424
13990
        Node eq = t.eqNode(ts);
425
        // apply SUBS proof rule if necessary
426
6995
        if (!updateInternal(eq, PfRule::SUBS, children, sargs, cdp))
427
        {
428
          // if we specified that we did not want to eliminate, add as step
429
          cdp->addStep(eq, PfRule::SUBS, children, sargs);
430
        }
431
6995
        tchildren.push_back(eq);
432
      }
433
    }
434
    else
435
    {
436
      // no substitute
437
67192
      ts = t;
438
    }
439
159318
    std::vector<Node> rargs;
440
79659
    rargs.push_back(ts);
441
79659
    MethodId rid = MethodId::RW_REWRITE;
442
79659
    if (args.size() >= 3)
443
    {
444
10
      if (builtin::BuiltinProofRuleChecker::getMethodId(args[2], rid))
445
      {
446
10
        rargs.push_back(args[2]);
447
      }
448
    }
449
    builtin::BuiltinProofRuleChecker* builtinPfC =
450
        static_cast<builtin::BuiltinProofRuleChecker*>(
451
79659
            d_pnm->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO));
452
159318
    Node tr = builtinPfC->applyRewrite(ts, rid);
453
159318
    Trace("smt-proof-pp-debug")
454
79659
        << "...eq intro rewrite equality is " << ts << " == " << tr << ", from "
455
79659
        << rid << std::endl;
456
79659
    if (ts != tr)
457
    {
458
96722
      Node eq = ts.eqNode(tr);
459
      // apply REWRITE proof rule
460
48361
      if (!updateInternal(eq, PfRule::REWRITE, {}, rargs, cdp))
461
      {
462
        // if not elimianted, add as step
463
        cdp->addStep(eq, PfRule::REWRITE, {}, rargs);
464
      }
465
48361
      tchildren.push_back(eq);
466
    }
467
79659
    if (t == tr)
468
    {
469
      // typically not necessary, but done to be robust
470
30336
      cdp->addStep(t.eqNode(tr), PfRule::REFL, {}, {t});
471
30336
      return t.eqNode(tr);
472
    }
473
    // must add TRANS if two step
474
49323
    return addProofForTrans(tchildren, cdp);
475
  }
476
122597
  else if (id == PfRule::MACRO_SR_PRED_INTRO)
477
  {
478
14198
    std::vector<Node> tchildren;
479
14198
    std::vector<Node> sargs = args;
480
    // take into account witness form, if necessary
481
7099
    bool reqWitness = d_wfpm.requiresWitnessFormIntro(args[0]);
482
14198
    Trace("smt-proof-pp-debug")
483
7099
        << "...pred intro reqWitness=" << reqWitness << std::endl;
484
    // (TRUE_ELIM
485
    // (TRANS
486
    //    (MACRO_SR_EQ_INTRO <children> :args (t args[1:]))
487
    //    ... proof of apply_SR(t) = toWitness(apply_SR(t)) ...
488
    //    (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))})
489
    // ))
490
    // Notice this is an optimized, one sided version of the expansion of
491
    // MACRO_SR_PRED_TRANSFORM below.
492
    // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
493
    // that this rule application is immediately expanded in the recursive
494
    // call and not added to the proof.
495
14198
    Node conc = expandMacros(PfRule::MACRO_SR_EQ_INTRO, children, sargs, cdp);
496
14198
    Trace("smt-proof-pp-debug")
497
7099
        << "...pred intro conclusion is " << conc << std::endl;
498
7099
    Assert(!conc.isNull());
499
7099
    Assert(conc.getKind() == EQUAL);
500
7099
    Assert(conc[0] == args[0]);
501
7099
    tchildren.push_back(conc);
502
7099
    if (reqWitness)
503
    {
504
5286
      Node weq = addProofForWitnessForm(conc[1], cdp);
505
2643
      Trace("smt-proof-pp-debug") << "...weq is " << weq << std::endl;
506
2643
      if (addToTransChildren(weq, tchildren))
507
      {
508
        // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
509
        // rewrite again, don't need substitution. Also we always use the
510
        // default rewriter, due to the definition of MACRO_SR_PRED_INTRO.
511
4734
        Node weqr = expandMacros(PfRule::MACRO_SR_EQ_INTRO, {}, {weq[1]}, cdp);
512
2367
        addToTransChildren(weqr, tchildren);
513
      }
514
    }
515
    // apply transitivity if necessary
516
14198
    Node eq = addProofForTrans(tchildren, cdp);
517
7099
    Assert(!eq.isNull());
518
7099
    Assert(eq.getKind() == EQUAL);
519
7099
    Assert(eq[0] == args[0]);
520
7099
    Assert(eq[1] == d_true);
521
522
7099
    cdp->addStep(eq[0], PfRule::TRUE_ELIM, {eq}, {});
523
7099
    return eq[0];
524
  }
525
115498
  else if (id == PfRule::MACRO_SR_PRED_ELIM)
526
  {
527
    // (EQ_RESOLVE
528
    //   children[0]
529
    //   (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
530
3946
    std::vector<Node> schildren(children.begin() + 1, children.end());
531
3946
    std::vector<Node> srargs;
532
1973
    srargs.push_back(children[0]);
533
1973
    srargs.insert(srargs.end(), args.begin(), args.end());
534
3946
    Node conc = expandMacros(PfRule::MACRO_SR_EQ_INTRO, schildren, srargs, cdp);
535
1973
    Assert(!conc.isNull());
536
1973
    Assert(conc.getKind() == EQUAL);
537
1973
    Assert(conc[0] == children[0]);
538
    // apply equality resolve
539
1973
    cdp->addStep(conc[1], PfRule::EQ_RESOLVE, {children[0], conc}, {});
540
1973
    return conc[1];
541
  }
542
113525
  else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
543
  {
544
    // (EQ_RESOLVE
545
    //   children[0]
546
    //   (TRANS
547
    //      (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
548
    //      ... proof of c = wc
549
    //      (MACRO_SR_EQ_INTRO {} wc)
550
    //      (SYMM
551
    //        (MACRO_SR_EQ_INTRO children[1:] :args <args>)
552
    //        ... proof of a = wa
553
    //        (MACRO_SR_EQ_INTRO {} wa))))
554
    // where
555
    // wa = toWitness(apply_SR(args[0])) and
556
    // wc = toWitness(apply_SR(children[0])).
557
66856
    Trace("smt-proof-pp-debug")
558
33428
        << "Transform " << children[0] << " == " << args[0] << std::endl;
559
33428
    if (CDProof::isSame(children[0], args[0]))
560
    {
561
2864
      Trace("smt-proof-pp-debug") << "...nothing to do" << std::endl;
562
      // nothing to do
563
2864
      return children[0];
564
    }
565
61128
    std::vector<Node> tchildren;
566
61128
    std::vector<Node> schildren(children.begin() + 1, children.end());
567
61128
    std::vector<Node> sargs = args;
568
    // first, compute if we need
569
30564
    bool reqWitness = d_wfpm.requiresWitnessFormTransform(children[0], args[0]);
570
30564
    Trace("smt-proof-pp-debug") << "...reqWitness=" << reqWitness << std::endl;
571
    // convert both sides, in three steps, take symmetry of second chain
572
91692
    for (unsigned r = 0; r < 2; r++)
573
    {
574
122256
      std::vector<Node> tchildrenr;
575
      // first rewrite children[0], then args[0]
576
61128
      sargs[0] = r == 0 ? children[0] : args[0];
577
      // t = apply_SR(t)
578
122256
      Node eq = expandMacros(PfRule::MACRO_SR_EQ_INTRO, schildren, sargs, cdp);
579
122256
      Trace("smt-proof-pp-debug")
580
61128
          << "transform subs_rewrite (" << r << "): " << eq << std::endl;
581
61128
      Assert(!eq.isNull() && eq.getKind() == EQUAL && eq[0] == sargs[0]);
582
61128
      addToTransChildren(eq, tchildrenr);
583
      // apply_SR(t) = toWitness(apply_SR(t))
584
61128
      if (reqWitness)
585
      {
586
22260
        Node weq = addProofForWitnessForm(eq[1], cdp);
587
22260
        Trace("smt-proof-pp-debug")
588
11130
            << "transform toWitness (" << r << "): " << weq << std::endl;
589
11130
        if (addToTransChildren(weq, tchildrenr))
590
        {
591
          // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
592
          // rewrite again, don't need substitution. Also, we always use the
593
          // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM.
594
          Node weqr =
595
8520
              expandMacros(PfRule::MACRO_SR_EQ_INTRO, {}, {weq[1]}, cdp);
596
8520
          Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
597
4260
                                      << "): " << weqr << std::endl;
598
4260
          addToTransChildren(weqr, tchildrenr);
599
        }
600
      }
601
122256
      Trace("smt-proof-pp-debug")
602
61128
          << "transform connect (" << r << ")" << std::endl;
603
      // add to overall chain
604
61128
      if (r == 0)
605
      {
606
        // add the current chain to the overall chain
607
30564
        tchildren.insert(tchildren.end(), tchildrenr.begin(), tchildrenr.end());
608
      }
609
      else
610
      {
611
        // add the current chain to cdp
612
61128
        Node eqr = addProofForTrans(tchildrenr, cdp);
613
30564
        if (!eqr.isNull())
614
        {
615
39292
          Trace("smt-proof-pp-debug") << "transform connect sym " << tchildren
616
19646
                                      << " " << eqr << std::endl;
617
          // take symmetry of above and add it to the overall chain
618
19646
          addToTransChildren(eqr, tchildren, true);
619
        }
620
      }
621
122256
      Trace("smt-proof-pp-debug")
622
61128
          << "transform finish (" << r << ")" << std::endl;
623
    }
624
625
    // apply transitivity if necessary
626
61128
    Node eq = addProofForTrans(tchildren, cdp);
627
628
30564
    cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {});
629
30564
    return args[0];
630
  }
631
80097
  else if (id == PfRule::MACRO_RESOLUTION)
632
  {
633
    // first generate the naive chain_resolution
634
41668
    std::vector<Node> chainResArgs{args.begin() + 1, args.end()};
635
20834
    Node chainConclusion = d_pnm->getChecker()->checkDebug(
636
41668
        PfRule::CHAIN_RESOLUTION, children, chainResArgs, Node::null(), "");
637
20834
    Trace("smt-proof-pp-debug") << "Original conclusion: " << args[0] << "\n";
638
41668
    Trace("smt-proof-pp-debug")
639
20834
        << "chainRes conclusion: " << chainConclusion << "\n";
640
    // There are n cases:
641
    // - if the conclusion is the same, just replace
642
    // - if they have the same literals but in different quantity, add a
643
    //   FACTORING step
644
    // - if the order is not the same, add a REORDERING step
645
    // - if there are literals in chainConclusion that are not in the original
646
    //   conclusion, we need to transform the MACRO_RESOLUTION into a series of
647
    //   CHAIN_RESOLUTION + FACTORING steps, so that we explicitly eliminate all
648
    //   these "crowding" literals. We do this via FACTORING so we avoid adding
649
    //   an exponential number of premises, which would happen if we just
650
    //   repeated in the premises the clauses needed for eliminating crowding
651
    //   literals, which could themselves add crowding literals.
652
20834
    if (chainConclusion == args[0])
653
    {
654
10729
      cdp->addStep(
655
          chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);
656
10729
      return chainConclusion;
657
    }
658
10105
    NodeManager* nm = NodeManager::currentNM();
659
    // If we got here, then chainConclusion is NECESSARILY an OR node
660
10105
    Assert(chainConclusion.getKind() == kind::OR);
661
    // get the literals in the chain conclusion
662
    std::vector<Node> chainConclusionLits{chainConclusion.begin(),
663
20210
                                          chainConclusion.end()};
664
    std::set<Node> chainConclusionLitsSet{chainConclusion.begin(),
665
20210
                                          chainConclusion.end()};
666
    // is args[0] a singleton clause? If it's not an OR node, then yes.
667
    // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet
668
20210
    std::vector<Node> conclusionLits;
669
    // whether conclusion is singleton
670
10105
    if (chainConclusionLitsSet.count(args[0]))
671
    {
672
902
      conclusionLits.push_back(args[0]);
673
    }
674
    else
675
    {
676
9203
      Assert(args[0].getKind() == kind::OR);
677
9203
      conclusionLits.insert(
678
18406
          conclusionLits.end(), args[0].begin(), args[0].end());
679
    }
680
    std::set<Node> conclusionLitsSet{conclusionLits.begin(),
681
20210
                                     conclusionLits.end()};
682
    // If the sets are different, there are "crowding" literals, i.e. literals
683
    // that were removed by implicit multi-usage of premises in the resolution
684
    // chain.
685
10105
    if (chainConclusionLitsSet != conclusionLitsSet)
686
    {
687
6996
      chainConclusion = eliminateCrowdingLits(
688
          chainConclusionLits, conclusionLits, children, args, cdp);
689
      // update vector of lits. Note that the set is no longer used, so we don't
690
      // need to update it
691
      //
692
      // We need again to check whether chainConclusion is a singleton
693
      // clause. As above, it's a singleton if it's in the original
694
      // chainConclusionLitsSet.
695
6996
      chainConclusionLits.clear();
696
6996
      if (chainConclusionLitsSet.count(chainConclusion))
697
      {
698
1
        chainConclusionLits.push_back(chainConclusion);
699
      }
700
      else
701
      {
702
6995
        Assert(chainConclusion.getKind() == kind::OR);
703
20985
        chainConclusionLits.insert(chainConclusionLits.end(),
704
                                   chainConclusion.begin(),
705
20985
                                   chainConclusion.end());
706
      }
707
    }
708
    else
709
    {
710
3109
      cdp->addStep(
711
          chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);
712
    }
713
20210
    Trace("smt-proof-pp-debug")
714
10105
        << "Conclusion after chain_res/elimCrowd: " << chainConclusion << "\n";
715
20210
    Trace("smt-proof-pp-debug")
716
10105
        << "Conclusion lits: " << chainConclusionLits << "\n";
717
    // Placeholder for running conclusion
718
20210
    Node n = chainConclusion;
719
    // factoring
720
10105
    if (chainConclusionLits.size() != conclusionLits.size())
721
    {
722
      // We build it rather than taking conclusionLits because the order may be
723
      // different
724
18618
      std::vector<Node> factoredLits;
725
18618
      std::unordered_set<TNode, TNodeHashFunction> clauseSet;
726
117547
      for (size_t i = 0, size = chainConclusionLits.size(); i < size; ++i)
727
      {
728
108238
        if (clauseSet.count(chainConclusionLits[i]))
729
        {
730
49575
          continue;
731
        }
732
58663
        factoredLits.push_back(n[i]);
733
58663
        clauseSet.insert(n[i]);
734
      }
735
9309
      Node factored = factoredLits.empty()
736
                          ? nm->mkConst(false)
737
9309
                          : factoredLits.size() == 1
738
901
                                ? factoredLits[0]
739
28828
                                : nm->mkNode(kind::OR, factoredLits);
740
9309
      cdp->addStep(factored, PfRule::FACTORING, {n}, {});
741
9309
      n = factored;
742
    }
743
    // either same node or n as a clause
744
10105
    Assert(n == args[0] || n.getKind() == kind::OR);
745
    // reordering
746
10105
    if (n != args[0])
747
    {
748
7010
      cdp->addStep(args[0], PfRule::REORDERING, {n}, {args[0]});
749
    }
750
10105
    return args[0];
751
  }
752
59263
  else if (id == PfRule::SUBS)
753
  {
754
6995
    NodeManager* nm = NodeManager::currentNM();
755
    // Notice that a naive way to reconstruct SUBS is to do a term conversion
756
    // proof for each substitution.
757
    // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
758
    //   TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
759
    // Notice that more optimal proofs are possible that do a single traversal
760
    // over t. This is done by applying later substitutions to the range of
761
    // previous substitutions, until a final simultaneous substitution is
762
    // applied to t.  For instance, in the above example, we first prove:
763
    //   CONG{g}( b = c )
764
    // by applying the second substitution { b -> c } to the range of the first,
765
    // giving us a proof of g(b)=g(c). We then construct the updated proof
766
    // by tranitivity:
767
    //   TRANS( a=g(b), CONG{g}( b=c ) )
768
    // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
769
    //   CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
770
    // which notice is more compact than the proof above.
771
13990
    Node t = args[0];
772
    // get the kind of substitution
773
6995
    MethodId ids = MethodId::SB_DEFAULT;
774
6995
    if (args.size() >= 2)
775
    {
776
4206
      builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
777
    }
778
13990
    std::vector<std::shared_ptr<CDProof>> pfs;
779
13990
    std::vector<TNode> vsList;
780
13990
    std::vector<TNode> ssList;
781
13990
    std::vector<TNode> fromList;
782
13990
    std::vector<ProofGenerator*> pgs;
783
    // first, compute the entire substitution
784
117408
    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
785
    {
786
      // get the substitution
787
220826
      builtin::BuiltinProofRuleChecker::getSubstitutionFor(
788
110413
          children[i], vsList, ssList, fromList, ids);
789
      // ensure proofs for each formula in fromList
790
110413
      if (children[i].getKind() == AND && ids == MethodId::SB_DEFAULT)
791
      {
792
        for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
793
             j++)
794
        {
795
          Node nodej = nm->mkConst(Rational(j));
796
          cdp->addStep(
797
              children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
798
        }
799
      }
800
    }
801
13990
    std::vector<Node> vvec;
802
13990
    std::vector<Node> svec;
803
117408
    for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
804
    {
805
      // Note we process in forward order, since later substitution should be
806
      // applied to earlier ones, and the last child of a SUBS is processed
807
      // first.
808
217636
      TNode var = vsList[i];
809
217636
      TNode subs = ssList[i];
810
217636
      TNode childFrom = fromList[i];
811
220826
      Trace("smt-proof-pp-debug")
812
110413
          << "...process " << var << " -> " << subs << " (" << childFrom << ", "
813
110413
          << ids << ")" << std::endl;
814
      // apply the current substitution to the range
815
110413
      if (!vvec.empty())
816
      {
817
        Node ss =
818
203646
            subs.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
819
103418
        if (ss != subs)
820
        {
821
6380
          Trace("smt-proof-pp-debug")
822
3190
              << "......updated to " << var << " -> " << ss
823
3190
              << " based on previous substitution" << std::endl;
824
          // make the proof for the tranitivity step
825
6380
          std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm);
826
3190
          pfs.push_back(pf);
827
          // prove the updated substitution
828
          TConvProofGenerator tcg(d_pnm,
829
                                  nullptr,
830
                                  TConvPolicy::ONCE,
831
                                  TConvCachePolicy::NEVER,
832
                                  "nested_SUBS_TConvProofGenerator",
833
                                  nullptr,
834
6380
                                  true);
835
          // add previous rewrite steps
836
552391
          for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
837
          {
838
            // substitutions are pre-rewrites
839
549201
            tcg.addRewriteStep(vvec[j], svec[j], pgs[j], true);
840
          }
841
          // get the proof for the update to the current substitution
842
6380
          Node seqss = subs.eqNode(ss);
843
6380
          std::shared_ptr<ProofNode> pfn = tcg.getProofFor(seqss);
844
3190
          Assert(pfn != nullptr);
845
          // add the proof
846
3190
          pf->addProof(pfn);
847
          // get proof for childFrom from cdp
848
3190
          pfn = cdp->getProofFor(childFrom);
849
3190
          pf->addProof(pfn);
850
          // ensure we have a proof of var = subs
851
6380
          Node veqs = addProofForSubsStep(var, subs, childFrom, pf.get());
852
          // transitivity
853
3190
          pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
854
          // add to the substitution
855
3190
          vvec.push_back(var);
856
3190
          svec.push_back(ss);
857
3190
          pgs.push_back(pf.get());
858
3190
          continue;
859
        }
860
      }
861
      // Just use equality from CDProof, but ensure we have a proof in cdp.
862
      // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
863
      // uses the assumption childFrom as a Boolean assignment (e.g.
864
      // childFrom = true if we are using MethodId::SB_LITERAL).
865
107223
      addProofForSubsStep(var, subs, childFrom, cdp);
866
107223
      vvec.push_back(var);
867
107223
      svec.push_back(subs);
868
107223
      pgs.push_back(cdp);
869
    }
870
13990
    Node ts = t.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
871
13990
    Node eq = t.eqNode(ts);
872
6995
    if (ts != t)
873
    {
874
      // should be implied by the substitution now
875
      TConvProofGenerator tcpg(d_pnm,
876
                               nullptr,
877
                               TConvPolicy::ONCE,
878
                               TConvCachePolicy::NEVER,
879
                               "SUBS_TConvProofGenerator",
880
                               nullptr,
881
13990
                               true);
882
117408
      for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
883
      {
884
        // substitutions are pre-rewrites
885
110413
        tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], true);
886
      }
887
      // add the proof constructed by the term conversion utility
888
13990
      std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq);
889
      // should give a proof, if not, then tcpg does not agree with the
890
      // substitution.
891
6995
      Assert(pfn != nullptr);
892
6995
      if (pfn == nullptr)
893
      {
894
        cdp->addStep(eq, PfRule::TRUST_SUBS, {}, {eq});
895
      }
896
      else
897
      {
898
6995
        cdp->addProof(pfn);
899
      }
900
    }
901
    else
902
    {
903
      // should not be necessary typically
904
      cdp->addStep(eq, PfRule::REFL, {}, {t});
905
    }
906
6995
    return eq;
907
  }
908
52268
  else if (id == PfRule::REWRITE)
909
  {
910
    // get the kind of rewrite
911
52268
    MethodId idr = MethodId::RW_REWRITE;
912
52268
    if (args.size() >= 2)
913
    {
914
6
      builtin::BuiltinProofRuleChecker::getMethodId(args[1], idr);
915
    }
916
    builtin::BuiltinProofRuleChecker* builtinPfC =
917
        static_cast<builtin::BuiltinProofRuleChecker*>(
918
52268
            d_pnm->getChecker()->getCheckerFor(PfRule::REWRITE));
919
104536
    Node ret = builtinPfC->applyRewrite(args[0], idr);
920
104536
    Node eq = args[0].eqNode(ret);
921
52268
    if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
922
    {
923
      // rewrites from theory::Rewriter
924
52268
      bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
925
      // use rewrite with proof interface
926
52268
      Rewriter* rr = d_smte->getRewriter();
927
104536
      TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
928
104536
      std::shared_ptr<ProofNode> pfn = trn.toProofNode();
929
52268
      if (pfn == nullptr)
930
      {
931
12
        Trace("smt-proof-pp-debug")
932
6
            << "Use TRUST_REWRITE for " << eq << std::endl;
933
        // did not have a proof of rewriting, probably isExtEq is true
934
6
        if (isExtEq)
935
        {
936
          // update to THEORY_REWRITE with idr
937
6
          Assert(args.size() >= 1);
938
6
          TheoryId theoryId = Theory::theoryOf(args[0].getType());
939
12
          Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
940
6
          cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]});
941
        }
942
        else
943
        {
944
          // this should never be applied
945
          cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
946
        }
947
      }
948
      else
949
      {
950
52262
        cdp->addProof(pfn);
951
      }
952
104536
      Assert(trn.getNode() == ret)
953
52268
          << "Unexpected rewrite " << args[0] << std::endl
954
52268
          << "Got: " << trn.getNode() << std::endl
955
52268
          << "Expected: " << ret;
956
    }
957
    else if (idr == MethodId::RW_EVALUATE)
958
    {
959
      // change to evaluate, which is never eliminated
960
      cdp->addStep(eq, PfRule::EVALUATE, {}, {args[0]});
961
    }
962
    else
963
    {
964
      // don't know how to eliminate
965
      return Node::null();
966
    }
967
52268
    if (args[0] == ret)
968
    {
969
      // should not be necessary typically
970
      cdp->addStep(eq, PfRule::REFL, {}, {args[0]});
971
    }
972
52268
    return eq;
973
  }
974
  else if (id == PfRule::THEORY_REWRITE)
975
  {
976
    Assert(!args.empty());
977
    Node eq = args[0];
978
    Assert(eq.getKind() == EQUAL);
979
    // try to replay theory rewrite
980
    // first, check that maybe its just an evaluation step
981
    ProofChecker* pc = d_pnm->getChecker();
982
    Node ceval =
983
        pc->checkDebug(PfRule::EVALUATE, {}, {eq[0]}, eq, "smt-proof-pp-debug");
984
    if (!ceval.isNull() && ceval == eq)
985
    {
986
      cdp->addStep(eq, PfRule::EVALUATE, {}, {eq[0]});
987
      return eq;
988
    }
989
    // otherwise no update
990
    Trace("final-pf-hole") << "hole: " << id << " : " << eq << std::endl;
991
  }
992
993
  // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
994
995
  return Node::null();
996
}
997
998
13773
Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp)
999
{
1000
27546
  Node tw = SkolemManager::getOriginalForm(t);
1001
13773
  Node eq = t.eqNode(tw);
1002
13773
  if (t == tw)
1003
  {
1004
    // not necessary, add REFL step
1005
7146
    cdp->addStep(eq, PfRule::REFL, {}, {t});
1006
7146
    return eq;
1007
  }
1008
13254
  std::shared_ptr<ProofNode> pn = d_wfpm.getProofFor(eq);
1009
6627
  if (pn != nullptr)
1010
  {
1011
    // add the proof
1012
6627
    cdp->addProof(pn);
1013
  }
1014
  else
1015
  {
1016
    Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
1017
                     "to add proof for witness form of "
1018
                  << t;
1019
  }
1020
6627
  return eq;
1021
}
1022
1023
117550
Node ProofPostprocessCallback::addProofForTrans(
1024
    const std::vector<Node>& tchildren, CDProof* cdp)
1025
{
1026
117550
  size_t tsize = tchildren.size();
1027
117550
  if (tsize > 1)
1028
  {
1029
28150
    Node lhs = tchildren[0][0];
1030
28150
    Node rhs = tchildren[tsize - 1][1];
1031
28150
    Node eq = lhs.eqNode(rhs);
1032
14075
    cdp->addStep(eq, PfRule::TRANS, tchildren, {});
1033
14075
    return eq;
1034
  }
1035
103475
  else if (tsize == 1)
1036
  {
1037
92557
    return tchildren[0];
1038
  }
1039
10918
  return Node::null();
1040
}
1041
1042
110413
Node ProofPostprocessCallback::addProofForSubsStep(Node var,
1043
                                                   Node subs,
1044
                                                   Node assump,
1045
                                                   CDProof* cdp)
1046
{
1047
  // ensure we have a proof of var = subs
1048
110413
  Node veqs = var.eqNode(subs);
1049
110413
  if (veqs != assump)
1050
  {
1051
    // should be true intro or false intro
1052
4206
    Assert(subs.isConst());
1053
12618
    cdp->addStep(
1054
        veqs,
1055
4206
        subs.getConst<bool>() ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO,
1056
        {assump},
1057
4206
        {});
1058
  }
1059
110413
  return veqs;
1060
}
1061
1062
101174
bool ProofPostprocessCallback::addToTransChildren(Node eq,
1063
                                                  std::vector<Node>& tchildren,
1064
                                                  bool isSymm)
1065
{
1066
101174
  Assert(!eq.isNull());
1067
101174
  Assert(eq.getKind() == kind::EQUAL);
1068
101174
  if (eq[0] == eq[1])
1069
  {
1070
36977
    return false;
1071
  }
1072
128394
  Node equ = isSymm ? eq[1].eqNode(eq[0]) : eq;
1073
64197
  Assert(tchildren.empty()
1074
         || (tchildren[tchildren.size() - 1].getKind() == kind::EQUAL
1075
             && tchildren[tchildren.size() - 1][1] == equ[0]));
1076
64197
  tchildren.push_back(equ);
1077
64197
  return true;
1078
}
1079
1080
962
ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
1081
962
    ProofNodeManager* pnm)
1082
    : d_ruleCount("finalProof::ruleCount"),
1083
      d_totalRuleCount("finalProof::totalRuleCount", 0),
1084
      d_minPedanticLevel("finalProof::minPedanticLevel", 10),
1085
      d_numFinalProofs("finalProofs::numFinalProofs", 0),
1086
      d_pnm(pnm),
1087
962
      d_pedanticFailure(false)
1088
{
1089
962
  smtStatisticsRegistry()->registerStat(&d_ruleCount);
1090
962
  smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
1091
962
  smtStatisticsRegistry()->registerStat(&d_minPedanticLevel);
1092
962
  smtStatisticsRegistry()->registerStat(&d_numFinalProofs);
1093
962
}
1094
1095
1924
ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
1096
{
1097
962
  smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
1098
962
  smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
1099
962
  smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel);
1100
962
  smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs);
1101
962
}
1102
1103
1146
void ProofPostprocessFinalCallback::initializeUpdate()
1104
{
1105
1146
  d_pedanticFailure = false;
1106
1146
  d_pedanticFailureOut.str("");
1107
1146
  ++d_numFinalProofs;
1108
1146
}
1109
1110
1815596
bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
1111
                                                 bool& continueUpdate)
1112
{
1113
1815596
  PfRule r = pn->getRule();
1114
  // if not doing eager pedantic checking, fail if below threshold
1115
1815596
  if (!options::proofEagerChecking())
1116
  {
1117
1815596
    if (!d_pedanticFailure)
1118
    {
1119
1815596
      Assert(d_pedanticFailureOut.str().empty());
1120
1815596
      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
1121
      {
1122
        d_pedanticFailure = true;
1123
      }
1124
    }
1125
  }
1126
1815596
  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
1127
1815596
  if (plevel != 0)
1128
  {
1129
6612
    d_minPedanticLevel.minAssign(plevel);
1130
  }
1131
  // record stats for the rule
1132
1815596
  d_ruleCount << r;
1133
1815596
  ++d_totalRuleCount;
1134
1815596
  return false;
1135
}
1136
1137
1146
bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
1138
{
1139
1146
  if (d_pedanticFailure)
1140
  {
1141
    out << d_pedanticFailureOut.str();
1142
    return true;
1143
  }
1144
1146
  return false;
1145
}
1146
1147
962
ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
1148
                                     SmtEngine* smte,
1149
962
                                     ProofGenerator* pppg)
1150
    : d_pnm(pnm),
1151
      d_cb(pnm, smte, pppg),
1152
      // the update merges subproofs
1153
      d_updater(d_pnm, d_cb, true),
1154
      d_finalCb(pnm),
1155
962
      d_finalizer(d_pnm, d_finalCb)
1156
{
1157
962
}
1158
1159
962
ProofPostproccess::~ProofPostproccess() {}
1160
1161
1146
void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
1162
{
1163
  // Initialize the callback, which computes necessary static information about
1164
  // how to process, including how to process assumptions in pf.
1165
1146
  d_cb.initializeUpdate();
1166
  // now, process
1167
1146
  d_updater.process(pf);
1168
  // take stats and check pedantic
1169
1146
  d_finalCb.initializeUpdate();
1170
1146
  d_finalizer.process(pf);
1171
1172
2292
  std::stringstream serr;
1173
1146
  bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr);
1174
1146
  if (wasPedanticFailure)
1175
  {
1176
    AlwaysAssert(!wasPedanticFailure)
1177
        << "ProofPostproccess::process: pedantic failure:" << std::endl
1178
        << serr.str();
1179
  }
1180
1146
}
1181
1182
6734
void ProofPostproccess::setEliminateRule(PfRule rule)
1183
{
1184
6734
  d_cb.setEliminateRule(rule);
1185
6734
}
1186
1187
}  // namespace smt
1188
26676
}  // namespace CVC4