Introduced a constraint solving option category to which all the options in CmdLineOptions.cpp are currently added.

2 files changed, 59 insertions, 17 deletions

diff --git a/include/klee/OptionCategories.h b/include/klee/OptionCategories.h
new file mode 100644
index 00000000..34783d77
--- /dev/null
+++ b/include/klee/OptionCategories.h
@@ -0,0 +1,23 @@
+//===-- OptionCategories.h --------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/*
+ * This header defines the option categories used in KLEE.
+ */
+
+#ifndef KLEE_SOLVERCOMMANDLINE_H
+#define KLEE_SOLVERCOMMANDLINE_H
+
+#include "llvm/Support/CommandLine.h"
+
+namespace klee {
+  extern cl::OptionCategory SolvingCat;
+}
+
+#endif
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index b071eab6..fc856096 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -12,8 +12,9 @@
  * data that are common to both KLEE and Kleaver.
  */
 
-#include "klee/SolverCmdLine.h"
 #include "klee/Config/Version.h"
+#include "klee/SolverCmdLine.h"
+#include "klee/OptionCategories.h"
 
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/StringMap.h"
@@ -32,53 +33,66 @@ cl::extrahelp TimeFormatInfo(
   "       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("(default=off)"));
+                 cl::init(false),
+                 cl::desc("(default=off)"),
+                 cl::cat(SolvingCat));
 
 cl::opt<bool>
 UseCexCache("use-cex-cache",
             cl::init(true),
-            cl::desc("Use counterexample caching (default=on)"));
+            cl::desc("Use counterexample caching (default=on)"),
+            cl::cat(SolvingCat));
 
 cl::opt<bool>
 UseCache("use-cache",
          cl::init(true),
-         cl::desc("Use validity caching (default=on)"));
+         cl::desc("Use validity caching (default=on)"),
+         cl::cat(SolvingCat));
 
 cl::opt<bool>
 UseIndependentSolver("use-independent-solver",
                      cl::init(true),
-                     cl::desc("Use constraint independence (default=on)"));
+                     cl::desc("Use constraint independence (default=on)"),
+                     cl::cat(SolvingCat));
 
 cl::opt<bool>
 DebugValidateSolver("debug-validate-solver",
-                    cl::init(false));
+                    cl::init(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)"));
+                           "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::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::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=on)"),
-                    cl::init(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 to core SMT solver (default=off)"),
-                          cl::init(false));
+                          cl::init(false),
+                          cl::cat(SolvingCat));
 
 cl::bits<QueryLoggingSolverType>
 queryLoggingOptions("use-query-log",
@@ -88,11 +102,13 @@ queryLoggingOptions("use-query-log",
                                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::CommaSeparated,
+                    cl::cat(SolvingCat));
 
 cl::opt<bool>
 UseAssignmentValidatingSolver("debug-assignment-validating-solver",
-                              cl::init(false));
+                              cl::init(false),
+                              cl::cat(SolvingCat));
 
 void KCommandLine::HideUnrelatedOptions(cl::OptionCategory &Category) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 7)
@@ -146,7 +162,8 @@ MetaSMTBackend("metasmt-backend",
                           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::init(METASMT_DEFAULT_BACKEND),
+               cl::cat(SolvingCat));
 
 #undef METASMT_DEFAULT_BACKEND
 #undef METASMT_DEFAULT_BACKEND_STR
@@ -181,7 +198,8 @@ CoreSolverToUse("solver-backend", cl::desc("Specifiy the core solver backend to
                            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::init(DEFAULT_CORE_SOLVER),
+                cl::cat(SolvingCat));
 
 cl::opt<CoreSolverType>
 DebugCrossCheckCoreSolverWith("debug-crosscheck-core-solver",
@@ -193,7 +211,8 @@ DebugCrossCheckCoreSolverWith("debug-crosscheck-core-solver",
                                          clEnumValN(NO_SOLVER, "none",
                                                     "Do not cross check (default)")
                                          KLEE_LLVM_CL_VAL_END),
-                              cl::init(NO_SOLVER));
+                              cl::init(NO_SOLVER),
+                              cl::cat(SolvingCat));
 }
 
 #undef STP_IS_DEFAULT_STR