Clear options manager (#6991)

This PR moves the remaining responsibilities from the options manager into option predicates. They belong there anyway, given that this code shall be executed immediately when an option is set. This also allows to remove the infrastructure for an options listener.

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index bdc369b60610b47d9143f2ef967f683df433cfd8..9a2d2f74ed952d8be5396b9e0879cfdb61a0734e 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -158,6 +158,7 @@ public = true
   category   = "regular"
   long       = "print-success"
   type       = "bool"
+  predicates = ["setPrintSuccess"]
   help       = "print the \"success\" output required of SMT-LIBv2"
 
 [[option]]

diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 075ce6fa92c06d8f1a8fde3007fc2fe0d6a12e2d..c95fd3dfc900a78da1743b47b33e8b09e2692394 100644 (file)
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -7,7 +7,8 @@ name   = "Expression"
   long       = "expr-depth=N"
   type       = "int64_t"
   default    = "0"
-  predicates = ["setDefaultExprDepthPredicate"]
+  minimum    = "-1"
+  predicates = ["setDefaultExprDepth"]
   help       = "print exprs to depth N (0 == default, -1 == no limit)"
 
 [[option]]
@@ -16,7 +17,8 @@ name   = "Expression"
   long       = "dag-thresh=N"
   type       = "int64_t"
   default    = "1"
-  predicates = ["setDefaultDagThreshPredicate"]
+  minimum    = "0"
+  predicates = ["setDefaultDagThresh"]
   help       = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
 
 [[option]]

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 02087d6a0b68bd1d0a8f0410257ac4c5054b9abb..15f319e9ce027ee12ad80874a8a985cff7d3373a 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -239,12 +239,13 @@ def get_predicates(option):
         return []
     optname = option.long_name if option.long else ""
     assert option.type != 'void'
-    res = ['opts.handler().{}("{}", option, value);'.format(x, optname)
-            for x in option.predicates]
+    res = []
     if option.minimum:
-        res.append('opts.handler().checkMinimum("{}", option, value, {});'.format(optname, option.minimum))
+        res.append('opts.handler().checkMinimum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.minimum))
     if option.maximum:
-        res.append('opts.handler().checkMaximum("{}", option, value, {});'.format(optname, option.maximum))
+        res.append('opts.handler().checkMaximum("{}", option, value, static_cast<{}>({}));'.format(optname, option.type, option.maximum))
+    res += ['opts.handler().{}("{}", option, value);'.format(x, optname)
+            for x in option.predicates]
     return res
 
 

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index f5c80a7589332aa7c6afb28ad7f28a9215089e5b..55661a0949501f257cd7940f43ae157ceef0f421 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -26,6 +26,7 @@
 #include "base/exception.h"
 #include "base/modal_exception.h"
 #include "base/output.h"
+#include "expr/expr_iomanip.h"
 #include "lib/strtok_r.h"
 #include "options/base_options.h"
 #include "options/bv_options.h"
@@ -35,6 +36,7 @@
 #include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
+#include "smt/command.h"
 #include "smt/dump.h"
 
 namespace cvc5 {
@@ -294,22 +296,29 @@ void OptionsHandler::threadN(const std::string& option, const std::string& flag)
 }
 
 // expr/options_handlers.h
-void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option,
-                                                  const std::string& flag,
-                                                  int depth)
+void OptionsHandler::setDefaultExprDepth(const std::string& option,
+                                         const std::string& flag,
+                                         int depth)
 {
-  if(depth < -1) {
-    throw OptionException("--expr-depth requires a positive argument, or -1.");
-  }
+  Debug.getStream() << expr::ExprSetDepth(depth);
+  Trace.getStream() << expr::ExprSetDepth(depth);
+  Notice.getStream() << expr::ExprSetDepth(depth);
+  Chat.getStream() << expr::ExprSetDepth(depth);
+  CVC5Message.getStream() << expr::ExprSetDepth(depth);
+  Warning.getStream() << expr::ExprSetDepth(depth);
 }
 
-void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option,
-                                                  const std::string& flag,
-                                                  int dag)
+void OptionsHandler::setDefaultDagThresh(const std::string& option,
+                                         const std::string& flag,
+                                         int dag)
 {
-  if(dag < 0) {
-    throw OptionException("--dag-thresh requires a nonnegative argument.");
-  }
+  Debug.getStream() << expr::ExprDag(dag);
+  Trace.getStream() << expr::ExprDag(dag);
+  Notice.getStream() << expr::ExprDag(dag);
+  Chat.getStream() << expr::ExprDag(dag);
+  CVC5Message.getStream() << expr::ExprDag(dag);
+  Warning.getStream() << expr::ExprDag(dag);
+  Dump.getStream() << expr::ExprDag(dag);
 }
 
 // main/options_handlers.h
