kleaver: Add some command line options for choosing the Solver.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73485 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 17 insertions, 2 deletions

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index e45b65d0..07de2784 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -62,6 +62,18 @@ namespace {
               clEnumValN(SimplifyingBuilder, "simplify",
                          "Fold constants and simplify expressions."),
               clEnumValEnd));
+
+  cl::opt<bool>
+  UseDummySolver("use-dummy-solver",
+		   cl::init(false));
+
+  cl::opt<bool>
+  UseFastCexSolver("use-fast-cex-solver",
+		   cl::init(false));
+  
+  cl::opt<bool>
+  UseSTPQueryPCLog("use-stp-query-pc-log",
+                   cl::init(false));
 }
 
 static std::string escapedString(const char *start, unsigned length) {
@@ -149,8 +161,11 @@ static bool EvaluateInputAST(const char *Filename,
     return false;
 
   // FIXME: Support choice of solver.
-  Solver *S, *STP = S = new STPSolver(true);
-  if (0)
+  Solver *S, *STP = S = 
+    UseDummySolver ? createDummySolver() : new STPSolver(true);
+  if (UseSTPQueryPCLog)
+    S = createPCLoggingSolver(S, "stp-queries.pc");
+  if (UseFastCexSolver)
     S = createFastCexSolver(S);
   S = createCexCachingSolver(S);
   S = createCachingSolver(S);