Patch by Dan Liew which unifies the solver construction between KLEE

and Kleaver and fixes --use-query-log in Kleaver.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176811 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 4 insertions, 58 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 714ae131..bc4c0023 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -26,6 +26,10 @@ llvm::cl::opt<bool>
 UseIndependentSolver("use-independent-solver",
                      llvm::cl::init(true),
                      llvm::cl::desc("Use constraint independence (default=on)"));
+
+llvm::cl::opt<bool>
+DebugValidateSolver("debug-validate-solver",
+		             llvm::cl::init(false));
   
 llvm::cl::opt<int>
 MinQueryTimeToLog("min-query-time-to-log",
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index ec053597..3f90c426 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -131,10 +131,6 @@ namespace {
                   cl::init(0));
 
   cl::opt<bool>
-  DebugValidateSolver("debug-validate-solver",
-		      cl::init(false));
-
-  cl::opt<bool>
   SuppressExternalWarnings("suppress-external-warnings");
 
   cl::opt<bool>
@@ -242,60 +238,6 @@ namespace klee {
   RNG theRNG;
 }
 
-Solver *constructSolverChain(STPSolver *stpSolver,
-                             std::string querySMT2LogPath,
-                             std::string baseSolverQuerySMT2LogPath,
-                             std::string queryPCLogPath,
-                             std::string baseSolverQueryPCLogPath) {
-  Solver *solver = stpSolver;
-
-  if (optionIsSet(queryLoggingOptions,SOLVER_PC))
-  {
-    solver = createPCLoggingSolver(solver, 
-                                   baseSolverQueryPCLogPath,
-		                   MinQueryTimeToLog);
-    klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str());
-  }
-
-  if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
-  {
-    solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath,
-                                       MinQueryTimeToLog);
-    klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
-  }
-
-  if (UseFastCexSolver)
-    solver = createFastCexSolver(solver);
-
-  if (UseCexCache)
-    solver = createCexCachingSolver(solver);
-
-  if (UseCache)
-    solver = createCachingSolver(solver);
-
-  if (UseIndependentSolver)
-    solver = createIndependentSolver(solver);
-
-  if (DebugValidateSolver)
-    solver = createValidatingSolver(solver, stpSolver);
-
-  if (optionIsSet(queryLoggingOptions,ALL_PC))
-  {
-    solver = createPCLoggingSolver(solver, 
-                                   queryPCLogPath,
-                                   MinQueryTimeToLog);
-    klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str());
-  }
-  
-  if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
-  {
-    solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
-                                       MinQueryTimeToLog);
-    klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
-  }
-
-  return solver;
-}
 
 Executor::Executor(const InterpreterOptions &opts,
                    InterpreterHandler *ih)