diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-06 17:10:53 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-06 17:10:53 +0000 |
commit | 86eb2490a00466d5b014976fc89b813011b663eb (patch) | |
tree | 5a9cf7efb8ba9ad356a9a4a0021400c191cd30e7 /src/parser/smt2/Smt2.g | |
parent | 971681afb1c9518d232d5d234800ab5da209a222 (diff) |
Adding Array types to SMT2 parser
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 91f2f205b..c23ccca6b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -359,9 +359,21 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] sortSymbol[CVC4::Type& t] @declarations { std::string name; + std::vector<CVC4::Type> args; } : sortName[name,CHECK_NONE] { t = PARSER_STATE->getSort(name); } + | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK + { + if( name == "Array" ) { + if( args.size() != 2 ) { + PARSER_STATE->parseError("Illegal array type."); + } + t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); + } else { + PARSER_STATE->parseError("Unhandled parameterized type."); + } + } ; /** |