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.

5 files changed, 25 insertions, 33 deletions

diff --git a/include/klee/Common.h b/include/klee/Common.h
index 1418f1b6..7149708a 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -22,7 +22,7 @@ namespace klee {
     const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc";
     const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc";
 
-    Solver *constructSolverChain(STPSolver *stpSolver,
+    Solver *constructSolverChain(Solver *coreSolver,
                                  std::string querySMT2LogPath,
                                  std::string baseSolverQuerySMT2LogPath,
                                  std::string queryPCLogPath,
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) {
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 6c2a29e5..accc48e4 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -211,25 +211,19 @@ static bool EvaluateInputAST(const char *Filename,
     return false;
 
   // FIXME: Support choice of solver.
-  Solver *S   = 0;
-  Solver *STP = 0;
+  Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+  
   if (!UseDummySolver) {
-    STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver);
     if (0 != MaxCoreSolverTime) {
-      stpSolver->setCoreSolverTimeout(MaxCoreSolverTime);    
+      coreSolver->setCoreSolverTimeout(MaxCoreSolverTime);
     }
-    STP = S = stpSolver;
-  }
-  else {
-    STP = S = createDummySolver(); 
   }
 
-  S= constructSolverChain((STPSolver*) STP,
-		  	  	  	      getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
-		  	  	  	      getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
-		  	  	  	      getQueryLogPath(ALL_QUERIES_PC_FILE_NAME),
-		  	  	  	      getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME));
-
+  Solver *S = constructSolverChain(coreSolver,
+                                   getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
+                                   getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
+                                   getQueryLogPath(ALL_QUERIES_PC_FILE_NAME),
+                                   getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME));
 
   unsigned Index = 0;
   for (std::vector<Decl*>::iterator it = Decls.begin(),