@@ -630,5 +639,25 @@ void OptionsHandler::decreaseVerbosity(const std::string& option,
   setVerbosity(option, flag, d_options->base.verbosity);
 }
 
+void OptionsHandler::setDumpMode(const std::string& option,
+                                 const std::string& flag,
+                                 const std::string& optarg)
+{
+  Dump.setDumpFromString(optarg);
+}
+
+void OptionsHandler::setPrintSuccess(const std::string& option,
+                                     const std::string& flag,
+                                     bool value)
+{
+  Debug.getStream() << Command::printsuccess(value);
+  Trace.getStream() << Command::printsuccess(value);
+  Notice.getStream() << Command::printsuccess(value);
+  Chat.getStream() << Command::printsuccess(value);
+  CVC5Message.getStream() << Command::printsuccess(value);
+  Warning.getStream() << Command::printsuccess(value);
+  *d_options->base.out << Command::printsuccess(value);
+}
+
 }  // namespace options
 }  // namespace cvc5

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 867d48a446211bb16cee8fc9ea117df6ee6fe56e..f19e63445bbf977836b53849efc3e06a44adc6f5 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -123,12 +123,12 @@ public:
                          const std::string& optarg);
 
   /* expr/options_handlers.h */
-  void setDefaultExprDepthPredicate(const std::string& option,
-                                    const std::string& flag,
-                                    int depth);
-  void setDefaultDagThreshPredicate(const std::string& option,
-                                    const std::string& flag,
-                                    int dag);
+  void setDefaultExprDepth(const std::string& option,
+                           const std::string& flag,
+                           int depth);
+  void setDefaultDagThresh(const std::string& option,
+                           const std::string& flag,
+                           int dag);
 
   /* main/options_handlers.h */
   void copyright(const std::string& option, const std::string& flag);
@@ -172,6 +172,13 @@ public:
                        const std::string& flag,
                        const std::string& optarg);
 
+  void setDumpMode(const std::string& option,
+                   const std::string& flag,
+                   const std::string& optarg);
+  void setPrintSuccess(const std::string& option,
+                       const std::string& flag,
+                       bool value);
+
  private:
 
   /** Pointer to the containing Options object.*/

diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index a744cf0a9919c5f2cb0868b78002f155959534e6..33c363b558dc54fc91d4eff128b180faddfeb797 100644 (file)
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -520,8 +520,6 @@ void set(Options& opts, const std::string& name, const std::string& optionarg)
                    << std::endl;
   // first update this object
   setInternal(opts, name, optionarg);
-  // then, notify the provided listener
-  opts.notifyListener(name);
 }
 
 std::vector<std::vector<std::string> > getAll(const Options& opts)

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index db58c3a4acbc2486cf928fd8a427e23e58f62c36..06a423438918dd7788b09ffe9f21e255d1b73b59 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -37,9 +37,8 @@ namespace cvc5
 {
   thread_local Options* Options::s_current = nullptr;
 
-  Options::Options(OptionsListener * ol)
+  Options::Options()
       :
-        d_olisten(ol),
 // clang-format off
 ${holder_mem_inits}$
 ${holder_ref_inits}$
@@ -58,15 +57,5 @@ ${holder_mem_copy}$
   }
 }
 
-void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
-  
-void Options::notifyListener(const std::string& key)
-  {
-    if (d_olisten != nullptr)
-    {
-      d_olisten->notifySetOption(key);
-    }
-  }
-
 }  // namespace cvc5
 

diff --git a/src/options/options_template.h b/src/options/options_template.h
index a4e595f0d857856fb7825310bbf2e4f66a245f6a..290b96f9eab208556ee2a9e7dfe5cccef389486c 100644 (file)
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -23,7 +23,6 @@
 #include <string>
 #include <vector>
 
-#include "base/listener.h"
 #include "cvc5_export.h"
 
 namespace cvc5 {
@@ -77,7 +76,7 @@ class CVC5_EXPORT Options
     return *s_current;
   }
 
