1 files changed, 55 insertions, 34 deletions

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index accc48e4..abc37d4b 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -34,17 +34,35 @@
 #undef PACKAGE_TARNAME
 #undef PACKAGE_VERSION
 
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-#include "llvm/System/Signals.h"
-#else
 #include "llvm/Support/Signals.h"
 #include "llvm/Support/system_error.h"
-#endif
 
 using namespace llvm;
 using namespace klee;
 using namespace klee::expr;
 
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+
+#define Expr VCExpr
+#define Type VCType
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef Type
+#undef STP
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+#endif /* SUPPORT_METASMT */
+
+
+
+
 namespace {
   llvm::cl::opt<std::string>
   InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional,
@@ -211,7 +229,39 @@ static bool EvaluateInputAST(const char *Filename,
     return false;
 
   // FIXME: Support choice of solver.
-  Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+  Solver *coreSolver = NULL; // 
+  
+#ifdef SUPPORT_METASMT
+  if (UseMetaSMT != METASMT_BACKEND_NONE) {
+    
+    std::string backend;
+    
+    switch (UseMetaSMT) {
+          case METASMT_BACKEND_STP:
+              backend = "STP"; 
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          case METASMT_BACKEND_Z3:
+              backend = "Z3";
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          case METASMT_BACKEND_BOOLECTOR:
+              backend = "Boolector";
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          default:
+              assert(false);
+              break;
+    };
+    std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n";
+  }
+  else {
+    coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+  }
+#else
+  coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+#endif /* SUPPORT_METASMT */
+  
   
   if (!UseDummySolver) {
     if (0 != MaxCoreSolverTime) {
@@ -405,20 +455,12 @@ int main(int argc, char **argv) {
 
   std::string ErrorStr;
   
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-  MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), &ErrorStr);
-  if (!MB) {
-    std::cerr << argv[0] << ": error: " << ErrorStr << "\n";
-    return 1;
-  }
-#else
   OwningPtr<MemoryBuffer> MB;
   error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), MB);
   if (ec) {
     std::cerr << argv[0] << ": error: " << ec.message() << "\n";
     return 1;
   }
-#endif
   
   ExprBuilder *Builder = 0;
   switch (BuilderKind) {
@@ -438,45 +480,24 @@ int main(int argc, char **argv) {
 
   switch (ToolAction) {
   case PrintTokens:
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-    PrintInputTokens(MB);
-#else
     PrintInputTokens(MB.get());
-#endif
     break;
   case PrintAST:
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-    success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB,
-                            Builder);
-#else
     success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB.get(),
                             Builder);
-#endif
     break;
   case Evaluate:
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-    success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(),
-                               MB, Builder);
-#else
     success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(),
                                MB.get(), Builder);
-#endif
     break;
   case PrintSMTLIBv2:
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-    success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB,Builder);
-#else
     success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder);
-#endif
     break;
   default:
     std::cerr << argv[0] << ": error: Unknown program action!\n";
   }
 
   delete Builder;
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-  delete MB;
-#endif
   llvm::llvm_shutdown();
   return success ? 0 : 1;
 }