(proof-new) Add the SMT proof post processor (#4913)

This PR adds the proof post-processor, which is the final authority on putting together the overall proof. It additionally implements lazy pedantic failures and statistics.

This PR also corrects a subtle bug in the elimination of SUBS which requires a TRUE_INTRO/FALSE_INTRO in certain cases.

2 files changed, 196 insertions, 12 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 5046dee92..197cdd4b7 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -404,17 +404,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           pfn = cdp->getProofFor(children[i]);
           pf->addProof(pfn);
           // ensure we have a proof of var = subs
-          Node veqs = var.eqNode(subs);
-          if (veqs != children[index])
-          {
-            // should be true intro or false intro
-            Assert(subs.isConst());
-            pf->addStep(veqs,
-                        subs.getConst<bool>() ? PfRule::TRUE_INTRO
-                                              : PfRule::FALSE_INTRO,
-                        {children[index]},
-                        {});
-          }
+          Node veqs = addProofForSubsStep(var, subs, children[index], pf.get());
+          // transitivity
           pf->addStep(var.eqNode(ss), PfRule::TRANS, {veqs, seqss}, {});
           // add to the substitution
           vvec.push_back(var);
@@ -423,7 +414,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           continue;
         }
       }
-      // just use equality from CDProof
+      // Just use equality from CDProof, but ensure we have a proof in cdp.
+      // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step
+      // uses the assumption children[index] as a Boolean assignment (e.g.
+      // children[index] = true if we are using MethodId::SB_LITERAL).
+      addProofForSubsStep(var, subs, children[index], cdp);
       vvec.push_back(var);
       svec.push_back(subs);
       pgs.push_back(cdp);
@@ -550,6 +545,26 @@ Node ProofPostprocessCallback::addProofForTrans(
   return Node::null();
 }
 
+Node ProofPostprocessCallback::addProofForSubsStep(Node var,
+                                                   Node subs,
+                                                   Node assump,
+                                                   CDProof* cdp)
+{
+  // ensure we have a proof of var = subs
+  Node veqs = var.eqNode(subs);
+  if (veqs != assump)
+  {
+    // should be true intro or false intro
+    Assert(subs.isConst());
+    cdp->addStep(
+        veqs,
+        subs.getConst<bool>() ? PfRule::TRUE_INTRO : PfRule::FALSE_INTRO,
+        {assump},
+        {});
+  }
+  return veqs;
+}
+
 bool ProofPostprocessCallback::addToTransChildren(Node eq,
                                                   std::vector<Node>& tchildren,
                                                   bool isSymm)
@@ -568,5 +583,104 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq,
   return true;
 }
 
+ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
+    ProofNodeManager* pnm)
+    : d_ruleCount("finalProof::ruleCount"),
+      d_totalRuleCount("finalProof::totalRuleCount", 0),
+      d_pnm(pnm),
+      d_pedanticFailure(false)
+{
+  smtStatisticsRegistry()->registerStat(&d_ruleCount);
+  smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
+}
+
+ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
+  smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
+}
+
+void ProofPostprocessFinalCallback::initializeUpdate()
+{
+  d_pedanticFailure = false;
+  d_pedanticFailureOut.str("");
+}
+
+bool ProofPostprocessFinalCallback::shouldUpdate(ProofNode* pn)
+{
+  PfRule r = pn->getRule();
+  if (Trace.isOn("final-pf-hole"))
+  {
+    if (r == PfRule::THEORY_REWRITE)
+    {
+      Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult()
+                            << std::endl;
+    }
+  }
+  // if not doing eager pedantic checking, fail if below threshold
+  if (!options::proofNewPedanticEager())
+  {
+    if (!d_pedanticFailure)
+    {
+      Assert(d_pedanticFailureOut.str().empty());
+      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
+      {
+        d_pedanticFailure = true;
+      }
+    }
+  }
+  // record stats for the rule
+  d_ruleCount << r;
+  ++d_totalRuleCount;
+  return false;
+}
+
+bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
+{
+  if (d_pedanticFailure)
+  {
+    out << d_pedanticFailureOut.str();
+    return true;
+  }
+  return false;
+}
+
+ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
+                                     SmtEngine* smte,
+                                     ProofGenerator* pppg)
+    : d_cb(pnm, smte, pppg), d_finalCb(pnm), d_pnm(pnm)
+{
+}
+
+ProofPostproccess::~ProofPostproccess() {}
+
+void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
+{
+  // Initialize the callback, which computes necessary static information about
+  // how to process, including how to process assumptions in pf.
+  d_cb.initializeUpdate();
+  // now, process
+  ProofNodeUpdater updater(d_pnm, d_cb);
+  updater.process(pf);
+  // take stats and check pedantic
+  d_finalCb.initializeUpdate();
+  ProofNodeUpdater finalizer(d_pnm, d_finalCb);
+  finalizer.process(pf);
+
+  std::stringstream serr;
+  bool wasPedanticFailure = d_finalCb.wasPedanticFailure(serr);
+  if (wasPedanticFailure)
+  {
+    AlwaysAssert(!wasPedanticFailure)
+        << "ProofPostproccess::process: pedantic failure:" << std::endl
+        << serr.str();
+  }
+}
+
+void ProofPostproccess::setEliminateRule(PfRule rule)
+{
+  d_cb.setEliminateRule(rule);
+}
+
 }  // namespace smt
 }  // namespace CVC4
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 8dc540701..6c75af5ce 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -119,12 +119,82 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
    * @return The conclusion of the TRANS step.
    */
   Node addProofForTrans(const std::vector<Node>& tchildren, CDProof* cdp);
