Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)

This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.

The changes that were required for this PR include:

The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.

7 files changed, 10 insertions, 252 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index b042b9352..9222393c4 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -27,8 +27,6 @@ libcvc4_add_sources(
   node_manager.cpp
   node_manager.h
   node_manager_attributes.h
-  node_manager_listeners.cpp
-  node_manager_listeners.h
   node_self_iterator.h
   node_trie.cpp
   node_trie.h
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d69dc73f9..7bec489a3 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -92,18 +92,6 @@ ExprManager::ExprManager() :
 #endif
 }
 
-ExprManager::ExprManager(const Options& options) :
-  d_nodeManager(new NodeManager(this, options)) {
-#ifdef CVC4_STATISTICS_ON
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
-    d_exprStatisticsVars[i] = NULL;
-  }
-  for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-    d_exprStatistics[i] = NULL;
-  }
-#endif
-}
-
 ExprManager::~ExprManager()
 {
   NodeManagerScope nms(d_nodeManager);
@@ -137,15 +125,6 @@ ExprManager::~ExprManager()
   }
 }
 
-const Options& ExprManager::getOptions() const {
-  return d_nodeManager->getOptions();
-}
-
-ResourceManager* ExprManager::getResourceManager()
-{
-  return d_nodeManager->getResourceManager();
-}
-
 BooleanType ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
   return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
@@ -915,9 +894,6 @@ Type ExprManager::getType(Expr expr, bool check)
 }
 
 Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL)
-      << "ExprManager::mkVar() should only be called externally, not from "
-         "within CVC4 code.  Please use mkSkolem().";
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -926,9 +902,6 @@ Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
 }
 
 Expr ExprManager::mkVar(Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL)
