Initial support for parametric datatypes in sygus (#6304)

Fixes #6298.

Enables parsing of par in the sygus parser, and adds support for default grammar construction.

Also fixes a bug related to single invocation for non-function types.

1 files changed, 7 insertions, 2 deletions

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 927c48dda..c358aa2e8 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -120,15 +120,20 @@ TypeNode DTypeConstructor::getSpecializedConstructorType(
       << "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
          "got "
       << returnType;
+  TypeNode ctn = d_constructor.getType();
   const DType& dt = DType::datatypeOf(d_constructor);
-  Assert(dt.isParametric());
+  if (!dt.isParametric())
+  {
+    // if the datatype is not parametric, then no specialization is needed
+    return ctn;
+  }
   TypeNode dtt = dt.getTypeNode();
   TypeMatcher m(dtt);
   m.doMatching(dtt, returnType);
   std::vector<TypeNode> subst;
   m.getMatches(subst);
   std::vector<TypeNode> params = dt.getParameters();
-  return d_constructor.getType().substitute(
+  return ctn.substitute(
       params.begin(), params.end(), subst.begin(), subst.end());
 }