Patch by Hristina Palikareva which enables Kleaver to configure the

solver chain.



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

3 files changed, 23 insertions, 20 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 4b537174..c8397cf1 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -20,6 +20,21 @@ llvm::cl::opt<bool>
 UseFastCexSolver("use-fast-cex-solver",
 		 llvm::cl::init(false),
 		 llvm::cl::desc("(default=off)"));
+
+llvm::cl::opt<bool>
+UseCexCache("use-cex-cache",
+            llvm::cl::init(true),
+            llvm::cl::desc("Use counterexample caching (default=on)"));
+
+llvm::cl::opt<bool>
+UseCache("use-cache",
+         llvm::cl::init(true),
+         llvm::cl::desc("Use validity caching (default=on)"));
+
+llvm::cl::opt<bool>
+UseIndependentSolver("use-independent-solver",
+                     llvm::cl::init(true),
+                     llvm::cl::desc("Use constraint independence (default=on)"));
   
 llvm::cl::opt<int>
 MinQueryTimeToLog("min-query-time-to-log",
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f3278c89..a0c4de1c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -145,31 +145,16 @@ namespace {
 			      cl::desc("Only output test cases covering new code."));
 
   cl::opt<bool>
-  UseIndependentSolver("use-independent-solver",
-                       cl::init(true),
-		       cl::desc("Use constraint independence (default=on)"));
-
-  cl::opt<bool>
   EmitAllErrors("emit-all-errors",
                 cl::init(false),
                 cl::desc("Generate tests cases for all errors "
                          "(default=off, i.e. one per (error,instruction) pair)"));
-
-  cl::opt<bool>
-  UseCexCache("use-cex-cache",
-              cl::init(true),
-	      cl::desc("Use counterexample caching (default=on)"));
-   
+  
   cl::opt<bool>
   NoExternals("no-externals", 
            cl::desc("Do not allow external function calls (default=off)"));
 
   cl::opt<bool>
-  UseCache("use-cache",
-	   cl::init(true),
-	   cl::desc("Use validity caching (default=on)"));
-
-  cl::opt<bool>
   AlwaysOutputSeeds("always-output-seeds",
 		    cl::init(true));
 
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 00034eb1..00ffc92f 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -183,10 +183,13 @@ static bool EvaluateInputAST(const char *Filename,
   if (true == optionIsSet(queryLoggingOptions, SOLVER_PC))
     S = createPCLoggingSolver(S, SOLVER_QUERIES_PC_FILE_NAME, MinQueryTimeToLog);
   if (UseFastCexSolver)
-    S = createFastCexSolver(S);
-  S = createCexCachingSolver(S);
-  S = createCachingSolver(S);
-  S = createIndependentSolver(S);
+    S = createFastCexSolver(S);  
+  if (UseCexCache)
+    S = createCexCachingSolver(S);
+  if (UseCache)
+    S = createCachingSolver(S);
+  if (UseIndependentSolver)
+    S = createIndependentSolver(S);
   if (0)
     S = createValidatingSolver(S, STP);