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.)

11 files changed, 53 insertions, 24 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 85742feef..f8e754868 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -187,7 +187,7 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* AstPrinter::toStream(CommandStatus*) */
 
-void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){
+void AstPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
   out << "Model()";
 }
 
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 1cac966df..d5701c088 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -36,7 +36,7 @@ public:
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   //for models
-  void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw();
+  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
 };/* class AstPrinter */
 
 }/* CVC4::printer::ast namespace */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 7f66d6fa0..6791b6c51 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -738,10 +738,10 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
-void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){
+void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
   theory::TheoryModel* tm = (theory::TheoryModel*)m;
-  if( c_type==Model::COMMAND_DECLARE_SORT ){
-    TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() );
+  if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
+    TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( tn.isSort() ){
       //print the cardinality
       if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
@@ -761,8 +761,8 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type )
         }
       }
     }
-  }else if( c_type==Model::COMMAND_DECLARE_FUN ){
-    Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() );
+  } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
+    Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
     TypeNode tn = n.getType();
     out << n << " : ";
     if( tn.isFunction() || tn.isPredicate() ){
@@ -959,12 +959,41 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
 
 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
+  out << "DATATYPE" << endl;
+  bool firstDatatype = true;
   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
         i_end = datatypes.end();
       i != i_end;
       ++i) {
-    out << *i;
+    if(! firstDatatype) {
+      out << ',' << endl;
+    }
+    const Datatype& dt = (*i).getDatatype();
+    out << "  " << dt.getName() << " = ";
+    bool firstConstructor = true;
+    for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
+      if(! firstConstructor) {
+        out << " | ";
+      }
+      firstConstructor = false;
+      const DatatypeConstructor& c = *j;
+      out << c.getName();
+      if(c.getNumArgs() > 0) {
+        out << '(';
+        bool firstSelector = true;
+        for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
+          if(! firstSelector) {
+            out << ", ";
+          }
+          firstSelector = false;
+          const DatatypeConstructorArg& selector = *k;
+          out << selector.getName() << ": " << selector.getType();
+        }
+        out << ')';
+      }
+    }
   }
+  out << endl << "END;" << endl;
 }
 
 static void toStream(std::ostream& out, const CommentCommand* c) throw() {
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index c868025ef..72564f24d 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -39,7 +39,7 @@ public:
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   //for models
-  void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw();
+  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
 };/* class CvcPrinter */
 
 }/* CVC4::printer::cvc namespace */
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 40b532612..98d6a26bb 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -136,7 +136,7 @@ void DagificationVisitor::done(TNode node) {
     // construct the let binder
     std::stringstream ss;
     ss << d_letVarPrefix << d_letVar++;
-    Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType());
+    Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 
     // apply previous substitutions to the rhs, enabling cascading LETs
     Node n = d_substitutions->apply(*i);
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 54482a8c3..eed9842e2 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -128,8 +128,8 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
 }/* Printer::toStream(SExpr) */
 
 void Printer::toStream(std::ostream& out, Model* m) const throw() {
-  for(size_t i = 0; i < m->getNumCommands(); i++ ){
-    toStream(out, m, m->getCommand(i), m->getCommandType(i));
+  for(size_t i = 0; i < m->getNumCommands(); ++i) {
+    toStream(out, m, m->getCommand(i));
   }
 }/* Printer::toStream(Model) */
 
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 6fedc854c..778c21f1f 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -83,7 +83,7 @@ public:
   //for models
 
   /** write model response to command */
-  virtual void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw() = 0;
+  virtual void toStream(std::ostream& out, Model* m, const Command* c) const throw() = 0;
 };/* class Printer */
 
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index 14a680a1e..bc61368c1 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -51,8 +51,8 @@ void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 }/* SmtPrinter::toStream() */
 
-void SmtPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c, c_type);
+void SmtPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c);
 }
 
 }/* CVC4::printer::smt namespace */
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 1cf7fcf50..a3d62a287 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -36,7 +36,7 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
   //for models
-  void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw();
+  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
 };/* class SmtPrinter */
 
 }/* CVC4::printer::smt namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e41fd9c65..28ecc11c4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -320,8 +320,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     // output that support for the kind needs to be added here.
     out << n.getKind() << ' ';
   }
-  if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
-     stillNeedToPrintParams) {
+  if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
+      stillNeedToPrintParams ) {
     if(toDepth != 0) {
       toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
     } else {
@@ -528,10 +528,10 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 }/* Smt2Printer::toStream(CommandStatus*) */
 
 
-void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){
+void Smt2Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
   theory::TheoryModel* tm = (theory::TheoryModel*)m;
-  if( c_type==Model::COMMAND_DECLARE_SORT ){
-    TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() );
+  if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
+    TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( tn.isSort() ){
       //print the cardinality
       if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){
@@ -551,8 +551,8 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type )
         }
       }
     }
-  }else if( c_type==Model::COMMAND_DECLARE_FUN ){
-    Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() );
+  } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
+    Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
     Node val = tm->getValue( n );
     if(val.getKind() == kind::LAMBDA) {
       out << "(define-fun " << n << " " << val[0]
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 475479095..ce48f36f3 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -36,7 +36,7 @@ public:
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   //for models
-  void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw();
+  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
   void toStream(std::ostream& out, const Result& r) const throw();
 };/* class Smt2Printer */