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/.

1 files changed, 0 insertions, 137 deletions

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