From 9abe9572e68748002d8bbb789587e2a036ff760d Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 16:15:56 +0100 Subject: Renaming solver-related command-line options in order to decouple them from STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well. --- lib/Basic/CmdLineOptions.cpp | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'lib/Basic') diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 6fe20b7e..ac0474fb 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -40,9 +40,20 @@ MinQueryTimeToLog("min-query-time-to-log", "Set this param to a negative value to log timeouts only.")); llvm::cl::opt -MaxSTPTime("max-stp-time", - llvm::cl::desc("Maximum amount of time for a single query (default=0s (off)). Enables --use-forked-stp"), - llvm::cl::init(0.0)); +MaxCoreSolverTime("max-solver-time", + llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"), + llvm::cl::init(0.0), + llvm::cl::value_desc("seconds")); + +llvm::cl::opt +UseForkedCoreSolver("use-forked-solver", + llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"), + llvm::cl::init(true)); + +llvm::cl::opt +CoreSolverOptimizeDivides("solver-optimize-divides", + llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"), + llvm::cl::init(true)); /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking -- cgit 1.4.1