Fix option handler for lazy/bv-sat-solver combinations. (#2225)

Further, unifies all *limitHandler and *limitPerHandler to limitHandler.

1 files changed, 34 insertions, 49 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()) {