From 6bac5cef88d22a2593d5da40dbb5cd45f63a266a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 15 Mar 2017 13:11:08 -0500 Subject: [PATCH] Allow 0 argument recursive functions. Fixes bug 782. --- src/parser/smt2/Smt2.g | 130 +++++++++++++++----------- test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/bug782.smt2 | 24 +++++ 3 files changed, 99 insertions(+), 58 deletions(-) create mode 100644 test/regress/regress0/fmf/bug782.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 92becbc68..07ace295c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1197,33 +1197,39 @@ smt25Command[CVC4::PtrCloser* cmd] ++i) { sorts.push_back((*i).second); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + t = EXPR_MANAGER->mkFunctionType(sorts, t); } Expr func = PARSER_STATE->mkVar(fname, t); seq->addCommand(new DeclareFunctionCommand(fname, func, t)); - std::vector< Expr > f_app; - f_app.push_back( func ); - PARSER_STATE->pushScope(true); - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; - ++i) { - Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); - bvs.push_back( v ); - f_app.push_back( v ); + if( sortedVarNames.empty() ){ + func_app = func; + }else{ + std::vector< Expr > f_app; + f_app.push_back( func ); + PARSER_STATE->pushScope(true); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; + ++i) { + Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); + bvs.push_back( v ); + f_app.push_back( v ); + } + func_app = MK_EXPR( kind::APPLY_UF, f_app ); } - func_app = MK_EXPR( kind::APPLY_UF, f_app ); } term[expr, expr2] { PARSER_STATE->popScope(); - 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 equality = MK_EXPR( kind::EQUAL, func_app, expr); - Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs); - Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, equality, aexpr); + 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()); } @@ -1239,13 +1245,15 @@ smt25Command[CVC4::PtrCloser* cmd] sortSymbol[t,CHECK_DECLARED] { sortedVarNamesList.push_back( sortedVarNames ); if( sortedVarNamesList[0].size() > 0 ) { - std::vector sorts; - for(std::vector >::const_iterator - i = sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; ++i) { - sorts.push_back((*i).second); + if( !sortedVarNames.empty() ){ + std::vector sorts; + for(std::vector >::const_iterator + i = sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; ++i) { + sorts.push_back((*i).second); + } + t = EXPR_MANAGER->mkFunctionType(sorts, t); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); } sortedVarNames.clear(); Expr func = PARSER_STATE->mkVar(fname, t); @@ -1262,52 +1270,60 @@ smt25Command[CVC4::PtrCloser* cmd] PARSER_STATE->parseError("Must define at least one function in " "define-funs-rec"); } - std::vector< Expr > f_app; - f_app.push_back( funcs[0] ); PARSER_STATE->pushScope(true); bvs.clear(); - for(std::vector >::const_iterator - i = sortedVarNamesList[0].begin(), - iend = sortedVarNamesList[0].end(); i != iend; ++i) { - Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); - bvs.push_back( v ); - f_app.push_back( v ); + if( sortedVarNamesList[0].empty() ){ + func_app = funcs[0]; + }else{ + std::vector< Expr > f_app; + f_app.push_back( funcs[0] ); + for(std::vector >::const_iterator + i = sortedVarNamesList[0].begin(), + iend = sortedVarNamesList[0].end(); i != iend; ++i) { + Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); + bvs.push_back( v ); + f_app.push_back( v ); + } + func_app = MK_EXPR( kind::APPLY_UF, f_app ); } - func_app = MK_EXPR( kind::APPLY_UF, f_app ); } ( term[expr,expr2] { func_defs.push_back( expr ); - - 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 - Expr as = EXPR_MANAGER->mkExpr( - kind::FORALL, - EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), - MK_EXPR( kind::EQUAL, func_app, expr ), - aexpr); + 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() f_app; - f_app.push_back( funcs[j] ); PARSER_STATE->pushScope(true); bvs.clear(); - for(std::vector >::const_iterator - i = sortedVarNamesList[j].begin(), - iend = sortedVarNamesList[j].end(); i != iend; ++i) { - Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); - bvs.push_back( v ); - f_app.push_back( v ); + unsigned j = func_defs.size(); + if( sortedVarNamesList[j].empty() ){ + func_app = funcs[j]; + }else{ + std::vector< Expr > f_app; + f_app.push_back( funcs[j] ); + for(std::vector >::const_iterator + i = sortedVarNamesList[j].begin(), + iend = sortedVarNamesList[j].end(); i != iend; ++i) { + Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); + bvs.push_back( v ); + f_app.push_back( v ); + } + func_app = MK_EXPR( kind::APPLY_UF, f_app ); } - func_app = MK_EXPR( kind::APPLY_UF, f_app ); } } )+ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 79cff2947..ec5255db7 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -67,7 +67,8 @@ TESTS = \ ko-bound-set.cvc \ cons-sets-bounds.smt2 \ bug651.smt2 \ - bug652.smt2 + bug652.smt2 \ + bug782.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug782.smt2 b/test/regress/regress0/fmf/bug782.smt2 new file mode 100644 index 000000000..603c783d3 --- /dev/null +++ b/test/regress/regress0/fmf/bug782.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(define-fun $$Bool.isTrue$$ ((b Bool)) Bool b) +(define-fun $$Bool.isFalse$$ ((b Bool)) Bool (not b)) + +(define-funs-rec + ( + (f123454321$multipleArgsFunction((x$$645421 Bool) (y$$645422 Bool)) Bool) + (f12345678$myConst() Int) + ) + ( + (= x$$645421 y$$645422) + 3 + ) +) + +(declare-fun i1000$$1000() Bool) +(declare-fun i1001$$1001() Bool) +(declare-fun i1002$$1002() Int) +(assert (f123454321$multipleArgsFunction i1000$$1000 i1001$$1001)) +(assert (= i1002$$1002 f12345678$myConst)) +(check-sat) -- 2.30.2