SymbLayer Struct Reference

The wide system symbols layer interface. More...

#include <SymbLayer.h>

Related Functions
(Note that these are not member functions.)
boolean	SymbLayer_can_declare_array_define (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new define array can be declared within this layer.
boolean	SymbLayer_can_declare_constant (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new constant can be declared within this layer.
boolean	SymbLayer_can_declare_define (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new DEFINE can be declared within this layer.
boolean	SymbLayer_can_declare_function (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new NFunction can be declared within this layer.
boolean	SymbLayer_can_declare_parameter (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new parameter can be declared within this layer.
boolean	SymbLayer_can_declare_var (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new variable can be declared within this layer.
boolean	SymbLayer_can_declare_variable_array (const SymbLayer_ptr self, const node_ptr name)
	Call this method to know if a new variable_array can be declared within this layer.
void	SymbLayer_committed_to_enc (SymbLayer_ptr self)
	Called every time an instance is committed within an encoding.
SymbLayer_ptr	SymbLayer_create (const char *name, const LayerInsertPolicy policy, SymbCache_ptr cache)
	Private interface accessed by class SymbTable.
void	SymbLayer_declare_array_define (SymbLayer_ptr self, node_ptr name, node_ptr ctx, node_ptr definition)
	Insert a new array define array.
void	SymbLayer_declare_constant (SymbLayer_ptr self, node_ptr name)
	Insert a new constant.
void	SymbLayer_declare_define (SymbLayer_ptr self, node_ptr name, node_ptr ctx, node_ptr definition)
	Insert a new DEFINE.
void	SymbLayer_declare_frozen_var (SymbLayer_ptr self, node_ptr var, SymbType_ptr type)
	Insert a new frozen variable.
void	SymbLayer_declare_function (SymbLayer_ptr self, node_ptr name, node_ptr ctx, SymbType_ptr type)
	Insert a new NFunction.
void	SymbLayer_declare_input_var (SymbLayer_ptr self, node_ptr var, SymbType_ptr type)
	Insert a new input variable.
void	SymbLayer_declare_parameter (SymbLayer_ptr self, node_ptr formal, node_ptr ctx, node_ptr actual)
	Insert a new formal parameters.
void	SymbLayer_declare_state_var (SymbLayer_ptr self, node_ptr var, SymbType_ptr type)
	Insert a new state variable.
void	SymbLayer_declare_variable_array (SymbLayer_ptr self, node_ptr var, SymbType_ptr type)
	Insert a new symbol-type association, i.e. array var.
void	SymbLayer_destroy (SymbLayer_ptr self)
	Class SymbLayer destructor.
void	SymbLayer_destroy_raw (SymbLayer_ptr self)
	Class SymbLayer destructor.
void	SymbLayer_gen_iter (const SymbLayer_ptr self, SymbLayerIter *iter, unsigned int mask)
	Generates an interator over the Symbol Cache symbols.
int	SymbLayer_get_array_defines_num (const SymbLayer_ptr self)
	Returns the number of define arrays.
int	SymbLayer_get_bool_frozen_vars_num (const SymbLayer_ptr self)
	Returns the number of declared boolean frozen variables.
int	SymbLayer_get_bool_input_vars_num (const SymbLayer_ptr self)
	Returns the number of declared boolean input variables.
int	SymbLayer_get_bool_state_vars_num (const SymbLayer_ptr self)
	Returns the number of declared boolean state variables.
int	SymbLayer_get_constants_num (const SymbLayer_ptr self)
	Returns the number of declared contants.
int	SymbLayer_get_defines_num (const SymbLayer_ptr self)
	Returns the number of DEFINEs.
NuSMVEnv_ptr	SymbLayer_get_environment (const SymbLayer_ptr self)
	SymbLayer environment instance getter.
int	SymbLayer_get_frozen_vars_num (const SymbLayer_ptr self)
	Returns the number of declared frozen variables.
int	SymbLayer_get_functions_num (const SymbLayer_ptr self)
	Returns the number of NFunctions.
int	SymbLayer_get_input_vars_num (const SymbLayer_ptr self)
	Returns the number of declared input variables.
LayerInsertPolicy	SymbLayer_get_insert_policy (const SymbLayer_ptr self)
	Returns the policy that must be adopted to stack this layer into a layers stack, within a SymbTable instance.
const char *	SymbLayer_get_name (const SymbLayer_ptr self)
	Returns the name self had been registered with.
int	SymbLayer_get_parameters_num (const SymbLayer_ptr self)
	Returns the number of parameters.
int	SymbLayer_get_state_vars_num (const SymbLayer_ptr self)
	Returns the number of declared state variables.
int	SymbLayer_get_symbols_num (const SymbLayer_ptr self)
	Returns the number of declared symbols.
int	SymbLayer_get_variable_arrays_num (const SymbLayer_ptr self)
	Returns the number of Symbol Types.
int	SymbLayer_get_vars_num (const SymbLayer_ptr self)
	Returns the number of declared variables.
boolean	SymbLayer_is_symbol_in_layer (SymbLayer_ptr self, node_ptr name)
boolean	SymbLayer_is_variable_in_layer (SymbLayer_ptr self, node_ptr name)
unsigned int	SymbLayer_iter_count (const SymbLayer_ptr self, SymbLayerIter iter)
	Counts the elements of the iterator.
boolean	SymbLayer_iter_filter_bool_vars (const SymbLayer_ptr self, const node_ptr sym, void *arg)
	Boolean Variables filter.
node_ptr	SymbLayer_iter_get_symbol (const SymbLayer_ptr self, const SymbLayerIter *iter)
	Get the symbol pointed by the iterator.
boolean	SymbLayer_iter_is_end (const SymbLayer_ptr self, const SymbLayerIter *iter)
	Checks if the iterator is at it's end.
void	SymbLayer_iter_next (const SymbLayer_ptr self, SymbLayerIter *iter)
	Moves the iterator over the next symbol.
NodeList_ptr	SymbLayer_iter_to_list (const SymbLayer_ptr self, SymbLayerIter iter)
	Generates a list starting from the given iterator.
Set_t	SymbLayer_iter_to_set (const SymbLayer_ptr self, SymbLayerIter iter)
	Generates a set starting from the given iterator.
boolean	SymbLayer_must_insert_before (const SymbLayer_ptr self, const SymbLayer_ptr other)
void	SymbLayer_redeclare_state_as_frozen_var (SymbLayer_ptr self, node_ptr var)
	Redeclare a state variable as a frozen variable.
void	SymbLayer_remove_define (SymbLayer_ptr self, node_ptr name)
	Removes a previously declared DEFINE.
void	SymbLayer_remove_function (SymbLayer_ptr self, node_ptr name)
	Removes a previously declared NFunction.
void	SymbLayer_remove_symbol (SymbLayer_ptr self, node_ptr name)
	Removes a symbol previously delcared.
void	SymbLayer_remove_var (SymbLayer_ptr self, node_ptr name)
	Removes a variable previously delcared.
void	SymbLayer_remove_variable_array (SymbLayer_ptr self, node_ptr name)
	Removes a previously declared array.
void	SymbLayer_removed_from_enc (SymbLayer_ptr self)
	Called every time an instance is removed from an encoding.
void	SymbLayer_set_name (SymbLayer_ptr self, const char *new_name)
	Sets the layer name.

---

Detailed Description

The wide system symbols layer interface.

Author:

Roberto Cavada This is the public interface of the class SymbLayer

Public type accessor for class SymbLayer See the description of class SymbLayer for further information.

---

Friends And Related Function Documentation

boolean SymbLayer_can_declare_array_define	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new define array can be declared within this layer.

Returns true if the given symbol does not exist within the symbol table which self belongs to. Returns false if the symbol was already declared.

boolean SymbLayer_can_declare_constant	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new constant can be declared within this layer.

Since more than one layer can declare the same constants, this method might return true even if another layer already contain the given constant. If the constant had already been declared within self, false is returned.

boolean SymbLayer_can_declare_define	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new DEFINE can be declared within this layer.

Returns true if the given symbol does not exist within the symbol table which self belongs to. Returns false if the symbol was already declared.

boolean SymbLayer_can_declare_function	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new NFunction can be declared within this layer.

Returns true if the given symbol does not exist within the symbol table which self belongs to. Returns false if the symbol was already declared.

boolean SymbLayer_can_declare_parameter	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new parameter can be declared within this layer.

Returns true if the given symbol does not exist within the symbol table which self belongs to. Returns false if the symbol was already declared.

boolean SymbLayer_can_declare_var	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new variable can be declared within this layer.

Returns true if the given symbol does not exist within the symbol table which self belongs to. Returns false if the symbol was already declared.

boolean SymbLayer_can_declare_variable_array	(	const SymbLayer_ptr	self,
		const node_ptr	name
	)			[related]

Call this method to know if a new variable_array can be declared within this layer.

Returns true if the given symbol does not exist within the symbol table which self belongs to. Returns false if the symbol was already declared.

void SymbLayer_committed_to_enc

(

SymbLayer_ptr

self

)

[related]

Called every time an instance is committed within an encoding.

This method is part of a private registration protocol between encodings and layers, and must be considered as a private method. Every time a layer is registered (committed) within an enconding, the layer is notified with a call to this method from the encoding instance which the layer is committed to. This mechanism helps to detect errors when a layer in use by an encoding is removed and destroyed from within a symbol table. The destructor will always check that self is not in use by any encoding when it is invoked.

See also:

removed_from_enc

SymbLayer_ptr SymbLayer_create	(	const char *	name,
		const LayerInsertPolicy	policy,
		SymbCache_ptr	cache
	)			[related]

Private interface accessed by class SymbTable.

Author:

Roberto Cavada

Todo:

: Missing description

Class SymbLayer constructor name is copied, the caller keeps ownership of cache.

void SymbLayer_declare_array_define	(	SymbLayer_ptr	self,
		node_ptr	name,
		node_ptr	ctx,
		node_ptr	definition
	)			[related]

Insert a new array define array.

A new define array of a given value is created. name must be contestualized, context is provided as a separated information

void SymbLayer_declare_constant	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Insert a new constant.

A new constant is created

See also:

SymbLayer_can_declare_constant

void SymbLayer_declare_define	(	SymbLayer_ptr	self,
		node_ptr	name,
		node_ptr	ctx,
		node_ptr	definition
	)			[related]

Insert a new DEFINE.

A new DEFINE of a given value is created. name must be contestualized, context is provided as a separated information

void SymbLayer_declare_frozen_var	(	SymbLayer_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Insert a new frozen variable.

A new frozen variable is created of a given type. The variable type can be created with SymbType_create or returned by funtions SymbTablePkg_..._type. The layer is responsible for destroying the variable's type.

void SymbLayer_declare_function	(	SymbLayer_ptr	self,
		node_ptr	name,
		node_ptr	ctx,
		SymbType_ptr	type
	)			[related]

Insert a new NFunction.

A new NFunction is declared within the layer. Name must be contestualized, context is provided as a separated information

See also:

SymbLayer_can_declare_function

void SymbLayer_declare_input_var	(	SymbLayer_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Insert a new input variable.

A new input variable is created of a given type. The variable type can be created with SymbType_create or returned by funtions SymbTablePkg_..._type. The layer is responsible for destroying the variable's type.

void SymbLayer_declare_parameter	(	SymbLayer_ptr	self,
		node_ptr	formal,
		node_ptr	ctx,
		node_ptr	actual
	)			[related]

Insert a new formal parameters.

A new parameter of a given value is created. name must be contestualized, context is provided as a separated information

void SymbLayer_declare_state_var	(	SymbLayer_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Insert a new state variable.

A new state variable is created of a given type. The variable type can be created with SymbType_create or returned by funtions SymbTablePkg_..._type. The layer is responsible for destroying the variable's type.

void SymbLayer_declare_variable_array	(	SymbLayer_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Insert a new symbol-type association, i.e. array var.

The specified name will be associated to the give array type in the symbols collection

void SymbLayer_destroy

(

SymbLayer_ptr

self

)

[related]

Class SymbLayer destructor.

Use this destructor if the SymbCache will not be destroyed after this call (ie. You are removing a layer from the Symbol Table)

void SymbLayer_destroy_raw

(

SymbLayer_ptr

self

)

[related]

Class SymbLayer destructor.

Use this destructor if the SymbCache will be destroyed after this call (ie. You are destroying the Symbol Table)

void SymbLayer_gen_iter	(	const SymbLayer_ptr	self,
		SymbLayerIter *	iter,
		unsigned int	mask
	)			[related]

Generates an interator over the Symbol Cache symbols.

Generates an interator over the Symbol Cache symbols. The iterator will ignore all symbols that do not satisfy the mask

int SymbLayer_get_array_defines_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of define arrays.

int SymbLayer_get_bool_frozen_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared boolean frozen variables.

int SymbLayer_get_bool_input_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared boolean input variables.

int SymbLayer_get_bool_state_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared boolean state variables.

int SymbLayer_get_constants_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared contants.

int SymbLayer_get_defines_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of DEFINEs.

NuSMVEnv_ptr SymbLayer_get_environment

(

const SymbLayer_ptr

self

)

[related]

SymbLayer environment instance getter.

SymbLayer environment instance getter

int SymbLayer_get_frozen_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared frozen variables.

int SymbLayer_get_functions_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of NFunctions.

int SymbLayer_get_input_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared input variables.

LayerInsertPolicy SymbLayer_get_insert_policy

(

const SymbLayer_ptr

self

)

[related]

Returns the policy that must be adopted to stack this layer into a layers stack, within a SymbTable instance.

This method is thought to be used exclusively by class SymbTable

const char * SymbLayer_get_name

(

const SymbLayer_ptr

self

)

[related]

Returns the name self had been registered with.

Returned string must not be freed, it belongs to self

int SymbLayer_get_parameters_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of parameters.

int SymbLayer_get_state_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared state variables.

int SymbLayer_get_symbols_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared symbols.

int SymbLayer_get_variable_arrays_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of Symbol Types.

int SymbLayer_get_vars_num

(

const SymbLayer_ptr

self

)

[related]

Returns the number of declared variables.

boolean SymbLayer_is_symbol_in_layer	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Returns true if the symbol is defined in the layer.

boolean SymbLayer_is_variable_in_layer	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Returns true if the variable is defined in the layer.

unsigned int SymbLayer_iter_count	(	const SymbLayer_ptr	self,
		SymbLayerIter	iter
	)			[related]

Counts the elements of the iterator.

Counts the elements of the iterator. The iter will not be consumed (since passed as copy)

boolean SymbLayer_iter_filter_bool_vars	(	const SymbLayer_ptr	self,
		const node_ptr	sym,
		void *	arg
	)			[related]

Boolean Variables filter.

SymbLayer built-in filter: Returns true iff the symbol is a boolean variable

node_ptr SymbLayer_iter_get_symbol	(	const SymbLayer_ptr	self,
		const SymbLayerIter *	iter
	)			[related]

Get the symbol pointed by the iterator.

Get the symbol pointed by the iterator

boolean SymbLayer_iter_is_end	(	const SymbLayer_ptr	self,
		const SymbLayerIter *	iter
	)			[related]

Checks if the iterator is at it's end.

Checks if the iterator is at it's end

void SymbLayer_iter_next	(	const SymbLayer_ptr	self,
		SymbLayerIter *	iter
	)			[related]

Moves the iterator over the next symbol.

Moves the iterator over the next symbol, regarding to the mask given when built using SymbCache_gen_iter

NodeList_ptr SymbLayer_iter_to_list	(	const SymbLayer_ptr	self,
		SymbLayerIter	iter
	)			[related]

Generates a list starting from the given iterator.

Generates a list starting from the given iterator. The iter will not be consumed (since passed as copy)

Set_t SymbLayer_iter_to_set	(	const SymbLayer_ptr	self,
		SymbLayerIter	iter
	)			[related]

Generates a set starting from the given iterator.

Generates a set starting from the given iterator. The iter will not be consumed (since passed as copy)

boolean SymbLayer_must_insert_before	(	const SymbLayer_ptr	self,
		const SymbLayer_ptr	other
	)			[related]

Compares the insertion policies of self and other, and returns true if self must be inserted *before* other.

void SymbLayer_redeclare_state_as_frozen_var	(	SymbLayer_ptr	self,
		node_ptr	var
	)			[related]

Redeclare a state variable as a frozen variable.

A variable is frozen if it is known then the var's value cannot change in transitions. 'var' must be a state variable already defined and not redeclared as frozen.

void SymbLayer_remove_define	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Removes a previously declared DEFINE.

This method can be called only if self is not currently commited to any encoding. It is not allowed to remove symbols from layers that are committed to any encoder. This is required as caches and other mechanisms may fail to work correctly otherwise.

void SymbLayer_remove_function	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Removes a previously declared NFunction.

This method can be called only if self is not currently commited to any encoding. It is not allowed to remove symbols from layers that are committed to any encoder. This is required as caches and other mechanisms may fail to work correctly otherwise.

void SymbLayer_remove_symbol	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Removes a symbol previously delcared.

Symbol must be a var, a variable array, a define or a function

This method can be called only if self is not currently commited to any encoding. It is not allowed to remove symbols from layers that are committed to any encoder. This is required as caches and other mechanisms may fail to work correctly otherwise.

void SymbLayer_remove_var	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Removes a variable previously delcared.

This method can be called only if self is not currently commited to any encoding. It is not allowed to remove symbols from layers that are committed to any encoder. This is required as caches and other mechanisms may fail to work correctly otherwise.

void SymbLayer_remove_variable_array	(	SymbLayer_ptr	self,
		node_ptr	name
	)			[related]

Removes a previously declared array.

This method can be called only if self is not currently commited to any encoding. It is not allowed to remove symbols from layers that are committed to any encoder. This is required as caches and other mechanisms may fail to work correctly otherwise.

void SymbLayer_removed_from_enc

(

SymbLayer_ptr

self

)

[related]

Called every time an instance is removed from an encoding.

This method is part of a private registration protocol between encodings and layers, and must be considered as a private method. Every time a layer is removed (uncommitted) from an enconding, the layer is notified with a call to this method from the encoding instance which the layer is being removed from. This mechanism helps to detect errors when a layer in use by an encoding is removed and destroyed from within a symbol table. The destructor will always check that self is not in use by any encoding when it is invoked.

See also:

commit_to_enc

void SymbLayer_set_name	(	SymbLayer_ptr	self,
		const char *	new_name
	)			[related]

Sets the layer name.

This method is protected (not usable by users, only used by the symbol table when renaming a layer

---

The documentation for this struct was generated from the following files:

• NuSMV/code/nusmv/core/compile/symb_table/SymbLayer.h
• NuSMV/code/nusmv/core/compile/symb_table/SymbLayer_private.h