cvc4-1.4
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

◆ SymbolTable()

CVC4::SymbolTable::SymbolTable ( )

Create a symbol table.

◆ ~SymbolTable()

CVC4::SymbolTable::~SymbolTable ( )

Destroy a symbol table.

Member Function Documentation

◆ bind()

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
namean identifier
objthe expression to bind to name
levelZeroset if the binding must be done at level 0

◆ bindDefinedFunction()

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
namean identifier
objthe expression to bind to name
levelZeroset if the binding must be done at level 0

◆ bindType() [1/2]

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
namean identifier
tthe type to bind to name
levelZeroset if the binding must be done at level 0

◆ bindType() [2/2]

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
namean identifier
paramsthe parameters to the type
tthe type to bind to name
levelZerotrue to bind it globally (default is to bind it locally within the current scope)

◆ getLevel()

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

Get the current level of this symbol table.

Referenced by CVC4::parser::Parser::scopeLevel().

◆ isBound()

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
namethe identifier to check.
Returns
true iff name is bound in the current scope.

◆ isBoundDefinedFunction() [1/2]

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

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

◆ isBoundDefinedFunction() [2/2]

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()).

◆ isBoundType()

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

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

Parameters
namethe identifier to check.
Returns
true iff name is bound to a type in the current scope.

◆ lookup()

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

Lookup a bound expression.

Parameters
namethe identifier to lookup
Returns
the expression bound to name in the current scope.

◆ lookupArity()

size_t CVC4::SymbolTable::lookupArity ( const std::string &  name)

Lookup the arity of a bound parameterized type.

◆ lookupType() [1/2]

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

Lookup a bound type.

Parameters
namethe type identifier to lookup
Returns
the type bound to name in the current scope.

◆ lookupType() [2/2]

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

Lookup a bound parameterized type.

Parameters
namethe type-constructor identifier to lookup
paramsthe types to use to parameterize the type
Returns
the type bound to name(params) in the current scope.

◆ popScope()

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.

Referenced by CVC4::parser::Parser::popScope().

◆ pushScope()

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

Push a scope level.

Referenced by CVC4::parser::Parser::pushScope().


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