From 2a6a0ca7e8db2c300f833e5623dc61993d149e8c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Mon, 11 Mar 2013 17:33:37 +0000 Subject: 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 --- lib/Basic/ConstructSolverChain.cpp | 77 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 lib/Basic/ConstructSolverChain.cpp (limited to 'lib/Basic/ConstructSolverChain.cpp') 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 +#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; + } + +} + + -- cgit 1.4.1