diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2013-07-11 16:21:15 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2013-07-11 16:21:15 +0000 |
| commit | d47bf6b91faeab6c97a06108ed35b2b7ad0a45fc (patch) | |
| tree | 2314b8f81c311f9077af964b9eb9872cfdede220 /lib/Solver/CachingSolver.cpp | |
| parent | e4ce97b38411de5d972ee4cf89cede342b7f82f0 (diff) | |
| download | klee-d47bf6b91faeab6c97a06108ed35b2b7ad0a45fc.tar.gz | |
Fixed and improved the stats on (cex)cache hits and misses.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186097 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Solver/CachingSolver.cpp')
| -rw-r--r-- | lib/Solver/CachingSolver.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index b6a93c7b..5911bbf3 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -73,12 +73,14 @@ public: bool computeValidity(const Query&, Solver::Validity &result); bool computeTruth(const Query&, bool &isValid); bool computeValue(const Query& query, ref<Expr> &result) { + ++stats::queryCacheMisses; return solver->impl->computeValue(query, result); } bool computeInitialValues(const Query& query, const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution) { + ++stats::queryCacheMisses; return solver->impl->computeInitialValues(query, objects, values, hasSolution); } @@ -141,19 +143,21 @@ bool CachingSolver::computeValidity(const Query& query, bool tmp, cacheHit = cacheLookup(query, cachedResult); if (cacheHit) { - ++stats::queryCacheHits; - switch(cachedResult) { case IncompleteSolver::MustBeTrue: result = Solver::True; + ++stats::queryCacheHits; return true; case IncompleteSolver::MustBeFalse: result = Solver::False; + ++stats::queryCacheHits; return true; case IncompleteSolver::TrueOrFalse: result = Solver::Unknown; + ++stats::queryCacheHits; return true; case IncompleteSolver::MayBeTrue: { + ++stats::queryCacheMisses; if (!solver->impl->computeTruth(query, tmp)) return false; if (tmp) { @@ -167,6 +171,7 @@ bool CachingSolver::computeValidity(const Query& query, } } case IncompleteSolver::MayBeFalse: { + ++stats::queryCacheMisses; if (!solver->impl->computeTruth(query.negateExpr(), tmp)) return false; if (tmp) { |