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, 21 insertions, 183 deletions

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;