Simplify internal representation of instantiated sorts (#8620)

Previously, sort constructors were stored as underlying operator of the NodeValue of instantiated sorts. This made it very difficult to access what sort constructor was used to construct the uninterpreted sort. Moreover, this representation made it virtually impossible to have a clean implementation of the LFSC printer for instantiated uninterpreted sorts, which requires renaming sort constructors.

This introduces a new kind INSTANTIATED_SORT_TYPE, which acts as an uninterpreted sort. The sort constructor is stored as the first child in its AST, which is analogous to parametric datatypes. It furthermore restricts SORT_TYPE to 0 children.

This is work towards having correct LFSC proof output when the input contains instantiated uninterpreted sorts.

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index c56d1721475a04851d80dc7091fab583b3f12cd4..cda9f8a6324823c16fb2df9363903535b46d5c13 100644 (file)
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -643,15 +643,21 @@ TypeNode DTypeConstructor::doParametricSubstitution(
     children.push_back(
         doParametricSubstitution((*i), paramTypes, paramReplacements));
   }
-  for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
+  if (range.getKind() == INSTANTIATED_SORT_TYPE)
   {
-    if (paramTypes[i].getUninterpretedSortConstructorArity()
-        == origChildren.size())
+    // paramTypes contains a list of uninterpreted sort constructors.
+    // paramReplacements contains a list of instantiated parametric datatypes.
+    // If range is (INSTANTIATED_SORT_TYPE c T1 ... Tn), and
+    //    paramTypes[i] is c
+    //    paramReplacements[i] is (PARAMETRIC_DATATYPE d S1 ... Sn)
+    // then we return (PARAMETRIC_DATATYPE d T'1 ... T'n) where T'1 ...T'n
+    // is the result of recursively processing T1 ... Tn.
+    for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
     {
-      TypeNode tn = paramTypes[i].instantiate(origChildren);
-      if (range == tn)
+      if (paramTypes[i] == origChildren[0])
       {
-        TypeNode tret = paramReplacements[i].instantiate(children);
+        std::vector<TypeNode> params(children.begin() + 1, children.end());
+        TypeNode tret = paramReplacements[i].instantiate(params);
         return tret;
       }
     }

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 57b59dce96ae6f073dd74fb5c7983e5c631bb4e3..7a367dcf01f1c2a3edbbf5924abcd3b256325034 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -894,17 +894,13 @@ TypeNode NodeManager::mkSort(TypeNode constructor,
   Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr())
          && hasAttribute(constructor.d_nv, expr::VarNameAttr()))
       << "expected a sort constructor";
-  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
   Assert(getAttribute(constructor.d_nv, expr::SortArityAttr())
          == children.size())
       << "arity mismatch in application of sort constructor";
-  NodeBuilder nb(this, kind::SORT_TYPE);
-  Node sortTag = Node(constructor.d_nv->d_children[0]);
-  nb << sortTag;
+  NodeBuilder nb(this, kind::INSTANTIATED_SORT_TYPE);
+  nb << constructor;
   nb.append(children);
-  TypeNode type = nb.constructTypeNode();
-  setAttribute(type, expr::VarNameAttr(), name);
-  return type;
+  return nb.constructTypeNode();
 }
 
 TypeNode NodeManager::mkSortConstructor(const std::string& name, size_t arity)

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index d7b832c701599208f8a4bf63e3edb62c6add4f2a..59feac41f844fea1227602f45445c5199560c268 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -369,9 +369,7 @@ std::vector<TypeNode> TypeNode::getInstantiatedParamTypes() const
 {
   Assert(isInstantiated());
   vector<TypeNode> params;
-  for (uint32_t i = isInstantiatedDatatype() ? 1 : 0, i_end = getNumChildren();
-       i < i_end;
-       ++i)
+  for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i)
   {
     params.push_back((*this)[i]);
   }
