Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated header SolverCmdLine.h) and moved it to the Solver library.

2 files changed, 0 insertions, 221 deletions

diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt
index d0a309c9..78890ea6 100644
--- a/lib/Basic/CMakeLists.txt
+++ b/lib/Basic/CMakeLists.txt
@@ -7,7 +7,6 @@
 #
 #===------------------------------------------------------------------------===#
 klee_add_component(kleeBasic
-  CmdLineOptions.cpp
   ConstructSolverChain.cpp
   KTest.cpp
   Statistics.cpp
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
deleted file mode 100644
index 9e190840..00000000
--- a/lib/Basic/CmdLineOptions.cpp
+++ /dev/null
@@ -1,220 +0,0 @@
-//===-- CmdLineOptions.cpp --------------------------------------*- C++ -*-===//
-//
-//                     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 command line options definitions and associated
- * data that are common to both KLEE and Kleaver.
- */
-
-#include "klee/Config/Version.h"
-#include "klee/SolverCmdLine.h"
-#include "klee/OptionCategories.h"
-
-#include "llvm/ADT/ArrayRef.h"
-#include "llvm/ADT/StringMap.h"
-#include "llvm/Support/CommandLine.h"
-
-using namespace llvm;
-
-namespace klee {
-
-cl::extrahelp TimeFormatInfo(
-    "\nTime format used by KLEE's options\n"
-    "\n"
-    "  Time spans can be specified in two ways:\n"
-    "    1. As positive real numbers representing seconds, e.g. '10', '3.5' "
-    "but not 'INF', 'NaN', '1e3', '-4.5s'\n"
-    "    2. As a sequence of natural numbers with specified units, e.g. "
-    "'1h10min' (= '70min'), '5min10s' but not '3.5min', '8S'\n"
-    "       The following units are supported: h, min, s, ms, us, ns.\n");
-
-cl::OptionCategory SolvingCat("Constraint solving options",
-                              "These options impact constraint solving.");
-
-cl::opt<bool> UseFastCexSolver(
-    "use-fast-cex-solver", cl::init(false),
-    cl::desc("Enable an experimental range-based solver (default=false)"),
-    cl::cat(SolvingCat));
-
-cl::opt<bool> UseCexCache("use-cex-cache", cl::init(true),
-                          cl::desc("Use the counterexample cache (default=true)"),
-                          cl::cat(SolvingCat));
-
-cl::opt<bool> UseBranchCache("use-branch-cache", cl::init(true),
-                             cl::desc("Use the branch cache (default=true)"),
-                             cl::cat(SolvingCat));
-
-cl::opt<bool>
-    UseIndependentSolver("use-independent-solver", cl::init(true),
-                         cl::desc("Use constraint independence (default=true)"),
-                         cl::cat(SolvingCat));
-
-cl::opt<bool> DebugValidateSolver(
-    "debug-validate-solver", cl::init(false),
-    cl::desc("Crosscheck the results of the solver chain above the core solver "
-             "with the results of the core solver (default=false)"),
-    cl::cat(SolvingCat));
-
-cl::opt<std::string> MinQueryTimeToLog(
-    "min-query-time-to-log",
-    cl::desc("Set time threshold for queries logged in files. "
-             "Only queries longer than threshold will be logged. (default=0s)"),
-    cl::cat(SolvingCat));
-
-cl::opt<bool>
-    LogTimedOutQueries("log-timed-out-queries", cl::init(true),
-                       cl::desc("Log queries that timed out. (default=true)."),
-                       cl::cat(SolvingCat));
-
-cl::opt<std::string> MaxCoreSolverTime(
-    "max-solver-time",
-    cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). "
-             "Enables --use-forked-solver"),
-    cl::cat(SolvingCat));
-
-cl::opt<bool> UseForkedCoreSolver(
-    "use-forked-solver",
-    cl::desc("Run the core SMT solver in a forked process (default=true)"),
-    cl::init(true), cl::cat(SolvingCat));
-
-cl::opt<bool> CoreSolverOptimizeDivides(
-    "solver-optimize-divides",
-    cl::desc("Optimize constant divides into add/shift/multiplies before "
-             "passing them to the core SMT solver (default=false)"),
-    cl::init(false), cl::cat(SolvingCat));
-
-cl::bits<QueryLoggingSolverType> QueryLoggingOptions(
-    "use-query-log",
-    cl::desc("Log queries to a file. Multiple options can be specified "
-             "separated by a comma. By default nothing is logged."),
-    cl::values(
-        clEnumValN(ALL_KQUERY, "all:kquery",
-                   "All queries in .kquery (KQuery) format"),
-        clEnumValN(ALL_SMTLIB, "all:smt2",
-                   "All queries in .smt2 (SMT-LIBv2) format"),
-        clEnumValN(
-            SOLVER_KQUERY, "solver:kquery",
-            "All queries reaching the solver in .kquery (KQuery) format"),
-        clEnumValN(
-            SOLVER_SMTLIB, "solver:smt2",
-            "All queries reaching the solver in .smt2 (SMT-LIBv2) format")
-            KLEE_LLVM_CL_VAL_END),
-    cl::CommaSeparated, cl::cat(SolvingCat));
-
-cl::opt<bool> UseAssignmentValidatingSolver(
-    "debug-assignment-validating-solver", cl::init(false),
-    cl::desc("Debug the correctness of generated assignments (default=false)"),
-    cl::cat(SolvingCat));
-
-
-void KCommandLine::HideOptions(llvm::cl::OptionCategory &Category) {
-  StringMap<cl::Option *> &map = cl::getRegisteredOptions();
-
-  for (auto &elem : map) {
-    if (elem.second->Category == &Category) {
-      elem.second->setHiddenFlag(cl::Hidden);
-    }
-  }
-}
-
-void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) {
-  StringMap<cl::Option *> &map = cl::getRegisteredOptions();
-  for (StringMap<cl::Option *>::iterator i = map.begin(), e = map.end(); i != e;
-       i++) {
-    if (i->second->Category != &Category) {
-      i->second->setHiddenFlag(cl::Hidden);
-    }
-  }
-}
-
-#ifdef ENABLE_METASMT
-
-#ifdef METASMT_DEFAULT_BACKEND_IS_BTOR
-#define METASMT_DEFAULT_BACKEND_STR "(default = btor)."
-#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_BOOLECTOR
-#elif METASMT_DEFAULT_BACKEND_IS_Z3
-#define METASMT_DEFAULT_BACKEND_STR "(default = z3)."
-#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3
-#elif METASMT_DEFAULT_BACKEND_IS_CVC4
-#define METASMT_DEFAULT_BACKEND_STR "(default = cvc4)."
-#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_CVC4
-#elif METASMT_DEFAULT_BACKEND_IS_YICES2
-#define METASMT_DEFAULT_BACKEND_STR "(default = yices2)."
-#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_YICES2
-#else
-#define METASMT_DEFAULT_BACKEND_STR "(default = stp)."
-#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP
-#endif
-
-cl::opt<klee::MetaSMTBackendType>
-MetaSMTBackend("metasmt-backend",
-               cl::desc("Specify the MetaSMT solver backend type " METASMT_DEFAULT_BACKEND_STR),
-               cl::values(clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
-                          clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
-                          clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor",
-                                     "Use metaSMT with Boolector"),
-                          clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"),
-                          clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2")
-                          KLEE_LLVM_CL_VAL_END),
-               cl::init(METASMT_DEFAULT_BACKEND),
-               cl::cat(SolvingCat));
-
-#undef METASMT_DEFAULT_BACKEND
-#undef METASMT_DEFAULT_BACKEND_STR
-
-#endif /* ENABLE_METASMT */
-
-// Pick the default core solver based on configuration
-#ifdef ENABLE_STP
-#define STP_IS_DEFAULT_STR " (default)"
-#define METASMT_IS_DEFAULT_STR ""
-#define Z3_IS_DEFAULT_STR ""
-#define DEFAULT_CORE_SOLVER STP_SOLVER
-#elif ENABLE_Z3
-#define STP_IS_DEFAULT_STR ""
-#define METASMT_IS_DEFAULT_STR ""
-#define Z3_IS_DEFAULT_STR " (default)"
-#define DEFAULT_CORE_SOLVER Z3_SOLVER
-#elif ENABLE_METASMT
-#define STP_IS_DEFAULT_STR ""
-#define METASMT_IS_DEFAULT_STR " (default)"
-#define Z3_IS_DEFAULT_STR ""
-#define DEFAULT_CORE_SOLVER METASMT_SOLVER
-#define Z3_IS_DEFAULT_STR ""
-#else
-#error "Unsupported solver configuration"
-#endif
-
-cl::opt<CoreSolverType> CoreSolverToUse(
-    "solver-backend", cl::desc("Specifiy the core solver backend to use"),
-    cl::values(clEnumValN(STP_SOLVER, "stp", "STP" STP_IS_DEFAULT_STR),
-               clEnumValN(METASMT_SOLVER, "metasmt",
-                          "metaSMT" METASMT_IS_DEFAULT_STR),
-               clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
-               clEnumValN(Z3_SOLVER, "z3", "Z3" Z3_IS_DEFAULT_STR)
-                   KLEE_LLVM_CL_VAL_END),
-    cl::init(DEFAULT_CORE_SOLVER), cl::cat(SolvingCat));
-
-cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith(
-    "debug-crosscheck-core-solver",
-    cl::desc(
-        "Specifiy a solver to use for crosschecking the results of the core solver"),
-    cl::values(clEnumValN(STP_SOLVER, "stp", "STP"),
-               clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
-               clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
-               clEnumValN(Z3_SOLVER, "z3", "Z3"),
-               clEnumValN(NO_SOLVER, "none", "Do not crosscheck (default)")
-                   KLEE_LLVM_CL_VAL_END),
-    cl::init(NO_SOLVER), cl::cat(SolvingCat));
-} // namespace klee
-
-#undef STP_IS_DEFAULT_STR
-#undef METASMT_IS_DEFAULT_STR
-#undef Z3_IS_DEFAULT_STR
-#undef DEFAULT_CORE_SOLVER