-  Options(OptionsListener* ol = nullptr);
+  Options();
   ~Options();
 
   options::OptionsHandler& handler() const {
@@ -87,18 +86,10 @@ class CVC5_EXPORT Options
   /**
    * Copies the value of the options stored in OptionsHolder into the current
    * Options object.
-   * This does not copy the listeners in the Options object.
    */
   void copyValues(const Options& options);
 
-  /** Set the generic listener associated with this class to ol */
-  void setListener(OptionsListener* ol);
-
-  void notifyListener(const std::string& key);
-
  private:
-  /** Pointer to the options listener, if one exists */
-  OptionsListener* d_olisten = nullptr;
 
 // clang-format off
 ${holder_mem_decls}$

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 3a0e3e9f5f694c0af3e030f9abfae3d13b8f0e79..8094b5a6bf23e9a5f55935e845ab76f756a70411 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -7,6 +7,7 @@ name   = "SMT Layer"
   long       = "dump=MODE"
   type       = "std::string"
   help       = "dump preprocessed assertions, etc., see --dump=help"
+  predicates = ["setDumpMode"]
 
 [[option]]
   name       = "dumpToFileName"

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 8bdbd77555bc32968000fa361fc2b2f205515def..a5dee27aefa24975faacd14dc5cf2b671934ba9b 100644 (file)
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -30,72 +30,12 @@ namespace smt {
 
 OptionsManager::OptionsManager(Options* opts) : d_options(opts)
 {
-  // set options that must take effect immediately
-  if (opts->expr.defaultExprDepthWasSetByUser)
-  {
-    notifySetOption(options::expr::defaultExprDepth__name);
-  }
-  if (opts->expr.defaultDagThreshWasSetByUser)
-  {
-    notifySetOption(options::expr::defaultDagThresh__name);
-  }
-  if (opts->smt.dumpModeStringWasSetByUser)
-  {
-    notifySetOption(options::smt::dumpModeString__name);
-  }
-  if (opts->base.printSuccessWasSetByUser)
-  {
-    notifySetOption(options::base::printSuccess__name);
-  }
-  // set this as a listener to be notified of options changes from now on
-  opts->setListener(this);
 }
 
 OptionsManager::~OptionsManager() {}
 
 void OptionsManager::notifySetOption(const std::string& key)
 {
-  Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")"
-               << std::endl;
-  if (key == options::expr::defaultExprDepth__name)
-  {
-    int depth = d_options->expr.defaultExprDepth;
-    Debug.getStream() << expr::ExprSetDepth(depth);
-    Trace.getStream() << expr::ExprSetDepth(depth);
-    Notice.getStream() << expr::ExprSetDepth(depth);
-    Chat.getStream() << expr::ExprSetDepth(depth);
-    CVC5Message.getStream() << expr::ExprSetDepth(depth);
-    Warning.getStream() << expr::ExprSetDepth(depth);
-    // intentionally exclude Dump stream from this list
-  }
-  else if (key == options::expr::defaultDagThresh__name)
-  {
-    int dag = d_options->expr.defaultDagThresh;
-    Debug.getStream() << expr::ExprDag(dag);
-    Trace.getStream() << expr::ExprDag(dag);
-    Notice.getStream() << expr::ExprDag(dag);
-    Chat.getStream() << expr::ExprDag(dag);
-    CVC5Message.getStream() << expr::ExprDag(dag);
-    Warning.getStream() << expr::ExprDag(dag);
-    Dump.getStream() << expr::ExprDag(dag);
-  }
-  else if (key == options::smt::dumpModeString__name)
-  {
-    const std::string& value = d_options->smt.dumpModeString;
-    Dump.setDumpFromString(value);
-  }
-  else if (key == options::base::printSuccess__name)
-  {
-    bool value = d_options->base.printSuccess;
-    Debug.getStream() << Command::printsuccess(value);
-    Trace.getStream() << Command::printsuccess(value);
-    Notice.getStream() << Command::printsuccess(value);
-    Chat.getStream() << Command::printsuccess(value);
-    CVC5Message.getStream() << Command::printsuccess(value);
-    Warning.getStream() << Command::printsuccess(value);
-    *options::out() << Command::printsuccess(value);
-  }
-  // otherwise, no action is necessary
 }
 
 void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver)