diff options
Diffstat (limited to 'src/expr/symbol_table.h')
| -rw-r--r-- | src/expr/symbol_table.h | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index fb6457f2e..35bed1dbf 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -29,6 +29,12 @@ namespace CVC4 { +namespace api { +class Solver; +class Sort; +class Term; +} // namespace api + class CVC4_PUBLIC ScopeException : public Exception {}; /** @@ -65,7 +71,7 @@ class CVC4_PUBLIC SymbolTable { * Returns false if the binding was invalid. */ bool bind(const std::string& name, - Expr obj, + api::Term obj, bool levelZero = false, bool doOverload = false); @@ -80,7 +86,7 @@ class CVC4_PUBLIC SymbolTable { * @param t the type to bind to <code>name</code> * @param levelZero set if the binding must be done at level 0 */ - void bindType(const std::string& name, Type t, bool levelZero = false); + void bindType(const std::string& name, api::Sort t, bool levelZero = false); /** * Bind a type to a name in the current scope. If <code>name</code> @@ -96,8 +102,8 @@ class CVC4_PUBLIC SymbolTable { * locally within the current scope) */ void bindType(const std::string& name, - const std::vector<Type>& params, - Type t, + const std::vector<api::Sort>& params, + api::Sort t, bool levelZero = false); /** @@ -125,7 +131,7 @@ class CVC4_PUBLIC SymbolTable { * It returns the null expression if there is not a unique expression bound to * <code>name</code> in the current scope (i.e. if there is not exactly one). */ - Expr lookup(const std::string& name) const; + api::Term lookup(const std::string& name) const; /** * Lookup a bound type. @@ -133,7 +139,7 @@ class CVC4_PUBLIC SymbolTable { * @param name the type identifier to lookup * @returns the type bound to <code>name</code> in the current scope. */ - Type lookupType(const std::string& name) const; + api::Sort lookupType(const std::string& name) const; /** * Lookup a bound parameterized type. @@ -143,8 +149,8 @@ class CVC4_PUBLIC SymbolTable { * @returns the type bound to <code>name(<i>params</i>)</code> in * the current scope. */ - Type lookupType(const std::string& name, - const std::vector<Type>& params) const; + api::Sort lookupType(const std::string& name, + const std::vector<api::Sort>& params) const; /** * Lookup the arity of a bound parameterized type. @@ -170,13 +176,14 @@ class CVC4_PUBLIC SymbolTable { //------------------------ operator overloading /** is this function overloaded? */ - bool isOverloadedFunction(Expr fun) const; + bool isOverloadedFunction(api::Term fun) const; /** Get overloaded constant for type. * If possible, it returns the defined symbol with name * that has type t. Otherwise returns null expression. */ - Expr getOverloadedConstantForType(const std::string& name, Type t) const; + api::Term getOverloadedConstantForType(const std::string& name, + api::Sort t) const; /** * If possible, returns the unique defined function for a name @@ -189,15 +196,12 @@ class CVC4_PUBLIC SymbolTable { * no functions with name and expected argTypes, or alternatively there is * more than one function with name and expected argTypes. */ - Expr getOverloadedFunctionForTypes(const std::string& name, - const std::vector< Type >& argTypes) const; + api::Term getOverloadedFunctionForTypes( + const std::string& name, const std::vector<api::Sort>& argTypes) const; //------------------------ end operator overloading private: - // Copying and assignment have not yet been implemented. - SymbolTable(const SymbolTable&); - SymbolTable& operator=(SymbolTable&); - + /** The implementation of the symbol table */ class Implementation; std::unique_ptr<Implementation> d_implementation; }; /* class SymbolTable */ |