Replace options listener infrastructure (#4764)

This replaces the old options listener infrastructure with the OptionsManager introduced in cb8d041.

It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization.

It also moves managed ostream objects to the OptionsManager.

@mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.

7 files changed, 4 insertions, 312 deletions

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 65eeda3ae..cab4332b8 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -151,6 +151,5 @@ header = "options/base_options.h"
   category   = "regular"
   long       = "print-success"
   type       = "bool"
-  notifies   = ["notifyPrintSuccess"]
   read_only  = true
   help       = "print the \"success\" output required of SMT-LIBv2"
diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 5f70aee43..037d46169 100644
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -9,7 +9,6 @@ header = "options/expr_options.h"
   type       = "int"
   default    = "0"
   predicates = ["setDefaultExprDepthPredicate"]
-  notifies   = ["notifySetDefaultExprDepth"]
   read_only  = true
   help       = "print exprs to depth N (0 == default, -1 == no limit)"
 
@@ -21,7 +20,6 @@ header = "options/expr_options.h"
   type       = "int"
   default    = "1"
   predicates = ["setDefaultDagThreshPredicate"]
-  notifies   = ["notifySetDefaultDagThresh"]
   read_only  = true
   help       = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
 
@@ -31,7 +29,6 @@ header = "options/expr_options.h"
   long       = "print-expr-types"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifySetPrintExprTypes"]
   read_only  = true
   help       = "print types with variables when printing exprs"
 
diff --git a/src/options/options.h b/src/options/options.h
index 2ea72ca92..44f4be7b4 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -53,36 +53,6 @@ class CVC4_PUBLIC Options {
   /** The current Options in effect */
   static thread_local Options* s_current;
 
-  /** Listeners for notifyBeforeSearch. */
-  ListenerCollection d_beforeSearchListeners;
-
-  /** Listeners for options::defaultExprDepth. */
-  ListenerCollection d_setDefaultExprDepthListeners;
-
-  /** Listeners for options::defaultDagThresh. */
-  ListenerCollection d_setDefaultDagThreshListeners;
-
-  /** Listeners for options::printExprTypes. */
-  ListenerCollection d_setPrintExprTypesListeners;
-
-  /** Listeners for options::dumpModeString. */
-  ListenerCollection d_setDumpModeListeners;
-
-  /** Listeners for options::printSuccess. */
-  ListenerCollection d_setPrintSuccessListeners;
-
-  /** Listeners for options::dumpToFileName. */
-  ListenerCollection d_dumpToFileListeners;
-
-  /** Listeners for options::regularChannelName. */
-  ListenerCollection d_setRegularChannelListeners;
-
-  /** Listeners for options::diagnosticChannelName. */
-  ListenerCollection d_setDiagnosticChannelListeners;
-
-  static ListenerCollection::Registration* registerAndNotify(
-      ListenerCollection& collection, Listener* listener, bool notify);
-
   /** Low-level assignment function for options */
   template <class T>
   void assign(T, std::string option, std::string value);
@@ -304,113 +274,6 @@ public:
 
   /** Set the generic listener associated with this class to ol */
   void setListener(OptionsListener* ol);
-  /**
-   * Registers a listener for the notification, notifyBeforeSearch.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   *
-   * This has multiple usages so having a notifyIfSet flag does not add
-   * clarity. Users should check the relevant flags before registering this.
-   */
-  ListenerCollection::Registration* registerBeforeSearchListener(
-      Listener* listener);
-
-  /**
-   * Registers a listener for options::defaultExprDepth being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDefaultExprDepthListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::defaultDagThresh being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDefaultExprDagListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::printExprTypes being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetPrintExprTypesListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::dumpModeString being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDumpModeListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::printSuccess being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetPrintSuccessListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::dumpToFileName being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerDumpToFileNameListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::regularChannelName being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetRegularOutputChannelListener(
-      Listener* listener, bool notifyIfSet);
-
-  /**
-   * Registers a listener for options::diagnosticChannelName being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
-      Listener* listener, bool notifyIfSet);
 
   /** Sends a std::flush to getErr(). */
   void flushErr();
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 40f9b898e..b752bfdda 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -69,17 +69,6 @@ void throwLazyBBUnsupported(options::SatSolverMode m)
 
 OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
 
-void OptionsHandler::notifyBeforeSearch(const std::string& option)
-{
-  try{
-    d_options->d_beforeSearchListeners.notify();
-  } catch (ModalException&){
-    std::stringstream ss;
-    ss << "cannot change option `" << option << "' after final initialization";
-    throw ModalException(ss.str());
-  }
-}
-
 unsigned long OptionsHandler::limitHandler(std::string option,
                                            std::string optarg)
 {
@@ -92,12 +81,6 @@ unsigned long OptionsHandler::limitHandler(std::string option,
   }
   return ms;
 }
-
-/* options/base_options_handlers.h */
-void OptionsHandler::notifyPrintSuccess(std::string option) {
-  d_options->d_setPrintSuccessListeners.notify();
-}
-
 // theory/quantifiers/options_handlers.h
 
 void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
@@ -310,19 +293,6 @@ void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) {
 #endif /* CVC4_USE_LFSC */
 }
 
-void OptionsHandler::notifyDumpToFile(std::string option) {
-  d_options->d_dumpToFileListeners.notify();
-}
-
-
-void OptionsHandler::notifySetRegularOutputChannel(std::string option) {
-  d_options->d_setRegularChannelListeners.notify();
-}
-
-void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
-  d_options->d_setDiagnosticChannelListeners.notify();
-}
-
 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 {
 #ifndef CVC4_STATISTICS_ON
@@ -338,12 +308,6 @@ void OptionsHandler::threadN(std::string option) {
   throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
 }
 
-void OptionsHandler::notifyDumpMode(std::string option)
-{
-  d_options->d_setDumpModeListeners.notify();
-}
-
-
 // expr/options_handlers.h
 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
   if(depth < -1) {
@@ -357,19 +321,6 @@ void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
   }
 }
 
