diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 54 |
1 files changed, 38 insertions, 16 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 436700826..dd261dcb6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -361,8 +361,12 @@ command [std::unique_ptr<CVC4::Command>* cmd] // we allow overloading for function definitions api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED, true); - cmd->reset(new DefineFunctionCommand( - name, func.getExpr(), api::termVectorToExprs(terms), expr.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + api::termVectorToExprs(terms), + expr.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] @@ -1204,7 +1208,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] expr = PARSER_STATE->mkHoApply( expr, flattenVars ); } cmd->reset(new DefineFunctionRecCommand( - func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr())); + func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr(), PARSER_STATE->getGlobalDeclarations())); } | DEFINE_FUNS_REC_TOK { PARSER_STATE->checkThatLogicIsSet();} @@ -1275,7 +1279,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] cmd->reset( new DefineFunctionRecCommand(api::termVectorToExprs(funcs), eformals, - api::termVectorToExprs(func_defs))); + api::termVectorToExprs(func_defs), PARSER_STATE->getGlobalDeclarations())); } ; @@ -1365,14 +1369,21 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { cmd->reset(seq.release()); } | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + ( // (define f t) + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } term[e,e2] - { api::Term func = PARSER_STATE->bindVar(name, e.getSort(), + { + api::Term func = PARSER_STATE->bindVar(name, e.getSort(), ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand(name, func.getExpr(), e.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + e.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } - | LPAREN_TOK + | // (define (f (v U) ...) t) + LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortedVarList[sortedVarNames] RPAREN_TOK @@ -1382,7 +1393,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[e,e2] - { PARSER_STATE->popScope(); + { + PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) @@ -1398,11 +1410,16 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] } api::Term func = PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand( - name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + api::termVectorToExprs(terms), + e.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } ) - | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + | // (define-const x U t) + DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] @@ -1412,14 +1429,19 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] terms = PARSER_STATE->bindBoundVars(sortedVarNames); } term[e, e2] - { PARSER_STATE->popScope(); + { + PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED); - cmd->reset(new DefineFunctionCommand( - name, func.getExpr(), api::termVectorToExprs(terms), e.getExpr())); + cmd->reset( + new DefineFunctionCommand(name, + func.getExpr(), + api::termVectorToExprs(terms), + e.getExpr(), + PARSER_STATE->getGlobalDeclarations())); } | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -2217,7 +2239,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] std::string name = sexpr.getValue(); // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand( - name, func.getExpr(), std::vector<Expr>(), expr.getExpr()); + name, func.getExpr(), std::vector<Expr>(), expr.getExpr(), PARSER_STATE->getGlobalDeclarations()); c->setMuted(true); PARSER_STATE->preemptCommand(c); } |