cvc4-1.3
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:226
Class encapsulating CVC4 expression types.
Definition: type.h:88
[[ Add one-line brief description here ]]
This is a forward declaration header to declare the CDHashMap<> template.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
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.