General subscriber infrastructure for NodeManager, as discussed in the

meeting last week.  The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.

The way to create a skolem is now:

  nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")

The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name).  Without a "$$", a "_$$"
is automatically appended to the given name.

The second argument is the type.

The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.

An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name).  Look at the documentation for details on these.

In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment.  This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.

Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit.  Some remains to be cleaned up.

(this commit was certified error- and warning-free by the test-and-commit script.)

6 files changed, 170 insertions, 60 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 53ca266f4..8b61e92d3 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -479,8 +479,6 @@ Type DeclareFunctionCommand::getType() const throw() {
 }
 
 void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this;
-  smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_FUN );
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -511,8 +509,6 @@ Type DeclareTypeCommand::getType() const throw() {
 }
 
 void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this;
-  smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_SORT );
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -552,7 +548,6 @@ Type DefineTypeCommand::getType() const throw() {
 }
 
 void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this;
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -602,7 +597,6 @@ Expr DefineFunctionCommand::getFormula() const throw() {
 }
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
-  //Dump("declarations") << *this; -- done by SmtEngine
   try {
     if(!d_func.isNull()) {
       smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -1275,8 +1269,6 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
 }
 
 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
-  Dump("declarations") << *this;
-  smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_DATATYPES );
   d_commandStatus = CommandSuccess::instance();
 }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 804d3af9a..03f3a04b0 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -646,6 +646,10 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     checkResolvedDatatype(*i);
   }
 
+  for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewDatatypes(dtts);
+  }
+
   return dtts;
 }
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 08c3a2b1e..c607ca0a7 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -140,7 +140,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
           // skolems are only available at the Node level (not the Expr level)
           TypeNode typeNode = TypeNode::fromType(type);
           NodeManager* to_nm = NodeManager::fromExprManager(to);
-          Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety
+          Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety
           to_e = n.toExpr();
         } else {
           Unhandled();
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fc2eec774..82242cb1c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -139,7 +139,7 @@ NodeManager::~NodeManager() {
   poolRemove( &expr::NodeValue::s_null );
 
   if(Debug.isOn("gc:leaks")) {
-    Debug("gc:leaks") << "still in pool:" << std::endl;
+    Debug("gc:leaks") << "still in pool:" << endl;
     for(NodeValuePool::const_iterator i = d_nodeValuePool.begin(),
           iend = d_nodeValuePool.end();
         i != iend;
@@ -147,9 +147,9 @@ NodeManager::~NodeManager() {
       Debug("gc:leaks") << "  " << *i
                         << " id=" << (*i)->d_id
                         << " rc=" << (*i)->d_rc
-                        << " " << **i << std::endl;
+                        << " " << **i << endl;
     }
-    Debug("gc:leaks") << ":end:" << std::endl;
+    Debug("gc:leaks") << ":end:" << endl;
   }
 
   delete d_statisticsRegistry;
@@ -183,10 +183,10 @@ void NodeManager::reclaimZombies() {
 
   vector<NodeValue*> zombies;
   zombies.reserve(d_zombies.size());
-  std::remove_copy_if(d_zombies.begin(),
-                      d_zombies.end(),
-                      std::back_inserter(zombies),
-                      NodeValueReferenceCountNonZero());
+  remove_copy_if(d_zombies.begin(),
+                 d_zombies.end(),
+                 back_inserter(zombies),
+                 NodeValueReferenceCountNonZero());
   d_zombies.clear();
 
   for(vector<NodeValue*>::iterator i = zombies.begin();
@@ -200,7 +200,7 @@ void NodeManager::reclaimZombies() {
         Debug("gc") << "deleting node value " << nv
                     << " [" << nv->d_id << "]: ";
         nv->printAst(Debug("gc"));
-        Debug("gc") << std::endl;
+        Debug("gc") << endl;
       }
 
       // remove from the pool
@@ -251,7 +251,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
   bool hasType = getAttribute(n, TypeAttr(), typeNode);
   bool needsCheck = check && !getAttribute(n, TypeCheckedAttr());
 
-  Debug("getType") << "getting type for " << n << std::endl;
+  Debug("getType") << "getting type for " << n << endl;
 
   if(needsCheck && !(*d_options)[options::earlyTypeChecking]) {
     /* Iterate and compute the children bottom up. This avoids stack
@@ -295,28 +295,57 @@ TypeNode NodeManager::getType(TNode n, bool check)
   /* The check should have happened, if we asked for it. */
   Assert( !check || getAttribute(n, TypeCheckedAttr()) );
 
-  Debug("getType") << "type of " << n << " is " << typeNode << std::endl;
+  Debug("getType") << "type of " << n << " is " << typeNode << endl;
   return typeNode;
 }
 
+Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const std::string& comment, int flags) {
+  Node n = NodeBuilder<0>(this, kind::SKOLEM);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
+  if((flags & SKOLEM_EXACT_NAME) == 0) {
+    size_t pos = name.find("$$");
+    if(pos != string::npos) {
+      // replace a "$$" with the node ID
+      stringstream id;
+      id << n.getId();
+      string newName = name;
+      newName.replace(pos, 2, id.str());
+      setAttribute(n, expr::VarNameAttr(), newName);
+    } else {
+      stringstream newName;
+      newName << name << '_' << n.getId();
+      setAttribute(n, expr::VarNameAttr(), newName.str());
+    }
+  } else {
+    setAttribute(n, expr::VarNameAttr(), name);
+  }
+  if((flags & SKOLEM_NO_NOTIFY) == 0) {
+    for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+      (*i)->nmNotifyNewSkolem(n, comment);
+    }
+  }
+  return n;
+}
+
 TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
                                         TypeNode range) {
-  std::vector<TypeNode> sorts;
-  Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
+  vector<TypeNode> sorts;
+  Debug("datatypes") << "ctor name: " << constructor.getName() << endl;
   for(DatatypeConstructor::const_iterator i = constructor.begin();
       i != constructor.end();
       ++i) {
     TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
-    Debug("datatypes") << selectorType << std::endl;
+    Debug("datatypes") << selectorType << endl;
     TypeNode sort = selectorType[1];
 
     // should be guaranteed here already, but just in case
     Assert(!sort.isFunctionLike());
 
-    Debug("datatypes") << "ctor sort: " << sort << std::endl;
+    Debug("datatypes") << "ctor sort: " << sort << endl;
     sorts.push_back(sort);
   }
-  Debug("datatypes") << "ctor range: " << range << std::endl;
+  Debug("datatypes") << "ctor range: " << range << endl;
   CheckArgument(!range.isFunctionLike(), range,
                 "cannot create higher-order function types");
   sorts.push_back(range);
@@ -335,7 +364,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
   TypeNode tn = lambdan.getType();
   if(! tn.isPredicateLike() ||
      tn.getArgTypes().size() != 1) {
-    std::stringstream ss;
+    stringstream ss;
     ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
     throw TypeCheckingExceptionPrivate(lambdan, ss.str());
   }
@@ -355,7 +384,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
   TypeNode tn = lambdan.getType();
   if(! tn.isPredicateLike() ||
      tn.getArgTypes().size() != 1) {
-    std::stringstream ss;
+    stringstream ss;
     ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
     throw TypeCheckingExceptionPrivate(lambdan, ss.str());
   }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 27d77a646..893fde64b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -63,6 +63,21 @@ typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 
 }/* CVC4::expr namespace */
 
+/**
+ * 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) { }
+  virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
+  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
+  virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
+  virtual void nmNotifyNewVar(TNode n) { }
+  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment) { }
+};/* class NodeManagerListener */
+
 class NodeManager {
   template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
   friend class NodeManagerScope;
@@ -70,8 +85,11 @@ class NodeManager {
   friend class expr::TypeChecker;
 
   // friends so they can access mkVar() here, which is private
-  friend Expr ExprManager::mkVar(const std::string& name, Type type);
-  friend Expr ExprManager::mkVar(Type type);
+  friend Expr ExprManager::mkVar(const std::string&, Type);
+  friend Expr ExprManager::mkVar(Type);
+
+  // friend so it can access NodeManager's d_listeners and notify clients
+  friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
@@ -138,6 +156,11 @@ class NodeManager {
   Node d_operators[kind::LAST_KIND];
 
   /**
+   * A list of subscribers for NodeManager events.
+   */
+  std::vector<NodeManagerListener*> d_listeners;
+
+  /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
    * NodeValue.  In particular, "non-inlined" constants are permitted
@@ -299,6 +322,19 @@ public:
     return d_statisticsRegistry;
   }
 
+  /** 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);
+  }
+
   // general expression-builders
 
   /** Create a node with one child. */
@@ -371,9 +407,39 @@ public:
   Node mkBoundVar(const TypeNode& type);
   Node* mkBoundVarPtr(const TypeNode& type);
 
-  /** Create a skolem constant with the given type. */
-  Node mkSkolem(const TypeNode& type);
-  Node mkSkolem(const std::string& name, const TypeNode& type);
+  /**
+   * Optional flags used to control behavior of NodeManager::mkSkolem().
+   * They should be composed with a bitwise OR (e.g.,
+   * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
+   * cannot be composed in such a manner.
+   */
+  enum SkolemFlags {
+    SKOLEM_DEFAULT = 0,   /**< default behavior */
+    SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
+    SKOLEM_EXACT_NAME = 2 /**< do not make the name unique by adding the id */
+  };/* enum SkolemFlags */
+
+  /**
+   * Create a skolem constant with the given name, type, and comment.
+   *
+   * @param name the name of the new skolem variable.  This name can
+   * contain the special character sequence "$$", in which case the
+   * $$ is replaced with the Node ID.  That way a family of skolem
+   * variables can be made with unique identifiers, used in dump,
+   * tracing, and debugging output.  By convention, you should probably
+   * call mkSkolem() with a custom name appended with "_$$".
+   *
+   * @param type the type of the skolem variable to create
+   *
+   * @param comment a comment for dumping output; if declarations are
+   * being dumped, this is included in a comment before the declaration
+   * and can be quite useful for debugging
+   *
+   * @param flags an optional mask of bits from SkolemFlags to control
+   * mkSkolem() behavior
+   */
+  Node mkSkolem(const std::string& name, const TypeNode& type,
+                const std::string& comment = "", int flags = SKOLEM_DEFAULT);
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
@@ -1118,13 +1184,23 @@ inline TypeNode NodeManager::mkSort() {
   NodeBuilder<1> nb(this, kind::SORT_TYPE);
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
   nb << sortTag;
-  return nb.constructTypeNode();
+  TypeNode tn = nb.constructTypeNode();
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewSort(tn);
+  }
+  return tn;
 }
 
 inline TypeNode NodeManager::mkSort(const std::string& name) {
-  TypeNode type = mkSort();
-  setAttribute(type, expr::VarNameAttr(), name);
-  return type;
+  NodeBuilder<1> nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  nb << sortTag;
+  TypeNode tn = nb.constructTypeNode();
+  setAttribute(tn, expr::VarNameAttr(), name);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewSort(tn);
+  }
+  return tn;
 }
 
 inline TypeNode NodeManager::mkSort(TypeNode constructor,
@@ -1145,6 +1221,9 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
   nb.append(children);
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyInstantiateSortConstructor(constructor, type);
+  }
   return type;
 }
 
@@ -1157,6 +1236,9 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
   setAttribute(type, expr::SortArityAttr(), arity);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewSortConstructor(type);
+  }
   return type;
 }
 
