cvc4-1.4
symbol_table.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #ifndef __CVC4__SYMBOL_TABLE_H
20 #define __CVC4__SYMBOL_TABLE_H
21 
22 #include <vector>
23 #include <utility>
24 #include <ext/hash_map>
25 
26 #include "expr/expr.h"
27 #include "util/hash.h"
28 
31 
32 namespace CVC4 {
33 
34 class Type;
35 
36 namespace context {
37  class Context;
38 }/* CVC4::context namespace */
39 
41 };/* class ScopeException */
42 
50  context::Context* d_context;
51 
53  context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
54 
56  context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
57 
59  context::CDHashSet<Expr, ExprHashFunction> *d_functions;
60 
61 public:
63  SymbolTable();
64 
66  ~SymbolTable();
67 
80  void bind(const std::string& name, Expr obj, bool levelZero = false) throw();
81 
94  void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw();
95 
107  void bindType(const std::string& name, Type t, bool levelZero = false) throw();
108 
122  void bindType(const std::string& name,
123  const std::vector<Type>& params,
124  Type t, bool levelZero = false) throw();
125 
133  bool isBound(const std::string& name) const throw();
134 
138  bool isBoundDefinedFunction(const std::string& name) const throw();
139 
144  bool isBoundDefinedFunction(Expr func) const throw();
145 
152  bool isBoundType(const std::string& name) const throw();
153 
160  Expr lookup(const std::string& name) const throw();
161 
168  Type lookupType(const std::string& name) const throw();
169 
178  Type lookupType(const std::string& name,
179  const std::vector<Type>& params) const throw();
180 
184  size_t lookupArity(const std::string& name);
185 
193  void popScope() throw(ScopeException);
194 
196  void pushScope() throw();
197 
199  size_t getLevel() const throw();
200 
201 };/* class SymbolTable */
202 
203 }/* CVC4 namespace */
204 
205 #endif /* __CVC4__SYMBOL_TABLE_H */
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
Definition: kind.h:57
Class encapsulating CVC4 expression types.
Definition: type.h:89
[[ Add one-line brief description here ]]
This is a forward declaration header to declare the CDHashMap<> template.
A convenience class for handling scoped declarations.
Definition: symbol_table.h:48
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
void * Context
expr.h
void * Type
This is a forward declaration header to declare the CDSet<> template.