Split listener classes from SmtEngine (#4816)

This moves listener classes owned by SmtEngine to their own file.

The SmtEnginePrivate class previously what itself a NodeManagerListener. This class will be deleted. Instead a new NodeManagerListener is introduced here whose sole responsibility is to do the work required for node manager listening.

Note I had to add a (temporary) friend relationship to SmtEngine, which will be removed in an upcoming PR to split the management of dumping to its own utility.

5 files changed, 197 insertions, 86 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 59b559cb2..53d049411 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -230,6 +230,8 @@ libcvc4_add_sources(
   smt/defined_function.h
   smt/dump.cpp
   smt/dump.h
+  smt/listeners.cpp
+  smt/listeners.h
   smt/logic_exception.h
   smt/logic_request.cpp
   smt/logic_request.h
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
new file mode 100644
index 000000000..5cfbfd1c5
--- /dev/null
+++ b/src/smt/listeners.cpp
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file listeners.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Implements listener classes for SMT engine.
+ **/
+
+#include "smt/listeners.h"
+
+#include "expr/attribute.h"
+#include "expr/expr.h"
+#include "expr/node_manager_attributes.h"
+#include "options/smt_options.h"
+#include "smt/command.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace smt {
+
+ResourceOutListener::ResourceOutListener(SmtEngine& smt) : d_smt(smt) {}
+
+void ResourceOutListener::notify()
+{
+  SmtScope scope(&d_smt);
+  Assert(smt::smtEngineInScope());
+  d_smt.interrupt();
+}
+
+SmtNodeManagerListener::SmtNodeManagerListener(SmtEngine& smt) : d_smt(smt) {}
+
+void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
+{
+  DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType());
+  if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
+  {
+    d_smt.addToModelCommandAndDump(c, flags);
+  }
+}
+
+void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
+                                                        uint32_t flags)
+{
+  DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
+                       tn.getAttribute(expr::SortArityAttr()),
+                       tn.toType());
+  if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
+  {
+    d_smt.addToModelCommandAndDump(c);
+  }
+}
+
+void SmtNodeManagerListener::nmNotifyNewDatatypes(
+    const std::vector<DatatypeType>& dtts, uint32_t flags)
+{
+  if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
+  {
+    std::vector<Type> types(dtts.begin(), dtts.end());
+    DatatypeDeclarationCommand c(types);
+    d_smt.addToModelCommandAndDump(c);
+  }
+}
+
+void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags)
+{
+  DeclareFunctionCommand c(
+      n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType());
+  if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
+  {
+    d_smt.addToModelCommandAndDump(c, flags);
+  }
+}
+
+void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
+                                               const std::string& comment,
+                                               uint32_t flags)
+{
+  std::string id = n.getAttribute(expr::VarNameAttr());
+  DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
+  if (Dump.isOn("skolems") && comment != "")
+  {
+    Dump("skolems") << CommentCommand(id + " is " + comment);
+  }
+  if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
+  {
+    d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
new file mode 100644
index 000000000..1eba41228
--- /dev/null
+++ b/src/smt/listeners.h
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file listeners.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Listener classes for SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__LISTENERS_H
+#define CVC4__SMT__LISTENERS_H
+
+#include <vector>
+
+#include "base/listener.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/** A listener for resource outs */
+class ResourceOutListener : public Listener
+{
+ public:
+  ResourceOutListener(SmtEngine& smt);
+  /** notify method, interupts SmtEngine */
+  void notify() override;
+
+ private:
+  /** Reference to the SmtEngine */
+  SmtEngine& d_smt;
+};
+
+/**
+ * A listener for node manager calls, which impacts certain dumping traces.
+ */
+class SmtNodeManagerListener : public NodeManagerListener
+{
+ public:
+  SmtNodeManagerListener(SmtEngine& smt);
+  /** Notify when new sort is created */
+  void nmNotifyNewSort(TypeNode tn, uint32_t flags) override;
+  /** Notify when new sort constructor is created */
+  void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override;
+  /** Notify when list of datatypes is created */
+  void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
+                            uint32_t flags) override;
+  /** Notify when new variable is created */
+  void nmNotifyNewVar(TNode n, uint32_t flags) override;
+  /** Notify when new skolem is created */
+  void nmNotifyNewSkolem(TNode n,
+                         const std::string& comment,
+                         uint32_t flags) override;
+  /** Notify when a term is deleted */
+  void nmNotifyDeleteNode(TNode n) override {}
+
+ private:
+  /** Reference to the smt engine */
+  SmtEngine& d_smt;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d8657c7dd..5d34e6fa2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -34,7 +34,6 @@
 #include "base/configuration.h"
 #include "base/configuration_private.h"
 #include "base/exception.h"
-#include "base/listener.h"
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "context/cdhashmap.h"
@@ -86,6 +85,7 @@
 #include "smt/command.h"
 #include "smt/command_list.h"
 #include "smt/defined_function.h"
+#include "smt/listeners.h"
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
@@ -147,19 +147,6 @@ void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
   commands.clear();
 }
 
-class ResourceOutListener : public Listener {
- public:
-  ResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
-  void notify() override
-  {
-    SmtScope scope(d_smt);
-    Assert(smt::smtEngineInScope());
-    d_smt->interrupt();
-  }
- private:
-  SmtEngine* d_smt;
-}; /* class ResourceOutListener */
-
 /**
  * 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
@@ -174,20 +161,13 @@ class ResourceOutListener : public Listener {
  * one) becomes an "interface shell" which simply acts as a forwarder
  * of method calls.
  */
-class SmtEnginePrivate : public NodeManagerListener {
+class SmtEnginePrivate
+{
   SmtEngine& d_smt;
 
   typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
-  /**
-   * Manager for limiting time and abstract resource usage.
-   */
-  ResourceManager* d_resourceManager;
-
-  /** Resource out listener */
-  std::unique_ptr<ResourceOutListener> d_routListener;
-
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
 
@@ -240,7 +220,6 @@ class SmtEnginePrivate : public NodeManagerListener {
  public:
   SmtEnginePrivate(SmtEngine& smt)
       : d_smt(smt),
-        d_routListener(new ResourceOutListener(d_smt)),
         d_propagator(true, true),
         d_assertions(),
         d_assertionsProcessed(smt.getUserContext(), false),
@@ -249,10 +228,7 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_iteRemover(smt.getUserContext()),
         d_sygusConjectureStale(smt.getUserContext(), true)
   {
-    d_smt.d_nodeManager->subscribeEvents(this);
     d_true = NodeManager::currentNM()->mkConst(true);
-    ResourceManager* rm = d_smt.getResourceManager();
-    rm->registerListener(d_routListener.get());
   }
 
   ~SmtEnginePrivate()
@@ -261,7 +237,6 @@ class SmtEnginePrivate : public NodeManagerListener {
       d_propagator.finish();
       d_propagator.setNeedsFinish(false);
     }
-    d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
   void spendResource(ResourceManager::Resource r)
@@ -271,64 +246,6 @@ class SmtEnginePrivate : public NodeManagerListener {
 
   ProcessAssertions* getProcessAssertions() { return &d_processor; }
 
-  void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
-  {
-    DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
-                         0,
-                         tn.toType());
-    if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) {
-      d_smt.addToModelCommandAndDump(c, flags);
-    }
-  }
-
-  void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override
-  {
-    DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
-                         tn.getAttribute(expr::SortArityAttr()),
-                         tn.toType());
-    if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
-    {
-      d_smt.addToModelCommandAndDump(c);
-    }
-  }
-
-  void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
-                            uint32_t flags) override
-  {
-    if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
-    {
-      std::vector<Type> types(dtts.begin(), dtts.end());
-      DatatypeDeclarationCommand c(types);
-      d_smt.addToModelCommandAndDump(c);
-    }
-  }
-
-  void nmNotifyNewVar(TNode n, uint32_t flags) override
-  {
-    DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
-                             n.toExpr(),
-                             n.getType().toType());
-    if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
-      d_smt.addToModelCommandAndDump(c, flags);
-    }
-  }
-
-  void nmNotifyNewSkolem(TNode n,
-                         const std::string& comment,
-                         uint32_t flags) override
-  {
-    string id = n.getAttribute(expr::VarNameAttr());
-    DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
-    if(Dump.isOn("skolems") && comment != "") {
-      Dump("skolems") << CommentCommand(id + " is " + comment);
-    }
-    if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
-      d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
-    }
-  }
-
-  void nmNotifyDeleteNode(TNode n) override {}
-
   Node applySubstitutions(TNode node)
   {
     return Rewriter::rewrite(
@@ -421,6 +338,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
+      d_routListener(new ResourceOutListener(*this)),
+      d_snmListener(new SmtNodeManagerListener(*this)),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr),
       d_proofManager(nullptr),
@@ -474,6 +393,11 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       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));
+  // listen to node manager events
+  d_nodeManager->subscribeEvents(d_snmListener.get());
+  // listen to resource out
+  d_resourceManager->registerListener(d_routListener.get());
+  // make statistics
   d_stats.reset(new SmtEngineStatistics());
   
   // The ProofManager is constructed before any other proof objects such as
