add support for CVC4 and Yices2 via metaSMT

3 files changed, 30 insertions, 11 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 79f9286b..9668d00b 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -61,7 +61,9 @@ enum MetaSMTBackendType
 {
     METASMT_BACKEND_STP,
     METASMT_BACKEND_Z3,
-    METASMT_BACKEND_BOOLECTOR
+    METASMT_BACKEND_BOOLECTOR,
+    METASMT_BACKEND_CVC4,
+    METASMT_BACKEND_YICES2
 };
 
 extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index bffd3a4f..aaba72f4 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -112,6 +112,12 @@ void KCommandLine::HideUnrelatedOptions(
 #elif METASMT_DEFAULT_BACKEND_IS_Z3
 #define METASMT_DEFAULT_BACKEND_STR "(default = z3)."
 #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3
+#elif METASMT_DEFAULT_BACKEND_IS_CVC4
+#define METASMT_DEFAULT_BACKEND_STR "(default = cvc4)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_CVC4
+#elif METASMT_DEFAULT_BACKEND_IS_YICES2
+#define METASMT_DEFAULT_BACKEND_STR "(default = yices2)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_YICES2
 #else
 #define METASMT_DEFAULT_BACKEND_STR "(default = stp)."
 #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP
@@ -123,7 +129,9 @@ MetaSMTBackend("metasmt-backend",
                cl::values(clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
                           clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
                           clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor",
-                                     "Use metaSMT with Boolector")
+                                     "Use metaSMT with Boolector"),
+                          clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"),
+                          clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2")
                           KLEE_LLVM_CL_VAL_END),
                cl::init(METASMT_DEFAULT_BACKEND));
 
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 9b49f995..9003b119 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -23,14 +23,18 @@
 #include <metaSMT/DirectSolver_Context.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
 #include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/CVC4.hpp>
+#include <metaSMT/backend/Yices2.hpp>
 
 #define Expr VCExpr
 #define Type VCType
 #define STP STP_Backend
+#define type_t STP_type_t
 #include <metaSMT/backend/STP.hpp>
 #undef Expr
 #undef Type
 #undef STP
+#undef type_t
 
 #include <errno.h>
 #include <unistd.h>
@@ -405,30 +409,35 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 
-template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >;
-template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >;
-template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >;
-
 Solver *createMetaSMTSolver() {
-  using metaSMT::DirectSolver_Context;
-  using namespace metaSMT::solver;
+  using namespace metaSMT;
 
   Solver *coreSolver = NULL;
   std::string backend;
   switch (MetaSMTBackend) {
   case METASMT_BACKEND_STP:
     backend = "STP";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >(
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >(
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
   case METASMT_BACKEND_Z3:
     backend = "Z3";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >(
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >(
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
   case METASMT_BACKEND_BOOLECTOR:
     backend = "Boolector";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >(
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  case METASMT_BACKEND_CVC4:
+    backend = "CVC4";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  case METASMT_BACKEND_YICES2:
+    backend = "Yices2";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >(
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
   default: