klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ConstructSolverChain.cpp
Go to the documentation of this file.
1 //===-- ConstructSolverChain.cpp ------------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 /*
11  * This file groups declarations that are common to both KLEE and Kleaver.
12  */
13 #include "klee/Common.h"
14 #include "klee/CommandLine.h"
15 #include "llvm/Support/raw_ostream.h"
16 
17 namespace klee
18 {
20  std::string querySMT2LogPath,
21  std::string baseSolverQuerySMT2LogPath,
22  std::string queryPCLogPath,
23  std::string baseSolverQueryPCLogPath)
24  {
25  Solver *solver = coreSolver;
26 
28  {
29  solver = createPCLoggingSolver(solver,
30  baseSolverQueryPCLogPath,
32  llvm::errs() << "Logging queries that reach solver in .pc format to "
33  << baseSolverQueryPCLogPath.c_str() << "\n";
34  }
35 
37  {
38  solver = createSMTLIBLoggingSolver(solver,
39  baseSolverQuerySMT2LogPath,
41  llvm::errs() << "Logging queries that reach solver in .smt2 format to "
42  << baseSolverQuerySMT2LogPath.c_str() << "\n";
43  }
44 
45  if (UseFastCexSolver)
46  solver = createFastCexSolver(solver);
47 
48  if (UseCexCache)
49  solver = createCexCachingSolver(solver);
50 
51  if (UseCache)
52  solver = createCachingSolver(solver);
53 
55  solver = createIndependentSolver(solver);
56 
58  solver = createValidatingSolver(solver, coreSolver);
59 
61  {
62  solver = createPCLoggingSolver(solver,
63  queryPCLogPath,
65  llvm::errs() << "Logging all queries in .pc format to "
66  << queryPCLogPath.c_str() << "\n";
67  }
68 
70  {
71  solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
73  llvm::errs() << "Logging all queries in .smt2 format to "
74  << querySMT2LogPath.c_str() << "\n";
75  }
76 
77  return solver;
78  }
79 
80 }
81 
82 
Solver * createSMTLIBLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)
Solver * createFastCexSolver(Solver *s)
llvm::cl::opt< int > MinQueryTimeToLog
Log all queries (un-optimised) in .pc (KQuery) format.
Definition: CommandLine.h:35
Solver * createCachingSolver(Solver *s)
Log queries passed to solver (optimised) in .pc (KQuery) format.
Definition: CommandLine.h:37
llvm::cl::opt< bool > UseCache
Log all queries (un-optimised) .smt2 (SMT-LIBv2) format.
Definition: CommandLine.h:36
llvm::cl::opt< bool > DebugValidateSolver
static bool optionIsSet(llvm::cl::list< T > list, T option)
Definition: CommandLine.h:63
Solver * createIndependentSolver(Solver *s)
llvm::cl::list< QueryLoggingSolverType > queryLoggingOptions
llvm::cl::opt< bool > UseFastCexSolver
Solver * createValidatingSolver(Solver *s, Solver *oracle)
Definition: Solver.cpp:450
llvm::cl::opt< bool > UseCexCache
llvm::cl::opt< bool > UseIndependentSolver
Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format.
Definition: CommandLine.h:38
Solver * createPCLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)
Solver * createCexCachingSolver(Solver *s)
Solver * constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryPCLogPath, std::string baseSolverQueryPCLogPath)