19 #ifndef __CVC4__SYMBOL_TABLE_H
20 #define __CVC4__SYMBOL_TABLE_H
24 #include <ext/hash_map>
53 context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
59 context::CDHashSet<Expr, ExprHashFunction> *d_functions;
80 void bind(
const std::string& name,
Expr obj,
bool levelZero =
false)
throw();
94 void bindDefinedFunction(
const std::string& name,
Expr obj,
bool levelZero =
false)
throw();
107 void bindType(
const std::string& name, Type t,
bool levelZero =
false)
throw();
122 void bindType(
const std::string& name,
123 const std::vector<Type>& params,
124 Type t,
bool levelZero =
false)
throw();
133 bool isBound(
const std::string& name)
const throw();
138 bool isBoundDefinedFunction(
const std::string& name)
const throw();
144 bool isBoundDefinedFunction(
Expr func)
const throw();
152 bool isBoundType(
const std::string& name)
const throw();
160 Expr lookup(
const std::string& name)
const throw();
168 Type lookupType(
const std::string& name)
const throw();
178 Type lookupType(
const std::string& name,
179 const std::vector<Type>& params)
const throw();
184 size_t lookupArity(
const std::string& name);
196 void pushScope()
throw();
199 size_t getLevel()
const throw();
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Class encapsulating CVC4 expression types.
[[ Add one-line brief description here ]]
This is a forward declaration header to declare the CDHashMap<> template.
A convenience class for handling scoped declarations.
Macros that should be defined everywhere during the building of the libraries and driver binary...
This is a forward declaration header to declare the CDSet<> template.