Forgot to add ConstructSolverChain.cpp in the previous patch.

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

1 files changed, 77 insertions, 0 deletions

diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
new file mode 100644
index 00000000..0cd3dc31
--- /dev/null
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -0,0 +1,77 @@
+//===-- ConstructSolverChain.cpp ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/*
+ * This file groups declarations that are common to both KLEE and Kleaver.
+ */
+#include <iostream>
+#include "klee/Common.h"
+#include "klee/CommandLine.h"
+
+namespace klee
+{
+	Solver *constructSolverChain(STPSolver *stpSolver,
+								 std::string querySMT2LogPath,
+								 std::string baseSolverQuerySMT2LogPath,
+								 std::string queryPCLogPath,
+								 std::string baseSolverQueryPCLogPath)
+	{
+	  Solver *solver = stpSolver;
+
+	  if (optionIsSet(queryLoggingOptions,SOLVER_PC))
+	  {
+		solver = createPCLoggingSolver(solver,
+									   baseSolverQueryPCLogPath,
+							   MinQueryTimeToLog);
+		std::cerr << "Logging queries that reach solver in .pc format to " << baseSolverQueryPCLogPath.c_str() << std::endl;
+	  }
+
+	  if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
+	  {
+		solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath,
+										   MinQueryTimeToLog);
+		std::cerr << "Logging queries that reach solver in .smt2 format to " << baseSolverQuerySMT2LogPath.c_str() << std::endl;
+	  }
+
+	  if (UseFastCexSolver)
+		solver = createFastCexSolver(solver);
+
+	  if (UseCexCache)
+		solver = createCexCachingSolver(solver);
+
+	  if (UseCache)
+		solver = createCachingSolver(solver);
+
+	  if (UseIndependentSolver)
+		solver = createIndependentSolver(solver);
+
+	  if (DebugValidateSolver)
+		solver = createValidatingSolver(solver, stpSolver);
+
+	  if (optionIsSet(queryLoggingOptions,ALL_PC))
+	  {
+		solver = createPCLoggingSolver(solver,
+									   queryPCLogPath,
+									   MinQueryTimeToLog);
+		std::cerr << "Logging all queries in .pc format to " << queryPCLogPath.c_str() << std::endl;
+	  }
+
+	  if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
+	  {
+		solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
+										   MinQueryTimeToLog);
+		std::cerr << "Logging all queries in .smt2 format to " << querySMT2LogPath.c_str() << std::endl;
+	  }
+
+	  return solver;
+	}
+
+}
+
+