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

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

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()) {