diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-13 22:47:04 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-13 22:47:04 +0000 |
commit | b574ccf82270f8887d2d697c537c591ff4ab68a2 (patch) | |
tree | eaecd85977bda2808e06618b981d16b60e2f5639 /src/smt | |
parent | 68174dedcb4bf9d91241585ab1cc876d2fa83d62 (diff) |
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`).
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 104 | ||||
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 81 |
2 files changed, 84 insertions, 101 deletions
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<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 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 <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) */ -} |