diff options
| -rw-r--r-- | lib/Core/TimingSolver.cpp | 32 |
1 files changed, 9 insertions, 23 deletions
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index b70bcbef..3b66f641 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -13,12 +13,10 @@ #include "klee/ExecutionState.h" #include "klee/Solver.h" #include "klee/Statistics.h" -#include "klee/Internal/System/Time.h" +#include "klee/TimerStatIncrementer.h" #include "CoreStats.h" -#include "llvm/Support/TimeValue.h" - using namespace klee; using namespace llvm; @@ -32,17 +30,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now = util::getWallTimeVal(); + TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->evaluate(Query(state.constraints, expr), result); - sys::TimeValue delta = util::getWallTimeVal(); - delta -= now; - stats::solverTime += delta.usec(); - state.queryCost += delta.usec()/1000000.; + state.queryCost += timer.check() / 1e6; return success; } @@ -55,17 +50,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now = util::getWallTimeVal(); + TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->mustBeTrue(Query(state.constraints, expr), result); - sys::TimeValue delta = util::getWallTimeVal(); - delta -= now; - stats::solverTime += delta.usec(); - state.queryCost += delta.usec()/1000000.; + state.queryCost += timer.check() / 1e6; return success; } @@ -101,17 +93,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now = util::getWallTimeVal(); + TimerStatIncrementer timer(stats::solverTime); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->getValue(Query(state.constraints, expr), result); - sys::TimeValue delta = util::getWallTimeVal(); - delta -= now; - stats::solverTime += delta.usec(); - state.queryCost += delta.usec()/1000000.; + state.queryCost += timer.check() / 1e6; return success; } @@ -125,16 +114,13 @@ TimingSolver::getInitialValues(const ExecutionState& state, if (objects.empty()) return true; - sys::TimeValue now = util::getWallTimeVal(); + TimerStatIncrementer timer(stats::solverTime); bool success = solver->getInitialValues(Query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result); - sys::TimeValue delta = util::getWallTimeVal(); - delta -= now; - stats::solverTime += delta.usec(); - state.queryCost += delta.usec()/1000000.; + state.queryCost += timer.check() / 1e6; return success; } |