Add statistics for proof gen./checking time, size (#2850)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 13 Mar 2019 22:47:04 +0000 (22:47 +0000)
committerGitHub <noreply@github.com>
Wed, 13 Mar 2019 22:47:04 +0000 (22:47 +0000)
commitb574ccf82270f8887d2d697c537c591ff4ab68a2
treeeaecd85977bda2808e06618b981d16b60e2f5639
parent68174dedcb4bf9d91241585ab1cc876d2fa83d62
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
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp [deleted file]