-void OptionsHandler::notifySetDefaultExprDepth(std::string option) {
-  d_options->d_setDefaultExprDepthListeners.notify();
-}
-
-void OptionsHandler::notifySetDefaultDagThresh(std::string option) {
-  d_options->d_setDefaultDagThreshListeners.notify();
-}
-
-void OptionsHandler::notifySetPrintExprTypes(std::string option) {
-  d_options->d_setPrintExprTypesListeners.notify();
-}
-
-
 // main/options_handlers.h
 
 static void print_config (const char * str, std::string config) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 876edfad7..221e6179f 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -84,14 +84,9 @@ public:
    * Throws a ModalException if this option is being set after final
    * initialization.
    */
-  void notifyBeforeSearch(const std::string& option);
-  void notifyDumpMode(std::string option);
   void setProduceAssertions(std::string option, bool value);
   void proofEnabledBuild(std::string option, bool value);
   void LFSCEnabledBuild(std::string option, bool value);
-  void notifyDumpToFile(std::string option);
-  void notifySetRegularOutputChannel(std::string option);
-  void notifySetDiagnosticOutputChannel(std::string option);
 
   void statsEnabledBuild(std::string option, bool value);
 
@@ -100,9 +95,6 @@ public:
   /* expr/options_handlers.h */
   void setDefaultExprDepthPredicate(std::string option, int depth);
   void setDefaultDagThreshPredicate(std::string option, int dag);
-  void notifySetDefaultExprDepth(std::string option);
-  void notifySetDefaultDagThresh(std::string option);
-  void notifySetPrintExprTypes(std::string option);
 
   /* main/options_handlers.h */
   void copyright(std::string option);
@@ -119,7 +111,6 @@ public:
   InputLanguage stringToInputLanguage(std::string option, std::string optarg);
   void enableTraceTag(std::string option, std::string optarg);
   void enableDebugTag(std::string option, std::string optarg);
-  void notifyPrintSuccess(std::string option);
 
  private:
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index b4aa3dae0..5afa9173e 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -224,12 +224,10 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h
   // that can throw exceptions.
 }
 
-
 Options::Options(OptionsListener* ol)
-    : d_holder(new options::OptionsHolder())
-    , d_handler(new options::OptionsHandler(this))
-    , d_beforeSearchListeners(),
-    d_olisten(ol)
+    : d_holder(new options::OptionsHolder()),
+      d_handler(new options::OptionsHandler(this)),
+      d_olisten(ol)
 {}
 
 Options::~Options() {
@@ -254,94 +252,6 @@ std::string Options::formatThreadOptionException(const std::string& option) {
 
 void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
 
-ListenerCollection::Registration* Options::registerAndNotify(
-    ListenerCollection& collection, Listener* listener, bool notify)
-{
-  ListenerCollection::Registration* registration =
-      collection.registerListener(listener);
-  if(notify) {
-    try
-    {
-      listener->notify();
-    }
-    catch (OptionException& e)
-    {
-      // It can happen that listener->notify() throws an OptionException. In
-      // that case, we have to make sure that we delete the registration of our
-      // listener before rethrowing the exception. Otherwise the
-      // ListenerCollection deconstructor will complain that not all
-      // registrations have been removed before invoking the deconstructor.
-      delete registration;
-      throw OptionException(e.getRawMessage());
-    }
-  }
-  return registration;
-}
-
-ListenerCollection::Registration* Options::registerBeforeSearchListener(
-   Listener* listener)
-{
-  return d_beforeSearchListeners.registerListener(listener);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth);
-  return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDagListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh);
-  return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintExprTypesListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::printExprTypes);
-  return registerAndNotify(d_setPrintExprTypesListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDumpModeListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::dumpModeString);
-  return registerAndNotify(d_setDumpModeListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintSuccessListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::printSuccess);
-  return registerAndNotify(d_setPrintSuccessListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerDumpToFileNameListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName);
-  return registerAndNotify(d_dumpToFileListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetRegularOutputChannelListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::regularChannelName);
-  return registerAndNotify(d_setRegularChannelListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetDiagnosticOutputChannelListener(
-    Listener* listener, bool notifyIfSet)
-{
-  bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName);
-  return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
-}
-
 ${custom_handlers}$
 
 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
