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

5 files changed, 50 insertions, 51 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index bdb3f6cf6..522bcd935 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -414,7 +414,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
       string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
       (*i).d_name.resize((*i).d_name.find('\0'));
       if(typeName == "") {
-        (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode)).toExpr();
+        (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector").toExpr();
       } else {
         map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
         if(j == resolutions.end()) {
@@ -424,7 +424,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
               << "of constructor \"" << d_name << "\"";
           throw DatatypeResolutionException(msg.str());
         } else {
-          (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second))).toExpr();
+          (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector").toExpr();
         }
       }
     } else {
@@ -437,7 +437,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
       if(!paramTypes.empty() ) {
         range = doParametricSubstitution( range, paramTypes, paramReplacements );
       }
-      (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range))).toExpr();
+      (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector").toExpr();
     }
     Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
     (*i).d_resolved = true;
@@ -450,8 +450,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
   // fails above, we want Constuctor::isResolved() to remain "false".
   // Further, mkConstructorType() iterates over the selectors, so
   // should get the results of any resolutions we did above.
-  d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode)).toExpr();
-  d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode)).toExpr();
+  d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester").toExpr();
+  d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor").toExpr();
   // associate constructor with all selectors
   for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
     (*i).d_constructor = d_constructor;
@@ -521,7 +521,7 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(selectorType);
 
-  Expr type = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(selectorType)).toExpr();
+  Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName + "_$$", TypeNode::fromType(selectorType), "is an unresolved selector type placeholder").toExpr();
   Debug("datatypes") << type << endl;
   d_args.push_back(DatatypeConstructorArg(selectorName, type));
 }
diff --git a/src/util/dump.h b/src/util/dump.h
index 382092474..8e81086b2 100644
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -96,17 +96,6 @@ public:
   void clear() { d_commands.clear(); }
   const CommandSequence& getCommands() const { return d_commands; }
 
-  void declareVar(Expr e, std::string comment) {
-    if(isOn("declarations")) {
-      std::stringstream ss;
-      ss << Expr::setlanguage(Expr::setlanguage::getLanguage(getStream())) << e;
-      std::string s = ss.str();
-      CVC4dumpstream(getStream(), d_commands)
-        << CommentCommand(s + " is " + comment)
-        << DeclareFunctionCommand(s, e, e.getType());
-    }
-  }
-
   bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
   bool on (std::string tag) { d_tags.insert(tag); return true; }
   bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 50713e2b4..e8a539615 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -55,9 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
     TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean()) {
       // Make the skolem to represent the ITE
-      Node skolem = nodeManager->mkSkolem(nodeType);
-
-      Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");
+      Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
 
       // The new assertion
       Node newAssertion =
diff --git a/src/util/model.cpp b/src/util/model.cpp
index 50683fdff..8b0e956cf 100644
--- a/src/util/model.cpp
+++ b/src/util/model.cpp
@@ -2,14 +2,39 @@
 /*! \file model.cpp
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
  ** \brief implementation of Model class
- **/
\ No newline at end of file
+ **/
+
+#include "util/model.h"
+#include "expr/command.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/command_list.h"
+
+#include <vector>
+
+using namespace std;
+
+namespace CVC4 {
+
+Model::Model() :
+  d_smt(*smt::currentSmtEngine()) {
+}
+
+size_t Model::getNumCommands() const {
+  return d_smt.d_modelCommands->size();
+}
+
+const Command* Model::getCommand(size_t i) const {
+  return (*d_smt.d_modelCommands)[i];
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/model.h b/src/util/model.h
index 36a5464b4..97010dd45 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -2,10 +2,10 @@
 /*! \file model.h
  ** \verbatim
  ** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -27,41 +27,28 @@
 
 namespace CVC4 {
 
-class Command;
+class CVC4_PUBLIC Command;
+class CVC4_PUBLIC SmtEngine;
 
-class Model
-{
-public:
-  //types of commands that are recorded for get-model
-  enum {
-    COMMAND_DECLARE_SORT,       //DeclareTypeCommand
-    COMMAND_DECLARE_FUN,        //DeclareFunctionCommand
-    COMMAND_DECLARE_DATATYPES,  //DatatypeDeclarationCommand
-  };
+class CVC4_PUBLIC Model {
 private:
-  //list of commands that the model must report when calling get model
-  std::vector< Command* > d_commands;
-  std::vector< int > d_command_types;
+  /** The SmtEngine we're associated to */
+  const SmtEngine& d_smt;
 public:
+  /** construct the base class */
+  Model();
   /** virtual destructor */
-  virtual ~Model() {}
-  /** add command */
-  virtual void addCommand( Command* c, int c_type ){
-    d_commands.push_back( c );
-    d_command_types.push_back( c_type );
-  }
+  virtual ~Model() { }
   /** get number of commands to report */
-  size_t getNumCommands() { return d_commands.size(); }
+  size_t getNumCommands() const;
   /** get command */
-  Command* getCommand( int i ) { return d_commands[i]; }
-  /** get type of command */
-  int getCommandType( int i ) { return d_command_types[i]; }
+  const Command* getCommand(size_t i) const;
 public:
   /** get value for expression */
-  virtual Expr getValue( const Expr& expr ) = 0;
+  virtual Expr getValue(Expr expr) = 0;
   /** get cardinality for sort */
-  virtual Cardinality getCardinality( const Type& t ) = 0;
-  /** to stream function */
+  virtual Cardinality getCardinality(Type t) = 0;
+  /** write the model to a stream */
   virtual void toStream(std::ostream& out) = 0;
 };/* class Model */