@@ -1368,15 +1450,25 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 
 
 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
-  Node n = mkVar(type);
+  Node n = NodeBuilder<0>(this, kind::VARIABLE);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(n);
+  }
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const std::string& name,
                                    const TypeNode& type) {
-  Node* n = mkVarPtr(type);
+  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
   setAttribute(*n, expr::VarNameAttr(), name);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(*n);
+  }
   return n;
 }
 
@@ -1397,6 +1489,9 @@ inline Node NodeManager::mkVar(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(n);
+  }
   return n;
 }
 
@@ -1404,6 +1499,9 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(*n);
+  }
   return n;
 }
 
@@ -1421,19 +1519,6 @@ inline Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
   return n;
 }
 
-inline Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type) {
-  Node n = mkSkolem(type);
-  setAttribute(n, expr::VarNameAttr(), name);
-  return n;
-}
-
-inline Node NodeManager::mkSkolem(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::SKOLEM);
-  setAttribute(n, TypeAttr(), type);
-  setAttribute(n, TypeCheckedAttr(), true);
-  return n;
-}
-
 inline Node NodeManager::mkInstConstant(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
   n.setAttribute(TypeAttr(), type);
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index c9234b5e0..e3bd898ef 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -50,7 +50,7 @@ SymbolTable::~SymbolTable() {
 }
 
 void SymbolTable::bind(const std::string& name, Expr obj,
-                            bool levelZero) throw(AssertionException) {
+                       bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
@@ -58,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj,
 }
 
 void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
-                            bool levelZero) throw(AssertionException) {
+                                      bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero){
@@ -89,18 +89,18 @@ Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException
 }
 
 void SymbolTable::bindType(const std::string& name, Type t,
-                                bool levelZero) throw() {
-  if(levelZero){
+                           bool levelZero) throw() {
+  if(levelZero) {
     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
-  }else{
+  } else {
     d_typeMap->insert(name, make_pair(vector<Type>(), t));
   }
 }
 
 void SymbolTable::bindType(const std::string& name,
-                                const std::vector<Type>& params,
-                                Type t,
-                                bool levelZero) throw() {
+                           const std::vector<Type>& params,
+                           Type t,
+                           bool levelZero) throw() {
   if(Debug.isOn("sort")) {
     Debug("sort") << "bindType(" << name << ", [";
     if(params.size() > 0) {
@@ -110,7 +110,7 @@ void SymbolTable::bindType(const std::string& name,
     }
     Debug("sort") << "], " << t << ")" << endl;
   }
-  if(levelZero){
+  if(levelZero) {
     d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
   } else {
     d_typeMap->insert(name, make_pair(params, t));
@@ -131,7 +131,7 @@ Type SymbolTable::lookupType(const std::string& name) const throw(AssertionExcep
 }
 
 Type SymbolTable::lookupType(const std::string& name,
-                                  const std::vector<Type>& params) const throw(AssertionException) {
+                             const std::vector<Type>& params) const throw(AssertionException) {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   Assert(p.first.size() == params.size(),
          "type constructor arity is wrong: "