From d8994e79a67778b99e03dbe5a9437c4eb75c6c06 Mon Sep 17 00:00:00 2001 From: Arjun Viswanathan Date: Fri, 6 Apr 2018 17:50:48 -0500 Subject: [PATCH] Add define rec fun to cvc parser (#1738) --- src/parser/cvc/Cvc.g | 86 +++++++++++++++++-- test/regress/Makefile.tests | 5 ++ test/regress/regress1/quantifiers/const.cvc | 4 + .../regress1/quantifiers/constfunc.cvc | 7 ++ .../regress1/quantifiers/mutualrec2.cvc | 14 +++ test/regress/regress1/quantifiers/recfact.cvc | 7 ++ .../regress2/quantifiers/mutualrec2.cvc | 14 +++ 7 files changed, 129 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress1/quantifiers/const.cvc create mode 100644 test/regress/regress1/quantifiers/constfunc.cvc create mode 100644 test/regress/regress1/quantifiers/mutualrec2.cvc create mode 100644 test/regress/regress1/quantifiers/recfact.cvc create mode 100644 test/regress/regress2/quantifiers/mutualrec2.cvc diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 47bee5740..a4333c81d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -81,7 +81,7 @@ tokens { ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER'; CONTINUE_TOK = 'CONTINUE'; RESTART_TOK = 'RESTART'; - + RECURSIVE_FUNCTION_TOK = 'REC-FUN'; /* operators */ AND_TOK = 'AND'; @@ -116,7 +116,7 @@ tokens { EXISTS_TOK = 'EXISTS'; PATTERN_TOK = 'PATTERN'; - LAMBDA = 'LAMBDA'; + LAMBDA_TOK = 'LAMBDA'; // Symbols @@ -707,6 +707,15 @@ mainCommand[std::unique_ptr* cmd] std::vector dts; Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; std::string s; + Expr func; + std::vector bvs; + std::vector funcs; + std::vector formulas; + std::vector> formals; + std::vector ids; + std::vector types; + bool idCommaFlag = true; + bool formCommaFlag = true; } /* our bread & butter */ : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f)); } @@ -880,6 +889,66 @@ mainCommand[std::unique_ptr* cmd] | CONTINUE_TOK { UNSUPPORTED("CONTINUE command"); } | RESTART_TOK formula[f] { UNSUPPORTED("RESTART command"); } + | RECURSIVE_FUNCTION_TOK (identifier[id,CHECK_NONE,SYM_VARIABLE] + { + if(idCommaFlag){ + idCommaFlag=false; + } + else{ + PARSER_STATE->parseError("Identifiers need to be comma separated"); + } + } + COLON type[t,CHECK_DECLARED] (COMMA { + idCommaFlag=true; + })? + { + func = PARSER_STATE->mkVar(id, t, ExprManager::VAR_FLAG_NONE, true); + ids.push_back(id); + types.push_back(t); + funcs.push_back(func); + })+ + EQUAL_TOK (formula[f] + { + if(formCommaFlag){ + formCommaFlag=false; + } + else{ + PARSER_STATE->parseError("Function definitions need to be comma separated"); + } + } + (COMMA{ + formCommaFlag=true; + })? + { + if( f.getKind()==kind::LAMBDA ){ + bvs.insert(bvs.end(), f[0].begin(), f[0].end()); + formals.push_back(bvs); + bvs.clear(); + f = f[1]; + formulas.push_back(f); + } + else { + formals.push_back(bvs); + formulas.push_back(f); + } + })+ + { + if(idCommaFlag){ + PARSER_STATE->parseError("Cannot end function list with comma"); + } + if(formCommaFlag){ + PARSER_STATE->parseError("Cannot end function definition list with comma"); + } + if(funcs.size()!=formulas.size()){ + PARSER_STATE->parseError("Number of functions doesn't match number of function definitions"); + } + for(unsigned int i = 0, size = funcs.size(); i < size; i++){ + if(!funcs[i].getType().isSubtypeOf(types[i])){ + PARSER_STATE->parseError("Type mismatch in definition"); + } + } + cmd->reset(new DefineFunctionRecCommand(funcs,formals,formulas)); + } | toplevelDeclaration[cmd] ; @@ -1074,6 +1143,10 @@ declareVariables[std::unique_ptr* cmd, CVC4::Type& t, } } else { // f is not null-- meaning this is a definition not a declaration + //Check if the formula f has the correct type, declared as t. + if(!f.getType().isSubtypeOf(t)){ + PARSER_STATE->parseError("Type mismatch in definition"); + } if(!topLevel) { // must be top-level; doesn't make sense to write something // like e.g. FORALL(x:INT = 4): [...] @@ -1434,16 +1507,13 @@ prefixFormula[CVC4::Expr& f] IN_TOK formula[f] { PARSER_STATE->popScope(); } /* lambda */ - | LAMBDA { PARSER_STATE->pushScope(); } LPAREN + | LAMBDA_TOK { PARSER_STATE->pushScope(); } LPAREN boundVarDeclsReturn[terms,types] RPAREN COLON formula[f] { PARSER_STATE->popScope(); Type t = EXPR_MANAGER->mkFunctionType(types, f.getType()); - std::string name = "lambda"; - Expr func = PARSER_STATE->mkAnonymousFunction(name, t, ExprManager::VAR_FLAG_DEFINED); - Command* cmd = new DefineFunctionCommand(name, func, terms, f); - PARSER_STATE->preemptCommand(cmd); - f = func; + Expr bvl = EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, terms ); + f = EXPR_MANAGER->mkExpr( kind::LAMBDA, bvl, f ); } ; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index de80368a4..c5b38dcd8 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1222,6 +1222,8 @@ REG1_TESTS = \ regress1/quantifiers/burns4.smt2 \ regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 \ regress1/quantifiers/cdt-0208-to.smt2 \ + regress1/quantifiers/const.cvc \ + regress1/quantifiers/constfunc.cvc \ regress1/quantifiers/ext-ex-deq-trigger.smt2 \ regress1/quantifiers/extract-nproc.smt2 \ regress1/quantifiers/florian-case-ax.smt2 \ @@ -1233,6 +1235,7 @@ REG1_TESTS = \ regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \ regress1/quantifiers/mix-coeff.smt2 \ regress1/quantifiers/model_6_1_bv.smt2 \ + regress1/quantifiers/mutualrec2.cvc \ regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \ regress1/quantifiers/opisavailable-12.smt2 \ regress1/quantifiers/parametric-lists.smt2 \ @@ -1257,6 +1260,7 @@ REG1_TESTS = \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ + regress1/quantifiers/recfact.cvc \ regress1/quantifiers/rew-to-0211-dd.smt2 \ regress1/quantifiers/ricart-agrawala6.smt2 \ regress1/quantifiers/set3.smt2 \ @@ -1535,6 +1539,7 @@ REG2_TESTS = \ regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \ regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 \ regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 \ + regress2/quantifiers/mutualrec2.cvc \ regress2/quantifiers/nunchaku2309663.nun.min.smt2 \ regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \ regress2/strings/cmu-dis-0707-3.smt2 \ diff --git a/test/regress/regress1/quantifiers/const.cvc b/test/regress/regress1/quantifiers/const.cvc new file mode 100644 index 000000000..41b13434a --- /dev/null +++ b/test/regress/regress1/quantifiers/const.cvc @@ -0,0 +1,4 @@ +% EXPECT: unsat +REC-FUN five : INT = 5; +ASSERT five = 6; +CHECKSAT; diff --git a/test/regress/regress1/quantifiers/constfunc.cvc b/test/regress/regress1/quantifiers/constfunc.cvc new file mode 100644 index 000000000..3b563cdad --- /dev/null +++ b/test/regress/regress1/quantifiers/constfunc.cvc @@ -0,0 +1,7 @@ +% EXPECT: unsat +OPTION "fmf-fun"; +REC-FUN f : INT -> INT = LAMBDA (x : INT) : 1; +x : INT; +ASSERT NOT (f(7) = x); +ASSERT f(8) = x; +CHECKSAT; diff --git a/test/regress/regress1/quantifiers/mutualrec2.cvc b/test/regress/regress1/quantifiers/mutualrec2.cvc new file mode 100644 index 000000000..66da896ae --- /dev/null +++ b/test/regress/regress1/quantifiers/mutualrec2.cvc @@ -0,0 +1,14 @@ +% EXPECT: unsat +OPTION "fmf-fun"; +REC-FUN iseven : (INT) -> INT, isodd : (INT) -> INT, fact : INT -> INT = +LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE (IF (isodd(x - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF, +LAMBDA (y : INT): IF (y = 0) THEN 0 ELSE (IF (iseven(y - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF, +LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE x * fact(x - 1) ENDIF; +a,b,x,y,z : INT; +ASSERT 1 = isodd(4); +ASSERT 0 = iseven(4); +ASSERT 0 = isodd(3); +ASSERT 1 = iseven(3); +ASSERT NOT (24 = fact(4)); +CHECKSAT; + diff --git a/test/regress/regress1/quantifiers/recfact.cvc b/test/regress/regress1/quantifiers/recfact.cvc new file mode 100644 index 000000000..b2ea3304f --- /dev/null +++ b/test/regress/regress1/quantifiers/recfact.cvc @@ -0,0 +1,7 @@ +% EXPECT: unsat +OPTION "fmf-fun"; +x : INT; +REC-FUN fact : (INT) -> INT = LAMBDA (x : INT) : IF (x > 0) THEN x * fact (x - 1) ELSE 1 ENDIF; +ASSERT fact(0) = 2; +ASSERT x = fact(3); +CHECKSAT; diff --git a/test/regress/regress2/quantifiers/mutualrec2.cvc b/test/regress/regress2/quantifiers/mutualrec2.cvc new file mode 100644 index 000000000..66da896ae --- /dev/null +++ b/test/regress/regress2/quantifiers/mutualrec2.cvc @@ -0,0 +1,14 @@ +% EXPECT: unsat +OPTION "fmf-fun"; +REC-FUN iseven : (INT) -> INT, isodd : (INT) -> INT, fact : INT -> INT = +LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE (IF (isodd(x - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF, +LAMBDA (y : INT): IF (y = 0) THEN 0 ELSE (IF (iseven(y - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF, +LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE x * fact(x - 1) ENDIF; +a,b,x,y,z : INT; +ASSERT 1 = isodd(4); +ASSERT 0 = iseven(4); +ASSERT 0 = isodd(3); +ASSERT 1 = iseven(3); +ASSERT NOT (24 = fact(4)); +CHECKSAT; + -- 2.30.2