@@ -428,7 +426,7 @@ bool TypeNode::isInstantiatedDatatype() const {
 
 bool TypeNode::isInstantiatedUninterpretedSort() const
 {
-  return isUninterpretedSort() && getNumChildren() > 0;
+  return getKind() == kind::INSTANTIATED_SORT_TYPE;
 }
 
 bool TypeNode::isInstantiated() const
@@ -439,7 +437,12 @@ bool TypeNode::isInstantiated() const
 TypeNode TypeNode::instantiate(const std::vector<TypeNode>& params) const
 {
   NodeManager* nm = NodeManager::currentNM();
-  if (getKind() == kind::PARAMETRIC_DATATYPE)
+  Kind k = getKind();
+  TypeNode ret;
+  // Note that parametric datatypes we instantiate have an AST where they are
+  // applied to their default parameters. In constrast, sort constructors have
+  // no children.
+  if (k == kind::PARAMETRIC_DATATYPE)
   {
     Assert(params.size() == getNumChildren() - 1);
     TypeNode cons =
@@ -450,10 +453,14 @@ TypeNode TypeNode::instantiate(const std::vector<TypeNode>& params) const
     {
       paramsNodes.push_back(t);
     }
-    return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
+    ret = nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
   }
-  Assert(isUninterpretedSortConstructor());
-  return nm->mkSort(*this, params);
+  else
+  {
+    Assert(isUninterpretedSortConstructor());
+    ret = nm->mkSort(*this, params);
+  }
+  return ret;
 }
 
 uint64_t TypeNode::getUninterpretedSortConstructorArity() const
@@ -476,10 +483,8 @@ std::string TypeNode::getName() const
 
 TypeNode TypeNode::getUninterpretedSortConstructor() const
 {
-  Assert(isInstantiatedUninterpretedSort());
-  NodeBuilder nb(kind::SORT_TYPE);
-  nb << NodeManager::operatorFromType(*this);
-  return nb.constructTypeNode();
+  Assert(getKind() == kind::INSTANTIATED_SORT_TYPE);
+  return (*this)[0];
 }
 
 bool TypeNode::isParameterInstantiatedDatatype(size_t n) const
@@ -509,7 +514,9 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
 /** Is this a sort kind */
 bool TypeNode::isUninterpretedSort() const
 {
-  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
+  Kind k = getKind();
+  return k == kind::INSTANTIATED_SORT_TYPE
+         || (k == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()));
 }
 
 /** Is this a sort constructor kind */

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 41fa39575d728b707ac82e20299c419683d11e09..5367c0e1959d8cf6e6baace04676551ccffe4c10 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -859,6 +859,7 @@ void Smt2Printer::toStream(std::ostream& out,
     }
   }
   break;
+  case kind::INSTANTIATED_SORT_TYPE: break;
   case kind::PARAMETRIC_DATATYPE: break;
 
   // separation logic

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index fafeb6e2f6abb59d80cd7cbb1925885d2df40264..4175947ef52ede357cd19f4887c8eeecea14c3d4 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -256,14 +256,23 @@ sort BUILTIN_OPERATOR_TYPE \
     "the type for built-in operators"
 
 variable SORT_TAG "sort tag"
-parameterized SORT_TYPE SORT_TAG 0: "specifies types of user-declared 'uninterpreted' sorts"
-# This is really "unknown" cardinality, but maybe this will be good
-# enough (for now) ?
+parameterized SORT_TYPE SORT_TAG 0 "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 \
     "::cvc5::internal::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
     "::cvc5::internal::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
+enumerator SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"
+
+# an instantiated sort has the same properties as an ordinary uninterpreted sort
+operator INSTANTIATED_SORT_TYPE 1: "instantiated uninterpreted sort"
+cardinality INSTANTIATED_SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
+well-founded INSTANTIATED_SORT_TYPE \
+    "::cvc5::internal::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
+    "::cvc5::internal::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
+enumerator INSTANTIATED_SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"
 
 constant UNINTERPRETED_SORT_VALUE \
     class \
@@ -272,7 +281,6 @@ constant UNINTERPRETED_SORT_VALUE \
     "util/uninterpreted_sort_value.h" \
     "the kind of expressions representing uninterpreted sort values; payload is an instance of the cvc5::internal::AbstractValue class (used in models)"
 typerule UNINTERPRETED_SORT_VALUE ::cvc5::internal::theory::builtin::UninterpretedSortValueTypeRule
-enumerator SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h"
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's

diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index 2593a46e5e40227afab9138dbe236b2fca5e5318..4464f630a07b7c9ae7093273d2fba53f8bb95d85 100644 (file)
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -26,7 +26,7 @@ UninterpretedSortEnumerator::UninterpretedSortEnumerator(
     TypeNode type, TypeEnumeratorProperties* tep)
     : TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0)
 {
-  Assert(type.getKind() == kind::SORT_TYPE);
+  Assert(type.isUninterpretedSort());
   d_has_fixed_bound = false;
   Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl;
   if (tep && tep->d_fixed_usort_card)

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index f4450a57d827b97c09b9b5be21597de7e70b0776..edf797da199353ee385226c6161235dba2f6b518 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -69,7 +69,8 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager,
     std::vector<TypeNode> instTypes;
     m.getMatches(instTypes);
     TypeNode range = t.instantiate(instTypes);
-    Trace("typecheck-idt") << "Return " << range << std::endl;
+    Trace("typecheck-idt") << "Return (constructor) " << range << " for " << n
+                           << std::endl;
     return range;
   }
   else
@@ -149,7 +150,8 @@ TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager,
     TypeNode range = selType[1];
     range = range.substitute(
         types.begin(), types.end(), matches.begin(), matches.end());
-    Trace("typecheck-idt") << "Return " << range << std::endl;
+    Trace("typecheck-idt") << "Return (selector) " << range << " for " << n
+                           << " from " << selType[1] << std::endl;
     return range;
   }
   else