From: Andrew Reynolds Date: Sat, 10 Aug 2019 19:26:02 +0000 (-0500) Subject: Simplify how defined functions are tracked during parsing (#3177) X-Git-Tag: cvc5-1.0.0~4032 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03a99a427eaa8c679ede508e11561467a2291334;p=cvc5.git Simplify how defined functions are tracked during parsing (#3177) --- diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index dd75170b5..c14143ef1 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -344,21 +344,18 @@ class SymbolTable::Implementation { Implementation() : d_context(), d_exprMap(new (true) CDHashMap(&d_context)), - d_typeMap(new (true) TypeMap(&d_context)), - d_functions(new (true) CDHashSet(&d_context)) { + d_typeMap(new (true) TypeMap(&d_context)) + { d_overload_trie = new OverloadedTypeTrie(&d_context); } ~Implementation() { d_exprMap->deleteSelf(); d_typeMap->deleteSelf(); - d_functions->deleteSelf(); delete d_overload_trie; } bool bind(const string& name, Expr obj, bool levelZero, bool doOverload); - bool bindDefinedFunction(const string& name, Expr obj, bool levelZero, - bool doOverload); void bindType(const string& name, Type t, bool levelZero = false); void bindType(const string& name, const vector& params, Type t, bool levelZero = false); @@ -396,9 +393,6 @@ class SymbolTable::Implementation { using TypeMap = CDHashMap, Type>>; TypeMap* d_typeMap; - /** A set of defined functions. */ - CDHashSet* d_functions; - //------------------------ operator overloading // the null expression Expr d_nullExpr; @@ -430,40 +424,10 @@ bool SymbolTable::Implementation::bind(const string& name, Expr obj, return true; } -bool SymbolTable::Implementation::bindDefinedFunction(const string& name, - Expr obj, bool levelZero, - bool doOverload) { - PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); - ExprManagerScope ems(obj); - if (doOverload) { - if (!bindWithOverloading(name, obj)) { - return false; - } - } - if (levelZero) { - d_exprMap->insertAtContextLevelZero(name, obj); - d_functions->insertAtContextLevelZero(obj); - } else { - d_exprMap->insert(name, obj); - d_functions->insert(obj); - } - return true; -} - bool SymbolTable::Implementation::isBound(const string& name) const { return d_exprMap->find(name) != d_exprMap->end(); } -bool SymbolTable::Implementation::isBoundDefinedFunction( - const string& name) const { - CDHashMap::const_iterator found = d_exprMap->find(name); - return found != d_exprMap->end() && d_functions->contains((*found).second); -} - -bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const { - return d_functions->contains(func); -} - Expr SymbolTable::Implementation::lookup(const string& name) const { Assert(isBound(name)); Expr expr = (*d_exprMap->find(name)).second; @@ -646,15 +610,6 @@ bool SymbolTable::bind(const string& name, return d_implementation->bind(name, obj, levelZero, doOverload); } -bool SymbolTable::bindDefinedFunction(const string& name, - Expr obj, - bool levelZero, - bool doOverload) -{ - return d_implementation->bindDefinedFunction(name, obj, levelZero, - doOverload); -} - void SymbolTable::bindType(const string& name, Type t, bool levelZero) { d_implementation->bindType(name, t, levelZero); @@ -672,16 +627,6 @@ bool SymbolTable::isBound(const string& name) const { return d_implementation->isBound(name); } - -bool SymbolTable::isBoundDefinedFunction(const string& name) const -{ - return d_implementation->isBoundDefinedFunction(name); -} - -bool SymbolTable::isBoundDefinedFunction(Expr func) const -{ - return d_implementation->isBoundDefinedFunction(func); -} bool SymbolTable::isBoundType(const string& name) const { return d_implementation->isBoundType(name); diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 07f557059..868106a19 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -69,36 +69,6 @@ class CVC4_PUBLIC SymbolTable { bool levelZero = false, bool doOverload = false); - /** - * Bind a function body to a name in the current scope. - * - * When doOverload is false: - * if name is already bound to an expression in the current - * level, then the binding is replaced. If name is bound - * in a previous level, then the binding is "covered" by this one - * until the current scope is popped. - * If levelZero is true the name shouldn't be already bound. - * - * When doOverload is true: - * if name is already bound to an expression in the current - * level, then we mark the previous bound expression and obj as overloaded - * functions. - * - * Same as bind() but registers this as a function (so that - * isBoundDefinedFunction() returns true). - * - * @param name an identifier - * @param obj the expression to bind to name - * @param levelZero set if the binding must be done at level 0 - * @param doOverload set if the binding can overload the function name. - * - * Returns false if the binding was invalid. - */ - bool bindDefinedFunction(const std::string& name, - Expr obj, - bool levelZero = false, - bool doOverload = false); - /** * Bind a type to a name in the current scope. If name * is already bound to a type in the current level, then the binding @@ -131,19 +101,13 @@ class CVC4_PUBLIC SymbolTable { bool levelZero = false); /** - * Check whether a name is bound to an expression with either bind() - * or bindDefinedFunction(). + * Check whether a name is bound to an expression with bind(). * * @param name the identifier to check. * @returns true iff name is bound in the current scope. */ bool isBound(const std::string& name) const; - /** - * Check whether a name was bound to a function with bindDefinedFunction(). - */ - bool isBoundDefinedFunction(const std::string& name) const; - /** * Check whether an Expr was bound to a function (i.e., was the * second arg to bindDefinedFunction()). diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 6de746ad7..7191ee064 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1153,7 +1153,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::Type& t, Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl; PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); - PARSER_STATE->defineFunction(*i, f); + PARSER_STATE->defineVar(*i, f); Command* decl = new DefineFunctionCommand(*i, func, f); seq->addCommand(decl); } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c8e09b8e0..8217e32c6 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -138,19 +138,25 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } Kind Parser::getKindForFunction(Expr fun) { - if(isDefinedFunction(fun)) { + Type t = fun.getType(); + if (t.isFunction()) + { return APPLY_UF; } - Type t = fun.getType(); - if(t.isConstructor()) { + else if (t.isConstructor()) + { return APPLY_CONSTRUCTOR; - } else if(t.isSelector()) { + } + else if (t.isSelector()) + { return APPLY_SELECTOR; - } else if(t.isTester()) { + } + else if (t.isTester()) + { return APPLY_TESTER; - } else if(t.isFunction()) { - return APPLY_UF; - }else{ + } + else + { parseError("internal error: unhandled function application kind"); return UNDEFINED_KIND; } @@ -191,20 +197,6 @@ bool Parser::isFunctionLike(Expr fun) { type.isSelector(); } -/* Returns true if name is bound to a defined function. */ -bool Parser::isDefinedFunction(const std::string& name) { - // more permissive in type than isFunction(), because defined - // functions can be zero-ary and declared functions cannot. - return d_symtab->isBoundDefinedFunction(name); -} - -/* Returns true if the Expr is a defined function. */ -bool Parser::isDefinedFunction(Expr func) { - // more permissive in type than isFunction(), because defined - // functions can be zero-ary and declared functions cannot. - return d_symtab->isBoundDefinedFunction(func); -} - /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { Expr expr = getVariable(name); @@ -228,17 +220,6 @@ Expr Parser::mkBoundVar(const std::string& name, const Type& type) { return expr; } -Expr Parser::mkFunction(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 = getExprManager()->mkVar(name, type, flags); - defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload); - return expr; -} - Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) { if (d_globalDeclarations) { @@ -282,16 +263,6 @@ void Parser::defineVar(const std::string& name, const Expr& val, assert(isDeclared(name)); } -void Parser::defineFunction(const std::string& name, const Expr& val, - 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)); -} - void Parser::defineType(const std::string& name, const Type& type) { d_symtab->bindType(name, type); assert(isDeclared(name, SYM_SORT)); diff --git a/src/parser/parser.h b/src/parser/parser.h index 8f9cc425a..9319181db 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -497,15 +497,10 @@ public: */ 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, - 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()). + * difference between mkAnonymousFunction() and mkVar()). * * flags specify information about the variable, e.g. whether it is global or defined * (see enum in expr_manager_template.h). @@ -522,15 +517,6 @@ public: void defineVar(const std::string& name, const Expr& val, bool levelZero = false, bool doOverload = false); - /** 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 doOverload = false); - /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); @@ -677,12 +663,6 @@ public: */ bool isFunctionLike(Expr fun); - /** Is the symbol bound to a defined function? */ - bool isDefinedFunction(const std::string& name); - - /** Is the Expr a defined function? */ - bool isDefinedFunction(Expr func); - /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2a736402e..c672d8ff5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -400,8 +400,8 @@ command [std::unique_ptr* cmd] // 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, true); + Expr func = PARSER_STATE->mkVar(name, t, + ExprManager::VAR_FLAG_DEFINED, true); cmd->reset(new DefineFunctionCommand(name, func, terms, expr)); } | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] @@ -745,7 +745,8 @@ sygusCommand [std::unique_ptr* cmd] } ( symbol[name,CHECK_NONE,SYM_VARIABLE] { if( !terms.empty() ){ - if( !PARSER_STATE->isDefinedFunction(name) ){ + if (!PARSER_STATE->isDeclared(name)) + { std::stringstream ss; ss << "Function " << name << " in inv-constraint is not defined."; PARSER_STATE->parseError(ss.str()); @@ -988,11 +989,10 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] // fail, but we need an operator to continue here.. Debug("parser-sygus") << "Sygus grammar " << fun << " : op (declare=" - << PARSER_STATE->isDeclared(name) << ", define=" - << PARSER_STATE->isDefinedFunction(name) << ") : " << name + << PARSER_STATE->isDeclared(name) << ") : " << name << std::endl; - if(!PARSER_STATE->isDeclared(name) && - !PARSER_STATE->isDefinedFunction(name) ){ + if (!PARSER_STATE->isDeclared(name)) + { PARSER_STATE->parseError("Functions in sygus grammars must be " "defined."); } @@ -1459,8 +1459,8 @@ extendedCommand[std::unique_ptr* cmd] ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } term[e,e2] - { Expr func = PARSER_STATE->mkFunction(name, e.getType(), - ExprManager::VAR_FLAG_DEFINED); + { Expr func = PARSER_STATE->mkVar(name, e.getType(), + ExprManager::VAR_FLAG_DEFINED); cmd->reset(new DefineFunctionCommand(name, func, e)); } | LPAREN_TOK @@ -1492,8 +1492,8 @@ extendedCommand[std::unique_ptr* cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkFunction(name, t, - ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(name, t, + ExprManager::VAR_FLAG_DEFINED); cmd->reset(new DefineFunctionCommand(name, func, terms, e)); } ) @@ -1515,8 +1515,8 @@ extendedCommand[std::unique_ptr* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Expr func = PARSER_STATE->mkFunction(name, t, - ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(name, t, + ExprManager::VAR_FLAG_DEFINED); cmd->reset(new DefineFunctionCommand(name, func, terms, e)); } @@ -2863,7 +2863,7 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] // check that sexpr is a fresh function symbol, and reserve it PARSER_STATE->reserveSymbolAtAssertionLevel(name); // define it - Expr func = PARSER_STATE->mkFunction(name, expr.getType()); + Expr func = PARSER_STATE->mkVar(name, expr.getType()); // remember the last term to have been given a :named attribute PARSER_STATE->setLastNamedTerm(expr, name); // bind name to expr with define-fun diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 039f573f9..be0306a9e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1171,7 +1171,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); std::stringstream ss; ss << datatypes[index].getName() << "_let"; - Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + Expr let_func = mkVar(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); d_sygus_defined_funs.push_back( let_func ); preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) ); @@ -1338,7 +1338,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, // the given name. spc = std::make_shared(cnames[i]); } - else if (isDefinedFunction(ops[i])) + else if (ops[i].getKind() == kind::VARIABLE) { Debug("parser-sygus") << "--> Defined function " << ops[i] << std::endl; diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 599b3bbe1..54fba4d1b 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -841,7 +841,7 @@ thfAtomTyping[CVC4::Command*& cmd] CVC4::Expr freshExpr; if (type.isFunction()) { - freshExpr = PARSER_STATE->mkFunction(name, type); + freshExpr = PARSER_STATE->mkVar(name, type); } else { @@ -1077,12 +1077,7 @@ tffTypedAtom[CVC4::Command*& cmd] } } else { // as yet, it's undeclared - CVC4::Expr expr; - if(type.isFunction()) { - expr = PARSER_STATE->mkFunction(name, type); - } else { - expr = PARSER_STATE->mkVar(name, type); - } + CVC4::Expr expr = PARSER_STATE->mkVar(name, type); cmd = new DeclareFunctionCommand(name, expr, type); } }