Enhancements to NodeManager tests, taking advantage of new Type implementation

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3a6b6e15a6484108c2e8dc2773cca1948ee16849..138a87493c351709bbd30d67ccc13292f2eb229e 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -473,6 +473,9 @@ public:
    */
   inline Type mkPredicateType(const std::vector<Type>& sorts);
 
+  /** Make a new sort. */
+  inline Type mkSort();
+
   /** Make a new sort with the given name. */
   inline Type mkSort(const std::string& name);
 
@@ -630,6 +633,10 @@ NodeManager::mkPredicateType(const std::vector<Type>& sorts) {
   return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
 }
 
+inline Type NodeManager::mkSort() {
+  return Type(this, mkVarPtr(kindType()));
+}
+
 inline Type NodeManager::mkSort(const std::string& name) {
   return Type(this, mkVarPtr(name, kindType()));
 }

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 873e28bb3e82eb135f848cf952d36b582bdad28f..118ba81733dc28954fb5a3889bd8c1037f4dbfae 100644 (file)
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -49,7 +49,7 @@ public:
     delete d_context;
   }
 
-  void testMkNode1() {
+  void testMkNodeNot() {
     Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(NOT, x);
     TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
@@ -57,7 +57,7 @@ public:
     TS_ASSERT_EQUALS( n[0], x);
   }
 
-  void testMkNode2() {
+  void testMkNodeBinary() {
     Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
     Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(IMPLIES, x, y);
@@ -67,7 +67,7 @@ public:
     TS_ASSERT_EQUALS( n[1], y);
   }
 
-  void testMkNode3() {
+  void testMkNodeThreeChildren() {
     Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
     Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
     Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
@@ -79,7 +79,7 @@ public:
     TS_ASSERT_EQUALS( n[2], z);
   }
 
-  void testMkNode4() {
+  void testMkNodeFourChildren() {
     Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
     Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
     Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -93,7 +93,7 @@ public:
     TS_ASSERT_EQUALS( n[3], x4 );
   }
 
-  void testMkNode5() {
+  void testMkNodeFiveChildren() {
     Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
     Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
     Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -109,7 +109,7 @@ public:
     TS_ASSERT_EQUALS( n[4], x5);
   }
 
-  void testMkNodeVecOfNode() {
+  void testMkNodeVectorOfNodeChildren() {
     Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
     Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
     Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -125,7 +125,7 @@ public:
     }
   }
 
-  void testMkNodeVecOfTNode() {
+  void testMkNodeVectorOfTNodeChildren() {
     Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
     Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
     Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
@@ -141,7 +141,7 @@ public:
     }
   }
 
-  void testMkVar1() {
+  void testMkVarWithNoName() {
     Type booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar(booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
@@ -149,7 +149,7 @@ public:
     TS_ASSERT_EQUALS(x.getType(),booleanType);
   }
 
-  void testMkVar2() {
+  void testMkVarWithName() {
     Type booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar("x", booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
@@ -187,76 +187,98 @@ public:
   }
 
   void testBooleanType() {
-    Type booleanType1 = d_nodeManager->booleanType();
-    Type booleanType2 = d_nodeManager->booleanType();
-    Type otherType = d_nodeManager->mkSort("T");
-    TS_ASSERT( booleanType1.isBoolean() );
-    TS_ASSERT_EQUALS(booleanType1, booleanType2);
-    TS_ASSERT( booleanType1 != otherType );
+    Type t = d_nodeManager->booleanType();
+    Type t2 = d_nodeManager->booleanType();
+    Type t3 = d_nodeManager->mkSort("T");
+    TS_ASSERT( t.isBoolean() );
+    TS_ASSERT( !t.isFunction() );
+    TS_ASSERT( !t.isKind() );
+    TS_ASSERT( !t.isNull() );
+    TS_ASSERT( !t.isPredicate() );
+    TS_ASSERT( !t.isSort() );
+    TS_ASSERT_EQUALS(t, t2);
+    TS_ASSERT( t != t3 );
+
+    BooleanType bt = t;
+    TS_ASSERT_EQUALS( bt, t);
   }
 
   void testKindType() {
-    Type kindType1 = d_nodeManager->kindType();
-    Type kindType2 = d_nodeManager->kindType();
-    Type otherType = d_nodeManager->mkSort("T");
-    TS_ASSERT( kindType1.isKind() );
-    TS_ASSERT_EQUALS(kindType1, kindType2);
-    TS_ASSERT( kindType1 != otherType );
-    // TODO: Is there a way to get the type of otherType (it should == kindType)
+    Type t = d_nodeManager->kindType();
+    Type t2 = d_nodeManager->kindType();
+    Type t3 = d_nodeManager->mkSort("T");
+
+    TS_ASSERT( !t.isBoolean() );
+    TS_ASSERT( !t.isFunction() );
+    TS_ASSERT( t.isKind() );
+    TS_ASSERT( !t.isNull() );
+    TS_ASSERT( !t.isPredicate() );
+    TS_ASSERT( !t.isSort() );
+
+    TS_ASSERT_EQUALS(t, t2);
+    TS_ASSERT( t != t3);
+
+    KindType kt = t;
+    TS_ASSERT_EQUALS( kt, t );
+    // TODO: Is there a way to get the type of otherType (it should == t)?
   }
 
-  /* TODO: All of the type comparisons in all of the following tests are
-   * strictly for pointer equality. This is too weak for disequalities and
-   * too strong for equalities! Also, it means we can't really check for
-   * structural equality between two identical calls to mkFunctionType (see
-   * the commented out assertions at the bottom of each test). Unfortunately,
-   * with the current type implementation it's the best we can do. */
-
-  void testMkFunctionType2() {
+  void testMkFunctionTypeBoolToBool() {
     Type booleanType = d_nodeManager->booleanType();
     Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
-    TS_ASSERT( t != booleanType );
+    Type t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
+
+    TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
+    TS_ASSERT( !t.isKind() );
+    TS_ASSERT( !t.isNull() );
+    TS_ASSERT( t.isPredicate() );
+    TS_ASSERT( !t.isSort() );
 
-    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS( t, t2 );
+
+    FunctionType ft = t;
+    TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
     TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 
-/*    Type *t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
-    TS_ASSERT_EQUALS( t, t2 );*/
   }
 
-  void testMkFunctionTypeVecType() {
-    Type a = d_nodeManager->mkSort("a");
-    Type b = d_nodeManager->mkSort("b");
-    Type c = d_nodeManager->mkSort("c");
+  void testMkFunctionTypeVectorOfArgsWithReturnType() {
+    Type a = d_nodeManager->mkSort();
+    Type b = d_nodeManager->mkSort();
+    Type c = d_nodeManager->mkSort();
 
     std::vector<Type> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
 
     Type t = d_nodeManager->mkFunctionType(argTypes,c);
+    Type t2 = d_nodeManager->mkFunctionType(argTypes,c);
 
-    TS_ASSERT( t != a );
-    TS_ASSERT( t != b );
-    TS_ASSERT( t != c );
+    TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
+    TS_ASSERT( !t.isKind() );
+    TS_ASSERT( !t.isNull() );
+    TS_ASSERT( !t.isPredicate() );
+    TS_ASSERT( !t.isSort() );
+
+    TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = (FunctionType)t;
+    FunctionType ft = t;
+    TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
     TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
     TS_ASSERT_EQUALS(ft.getRangeType(), c);
 
-/*    Type *t2 = d_nodeManager->mkFunctionType(argTypes,c);
-    TS_ASSERT_EQUALS( t, t2 );*/
   }
 
-  void testMkFunctionTypeVec() {
-    Type a = d_nodeManager->mkSort("a");
-    Type b = d_nodeManager->mkSort("b");
-    Type c = d_nodeManager->mkSort("c");
+  void testMkFunctionTypeVectorOfArguments() {
+    Type a = d_nodeManager->mkSort();
+    Type b = d_nodeManager->mkSort();
+    Type c = d_nodeManager->mkSort();
 
     std::vector<Type> types;
     types.push_back(a);
@@ -264,20 +286,23 @@ public:
     types.push_back(c);
 
     Type t = d_nodeManager->mkFunctionType(types);
+    Type t2 = d_nodeManager->mkFunctionType(types);
 
-    TS_ASSERT( t != a );
-    TS_ASSERT( t != b );
-    TS_ASSERT( t != c );
+    TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
+    TS_ASSERT( !t.isKind() );
+    TS_ASSERT( !t.isNull() );
+    TS_ASSERT( !t.isPredicate() );
+    TS_ASSERT( !t.isSort() );
 
-    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS( t, t2 );
+
+    FunctionType ft = t;
+    TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
     TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
     TS_ASSERT_EQUALS(ft.getRangeType(), c);
-
-/*    Type *t2 = d_nodeManager->mkFunctionType(types);
-    TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkPredicateType() {
@@ -292,21 +317,24 @@ public:
     argTypes.push_back(c);
 
     Type t = d_nodeManager->mkPredicateType(argTypes);
+    Type t2 = d_nodeManager->mkPredicateType(argTypes);
 
-    TS_ASSERT( t != a );
-    TS_ASSERT( t != b );
-    TS_ASSERT( t != c );
-    TS_ASSERT( t != booleanType );
+    TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
+    TS_ASSERT( !t.isKind() );
+    TS_ASSERT( !t.isNull() );
+    TS_ASSERT( t.isPredicate() );
+    TS_ASSERT( !t.isSort() );
+
+    TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = (FunctionType)t;
+    FunctionType ft = t;
+    TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
     TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
     TS_ASSERT_EQUALS(ft.getArgTypes()[2], c);
     TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 
-//    Type *t2 = d_nodeManager->mkPredicateType(argTypes);
-//    TS_ASSERT_EQUALS( t, t2 );
   }
 };