Finish refactoring on option handlers (#7295)

This PR finishes refactoring on the option handlers.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 27ab63ae75534d0cdfb52995f32823aa04a37dcd..0dfeb3b2c59ebbae4c508e72306a917f6f90a57a 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -47,27 +47,6 @@ namespace options {
 // helper functions
 namespace {
 
-void throwLazyBBUnsupported(options::SatSolverMode m)
-{
-  std::string sat_solver;
-  if (m == options::SatSolverMode::CADICAL)
-  {
-    sat_solver = "CaDiCaL";
-  }
-  else if (m == options::SatSolverMode::KISSAT)
-  {
-    sat_solver = "Kissat";
-  }
-  else
-  {
-    Assert(m == options::SatSolverMode::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");
-}
-
 static void printTags(const std::vector<std::string>& tags)
 {
   std::cout << "available tags:";
@@ -104,6 +83,44 @@ void OptionsHandler::setErrStream(const std::string& option,
   Trace.setStream(me);
 }
 
+Language OptionsHandler::stringToLanguage(const std::string& option,
+                                          const std::string& flag,
+                                          const std::string& optarg)
+{
+  if (optarg == "help")
+  {
+    *d_options->base.out << R"FOOBAR(
+Languages currently supported as arguments to the -L / --lang option:
+  auto                           attempt to automatically determine language
+  smt | smtlib | smt2 |
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard
+  tptp                           TPTP format (cnf, fof and tff)
+  sygus | sygus2                 SyGuS version 2.0
+
+Languages currently supported as arguments to the --output-lang option:
+  auto                           match output language to input language
+  smt | smtlib | smt2 |
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard
+  tptp                           TPTP format
+  ast                            internal format (simple syntax trees)
+)FOOBAR" << std::endl;
+    std::exit(1);
+    return Language::LANG_AUTO;
+  }
+
+  try
+  {
+    return language::toLanguage(optarg);
+  }
+  catch (OptionException& oe)
+  {
+    throw OptionException("Error in " + option + ": " + oe.getMessage()
+                          + "\nTry --lang help");
+  }
+
+  Unreachable();
+}
+
 void OptionsHandler::languageIsNotAST(const std::string& option,
                                       const std::string& flag,
                                       Language lang)
@@ -292,116 +309,6 @@ void OptionsHandler::setResourceWeight(const std::string& option,
   d_options->base.resourceWeightHolder.emplace_back(optarg);
 }
 
-static void print_config (const char * str, std::string config) {
-  std::string s(str);
-  unsigned sz = 14;
-  if (s.size() < sz) s.resize(sz, ' ');
-  std::cout << s << ": " << config << std::endl;
-}
-
-static void print_config_cond (const char * str, bool cond = false) {
-  print_config(str, cond ? "yes" : "no");
-}
-
-void OptionsHandler::showConfiguration(const std::string& option,
-                                       const std::string& flag)
-{
-  std::cout << Configuration::about() << std::endl;
-
-  print_config ("version", Configuration::getVersionString());
-
-  if(Configuration::isGitBuild()) {
-    const char* branchName = Configuration::getGitBranchName();
-    if(*branchName == '\0')  { branchName = "-"; }
-    std::stringstream ss;
-    ss << "git ["
-       << branchName << " "
-       << std::string(Configuration::getGitCommit()).substr(0, 8)
-       << (Configuration::hasGitModifications() ? " (with modifications)" : "")
-       << "]";
-    print_config("scm", ss.str());
-  } else {
-    print_config_cond("scm", false);
-  }
-
-  std::cout << std::endl;
-
-  std::stringstream ss;
-  ss << Configuration::getVersionMajor() << "."
-     << Configuration::getVersionMinor() << "."
-     << Configuration::getVersionRelease();
-  print_config("library", ss.str());
-
-  std::cout << std::endl;
-
-  print_config_cond("debug code", Configuration::isDebugBuild());
-  print_config_cond("statistics", Configuration::isStatisticsBuild());
-  print_config_cond("tracing", Configuration::isTracingBuild());
-  print_config_cond("dumping", Configuration::isDumpingBuild());
-  print_config_cond("muzzled", Configuration::isMuzzledBuild());
-  print_config_cond("assertions", Configuration::isAssertionBuild());
-  print_config_cond("coverage", Configuration::isCoverageBuild());
-  print_config_cond("profiling", Configuration::isProfilingBuild());
-  print_config_cond("asan", Configuration::isAsanBuild());
-  print_config_cond("ubsan", Configuration::isUbsanBuild());
-  print_config_cond("tsan", Configuration::isTsanBuild());
-  print_config_cond("competition", Configuration::isCompetitionBuild());
-
-  std::cout << std::endl;
-
-  print_config_cond("abc", Configuration::isBuiltWithAbc());
-  print_config_cond("cln", Configuration::isBuiltWithCln());
-  print_config_cond("glpk", Configuration::isBuiltWithGlpk());
-  print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
-  print_config_cond("gmp", Configuration::isBuiltWithGmp());
-  print_config_cond("kissat", Configuration::isBuiltWithKissat());
-  print_config_cond("poly", Configuration::isBuiltWithPoly());
-  print_config_cond("editline", Configuration::isBuiltWithEditline());
-
-  std::exit(0);
-}
-
-void OptionsHandler::showCopyright(const std::string& option,
-                               const std::string& flag)
-{
-  std::cout << Configuration::copyright() << std::endl;
-  std::exit(0);
-}
-
-void OptionsHandler::showVersion(const std::string& option,
-                                       const std::string& flag)
-{
-  d_options->base.out << Configuration::about() << std::endl;
-  std::exit(0);
-}
-
-void OptionsHandler::showDebugTags(const std::string& option,
-                                   const std::string& flag)
-{
-  if (!Configuration::isDebugBuild())
-  {
-    throw OptionException("debug tags not available in non-debug builds");
-  }
-  else if (!Configuration::isTracingBuild())
-  {
-    throw OptionException("debug tags not available in non-tracing builds");
-  }
-  printTags(Configuration::getDebugTags());
-  std::exit(0);
-}
-
-void OptionsHandler::showTraceTags(const std::string& option,
-                                   const std::string& flag)
-{
-  if (!Configuration::isTracingBuild())
-  {
-    throw OptionException("trace tags not available in non-tracing build");
-  }
-  printTags(Configuration::getTraceTags());
-  std::exit(0);
-}
-
-// theory/bv/options_handlers.h
 void OptionsHandler::abcEnabledBuild(const std::string& option,
                                      const std::string& flag,
                                      bool value)
@@ -462,29 +369,24 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
     if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
         && d_options->bv.bitblastModeWasSetByUser)
     {
-      throwLazyBBUnsupported(m);
-    }
-    options::bv::setDefaultBitvectorToBool(*d_options, true);
-  }
-}
-
-void OptionsHandler::checkBitblastMode(const std::string& option,
-                                       const std::string& flag,
-                                       BitblastMode m)
-{
-  if (m == options::BitblastMode::LAZY)
-  {
-    options::bv::setDefaultBitvectorPropagate(*d_options, true);
-    options::bv::setDefaultBitvectorEqualitySolver(*d_options, true);
-    options::bv::setDefaultBitvectorInequalitySolver(*d_options, true);
-    options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true);
-    if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT)
-    {
-      throwLazyBBUnsupported(d_options->bv.bvSatSolver);
+      std::string sat_solver;
+      if (m == options::SatSolverMode::CADICAL)
+      {
+        sat_solver = "CaDiCaL";
+      }
+      else if (m == options::SatSolverMode::KISSAT)
+      {
+        sat_solver = "Kissat";
+      }
+      else
+      {
+        Assert(m == options::SatSolverMode::CRYPTOMINISAT);
+        sat_solver = "CryptoMiniSat";
+      }
+      throw OptionException(sat_solver
+                            + " does not support lazy bit-blasting.\n"
+                            + "Try --bv-sat-solver=minisat");
     }
-  }
-  else if (m == BitblastMode::EAGER)
-  {
     options::bv::setDefaultBitvectorToBool(*d_options, true);
   }
 }
