diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-06 20:57:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-06 20:57:44 -0600 |
commit | 691abe521ea8a7e87db51e22880cf101d59bf3e7 (patch) | |
tree | a3e7e336a64597a03b3142bd6cd39c7d42322bec /src/parser | |
parent | a97411d90188fc3ceda419faf7be4b3508e305a5 (diff) |
Add command for define-fun-rec and add to API (#1412)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 48 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 12 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 |
3 files changed, 9 insertions, 53 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5351bae15..1135d6dd4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1151,10 +1151,10 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] SExpr sexpr; Type t; Expr func; - Expr func_app; std::vector<Expr> bvs; std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList; std::vector<std::vector<Expr>> flattenVarsList; + std::vector<std::vector<Expr>> formals; std::vector<Expr> funcs; std::vector<Expr> func_defs; Expr aexpr; @@ -1198,41 +1198,24 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->resetAssertions(); } | DEFINE_FUN_REC_TOK - { PARSER_STATE->checkThatLogicIsSet(); - seq.reset(new CVC4::CommandSequence()); - } + { PARSER_STATE->checkThatLogicIsSet(); } symbol[fname,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(fname); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars); - seq->addCommand(new DeclareFunctionCommand(fname, func, t)); - PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, func_app, bvs, true ); + PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, bvs, true ); } term[expr, expr2] { PARSER_STATE->popScope(); if( !flattenVars.empty() ){ expr = PARSER_STATE->mkHoApply( expr, flattenVars ); } - Expr as = MK_EXPR( kind::EQUAL, func_app, expr); - if( !bvs.empty() ){ - std::string attr_name("fun-def"); - aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); - aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr); - //set the attribute to denote this is a function definition - seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); - //assert it - Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs); - as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, as, aexpr); - } - seq->addCommand( new AssertCommand(as, false) ); - cmd->reset(seq.release()); + cmd->reset(new DefineFunctionRecCommand(func,bvs,expr)); } | DEFINE_FUNS_REC_TOK - { PARSER_STATE->checkThatLogicIsSet(); - seq.reset(new CVC4::CommandSequence()); - } + { PARSER_STATE->checkThatLogicIsSet();} LPAREN_TOK ( LPAREN_TOK symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] @@ -1242,7 +1225,6 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] { flattenVars.clear(); func = PARSER_STATE->mkDefineFunRec( fname, sortedVarNames, t, flattenVars ); - seq->addCommand(new DeclareFunctionCommand(fname, func, t)); funcs.push_back( func ); // add to lists (need to remember for when parsing the bodies) @@ -1265,7 +1247,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] } bvs.clear(); PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0], - flattenVarsList[0], func_app, bvs, true); + flattenVarsList[0], bvs, true); } ( term[expr,expr2] @@ -1275,26 +1257,14 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] ); } func_defs.push_back( expr ); + formals.push_back(bvs); j++; - Expr as = MK_EXPR( kind::EQUAL, func_app, expr ); - if( !bvs.empty() ){ - std::string attr_name("fun-def"); - aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); - aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); - //set the attribute to denote these are function definitions - seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); - //assert it - as = EXPR_MANAGER->mkExpr( kind::FORALL, - EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), - as, aexpr); - } - seq->addCommand( new AssertCommand(as, false) ); //set up the next scope PARSER_STATE->popScope(); if( func_defs.size()<funcs.size() ){ bvs.clear(); PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j], - flattenVarsList[j], func_app, bvs, true); + flattenVarsList[j], bvs, true); } } )+ @@ -1304,7 +1274,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] "Number of functions defined does not match number listed in " "define-funs-rec")); } - cmd->reset(seq.release()); + cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs)); } // CHECK_SAT_ASSUMING still being discussed // GET_UNSAT_ASSUMPTIONS diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 032fdc673..381a60fa8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -373,7 +373,6 @@ void Smt2::pushDefineFunRecScope( const std::vector<std::pair<std::string, Type> >& sortedVarNames, Expr func, const std::vector<Expr>& flattenVars, - Expr& func_app, std::vector<Expr>& bvs, bool bindingLevel) { @@ -391,17 +390,6 @@ void Smt2::pushDefineFunRecScope( } bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end()); - - // make the function application - if (bvs.empty()) - { - // it has no arguments - func_app = func; - } - else - { - func_app = getExprManager()->mkExpr(kind::APPLY_UF, f_app); - } } void Smt2::reset() { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 835ff2b58..4832fc6b5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -127,13 +127,11 @@ public: * (1) Calls Parser::pushScope(bindingLevel). * (2) Computes the bound variable list for the quantified formula * that defined this definition and stores it in bvs. - * (3) Sets func_app to the APPLY_UF with func applied to bvs. */ void pushDefineFunRecScope( const std::vector<std::pair<std::string, Type> >& sortedVarNames, Expr func, const std::vector<Expr>& flattenVars, - Expr& func_app, std::vector<Expr>& bvs, bool bindingLevel = false); |