From 454dfc67045fbbc3358b28f855f3af0af31daf47 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Mon, 11 Mar 2013 17:11:06 +0000
Subject: 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
---
 lib/Core/Executor.cpp | 58 ---------------------------------------------------
 1 file changed, 58 deletions(-)

(limited to 'lib/Core')

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
@@ -130,10 +130,6 @@ namespace {
   MaxSymArraySize("max-sym-array-size",
                   cl::init(0));
 
-  cl::opt<bool>
-  DebugValidateSolver("debug-validate-solver",
-		      cl::init(false));
-
   cl::opt<bool>
   SuppressExternalWarnings("suppress-external-warnings");
 
@@ -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) 
-- 
cgit 1.4.1