From 4a426569a38760b9ecf34af46b4eeca76e21e8e6 Mon Sep 17 00:00:00 2001
From: Hristina Palikareva <h.palikareva@imperial.ac.uk>
Date: Tue, 6 Aug 2013 18:25:16 +0100
Subject: 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.

---
 lib/Basic/ConstructSolverChain.cpp | 14 +++++++-------
 lib/Core/Executor.cpp              |  9 +++++----
 lib/Core/TimingSolver.h            | 11 ++++-------
 3 files changed, 16 insertions(+), 18 deletions(-)

(limited to 'lib')

diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 70c728df..c0d0ef61 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -16,13 +16,13 @@
 
 namespace klee
 {
-	Solver *constructSolverChain(STPSolver *stpSolver,
-								 std::string querySMT2LogPath,
-								 std::string baseSolverQuerySMT2LogPath,
-								 std::string queryPCLogPath,
-								 std::string baseSolverQueryPCLogPath)
+        Solver *constructSolverChain(Solver *coreSolver,
+                                     std::string querySMT2LogPath,
+                                     std::string baseSolverQuerySMT2LogPath,
+                                     std::string queryPCLogPath,
+                                     std::string baseSolverQueryPCLogPath)
 	{
-	  Solver *solver = stpSolver;
+	  Solver *solver = coreSolver;
 
 	  if (optionIsSet(queryLoggingOptions, SOLVER_PC))
 	  {
@@ -55,7 +55,7 @@ namespace klee
 		solver = createIndependentSolver(solver);
 
 	  if (DebugValidateSolver)
-		solver = createValidatingSolver(solver, stpSolver);
+		solver = createValidatingSolver(solver, coreSolver);
 
 	  if (optionIsSet(queryLoggingOptions, ALL_PC))
 	  {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 309c5fd5..b57b1956 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -251,16 +251,17 @@ Executor::Executor(const InterpreterOptions &opts,
     coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
       ? std::min(MaxCoreSolverTime,MaxInstructionTime)
       : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
+      
   if (coreSolverTimeout) UseForkedCoreSolver = true;
-  STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+  Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);  
   Solver *solver = 
-    constructSolverChain(stpSolver,
+    constructSolverChain(coreSolver,
                          interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
                          interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
                          interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
                          interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
   
-  this->solver = new TimingSolver(solver, stpSolver);
+  this->solver = new TimingSolver(solver);
 
   memory = new MemoryManager();
 }
@@ -3280,7 +3281,7 @@ void Executor::getConstraintLog(const ExecutionState &state,
   case STP:
   {
 	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-	  char *log = solver->stpSolver->getConstraintLog(query);
+	  char *log = solver->getConstraintLog(query);
 	  res = std::string(log);
 	  free(log);
   }
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) {
-- 
cgit 1.4.1