src/smt/proof_post_processor.cpp

   1 /*********************                                                        */
   2 /*! \file proof_post_processor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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/skolem_manager.h"
  18 #include "options/smt_options.h"
  19 #include "preprocessing/assertion_pipeline.h"
  20 #include "smt/smt_engine.h"
  21 #include "smt/smt_statistics_registry.h"
  22 #include "theory/builtin/proof_checker.h"
  23 #include "theory/rewriter.h"
  24
  25 using namespace CVC4::kind;
  26 using namespace CVC4::theory;
  27
  28 namespace CVC4 {
  29 namespace smt {
  30
  31 ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm,
  32                                                    SmtEngine* smte,
  33                                                    ProofGenerator* pppg)
  34     : d_pnm(pnm), d_smte(smte), d_pppg(pppg), d_wfpm(pnm)
  35 {
  36   d_true = NodeManager::currentNM()->mkConst(true);
  37   // always check whether to update ASSUME
  38   d_elimRules.insert(PfRule::ASSUME);
  39 }
  40
  41 void ProofPostprocessCallback::initializeUpdate()
  42 {
  43   d_assumpToProof.clear();
  44   d_wfAssumptions.clear();
  45 }
  46
  47 void ProofPostprocessCallback::setEliminateRule(PfRule rule)
  48 {
  49   d_elimRules.insert(rule);
  50 }
  51
  52 bool ProofPostprocessCallback::shouldUpdate(ProofNode* pn)
  53 {
  54   return d_elimRules.find(pn->getRule()) != d_elimRules.end();
  55 }
  56
  57 bool ProofPostprocessCallback::update(Node res,
  58                                       PfRule id,
  59                                       const std::vector<Node>& children,
  60                                       const std::vector<Node>& args,
  61                                       CDProof* cdp,
  62                                       bool& continueUpdate)
  63 {
  64   Trace("smt-proof-pp-debug") << "- Post process " << id << " " << children
  65                               << " / " << args << std::endl;
  66
  67   if (id == PfRule::ASSUME)
  68   {
  69     // we cache based on the assumption node, not the proof node, since there
  70     // may be multiple occurrences of the same node.
  71     Node f = args[0];
  72     std::shared_ptr<ProofNode> pfn;
  73     std::map<Node, std::shared_ptr<ProofNode>>::iterator it =
  74         d_assumpToProof.find(f);
  75     if (it != d_assumpToProof.end())
  76     {
  77       Trace("smt-proof-pp-debug") << "...already computed" << std::endl;
  78       pfn = it->second;
  79     }
  80     else
  81     {
  82       Assert(d_pppg != nullptr);
  83       // get proof from preprocess proof generator
  84       pfn = d_pppg->getProofFor(f);
  85       // print for debugging
  86       if (pfn == nullptr)
  87       {
  88         Trace("smt-proof-pp-debug")
  89             << "...no proof, possibly an input assumption" << std::endl;
  90       }
  91       else
  92       {
  93         Assert(pfn->getResult() == f);
  94         if (Trace.isOn("smt-proof-pp"))
  95         {
  96           Trace("smt-proof-pp")
  97               << "=== Connect proof for preprocessing: " << f << std::endl;
  98           Trace("smt-proof-pp") << *pfn.get() << std::endl;
  99         }
 100       }
 101       d_assumpToProof[f] = pfn;
 102     }
 103     if (pfn == nullptr)
 104     {
 105       // no update
 106       return false;
 107     }
 108     // connect the proof
 109     cdp->addProof(pfn);
 110     return true;
 111   }
 112   Node ret = expandMacros(id, children, args, cdp);
 113   Trace("smt-proof-pp-debug") << "...expanded = " << !ret.isNull() << std::endl;
 114   return !ret.isNull();
 115 }
 116
 117 bool ProofPostprocessCallback::updateInternal(Node res,
 118                                               PfRule id,
 119                                               const std::vector<Node>& children,
 120                                               const std::vector<Node>& args,
 121                                               CDProof* cdp)
 122 {
 123   bool continueUpdate = true;
 124   return update(res, id, children, args, cdp, continueUpdate);
 125 }
 126
 127 Node ProofPostprocessCallback::expandMacros(PfRule id,
 128                                             const std::vector<Node>& children,
 129                                             const std::vector<Node>& args,
 130                                             CDProof* cdp)
 131 {
 132   if (d_elimRules.find(id) == d_elimRules.end())
 133   {
 134     // not eliminated
 135     return Node::null();
 136   }
 137   // macro elimination
 138   if (id == PfRule::MACRO_SR_EQ_INTRO)
 139   {
 140     // (TRANS
 141     //   (SUBS <children> :args args[0:1])
 142     //   (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))
 143     std::vector<Node> tchildren;
 144     Node t = args[0];
 145     Node ts;
 146     if (!children.empty())
 147     {
 148       std::vector<Node> sargs;
 149       sargs.push_back(t);
 150       MethodId sid = MethodId::SB_DEFAULT;
 151       if (args.size() >= 2)
 152       {
 153         if (builtin::BuiltinProofRuleChecker::getMethodId(args[1], sid))
 154         {
 155           sargs.push_back(args[1]);
 156         }
 157       }
 158       ts =
 159           builtin::BuiltinProofRuleChecker::applySubstitution(t, children, sid);
 160       if (ts != t)
 161       {
 162         Node eq = t.eqNode(ts);
 163         // apply SUBS proof rule if necessary
 164         if (!updateInternal(eq, PfRule::SUBS, children, sargs, cdp))
 165         {
 166           // if not elimianted, add as step
 167           cdp->addStep(eq, PfRule::SUBS, children, sargs);
 168         }
 169         tchildren.push_back(eq);
 170       }
 171     }
 172     else
 173     {
 174       // no substitute
 175       ts = t;
 176     }
 177     std::vector<Node> rargs;
 178     rargs.push_back(ts);
 179     MethodId rid = MethodId::RW_REWRITE;
 180     if (args.size() >= 3)
 181     {
 182       if (builtin::BuiltinProofRuleChecker::getMethodId(args[2], rid))
 183       {
 184         rargs.push_back(args[2]);
 185       }
 186     }
 187     builtin::BuiltinProofRuleChecker* builtinPfC =
 188         static_cast<builtin::BuiltinProofRuleChecker*>(
 189             d_pnm->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO));
 190     Node tr = builtinPfC->applyRewrite(ts, rid);
 191     if (ts != tr)
 192     {
 193       Node eq = ts.eqNode(tr);
 194       // apply REWRITE proof rule
 195       if (!updateInternal(eq, PfRule::REWRITE, {}, rargs, cdp))
 196       {
 197         // if not elimianted, add as step
 198         cdp->addStep(eq, PfRule::REWRITE, {}, rargs);
 199       }
 200       tchildren.push_back(eq);
 201     }
 202     if (t == tr)
 203     {
 204       // typically not necessary, but done to be robust
 205       cdp->addStep(t.eqNode(tr), PfRule::REFL, {}, {t});
 206       return t.eqNode(tr);
 207     }
 208     // must add TRANS if two step
 209     return addProofForTrans(tchildren, cdp);
 210   }
 211   else if (id == PfRule::MACRO_SR_PRED_INTRO)
 212   {
 213     std::vector<Node> tchildren;
 214     std::vector<Node> sargs = args;
 215     // take into account witness form, if necessary
 216     if (d_wfpm.requiresWitnessFormIntro(args[0]))
 217     {
 218       Node weq = addProofForWitnessForm(args[0], cdp);
 219       tchildren.push_back(weq);
 220       // replace the first argument
 221       sargs[0] = weq[1];
 222     }
 223     // (TRUE_ELIM
 224     // (TRANS
 225     //    ... proof of t = toWitness(t) ...
 226     //    (MACRO_SR_EQ_INTRO <children> :args (toWitness(t) args[1:]))))
 227     // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice
 228     // that this rule application is immediately expanded in the recursive
 229     // call and not added to the proof.
 230     Node conc = expandMacros(PfRule::MACRO_SR_EQ_INTRO, children, sargs, cdp);
 231     tchildren.push_back(conc);
 232     Assert(!conc.isNull() && conc.getKind() == EQUAL && conc[0] == sargs[0]
 233            && conc[1] == d_true);
 234     // transitivity if necessary
 235     Node eq = addProofForTrans(tchildren, cdp);
 236
 237     cdp->addStep(eq[0], PfRule::TRUE_ELIM, {eq}, {});
 238     Assert(eq[0] == args[0]);
 239     return eq[0];
 240   }
 241   else if (id == PfRule::MACRO_SR_PRED_ELIM)
 242   {
 243     // (TRUE_ELIM
 244     //   (TRANS
 245     //     (SYMM (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))
 246     //     (TRUE_INTRO children[0])))
 247     std::vector<Node> schildren(children.begin() + 1, children.end());
 248     std::vector<Node> srargs;
 249     srargs.push_back(children[0]);
 250     srargs.insert(srargs.end(), args.begin(), args.end());
 251     Node conc = expandMacros(PfRule::MACRO_SR_EQ_INTRO, schildren, srargs, cdp);
 252     Assert(!conc.isNull() && conc.getKind() == EQUAL && conc[0] == children[0]);
 253
 254     Node eq1 = children[0].eqNode(d_true);
 255     cdp->addStep(eq1, PfRule::TRUE_INTRO, {children[0]}, {});
 256
 257     Node concSym = conc[1].eqNode(conc[0]);
 258     Node eq2 = conc[1].eqNode(d_true);
 259     cdp->addStep(eq2, PfRule::TRANS, {concSym, eq1}, {});
 260
 261     cdp->addStep(conc[1], PfRule::TRUE_ELIM, {eq2}, {});
 262     return conc[1];
 263   }
 264   else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
 265   {
 266     // (TRUE_ELIM
 267     // (TRANS
 268     //    (MACRO_SR_EQ_INTRO children[1:] :args <args>)
 269     //    ... proof of a = wa
 270     //    (MACRO_SR_EQ_INTRO {} wa)
 271     //    (SYMM
 272     //      (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))
 273     //      ... proof of c = wc
 274     //      (MACRO_SR_EQ_INTRO {} wc))
 275     //    (TRUE_INTRO children[0])))
 276     // where
 277     // wa = toWitness(apply_SR(args[0])) and
 278     // wc = toWitness(apply_SR(children[0])).
 279     Trace("smt-proof-pp-debug")
 280         << "Transform " << children[0] << " == " << args[0] << std::endl;
 281     if (CDProof::isSame(children[0], args[0]))
 282     {
 283       // nothing to do
 284       return children[0];
 285     }
 286     std::vector<Node> tchildren;
 287     std::vector<Node> schildren(children.begin() + 1, children.end());
 288     std::vector<Node> sargs = args;
 289     // first, compute if we need
 290     bool reqWitness = d_wfpm.requiresWitnessFormTransform(children[0], args[0]);
 291     // convert both sides, in three steps, take symmetry of second chain
 292     for (unsigned r = 0; r < 2; r++)
 293     {
 294       std::vector<Node> tchildrenr;
 295       // first rewrite args[0], then children[0]
 296       sargs[0] = r == 0 ? args[0] : children[0];
 297       // t = apply_SR(t)
 298       Node eq = expandMacros(PfRule::MACRO_SR_EQ_INTRO, schildren, sargs, cdp);
 299       Trace("smt-proof-pp-debug")
 300           << "transform subs_rewrite (" << r << "): " << eq << std::endl;
 301       Assert(!eq.isNull() && eq.getKind() == EQUAL && eq[0] == sargs[0]);
 302       addToTransChildren(eq, tchildrenr);
 303       // apply_SR(t) = toWitness(apply_SR(t))
 304       if (reqWitness)
 305       {
 306         Node weq = addProofForWitnessForm(eq[1], cdp);
 307         Trace("smt-proof-pp-debug")
 308             << "transform toWitness (" << r << "): " << weq << std::endl;
 309         if (addToTransChildren(weq, tchildrenr))
 310         {
 311           sargs[0] = weq[1];
 312           // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))
 313           // rewrite again, don't need substitution
 314           Node weqr = expandMacros(PfRule::MACRO_SR_EQ_INTRO, {}, sargs, cdp);
 315           Trace("smt-proof-pp-debug") << "transform rewrite_witness (" << r
 316                                       << "): " << weqr << std::endl;
 317           addToTransChildren(weqr, tchildrenr);
 318         }
 319       }
 320       Trace("smt-proof-pp-debug")
 321           << "transform connect (" << r << ")" << std::endl;
 322       // add to overall chain
 323       if (r == 0)
 324       {
 325         // add the current chain to the overall chain
 326         tchildren.insert(tchildren.end(), tchildrenr.begin(), tchildrenr.end());
 327       }
 328       else
 329       {
 330         // add the current chain to cdp
 331         Node eqr = addProofForTrans(tchildrenr, cdp);
 332         if (!eqr.isNull())
 333         {
 334           // take symmetry of above and add it to the overall chain
 335           addToTransChildren(eqr, tchildren, true);
 336         }
 337       }
 338       Trace("smt-proof-pp-debug")
 339           << "transform finish (" << r << ")" << std::endl;
 340     }
 341
 342     // children[0] = true
 343     Node eq3 = children[0].eqNode(d_true);
 344     Trace("smt-proof-pp-debug") << "transform true_intro: " << eq3 << std::endl;
 345     cdp->addStep(eq3, PfRule::TRUE_INTRO, {children[0]}, {});
 346     addToTransChildren(eq3, tchildren);
 347
 348     // apply transitivity if necessary
 349     Node eq = addProofForTrans(tchildren, cdp);
 350
 351     cdp->addStep(args[0], PfRule::TRUE_ELIM, {eq}, {});
 352     return args[0];
 353   }
 354   else if (id == PfRule::SUBS)
 355   {
 356     // Notice that a naive way to reconstruct SUBS is to do a term conversion
 357     // proof for each substitution.
 358     // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
 359     //   TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
 360     // Notice that more optimal proofs are possible that do a single traversal
 361     // over t. This is done by applying later substitutions to the range of
 362     // previous substitutions, until a final simultaneous substitution is
 363     // applied to t.  For instance, in the above example, we first prove:
 364     //   CONG{g}( b = c )
 365     // by applying the second substitution { b -> c } to the range of the first,
 366     // giving us a proof of g(b)=g(c). We then construct the updated proof
 367     // by tranitivity:
 368     //   TRANS( a=g(b), CONG{g}( b=c ) )
 369     // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
 370     //   CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
 371     // which notice is more compact than the proof above.
 372     Node t = args[0];
 373     // get the kind of substitution
 374     MethodId ids = MethodId::SB_DEFAULT;
 375     if (args.size() >= 2)
 376     {
 377       builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
 378     }
 379     std::vector<std::shared_ptr<CDProof>> pfs;
 380     std::vector<Node> vvec;
 381     std::vector<Node> svec;
 382     std::vector<ProofGenerator*> pgs;
 383     for (size_t i = 0, nchild = children.size(); i < nchild; i++)
 384     {
 385       // process in reverse order
 386       size_t index = nchild - (i + 1);
 387       // get the substitution
 388       TNode var, subs;
 389       builtin::BuiltinProofRuleChecker::getSubstitution(
 390           children[index], var, subs, ids);
 391       // apply the current substitution to the range
 392       if (!vvec.empty())
 393       {
 394         Node ss =
 395             subs.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
 396         if (ss != subs)
 397         {
 398           // make the proof for the tranitivity step
 399           std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm);
 400           pfs.push_back(pf);
 401           // prove the updated substitution
 402           TConvProofGenerator tcg(d_pnm, nullptr, TConvPolicy::ONCE);
 403           // add previous rewrite steps
 404           for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
 405           {
 406             tcg.addRewriteStep(vvec[j], svec[j], pgs[j]);
 407           }
 408           // get the proof for the update to the current substitution
 409           Node seqss = subs.eqNode(ss);
 410           std::shared_ptr<ProofNode> pfn = tcg.getProofFor(seqss);
 411           Assert(pfn != nullptr);
 412           // add the proof
 413           pf->addProof(pfn);
 414           // get proof for children[i] from cdp
 415           pfn = cdp->getProofFor(children[i]);
 416           pf->addProof(pfn);
 417           // ensure we have a proof of var = subs
 418           Node veqs = addProofForSubsStep(var, subs, children[index], pf.get());
 419           // transitivity
 420           pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
 421           // add to the substitution
 422           vvec.push_back(var);
 423           svec.push_back(ss);
 424           pgs.push_back(pf.get());
 425           continue;
 426         }
 427       }
 428       // Just use equality from CDProof, but ensure we have a proof in cdp.
 429       // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
 430       // uses the assumption children[index] as a Boolean assignment (e.g.
 431       // children[index] = true if we are using MethodId::SB_LITERAL).
 432       addProofForSubsStep(var, subs, children[index], cdp);
 433       vvec.push_back(var);
 434       svec.push_back(subs);
 435       pgs.push_back(cdp);
 436     }
 437     Node ts = t.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
 438     Node eq = t.eqNode(ts);
 439     if (ts != t)
 440     {
 441       // should be implied by the substitution now
 442       TConvProofGenerator tcpg(d_pnm, nullptr, TConvPolicy::ONCE);
 443       for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
 444       {
 445         tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]);
 446       }
 447       // add the proof constructed by the term conversion utility
 448       std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq);
 449       // should give a proof, if not, then tcpg does not agree with the
 450       // substitution.
 451       Assert(pfn != nullptr);
 452       if (pfn != nullptr)
 453       {
 454         cdp->addProof(pfn);
 455       }
 456     }
 457     else
 458     {
 459       // should not be necessary typically
 460       cdp->addStep(eq, PfRule::REFL, {}, {t});
 461     }
 462     return eq;
 463   }
 464   else if (id == PfRule::REWRITE)
 465   {
 466     // get the kind of rewrite
 467     MethodId idr = MethodId::RW_REWRITE;
 468     if (args.size() >= 2)
 469     {
 470       builtin::BuiltinProofRuleChecker::getMethodId(args[1], idr);
 471     }
 472     builtin::BuiltinProofRuleChecker* builtinPfC =
 473         static_cast<builtin::BuiltinProofRuleChecker*>(
 474             d_pnm->getChecker()->getCheckerFor(PfRule::REWRITE));
 475     Node ret = builtinPfC->applyRewrite(args[0], idr);
 476     Node eq = args[0].eqNode(ret);
 477     if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
 478     {
 479       // rewrites from theory::Rewriter
 480       // automatically expand THEORY_REWRITE as well here if set
 481       bool elimTR =
 482           (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end());
 483       bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
 484       // use rewrite with proof interface
 485       Rewriter* rr = d_smte->getRewriter();
 486       TrustNode trn = rr->rewriteWithProof(args[0], elimTR, isExtEq);
 487       std::shared_ptr<ProofNode> pfn =
 488           trn.getGenerator()->getProofFor(trn.getProven());
 489       cdp->addProof(pfn);
 490       Assert(trn.getNode() == ret);
 491     }
 492     else if (idr == MethodId::RW_EVALUATE)
 493     {
 494       // change to evaluate, which is never eliminated
 495       cdp->addStep(eq, PfRule::EVALUATE, {}, {args[0]});
 496     }
 497     else
 498     {
 499       // don't know how to eliminate
 500       return Node::null();
 501     }
 502     if (args[0] == ret)
 503     {
 504       // should not be necessary typically
 505       cdp->addStep(eq, PfRule::REFL, {}, {args[0]});
 506     }
 507     return eq;
 508   }
 509
 510   // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
 511
 512   return Node::null();
 513 }
 514
 515 Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp)
 516 {
 517   Node tw = SkolemManager::getWitnessForm(t);
 518   Node eq = t.eqNode(tw);
 519   if (t == tw)
 520   {
 521     // not necessary, add REFL step
 522     cdp->addStep(eq, PfRule::REFL, {}, {t});
 523     return eq;
 524   }
 525   std::shared_ptr<ProofNode> pn = d_wfpm.getProofFor(eq);
 526   if (pn != nullptr)
 527   {
 528     // add the proof
 529     cdp->addProof(pn);
 530   }
 531   else
 532   {
 533     Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
 534                      "to add proof for witness form of "
 535                   << t;
 536   }
 537   return eq;
 538 }
 539
 540 Node ProofPostprocessCallback::addProofForTrans(
 541     const std::vector<Node>& tchildren, CDProof* cdp)
 542 {
 543   size_t tsize = tchildren.size();
 544   if (tsize > 1)
 545   {
 546     Node lhs = tchildren[0][0];
 547     Node rhs = tchildren[tsize - 1][1];
 548     Node eq = lhs.eqNode(rhs);
 549     cdp->addStep(eq, PfRule::TRANS, tchildren, {});
 550     return eq;
 551   }
 552   else if (tsize == 1)
 553   {
 554     return tchildren[0];
 555   }
 556   return Node::null();
 557 }
 558
 559 Node ProofPostprocessCallback::addProofForSubsStep(Node var,
 560                                                    Node subs,
 561                                                    Node assump,
 562                                                    CDProof* cdp)
 563 {
 564   // ensure we have a proof of var = subs
 565   Node veqs = var.eqNode(subs);
 566   if (veqs != assump)
 567   {
 568     // should be true intro or false intro
 569     Assert(subs.isConst());
 570     cdp->addStep(
 571         veqs,
 572         subs.getConst<bool>() ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO,
 573         {assump},
 574         {});
 575   }
 576   return veqs;
 577 }
 578
 579 bool ProofPostprocessCallback::addToTransChildren(Node eq,
 580                                                   std::vector<Node>& tchildren,
 581                                                   bool isSymm)
 582 {
 583   Assert(!eq.isNull());
 584   Assert(eq.getKind() == kind::EQUAL);
 585   if (eq[0] == eq[1])
 586   {
 587     return false;
 588   }
 589   Node equ = isSymm ? eq[1].eqNode(eq[0]) : eq;
 590   Assert(tchildren.empty()
 591          || (tchildren[tchildren.size() - 1].getKind() == kind::EQUAL
 592              && tchildren[tchildren.size() - 1][1] == equ[0]));
 593   tchildren.push_back(equ);
 594   return true;
 595 }
 596
 597 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
 598     ProofNodeManager* pnm)
 599     : d_ruleCount("finalProof::ruleCount"),
 600       d_totalRuleCount("finalProof::totalRuleCount", 0),
 601       d_pnm(pnm),
 602       d_pedanticFailure(false)
 603 {
 604   smtStatisticsRegistry()->registerStat(&d_ruleCount);
 605   smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
 606 }
 607
 608 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
 609 {
 610   smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
 611   smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
 612 }
 613
 614 void ProofPostprocessFinalCallback::initializeUpdate()
 615 {
 616   d_pedanticFailure = false;
 617   d_pedanticFailureOut.str("");
 618 }
 619
 620 bool ProofPostprocessFinalCallback::shouldUpdate(ProofNode* pn)
 621 {
 622   PfRule r = pn->getRule();
 623   if (Trace.isOn("final-pf-hole"))
 624   {
 625     if (r == PfRule::THEORY_REWRITE)
 626     {
 627       Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult()
 628                             << std::endl;
 629     }
 630   }
 631   // if not doing eager pedantic checking, fail if below threshold
 632   if (!options::proofNewPedanticEager())
 633   {
 634     if (!d_pedanticFailure)
 635     {
 636       Assert(d_pedanticFailureOut.str().empty());
 637       if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
 638       {
 639         d_pedanticFailure = true;
 640       }
 641     }
 642   }
 643   // record stats for the rule
 644   d_ruleCount << r;
 645   ++d_totalRuleCount;
 646   return false;
 647 }
 648
 649 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
 650 {
 651   if (d_pedanticFailure)
 652   {
 653     out << d_pedanticFailureOut.str();
 654     return true;
 655   }
 656   return false;
 657 }
 658
 659 ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
 660                                      SmtEngine* smte,
 661                                      ProofGenerator* pppg)
 662     : d_cb(pnm, smte, pppg), d_finalCb(pnm), d_pnm(pnm)
 663 {
 664 }
 665
 666 ProofPostproccess::~ProofPostproccess() {}
 667
 668 void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
 669 {
 670   // Initialize the callback, which computes necessary static information about
 671   // how to process, including how to process assumptions in pf.
 672   d_cb.initializeUpdate();
 673   // now, process
 674   ProofNodeUpdater updater(d_pnm, d_cb);
 675   updater.process(pf);
 676   // take stats and check pedantic
 677   d_finalCb.initializeUpdate();
 678   ProofNodeUpdater finalizer(d_pnm, d_finalCb);
 679   finalizer.process(pf);
 680
 681   std::stringstream serr;
 682   bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr);
 683   if (wasPedanticFailure)
 684   {
 685     AlwaysAssert(!wasPedanticFailure)
 686         << "ProofPostproccess::process: pedantic failure:" << std::endl
 687         << serr.str();
 688   }
 689 }
 690
 691 void ProofPostproccess::setEliminateRule(PfRule rule)
 692 {
 693   d_cb.setEliminateRule(rule);
 694 }
 695
 696 }  // namespace smt
 697 }  // namespace CVC4