diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:50:10 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:50:15 -0400 |
commit | bd05758bc141f0b922916b63089e7e8748f8da31 (patch) | |
tree | 0702eda96a43b70538b0e87a26c19c7c25597db9 | |
parent | 3a29fafdb098d82ba56cdc02af7f1b0981a74d02 (diff) |
SMT-LIB parser support for array constants (Z3 syntax).
-rw-r--r-- | src/parser/smt2/Smt2.g | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 61b898806..4491e5643 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -999,11 +999,25 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } expr = MK_EXPR(kind, args); } - | /* An indexed function application */ - LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK - { expr = MK_EXPR(op, args); - PARSER_STATE->checkOperator(expr.getKind(), args.size()); - } + | LPAREN_TOK + ( /* An indexed function application */ + indexedFunctionName[op] termList[args,expr] RPAREN_TOK + { expr = MK_EXPR(op, args); + PARSER_STATE->checkOperator(expr.getKind(), args.size()); + } + | /* Array constant (in Z3 syntax) */ + LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED] + RPAREN_TOK term[f, f2] RPAREN_TOK + { + if(!type.isArray()) { + PARSER_STATE->parseError("(as const...) type ascription can only be used for array sorts."); + } + if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) { + PARSER_STATE->parseError("type of the array cast is not compatible with term."); + } + expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) ); + } + ) | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(true); } @@ -1710,6 +1724,7 @@ GET_OPTION_TOK : 'get-option'; PUSH_TOK : 'push'; POP_TOK : 'pop'; AS_TOK : 'as'; +CONST_TOK : 'const'; // extended commands DECLARE_DATATYPES_TOK : 'declare-datatypes'; |