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/proof | |
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/proof')
-rw-r--r-- | src/proof/proof_manager.cpp | 16 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 25 |
2 files changed, 37 insertions, 4 deletions
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 <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 |