From 8a7705ad979096d4e611fb2b8b397c48dd5fffc1 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 12 Dec 2015 20:14:01 +0000
Subject: 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.
---
 include/klee/CommandLine.h      |  4 ++--
 include/klee/Config/config.h.in | 12 ++++++------
 include/klee/Solver.h           |  6 ++++--
 3 files changed, 12 insertions(+), 10 deletions(-)

(limited to 'include')

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 44f1afd4..dc0f135a 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -47,7 +47,7 @@ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER };
 extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 enum MetaSMTBackendType
 {
@@ -58,7 +58,7 @@ enum MetaSMTBackendType
 
 extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
 template <typename T>
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 978c901f..9d34e7b6 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -6,15 +6,18 @@
 /* Enable KLEE DEBUG checks */
 #undef ENABLE_KLEE_DEBUG
 
+/* Enable metaSMT API */
+#undef ENABLE_METASMT
+
+/* Using STP Solver backend */
+#undef ENABLE_STP
+
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
 /* Define to 1 if you have the <inttypes.h> header file. */
 #undef HAVE_INTTYPES_H
 
-/* Define to 1 if you have the `stp' library (-lstp). */
-#undef HAVE_LIBSTP
-
 /* Define if mallinfo() is available on this platform. */
 #undef HAVE_MALLINFO
 
@@ -93,7 +96,4 @@
 /* klee-uclibc is supported */
 #undef SUPPORT_KLEE_UCLIBC
 
-/* Supporting metaSMT API */
-#undef SUPPORT_METASMT
-
 #endif
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index e3adac6a..fed6191a 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -203,6 +203,7 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
   };
 
+#ifdef ENABLE_STP
   /// STPSolver - A complete solver based on STP.
   class STPSolver : public Solver {
   public:
@@ -222,9 +223,10 @@ namespace klee {
     /// is off.
     virtual void setCoreSolverTimeout(double timeout);
   };
+#endif // ENABLE_STP
 
   
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
   
   template<typename SolverContext>
   class MetaSMTSolver : public Solver {
@@ -236,7 +238,7 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
 };
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
   /* *** */
 
-- 
cgit 1.4.1