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, 4 insertions, 97 deletions

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