diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 56fa93a94..93d596264 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -384,6 +384,7 @@ 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 { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } @@ -569,7 +570,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr f, f2; std::string attr; Expr attexpr; - std::vector<Expr> attexprs; + std::vector<Expr> patexprs; std::hash_set<std::string, StringHashFunction> names; std::vector< std::pair<std::string, Expr> > binders; } @@ -714,8 +715,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] ( attribute[expr, attexpr,attr] - { if(! attexpr.isNull()) { - attexprs.push_back(attexpr); + { if( attr == ":pattern" && ! attexpr.isNull()) { + patexprs.push_back( attexpr ); + }else if( attr==":axiom" ){ + //do this? } } )+ RPAREN_TOK @@ -745,10 +748,15 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] else PARSER_STATE->parseError("Error parsing rewrite rule."); expr = MK_EXPR( kind, args ); - } else if(! attexprs.empty()) { - if(attexprs[0].getKind() == kind::INST_PATTERN) { - expr2 = MK_EXPR(kind::INST_PATTERN_LIST, attexprs); + } else if(! patexprs.empty()) { + if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ + for( size_t i=0; i<f2.getNumChildren(); i++ ){ + patexprs.push_back( f2[i] ); + } } + expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs); + }else{ + expr2 = f2; } } /* constants */ |