about summary refs log tree commit diff homepage
path: root/lib/Basic/ConstructSolverChain.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Basic/ConstructSolverChain.cpp')
-rw-r--r--lib/Basic/ConstructSolverChain.cpp98
1 files changed, 42 insertions, 56 deletions
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 59790551..b48c5cb0 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -1,4 +1,4 @@
-//===-- ConstructSolverChain.cpp ------------------------------------------------*- C++ -*-===//
+//===-- ConstructSolverChain.cpp ------------------------------------++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -14,69 +14,55 @@
 #include "klee/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
-namespace klee
-{
-        Solver *constructSolverChain(Solver *coreSolver,
-                                     std::string querySMT2LogPath,
-                                     std::string baseSolverQuerySMT2LogPath,
-                                     std::string queryPCLogPath,
-                                     std::string baseSolverQueryPCLogPath)
-	{
-	  Solver *solver = coreSolver;
+namespace klee {
+Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
+                             std::string baseSolverQuerySMT2LogPath,
+                             std::string queryPCLogPath,
+                             std::string baseSolverQueryPCLogPath) {
+  Solver *solver = coreSolver;
 
-	  if (optionIsSet(queryLoggingOptions, SOLVER_PC))
-	  {
-		solver = createPCLoggingSolver(solver,
-					       baseSolverQueryPCLogPath,
-					       MinQueryTimeToLog);
-		llvm::errs() << "Logging queries that reach solver in .pc format to "
-			  << baseSolverQueryPCLogPath.c_str() << "\n";
-	  }
+  if (optionIsSet(queryLoggingOptions, SOLVER_PC)) {
+    solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath,
+                                   MinQueryTimeToLog);
+    llvm::errs() << "Logging queries that reach solver in .pc format to "
+                 << baseSolverQueryPCLogPath.c_str() << "\n";
+  }
 
-	  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB))
-	  {
-		solver = createSMTLIBLoggingSolver(solver,
-						   baseSolverQuerySMT2LogPath,
-						   MinQueryTimeToLog);
-		llvm::errs() << "Logging queries that reach solver in .smt2 format to "
-			  << baseSolverQuerySMT2LogPath.c_str() << "\n";
-	  }
+  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
+    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
+                                       MinQueryTimeToLog);
+    llvm::errs() << "Logging queries that reach solver in .smt2 format to "
+                 << baseSolverQuerySMT2LogPath.c_str() << "\n";
+  }
 
-	  if (UseFastCexSolver)
-		solver = createFastCexSolver(solver);
+  if (UseFastCexSolver)
+    solver = createFastCexSolver(solver);
 
-	  if (UseCexCache)
-		solver = createCexCachingSolver(solver);
+  if (UseCexCache)
+    solver = createCexCachingSolver(solver);
 
-	  if (UseCache)
-		solver = createCachingSolver(solver);
+  if (UseCache)
+    solver = createCachingSolver(solver);
 
-	  if (UseIndependentSolver)
-		solver = createIndependentSolver(solver);
+  if (UseIndependentSolver)
+    solver = createIndependentSolver(solver);
 
-	  if (DebugValidateSolver)
-		solver = createValidatingSolver(solver, coreSolver);
+  if (DebugValidateSolver)
+    solver = createValidatingSolver(solver, coreSolver);
 
-	  if (optionIsSet(queryLoggingOptions, ALL_PC))
-	  {
-		solver = createPCLoggingSolver(solver,
-					       queryPCLogPath,
-					       MinQueryTimeToLog);
-		llvm::errs() << "Logging all queries in .pc format to "
-			  << queryPCLogPath.c_str() << "\n";
-	  }
+  if (optionIsSet(queryLoggingOptions, ALL_PC)) {
+    solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog);
+    llvm::errs() << "Logging all queries in .pc format to "
+                 << queryPCLogPath.c_str() << "\n";
+  }
 
-	  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB))
-	  {
-		solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
-						   MinQueryTimeToLog);
-		llvm::errs() << "Logging all queries in .smt2 format to "
-			  << querySMT2LogPath.c_str() << "\n";
-	  }
-
-	  return solver;
-	}
+  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {
+    solver =
+        createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
+    llvm::errs() << "Logging all queries in .smt2 format to "
+                 << querySMT2LogPath.c_str() << "\n";
+  }
 
+  return solver;
+}
 }
-
-