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

6 files changed, 60 insertions, 206 deletions

diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 577ef3226..c53def1f8 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -74,20 +74,6 @@ class ManagedOstream {
   std::ostream* d_managed;
 }; /* class ManagedOstream */
 
-class SetToDefaultSourceListener : public Listener {
- public:
-  SetToDefaultSourceListener(ManagedOstream* managedOstream)
-      : d_managedOstream(managedOstream){}
-
-  void notify() override
-  {
-    d_managedOstream->set(d_managedOstream->defaultSource());
-  }
-
- private:
-  ManagedOstream* d_managedOstream;
-};
-
 /**
  * This controls the memory associated with --dump-to.
  * This is is assumed to recieve a set whenever diagnosticChannelName
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 5b976bc31..ce5652650 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -51,6 +51,18 @@ OptionsManager::OptionsManager(Options* opts, ResourceManager* rm)
   {
     notifySetOption(options::printSuccess.getName());
   }
+  if (opts->wasSetByUser(options::diagnosticChannelName))
+  {
+    notifySetOption(options::diagnosticChannelName.getName());
+  }
+  if (opts->wasSetByUser(options::regularChannelName))
+  {
+    notifySetOption(options::regularChannelName.getName());
+  }
+  if (opts->wasSetByUser(options::dumpToFileName))
+  {
+    notifySetOption(options::dumpToFileName.getName());
+  }
   // set this as a listener to be notified of options changes from now on
   opts->setListener(this);
 }
@@ -110,6 +122,18 @@ void OptionsManager::notifySetOption(const std::string& key)
     Warning.getStream() << Command::printsuccess(value);
     *options::out() << Command::printsuccess(value);
   }
+  else if (key == options::regularChannelName.getName())
+  {
+    d_managedRegularChannel.set(options::regularChannelName());
+  }
+  else if (key == options::diagnosticChannelName.getName())
+  {
+    d_managedDiagnosticChannel.set(options::diagnosticChannelName());
+  }
+  else if (key == options::dumpToFileName.getName())
+  {
+    d_managedDumpChannel.set(options::dumpToFileName());
+  }
   // otherwise, no action is necessary
 }
 
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index bc58f17ba..ad5fe9fa2 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -17,6 +17,7 @@
 
 #include "options/options.h"
 #include "options/options_listener.h"
+#include "smt/managed_ostreams.h"
 
 namespace CVC4 {
 
@@ -65,6 +66,12 @@ class OptionsManager : public OptionsListener
   Options* d_options;
   /** Pointer to the resource manager */
   ResourceManager* d_resourceManager;
