#include "klee/Solver/SolverCmdLine.h"
#include "klee/Config/Version.h"
#include "klee/Support/OptionCategories.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/Support/CommandLine.h"

Include dependency graph for SolverCmdLine.cpp:

Namespaces
namespace	klee

Functions
cl::extrahelp	klee::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	klee::SolvingCat ("Constraint solving options", "These options impact constraint solving.")

cl::opt< bool >	klee::UseFastCexSolver ("use-fast-cex-solver", cl::init(false), cl::desc("Enable an experimental range-based solver (default=false)"), cl::cat(SolvingCat))

cl::opt< bool >	klee::UseCexCache ("use-cex-cache", cl::init(true), cl::desc("Use the counterexample cache (default=true)"), cl::cat(SolvingCat))

cl::opt< bool >	klee::UseBranchCache ("use-branch-cache", cl::init(true), cl::desc("Use the branch cache (default=true)"), cl::cat(SolvingCat))

cl::opt< bool >	klee::UseIndependentSolver ("use-independent-solver", cl::init(true), cl::desc("Use constraint independence (default=true)"), cl::cat(SolvingCat))

cl::opt< bool >	klee::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 >	klee::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 >	klee::LogTimedOutQueries ("log-timed-out-queries", cl::init(true), cl::desc("Log queries that timed out. (default=true)."), cl::cat(SolvingCat))

cl::opt< std::string >	klee::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 >	klee::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 >	klee::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 >	klee::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")), cl::CommaSeparated, cl::cat(SolvingCat))

cl::opt< bool >	klee::UseAssignmentValidatingSolver ("debug-assignment-validating-solver", cl::init(false), cl::desc("Debug the correctness of generated assignments (default=false)"), cl::cat(SolvingCat))

cl::opt< CoreSolverType >	klee::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)), cl::init(DEFAULT_CORE_SOLVER), cl::cat(SolvingCat))

cl::opt< CoreSolverType >	klee::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)")), cl::init(NO_SOLVER), cl::cat(SolvingCat))

Namespaces

Functions