1 //===-- CoreSolver.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 #include "STPSolver.h"
11 #include "Z3Solver.h"
12 #include "MetaSMTSolver.h"
13 
14 #include "klee/Solver/SolverCmdLine.h"
15 #include "klee/Support/ErrorHandling.h"
16 #include "klee/Solver/Solver.h"
17 
18 #include "llvm/Support/ErrorHandling.h"
19 #include "llvm/Support/raw_ostream.h"
20 
21 #include <string>
22 
23 namespace klee {
24 
createCoreSolver(CoreSolverType cst)25 Solver *createCoreSolver(CoreSolverType cst) {
26   switch (cst) {
27   case STP_SOLVER:
28 #ifdef ENABLE_STP
29     klee_message("Using STP solver backend");
30     return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
31 #else
32     klee_message("Not compiled with STP support");
33     return NULL;
34 #endif
35   case METASMT_SOLVER:
36 #ifdef ENABLE_METASMT
37     klee_message("Using MetaSMT solver backend");
38     return createMetaSMTSolver();
39 #else
40     klee_message("Not compiled with MetaSMT support");
41     return NULL;
42 #endif
43   case DUMMY_SOLVER:
44     return createDummySolver();
45   case Z3_SOLVER:
46 #ifdef ENABLE_Z3
47     klee_message("Using Z3 solver backend");
48     return new Z3Solver();
49 #else
50     klee_message("Not compiled with Z3 support");
51     return NULL;
52 #endif
53   case NO_SOLVER:
54     klee_message("Invalid solver");
55     return NULL;
56   default:
57     llvm_unreachable("Unsupported CoreSolverType");
58   }
59 }
60 }
61