diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 12 | ||||
| -rw-r--r-- | test/regress/regress0/arr1.smt2 | 10 |
2 files changed, 22 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."); + } + } ; /** diff --git a/test/regress/regress0/arr1.smt2 b/test/regress/regress0/arr1.smt2 new file mode 100644 index 000000000..844f7d8e5 --- /dev/null +++ b/test/regress/regress0/arr1.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_AX) +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun a () (Array Index Element)) +(declare-fun i1 () Index) +(declare-fun i2 () Index) +(assert (not (=> (= i1 i2) (= (select a i1) (select a i2))))) +(check-sat) + |