GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/symbol_table.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

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