From e1f055b1785fd7f23fc4d30eeb0276278892ed20 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Thu, 15 Aug 2019 22:32:39 +0100
Subject: Moved ConstructSolverChain.cpp to the Solver library.

---
 lib/Basic/CMakeLists.txt           | 10 -----
 lib/Basic/ConstructSolverChain.cpp | 77 --------------------------------------
 2 files changed, 87 deletions(-)
 delete mode 100644 lib/Basic/ConstructSolverChain.cpp

(limited to 'lib/Basic')

diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt
index 78890ea6..d156116f 100644
--- a/lib/Basic/CMakeLists.txt
+++ b/lib/Basic/CMakeLists.txt
@@ -7,7 +7,6 @@
 #
 #===------------------------------------------------------------------------===#
 klee_add_component(kleeBasic
-  ConstructSolverChain.cpp
   KTest.cpp
   Statistics.cpp
 )
@@ -17,12 +16,3 @@ set(LLVM_COMPONENTS
 
 klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS})
 target_link_libraries(kleeBasic PUBLIC ${LLVM_LIBS})
-
-target_link_libraries(kleeBasic PRIVATE
-  # FIXME: THIS IS STUPID.
-  # `ConstructSolverChain.cpp` should be in
-  # `kleaverSolver` not in in `kleeBasic`.
-  # We are creating a circular dependency because
-  # of this because `kleaverSolver` depends on `kleeBasic`.
-  kleaverSolver
-)
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
deleted file mode 100644
index 39e0e824..00000000
--- a/lib/Basic/ConstructSolverChain.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-//===-- ConstructSolverChain.cpp ------------------------------------++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-/*
- * This file groups declarations that are common to both KLEE and Kleaver.
- */
-#include "klee/Common.h"
-#include "klee/SolverCmdLine.h"
-#include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/Internal/System/Time.h"
-#include "llvm/Support/raw_ostream.h"
-
-
-namespace klee {
-Solver *constructSolverChain(Solver *coreSolver,
-                             std::string querySMT2LogPath,
-                             std::string baseSolverQuerySMT2LogPath,
-                             std::string queryKQueryLogPath,
-                             std::string baseSolverQueryKQueryLogPath) {
-  Solver *solver = coreSolver;
-  const time::Span minQueryTimeToLog(MinQueryTimeToLog);
-
-  if (QueryLoggingOptions.isSet(SOLVER_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
-    klee_message("Logging queries that reach solver in .kquery format to %s\n",
-                 baseSolverQueryKQueryLogPath.c_str());
-  }
-
-  if (QueryLoggingOptions.isSet(SOLVER_SMTLIB)) {
-    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
-    klee_message("Logging queries that reach solver in .smt2 format to %s\n",
-                 baseSolverQuerySMT2LogPath.c_str());
-  }
-
-  if (UseAssignmentValidatingSolver)
-    solver = createAssignmentValidatingSolver(solver);
-
-  if (UseFastCexSolver)
-    solver = createFastCexSolver(solver);
-
-  if (UseCexCache)
-    solver = createCexCachingSolver(solver);
-
-  if (UseBranchCache)
-    solver = createCachingSolver(solver);
-
-  if (UseIndependentSolver)
-    solver = createIndependentSolver(solver);
-
-  if (DebugValidateSolver)
-    solver = createValidatingSolver(solver, coreSolver);
-
-  if (QueryLoggingOptions.isSet(ALL_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
-    klee_message("Logging all queries in .kquery format to %s\n",
-                 queryKQueryLogPath.c_str());
-  }
-
-  if (QueryLoggingOptions.isSet(ALL_SMTLIB)) {
-    solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
-    klee_message("Logging all queries in .smt2 format to %s\n",
-                 querySMT2LogPath.c_str());
-  }
-  if (DebugCrossCheckCoreSolverWith != NO_SOLVER) {
-    Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith);
-    solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver);
-  }
-
-  return solver;
-}
-}
-- 
cgit 1.4.1