Use TypeNode in UninterpretedConstant (#4748)

This commit changes UninterpretedConstant to use TypeNode instead of
Type.

2 files changed, 6 insertions, 10 deletions

diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 67a36200f..0a97f4c42 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -86,13 +86,11 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
   void testSetOfUF()
   {
-    TypeNode typeNode = d_nm->mkSort("Atom");
-    Type sort = typeNode.toType();
-    SetEnumerator setEnumerator(d_nm->mkSetType(typeNode));
+    TypeNode sort = d_nm->mkSort("Atom");
+    SetEnumerator setEnumerator(d_nm->mkSetType(sort));
 
     Node actual0 = *setEnumerator;
-    Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode)));
+    Node expected0 = d_nm->mkConst(EmptySet(d_nm->mkSetType(sort)));
     TS_ASSERT_EQUALS(expected0, actual0);
     TS_ASSERT(!setEnumerator.isFinished());
 
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index b996919ee..cf1f002aa 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -70,11 +70,9 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
   }
 
   void testUF() {
-    TypeNode sortn = d_nm->mkSort("T");
-    Type sort = sortn.toType();
-    TypeNode sortn2 = d_nm->mkSort("U");
-    Type sort2 = sortn2.toType();
-    TypeEnumerator te(sortn);
+    TypeNode sort = d_nm->mkSort("T");
+    TypeNode sort2 = d_nm->mkSort("U");
+    TypeEnumerator te(sort);
     TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0)));
     for(size_t i = 1; i < 100; ++i) {
       TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i)));