diff options
author | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2013-08-06 18:25:16 +0100 |
---|---|---|
committer | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2013-08-06 18:25:16 +0100 |
commit | 4a426569a38760b9ecf34af46b4eeca76e21e8e6 (patch) | |
tree | fbba933bdc9f380b89192bbe25bee09d5a99a660 /lib/Core/TimingSolver.h | |
parent | ca83defeab023dbfbbd21d8a497a42af9abdf7fd (diff) | |
download | klee-4a426569a38760b9ecf34af46b4eeca76e21e8e6.tar.gz |
TimingSolver and constructSolverChain() no longer coupled with pointers to STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver.
Diffstat (limited to 'lib/Core/TimingSolver.h')
-rw-r--r-- | lib/Core/TimingSolver.h | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 2684e071..c98dd881 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -17,15 +17,13 @@ namespace klee { class ExecutionState; - class Solver; - class STPSolver; + class Solver; /// TimingSolver - A simple class which wraps a solver and handles /// tracking the statistics that we care about. class TimingSolver { public: Solver *solver; - STPSolver *stpSolver; bool simplifyExprs; public: @@ -34,15 +32,14 @@ namespace klee { /// \param _simplifyExprs - Whether expressions should be /// simplified (via the constraint manager interface) prior to /// querying. - TimingSolver(Solver *_solver, STPSolver *_stpSolver, - bool _simplifyExprs = true) - : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {} + TimingSolver(Solver *_solver, bool _simplifyExprs = true) + : solver(_solver), simplifyExprs(_simplifyExprs) {} ~TimingSolver() { delete solver; } void setTimeout(double t) { - stpSolver->setCoreSolverTimeout(t); + solver->setCoreSolverTimeout(t); } char *getConstraintLog(const Query& query) { |