@@ -500,22 +402,11 @@ void OptionsHandler::setBitblastAig(const std::string& option,
         throw OptionException("bitblast-aig must be used with eager bitblaster");
       }
     } else {
-      options::BitblastMode mode = stringToBitblastMode("eager");
-      d_options->bv.bitblastMode = mode;
+      d_options->bv.bitblastMode = options::BitblastMode::EAGER;
     }
   }
 }
 
-void OptionsHandler::setProduceAssertions(const std::string& option,
-                                          const std::string& flag,
-                                          bool value)
-{
-  d_options->smt.produceAssertions = value;
-  d_options->smt.interactiveMode = value;
-}
-
-
-// expr/options_handlers.h
 void OptionsHandler::setDefaultExprDepth(const std::string& option,
                                          const std::string& flag,
                                          int depth)
@@ -541,40 +432,132 @@ void OptionsHandler::setDefaultDagThresh(const std::string& option,
   Dump.getStream() << expr::ExprDag(dag);
 }
 
-// main/options_handlers.h
+static void print_config(const char* str, std::string config)
+{
+  std::string s(str);
+  unsigned sz = 14;
+  if (s.size() < sz) s.resize(sz, ' ');
+  std::cout << s << ": " << config << std::endl;
+}
 
-Language OptionsHandler::stringToLanguage(const std::string& option,
-                                          const std::string& flag,
-                                          const std::string& optarg)
+static void print_config_cond(const char* str, bool cond = false)
 {
-  if(optarg == "help") {
-    *d_options->base.out << R"FOOBAR(
-Languages currently supported as arguments to the -L / --lang option:
-  auto                           attempt to automatically determine language
-  smt | smtlib | smt2 |
-  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard
-  tptp                           TPTP format (cnf, fof and tff)
-  sygus | sygus2                 SyGuS version 2.0
+  print_config(str, cond ? "yes" : "no");
+}
 
-Languages currently supported as arguments to the --output-lang option:
-  auto                           match output language to input language
-  smt | smtlib | smt2 |
-  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard
-  tptp                           TPTP format
-  ast                            internal format (simple syntax trees)
-)FOOBAR" << std::endl;
-    std::exit(1);
-    return Language::LANG_AUTO;
+void OptionsHandler::showConfiguration(const std::string& option,
+                                       const std::string& flag)
+{
+  std::cout << Configuration::about() << std::endl;
+
+  print_config("version", Configuration::getVersionString());
+
+  if (Configuration::isGitBuild())
+  {
+    const char* branchName = Configuration::getGitBranchName();
+    if (*branchName == '\0')
+    {
+      branchName = "-";
+    }
+    std::stringstream ss;
+    ss << "git [" << branchName << " "
+       << std::string(Configuration::getGitCommit()).substr(0, 8)
+       << (Configuration::hasGitModifications() ? " (with modifications)" : "")
+       << "]";
+    print_config("scm", ss.str());
+  }
+  else
+  {
+    print_config_cond("scm", false);
   }
 
-  try {
-    return language::toLanguage(optarg);
-  } catch(OptionException& oe) {
-    throw OptionException("Error in " + option + ": " + oe.getMessage()
-                          + "\nTry --lang help");
+  std::cout << std::endl;
+
+  std::stringstream ss;
+  ss << Configuration::getVersionMajor() << "."
+     << Configuration::getVersionMinor() << "."
+     << Configuration::getVersionRelease();
+  print_config("library", ss.str());
+
+  std::cout << std::endl;
+
+  print_config_cond("debug code", Configuration::isDebugBuild());
+  print_config_cond("statistics", Configuration::isStatisticsBuild());
+  print_config_cond("tracing", Configuration::isTracingBuild());
+  print_config_cond("dumping", Configuration::isDumpingBuild());
+  print_config_cond("muzzled", Configuration::isMuzzledBuild());
+  print_config_cond("assertions", Configuration::isAssertionBuild());
+  print_config_cond("coverage", Configuration::isCoverageBuild());
+  print_config_cond("profiling", Configuration::isProfilingBuild());
+  print_config_cond("asan", Configuration::isAsanBuild());
+  print_config_cond("ubsan", Configuration::isUbsanBuild());
+  print_config_cond("tsan", Configuration::isTsanBuild());
+  print_config_cond("competition", Configuration::isCompetitionBuild());
+
+  std::cout << std::endl;
+
+  print_config_cond("abc", Configuration::isBuiltWithAbc());
+  print_config_cond("cln", Configuration::isBuiltWithCln());
+  print_config_cond("glpk", Configuration::isBuiltWithGlpk());
+  print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
+  print_config_cond("gmp", Configuration::isBuiltWithGmp());
+  print_config_cond("kissat", Configuration::isBuiltWithKissat());
+  print_config_cond("poly", Configuration::isBuiltWithPoly());
+  print_config_cond("editline", Configuration::isBuiltWithEditline());
+
+  std::exit(0);
+}
+
+void OptionsHandler::showCopyright(const std::string& option,
+                                   const std::string& flag)
+{
+  std::cout << Configuration::copyright() << std::endl;
+  std::exit(0);
+}
+
+void OptionsHandler::showVersion(const std::string& option,
+                                 const std::string& flag)
+{
+  d_options->base.out << Configuration::about() << std::endl;
+  std::exit(0);
+}
+
+void OptionsHandler::showDebugTags(const std::string& option,
+                                   const std::string& flag)
+{
+  if (!Configuration::isDebugBuild())
+  {
+    throw OptionException("debug tags not available in non-debug builds");
+  }
+  else if (!Configuration::isTracingBuild())
+  {
+    throw OptionException("debug tags not available in non-tracing builds");
   }
+  printTags(Configuration::getDebugTags());
+  std::exit(0);
+}
 
-  Unreachable();
+void OptionsHandler::showTraceTags(const std::string& option,
+                                   const std::string& flag)
+{
+  if (!Configuration::isTracingBuild())
+  {
+    throw OptionException("trace tags not available in non-tracing build");
+  }
+  printTags(Configuration::getTraceTags());
+  std::exit(0);
+}
+
+void OptionsHandler::setDumpMode(const std::string& option,
+                                 const std::string& flag,
+                                 const std::string& optarg)
+{
+#ifdef CVC5_DUMPING
+  Dump.setDumpFromString(optarg);
+#else  /* CVC5_DUMPING */
+  throw OptionException(
+      "The dumping feature was disabled in this build of cvc5.");
+#endif /* CVC5_DUMPING */
 }
 
 void OptionsHandler::setDumpStream(const std::string& option,
@@ -588,13 +571,6 @@ void OptionsHandler::setDumpStream(const std::string& option,
       "The dumping feature was disabled in this build of cvc5.");
 #endif /* CVC5_DUMPING */
 }
-/* options/base_options_handlers.h */
-void OptionsHandler::setDumpMode(const std::string& option,
-                                 const std::string& flag,
-                                 const std::string& optarg)
-{
-  Dump.setDumpFromString(optarg);
-}
 
 }  // namespace options
 }  // namespace cvc5

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 5ced2ed488885b8761884cfcc7d5b9663a6da98f..c3cd8c358ab9a8bfca92505f12da996889bdfe06 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -40,8 +40,9 @@ namespace options {
  *
  * Most functions can throw an OptionException on failure.
  */
-class OptionsHandler {
-public:
+class OptionsHandler
+{
+ public:
   OptionsHandler(Options* options);
 
   template <typename T>
@@ -128,65 +129,58 @@ public:
                          const std::string& flag,
                          const std::string& optarg);
 
-  /******************************* main options *******************************/
-  /** Show the solver build configuration and exit */
-  void showConfiguration(const std::string& option, const std::string& flag);
-  /** Show copyright information and exit */
-  void showCopyright(const std::string& option, const std::string& flag);
-  /** Show version information and exit */
-  void showVersion(const std::string& option, const std::string& flag);
-  /** Show all debug tags and exit */
-  void showDebugTags(const std::string& option, const std::string& flag);
-  /** Show all trace tags and exit */
-  void showTraceTags(const std::string& option, const std::string& flag);
+  /******************************* bv options *******************************/
 
-  // theory/bv/options_handlers.h
+  /** Check that abc is enabled */
   void abcEnabledBuild(const std::string& option,
                        const std::string& flag,
                        bool value);
+  /** Check that abc is enabled */
   void abcEnabledBuild(const std::string& option,
                        const std::string& flag,
                        const std::string& value);
-
+  /** Check that the sat solver mode is compatible with other bv options */
   void checkBvSatSolver(const std::string& option,
                         const std::string& flag,
                         SatSolverMode m);
-  void checkBitblastMode(const std::string& option,
-                         const std::string& flag,
-                         BitblastMode m);
-
+  /** Check that we use eager bitblasting for aig */
   void setBitblastAig(const std::string& option,
                       const std::string& flag,
                       bool arg);
 
-  /**
-   * Throws a ModalException if this option is being set after final
-   * initialization.
-   */
-  void setProduceAssertions(const std::string& option,
-                            const std::string& flag,
-                            bool value);
-
-  /* expr/options_handlers.h */
+  /******************************* expr options *******************************/
+  /** Set ExprSetDepth on all output streams */
   void setDefaultExprDepth(const std::string& option,
                            const std::string& flag,
                            int depth);
+  /** Set ExprDag on all output streams */
   void setDefaultDagThresh(const std::string& option,
                            const std::string& flag,
                            int dag);
 
+  /******************************* main options *******************************/
+  /** Show the solver build configuration and exit */
+  void showConfiguration(const std::string& option, const std::string& flag);
+  /** Show copyright information and exit */
+  void showCopyright(const std::string& option, const std::string& flag);
+  /** Show version information and exit */
+  void showVersion(const std::string& option, const std::string& flag);
+  /** Show all debug tags and exit */
+  void showDebugTags(const std::string& option, const std::string& flag);
+  /** Show all trace tags and exit */
+  void showTraceTags(const std::string& option, const std::string& flag);
 
-  /* options/base_options_handlers.h */
-  void setDumpStream(const std::string& option,
-                     const std::string& flag,
-                     const ManagedOut& mo);
-
+  /******************************* smt options *******************************/
+  /** Set a mode on the dumping output stream. */
   void setDumpMode(const std::string& option,
                    const std::string& flag,
                    const std::string& optarg);
+  /** Set the dumping output stream. */
+  void setDumpStream(const std::string& option,
+                     const std::string& flag,
+                     const ManagedOut& mo);
 
  private:
-
   /** Pointer to the containing Options object.*/
   Options* d_options;
 }; /* class OptionHandler */

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 95cc79a0d1f63a83d1efe0166cde0aca2756547b..19862cab2ad0b056f39461005cd3d4efcd279637 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -254,20 +254,11 @@ name   = "SMT Layer"
   default    = "false"
   help       = "support the get-assignment command"
 
-[[option]]
-  name       = "interactiveMode"
-  long       = "interactive-mode"
-  category   = "undocumented"
-  type       = "bool"
-  predicates = ["setProduceAssertions"]
-  help       = "deprecated name for produce-assertions"
-
 [[option]]
   name       = "produceAssertions"
   category   = "common"
   long       = "produce-assertions"
   type       = "bool"
-  predicates = ["setProduceAssertions"]
   help       = "keep an assertions list (enables get-assertions command)"
 
 [[option]]

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index d74668433e62fd59db7c0e307fd4addfb841c5c5..ab6144e021d8386e6191eca5d2ea55c6c4481695 100644 (file)
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -57,7 +57,8 @@ CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc)
 
 DumpC DumpChannel;
 
