diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6a98755f2..e7d614b85 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -344,28 +344,6 @@ command returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } - | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } - sortSymbol[t,CHECK_DECLARED] - { /* add variables to parser state before parsing term */ - Debug("parser") << "define const: '" << name << "'" << std::endl; - PARSER_STATE->pushScope(true); - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; - ++i) { - terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); - } - } - term[expr, expr2] - { PARSER_STATE->popScope(); - // declare the name down here (while parsing term, signature - // must not be extended with the name itself; no recursion - // permitted) - Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); - $cmd = new DefineFunctionCommand(name, func, terms, expr); - } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -624,6 +602,28 @@ extendedCommand[CVC4::Command*& cmd] $cmd = new DefineFunctionCommand(name, func, terms, e); } ) + | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define const: '" << name << "'" << std::endl; + PARSER_STATE->pushScope(true); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); + } + } + term[e, e2] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); + $cmd = new DefineFunctionCommand(name, func, terms, e); + } | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] |