diff options
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) { |