From 0b2eb659087dd3643e57fe39ee84f6cb42721e94 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 31 Jul 2018 11:25:27 -0700 Subject: [PATCH] Fix option handler for lazy/bv-sat-solver combinations. (#2225) Further, unifies all *limitHandler and *limitPerHandler to limitHandler. --- src/options/options_handler.cpp | 83 ++++++++++++++------------------- src/options/options_handler.h | 5 +- src/options/smt_options.toml | 8 ++-- src/smt/smt_engine.cpp | 7 +++ 4 files changed, 46 insertions(+), 57 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a72eb2c30..b0e46d8cc 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -53,6 +53,28 @@ namespace CVC4 { namespace options { +// helper functions +namespace { + +void throwLazyBBUnsupported(theory::bv::SatSolverMode m) +{ + std::string sat_solver; + if (m == theory::bv::SAT_SOLVER_CADICAL) + { + sat_solver = "CaDiCaL"; + } + else + { + Assert(m == theory::bv::SAT_SOLVER_CRYPTOMINISAT); + sat_solver = "CryptoMiniSat"; + } + std::string indent(25, ' '); + throw OptionException(sat_solver + " does not support lazy bit-blasting.\n" + + indent + "Try --bv-sat-solver=minisat"); +} + +} // namespace + OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } void OptionsHandler::notifyForceLogic(const std::string& option){ @@ -88,55 +110,19 @@ void OptionsHandler::notifyRlimitPer(const std::string& option) { d_options->d_rlimitPerListeners.notify(); } -unsigned long OptionsHandler::tlimitHandler(std::string option, - std::string optarg) -{ - unsigned long ms; - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - return ms; -} - -unsigned long OptionsHandler::tlimitPerHandler(std::string option, - std::string optarg) -{ - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - return ms; -} - -unsigned long OptionsHandler::rlimitHandler(std::string option, - std::string optarg) -{ - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - return ms; -} - -unsigned long OptionsHandler::rlimitPerHandler(std::string option, - std::string optarg) +unsigned long OptionsHandler::limitHandler(std::string option, + std::string optarg) { unsigned long ms; - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); + if (!(convert >> ms)) + { + throw OptionException("option `" + option + + "` requires a number as an argument"); } - return ms; } - /* options/base_options_handlers.h */ void OptionsHandler::notifyPrintSuccess(std::string option) { d_options->d_setPrintSuccessListeners.notify(); @@ -1087,12 +1073,9 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, if(optarg == "minisat") { return theory::bv::SAT_SOLVER_MINISAT; } else if(optarg == "cryptominisat") { - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && options::bitblastMode.wasSetByUser()) { - throw OptionException( - std::string("CryptoMiniSat does not support lazy bit-blasting. \n\ - Try --bv-sat-solver=minisat")); + throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CRYPTOMINISAT); } if (!options::bitvectorToBool.wasSetByUser()) { options::bitvectorToBool.set(true); @@ -1113,9 +1096,7 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, 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")); + throwLazyBBUnsupported(theory::bv::SAT_SOLVER_CADICAL); } if (!options::bitvectorToBool.wasSetByUser()) { @@ -1167,6 +1148,10 @@ theory::bv::BitblastMode OptionsHandler::stringToBitblastMode( if (!options::bitvectorAlgebraicSolver.wasSetByUser()) { options::bitvectorAlgebraicSolver.set(true); } + if (options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT) + { + throwLazyBBUnsupported(options::bvSatSolver()); + } return theory::bv::BITBLAST_MODE_LAZY; } else if(optarg == "eager") { if (!options::bitvectorToBool.wasSetByUser()) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 6e2044957..1869dc6a0 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -182,10 +182,7 @@ public: void statsEnabledBuild(std::string option, bool value); - unsigned long tlimitHandler(std::string option, std::string optarg); - unsigned long tlimitPerHandler(std::string option, std::string optarg); - unsigned long rlimitHandler(std::string option, std::string optarg); - unsigned long rlimitPerHandler(std::string option, std::string optarg); + unsigned long limitHandler(std::string option, std::string optarg); void notifyTlimit(const std::string& option); void notifyTlimitPer(const std::string& option); diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 7301272b1..36ada5a95 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -419,7 +419,7 @@ header = "options/smt_options.h" category = "common" long = "tlimit=MS" type = "unsigned long" - handler = "tlimitHandler" + handler = "limitHandler" notifies = ["notifyTlimit"] read_only = true help = "enable time limiting (give milliseconds)" @@ -430,7 +430,7 @@ header = "options/smt_options.h" category = "common" long = "tlimit-per=MS" type = "unsigned long" - handler = "tlimitPerHandler" + handler = "limitHandler" notifies = ["notifyTlimitPer"] read_only = true help = "enable time limiting per query (give milliseconds)" @@ -441,7 +441,7 @@ header = "options/smt_options.h" category = "common" long = "rlimit=N" type = "unsigned long" - handler = "rlimitHandler" + handler = "limitHandler" notifies = ["notifyRlimit"] read_only = true help = "enable resource limiting (currently, roughly the number of SAT conflicts)" @@ -452,7 +452,7 @@ header = "options/smt_options.h" category = "common" long = "rlimit-per=N" type = "unsigned long" - handler = "rlimitPerHandler" + handler = "limitHandler" notifies = ["notifyRlimitPer"] read_only = true help = "enable resource limiting per query" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index de4537807..801711a13 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1334,6 +1334,13 @@ void SmtEngine::setDefaults() { << "generation" << endl; setOption("bitblastMode", SExpr("lazy")); } + + if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV)) + { + throw OptionException( + "Incremental eager bit-blasting is currently " + "only supported for QF_BV. Try --bitblast=lazy."); + } } if(options::forceLogicString.wasSetByUser()) { -- 2.30.2