diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-07 12:00:25 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-12 11:40:39 +0000 |
| commit | e81f5ceed580d4d267e3c857b47637d6bd065499 (patch) | |
| tree | eb9f3b74b036a59edd1164bc68e9e00d5156936d /include | |
| parent | 9da07ca0ccc58286f8247bc2e7d7745abfa0cc54 (diff) | |
| download | klee-e81f5ceed580d4d267e3c857b47637d6bd065499.tar.gz | |
Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing
a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles...
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/CommandLine.h | 6 | ||||
| -rw-r--r-- | include/klee/Solver.h | 5 |
2 files changed, 8 insertions, 3 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index c4c70069..44f1afd4 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -44,17 +44,19 @@ enum QueryLoggingSolverType */ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions; +enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER }; +extern llvm::cl::opt<CoreSolverType> CoreSolverToUse; + #ifdef SUPPORT_METASMT enum MetaSMTBackendType { - METASMT_BACKEND_NONE, METASMT_BACKEND_STP, METASMT_BACKEND_Z3, METASMT_BACKEND_BOOLECTOR }; -extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT; +extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend; #endif /* SUPPORT_METASMT */ diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 906309d2..e3adac6a 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -10,6 +10,7 @@ #ifndef KLEE_SOLVER_H #define KLEE_SOLVER_H +#include "klee/CommandLine.h" // FIXME: This is just for CoreSolverType #include "klee/Expr.h" #include <vector> @@ -290,7 +291,9 @@ namespace klee { /// createDummySolver - Create a dummy solver implementation which always /// fails. Solver *createDummySolver(); - + + // Create a solver based on the supplied ``CoreSolverType``. + Solver *createCoreSolver(CoreSolverType cst); } #endif |