CVC4::SymbolTable Class Reference

A convenience class for handling scoped declarations. More...

#include <symbol_table.h>

Public Member Functions
	SymbolTable ()
	Create a symbol table. More...
	~SymbolTable ()
	Destroy a symbol table. More...
void	bind (const std::string &name, Expr obj, bool levelZero=false) throw ()
	Bind an expression to a name in the current scope level. More...
void	bindDefinedFunction (const std::string &name, Expr obj, bool levelZero=false) throw ()
	Bind a function body to a name in the current scope. More...
void	bindType (const std::string &name, Type t, bool levelZero=false) throw ()
	Bind a type to a name in the current scope. More...
void	bindType (const std::string &name, const std::vector< Type > &params, Type t, bool levelZero=false) throw ()
	Bind a type to a name in the current scope. More...
bool	isBound (const std::string &name) const throw ()
	Check whether a name is bound to an expression with either bind() or bindDefinedFunction(). More...
bool	isBoundDefinedFunction (const std::string &name) const throw ()
	Check whether a name was bound to a function with bindDefinedFunction(). More...
bool	isBoundDefinedFunction (Expr func) const throw ()
	Check whether an Expr was bound to a function (i.e., was the second arg to bindDefinedFunction()). More...
bool	isBoundType (const std::string &name) const throw ()
	Check whether a name is bound to a type (or type constructor). More...
Expr	lookup (const std::string &name) const throw ()
	Lookup a bound expression. More...
Type	lookupType (const std::string &name) const throw ()
	Lookup a bound type. More...
Type	lookupType (const std::string &name, const std::vector< Type > &params) const throw ()
	Lookup a bound parameterized type. More...
size_t	lookupArity (const std::string &name)
	Lookup the arity of a bound parameterized type. More...
void	popScope () throw (ScopeException)
	Pop a scope level. More...
void	pushScope () throw ()
	Push a scope level. More...
size_t	getLevel () const throw ()
	Get the current level of this symbol table. More...

Detailed Description

A convenience class for handling scoped declarations.

Implements the usual nested scoping rules for declarations, with separate bindings for expressions and types.

Definition at line 48 of file symbol_table.h.

Constructor & Destructor Documentation

CVC4::SymbolTable::SymbolTable

(

)

Create a symbol table.

CVC4::SymbolTable::~SymbolTable

(

)

Destroy a symbol table.

Member Function Documentation

void CVC4::SymbolTable::bind	(	const std::string &	name,
		Expr	obj,
		bool	levelZero = false
	)
throw	(
	)

Bind an expression to a name in the current scope level.

If name is already bound to an expression in the current level, then the binding is replaced. If name 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.

Parameters

name	an identifier
obj	the expression to bind to name
levelZero	set if the binding must be done at level 0

void CVC4::SymbolTable::bindDefinedFunction	(	const std::string &	name,
		Expr	obj,
		bool	levelZero = false
	)
throw	(
	)

Bind a function body to a name in the current scope.

If name is already bound to an expression in the current level, then the binding is replaced. If name is bound in a previous level, then the binding is "covered" by this one until the current scope is popped. Same as bind() but registers this as a function (so that isBoundDefinedFunction() returns true).

Parameters

name	an identifier
obj	the expression to bind to name
levelZero	set if the binding must be done at level 0

void CVC4::SymbolTable::bindType	(	const std::string &	name,
		Type	t,
		bool	levelZero = false
	)
throw	(
	)

Bind a type to a name in the current scope.

If name is already bound to a type in the current level, then the binding is replaced. If name is bound in a previous level, then the binding is "covered" by this one until the current scope is popped.

Parameters

name	an identifier
t	the type to bind to name
levelZero	set if the binding must be done at level 0

void CVC4::SymbolTable::bindType	(	const std::string &	name,
		const std::vector< Type > &	params,
		Type	t,
		bool	levelZero = false
	)
throw	(
	)

Bind a type to a name in the current scope.

If name is already bound to a type or type constructor in the current level, then the binding is replaced. If name is bound in a previous level, then the binding is "covered" by this one until the current scope is popped.

Parameters

name	an identifier
params	the parameters to the type
t	the type to bind to name
levelZero	true to bind it globally (default is to bind it locally within the current scope)

size_t CVC4::SymbolTable::getLevel	(		)	const
throw	(
	)

Get the current level of this symbol table.

bool CVC4::SymbolTable::isBound	(	const std::string &	name	)	const
throw	(
	)

Check whether a name is bound to an expression with either bind() or bindDefinedFunction().

Parameters

name	the identifier to check.

Returns

true iff name is bound in the current scope.

bool CVC4::SymbolTable::isBoundDefinedFunction	(	const std::string &	name	)	const
throw	(
	)

Check whether a name was bound to a function with bindDefinedFunction().

bool CVC4::SymbolTable::isBoundDefinedFunction	(	Expr	func	)	const
throw	(
	)

Check whether an Expr was bound to a function (i.e., was the second arg to bindDefinedFunction()).

bool CVC4::SymbolTable::isBoundType	(	const std::string &	name	)	const
throw	(
	)

Check whether a name is bound to a type (or type constructor).

Parameters

name	the identifier to check.

Returns

true iff name is bound to a type in the current scope.

Expr CVC4::SymbolTable::lookup	(	const std::string &	name	)	const
throw	(
	)

Lookup a bound expression.

Parameters

name	the identifier to lookup

Returns

the expression bound to name in the current scope.

size_t CVC4::SymbolTable::lookupArity

(

const std::string &

name

)

Lookup the arity of a bound parameterized type.

Type CVC4::SymbolTable::lookupType	(	const std::string &	name	)	const
throw	(
	)

Lookup a bound type.

Parameters

name	the type identifier to lookup

Returns

the type bound to name in the current scope.

Type CVC4::SymbolTable::lookupType	(	const std::string &	name,
		const std::vector< Type > &	params
	)		const
throw	(
	)

Lookup a bound parameterized type.

Parameters

name	the type-constructor identifier to lookup
params	the types to use to parameterize the type

Returns

the type bound to name(params) in the current scope.

void CVC4::SymbolTable::popScope	(		)
throw	(	ScopeException
	)

Pop a scope level.

Deletes all bindings since the last call to pushScope. Calls to pushScope and popScope must be "properly nested." I.e., a call to popScope is only legal if the number of prior calls to pushScope on this SymbolTable is strictly greater than then number of prior calls to popScope.

void CVC4::SymbolTable::pushScope	(		)
throw	(
	)

Push a scope level.

---

The documentation for this class was generated from the following file:

• src/expr/symbol_table.h