Replace the old dump infrastructure (#7572)

This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.

This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.

This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.

The other dumping tags are deleted for now, and will be reimplemented as needed.

1 files changed, 0 insertions, 44 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5b5f07e6f..d0c607a4b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -56,30 +56,6 @@ namespace expr {
   class TypeChecker;
   }  // namespace expr
 
-/**
- * An interface that an interested party can implement and then subscribe
- * to NodeManager events via NodeManager::subscribeEvents(this).
- */
-class NodeManagerListener {
- public:
-  virtual ~NodeManagerListener() {}
-  virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {}
-  virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {}
-  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
-                                                  uint32_t flags) {}
-  virtual void nmNotifyNewDatatypes(const std::vector<TypeNode>& datatypes,
-                                    uint32_t flags)
-  {
-  }
-  virtual void nmNotifyNewVar(TNode n) {}
-  /**
-   * Notify a listener of a Node that's being GCed.  If this function stores a
-   * reference
-   * to the Node somewhere, very bad things will happen.
-   */
-  virtual void nmNotifyDeleteNode(TNode n) {}
-}; /* class NodeManagerListener */
-
 class NodeManager
 {
   friend class api::Solver;
@@ -175,11 +151,6 @@ class NodeManager
   /** unique vars per (Kind,Type) */
   std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
 
-  /**
-   * A list of subscribers for NodeManager events.
-   */
-  std::vector<NodeManagerListener*> d_listeners;
-
   /** A list of datatypes owned by this node manager */
   std::vector<std::unique_ptr<DType> > d_dtypes;
 
@@ -370,21 +341,6 @@ class NodeManager
   /** Get this node manager's bound variable manager */
   BoundVarManager* getBoundVarManager() { return d_bvManager.get(); }
 
-  /** Subscribe to NodeManager events */
-  void subscribeEvents(NodeManagerListener* listener) {
-    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener)
-           == d_listeners.end())
-        << "listener already subscribed";
-    d_listeners.push_back(listener);
-  }
-
-  /** Unsubscribe from NodeManager events */
-  void unsubscribeEvents(NodeManagerListener* listener) {
-    std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
-    Assert(elt != d_listeners.end()) << "listener not subscribed";
-    d_listeners.erase(elt);
-  }
-
   /**
    * Return the datatype at the given index owned by this class. Type nodes are
    * associated with datatypes through the DatatypeIndexConstant class. The