From b574ccf82270f8887d2d697c537c591ff4ab68a2 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 13 Mar 2019 22:47:04 +0000 Subject: [PATCH] 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`). --- src/CMakeLists.txt | 1 - src/proof/proof_manager.cpp | 16 +++++ src/proof/proof_manager.h | 25 +++++-- src/smt/smt_engine.cpp | 104 +++++++++++++++++++++++------ src/smt/smt_engine_check_proof.cpp | 81 ---------------------- 5 files changed, 121 insertions(+), 106 deletions(-) delete mode 100644 src/smt/smt_engine_check_proof.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 388e3c4fb..5f34fe59b 100644 --- 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 9878972bf..5f0ade86a 100644 --- 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 82efbab0f..081ce7a74 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -24,9 +24,9 @@ #include #include -#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 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 68b7e2251..bac2f2f50 100644 --- 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 @@ -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 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& 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(pfStream.tellp()); + + pf.toStream(pfStream); + d_stats->d_proofsSize += + static_cast(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 index 55d27a014..000000000 --- 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 -#include - -#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) */ -} -- 2.30.2