about summary refs log tree commit diff homepage
path: root/lib/Core/TimingSolver.h
diff options
context:
space:
mode:
authorHristina Palikareva <h.palikareva@imperial.ac.uk>2013-08-06 18:25:16 +0100
committerHristina Palikareva <h.palikareva@imperial.ac.uk>2013-08-06 18:25:16 +0100
commit4a426569a38760b9ecf34af46b4eeca76e21e8e6 (patch)
treefbba933bdc9f380b89192bbe25bee09d5a99a660 /lib/Core/TimingSolver.h
parentca83defeab023dbfbbd21d8a497a42af9abdf7fd (diff)
downloadklee-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.h11
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) {