Simplify internal represenation of uninterpreted sorts (#8660)

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
index 659c2baca911405296539571fded700aa73e82cc..07dd2c4e8f1b9b564d83cedbd45af1ac4f3879e3 100644 (file)
--- a/src/expr/node_converter.cpp
+++ b/src/expr/node_converter.cpp
@@ -196,11 +196,8 @@ TypeNode NodeConverter::convertType(TypeNode tn)
         // reconstruct using a node builder, which seems to be required for
         // type nodes.
         NodeBuilder nb(ret.getKind());
-        if (ret.getMetaKind() == kind::metakind::PARAMETERIZED)
-        {
-          // push the operator
-          nb << NodeManager::operatorFromType(ret);
-        }
+        // there are no parameterized types
+        Assert (ret.getMetaKind() != kind::metakind::PARAMETERIZED);
         for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
              j != iend;
              ++j)

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 7a367dcf01f1c2a3edbbf5924abcd3b256325034..2b1412c21873892935d50035b47d30c69f339167 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -869,16 +869,12 @@ TypeNode NodeManager::mkRecordType(const Record& rec)
 TypeNode NodeManager::mkSort()
 {
   NodeBuilder nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder(this, kind::SORT_TAG);
-  nb << sortTag;
   return nb.constructTypeNode();
 }
 
 TypeNode NodeManager::mkSort(const std::string& name)
 {
   NodeBuilder nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder(this, kind::SORT_TAG);
-  nb << sortTag;
   TypeNode tn = nb.constructTypeNode();
   setAttribute(tn, expr::VarNameAttr(), name);
   return tn;
@@ -907,8 +903,6 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, size_t arity)
 {
   Assert(arity > 0);
   NodeBuilder nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder(this, kind::SORT_TAG);
-  nb << sortTag;
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
   setAttribute(type, expr::SortArityAttr(), arity);

diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h
index 4e84b16fc36d3dd83952c4442597a943367c54e2..fc72be0092555b1b699d3dbfa5f89c29f3ec369e 100644 (file)
--- a/src/expr/node_manager_template.h
+++ b/src/expr/node_manager_template.h
@@ -81,18 +81,6 @@ class NodeManager
    */
   static bool isNAryKind(Kind k);
 
-  /**
-   * Returns a node representing the operator of this `TypeNode`.
-   * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) have an
-   * operator. "Little-p parameterized" types (like Array), are OPERATORs, not
-   * PARAMETERIZEDs.
-   */
-  static Node operatorFromType(const TypeNode& tn)
-  {
-    Assert(tn.getMetaKind() == kind::metakind::PARAMETERIZED);
-    return Node(tn.d_nv->getOperator());
-  }
-
   /** The node manager in the current public-facing cvc5 library context */
   static NodeManager* currentNM();
 

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 4175947ef52ede357cd19f4887c8eeecea14c3d4..fa4036d96fae7ee604e112f88046825d5f8d2b1d 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -255,8 +255,7 @@ sort BUILTIN_OPERATOR_TYPE \
     not-well-founded \
     "the type for built-in operators"
 
-variable SORT_TAG "sort tag"
-parameterized SORT_TYPE SORT_TAG 0 "specifies types of user-declared 'uninterpreted' sorts"
+variable SORT_TYPE "specifies types of user-declared 'uninterpreted' sorts"
 # The cardinality of uninterpreted sorts is defined infinite here, although they are given special treatment in TypeNode::getCardinalityClass
 cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
 well-founded SORT_TYPE \