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