-std::ostream& DumpC::setStream(std::ostream* os) {
+std::ostream& DumpC::setStream(std::ostream* os)
+{
   ::cvc5::DumpOutChannel.setStream(os);
   return *os;
 }
@@ -67,7 +68,8 @@ std::ostream* DumpC::getStreamPointer()
   return ::cvc5::DumpOutChannel.getStreamPointer();
 }
 
-void DumpC::setDumpFromString(const std::string& optarg) {
+void DumpC::setDumpFromString(const std::string& optarg)
+{
   if (Configuration::isDumpingBuild())
   {
     // Make a copy of optarg for strtok_r to use.

diff --git a/test/regress/regress1/fmf/forall_unit_data.smt2 b/test/regress/regress1/fmf/forall_unit_data.smt2
index 411c03c8a761bbecaef3764675cdb9fbd7a78123..b942f1165d88ec714b79b93d23b8a49a8d9fba9d 100644 (file)
--- a/test/regress/regress1/fmf/forall_unit_data.smt2
+++ b/test/regress/regress1/fmf/forall_unit_data.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-option :produce-models true)
-(set-option :interactive-mode true)
+(set-option :produce-assertions true)
 (set-logic ALL)
 (declare-sort a 0)
 (declare-datatypes ((w 0)) (((Wrap (unw a)))))