From d47bf6b91faeab6c97a06108ed35b2b7ad0a45fc Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Thu, 11 Jul 2013 16:21:15 +0000
Subject: 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
---
 lib/Solver/CachingSolver.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'lib/Solver/CachingSolver.cpp')

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) {
-- 
cgit 1.4.1