From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Apr 2022 15:45:45 +0000 (-0500)
Subject: Simplify internal represenation of uninterpreted sorts (#8660)
X-Git-Tag: cvc5-1.0.1~223
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b35b19bea0012d7b8d6d43ea634fddd4cd16afe5;p=cvc5.git

Simplify internal represenation of uninterpreted sorts (#8660)
---

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
index 659c2baca..07dd2c4e8 100644
--- 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 7a367dcf0..2b1412c21 100644
--- 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 4e84b16fc..fc72be009 100644
--- 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 4175947ef..fa4036d96 100644
--- 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 \