diff options
author | Frank Busse <bb0xfb@gmail.com> | 2023-03-17 13:11:58 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-22 21:02:22 +0000 |
commit | a52050202a53161615e1d088e61ff19d82aeef50 (patch) | |
tree | 06595daa6a3d5adaf55bcb014fb1cc477944d7f1 /lib | |
parent | 5607a7f1910e579acc0b93b1ae2caba88e7d5fd7 (diff) | |
download | klee-a52050202a53161615e1d088e61ff19d82aeef50.tar.gz |
STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Solver/STPSolver.cpp | 65 |
1 files changed, 63 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); |