Fix parametric datatype instantiation (#4493)

A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.

5 files changed, 38 insertions, 1 deletions

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 428097d54..8923667b1 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -480,6 +480,7 @@ bool DTypeConstructor::resolve(
   NodeManager* nm = NodeManager::currentNM();
   size_t index = 0;
   std::vector<TypeNode> argTypes;
+  Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
   for (std::shared_ptr<DTypeSelector> arg : d_args)
   {
     std::string argName = arg->d_name;
@@ -488,9 +489,12 @@ bool DTypeConstructor::resolve(
     {
       // the unresolved type wasn't created here; do name resolution
       std::string typeName = argName.substr(argName.find('\0') + 1);
+      Trace("datatypes-init")
+          << "  - selector, typeName is " << typeName << std::endl;
       argName.resize(argName.find('\0'));
       if (typeName == "")
       {
+        Trace("datatypes-init") << "  ...self selector" << std::endl;
         range = self;
         arg->d_selector = nm->mkSkolem(
             argName,
@@ -504,11 +508,14 @@ bool DTypeConstructor::resolve(
             resolutions.find(typeName);
         if (j == resolutions.end())
         {
+          Trace("datatypes-init")
+              << "  ...failed to resolve selector" << std::endl;
           // failed to resolve selector
           return false;
         }
         else
         {
+          Trace("datatypes-init") << "  ...resolved selector" << std::endl;
           range = (*j).second;
           arg->d_selector = nm->mkSkolem(
               argName,
@@ -523,6 +530,8 @@ bool DTypeConstructor::resolve(
       // the type for the selector already exists; may need
       // complex-type substitution
       range = arg->d_selector.getType();
+      Trace("datatypes-init")
+          << "  - null selector, range = " << range << std::endl;
       if (!placeholders.empty())
       {
         range = range.substitute(placeholders.begin(),
@@ -530,10 +539,14 @@ bool DTypeConstructor::resolve(
                                  replacements.begin(),
                                  replacements.end());
       }
+      Trace("datatypes-init")
+          << "  ...range after placeholder replacement " << range << std::endl;
       if (!paramTypes.empty())
       {
         range = doParametricSubstitution(range, paramTypes, paramReplacements);
       }
+      Trace("datatypes-init")
+          << "  ...range after parametric substitution " << range << std::endl;
       arg->d_selector = nm->mkSkolem(
           argName,
           nm->mkSelectorType(self, range),
@@ -597,7 +610,7 @@ TypeNode DTypeConstructor::doParametricSubstitution(
   }
   for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
   {
-    if (paramTypes[i].getNumChildren() + 1 == origChildren.size())
+    if (paramTypes[i].getSortConstructorArity() == origChildren.size())
     {
       TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren);
       if (range == tn)
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index e6c695dd6..110db6162 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -459,9 +459,16 @@ TypeNode TypeNode::instantiateParametricDatatype(
   return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
 }
 
+uint64_t TypeNode::getSortConstructorArity() const
+{
+  Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr()));
+  return getAttribute(expr::SortArityAttr());
+}
+
 TypeNode TypeNode::instantiateSortConstructor(
     const std::vector<TypeNode>& params) const
 {
+  Assert(isSortConstructor());
   return NodeManager::currentNM()->mkSort(*this, params);
 }
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 6de4a0271..70392fb01 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -674,6 +674,9 @@ public:
   /** Is this a sort constructor kind */
   bool isSortConstructor() const;
 
+  /** Get sort constructor arity */
+  uint64_t getSortConstructorArity() const;
+
   /**
    * Instantiate a sort constructor type. The type on which this method is
    * called should be a sort constructor type whose parameter list is the
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6f948b02b..d5174af5e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -416,6 +416,7 @@ set(regress_0_tests
   regress0/datatypes/mutually-recursive.cvc
   regress0/datatypes/pair-bool-bool.cvc
   regress0/datatypes/pair-real-bool.smt2
+  regress0/datatypes/parametric-alt-list.cvc
   regress0/datatypes/rec1.cvc
   regress0/datatypes/rec2.cvc
   regress0/datatypes/rec4.cvc
diff --git a/test/regress/regress0/datatypes/parametric-alt-list.cvc b/test/regress/regress0/datatypes/parametric-alt-list.cvc
new file mode 100644
index 000000000..f523272ae
--- /dev/null
+++ b/test/regress/regress0/datatypes/parametric-alt-list.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+DATATYPE
+List[X,Y] = nil | cons (head: X, tail: List[Y,X])
+END;
+
+x : List[INT,STRING]; % = cons(1, nil::List[STRING,INT]);
+y : List[INT,STRING];
+
+ASSERT NOT( x = y );
+
+ASSERT NOT ( x = tail(tail(x)) );
+
+CHECKSAT;