+  /** Manager for the memory of regular-output-channel. */
+  ManagedRegularOutputChannel d_managedRegularChannel;
+  /** Manager for the memory of diagnostic-output-channel. */
+  ManagedDiagnosticOutputChannel d_managedDiagnosticChannel;
+  /** Manager for the memory of --dump-to. */
+  ManagedDumpOStream d_managedDumpChannel;
 };
 
 }  // namespace smt
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 606921b7c..972d828bd 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -28,7 +28,7 @@ namespace smt {
  * updated by this method based on the current options and the logic itself.
  * @param isInternalSubsolver Whether we are setting the options for an
  * internal subsolver (see SmtEngine::isInternalSubsolver).
- * 
+ *
  * NOTE: we currently modify the current options in scope. This method
  * can be further refactored to modify an options object provided as an
  * explicit argument.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 16e4e916a..c8896b621 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -81,17 +81,16 @@
 #include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
-#include "smt/abstract_values.h"
 #include "smt/abduction_solver.h"
+#include "smt/abstract_values.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
 #include "smt/defined_function.h"
 #include "smt/logic_request.h"
-#include "smt/managed_ostreams.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
+#include "smt/options_manager.h"
 #include "smt/process_assertions.h"
-#include "smt/set_defaults.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_stats.h"
 #include "smt/term_formula_removal.h"
@@ -161,86 +160,6 @@ class ResourceOutListener : public Listener {
   SmtEngine* d_smt;
 }; /* class ResourceOutListener */
 
-class BeforeSearchListener : public Listener {
- public:
-  BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
-  void notify() override { d_smt->beforeSearch(); }
-
- private:
-  SmtEngine* d_smt;
-}; /* class BeforeSearchListener */
-
-class SetDefaultExprDepthListener : public Listener {
- public:
-  void notify() override
-  {
-    int depth = options::defaultExprDepth();
-    Debug.getStream() << expr::ExprSetDepth(depth);
-    Trace.getStream() << expr::ExprSetDepth(depth);
-    Notice.getStream() << expr::ExprSetDepth(depth);
-    Chat.getStream() << expr::ExprSetDepth(depth);
-    Message.getStream() << expr::ExprSetDepth(depth);
-    Warning.getStream() << expr::ExprSetDepth(depth);
-    // intentionally exclude Dump stream from this list
-  }
-};
-
-class SetDefaultExprDagListener : public Listener {
- public:
-  void notify() override
-  {
-    int dag = options::defaultDagThresh();
-    Debug.getStream() << expr::ExprDag(dag);
-    Trace.getStream() << expr::ExprDag(dag);
-    Notice.getStream() << expr::ExprDag(dag);
-    Chat.getStream() << expr::ExprDag(dag);
-    Message.getStream() << expr::ExprDag(dag);
-    Warning.getStream() << expr::ExprDag(dag);
-    Dump.getStream() << expr::ExprDag(dag);
-  }
-};
-
-class SetPrintExprTypesListener : public Listener {
- public:
-  void notify() override
-  {
-    bool value = options::printExprTypes();
-    Debug.getStream() << expr::ExprPrintTypes(value);
-    Trace.getStream() << expr::ExprPrintTypes(value);
-    Notice.getStream() << expr::ExprPrintTypes(value);
-    Chat.getStream() << expr::ExprPrintTypes(value);
-    Message.getStream() << expr::ExprPrintTypes(value);
-    Warning.getStream() << expr::ExprPrintTypes(value);
-    // intentionally exclude Dump stream from this list
-  }
-};
-
-class DumpModeListener : public Listener {
- public:
-  void notify() override
-  {
-    const std::string& value = options::dumpModeString();
-    Dump.setDumpFromString(value);
-  }
-};
-
-class PrintSuccessListener : public Listener {
- public:
-  void notify() override
-  {
-    bool value = options::printSuccess();
-    Debug.getStream() << Command::printsuccess(value);
-    Trace.getStream() << Command::printsuccess(value);
-    Notice.getStream() << Command::printsuccess(value);
-    Chat.getStream() << Command::printsuccess(value);
-    Message.getStream() << Command::printsuccess(value);
-    Warning.getStream() << Command::printsuccess(value);
-    *options::out() << Command::printsuccess(value);
-  }
-};
-
-
-
 /**
  * This is an inelegant solution, but for the present, it will work.
  * The point of this is to separate the public and private portions of
@@ -261,25 +180,13 @@ class SmtEnginePrivate : public NodeManagerListener {
   typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
-  /** Manager for the memory of regular-output-channel. */
-  ManagedRegularOutputChannel d_managedRegularChannel;
-
-  /** Manager for the memory of diagnostic-output-channel. */
-  ManagedDiagnosticOutputChannel d_managedDiagnosticChannel;
-
-  /** Manager for the memory of --dump-to. */
-  ManagedDumpOStream d_managedDumpChannel;
-
   /**
-   * This list contains:
-   *  softResourceOut
-   *  hardResourceOut
-   *  beforeSearchListener
-   *
-   * This needs to be deleted before both NodeManager's Options,
-   * SmtEngine, d_resourceManager, and TheoryEngine.
+   * Manager for limiting time and abstract resource usage.
    */
-  ListenerRegistrationList* d_listenerRegistrations;
+  ResourceManager* d_resourceManager;
+
+  /** Resource out listener */
+  std::unique_ptr<ResourceOutListener> d_routListener;
 
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
@@ -333,15 +240,11 @@ class SmtEnginePrivate : public NodeManagerListener {
  public:
   SmtEnginePrivate(SmtEngine& smt)
       : d_smt(smt),
-        d_managedRegularChannel(),
-        d_managedDiagnosticChannel(),
-        d_managedDumpChannel(),
-        d_listenerRegistrations(new ListenerRegistrationList()),
+        d_routListener(new ResourceOutListener(d_smt)),
         d_propagator(true, true),
         d_assertions(),
         d_assertionsProcessed(smt.getUserContext(), false),
         d_processor(smt, *smt.getResourceManager()),
-        // d_needsExpandDefs(true),  //TODO?
         d_exprNames(smt.getUserContext()),
         d_iteRemover(smt.getUserContext()),
         d_sygusConjectureStale(smt.getUserContext(), true)
@@ -349,62 +252,11 @@ class SmtEnginePrivate : public NodeManagerListener {
     d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
     ResourceManager* rm = d_smt.getResourceManager();
-
-    d_listenerRegistrations->add(
-        rm->registerListener(new ResourceOutListener(d_smt)));
-
-    try
-    {
-      Options& opts = d_smt.getOptions();
-      // Multiple options reuse BeforeSearchListener so registration requires an
-      // extra bit of care.
-      // We can safely not call notify on this before search listener at
-      // registration time. This d_smt cannot be beforeSearch at construction
-      // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
-      // not have to be called.
-      d_listenerRegistrations->add(
-          opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt)));
-
-      // These do need registration calls.
-      d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener(
-          new SetDefaultExprDepthListener(), true));
-      d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener(
-          new SetDefaultExprDagListener(), true));
-      d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener(
-          new SetPrintExprTypesListener(), true));
-      d_listenerRegistrations->add(
-          opts.registerSetDumpModeListener(new DumpModeListener(), true));
-      d_listenerRegistrations->add(opts.registerSetPrintSuccessListener(
-          new PrintSuccessListener(), true));
-      d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener(
-          new SetToDefaultSourceListener(&d_managedRegularChannel), true));
-      d_listenerRegistrations->add(
-          opts.registerSetDiagnosticOutputChannelListener(
-              new SetToDefaultSourceListener(&d_managedDiagnosticChannel),
-              true));
-      d_listenerRegistrations->add(opts.registerDumpToFileNameListener(
-          new SetToDefaultSourceListener(&d_managedDumpChannel), true));
-    }
-    catch (OptionException& e)
-    {
-      // Registering the option listeners can lead to OptionExceptions, e.g.
-      // when the user chooses a dump tag that does not exist. In that case, we
-      // have to make sure that we delete existing listener registrations and
-      // that we unsubscribe from NodeManager events. Otherwise we will have
-      // errors in the deconstructors of the NodeManager (because the
-      // NodeManager tries to notify an SmtEnginePrivate that does not exist)
-      // and the ListenerCollection (because not all registrations have been
-      // removed before calling the deconstructor).
-      delete d_listenerRegistrations;
-      d_smt.d_nodeManager->unsubscribeEvents(this);
-      throw OptionException(e.getRawMessage());
-    }
+    rm->registerListener(d_routListener.get());
   }
 
   ~SmtEnginePrivate()
   {
-    delete d_listenerRegistrations;
-
     if(d_propagator.getNeedsFinish()) {
       d_propagator.finish();
       d_propagator.setNeedsFinish(false);
@@ -620,6 +472,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_statisticsRegistry.reset(new StatisticsRegistry());
   d_resourceManager.reset(
       new ResourceManager(*d_statisticsRegistry.get(), d_options));
+  d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
   d_private.reset(new smt::SmtEnginePrivate(*this));
   d_stats.reset(new SmtEngineStatistics());
   
@@ -645,27 +498,14 @@ void SmtEngine::finishInit()
   // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
   // of SMT-LIB 2.6 standard.
 
-  // Inialize the resource manager based on the options.
-  if (options::perCallResourceLimit() != 0)
-  {
-    d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
-  }
-  if (options::cumulativeResourceLimit() != 0)
-  {
-    d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
-                                        true);
-  }
-  if (options::perCallMillisecondLimit() != 0)
-  {
-    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
-  }
-
   // set the random seed
   Random::getRandom().setSeed(options::seed());
 
-  // ensure that our heuristics are properly set up
-  setDefaults(d_logic, d_isInternalSubsolver);
-  
+  // Call finish init on the options manager. This inializes the resource
+  // manager based on the options, and sets up the best default options
+  // based on our heuristics.
+  d_optm->finishInit(d_logic, d_isInternalSubsolver);
+
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
@@ -850,6 +690,7 @@ SmtEngine::~SmtEngine()
 
     d_stats.reset(nullptr);
     d_private.reset(nullptr);
+    d_optm.reset(nullptr);
     // d_resourceManager must be destroyed before d_statisticsRegistry
     d_resourceManager.reset(nullptr);
     d_statisticsRegistry.reset(nullptr);
@@ -3425,17 +3266,14 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
   }
 }
 
