From 252860a96565f3c73fff7132eb06059c90582bdd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Oct 2017 07:05:28 -0500 Subject: [PATCH] Op overload parser (#1162) * Update parser for operator overloading. * Improvements * Updates * Add assert --- src/parser/cvc/Cvc.g | 26 +-- src/parser/parser.cpp | 145 +++++++++++---- src/parser/parser.h | 147 +++++++++++++--- src/parser/smt1/Smt1.g | 4 +- src/parser/smt2/Smt2.g | 165 ++++++++++-------- src/parser/smt2/smt2.cpp | 12 ++ src/parser/smt2/smt2.h | 5 + test/regress/regress0/Makefile.am | 4 + test/regress/regress0/datatypes/error.cvc | 4 +- .../issue1063-overloading-dt-cons.smt2 | 14 ++ .../issue1063-overloading-dt-fun.smt2 | 11 ++ .../issue1063-overloading-dt-sel.smt2 | 11 ++ 12 files changed, 390 insertions(+), 158 deletions(-) create mode 100644 test/regress/regress0/issue1063-overloading-dt-cons.smt2 create mode 100644 test/regress/regress0/issue1063-overloading-dt-fun.smt2 create mode 100644 test/regress/regress0/issue1063-overloading-dt-sel.smt2 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d0324cc45..eef7ca54d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1047,7 +1047,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::Type& t, i != i_end; ++i) { if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) { - Type oldType = PARSER_STATE->getType(*i); + Type oldType = PARSER_STATE->getVariable(*i).getType(); Debug("parser") << " " << *i << " was declared previously " << "with type " << oldType << std::endl; if(oldType != t) { @@ -1745,22 +1745,10 @@ postfixTerm[CVC4::Expr& f] formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN // TODO: check arity - { Type t = args.front().getType(); - Debug("parser") << "type is " << t << std::endl; + { Kind k = PARSER_STATE->getKindForFunction(args.front()); Debug("parser") << "expr is " << args.front() << std::endl; - if(PARSER_STATE->isDefinedFunction(args.front())) { - f = MK_EXPR(CVC4::kind::APPLY, args); - } else if(t.isFunction()) { - f = MK_EXPR(CVC4::kind::APPLY_UF, args); - } else if(t.isConstructor()) { - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); - } else if(t.isSelector()) { - f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args); - } else if(t.isTester()) { - f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); - } else { - PARSER_STATE->parseError("internal error: unhandled function application kind"); - } + Debug("parser") << "kind is " << k << std::endl; + f = MK_EXPR(k, args); } /* record / tuple select */ @@ -2137,9 +2125,9 @@ simpleTerm[CVC4::Expr& f] /* variable / zero-ary constructor application */ | identifier[name,CHECK_DECLARED,SYM_VARIABLE] /* ascriptions will be required for parameterized zero-ary constructors */ - { f = PARSER_STATE->getVariable(name); } - { // datatypes: zero-ary constructors - Type t2 = PARSER_STATE->getType(name); + { f = PARSER_STATE->getVariable(name); + // datatypes: zero-ary constructors + Type t2 = f.getType(); if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) { // don't require parentheses, immediately turn it into an apply f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 63492caa8..c8b4ac966 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -23,6 +23,7 @@ #include #include #include +#include #include "base/output.h" #include "expr/expr.h" @@ -92,11 +93,61 @@ Expr Parser::getFunction(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Type Parser::getType(const std::string& var_name, SymbolType type) { - checkDeclaration(var_name, CHECK_DECLARED, type); - assert(isDeclared(var_name, type)); - Type t = getSymbol(var_name, type).getType(); - return t; +Expr Parser::getExpressionForName(const std::string& name) { + Type t; + return getExpressionForNameAndType(name, t); +} + +Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { + assert( isDeclared(name) ); + // first check if the variable is declared and not overloaded + Expr expr = getVariable(name); + if(expr.isNull()) { + // the variable is overloaded, try with type if the type exists + if(!t.isNull()) { + // if we decide later to support annotations for function types, this will update to + // separate t into ( argument types, return type ) + expr = getOverloadedConstantForType(name, t); + if(expr.isNull()) { + parseError("Cannot get overloaded constant for type ascription."); + } + }else{ + parseError("Overloaded constants must be type cast."); + } + } + // now, post-process the expression + assert( !expr.isNull() ); + if(isDefinedFunction(expr)) { + // defined functions/constants are wrapped in an APPLY so that they are + // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions + expr = d_exprManager->mkExpr(CVC4::kind::APPLY, expr); + }else{ + Type te = expr.getType(); + if(te.isConstructor() && ConstructorType(te).getArity() == 0) { + // nullary constructors have APPLY_CONSTRUCTOR kind with no children + expr = d_exprManager->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr); + } + } + return expr; +} + +Kind Parser::getKindForFunction(Expr fun) { + if(isDefinedFunction(fun)) { + return APPLY; + } + Type t = fun.getType(); + if(t.isConstructor()) { + return APPLY_CONSTRUCTOR; + } else if(t.isSelector()) { + return APPLY_SELECTOR; + } else if(t.isTester()) { + return APPLY_TESTER; + } else if(t.isFunction()) { + return APPLY_UF; + }else{ + parseError("internal error: unhandled function application kind"); + return UNDEFINED_KIND; + } } Type Parser::getSort(const std::string& name) { @@ -121,16 +172,15 @@ size_t Parser::getArity(const std::string& sort_name) { /* Returns true if name is bound to a boolean variable. */ bool Parser::isBoolean(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); + Expr expr = getVariable(name); + return !expr.isNull() && expr.getType().isBoolean(); } -/* Returns true if name is bound to a function-like thing (function, - * constructor, tester, or selector). */ -bool Parser::isFunctionLike(const std::string& name) { - if (!isDeclared(name, SYM_VARIABLE)) { +bool Parser::isFunctionLike(Expr fun) { + if(fun.isNull()) { return false; } - Type type = getType(name); + Type type = fun.getType(); return type.isFunction() || type.isConstructor() || type.isTester() || type.isSelector(); } @@ -151,16 +201,17 @@ bool Parser::isDefinedFunction(Expr func) { /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); + Expr expr = getVariable(name); + return !expr.isNull() && expr.getType().isPredicate(); } -Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) { +Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags, bool doOverload) { if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type, flags); - defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL); + defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } @@ -172,13 +223,13 @@ Expr Parser::mkBoundVar(const std::string& name, const Type& type) { } Expr Parser::mkFunction(const std::string& name, const Type& type, - uint32_t flags) { + uint32_t flags, bool doOverload) { if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type, flags); - defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL); + defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); return expr; } @@ -193,13 +244,13 @@ Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, } std::vector Parser::mkVars(const std::vector names, - const Type& type, uint32_t flags) { + const Type& type, uint32_t flags, bool doOverload) { if (d_globalDeclarations) { flags |= ExprManager::VAR_FLAG_GLOBAL; } std::vector vars; for (unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i], type, flags)); + vars.push_back(mkVar(names[i], type, flags, doOverload)); } return vars; } @@ -214,15 +265,23 @@ std::vector Parser::mkBoundVars(const std::vector names, } void Parser::defineVar(const std::string& name, const Expr& val, - bool levelZero) { + bool levelZero, bool doOverload) { Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl; - d_symtab->bind(name, val, levelZero); + if (!d_symtab->bind(name, val, levelZero, doOverload)) { + std::stringstream ss; + ss << "Failed to bind " << name << " to symbol of type " << val.getType(); + parseError(ss.str()); + } assert(isDeclared(name)); } void Parser::defineFunction(const std::string& name, const Expr& val, - bool levelZero) { - d_symtab->bindDefinedFunction(name, val, levelZero); + bool levelZero, bool doOverload) { + if (!d_symtab->bindDefinedFunction(name, val, levelZero, doOverload)) { + std::stringstream ss; + ss << "Failed to bind defined function " << name << " to symbol of type " << val.getType(); + parseError(ss.str()); + } assert(isDeclared(name)); } @@ -305,7 +364,7 @@ bool Parser::isUnresolvedType(const std::string& name) { } std::vector Parser::mkMutualDatatypeTypes( - std::vector& datatypes) { + std::vector& datatypes, bool doOverload) { try { std::vector types = d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved); @@ -326,6 +385,8 @@ std::vector Parser::mkMutualDatatypeTypes( } else { defineType(name, t); } + std::unordered_set< std::string > consNames; + std::unordered_set< std::string > selNames; for (Datatype::const_iterator j = dt.begin(), j_end = dt.end(); j != j_end; ++j) { const DatatypeConstructor& ctor = *j; @@ -333,27 +394,37 @@ std::vector Parser::mkMutualDatatypeTypes( Expr constructor = ctor.getConstructor(); Debug("parser-idt") << "+ define " << constructor << std::endl; string constructorName = ctor.getName(); - if (isDeclared(constructorName, SYM_VARIABLE)) { - throw ParserException(constructorName + " already declared"); + if(consNames.find(constructorName)==consNames.end()) { + if(!doOverload) { + checkDeclaration(constructorName, CHECK_UNDECLARED); + } + defineVar(constructorName, constructor, false, doOverload); + consNames.insert(constructorName); + }else{ + throw ParserException(constructorName + " already declared in this datatype"); } - defineVar(constructorName, constructor); Expr tester = ctor.getTester(); Debug("parser-idt") << "+ define " << tester << std::endl; string testerName = ctor.getTesterName(); - if (isDeclared(testerName, SYM_VARIABLE)) { - throw ParserException(testerName + " already declared"); + if(!doOverload) { + checkDeclaration(testerName, CHECK_UNDECLARED); } - defineVar(testerName, tester); + defineVar(testerName, tester, false, doOverload); for (DatatypeConstructor::const_iterator k = ctor.begin(), k_end = ctor.end(); k != k_end; ++k) { Expr selector = (*k).getSelector(); Debug("parser-idt") << "+++ define " << selector << std::endl; string selectorName = (*k).getName(); - if (isDeclared(selectorName, SYM_VARIABLE)) { - throw ParserException(selectorName + " already declared"); + if(selNames.find(selectorName)==selNames.end()) { + if(!doOverload) { + checkDeclaration(selectorName, CHECK_UNDECLARED); + } + defineVar(selectorName, selector, false, doOverload); + selNames.insert(selectorName); + }else{ + throw ParserException(selectorName + " already declared in this datatype"); } - defineVar(selectorName, selector); } } } @@ -426,9 +497,13 @@ void Parser::checkDeclaration(const std::string& varName, } } -void Parser::checkFunctionLike(const std::string& name) throw(ParserException) { - if (d_checksEnabled && !isFunctionLike(name)) { - parseError("Expecting function-like symbol, found '" + name + "'"); +void Parser::checkFunctionLike(Expr fun) throw(ParserException) { + if (d_checksEnabled && !isFunctionLike(fun)) { + stringstream ss; + ss << "Expecting function-like symbol, found '"; + ss << fun; + ss << "'"; + parseError(ss.str()); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index 5e867afa3..eb0588ab0 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -134,7 +134,7 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { */ class CVC4_PUBLIC Parser { friend class ParserBuilder; - +private: /** The expression manager */ ExprManager *d_exprManager; /** The resource manager associated with this expr manager */ @@ -235,7 +235,9 @@ class CVC4_PUBLIC Parser { */ std::list d_commandQueue; - /** Lookup a symbol in the given namespace. */ + /** Lookup a symbol in the given namespace (as specified by the type). + * Only returns a symbol if it is not overloaded, returns null otherwise. + */ Expr getSymbol(const std::string& var_name, SymbolType type); protected: @@ -318,21 +320,52 @@ public: bool logicIsForced() const { return d_logicIsForced; } /** - * Returns a variable, given a name. + * Gets the variable currently bound to name. * * @param name the name of the variable * @return the variable expression + * Only returns a variable if its name is not overloaded, returns null otherwise. */ Expr getVariable(const std::string& name); /** - * Returns a function, given a name. + * Gets the function currently bound to name. * * @param name the name of the variable * @return the variable expression + * Only returns a function if its name is not overloaded, returns null otherwise. */ Expr getFunction(const std::string& name); + /** + * Returns the expression that name should be interpreted as, based on the current binding. + * + * The symbol name should be declared. + * This creates the expression that the string "name" should be interpreted as. + * Typically this corresponds to a variable, but it may also correspond to + * a nullary constructor or a defined function. + * Only returns an expression if its name is not overloaded, returns null otherwise. + */ + virtual Expr getExpressionForName(const std::string& name); + + /** + * Returns the expression that name should be interpreted as, based on the current binding. + * + * This is the same as above but where the name has been type cast to t. + */ + virtual Expr getExpressionForNameAndType(const std::string& name, Type t); + + /** + * Returns the kind that should be used for applications of expression fun, where + * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true. + * Returns a parse error if fun does not have function-like type. + * + * For example, this function returns + * APPLY_UF if fun has function type, + * APPLY_CONSTRUCTOR if fun has constructor type. + */ + Kind getKindForFunction(Expr fun); + /** * Returns a sort, given a name. * @param sort_name the name to look up @@ -377,12 +410,15 @@ public: void reserveSymbolAtAssertionLevel(const std::string& name); /** - * Checks whether the given name is bound to a function. - * @param name the name to check - * @throws ParserException if checks are enabled and name is not - * bound to a function + * Checks whether the given expression is function-like, i.e. + * it expects arguments. This is checked by looking at the type + * of fun. Examples of function types are function, constructor, + * selector, tester. + * @param fun the expression to check + * @throws ParserException if checks are enabled and fun is not + * a function */ - void checkFunctionLike(const std::string& name) throw(ParserException); + void checkFunctionLike(Expr fun) throw(ParserException); /** * Check that kind can accept numArgs arguments. @@ -405,52 +441,82 @@ public: */ void checkOperator(Kind kind, unsigned numArgs) throw(ParserException); - /** - * Returns the type for the variable with the given name. + /** Create a new CVC4 variable expression of the given type. * - * @param var_name the symbol to lookup - * @param type the (namespace) type of the symbol + * flags specify information about the variable, e.g. whether it is global or defined + * (see enum in expr_manager_template.h). + * + * If a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. */ - Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); - - /** Create a new CVC4 variable expression of the given type. */ Expr mkVar(const std::string& name, const Type& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE); + uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool doOverload = false); /** * Create a set of new CVC4 variable expressions of the given type. + * + * flags specify information about the variable, e.g. whether it is global or defined + * (see enum in expr_manager_template.h). + * + * For each name, if a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. */ std::vector mkVars(const std::vector names, const Type& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE); + uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool doOverload = false); /** Create a new CVC4 bound variable expression of the given type. */ Expr mkBoundVar(const std::string& name, const Type& type); /** * Create a set of new CVC4 bound variable expressions of the given type. + * + * flags specify information about the variable, e.g. whether it is global or defined + * (see enum in expr_manager_template.h). + * + * For each name, if a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. */ std::vector mkBoundVars(const std::vector names, const Type& type); /** Create a new CVC4 function expression of the given type. */ Expr mkFunction(const std::string& name, const Type& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE); + uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool doOverload=false); /** * Create a new CVC4 function expression of the given type, * appending a unique index to its name. (That's the ONLY * difference between mkAnonymousFunction() and mkFunction()). + * + * flags specify information about the variable, e.g. whether it is global or defined + * (see enum in expr_manager_template.h). */ Expr mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); - /** Create a new variable definition (e.g., from a let binding). */ + /** Create a new variable definition (e.g., from a let binding). + * levelZero is set if the binding must be done at level 0. + * If a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. + */ void defineVar(const std::string& name, const Expr& val, - bool levelZero = false); + bool levelZero = false, bool doOverload = false); - /** Create a new function definition (e.g., from a define-fun). */ + /** Create a new function definition (e.g., from a define-fun). + * levelZero is set if the binding must be done at level 0. + * If a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. + */ void defineFunction(const std::string& name, const Expr& val, - bool levelZero = false); + bool levelZero = false, bool doOverload = false); /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); @@ -500,9 +566,12 @@ public: /** * Create sorts of mutually-recursive datatypes. + * For each symbol defined by the datatype, if a symbol with name already exists, + * then if doOverload is true, we create overloaded operators. + * else if doOverload is false, the existing expression is shadowed by the new expression. */ std::vector - mkMutualDatatypeTypes(std::vector& datatypes); + mkMutualDatatypeTypes(std::vector& datatypes, bool doOverload=false); /** * Add an operator to the current legal set. @@ -522,8 +591,10 @@ public: /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); - /** Is the symbol bound to a function (or function-like thing)? */ - bool isFunctionLike(const std::string& name); + /** Is fun a function (or function-like thing)? + * Currently this means its type is either a function, constructor, tester, or selector. + */ + bool isFunctionLike(Expr fun); /** Is the symbol bound to a defined function? */ bool isDefinedFunction(const std::string& name); @@ -663,6 +734,30 @@ public: ~ExprStream() { delete d_parser; } Expr nextExpr() { return d_parser->nextExpression(); } };/* class Parser::ExprStream */ + + //------------------------ operator overloading + /** is this function overloaded? */ + bool isOverloadedFunction(Expr fun) { + return d_symtab->isOverloadedFunction(fun); + } + + /** Get overloaded constant for type. + * If possible, it returns a defined symbol with name + * that has type t. Otherwise returns null expression. + */ + Expr getOverloadedConstantForType(const std::string& name, Type t) { + return d_symtab->getOverloadedConstantForType(name, t); + } + + /** + * If possible, returns a defined function for a name + * and a vector of expected argument types. Otherwise returns + * null expression. + */ + Expr getOverloadedFunctionForTypes(const std::string& name, std::vector< Type >& argTypes) { + return d_symtab->getOverloadedFunctionForTypes(name, argTypes); + } + //------------------------ end operator overloading };/* class Parser */ }/* CVC4::parser namespace */ diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 93169504d..479ef35c5 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -483,8 +483,8 @@ functionSymbol[CVC4::Expr& fun] std::string name; } : functionName[name,CHECK_DECLARED] - { PARSER_STATE->checkFunctionLike(name); - fun = PARSER_STATE->getVariable(name); } + { fun = PARSER_STATE->getVariable(name); + PARSER_STATE->checkFunctionLike(fun); } ; /** diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2aa85fbe3..3deffe703 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -339,7 +339,7 @@ command [std::unique_ptr* cmd] } | /* function declaration */ DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] @@ -351,7 +351,8 @@ command [std::unique_ptr* cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkVar(name, t); + // we allow overloading for function declarations + Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); cmd->reset(new DeclareFunctionCommand(name, func, t)); } | /* function definition */ @@ -386,8 +387,9 @@ command [std::unique_ptr* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) + // we allow overloading for function definitions Expr func = PARSER_STATE->mkFunction(name, t, - ExprManager::VAR_FLAG_DEFINED); + ExprManager::VAR_FLAG_DEFINED, true); cmd->reset(new DefineFunctionCommand(name, func, terms, expr)); } | /* value query */ @@ -622,7 +624,8 @@ sygusCommand [std::unique_ptr* cmd] }else{ synth_fun_type = range; } - synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type); + // allow overloading for synth fun + synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true); PARSER_STATE->pushScope(true); for(std::vector >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; @@ -1145,10 +1148,11 @@ smt25Command[std::unique_ptr* cmd] /* declare-const */ | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] - { Expr c = PARSER_STATE->mkVar(name, t); + { // allow overloading here + Expr c = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); cmd->reset(new DeclareFunctionCommand(name, c, t)); } /* get model */ @@ -1178,7 +1182,7 @@ smt25Command[std::unique_ptr* cmd] { PARSER_STATE->checkThatLogicIsSet(); seq.reset(new CVC4::CommandSequence()); } - symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] + symbol[fname,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(fname); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] @@ -1192,7 +1196,8 @@ smt25Command[std::unique_ptr* cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkVar(fname, t); + // allow overloading + Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true); seq->addCommand(new DeclareFunctionCommand(fname, func, t)); if( sortedVarNames.empty() ){ func_app = func; @@ -1249,7 +1254,8 @@ smt25Command[std::unique_ptr* cmd] } } sortedVarNames.clear(); - Expr func = PARSER_STATE->mkVar(fname, t); + // allow overloading + Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true); seq->addCommand(new DeclareFunctionCommand(fname, func, t)); funcs.push_back( func ); } @@ -1391,7 +1397,8 @@ extendedCommand[std::unique_ptr* cmd] } else { t = sorts[0]; } - Expr func = PARSER_STATE->mkVar(name, t); + // allow overloading + Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } @@ -1412,7 +1419,8 @@ extendedCommand[std::unique_ptr* cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkVar(name, t); + // allow overloading + Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } @@ -1513,7 +1521,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr* cmd] RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); - cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); + cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true))); } ; @@ -1529,7 +1537,7 @@ datatypeDefCommand[bool isCo, std::unique_ptr* cmd] } ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ RPAREN_TOK - { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); } + { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true))); } ; datatypesDefCommand[bool isCo, std::unique_ptr* cmd] @@ -1591,7 +1599,7 @@ datatypesDefCommand[bool isCo, std::unique_ptr* cmd] )+ RPAREN_TOK { PARSER_STATE->popScope(); - cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); + cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true))); } ; @@ -1787,6 +1795,22 @@ symbolicExpr[CVC4::SExpr& sexpr] * @return the expression representing the formula */ term[CVC4::Expr& expr, CVC4::Expr& expr2] +@init { + std::string name; +} +: termNonVariable[expr, expr2] + /* a variable */ + | symbol[name,CHECK_DECLARED,SYM_VARIABLE] + { expr = PARSER_STATE->getExpressionForName(name); + assert( !expr.isNull() ); + } + ; + +/** + * Matches a term. + * @return the expression representing the formula + */ +termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind = kind::NULL_EXPR; @@ -1804,6 +1828,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Type type; std::string s; bool isBuiltinOperator = false; + bool isOverloadedFunction = false; + bool readVariable = false; int match_vindex = -1; std::vector match_ptypes; } @@ -1852,17 +1878,29 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK + | LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } ) + sortSymbol[type, CHECK_DECLARED] RPAREN_TOK { + if(readVariable) { + Trace("parser-overloading") << "Getting variable expression of type " << name << " with type " << type << std::endl; + // get the variable expression for the type + f = PARSER_STATE->getExpressionForNameAndType(name, type); + assert( !f.isNull() ); + } if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) { - std::vector v; - Expr e = f.getOperator(); - const DatatypeConstructor& dtc = - Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() )); - v.insert(v.end(), f.begin(), f.end()); - expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); + // could be a parametric type constructor or just an overloaded constructor + if(((DatatypeType)type).isParametric()) { + std::vector v; + Expr e = f.getOperator(); + const DatatypeConstructor& dtc = + Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, + MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() )); + v.insert(v.end(), f.begin(), f.end()); + expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); + }else{ + expr = f; + } } else if(f.getKind() == CVC4::kind::EMPTYSET) { Debug("parser") << "Empty set encountered: " << f << " " << f2 << " " << type << std::endl; @@ -1877,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); + }else{ + expr = f; } } } @@ -1925,32 +1965,20 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else { /* A non-built-in function application */ PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE); - //hack to allow constants with parentheses (disabled for now) - //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(name) ){ - // op = PARSER_STATE->getVariable(name); - //}else{ - PARSER_STATE->checkFunctionLike(name); - const bool isDefinedFunction = - PARSER_STATE->isDefinedFunction(name); - if(isDefinedFunction) { - expr = PARSER_STATE->getFunction(name); - kind = CVC4::kind::APPLY; - } else { - expr = PARSER_STATE->getVariable(name); - Type t = expr.getType(); - if(t.isConstructor()) { - kind = CVC4::kind::APPLY_CONSTRUCTOR; - } else if(t.isSelector()) { - kind = CVC4::kind::APPLY_SELECTOR; - } else if(t.isTester()) { - kind = CVC4::kind::APPLY_TESTER; - } else { - kind = CVC4::kind::APPLY_UF; - } + expr = PARSER_STATE->getVariable(name); + if(!expr.isNull()) { + //hack to allow constants with parentheses (disabled for now) + //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(expr) ){ + // op = PARSER_STATE->getVariable(name); + //}else{ + PARSER_STATE->checkFunctionLike(expr); + kind = PARSER_STATE->getKindForFunction(expr); + args.push_back(expr); + }else{ + isOverloadedFunction = true; } - args.push_back(expr); } - } + } //(termList[args,expr])? RPAREN_TOK termList[args,expr] RPAREN_TOK { Debug("parser") << "args has size " << args.size() << std::endl @@ -1958,6 +1986,20 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { Debug("parser") << "++ " << *i << std::endl; } + if(isOverloadedFunction) { + std::vector< Type > argTypes; + for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { + argTypes.push_back( (*i).getType() ); + } + expr = PARSER_STATE->getOverloadedFunctionForTypes(name, argTypes); + if(!expr.isNull()) { + PARSER_STATE->checkFunctionLike(expr); + kind = PARSER_STATE->getKindForFunction(expr); + args.insert(args.begin(),expr); + }else{ + PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types."); + } + } if(isBuiltinOperator) { PARSER_STATE->checkOperator(kind, args.size()); } @@ -2169,30 +2211,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] // ConstructorType(expr.getType()).getArity()==0; expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); } - /* a variable */ - | symbol[name,CHECK_DECLARED,SYM_VARIABLE] - { if( PARSER_STATE->sygus() && name[0]=='-' && - name.find_first_not_of("0123456789", 1) == std::string::npos ){ - //allow unary minus in sygus - expr = MK_CONST(Rational(name)); - }else{ - const bool isDefinedFunction = - PARSER_STATE->isDefinedFunction(name); - if(PARSER_STATE->isAbstractValue(name)) { - expr = PARSER_STATE->mkAbstractValue(name); - } else if(isDefinedFunction) { - expr = MK_EXPR(CVC4::kind::APPLY, - PARSER_STATE->getFunction(name)); - } else { - expr = PARSER_STATE->getVariable(name); - Type t = PARSER_STATE->getType(name); - if(t.isConstructor() && ConstructorType(t).getArity() == 0) { - // don't require parentheses, immediately turn it into an apply - expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); - } - } - } - } /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] @@ -2966,11 +2984,10 @@ constructorDef[CVC4::Datatype& type] std::string id; CVC4::DatatypeConstructor* ctor = NULL; } - : symbol[id,CHECK_UNDECLARED,SYM_VARIABLE] + : symbol[id,CHECK_NONE,SYM_VARIABLE] { // make the tester std::string testerId("is-"); testerId.append(id); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); ctor = new CVC4::DatatypeConstructor(id, testerId); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* @@ -2986,7 +3003,7 @@ selector[CVC4::DatatypeConstructor& ctor] std::string id; Type t, t2; } - : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE] + : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE] { ctor.addArg(id, t); Debug("parser-idt") << "selector: " << id.c_str() << " of type " << t << std::endl; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index aeabdbac2..acfd886ce 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -337,6 +337,18 @@ bool Smt2::logicIsSet() { return d_logicSet; } +Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) { + if(sygus() && name[0]=='-' && + name.find_first_not_of("0123456789", 1) == std::string::npos) { + //allow unary minus in sygus + return getExprManager()->mkConst(Rational(name)); + }else if(isAbstractValue(name)) { + return mkAbstractValue(name); + }else{ + return Parser::getExpressionForNameAndType(name, t); + } +} + void Smt2::reset() { d_logicSet = false; d_logic = LogicInfo(); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index e470c8111..46f1c631b 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -87,6 +87,11 @@ public: bool isTheoryEnabled(Theory theory) const; bool logicIsSet(); + + /** + * Returns the expression that name should be interpreted as. + */ + virtual Expr getExpressionForNameAndType(const std::string& name, Type t); void reset(); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5000be7a2..43c7ae3b1 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -70,9 +70,13 @@ SMT2_TESTS = \ hung13sdk_output2.smt2 \ declare-funs.smt2 \ declare-fun-is-match.smt2 \ + issue1063-overloading-dt-cons.smt2 \ + issue1063-overloading-dt-sel.smt2 \ + issue1063-overloading-dt-fun.smt2 \ non-fatal-errors.smt2 \ sqrt2-sort-inf-unk.smt2 + # Regression tests for PL inputs CVC_TESTS = \ boolean.cvc \ diff --git a/test/regress/regress0/datatypes/error.cvc b/test/regress/regress0/datatypes/error.cvc index 66fa17e02..23e658e6c 100644 --- a/test/regress/regress0/datatypes/error.cvc +++ b/test/regress/regress0/datatypes/error.cvc @@ -1,7 +1,7 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: foo already declared +% EXPECT-ERROR: Parse Error: foo already declared in this datatype % EXIT: 1 -DATATYPE single_ctor = foo(bar:REAL) END; +DATATYPE single_ctor = foo(bar:REAL) | foo(bar2:REAL) END; DATATYPE double_ctor = foo(bar:REAL) END; diff --git a/test/regress/regress0/issue1063-overloading-dt-cons.smt2 b/test/regress/regress0/issue1063-overloading-dt-cons.smt2 new file mode 100644 index 000000000..f8ca2a9e5 --- /dev/null +++ b/test/regress/regress0/issue1063-overloading-dt-cons.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes () ((Enum0 (In_Air) (On_Ground) (None)))) +(declare-datatypes () ((Enum1 (True) (False) (None)))) +(declare-fun var_0 (Int) Enum0) +(declare-fun var_1 (Int) Enum1) +(assert (= (var_0 0) (as None Enum0))) +(assert (= (var_1 1) (as None Enum1))) +(assert (not (is-In_Air (var_0 0)))) +(declare-fun var_2 () Enum1) +(assert (is-None var_2)) +(check-sat) diff --git a/test/regress/regress0/issue1063-overloading-dt-fun.smt2 b/test/regress/regress0/issue1063-overloading-dt-fun.smt2 new file mode 100644 index 000000000..9cae20647 --- /dev/null +++ b/test/regress/regress0/issue1063-overloading-dt-fun.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes () ((Enum (cons (val Int)) (On_Ground) (None)))) +(declare-fun cons (Int Int) Int) +(declare-fun cons (Enum) Bool) +(declare-fun cons (Bool) Int) +(assert (cons (cons 0))) +(assert (= (cons (cons true) (cons false)) 4)) +(check-sat) diff --git a/test/regress/regress0/issue1063-overloading-dt-sel.smt2 b/test/regress/regress0/issue1063-overloading-dt-sel.smt2 new file mode 100644 index 000000000..b3316d373 --- /dev/null +++ b/test/regress/regress0/issue1063-overloading-dt-sel.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes () ((Enum0 (cons (data Int)) (None)))) +(declare-datatypes () ((Enum1 (cons (data Bool)) (None)))) +(declare-fun var_0 () Enum0) +(declare-fun var_1 () Enum1) +(assert (= (data var_0) 5)) +(assert (data var_1)) +(check-sat) -- 2.30.2