diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-10 14:26:02 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-10 14:26:02 -0500 |
commit | 03a99a427eaa8c679ede508e11561467a2291334 (patch) | |
tree | b74688f17420c9d8a352b22eed339983d4e369ab /src/expr | |
parent | d1f3225e26b9d64f065048885053392b10994e71 (diff) |
Simplify how defined functions are tracked during parsing (#3177)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/symbol_table.cpp | 59 | ||||
-rw-r--r-- | src/expr/symbol_table.h | 38 |
2 files changed, 3 insertions, 94 deletions
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<string, Expr>(&d_context)), - d_typeMap(new (true) TypeMap(&d_context)), - d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&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<Type>& params, Type t, bool levelZero = false); @@ -396,9 +393,6 @@ class SymbolTable::Implementation { using TypeMap = CDHashMap<string, std::pair<vector<Type>, Type>>; TypeMap* d_typeMap; - /** A set of defined functions. */ - CDHashSet<Expr, ExprHashFunction>* 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<string, Expr>::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 @@ -70,36 +70,6 @@ class CVC4_PUBLIC SymbolTable { bool doOverload = false); /** - * Bind a function body to a name in the current scope. - * - * When doOverload is false: - * if <code>name</code> is already bound to an expression in the current - * level, then the binding is replaced. If <code>name</code> 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 <code>name</code> 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 <code>name</code> - * @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 <code>name</code> * is already bound to a type in the current level, then the binding * is replaced. If <code>name</code> is bound in a previous level, @@ -131,8 +101,7 @@ 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. @@ -140,11 +109,6 @@ class CVC4_PUBLIC SymbolTable { 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()). */ |