-      << "ExprManager::mkVar() should only be called externally, not from "
-         "within CVC4 code.  Please use mkSkolem().";
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 4dfd77686..db5d22fa8 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -88,19 +88,8 @@ class CVC4_PUBLIC ExprManager {
   /** A list of datatypes owned by this expr manager. */
   std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
 
-  /**
-   * Creates an expression manager with default options.
-   */
+  /** Creates an expression manager. */
   ExprManager();
-
-  /**
-   * Creates an expression manager.
-   *
-   * @param options the earlyTypeChecking field is used to configure
-   * whether to do at Expr creation time.
-   */
-  explicit ExprManager(const Options& options);
-
  public:
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
@@ -109,12 +98,6 @@ class CVC4_PUBLIC ExprManager {
    */
   ~ExprManager();
 
-  /** Get this expr manager's options */
-  const Options& getOptions() const;
-
-  /** Get this expr manager's resource manager */
-  ResourceManager* getResourceManager();
-
   /** Get the type for booleans */
   BooleanType booleanType() const;
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 88c4db778..c68b0df86 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -26,7 +26,6 @@
 #include "expr/attribute.h"
 #include "expr/dtype.h"
 #include "expr/node_manager_attributes.h"
-#include "expr/node_manager_listeners.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
 #include "options/options.h"
@@ -93,11 +92,8 @@ namespace attr {
 typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
 
 NodeManager::NodeManager(ExprManager* exprManager)
-    : d_options(new Options()),
-      d_statisticsRegistry(new StatisticsRegistry()),
-      d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
+    : d_statisticsRegistry(new StatisticsRegistry()),
       d_skManager(new SkolemManager),
-      d_registrations(new ListenerRegistrationList()),
       next_id(0),
       d_attrManager(new expr::attr::AttributeManager()),
       d_exprManager(exprManager),
@@ -109,24 +105,6 @@ NodeManager::NodeManager(ExprManager* exprManager)
   init();
 }
 
-NodeManager::NodeManager(ExprManager* exprManager, const Options& options)
-    : d_options(new Options()),
-      d_statisticsRegistry(new StatisticsRegistry()),
-      d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
-      d_skManager(new SkolemManager),
-      d_registrations(new ListenerRegistrationList()),
-      next_id(0),
-      d_attrManager(new expr::attr::AttributeManager()),
-      d_exprManager(exprManager),
-      d_nodeUnderDeletion(NULL),
-      d_inReclaimZombies(false),
-      d_abstractValueCount(0),
-      d_skolemCounter(0)
-{
-  d_options->copyValues(options);
-  init();
-}
-
 void NodeManager::init() {
   poolInsert( &expr::NodeValue::null() );
 
@@ -137,32 +115,6 @@ void NodeManager::init() {
       d_operators[i] = mkConst(Kind(k));
     }
   }
-  d_resourceManager->setHardLimit((*d_options)[options::hardLimit]);
-  if((*d_options)[options::perCallResourceLimit] != 0) {
-    d_resourceManager->setResourceLimit((*d_options)[options::perCallResourceLimit], false);
-  }
-  if((*d_options)[options::cumulativeResourceLimit] != 0) {
-    d_resourceManager->setResourceLimit((*d_options)[options::cumulativeResourceLimit], true);
-  }
-  if((*d_options)[options::perCallMillisecondLimit] != 0) {
-    d_resourceManager->setTimeLimit((*d_options)[options::perCallMillisecondLimit], false);
-  }
-  if((*d_options)[options::cumulativeMillisecondLimit] != 0) {
-    d_resourceManager->setTimeLimit((*d_options)[options::cumulativeMillisecondLimit], true);
-  }
-  if((*d_options)[options::cpuTime]) {
-    d_resourceManager->useCPUTime(true);
-  }
-
-  // Do not notify() upon registration as these were handled manually above.
-  d_registrations->add(d_options->registerTlimitListener(
-      new TlimitListener(d_resourceManager), false));
-  d_registrations->add(d_options->registerTlimitPerListener(
-      new TlimitPerListener(d_resourceManager), false));
-  d_registrations->add(d_options->registerRlimitListener(
-      new RlimitListener(d_resourceManager), false));
-  d_registrations->add(d_options->registerRlimitPerListener(
-      new RlimitPerListener(d_resourceManager), false));
 }
 
 NodeManager::~NodeManager() {
@@ -234,16 +186,10 @@ NodeManager::~NodeManager() {
   }
 
   // defensive coding, in case destruction-order issues pop up (they often do)
-  delete d_resourceManager;
-  d_resourceManager = NULL;
   delete d_statisticsRegistry;
   d_statisticsRegistry = NULL;
-  delete d_registrations;
-  d_registrations = NULL;
   delete d_attrManager;
   d_attrManager = NULL;
-  delete d_options;
-  d_options = NULL;
 }
 
 size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt)
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 098ff8eea..499cba457 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -109,20 +109,11 @@ class NodeManager {
 
   static thread_local NodeManager* s_current;
 
-  Options* d_options;
   StatisticsRegistry* d_statisticsRegistry;
 
-  ResourceManager* d_resourceManager;
-
   /** The skolem manager */
   std::shared_ptr<SkolemManager> d_skManager;
 
-  /**
-   * A list of registrations on d_options to that call into d_resourceManager.
-   * These must be garbage collected before d_options and d_resourceManager.
-   */
-  ListenerRegistrationList* d_registrations;
-
   NodeValuePool d_nodeValuePool;
 
   size_t next_id;
@@ -389,26 +380,10 @@ class NodeManager {
 public:
 
   explicit NodeManager(ExprManager* exprManager);
-  explicit NodeManager(ExprManager* exprManager, const Options& options);
   ~NodeManager();
 
   /** The node manager in the current public-facing CVC4 library context */
   static NodeManager* currentNM() { return s_current; }
-  /** The resource manager associated with the current node manager */
-  static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
-
-  /** Get this node manager's options (const version) */
-  const Options& getOptions() const {
-    return *d_options;
-  }
-
-  /** Get this node manager's options (non-const version) */
-  Options& getOptions() {
-    return *d_options;
-  }
-
-  /** Get this node manager's resource manager */
-  ResourceManager* getResourceManager() { return d_resourceManager; }
   /** Get this node manager's skolem manager */
   SkolemManager* getSkolemManager() { return d_skManager.get(); }
 
@@ -1037,25 +1012,19 @@ public:
 class NodeManagerScope {
   /** The old NodeManager, to be restored on destruction. */
   NodeManager* d_oldNodeManager;
-  Options::OptionsScope d_optionsScope;
 public:
-
-  NodeManagerScope(NodeManager* nm)
-      : d_oldNodeManager(NodeManager::s_current)
-      , d_optionsScope(nm ? nm->d_options : NULL) {
-    // There are corner cases where nm can be NULL and it's ok.
-    // For example, if you write { Expr e; }, then when the null
-    // Expr is destructed, there's no active node manager.
-    //Assert(nm != NULL);
-    NodeManager::s_current = nm;
-    //Options::s_current = nm ? nm->d_options : NULL;
-    Debug("current") << "node manager scope: "
-                     << NodeManager::s_current << "\n";
+ NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
+ {
+   // There are corner cases where nm can be NULL and it's ok.
+   // For example, if you write { Expr e; }, then when the null
+   // Expr is destructed, there's no active node manager.
+   // Assert(nm != NULL);
+   NodeManager::s_current = nm;
+   Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
 
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
-    //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
     Debug("current") << "node manager scope: "
                      << "returning to " << NodeManager::s_current << "\n";
   }
diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp
deleted file mode 100644
index 56a827deb..000000000
--- a/src/expr/node_manager_listeners.cpp
+++ /dev/null
@@ -1,44 +0,0 @@
-/*********************                                                        */
-/*! \file node_manager_listeners.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Listeners that NodeManager registers to its Options object.
- **
- ** Listeners that NodeManager registers to its Options object.
- **/
-
-#include "node_manager_listeners.h"
-
-#include "base/listener.h"
-#include "options/smt_options.h"
-#include "util/resource_manager.h"
-
-namespace CVC4 {
-namespace expr {
-
-
-void TlimitListener::notify() {
-  d_rm->setTimeLimit(options::cumulativeMillisecondLimit(), true);
-}
-
-void TlimitPerListener::notify() {
-  d_rm->setTimeLimit(options::perCallMillisecondLimit(), false);
-}
-
-void RlimitListener::notify() {
-  d_rm->setTimeLimit(options::cumulativeResourceLimit(), true);
-}
-
-void RlimitPerListener::notify() {
-  d_rm->setTimeLimit(options::perCallResourceLimit(), false);
-}
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h
deleted file mode 100644
index e296b7ec6..000000000
--- a/src/expr/node_manager_listeners.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file node_manager_listeners.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Listeners that NodeManager registers to its Options object.
- **
- ** Listeners that NodeManager registers to its Options object.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__EXPR__NODE_MANAGER_LISTENERS_H
-#define CVC4__EXPR__NODE_MANAGER_LISTENERS_H
-
-#include "base/listener.h"
-#include "util/resource_manager.h"
-
-namespace CVC4 {
-namespace expr {
-
-class TlimitListener : public Listener {
- public:
-  TlimitListener(ResourceManager* rm) : d_rm(rm) {}
-  void notify() override;
-
- private:
-  ResourceManager* d_rm;
-};
-
-class TlimitPerListener : public Listener {
- public:
-  TlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
-  void notify() override;
-
- private:
-  ResourceManager* d_rm;
-};
-
-class RlimitListener : public Listener {
- public:
-  RlimitListener(ResourceManager* rm) : d_rm(rm) {}
-  void notify() override;
-
- private:
-  ResourceManager* d_rm;
-};
-
-class RlimitPerListener : public Listener {
- public:
-  RlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
-  void notify() override;
-
- private:
-  ResourceManager* d_rm;
-};
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR__NODE_MANAGER_LISTENERS_H */