Split proof final callback to its own file (#6984)

5 files changed, 187 insertions, 119 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index bc7103f0d..2aa91f61b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -323,6 +323,8 @@ libcvc5_add_sources(
   smt/process_assertions.h
   smt/proof_manager.cpp
   smt/proof_manager.h
+  smt/proof_final_callback.cpp
+  smt/proof_final_callback.h
   smt/proof_post_processor.cpp
   smt/proof_post_processor.h
   smt/set_defaults.cpp
diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
new file mode 100644
index 000000000..ae35b346c
--- /dev/null
+++ b/src/smt/proof_final_callback.cpp
@@ -0,0 +1,109 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of module for final processing proof nodes.
+ */
+
+#include "smt/proof_final_callback.h"
+
+#include "options/proof_options.h"
+#include "proof/proof_checker.h"
+#include "proof/proof_node_manager.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/builtin/proof_checker.h"
+#include "theory/theory_id.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+
+namespace cvc5 {
+namespace smt {
+
+ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm)
+    : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
+          "finalProof::ruleCount")),
+      d_instRuleIds(
+          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
+              "finalProof::instRuleId")),
+      d_totalRuleCount(
+          smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
+      d_minPedanticLevel(
+          smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
+      d_numFinalProofs(
+          smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
+      d_pnm(pnm),
+      d_pedanticFailure(false)
+{
+  d_minPedanticLevel += 10;
+}
+
+void ProofFinalCallback::initializeUpdate()
+{
+  d_pedanticFailure = false;
+  d_pedanticFailureOut.str("");
+  ++d_numFinalProofs;
+}
+
+bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                      const std::vector<Node>& fa,
+                                      bool& continueUpdate)
+{
+  PfRule r = pn->getRule();
+  // if not doing eager pedantic checking, fail if below threshold
+  if (!options::proofEagerChecking())
+  {
+    if (!d_pedanticFailure)
+    {
+      Assert(d_pedanticFailureOut.str().empty());
+      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
+      {
+        d_pedanticFailure = true;
+      }
+    }
+  }
+  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
+  if (plevel != 0)
+  {
+    d_minPedanticLevel.minAssign(plevel);
+  }
+  // record stats for the rule
+  d_ruleCount << r;
+  ++d_totalRuleCount;
+  // take stats on the instantiations in the proof
+  if (r == PfRule::INSTANTIATE)
+  {
+    Node q = pn->getChildren()[0]->getResult();
+    const std::vector<Node>& args = pn->getArguments();
+    if (args.size() > q[0].getNumChildren())
+    {
+      InferenceId id;
+      if (getInferenceId(args[q[0].getNumChildren()], id))
+      {
+        d_instRuleIds << id;
+      }
+    }
+  }
+  return false;
+}
+
+bool ProofFinalCallback::wasPedanticFailure(std::ostream& out) const
+{
+  if (d_pedanticFailure)
+  {
+    out << d_pedanticFailureOut.str();
+    return true;
+  }
+  return false;
+}
+
+}  // namespace smt
+}  // namespace cvc5
diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h
new file mode 100644
index 000000000..88b8e20ef
--- /dev/null
+++ b/src/smt/proof_final_callback.h
@@ -0,0 +1,74 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The module for final processing proof nodes.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__PROOF_FINAL_CALLBACK_H
+#define CVC5__SMT__PROOF_FINAL_CALLBACK_H
+
+#include <map>
+#include <sstream>
+#include <unordered_set>
+
+#include "proof/proof_node_updater.h"
+#include "theory/inference_id.h"
+#include "util/statistics_stats.h"
+
+namespace cvc5 {
+namespace smt {
+
+/** Final callback class, for stats and pedantic checking */
+class ProofFinalCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  ProofFinalCallback(ProofNodeManager* pnm);
+  /**
+   * 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(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
+                    bool& continueUpdate) 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;
+  /**
+   * Counts number of postprocessed proof nodes of rule INSTANTIATE that were
+   * marked with the given inference id.
+   */
+  HistogramStat<theory::InferenceId> d_instRuleIds;
+  /** Total number of postprocessed rule applications */
+  IntStat d_totalRuleCount;
+  /** The minimum pedantic level of any rule encountered */
+  IntStat d_minPedanticLevel;
+  /** The total number of final proofs */
+  IntStat d_numFinalProofs;
+  /** 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;
+};
+
+}  // namespace smt
+}  // namespace cvc5
+
+#endif
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 66f9fde7c..98ec30093 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -21,7 +21,6 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_node_manager.h"
 #include "smt/smt_engine.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/rewriter.h"
@@ -1179,84 +1178,6 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq,
   return true;
 }
 
-ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
-    ProofNodeManager* pnm)
-    : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
-          "finalProof::ruleCount")),
-      d_instRuleIds(
-          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
-              "finalProof::instRuleId")),
-      d_totalRuleCount(
-          smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
-      d_minPedanticLevel(
-          smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
-      d_numFinalProofs(
-          smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
-      d_pnm(pnm),
-      d_pedanticFailure(false)
-{
-  d_minPedanticLevel += 10;
-}
-
-void ProofPostprocessFinalCallback::initializeUpdate()
-{
-  d_pedanticFailure = false;
-  d_pedanticFailureOut.str("");
-  ++d_numFinalProofs;
-}
-
-bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
-                                                 const std::vector<Node>& fa,
-                                                 bool& continueUpdate)
-{
-  PfRule r = pn->getRule();
-  // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofEagerChecking())
-  {
-    if (!d_pedanticFailure)
-    {
-      Assert(d_pedanticFailureOut.str().empty());
-      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
-      {
-        d_pedanticFailure = true;
-      }
-    }
-  }
-  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
-  if (plevel != 0)
-  {
-    d_minPedanticLevel.minAssign(plevel);
-  }
-  // record stats for the rule
-  d_ruleCount << r;
-  ++d_totalRuleCount;
-  // take stats on the instantiations in the proof
-  if (r == PfRule::INSTANTIATE)
-  {
-    Node q = pn->getChildren()[0]->getResult();
-    const std::vector<Node>& args = pn->getArguments();
-    if (args.size() > q[0].getNumChildren())
-    {
-      InferenceId id;
-      if (getInferenceId(args[q[0].getNumChildren()], id))
-      {
-        d_instRuleIds << id;
-      }
-    }
-  }
-  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,
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 056f77695..1aa52dd50 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -23,6 +23,7 @@
 #include <unordered_set>
 
 #include "proof/proof_node_updater.h"
+#include "smt/proof_final_callback.h"
 #include "smt/witness_form.h"
 #include "theory/inference_id.h"
 #include "util/statistics_stats.h"
@@ -237,45 +238,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
                              CDProof* cdp);
 };
 
-/** Final callback class, for stats and pedantic checking */
-class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
-{
- public:
-  ProofPostprocessFinalCallback(ProofNodeManager* pnm);
-  /**
-   * 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(std::shared_ptr<ProofNode> pn,
-                    const std::vector<Node>& fa,
-                    bool& continueUpdate) 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;
-  /**
-   * Counts number of postprocessed proof nodes of rule INSTANTIATE that were
-   * marked with the given inference id.
-   */
-  HistogramStat<theory::InferenceId> d_instRuleIds;
-  /** Total number of postprocessed rule applications */
-  IntStat d_totalRuleCount;
-  /** The minimum pedantic level of any rule encountered */
-  IntStat d_minPedanticLevel;
-  /** The total number of final proofs */
-  IntStat d_numFinalProofs;
-  /** 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:
@@ -314,7 +276,7 @@ class ProofPostproccess
    */
   ProofNodeUpdater d_updater;
   /** The post process callback for finalization */
-  ProofPostprocessFinalCallback d_finalCb;
+  ProofFinalCallback d_finalCb;
   /**
    * The finalizer, which is responsible for taking stats and checking for
    * (lazy) pedantic failures.