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)25Solver *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