1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Morgan Deters, Christopher L. Conway
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Convenience class for scoping variable and type declarations.
16 #include "cvc5_public.h"
18 #ifndef CVC5__SYMBOL_TABLE_H
19 #define CVC5__SYMBOL_TABLE_H
25 #include "base/exception.h"
26 #include "cvc5_export.h"
36 class CVC5_EXPORT ScopeException
: public Exception
41 * A convenience class for handling scoped declarations. Implements the usual
42 * nested scoping rules for declarations, with separate bindings for expressions
45 class CVC5_EXPORT SymbolTable
48 /** Create a symbol table. */
53 * Bind an expression to a name in the current scope level.
55 * When doOverload is false:
56 * if <code>name</code> is already bound to an expression in the current
57 * level, then the binding is replaced. If <code>name</code> is bound
58 * in a previous level, then the binding is "covered" by this one
59 * until the current scope is popped.
60 * If levelZero is true the name shouldn't be already bound.
62 * When doOverload is true:
63 * if <code>name</code> is already bound to an expression in the current
64 * level, then we mark the previous bound expression and obj as overloaded
67 * @param name an identifier
68 * @param obj the expression to bind to <code>name</code>
69 * @param levelZero set if the binding must be done at level 0
70 * @param doOverload set if the binding can overload the function name.
72 * Returns false if the binding was invalid.
74 bool bind(const std::string
& name
,
76 bool levelZero
= false,
77 bool doOverload
= false);
80 * Bind a type to a name in the current scope. If <code>name</code>
81 * is already bound to a type in the current level, then the binding
82 * is replaced. If <code>name</code> is bound in a previous level,
83 * then the binding is "covered" by this one until the current scope
86 * @param name an identifier
87 * @param t the type to bind to <code>name</code>
88 * @param levelZero set if the binding must be done at level 0
90 void bindType(const std::string
& name
, api::Sort t
, bool levelZero
= false);
93 * Bind a type to a name in the current scope. If <code>name</code>
94 * is already bound to a type or type constructor in the current
95 * level, then the binding is replaced. If <code>name</code> is
96 * bound in a previous level, then the binding is "covered" by this
97 * one until the current scope is popped.
99 * @param name an identifier
100 * @param params the parameters to the type
101 * @param t the type to bind to <code>name</code>
102 * @param levelZero true to bind it globally (default is to bind it
103 * locally within the current scope)
105 void bindType(const std::string
& name
,
106 const std::vector
<api::Sort
>& params
,
108 bool levelZero
= false);
111 * Check whether a name is bound to an expression with bind().
113 * @param name the identifier to check.
114 * @returns true iff name is bound in the current scope.
116 bool isBound(const std::string
& name
) const;
119 * Check whether a name is bound to a type (or type constructor).
121 * @param name the identifier to check.
122 * @returns true iff name is bound to a type in the current scope.
124 bool isBoundType(const std::string
& name
) const;
127 * Lookup a bound expression.
129 * @param name the identifier to lookup
130 * @returns the unique expression bound to <code>name</code> in the current
132 * It returns the null expression if there is not a unique expression bound to
133 * <code>name</code> in the current scope (i.e. if there is not exactly one).
135 api::Term
lookup(const std::string
& name
) const;
138 * Lookup a bound type.
140 * @param name the type identifier to lookup
141 * @returns the type bound to <code>name</code> in the current scope.
143 api::Sort
lookupType(const std::string
& name
) const;
146 * Lookup a bound parameterized type.
148 * @param name the type-constructor identifier to lookup
149 * @param params the types to use to parameterize the type
150 * @returns the type bound to <code>name(<i>params</i>)</code> in
153 api::Sort
lookupType(const std::string
& name
,
154 const std::vector
<api::Sort
>& params
) const;
157 * Lookup the arity of a bound parameterized type.
159 size_t lookupArity(const std::string
& name
);
162 * Pop a scope level, deletes all bindings since the last call to pushScope,
163 * and decreases the level by 1.
165 * @throws ScopeException if the scope level is 0.
169 /** Push a scope level and increase the scope level by 1. */
172 /** Get the current level of this symbol table. */
173 size_t getLevel() const;
175 /** Reset everything. */
177 /** Reset assertions. */
178 void resetAssertions();
180 //------------------------ operator overloading
181 /** is this function overloaded? */
182 bool isOverloadedFunction(api::Term fun
) const;
184 /** Get overloaded constant for type.
185 * If possible, it returns the defined symbol with name
186 * that has type t. Otherwise returns null expression.
188 api::Term
getOverloadedConstantForType(const std::string
& name
,
192 * If possible, returns the unique defined function for a name
193 * that expects arguments with types "argTypes".
194 * For example, if argTypes = (T1, ..., Tn), then this may return an
195 * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
197 * If there is not a unique defined function for the name and argTypes,
198 * this returns the null expression. This can happen either if there are
199 * no functions with name and expected argTypes, or alternatively there is
200 * more than one function with name and expected argTypes.
202 api::Term
getOverloadedFunctionForTypes(
203 const std::string
& name
, const std::vector
<api::Sort
>& argTypes
) const;
204 //------------------------ end operator overloading
207 /** The implementation of the symbol table */
208 class Implementation
;
209 std::unique_ptr
<Implementation
> d_implementation
;
210 }; /* class SymbolTable */
214 #endif /* CVC5__SYMBOL_TABLE_H */