diff options
Diffstat (limited to 'src/options/options_handler.cpp')
-rw-r--r-- | src/options/options_handler.cpp | 51 |
1 files changed, 41 insertions, 10 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 61f7646ee..9b2eb1cb2 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1042,25 +1042,29 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) void OptionsHandler::satSolverEnabledBuild(std::string option, bool value) { -#ifndef CVC4_USE_CRYPTOMINISAT - if(value) { +#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) + if (value) + { std::stringstream ss; - ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + ss << "option `" << option + << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL"; throw OptionException(ss.str()); } -#endif /* CVC4_USE_CRYPTOMINISAT */ +#endif } void OptionsHandler::satSolverEnabledBuild(std::string option, std::string value) { -#ifndef CVC4_USE_CRYPTOMINISAT - if(!value.empty()) { +#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) + if (!value.empty()) + { std::stringstream ss; - ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + ss << "option `" << option + << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL"; throw OptionException(ss.str()); } -#endif /* CVC4_USE_CRYPTOMINISAT */ +#endif } const std::string OptionsHandler::s_bvSatSolverHelp = "\ @@ -1068,6 +1072,8 @@ Sat solvers currently supported by the --bv-sat-solver option:\n\ \n\ minisat (default)\n\ \n\ +cadical\n\ +\n\ cryptominisat\n\ "; @@ -1080,13 +1086,14 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, if (options::incrementalSolving() && options::incrementalSolving.wasSetByUser()) { - throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\ + throw OptionException(std::string("CryptoMinSat does not support incremental mode. \n\ Try --bv-sat-solver=minisat")); } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && options::bitblastMode.wasSetByUser()) { - throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\ + throw OptionException( + std::string("CryptoMiniSat does not support lazy bit-blasting. \n\ Try --bv-sat-solver=minisat")); } if (!options::bitvectorToBool.wasSetByUser()) { @@ -1099,6 +1106,29 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, // options::skolemizeArguments.set(true); // } return theory::bv::SAT_SOLVER_CRYPTOMINISAT; + } + else if (optarg == "cadical") + { + if (options::incrementalSolving() + && options::incrementalSolving.wasSetByUser()) + { + throw OptionException( + std::string("CaDiCaL does not support incremental mode. \n\ + Try --bv-sat-solver=minisat")); + } + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY + && options::bitblastMode.wasSetByUser()) + { + throw OptionException( + std::string("CaDiCaL does not support lazy bit-blasting. \n\ + Try --bv-sat-solver=minisat")); + } + if (!options::bitvectorToBool.wasSetByUser()) + { + options::bitvectorToBool.set(true); + } + return theory::bv::SAT_SOLVER_CADICAL; } else if(optarg == "help") { puts(s_bvSatSolverHelp.c_str()); exit(1); @@ -1658,6 +1688,7 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("abc", Configuration::isBuiltWithAbc()); print_config_cond("cln", Configuration::isBuiltWithCln()); print_config_cond("glpk", Configuration::isBuiltWithGlpk()); + print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); |