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

4 files changed, 64 insertions, 72 deletions

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 93fbe049a..02de21635 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -74,7 +74,7 @@ public:
 
   void testDeallocation() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
     MyData* data;
     MyData* data1;
     MyDataAttribute attr;
@@ -92,7 +92,7 @@ public:
   typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
   void testInts(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
     const uint64_t val = 63489;
     uint64_t data0 = 0;
     uint64_t data1 = 0;
@@ -120,9 +120,9 @@ public:
   typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
   void testTNodes(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
 
-    Node val(d_nodeManager->mkSkolem(booleanType));
+    Node val(d_nodeManager->mkSkolem("b", booleanType));
     TNode data0;
     TNode data1;
 
@@ -155,7 +155,7 @@ public:
   typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
   void testPtrs(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
 
     Foo* val = new Foo(63489);
     Foo* data0 = NULL;
@@ -186,7 +186,7 @@ public:
   typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
   void testConstPtrs(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
 
     const Foo* val = new Foo(63489);
     const Foo* data0 = NULL;
@@ -216,7 +216,7 @@ public:
   typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
   void testStrings(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
 
     std::string val("63489");
     std::string data0;
@@ -245,7 +245,7 @@ public:
   typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
   void testBools(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
 
     bool val = true;
     bool data0 = false;
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 53af9db53..1518efadf 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -102,12 +102,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkSkolem(*d_booleanType);
+    b = d_nodeManager->mkSkolem("b", *d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkSkolem(*d_booleanType);
+    Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -142,12 +142,12 @@ public:
 
     Node a, b, c;
 
-    b = d_nodeManager->mkSkolem(*d_booleanType);
+    b = d_nodeManager->mkSkolem("b", *d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkSkolem(*d_booleanType);
+    Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a, !(a==a)));
@@ -204,7 +204,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem(*d_booleanType));
+    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
 
     b = c;
     TS_ASSERT(b==c);
@@ -268,8 +268,8 @@ public:
     /* Node eqNode(const Node& right) const; */
 
     TypeNode t = d_nodeManager->mkSort();
-    Node left = d_nodeManager->mkSkolem(t);
-    Node right = d_nodeManager->mkSkolem(t);
+    Node left = d_nodeManager->mkSkolem("left", t);
+    Node right = d_nodeManager->mkSkolem("right", t);
     Node eq = left.eqNode(right);
 
     TS_ASSERT(EQUAL == eq.getKind());
@@ -326,8 +326,8 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkSkolem(*d_booleanType);
-    Node b = d_nodeManager->mkSkolem(*d_booleanType);
+    Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
+    Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
 
     Node cnd = d_nodeManager->mkNode(OR, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -389,8 +389,8 @@ public:
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkSkolem(*d_booleanType);
-    Node b = d_nodeManager->mkSkolem(*d_booleanType);
+    Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
+    Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -398,8 +398,8 @@ public:
     n = d_nodeManager->mkNode(IFF, a, b);
     TS_ASSERT(IFF == n.getKind());
 
-    Node x = d_nodeManager->mkSkolem(*d_realType);
-    Node y = d_nodeManager->mkSkolem(*d_realType);
+    Node x = d_nodeManager->mkSkolem("x", *d_realType);
+    Node y = d_nodeManager->mkSkolem("y", *d_realType);
 
     n = d_nodeManager->mkNode(PLUS, x, y);
     TS_ASSERT(PLUS == n.getKind());
@@ -413,8 +413,8 @@ public:
     TypeNode booleanType = d_nodeManager->booleanType();
     TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
-    Node f = d_nodeManager->mkSkolem(predType);
-    Node a = d_nodeManager->mkSkolem(sort);
+    Node f = d_nodeManager->mkSkolem("f", predType);
+    Node a = d_nodeManager->mkSkolem("a", sort);
     Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
 
     TS_ASSERT( fa.hasOperator() );
@@ -476,9 +476,9 @@ public:
   // test iterators
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkSkolem(*d_booleanType);
-    Node y = d_nodeManager->mkSkolem(*d_booleanType);
-    Node z = d_nodeManager->mkSkolem(*d_booleanType);
+    Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+    Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
+    Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
     Node n = b << x << y << z << kind::AND;
 
     { // iterator
@@ -525,10 +525,10 @@ public:
   void testToString() {
     TypeNode booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkSkolem("w", booleanType);
-    Node x = d_nodeManager->mkSkolem("x", booleanType);
-    Node y = d_nodeManager->mkSkolem("y", booleanType);
-    Node z = d_nodeManager->mkSkolem("z", booleanType);
+    Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
     Node m = NodeBuilder<>() << w << x << kind::OR;
     Node n = NodeBuilder<>() << m << y << z << kind::AND;
 
@@ -538,10 +538,10 @@ public:
   void testToStream() {
     TypeNode booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkSkolem("w", booleanType);
-    Node x = d_nodeManager->mkSkolem("x", booleanType);
-    Node y = d_nodeManager->mkSkolem("y", booleanType);
-    Node z = d_nodeManager->mkSkolem("z", booleanType);
+    Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
     Node m = NodeBuilder<>() << x << y << kind::OR;
     Node n = NodeBuilder<>() << w << m << z << kind::AND;
     Node o = NodeBuilder<>() << n << n << kind::XOR;
@@ -600,10 +600,10 @@ public:
     TypeNode intType = d_nodeManager->integerType();
     TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
 
-    Node x = d_nodeManager->mkSkolem("x", intType);
-    Node y = d_nodeManager->mkSkolem("y", intType);
-    Node f = d_nodeManager->mkSkolem("f", fnType);
-    Node g = d_nodeManager->mkSkolem("g", fnType);
+    Node x = d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node y = d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node f = d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+    Node g = d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
     Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
     Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
     Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
@@ -644,7 +644,7 @@ public:
 //  This is for demonstrating what a certain type of user error looks like.
 //   Node level0(){
 //     NodeBuilder<> nb(kind::AND);
-//     Node x = d_nodeManager->mkSkolem(*d_booleanType);
+//     Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
 //     nb << x;
 //     nb << x;
 //     return Node(nb.constructNode());
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index fc9fdd2a6..97abddc00 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -246,9 +246,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkSkolem(*d_booleanType);
-    Node y = d_nm->mkSkolem(*d_booleanType);
-    Node z = d_nm->mkSkolem(*d_booleanType);
+    Node x = d_nm->mkSkolem("x", *d_booleanType);
+    Node y = d_nm->mkSkolem("z", *d_booleanType);
+    Node z = d_nm->mkSkolem("y", *d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -274,7 +274,7 @@ public:
     NodeBuilder<> noKind;
     TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
 
-    Node x( d_nm->mkSkolem( *d_integerType ) );
+    Node x( d_nm->mkSkolem( "x", *d_integerType ) );
     noKind << x << x;
     //     push_back(noKind, K);
     TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
@@ -297,7 +297,7 @@ public:
 
   void testGetNumChildren() {
     /* unsigned getNumChildren() const; */
-    Node x( d_nm->mkSkolem( *d_integerType ) );
+    Node x( d_nm->mkSkolem( "x", *d_integerType ) );
 
     NodeBuilder<> nb;
 #ifdef CVC4_ASSERTIONS
@@ -515,16 +515,16 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkSkolem(*d_booleanType);
-    Node y = d_nm->mkSkolem(*d_booleanType);
-    Node z = d_nm->mkSkolem(*d_booleanType);
+    Node x = d_nm->mkSkolem("x", *d_booleanType);
+    Node y = d_nm->mkSkolem("y", *d_booleanType);
+    Node z = d_nm->mkSkolem("z", *d_booleanType);
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
 
-    Node r = d_nm->mkSkolem(*d_realType);
-    Node s = d_nm->mkSkolem(*d_realType);
-    Node t = d_nm->mkSkolem(*d_realType);
+    Node r = d_nm->mkSkolem("r", *d_realType);
+    Node s = d_nm->mkSkolem("s", *d_realType);
+    Node t = d_nm->mkSkolem("t", *d_realType);
 
     Node p = d_nm->mkNode(EQUAL, d_nm->mkConst<Rational>(0),
                           d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t));
@@ -599,13 +599,13 @@ public:
   void testLeftistBuilding() {
     NodeBuilder<> nb;
 
-    Node a = d_nm->mkSkolem(*d_booleanType);
+    Node a = d_nm->mkSkolem("a", *d_booleanType);
 
-    Node b = d_nm->mkSkolem(*d_booleanType);
-    Node c = d_nm->mkSkolem(*d_booleanType);
+    Node b = d_nm->mkSkolem("b", *d_booleanType);
+    Node c = d_nm->mkSkolem("c", *d_booleanType);
 
-    Node d = d_nm->mkSkolem(*d_realType);
-    Node e = d_nm->mkSkolem(*d_realType);
+    Node d = d_nm->mkSkolem("d", *d_realType);
+    Node e = d_nm->mkSkolem("e", *d_realType);
 
     nb << a << NOT
        << b << c << OR
@@ -628,14 +628,14 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkSkolem(*d_booleanType);
+    Node a = d_nm->mkSkolem("a", *d_booleanType);
 
-    Node b = d_nm->mkSkolem(*d_booleanType);
-    Node c = d_nm->mkSkolem(*d_booleanType);
+    Node b = d_nm->mkSkolem("b", *d_booleanType);
+    Node c = d_nm->mkSkolem("c", *d_booleanType);
 
-    Node d = d_nm->mkSkolem(*d_realType);
-    Node e = d_nm->mkSkolem(*d_realType);
-    Node f = d_nm->mkSkolem(*d_realType);
+    Node d = d_nm->mkSkolem("d", *d_realType);
+    Node e = d_nm->mkSkolem("e", *d_realType);
+    Node f = d_nm->mkSkolem("f", *d_realType);
 
     Node m = a && b;
     TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index d392050f8..75c3618ff 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -144,17 +144,9 @@ public:
     }
   }
 
-  void testMkVarWithNoName() {
-    TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkSkolem(booleanType);
-    TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
-    TS_ASSERT_EQUALS(x.getNumChildren(),0u);
-    TS_ASSERT_EQUALS(x.getType(),booleanType);
-  }
-
   void testMkVarWithName() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkSkolem("x", booleanType);
+    Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
     TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
     TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
@@ -337,7 +329,7 @@ public:
   /* This test is only valid if assertions are enabled. */
   void testMkNodeTooFew() {
 #ifdef CVC4_ASSERTIONS
-    Node x = d_nodeManager->mkSkolem( d_nodeManager->booleanType() );
+    Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() );
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
 #endif
   }
@@ -349,7 +341,7 @@ public:
     const unsigned int max = metakind::getUpperBoundForKind(AND);
     TypeNode boolType = d_nodeManager->booleanType();
     for( unsigned int i = 0; i <= max; ++i ) {
-      vars.push_back( d_nodeManager->mkSkolem(boolType) );
+      vars.push_back( d_nodeManager->mkSkolem("i", boolType) );
     }
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
 #endif