-void SmtEngine::beforeSearch()
+void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 {
+  // Always check whether the SmtEngine has been initialized (which is done
+  // upon entering Assert mode the first time). No option can  be set after
+  // initialized.
   if(d_fullyInited) {
-    throw ModalException(
-        "SmtEngine::beforeSearch called after initialization.");
+    throw ModalException("SmtEngine::setOption called after initialization.");
   }
-}
-
-
-void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
-{
   NodeManagerScope nms(d_nodeManager);
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 591b69424..b38ec2d7a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -93,6 +93,7 @@ namespace prop {
 namespace smt {
 /** Utilities */
 class AbstractValues;
+class OptionsManager;
 /** Subsolvers */
 class AbductionSolver;
 /**
@@ -856,14 +857,6 @@ class CVC4_PUBLIC SmtEngine
   void setPrintFuncInModel(Expr f, bool p);
 
   /**
-   * Check and throw a ModalException if the SmtEngine has been fully
-   * initialized.
-   *
-   * throw@ ModalException
-   */
-  void beforeSearch();
-
-  /**
    * Get expression name.
    *
    * Return true if given expressoion has a name in the current context.
@@ -1299,6 +1292,12 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<ResourceManager> d_resourceManager;
   /**
+   * The options manager, which is responsible for implementing core options
+   * such as those related to time outs and printing. It is also responsible
+   * for set default options based on the logic.
+   */
+  std::unique_ptr<smt::OptionsManager> d_optm;
+  /**
    * The global scope object. Upon creation of this SmtEngine, it becomes the
    * SmtEngine in scope. It says the SmtEngine in scope until it is destructed,
    * or another SmtEngine is created.