From: Andrew Reynolds Date: Thu, 8 Nov 2012 00:07:22 +0000 (+0000) Subject: added support for parametric datatypes in smt2 parser, includes support for 'as'... X-Git-Tag: cvc5-1.0.0~7644 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=182f242b6d7a9af3410d4930c98b177c26a8f58b;p=cvc5.git added support for parametric datatypes in smt2 parser, includes support for 'as' qualifier --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8db38037d..39149ec89 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -388,8 +388,12 @@ extendedCommand[CVC4::Command*& cmd] : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } { /* open a scope to keep the UnresolvedTypes contained */ PARSER_STATE->pushScope(); } - LPAREN_TOK RPAREN_TOK //TODO: parametric datatypes - LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK + LPAREN_TOK /* parametric sorts */ + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { + sorts.push_back( PARSER_STATE->mkSort(name) ); } + )* + RPAREN_TOK + LPAREN_TOK ( LPAREN_TOK datatypeDef[dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } | /* get model */ @@ -677,6 +681,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::vector patexprs; std::hash_set names; std::vector< std::pair > binders; + Type type; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -710,6 +715,22 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } + | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK + { + if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) { + std::vector v; + Expr e = f.getOperator(); + const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, + MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() )); + v.insert(v.end(), f.begin(), f.end()); + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); + } else { + if(f.getType() != type) { + PARSER_STATE->parseError("Type ascription not satisfied."); + } + } + } | LPAREN_TOK quantOp[kind] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK { @@ -1170,13 +1191,26 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } | 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."); + if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) { + if( name == "Array" ) { + if( args.size() != 2 ) { + PARSER_STATE->parseError("Illegal array type."); + } + t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); + } else { + t = PARSER_STATE->getSort(name, args); + } + }else{ + //make unresolved type + if(args.empty()) { + t = PARSER_STATE->mkUnresolvedType(name); + Debug("parser-param") << "param: make unres type " << name << std::endl; + }else{ + t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args); + t = SortConstructorType(t).instantiate( args ); + Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " " + << PARSER_STATE->getArity( name ) << std::endl; } - t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); - } else { - t = PARSER_STATE->getSort(name, args); } } ; @@ -1234,18 +1268,16 @@ nonemptyNumeralList[std::vector& numerals] /** * Parses a datatype definition */ -datatypeDef[std::vector& datatypes] +datatypeDef[std::vector& datatypes, std::vector< CVC4::Type >& params] @init { - std::string id, id2; - Type t; - std::vector< Type > params; + std::string id; } /* This really needs to be CHECK_NONE, or mutually-recursive * datatypes won't work, because this type will already be * "defined" as an unresolved type; don't worry, we check * below. */ : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } - ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] { + /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] { t = PARSER_STATE->mkSort(id2); params.push_back( t ); } @@ -1253,7 +1285,7 @@ datatypeDef[std::vector& datatypes] t = PARSER_STATE->mkSort(id2); params.push_back( t ); } )* ']' - )? + )?*/ //AJR: this isn't necessary if we use z3's style { datatypes.push_back(Datatype(id,params)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared @@ -1324,6 +1356,7 @@ SET_OPTION_TOK : 'set-option'; GET_OPTION_TOK : 'get-option'; PUSH_TOK : 'push'; POP_TOK : 'pop'; +AS_TOK : 'as'; // extended commands DECLARE_DATATYPES_TOK : 'declare-datatypes';