diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-23 20:07:19 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-23 20:07:19 -0600 |
commit | 612509379a1417f8d4a5e001ff143ba819f5516f (patch) | |
tree | 764c379a42fa29ec36d9c83d448901c975e2fa29 /src/parser | |
parent | c9ae6b9812e737ae7932df91fa5f334d6d2588d4 (diff) |
Ho parsing and regressions (#1350)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 52 | ||||
-rw-r--r-- | src/parser/parser.h | 65 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 180 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 55 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 46 |
5 files changed, 314 insertions, 84 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c8b4ac966..0d8cc1fcb 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -448,6 +448,58 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes( } } +Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, + Type range, + std::vector<Expr>& flattenVars) +{ + if (range.isFunction()) + { + std::vector<Type> domainTypes = + (static_cast<FunctionType>(range)).getArgTypes(); + for (unsigned i = 0, size = domainTypes.size(); i < size; i++) + { + sorts.push_back(domainTypes[i]); + // the introduced variable is internal (not parsable) + std::stringstream ss; + ss << "__flatten_var_" << i; + Expr v = d_exprManager->mkBoundVar(ss.str(), domainTypes[i]); + flattenVars.push_back(v); + } + range = static_cast<FunctionType>(range).getRangeType(); + } + if (sorts.empty()) + { + return range; + } + return d_exprManager->mkFunctionType(sorts, range); +} + +Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range) +{ + if (sorts.empty()) + { + // no difference + return range; + } + while (range.isFunction()) + { + std::vector<Type> domainTypes = + static_cast<FunctionType>(range).getArgTypes(); + sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end()); + range = static_cast<FunctionType>(range).getRangeType(); + } + return d_exprManager->mkFunctionType(sorts, range); +} + +Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex) +{ + for (unsigned i = startIndex; i < args.size(); i++) + { + expr = d_exprManager->mkExpr(HO_APPLY, expr, args[i]); + } + return expr; +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch (type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index e1518f9ca..f2044c7ef 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -573,6 +573,71 @@ public: std::vector<DatatypeType> mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, bool doOverload=false); + /** make flat function type + * + * Returns the "flat" function type corresponding to the function taking + * argument types "sorts" and range type "range". A flat function type is + * one whose range is not a function. Notice that if sorts is empty and range + * is not a function, then this function returns range itself. + * + * If range is a function type, we add its function argument sorts to sorts + * and consider its function range as the new range. For each sort S added + * to sorts in this process, we add a new bound variable of sort S to + * flattenVars. + * + * For example: + * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ): + * - returns the the function type (-> Int (-> Real Real) Int Bool) + * - updates sorts to { Int, (-> Real Real), Int }, + * - updates flattenVars to { x }, where x is bound variable of type Int. + * + * Notice that this method performs only one level of flattening, for example, + * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}): + * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool)) + * - updates sorts to { Int, (-> Real Real), Int }, + * - updates flattenVars to { x }, where x is bound variable of type Int. + * + * This method is required so that we do not return functions + * that have function return type (these give an unhandled exception + * in the ExprManager). For examples of the equivalence between function + * definitions in the proposed higher-order extension of the smt2 language, + * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf. + * + * The argument flattenVars is needed in the case of defined functions + * with function return type. These have implicit arguments, for instance: + * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x))) + * is equivalent to the command: + * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z)) + * where @ is (higher-order) application. In this example, z is added to + * flattenVars. + */ + Type mkFlatFunctionType(std::vector<Type>& sorts, + Type range, + std::vector<Expr>& flattenVars); + + /** make flat function type + * + * Same as above, but does not take argument flattenVars. + * This is used when the arguments of the function are not important (for + * instance, if we are only using this type in a declare-fun). + */ + Type mkFlatFunctionType(std::vector<Type>& sorts, Type range); + + /** make higher-order apply + * + * This returns the left-associative curried application of (function) expr to + * the arguments in args, starting at index startIndex. + * + * For example, mkHoApply( f, { a, b }, 0 ) returns + * (HO_APPLY (HO_APPLY f a) b) + * + * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where + * args[i-startIndex].getType() = Ti + * for each i where startIndex <= i < args.size(). If expr is not of this + * type, the expression returned by this method will not be well typed. + */ + Expr mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex = 0); + /** * Add an operator to the current legal set. * diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4d39c7635..5351bae15 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -266,6 +266,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] std::vector<Expr> terms; std::vector<Type> sorts; std::vector<std::pair<std::string, Type> > sortedVarNames; + std::vector<Expr> flattenVars; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -344,12 +345,12 @@ command [std::unique_ptr<CVC4::Command>* cmd] LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; - if( sorts.size() > 0 ) { - if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot " - "be declared in logic "); - } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + if( !sorts.empty() ) { + t = PARSER_STATE->mkFlatFunctionType(sorts, t); + } + if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { + PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot " + "be declared in logic "); } // we allow overloading for function declarations Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); @@ -364,7 +365,6 @@ command [std::unique_ptr<CVC4::Command>* cmd] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; if( sortedVarNames.size() > 0 ) { - std::vector<CVC4::Type> sorts; sorts.reserve(sortedVarNames.size()); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); @@ -372,7 +372,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] ++i) { sorts.push_back((*i).second); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars); } PARSER_STATE->pushScope(true); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = @@ -383,7 +383,14 @@ command [std::unique_ptr<CVC4::Command>* cmd] } } term[expr, expr2] - { PARSER_STATE->popScope(); + { + if( !flattenVars.empty() ){ + // if this function has any implicit variables flattenVars, + // we apply the body of the definition to the flatten vars + expr = PARSER_STATE->mkHoApply(expr, flattenVars); + terms.insert(terms.end(), flattenVars.begin(), flattenVars.end()); + } + PARSER_STATE->popScope(); // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) @@ -608,6 +615,9 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] if( range.isNull() ){ PARSER_STATE->parseError("Must supply return type for synth-fun."); } + if( range.isFunction() ){ + PARSER_STATE->parseError("Cannot use synth-fun with function return type."); + } seq.reset(new CommandSequence()); std::vector<Type> var_sorts; for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = @@ -1140,13 +1150,17 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] std::vector<std::pair<std::string, Type> > sortedVarNames; 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<Expr> funcs; std::vector<Expr> func_defs; Expr aexpr; std::unique_ptr<CVC4::CommandSequence> seq; + std::vector<Type> sorts; + std::vector<Expr> flattenVars; } /* meta-info */ : META_INFO_TOK metaInfoInternal[cmd] @@ -1191,37 +1205,16 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] { PARSER_STATE->checkUserSymbol(fname); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] - { if( sortedVarNames.size() > 0 ) { - std::vector<CVC4::Type> sorts; - sorts.reserve(sortedVarNames.size()); - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; - ++i) { - sorts.push_back((*i).second); - } - t = EXPR_MANAGER->mkFunctionType(sorts, t); - } - // allow overloading - Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true); + { + func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars); seq->addCommand(new DeclareFunctionCommand(fname, func, t)); - if( sortedVarNames.empty() ){ - func_app = func; - }else{ - std::vector< Expr > f_app; - f_app.push_back( func ); - PARSER_STATE->pushScope(true); - for(std::vector<std::pair<std::string, CVC4::Type> >::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 ); - } + PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, func_app, 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"); @@ -1246,23 +1239,19 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] { PARSER_STATE->checkUserSymbol(fname); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] - { sortedVarNamesList.push_back( sortedVarNames ); - if( sortedVarNamesList[0].size() > 0 ) { - if( !sortedVarNames.empty() ){ - std::vector<CVC4::Type> sorts; - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator - i = sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; ++i) { - sorts.push_back((*i).second); - } - t = EXPR_MANAGER->mkFunctionType(sorts, t); - } - } - sortedVarNames.clear(); - // allow overloading - Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true); + { + 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) + sortedVarNamesList.push_back( sortedVarNames ); + flattenVarsList.push_back( flattenVars ); + + // set up parsing the next variable list block + sortedVarNames.clear(); + flattenVars.clear(); } RPAREN_TOK )+ @@ -1274,27 +1263,19 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->parseError("Must define at least one function in " "define-funs-rec"); } - PARSER_STATE->pushScope(true); bvs.clear(); - if( sortedVarNamesList[0].empty() ){ - func_app = funcs[0]; - }else{ - std::vector< Expr > f_app; - f_app.push_back( funcs[0] ); - for(std::vector<std::pair<std::string, CVC4::Type> >::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 ); - } + PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0], + flattenVarsList[0], func_app, bvs, true); } ( term[expr,expr2] { + unsigned j = func_defs.size(); + if( !flattenVarsList[j].empty() ){ + expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] ); + } func_defs.push_back( expr ); + j++; Expr as = MK_EXPR( kind::EQUAL, func_app, expr ); if( !bvs.empty() ){ std::string attr_name("fun-def"); @@ -1311,23 +1292,9 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] //set up the next scope PARSER_STATE->popScope(); if( func_defs.size()<funcs.size() ){ - PARSER_STATE->pushScope(true); bvs.clear(); - 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<std::pair<std::string, CVC4::Type> >::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 ); - } + PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j], + flattenVarsList[j], func_app, bvs, true); } } )+ @@ -1398,7 +1365,10 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) " "cannot be declared in logic "); } - t = EXPR_MANAGER->mkFunctionType(sorts); + // must flatten + Type range = sorts.back(); + sorts.pop_back(); + t = PARSER_STATE->mkFlatFunctionType(sorts, range); } else { t = sorts[0]; } @@ -2008,7 +1978,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] if(isBuiltinOperator) { PARSER_STATE->checkOperator(kind, args.size()); } - expr = MK_EXPR(kind, args); + // may be partially applied function, in this case we should use HO_APPLY + if( args.size()>=2 && args[0].getType().isFunction() && + (args.size()-1)<((FunctionType)args[0].getType()).getArity() ){ + Debug("parser") << "Partial application of " << args[0]; + Debug("parser") << " : #argTypes = " << ((FunctionType)args[0].getType()).getArity(); + Debug("parser") << ", #args = " << args.size()-1 << std::endl; + // must curry the application + expr = args[0]; + expr = PARSER_STATE->mkHoApply( expr, args, 1 ); + }else{ + expr = MK_EXPR(kind, args); + } } | LPAREN_TOK @@ -2270,6 +2251,24 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] expr2 = f2; } } + | /* lambda */ + LPAREN_TOK HO_LAMBDA_TOK + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { + PARSER_STATE->pushScope(true); + for(const std::pair<std::string, CVC4::Type>& svn : sortedVarNames){ + args.push_back(PARSER_STATE->mkBoundVar(svn.first, svn.second)); + } + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); + args.clear(); + args.push_back(bvl); + } + term[f, f2] RPAREN_TOK + { + args.push_back( f ); + PARSER_STATE->popScope(); + expr = MK_EXPR( CVC4::kind::LAMBDA, args ); + } /* constants */ | INTEGER_LITERAL { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } @@ -2877,6 +2876,16 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } } ) RPAREN_TOK + | LPAREN_TOK HO_ARROW_TOK sortList[args] RPAREN_TOK + { + if(args.size()<2) { + PARSER_STATE->parseError("Arrow types must have at least 2 arguments"); + } + //flatten the type + Type rangeType = args.back(); + args.pop_back(); + t = PARSER_STATE->mkFlatFunctionType( args, rangeType ); + } ; /** @@ -3171,6 +3180,9 @@ FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowa FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative'; FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero'; +HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->'; +HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda'; + /** * A sequence of printable ASCII characters (except backslash) that starts * and ends with | and does not otherwise contain |. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7a681f327..c542e5917 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -349,6 +349,61 @@ Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) { } } +Expr Smt2::mkDefineFunRec( + const std::string& fname, + const std::vector<std::pair<std::string, Type> >& sortedVarNames, + Type t, + std::vector<Expr>& flattenVars) +{ + std::vector<Type> sorts; + for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames) + { + sorts.push_back(svn.second); + } + + // make the flattened function type, add bound variables + // to flattenVars if the defined function was given a function return type. + Type ft = mkFlatFunctionType(sorts, t, flattenVars); + + // allow overloading + return mkVar(fname, ft, ExprManager::VAR_FLAG_NONE, true); +} + +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) +{ + pushScope(bindingLevel); + + std::vector<Expr> f_app; + f_app.push_back(func); + // bound variables are those that are explicitly named in the preamble + // of the define-fun(s)-rec command, we define them here + for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames) + { + Expr v = mkBoundVar(svn.first, svn.second); + bvs.push_back(v); + f_app.push_back(v); + } + + 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() { d_logicSet = false; d_logic = LogicInfo(); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 84c049ce9..835ff2b58 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -91,6 +91,52 @@ public: */ virtual Expr getExpressionForNameAndType(const std::string& name, Type t); + /** Make function defined by a define-fun(s)-rec command. + * + * fname : the name of the function. + * sortedVarNames : the list of variable arguments for the function. + * t : the range type of the function we are defining. + * + * This function will create a bind a new function term to name fname. + * The type of this function is + * Parser::mkFlatFunctionType(sorts,t,flattenVars), + * where sorts are the types in the second components of sortedVarNames. + * As descibed in Parser::mkFlatFunctionType, new bound variables may be + * added to flattenVars in this function if the function is given a function + * range type. + */ + Expr mkDefineFunRec( + const std::string& fname, + const std::vector<std::pair<std::string, Type> >& sortedVarNames, + Type t, + std::vector<Expr>& flattenVars); + + /** Push scope for define-fun-rec + * + * This calls Parser::pushScope(bindingLevel) and sets up + * initial information for reading a body of a function definition + * in the define-fun-rec and define-funs-rec command. + * The input parameters func/flattenVars are the result + * of a call to mkDefineRec above. + * + * func : the function whose body we are defining. + * sortedVarNames : the list of variable arguments for the function. + * flattenVars : the implicit variables introduced when defining func. + * + * This function: + * (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); + void reset(); void resetAssertions(); |