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     NodeManager* nm = NodeManager::currentNM();
 380     // Notice that a naive way to reconstruct SUBS is to do a term conversion
 381     // proof for each substitution.
 382     // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:
 383     //   TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )
 384     // Notice that more optimal proofs are possible that do a single traversal
 385     // over t. This is done by applying later substitutions to the range of
 386     // previous substitutions, until a final simultaneous substitution is
 387     // applied to t.  For instance, in the above example, we first prove:
 388     //   CONG{g}( b = c )
 389     // by applying the second substitution { b -> c } to the range of the first,
 390     // giving us a proof of g(b)=g(c). We then construct the updated proof
 391     // by tranitivity:
 392     //   TRANS( a=g(b), CONG{g}( b=c ) )
 393     // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:
 394     //   CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )
 395     // which notice is more compact than the proof above.
 396     Node t = args[0];
 397     // get the kind of substitution
 398     MethodId ids = MethodId::SB_DEFAULT;
 399     if (args.size() >= 2)
 400     {
 401       builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
 402     }
 403     std::vector<std::shared_ptr<CDProof>> pfs;
 404     std::vector<TNode> vsList;
 405     std::vector<TNode> ssList;
 406     std::vector<TNode> fromList;
 407     std::vector<ProofGenerator*> pgs;
 408     // first, compute the entire substitution
 409     for (size_t i = 0, nchild = children.size(); i < nchild; i++)
 410     {
 411       // get the substitution
 412       builtin::BuiltinProofRuleChecker::getSubstitutionFor(
 413           children[i], vsList, ssList, fromList, ids);
 414       // ensure proofs for each formula in fromList
 415       if (children[i].getKind() == AND && ids == MethodId::SB_DEFAULT)
 416       {
 417         for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
 418              j++)
 419         {
 420           Node nodej = nm->mkConst(Rational(j));
 421           cdp->addStep(
 422               children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
 423         }
 424       }
 425     }
 426     std::vector<Node> vvec;
 427     std::vector<Node> svec;
 428     for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
 429     {
 430       // Note we process in forward order, since later substitution should be
 431       // applied to earlier ones, and the last child of a SUBS is processed
 432       // first.
 433       TNode var = vsList[i];
 434       TNode subs = ssList[i];
 435       TNode childFrom = fromList[i];
 436       Trace("smt-proof-pp-debug")
 437           << "...process " << var << " -> " << subs << " (" << childFrom << ", "
 438           << ids << ")" << std::endl;
 439       // apply the current substitution to the range
 440       if (!vvec.empty())
 441       {
 442         Node ss =
 443             subs.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
 444         if (ss != subs)
 445         {
 446           Trace("smt-proof-pp-debug")
 447               << "......updated to " << var << " -> " << ss
 448               << " based on previous substitution" << std::endl;
 449           // make the proof for the tranitivity step
 450           std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm);
 451           pfs.push_back(pf);
 452           // prove the updated substitution
 453           TConvProofGenerator tcg(d_pnm,
 454                                   nullptr,
 455                                   TConvPolicy::ONCE,
 456                                   TConvCachePolicy::NEVER,
 457                                   "nested_SUBS_TConvProofGenerator",
 458                                   nullptr,
 459                                   true);
 460           // add previous rewrite steps
 461           for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
 462           {
 463             // not necessarily closed, so we pass false to addRewriteStep.
 464             tcg.addRewriteStep(vvec[j], svec[j], pgs[j], false);
 465           }
 466           // get the proof for the update to the current substitution
 467           Node seqss = subs.eqNode(ss);
 468           std::shared_ptr<ProofNode> pfn = tcg.getProofFor(seqss);
 469           Assert(pfn != nullptr);
 470           // add the proof
 471           pf->addProof(pfn);
 472           // get proof for childFrom from cdp
 473           pfn = cdp->getProofFor(childFrom);
 474           pf->addProof(pfn);
 475           // ensure we have a proof of var = subs
 476           Node veqs = addProofForSubsStep(var, subs, childFrom, pf.get());
 477           // transitivity
 478           pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
 479           // add to the substitution
 480           vvec.push_back(var);
 481           svec.push_back(ss);
 482           pgs.push_back(pf.get());
 483           continue;
 484         }
 485       }
 486       // Just use equality from CDProof, but ensure we have a proof in cdp.
 487       // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
 488       // uses the assumption childFrom as a Boolean assignment (e.g.
 489       // childFrom = true if we are using MethodId::SB_LITERAL).
 490       addProofForSubsStep(var, subs, childFrom, cdp);
 491       vvec.push_back(var);
 492       svec.push_back(subs);
 493       pgs.push_back(cdp);
 494     }
 495     Node ts = t.substitute(vvec.begin(), vvec.end(), svec.begin(), svec.end());
 496     Node eq = t.eqNode(ts);
 497     if (ts != t)
 498     {
 499       // should be implied by the substitution now
 500       TConvProofGenerator tcpg(d_pnm,
 501                                nullptr,
 502                                TConvPolicy::ONCE,
 503                                TConvCachePolicy::NEVER,
 504                                "SUBS_TConvProofGenerator",
 505                                nullptr,
 506                                true);
 507       for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++)
 508       {
 509         // not necessarily closed, so we pass false to addRewriteStep.
 510         tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], false);
 511       }
 512       // add the proof constructed by the term conversion utility
 513       std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq);
 514       // should give a proof, if not, then tcpg does not agree with the
 515       // substitution.
 516       Assert(pfn != nullptr);
 517       if (pfn == nullptr)
 518       {
 519         cdp->addStep(eq, PfRule::TRUST_SUBS, {}, {eq});
 520       }
 521       else
 522       {
 523         cdp->addProof(pfn);
 524       }
 525     }
 526     else
 527     {
 528       // should not be necessary typically
 529       cdp->addStep(eq, PfRule::REFL, {}, {t});
 530     }
 531     return eq;
 532   }
 533   else if (id == PfRule::REWRITE)
 534   {
 535     // get the kind of rewrite
 536     MethodId idr = MethodId::RW_REWRITE;
 537     if (args.size() >= 2)
 538     {
 539       builtin::BuiltinProofRuleChecker::getMethodId(args[1], idr);
 540     }
 541     builtin::BuiltinProofRuleChecker* builtinPfC =
 542         static_cast<builtin::BuiltinProofRuleChecker*>(
 543             d_pnm->getChecker()->getCheckerFor(PfRule::REWRITE));
 544     Node ret = builtinPfC->applyRewrite(args[0], idr);
 545     Node eq = args[0].eqNode(ret);
 546     if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
 547     {
 548       // rewrites from theory::Rewriter
 549       // automatically expand THEORY_REWRITE as well here if set
 550       bool elimTR =
 551           (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end());
 552       bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
 553       // use rewrite with proof interface
 554       Rewriter* rr = d_smte->getRewriter();
 555       TrustNode trn = rr->rewriteWithProof(args[0], elimTR, isExtEq);
 556       std::shared_ptr<ProofNode> pfn = trn.toProofNode();
 557       if (pfn == nullptr)
 558       {
 559         Trace("smt-proof-pp-debug")
 560             << "Use TRUST_REWRITE for " << eq << std::endl;
 561         // did not have a proof of rewriting, probably isExtEq is true
 562         if (isExtEq)
 563         {
 564           // don't update
 565           return Node::null();
 566         }
 567         cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
 568       }
 569       else
 570       {
 571         cdp->addProof(pfn);
 572       }
 573       Assert(trn.getNode() == ret)
 574           << "Unexpected rewrite " << args[0] << std::endl
 575           << "Got: " << trn.getNode() << std::endl
 576           << "Expected: " << ret;
 577     }
 578     else if (idr == MethodId::RW_EVALUATE)
 579     {
 580       // change to evaluate, which is never eliminated
 581       cdp->addStep(eq, PfRule::EVALUATE, {}, {args[0]});
 582     }
 583     else
 584     {
 585       // don't know how to eliminate
 586       return Node::null();
 587     }
 588     if (args[0] == ret)
 589     {
 590       // should not be necessary typically
 591       cdp->addStep(eq, PfRule::REFL, {}, {args[0]});
 592     }
 593     return eq;
 594   }
 595
 596   // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
 597
 598   return Node::null();
 599 }
 600
 601 Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp)
 602 {
 603   Node tw = SkolemManager::getWitnessForm(t);
 604   Node eq = t.eqNode(tw);
 605   if (t == tw)
 606   {
 607     // not necessary, add REFL step
 608     cdp->addStep(eq, PfRule::REFL, {}, {t});
 609     return eq;
 610   }
 611   std::shared_ptr<ProofNode> pn = d_wfpm.getProofFor(eq);
 612   if (pn != nullptr)
 613   {
 614     // add the proof
 615     cdp->addProof(pn);
 616   }
 617   else
 618   {
 619     Assert(false) << "ProofPostprocessCallback::addProofForWitnessForm: failed "
 620                      "to add proof for witness form of "
 621                   << t;
 622   }
 623   return eq;
 624 }
 625
 626 Node ProofPostprocessCallback::addProofForTrans(
 627     const std::vector<Node>& tchildren, CDProof* cdp)
 628 {
 629   size_t tsize = tchildren.size();
 630   if (tsize > 1)
 631   {
 632     Node lhs = tchildren[0][0];
 633     Node rhs = tchildren[tsize - 1][1];
 634     Node eq = lhs.eqNode(rhs);
 635     cdp->addStep(eq, PfRule::TRANS, tchildren, {});
 636     return eq;
 637   }
 638   else if (tsize == 1)
 639   {
 640     return tchildren[0];
 641   }
 642   return Node::null();
 643 }
 644
 645 Node ProofPostprocessCallback::addProofForSubsStep(Node var,
 646                                                    Node subs,
 647                                                    Node assump,
 648                                                    CDProof* cdp)
 649 {
 650   // ensure we have a proof of var = subs
 651   Node veqs = var.eqNode(subs);
 652   if (veqs != assump)
 653   {
 654     // should be true intro or false intro
 655     Assert(subs.isConst());
 656     cdp->addStep(
 657         veqs,
 658         subs.getConst<bool>() ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO,
 659         {assump},
 660         {});
 661   }
 662   return veqs;
 663 }
 664
 665 bool ProofPostprocessCallback::addToTransChildren(Node eq,
 666                                                   std::vector<Node>& tchildren,
 667                                                   bool isSymm)
 668 {
 669   Assert(!eq.isNull());
 670   Assert(eq.getKind() == kind::EQUAL);
 671   if (eq[0] == eq[1])
 672   {
 673     return false;
 674   }
 675   Node equ = isSymm ? eq[1].eqNode(eq[0]) : eq;
 676   Assert(tchildren.empty()
 677          || (tchildren[tchildren.size() - 1].getKind() == kind::EQUAL
 678              && tchildren[tchildren.size() - 1][1] == equ[0]));
 679   tchildren.push_back(equ);
 680   return true;
 681 }
 682
 683 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
 684     ProofNodeManager* pnm)
 685     : d_ruleCount("finalProof::ruleCount"),
 686       d_totalRuleCount("finalProof::totalRuleCount", 0),
 687       d_minPedanticLevel("finalProof::minPedanticLevel", 10),
 688       d_numFinalProofs("finalProofs::numFinalProofs", 0),
 689       d_pnm(pnm),
 690       d_pedanticFailure(false)
 691 {
 692   smtStatisticsRegistry()->registerStat(&d_ruleCount);
 693   smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
 694   smtStatisticsRegistry()->registerStat(&d_minPedanticLevel);
 695   smtStatisticsRegistry()->registerStat(&d_numFinalProofs);
 696 }
 697
 698 ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
 699 {
 700   smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
 701   smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
 702   smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel);
 703   smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs);
 704 }
 705
 706 void ProofPostprocessFinalCallback::initializeUpdate()
 707 {
 708   d_pedanticFailure = false;
 709   d_pedanticFailureOut.str("");
 710   ++d_numFinalProofs;
 711 }
 712
 713 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 714                                                  bool& continueUpdate)
 715 {
 716   PfRule r = pn->getRule();
 717   if (Trace.isOn("final-pf-hole"))
 718   {
 719     if (r == PfRule::THEORY_REWRITE)
 720     {
 721       Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult()
 722                             << std::endl;
 723     }
 724   }
 725   // if not doing eager pedantic checking, fail if below threshold
 726   if (!options::proofNewPedanticEager())
 727   {
 728     if (!d_pedanticFailure)
 729     {
 730       Assert(d_pedanticFailureOut.str().empty());
 731       if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
 732       {
 733         d_pedanticFailure = true;
 734       }
 735     }
 736   }
 737   uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
 738   if (plevel != 0)
 739   {
 740     d_minPedanticLevel.minAssign(plevel);
 741   }
 742   // record stats for the rule
 743   d_ruleCount << r;
 744   ++d_totalRuleCount;
 745   return false;
 746 }
 747
 748 bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
 749 {
 750   if (d_pedanticFailure)
 751   {
 752     out << d_pedanticFailureOut.str();
 753     return true;
 754   }
 755   return false;
 756 }
 757
 758 ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
 759                                      SmtEngine* smte,
 760                                      ProofGenerator* pppg)
 761     : d_pnm(pnm),
 762       d_cb(pnm, smte, pppg),
 763       d_updater(d_pnm, d_cb),
 764       d_finalCb(pnm),
 765       d_finalizer(d_pnm, d_finalCb)
 766 {
 767 }
 768
 769 ProofPostproccess::~ProofPostproccess() {}
 770
 771 void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
 772 {
 773   // Initialize the callback, which computes necessary static information about
 774   // how to process, including how to process assumptions in pf.
 775   d_cb.initializeUpdate();
 776   // now, process
 777   d_updater.process(pf);
 778   // take stats and check pedantic
 779   d_finalCb.initializeUpdate();
 780   d_finalizer.process(pf);
 781
 782   std::stringstream serr;
 783   bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr);
 784   if (wasPedanticFailure)
 785   {
 786     AlwaysAssert(!wasPedanticFailure)
 787         << "ProofPostproccess::process: pedantic failure:" << std::endl
 788         << serr.str();
 789   }
 790 }
 791
 792 void ProofPostproccess::setEliminateRule(PfRule rule)
 793 {
 794   d_cb.setEliminateRule(rule);
 795 }
 796
 797 }  // namespace smt
 798 }  // namespace CVC4