From 4247dc59f1219695750a33db776ae02b244cee7f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 23 Mar 2015 17:54:55 +0100 Subject: [PATCH] Parsing support for define-fun-rec/define-funs-rec. --- src/parser/smt2/Smt2.g | 136 +++++++++++++++--- test/regress/regress0/quantifiers/Makefile.am | 5 +- .../regress0/quantifiers/is-even-pred.smt2 | 7 + .../regress/regress0/quantifiers/is-even.smt2 | 7 + .../regress0/quantifiers/simp-len.smt2 | 9 ++ 5 files changed, 147 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress0/quantifiers/is-even-pred.smt2 create mode 100644 test/regress/regress0/quantifiers/is-even.smt2 create mode 100644 test/regress/regress0/quantifiers/simp-len.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 576767c78..eac16372a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -829,10 +829,17 @@ setOptionInternal[CVC4::Command*& cmd] smt25Command[CVC4::Command*& cmd] @declarations { std::string name; + std::string fname; Expr expr, expr2; std::vector > sortedVarNames; SExpr sexpr; Type t; + Expr func_app; + std::vector bvs; + std::vector< std::vector > > sortedVarNamesList; + std::vector funcs; + std::vector func_defs; + Expr aexpr; } /* meta-info */ : META_INFO_TOK metaInfoInternal[cmd] @@ -871,17 +878,14 @@ smt25Command[CVC4::Command*& cmd] { cmd = new ResetAssertionsCommand(); PARSER_STATE->resetAssertions(); } - - | /* recursive function definition */ - DEFINE_FUN_REC_TOK { PARSER_STATE->checkThatLogicIsSet(); } LPAREN_TOK - { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } + | DEFINE_FUN_REC_TOK { + PARSER_STATE->checkThatLogicIsSet(); + cmd = new CommandSequence();} + symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(fname); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - sortSymbol[t,CHECK_DECLARED] - { /* add variables to parser state before parsing term */ - Debug("parser") << "define fun rec: '" << name << "'" << std::endl; - if( sortedVarNames.size() > 0 ) { + sortSymbol[t,CHECK_DECLARED] { + if( sortedVarNames.size() > 0 ) { std::vector sorts; sorts.reserve(sortedVarNames.size()); for(std::vector >::const_iterator i = @@ -892,19 +896,118 @@ smt25Command[CVC4::Command*& cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED); + 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) { - PARSER_STATE->mkBoundVar((*i).first, (*i).second); + 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 ); } term[expr, expr2] - { PARSER_STATE->popScope(); } - RPAREN_TOK )+ RPAREN_TOK - { PARSER_STATE->popScope(); } + { PARSER_STATE->popScope(); + std::string attr_name("fun-def"); + Type t = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, t); + aexpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); + aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); + //set the attribute to denote this is a function definition + static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) ); + //assert it + Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr); + static_cast($cmd)->addCommand( new AssertCommand(as, false) ); + } + | DEFINE_FUNS_REC_TOK { + PARSER_STATE->checkThatLogicIsSet(); + cmd = new CommandSequence();} + LPAREN_TOK + ( LPAREN_TOK + symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(fname); } + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + 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); + } + t = EXPR_MANAGER->mkFunctionType(sorts, t); + } + sortedVarNames.clear(); + Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED); + funcs.push_back( func ); + } + RPAREN_TOK + )+ + RPAREN_TOK + LPAREN_TOK + { + std::string attr_name("fun-def"); + Type t = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, t); + aexpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); + aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); + //set the attribute to denote these are function definitions + static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) ); + + //set up the first scope + if( sortedVarNamesList.empty() ){ + PARSER_STATE->parseError(std::string("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 ); + } + func_app = MK_EXPR( kind::APPLY_UF, f_app ); + } + ( + term[expr,expr2] + { + func_defs.push_back( expr ); + //assert it + Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr); + static_cast($cmd)->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 ); + } + func_app = MK_EXPR( kind::APPLY_UF, f_app ); + } + } + )+ + RPAREN_TOK + { + if( funcs.size()!=func_defs.size() ){ + PARSER_STATE->parseError(std::string("Number of functions defined does not match number listed in define-funs-rec")); + } + } + // CHECK_SAT_ASSUMING still being discussed // GET_UNSAT_ASSUMPTIONS @@ -1225,7 +1328,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] // } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } - | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) + | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } | builtinOp[k] { std::stringstream ss; @@ -2322,6 +2425,7 @@ DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; DEFINE_FUN_REC_TOK : 'define-fun-rec'; +DEFINE_FUNS_REC_TOK : 'define-funs-rec'; DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; GET_ASSIGNMENT_TOK : 'get-assignment'; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f8cc9ea35..ff3607b5b 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -45,7 +45,10 @@ TESTS = \ bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ - stream-x2014-09-18-unsat.smt2 + stream-x2014-09-18-unsat.smt2 \ + simp-len.smt2 \ + is-even.smt2 \ + is-even-pred.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/is-even-pred.smt2 b/test/regress/regress0/quantifiers/is-even-pred.smt2 new file mode 100644 index 000000000..9808f4936 --- /dev/null +++ b/test/regress/regress0/quantifiers/is-even-pred.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(define-funs-rec ((is-even ((x Int)) Bool) (is-odd ((x Int)) Bool)) ((or (= x 0) (is-odd (- x 1))) (and (not (= x 0)) (is-even (- x 1))))) + +(assert (is-even 5)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/is-even.smt2 b/test/regress/regress0/quantifiers/is-even.smt2 new file mode 100644 index 000000000..9aaac5e09 --- /dev/null +++ b/test/regress/regress0/quantifiers/is-even.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(define-funs-rec ((is-even ((x Int)) Int) (is-odd ((y Int)) Int)) ((ite (= x 0) 1 (ite (= (is-odd (- x 1)) 0) 1 0)) (ite (= y 0) 0 (ite (= (is-even (- y 1)) 0) 1 0)))) + +(assert (= (is-even 4) 0)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2 new file mode 100644 index 000000000..d213e3426 --- /dev/null +++ b/test/regress/regress0/quantifiers/simp-len.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) + +(define-fun-rec len ((x Lst)) Int (ite (is-cons x) (+ 1 (len (tail x))) 0)) + +(assert (= (len (cons 0 nil)) 0)) +(check-sat) \ No newline at end of file -- 2.30.2