From 4cf91341622270e4aaefe926d4be7fe148c6fa74 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 Aug 2021 13:48:42 -0500 Subject: [PATCH] Split proof final callback to its own file (#6984) --- src/CMakeLists.txt | 2 + src/smt/proof_final_callback.cpp | 109 +++++++++++++++++++++++++++++++ src/smt/proof_final_callback.h | 74 +++++++++++++++++++++ src/smt/proof_post_processor.cpp | 79 ---------------------- src/smt/proof_post_processor.h | 42 +----------- 5 files changed, 187 insertions(+), 119 deletions(-) create mode 100644 src/smt/proof_final_callback.cpp create mode 100644 src/smt/proof_final_callback.h 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( + "finalProof::ruleCount")), + d_instRuleIds( + smtStatisticsRegistry().registerHistogram( + "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 pn, + const std::vector& 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& 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 +#include +#include + +#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 pn, + const std::vector& 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 d_ruleCount; + /** + * Counts number of postprocessed proof nodes of rule INSTANTIATE that were + * marked with the given inference id. + */ + HistogramStat 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( - "finalProof::ruleCount")), - d_instRuleIds( - smtStatisticsRegistry().registerHistogram( - "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 pn, - const std::vector& 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& 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 #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 pn, - const std::vector& 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 d_ruleCount; - /** - * Counts number of postprocessed proof nodes of rule INSTANTIATE that were - * marked with the given inference id. - */ - HistogramStat 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. -- 2.30.2