@@ -690,6 +614,9 @@ SmtEngine::~SmtEngine()
 
     d_stats.reset(nullptr);
     d_private.reset(nullptr);
+    d_nodeManager->unsubscribeEvents(d_snmListener.get());
+    d_snmListener.reset(nullptr);
+    d_routListener.reset(nullptr);
     d_optm.reset(nullptr);
     // d_resourceManager must be destroyed before d_statisticsRegistry
     d_resourceManager.reset(nullptr);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a651b8d1e..f260a307b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -93,6 +93,8 @@ namespace prop {
 namespace smt {
 /** Utilities */
 class AbstractValues;
+class ResourceOutListener;
+class SmtNodeManagerListener;
 class OptionsManager;
 /** Subsolvers */
 class AbductionSolver;
@@ -146,6 +148,8 @@ class CVC4_PUBLIC SmtEngine
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
   friend class ::CVC4::Model;  // to access d_modelCommands
+  friend class ::CVC4::smt::SmtNodeManagerListener;  // to access
+                                                     // addToModelCommandAndDump
   friend class ::CVC4::theory::TheoryModel;
   friend class ::CVC4::theory::Rewriter;
 
@@ -1122,6 +1126,10 @@ class CVC4_PUBLIC SmtEngine
   NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
+  /** Resource out listener */
+  std::unique_ptr<smt::ResourceOutListener> d_routListener;
+  /** Node manager listener */
+  std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
 
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;