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
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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
#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"
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,
#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"
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:
*/
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.
projects / cvc5.git / commitdiff