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 | |
parent | 113e7001e03ec7d1c2b79e0bb2cc9b762519bc22 (diff) |
Fix issues with printing parametric datatypes in smt2 (#2213)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 14 | ||||
-rw-r--r-- | src/parser/parser.h | 5 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
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 |