Fix issues with printing parametric datatypes in smt2 (#2213)

3 files changed, 15 insertions, 8 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1f9c3fd2b..47124a589 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -324,10 +324,13 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) {
 }
 
 SortConstructorType Parser::mkSortConstructor(const std::string& name,
-                                              size_t arity) {
+                                              size_t arity,
+                                              uint32_t flags)
+{
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
-  SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
+  SortConstructorType type =
+      d_exprManager->mkSortConstructor(name, arity, flags);
   defineType(name, vector<Type>(arity), type);
   return type;
 }
@@ -340,7 +343,8 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
 
 SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                                         size_t arity) {
-  SortConstructorType unresolved = mkSortConstructor(name, arity);
+  SortConstructorType unresolved =
+      mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
@@ -349,8 +353,8 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor(
     const std::string& name, const std::vector<Type>& params) {
   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
-  SortConstructorType unresolved =
-      d_exprManager->mkSortConstructor(name, params.size());
+  SortConstructorType unresolved = d_exprManager->mkSortConstructor(
+      name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
   defineType(name, params, unresolved);
   Type t = getSort(name, params);
   d_unresolved.insert(unresolved);
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 769f4c812..78cbcaafb 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -540,7 +540,10 @@ public:
   /**
    * Creates a new sort constructor with the given name and arity.
    */
-  SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
+  SortConstructorType mkSortConstructor(
+      const std::string& name,
+      size_t arity,
+      uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /**
    * Creates a new "unresolved type," used only during parsing.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b52be77bb..d3bec9d42 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1479,7 +1479,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
     PARSER_STATE->pushScope(true); }
   LPAREN_TOK /* parametric sorts */
   ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
-    { sorts.push_back( PARSER_STATE->mkSort(name) ); }
+    { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
   )*
   RPAREN_TOK
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
@@ -1550,7 +1550,7 @@ datatypesDef[bool isCo,
     }
     ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
       ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
-        { params.push_back( PARSER_STATE->mkSort(name) ); }
+        { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); }
       )*
       RPAREN_TOK {
         // if the arity was fixed by prelude and is not equal to the number of parameters