+  /**
+   * Add proof for substitution step. Some substitutions are derived based
+   * on viewing a formula as a Boolean assignment (see MethodId::SB_LITERAL for
+   * example). This method ensures that the proof of var == subs exists
+   * in cdp, where var, subs were derived from BuiltinProofRuleChecker's
+   * getSubstitution method.
+   *
+   * @param var The variable of the substitution
+   * @param subs The substituted term
+   * @param assump The formula the substitution was derived from
+   * @param cdp The proof to add to
+   * @return var == subs, the conclusion of the substitution step.
+   */
+  Node addProofForSubsStep(Node var, Node subs, Node assump, CDProof* cdp);
   /** Add eq (or its symmetry) to transivity children, if not reflexive */
   bool addToTransChildren(Node eq,
                           std::vector<Node>& tchildren,
                           bool isSymm = false);
 };
 
+/** Final callback class, for stats and pedantic checking */
+class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  ProofPostprocessFinalCallback(ProofNodeManager* pnm);
+  ~ProofPostprocessFinalCallback();
+  /**
+   * Initialize, called once for each new ProofNode to process. This initializes
+   * static information to be used by successive calls to update.
+   */
+  void initializeUpdate();
+  /** Should proof pn be updated? Returns false, adds to stats. */
+  bool shouldUpdate(ProofNode* pn) override;
+  /** was pedantic failure */
+  bool wasPedanticFailure(std::ostream& out) const;
+
+ private:
+  /** Counts number of postprocessed proof nodes for each kind of proof rule */
+  HistogramStat<PfRule> d_ruleCount;
+  /** Total number of postprocessed rule applications */
+  IntStat d_totalRuleCount;
+  /** Proof node manager (used for pedantic checking) */
+  ProofNodeManager* d_pnm;
+  /** Was there a pedantic failure? */
+  bool d_pedanticFailure;
+  /** The pedantic failure string for debugging */
+  std::stringstream d_pedanticFailureOut;
+};
+
+/**
+ * The proof postprocessor module. This postprocesses the final proof
+ * produced by an SmtEngine. Its main two tasks are to:
+ * (1) Connect proofs of preprocessing,
+ * (2) Expand macro PfRule applications.
+ */
+class ProofPostproccess
+{
+ public:
+  ProofPostproccess(ProofNodeManager* pnm,
+                    SmtEngine* smte,
+                    ProofGenerator* pppg);
+  ~ProofPostproccess();
+  /** post-process */
+  void process(std::shared_ptr<ProofNode> pf);
+  /** set eliminate rule */
+  void setEliminateRule(PfRule rule);
+
+ private:
+  /** The post process callback */
+  ProofPostprocessCallback d_cb;
+  /** The post process callback for finalization */
+  ProofPostprocessFinalCallback d_finalCb;
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
 }  // namespace smt
 }  // namespace CVC4