STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat

2 files changed, 94 insertions, 2 deletions

diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index 95728cde..13536910 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -16,13 +16,14 @@
 #include "klee/Expr/Assignment.h"
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/ExprUtil.h"
-#include "klee/Support/OptionCategories.h"
 #include "klee/Solver/SolverImpl.h"
 #include "klee/Support/ErrorHandling.h"
+#include "klee/Support/OptionCategories.h"
 
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/Errno.h"
 
+#include <array>
 #include <csignal>
 #include <sys/ipc.h>
 #include <sys/shm.h>
@@ -40,7 +41,24 @@ llvm::cl::opt<bool> IgnoreSolverFailures(
     "ignore-solver-failures", llvm::cl::init(false),
     llvm::cl::desc("Ignore any STP solver failures (default=false)"),
     llvm::cl::cat(klee::SolvingCat));
-}
+
+enum SAT { MINISAT, SIMPLEMINISAT, CRYPTOMINISAT, RISS };
+const std::array<std::string, 4> SATNames{"MiniSat", "simplifying MiniSat",
+                                          "CryptoMiniSat", "RISS"};
+
+llvm::cl::opt<SAT> SATSolver(
+    "stp-sat-solver",
+    llvm::cl::desc(
+        "Set the underlying SAT solver for STP (default=cryptominisat)"),
+    llvm::cl::values(clEnumValN(SAT::MINISAT, "minisat",
+                                SATNames[SAT::MINISAT]),
+                     clEnumValN(SAT::SIMPLEMINISAT, "simpleminisat",
+                                SATNames[SAT::SIMPLEMINISAT]),
+                     clEnumValN(SAT::CRYPTOMINISAT, "cryptominisat",
+                                SATNames[SAT::CRYPTOMINISAT]),
+                     clEnumValN(SAT::RISS, "riss", SATNames[SAT::RISS])),
+    llvm::cl::init(CRYPTOMINISAT), llvm::cl::cat(klee::SolvingCat));
+} // namespace
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
 
@@ -103,6 +121,49 @@ STPSolverImpl::STPSolverImpl(bool useForkedSTP, bool optimizeDivides)
   // we restore the old behaviour.
   vc_setInterfaceFlags(vc, EXPRDELETE, 0);
 
+  // set SAT solver
+  bool SATSolverAvailable = false;
+  bool specifiedOnCommandLine = SATSolver.getNumOccurrences() > 0;
+  switch (SATSolver) {
+  case SAT::MINISAT: {
+    SATSolverAvailable = vc_useMinisat(vc);
+    break;
+  }
+  case SAT::SIMPLEMINISAT: {
+    SATSolverAvailable = vc_useSimplifyingMinisat(vc);
+    break;
+  }
+  case SAT::CRYPTOMINISAT: {
+    SATSolverAvailable = vc_useCryptominisat(vc);
+    break;
+  }
+  case SAT::RISS: {
+    SATSolverAvailable = vc_useRiss(vc);
+    break;
+  }
+  default:
+    assert(false && "Illegal SAT solver value.");
+  }
+
+  // print SMT/SAT status
+  const auto expectedSATName = SATNames[SATSolver.getValue()];
+  std::string SATName{"unknown"};
+  if (vc_isUsingMinisat(vc))
+    SATName = SATNames[SAT::MINISAT];
+  else if (vc_isUsingSimplifyingMinisat(vc))
+    SATName = SATNames[SAT::SIMPLEMINISAT];
+  else if (vc_isUsingCryptominisat(vc))
+    SATName = SATNames[SAT::CRYPTOMINISAT];
+  else if (vc_isUsingRiss(vc))
+    SATName = SATNames[SAT::RISS];
+
+  if (!specifiedOnCommandLine || SATSolverAvailable) {
+    klee_message("SAT solver: %s", SATName.c_str());
+  } else {
+    klee_warning("%s not supported by STP", expectedSATName.c_str());
+    klee_message("Fallback SAT solver: %s", SATName.c_str());
+  }
+
   make_division_total(vc);
 
   vc_registerErrorHandler(::stp_error_handler);
diff --git a/test/Solver/STPswitchSAT.c b/test/Solver/STPswitchSAT.c
new file mode 100644
index 00000000..f205aca7
--- /dev/null
+++ b/test/Solver/STPswitchSAT.c
@@ -0,0 +1,31 @@
+// REQUIRES: stp
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+//
+// RUN: rm -rf %t.klee-out-minisat
+// RUN: %klee --output-dir=%t.klee-out-minisat -solver-backend=stp --stp-sat-solver=minisat %t1.bc
+// RUN: cat %t.klee-out-minisat/messages.txt %t.klee-out-minisat/warnings.txt > %t.klee-out-minisat/all.txt
+// RUN: FileCheck --input-file=%t.klee-out-minisat/all.txt --check-prefix=MINISAT %s
+//
+// RUN: rm -rf %t.klee-out-riss
+// RUN: %klee --output-dir=%t.klee-out-riss -solver-backend=stp --stp-sat-solver=riss %t1.bc
+// RUN: cat %t.klee-out-riss/messages.txt %t.klee-out-riss/warnings.txt > %t.klee-out-riss/all.txt
+// RUN: FileCheck --input-file=%t.klee-out-riss/all.txt --check-prefix=RISS %s
+
+#include "klee/klee.h"
+
+int main(void) {
+	int foo;
+	int bar = 42;
+	klee_make_symbolic(&foo, sizeof(foo), "foo");
+
+	if (foo) bar -= 17;
+	else bar += 5;
+
+	return bar;
+}
+
+// MINISAT: KLEE: Using STP solver backend
+// MINISAT: {{KLEE: SAT solver: MiniSat|KLEE: Fallback SAT solver}}
+
+// RISS: KLEE: Using STP solver backend
+// RISS: {{KLEE: SAT solver: RISS|KLEE: Fallback SAT solver}}