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