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/CMakeLists.txt | |
| 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/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 1 |
1 files changed, 0 insertions, 1 deletions
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 |