Make it possible to build KLEE without using STP and only MetaSMT.

The default core solver is STP if KLEE is built with STP otherwise
it is MetaSMT.

Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for
consistency.

5 files changed, 19 insertions, 11 deletions

diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 9d21931d..0d451f27 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -13,7 +13,7 @@
 #include "llvm/Support/raw_ostream.h"
 #include <string>
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include <metaSMT/frontend/Array.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
@@ -61,17 +61,22 @@ static Solver *handleMetaSMT() {
   llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
   return coreSolver;
 }
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 namespace klee {
 
 Solver *createCoreSolver(CoreSolverType cst) {
   switch (cst) {
   case STP_SOLVER:
+#ifdef ENABLE_STP
     llvm::errs() << "Using STP solver backend\n";
     return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+#else
+    llvm::errs() << "Not compiled with STP support\n";
+    return NULL;
+#endif
   case METASMT_SOLVER:
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
     llvm::errs() << "Using MetaSMT solver backend\n";
     return handleMetaSMT();
 #else
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 6da1b492..ffd3cfe9 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -15,7 +15,7 @@
 #include "klee/util/ExprHashMap.h"
 #include "ConstantDivision.h"
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include "llvm/Support/CommandLine.h"
 
@@ -1177,6 +1177,6 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
 
 }  /* end of namespace klee */
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 #endif /* METASMTBUILDER_H_ */
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 8394bbf3..971ef371 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -6,8 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
-#ifdef SUPPORT_METASMT
+#include "klee/Config/config.h"
+#ifdef ENABLE_METASMT
 
 #include "MetaSMTBuilder.h"
 #include "klee/Constraints.h"
@@ -463,4 +463,4 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
-#endif // SUPPORT_METASMT
+#endif // ENABLE_METASMT
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 2f51c2b9..2b07f391 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -6,7 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
+#include "klee/Config/config.h"
+#ifdef ENABLE_STP
 #include "STPBuilder.h"
 
 #include "klee/Expr.h"
@@ -902,5 +903,5 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return vc_trueExpr(vc);
   }
 }
-
+#endif // ENABLE_STP
 
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index cb15a23c..5c49521e 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -6,7 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
+#include "klee/Config/config.h"
+#ifdef ENABLE_STP
 #include "STPBuilder.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
@@ -382,3 +383,4 @@ void STPSolver::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
+#endif // ENABLE_STP