1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
|
/********************* */
/*! \file symbol_table.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Christopher L. Conway
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Convenience class for scoping variable and type declarations.
**
** Convenience class for scoping variable and type declarations.
**/
#include "cvc4_public.h"
#ifndef CVC4__SYMBOL_TABLE_H
#define CVC4__SYMBOL_TABLE_H
#include <memory>
#include <string>
#include <vector>
#include "base/exception.h"
#include "cvc4_export.h"
namespace CVC4 {
namespace api {
class Solver;
class Sort;
class Term;
} // namespace api
class CVC4_EXPORT ScopeException : public Exception
{
};
/**
* A convenience class for handling scoped declarations. Implements the usual
* nested scoping rules for declarations, with separate bindings for expressions
* and types.
*/
class CVC4_EXPORT SymbolTable
{
public:
/** Create a symbol table. */
SymbolTable();
~SymbolTable();
/**
* Bind an expression to a name in the current scope level.
*
* 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.
*
* @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 bind(const std::string& name,
api::Term 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,
* then the binding is "covered" by this one until the current scope
* is popped.
*
* @param name an identifier
* @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, api::Sort t, bool levelZero = false);
/**
* Bind a type to a name in the current scope. If <code>name</code>
* is already bound to a type or type constructor 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.
*
* @param name an identifier
* @param params the parameters to the type
* @param t the type to bind to <code>name</code>
* @param levelZero true to bind it globally (default is to bind it
* locally within the current scope)
*/
void bindType(const std::string& name,
const std::vector<api::Sort>& params,
api::Sort t,
bool levelZero = false);
/**
* 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.
*/
bool isBound(const std::string& name) const;
/**
* Check whether a name is bound to a type (or type constructor).
*
* @param name the identifier to check.
* @returns true iff name is bound to a type in the current scope.
*/
bool isBoundType(const std::string& name) const;
/**
* Lookup a bound expression.
*
* @param name the identifier to lookup
* @returns the unique expression bound to <code>name</code> in the current
* scope.
* 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).
*/
api::Term lookup(const std::string& name) const;
/**
* Lookup a bound type.
*
* @param name the type identifier to lookup
* @returns the type bound to <code>name</code> in the current scope.
*/
api::Sort lookupType(const std::string& name) const;
/**
* Lookup a bound parameterized type.
*
* @param name the type-constructor identifier to lookup
* @param params the types to use to parameterize the type
* @returns the type bound to <code>name(<i>params</i>)</code> in
* the current scope.
*/
api::Sort lookupType(const std::string& name,
const std::vector<api::Sort>& params) const;
/**
* Lookup the arity of a bound parameterized type.
*/
size_t lookupArity(const std::string& name);
/**
* Pop a scope level, deletes all bindings since the last call to pushScope,
* and decreases the level by 1.
*
* @throws ScopeException if the scope level is 0.
*/
void popScope();
/** Push a scope level and increase the scope level by 1. */
void pushScope();
/** Get the current level of this symbol table. */
size_t getLevel() const;
/** Reset everything. */
void reset();
/** Reset assertions. */
void resetAssertions();
//------------------------ operator overloading
/** is this function overloaded? */
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.
*/
api::Term getOverloadedConstantForType(const std::string& name,
api::Sort t) const;
/**
* If possible, returns the unique defined function for a name
* that expects arguments with types "argTypes".
* For example, if argTypes = (T1, ..., Tn), then this may return an
* expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
*
* If there is not a unique defined function for the name and argTypes,
* this returns the null expression. This can happen either if there are
* no functions with name and expected argTypes, or alternatively there is
* more than one function with name and expected argTypes.
*/
api::Term getOverloadedFunctionForTypes(
const std::string& name, const std::vector<api::Sort>& argTypes) const;
//------------------------ end operator overloading
private:
/** The implementation of the symbol table */
class Implementation;
std::unique_ptr<Implementation> d_implementation;
}; /* class SymbolTable */
} // namespace CVC4
#endif /* CVC4__SYMBOL_TABLE_H */
|
