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