diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 19:10:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-01 19:10:47 -0500 |
commit | 7b815181bfd58100478970f52b80461638fd42a8 (patch) | |
tree | 89d21d0ef97781eacb1a49c656db25d9946b031a /src/parser/parser.cpp | |
parent | 113e7001e03ec7d1c2b79e0bb2cc9b762519bc22 (diff) |
Fix issues with printing parametric datatypes in smt2 (#2213)
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 14 |
1 files changed, 9 insertions, 5 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); |