@@ -497,7 +407,6 @@ std::vector<std::string> Options::parseOptions(Options* options,
   }
   options->d_holder->binary_name = std::string(progName);
 
-
   std::vector<std::string> nonoptions;
   parseOptionsRecursive(options, argc, argv, &nonoptions);
   if(Debug.isOn("options")){
@@ -688,11 +597,9 @@ void Options::setOptionInternal(const std::string& key,
 
 std::string Options::getOption(const std::string& key) const
 {
-  Trace("options") << "SMT getOption(" << key << ")" << std::endl;
-
+  Trace("options") << "Options::getOption(" << key << ")" << std::endl;
   ${getoption_handlers}$
 
-
   throw UnrecognizedOptionException(key);
 }
 
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 18a99ad3c..3fecab5c9 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -8,7 +8,6 @@ header = "options/smt_options.h"
   category   = "common"
   long       = "dump=MODE"
   type       = "std::string"
-  notifies   = ["notifyDumpMode"]
   read_only  = true
   help       = "dump preprocessed assertions, etc., see --dump=help"
 
@@ -18,7 +17,6 @@ header = "options/smt_options.h"
   category   = "common"
   long       = "dump-to=FILE"
   type       = "std::string"
-  notifies   = ["notifyDumpToFile"]
   read_only  = true
   help       = "all dumping goes to FILE (instead of stdout)"
 
@@ -71,7 +69,6 @@ header = "options/smt_options.h"
   long       = "produce-models"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   help       = "support the get-value and get-model commands"
 
 [[option]]
@@ -79,7 +76,6 @@ header = "options/smt_options.h"
   category   = "regular"
   long       = "check-models"
   type       = "bool"
-  notifies   = ["notifyBeforeSearch"]
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"
 
 [[option]]
@@ -87,7 +83,6 @@ header = "options/smt_options.h"
   category   = "regular"
   long       = "debug-check-models"
   type       = "bool"
-  notifies   = ["notifyBeforeSearch"]
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"
 
 [[option]]
@@ -143,7 +138,6 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   predicates = ["proofEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "turn on proof generation"
 
 [[option]]
@@ -152,7 +146,6 @@ header = "options/smt_options.h"
   long       = "check-proofs"
   type       = "bool"
   predicates = ["LFSCEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "after UNSAT/VALID, machine-check the generated proof"
 
 [[option]]
@@ -234,7 +227,6 @@ header = "options/smt_options.h"
   long       = "produce-unsat-cores"
   type       = "bool"
   predicates = ["proofEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "turn on unsat core generation"
 
 [[option]]
@@ -250,7 +242,6 @@ header = "options/smt_options.h"
   long       = "dump-unsat-cores"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   help       = "output unsat cores after every UNSAT/VALID response"
 
 [[option]]
@@ -259,7 +250,6 @@ header = "options/smt_options.h"
   long       = "dump-unsat-cores-full"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   read_only  = true
   help       = "dump the full unsat core, including unlabeled assertions"
 
@@ -270,7 +260,6 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   predicates = ["proofEnabledBuild"]
-  notifies   = ["notifyBeforeSearch"]
   read_only  = true
   help       = "turn on unsat assumptions generation"
 
@@ -288,7 +277,6 @@ header = "options/smt_options.h"
   long       = "produce-assignments"
   type       = "bool"
   default    = "false"
-  notifies   = ["notifyBeforeSearch"]
   help       = "support the get-assignment command"
 
 [[option]]
@@ -297,7 +285,6 @@ header = "options/smt_options.h"
   category   = "undocumented"
   type       = "bool"
   predicates = ["setProduceAssertions"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "deprecated name for produce-assertions"
 
 [[option]]
@@ -306,7 +293,6 @@ header = "options/smt_options.h"
   long       = "produce-assertions"
   type       = "bool"
   predicates = ["setProduceAssertions"]
-  notifies   = ["notifyBeforeSearch"]
   help       = "keep an assertions list (enables get-assertions command)"
 
 [[option]]
@@ -429,7 +415,6 @@ header = "options/smt_options.h"
   smt_name   = "regular-output-channel"
   category   = "regular"
   type       = "std::string"
-  notifies   = ["notifySetRegularOutputChannel"]
   read_only  = true
   help       = "set the regular output channel of the solver"
 
@@ -438,7 +423,6 @@ header = "options/smt_options.h"
   smt_name   = "diagnostic-output-channel"
   category   = "regular"
   type       = "std::string"
-  notifies   = ["notifySetDiagnosticOutputChannel"]
   read_only  = true
   help       = "set the diagnostic output channel of the solver"