Add statistics for proof gen./checking time, size (#2850)

This commit adds a statistic that records the total size of all proofs
generated by an instance of `SmtEngine`. The commit also moves
`SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know
the complete type of `d_stats` (and the separate file for that method
didn't seem that useful). Additionally, it changes
`smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime`
that only measures the time spent in LFSC and adds a statistic
`proof::ProofManager::proofProductionTime` that measures the proof
production time separately (also works with `get-proof`/`--dump-proof`).

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 388e3c4fb8d6e54aa3db53b34186b3ec7ad59368..5f34fe59b612a960dcf5bb8727d46391059de830 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -237,7 +237,6 @@ libcvc4_add_sources(
   smt/model_core_builder.h
   smt/smt_engine.cpp
   smt/smt_engine.h
-  smt/smt_engine_check_proof.cpp
   smt/smt_engine_scope.cpp
   smt/smt_engine_scope.h
   smt/smt_statistics_registry.cpp

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9878972bfb7711c7c72bb69652f0cc210684ea45..5f0ade86a427ec9b30da2c7abb827179111e8cb6 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -30,6 +30,7 @@
 #include "proof/theory_proof.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/output_channel.h"
@@ -559,6 +560,9 @@ void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
 
 void LFSCProof::toStream(std::ostream& out) const
 {
+  TimerStat::CodeTimer proofProductionTimer(
+      *ProofManager::currentPM()->getProofProductionTime());
+
   Assert(!d_satProof->proofConstructed());
   d_satProof->constructProof();
 
@@ -1069,4 +1073,16 @@ void ProofManager::printTrustedTerm(Node term,
   tpe->printTheoryTerm(term.toExpr(), os, globalLetMap);
   if (tpe->printsAsBool(term)) os << ")";
 }
+
+ProofManager::ProofManagerStatistics::ProofManagerStatistics()
+    : d_proofProductionTime("proof::ProofManager::proofProductionTime")
+{
+  smtStatisticsRegistry()->registerStat(&d_proofProductionTime);
+}
+
+ProofManager::ProofManagerStatistics::~ProofManagerStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_proofProductionTime);
+}
+
 } /* CVC4  namespace */

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 82efbab0f871310429deb70d8f925d3a27153c88..081ce7a74087bf8d16b0361bd98b9b84fa0d878b 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -24,9 +24,9 @@
 #include <unordered_map>
 #include <unordered_set>
 
-#include "expr/node.h"
-#include "context/cdhashset.h"
 #include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "expr/node.h"
 #include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "proof/proof_utils.h"
@@ -34,7 +34,7 @@
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
 #include "util/proof.h"
-
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -298,9 +298,26 @@ public:
                          std::ostream& out,
                          std::ostringstream& paren);
 
-private:
+  TimerStat* getProofProductionTime() { return &d_stats.d_proofProductionTime; }
+
+ private:
   void constructSatProof();
   std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
+
+  struct ProofManagerStatistics
+  {
+    ProofManagerStatistics();
+    ~ProofManagerStatistics();
+
+    /**
+     * Time spent producing proofs (i.e. generating the proof from the logging
+     * information)
+     */
+    TimerStat d_proofProductionTime;
+  }; /* struct ProofManagerStatistics */
+
+  ProofManagerStatistics d_stats;
+
 };/* class ProofManager */
 
 class LFSCProof : public Proof

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 68b7e225112693d2d4028c5ae4b9c02dca215e05..bac2f2f505028dedf34ea59afc561747e6583db8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -111,6 +111,10 @@
 #include "util/random.h"
 #include "util/resource_manager.h"
 
+#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
+#include "lfscc.h"
+#endif
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
@@ -120,6 +124,11 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 namespace CVC4 {
+
+namespace proof {
+extern const char* const plf_signatures;
+}  // namespace proof
+
 namespace smt {
 
 struct DeleteCommandFunction : public std::unary_function<const Command*, void>
@@ -178,10 +187,12 @@ struct SmtEngineStatistics {
   IntStat d_numAssertionsPre;
   /** Num of assertions after ite removal */
   IntStat d_numAssertionsPost;
+  /** Size of all proofs generated */
+  IntStat d_proofsSize;
   /** time spent in checkModel() */
   TimerStat d_checkModelTime;
-  /** time spent in checkProof() */
-  TimerStat d_checkProofTime;
+  /** time spent checking the proof with LFSC */
+  TimerStat d_lfscCheckProofTime;
   /** time spent in checkUnsatCore() */
   TimerStat d_checkUnsatCoreTime;
   /** time spent in PropEngine::checkSat() */
@@ -196,28 +207,30 @@ struct SmtEngineStatistics {
   /** Number of resource units spent. */
   ReferenceStat<uint64_t> d_resourceUnitsUsed;
 
-  SmtEngineStatistics() :
-    d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
-    d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
-    d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
-    d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
-    d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
-    d_checkModelTime("smt::SmtEngine::checkModelTime"),
-    d_checkProofTime("smt::SmtEngine::checkProofTime"),
-    d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
-    d_solveTime("smt::SmtEngine::solveTime"),
-    d_pushPopTime("smt::SmtEngine::pushPopTime"),
-    d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
-    d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
-    d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
- {
+  SmtEngineStatistics()
+      : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
+        d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
+        d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
+        d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
+        d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
+        d_proofsSize("smt::SmtEngine::proofsSize", 0),
+        d_checkModelTime("smt::SmtEngine::checkModelTime"),
+        d_lfscCheckProofTime("smt::SmtEngine::lfscCheckProofTime"),
+        d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
+        d_solveTime("smt::SmtEngine::solveTime"),
+        d_pushPopTime("smt::SmtEngine::pushPopTime"),
+        d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
+        d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
+        d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
+  {
     smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
     smtStatisticsRegistry()->registerStat(&d_numConstantProps);
     smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
     smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
     smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
+    smtStatisticsRegistry()->registerStat(&d_proofsSize);
     smtStatisticsRegistry()->registerStat(&d_checkModelTime);
-    smtStatisticsRegistry()->registerStat(&d_checkProofTime);
+    smtStatisticsRegistry()->registerStat(&d_lfscCheckProofTime);
     smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
     smtStatisticsRegistry()->registerStat(&d_solveTime);
     smtStatisticsRegistry()->registerStat(&d_pushPopTime);
@@ -232,8 +245,9 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
     smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
     smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
+    smtStatisticsRegistry()->unregisterStat(&d_proofsSize);
     smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
-    smtStatisticsRegistry()->unregisterStat(&d_checkProofTime);
+    smtStatisticsRegistry()->unregisterStat(&d_lfscCheckProofTime);
     smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
     smtStatisticsRegistry()->unregisterStat(&d_solveTime);
     smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
@@ -3712,7 +3726,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
     // Check that UNSAT results generate a proof correctly.
     if(options::checkProofs()) {
       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-        TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
         checkProof();
       }
     }
@@ -4367,6 +4380,57 @@ Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
 Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
+void SmtEngine::checkProof()
+{
+#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
+
+  Chat() << "generating proof..." << endl;
+
+  const Proof& pf = getProof();
+
+  Chat() << "checking proof..." << endl;
+
+  std::string logicString = d_logic.getLogicString();
+
+  if (!(
+          // Pure logics
+          logicString == "QF_UF" || logicString == "QF_AX"
+          || logicString == "QF_BV" ||
+          // Non-pure logics
+          logicString == "QF_AUF" || logicString == "QF_UFBV"
+          || logicString == "QF_ABV" || logicString == "QF_AUFBV"))
+  {
+    // This logic is not yet supported
+    Notice() << "Notice: no proof-checking for " << logicString << " proofs yet"
+             << endl;
+    return;
+  }
+
+  std::stringstream pfStream;
+
+  pfStream << proof::plf_signatures << endl;
+  int64_t sizeBeforeProof = static_cast<int64_t>(pfStream.tellp());
+
+  pf.toStream(pfStream);
+  d_stats->d_proofsSize +=
+      static_cast<int64_t>(pfStream.tellp()) - sizeBeforeProof;
+
+  {
+    TimerStat::CodeTimer checkProofTimer(d_stats->d_lfscCheckProofTime);
+    lfscc_init();
+    lfscc_check_file(pfStream, false, false, false, false, false, false, false);
+  }
+  // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
+  // segfaults on regress0/bv/core/bitvec7.smt
+  // lfscc_cleanup();
+
+#else  /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
+  Unreachable(
+      "This version of CVC4 was built without proof support; cannot check "
+      "proofs.");
+#endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
+}
+
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
 #if IS_PROOFS_BUILD

diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
deleted file mode 100644 (file)
index 55d27a0..0000000
--- a/src/smt/smt_engine_check_proof.cpp
+++ /dev/null
@@ -1,81 +0,0 @@
-/*********************                                                        */
-/*! \file smt_engine_check_proof.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mark Laws, Guy Katz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include <sstream>
-#include <string>
-
-#include "base/configuration_private.h"
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-#include "smt/smt_engine.h"
-#include "util/proof.h"
-#include "util/statistics_registry.h"
-
-#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
-#include "lfscc.h"
-#endif
-
-using namespace CVC4;
-using namespace std;
-
-namespace CVC4 {
-namespace proof {
-extern const char *const plf_signatures;
-}  // namespace proof
-}  // namespace CVC4
-
-void SmtEngine::checkProof() {
-
-#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
-
-  Chat() << "generating proof..." << endl;
-
-  const Proof& pf = getProof();
-
-  Chat() << "checking proof..." << endl;
-
-  std::string logicString = d_logic.getLogicString();
-
-  if (!(
-        // Pure logics
-        logicString == "QF_UF" ||
-        logicString == "QF_AX" ||
-        logicString == "QF_BV" ||
-        // Non-pure logics
-        logicString == "QF_AUF" ||
-        logicString == "QF_UFBV" ||
-        logicString == "QF_ABV" ||
-        logicString == "QF_AUFBV"
-        )) {
-    // This logic is not yet supported
-    Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl;
-    return;
-  }
-
-  std::stringstream pfStream;
-  pfStream << proof::plf_signatures << endl;
-  pf.toStream(pfStream);
-  lfscc_init();
-  lfscc_check_file(pfStream, false, false, false, false, false, false, false);
-  // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
-  // segfaults on regress0/bv/core/bitvec7.smt
-  //lfscc_cleanup();
-
-#else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
-  Unreachable("This version of CVC4 was built without proof support; cannot check proofs.");
-#endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
-}