diff options
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 42 |
1 files changed, 24 insertions, 18 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d8157acbc..867250c0f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -705,8 +705,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] ( attribute[expr, attexpr,attr] { if( attr == ":pattern" && ! attexpr.isNull()) { patexprs.push_back( attexpr ); - }else if( attr==":axiom" ){ - //do this? } } )+ RPAREN_TOK @@ -788,18 +786,15 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] Expr e2; } : KEYWORD - { attr = AntlrInput::tokenText($KEYWORD); } - symbolicExpr[sexpr] - { if(attr == ":named") { - std::string name = sexpr.getValue(); - // FIXME ensure expr is a closed subterm - // check that sexpr is a fresh function symbol - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - // define it - Expr func = PARSER_STATE->mkFunction(name, expr.getType()); - // bind name to expr with define-fun - Command* c = - new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); + { + attr = AntlrInput::tokenText($KEYWORD); + //EXPR_MANAGER->setNamedAttribute( expr, attr ); + if( attr==":rewrite-rule" ){ + //do nothing + } else if( attr==":axiom" || attr==":conjecture" ){ + std::string attr_name = attr; + attr_name.erase( attr_name.begin() ); + Command* c = new SetUserAttributeCommand( attr_name, expr ); PARSER_STATE->preemptCommand(c); } else { std::stringstream ss; @@ -812,9 +807,20 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] attr = std::string(":pattern"); retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); } - | ATTRIBUTE_REWRITE_RULE { - attr = std::string(":rewrite-rule"); - } + | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] + { + attr = std::string(":named"); + std::string name = sexpr.getValue(); + // FIXME ensure expr is a closed subterm + // check that sexpr is a fresh function symbol + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + // define it + Expr func = PARSER_STATE->mkFunction(name, expr.getType()); + // bind name to expr with define-fun + Command* c = + new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); + PARSER_STATE->preemptCommand(c); + } ; /** @@ -1198,7 +1204,7 @@ PROPAGATION_RULE_TOK : 'assert-propagation'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; -ATTRIBUTE_REWRITE_RULE : ':rewrite-rule'; +ATTRIBUTE_NAMED_TOK : ':named'; // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; |