diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-05-22 06:41:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-22 08:41:50 -0500 |
commit | c531152e6a707b66b885e508ea61e2a67e195ccc (patch) | |
tree | a18a2d342b03db1700a963470f2064cf3ac8d086 /src/options/options_handler.cpp | |
parent | ae33f11d0f4156b4d21b9e77f6df59ec0f9e8184 (diff) |
Add support for SAT solver Kissat. (#4514)
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 9253ea1c8..af811e085 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -51,6 +51,10 @@ void throwLazyBBUnsupported(options::SatSolverMode m) { sat_solver = "CaDiCaL"; } + else if (m == options::SatSolverMode::KISSAT) + { + sat_solver = "Kissat"; + } else { Assert(m == options::SatSolverMode::CRYPTOMINISAT); @@ -166,7 +170,17 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) throw OptionException(ss.str()); } - if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL) + if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) + { + std::stringstream ss; + ss << "option `" << option + << "' requires a Kissat build of CVC4; this binary was not built with " + "Kissat support"; + throw OptionException(ss.str()); + } + + if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL + || m == SatSolverMode::KISSAT) { if (options::bitblastMode() == options::BitblastMode::LAZY && options::bitblastMode.wasSetByUser()) @@ -443,6 +457,7 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); + print_config_cond("kissat", Configuration::isBuiltWithKissat()); print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); print_config_cond("readline", Configuration::isBuiltWithReadline()); print_config_cond("symfpu", Configuration::isBuiltWithSymFPU()); |