SymbCache Struct Reference

The public interface of class SymbCache. More...

#include <SymbCache.h>

Related Functions
(Note that these are not member functions.)
void	SymbCache_add_trigger (const SymbCache_ptr self, SymbTableTriggerFun trigger, SymbTableTriggerAction action, void *arg1, boolean must_free_arg)
	Adds a trigger to the symbol cache.
SymbCache_ptr	SymbCache_create (SymbTable_ptr symb_table, NuSMVEnv_ptr env)
	The SymbCache class private interface.
void	SymbCache_destroy (SymbCache_ptr self)
	Class destructor.
void	SymbCache_gen_iter (const SymbCache_ptr self, SymbTableIter *iter, const unsigned int mask)
	Generates an interator over the Symbol Cache symbols.
node_ptr	SymbCache_get_actual_parameter (const SymbCache_ptr self, const node_ptr name)
	Returns the actual param of the given formal parameter.
node_ptr	SymbCache_get_actual_parameter_context (const SymbCache_ptr self, const node_ptr name)
	Returns the context of the actual parameter associated with the given formal parameter.
node_ptr	SymbCache_get_array_define_body (const SymbCache_ptr self, const node_ptr name)
	Returns the body of the given define array name.
node_ptr	SymbCache_get_array_define_context (const SymbCache_ptr self, const node_ptr name)
	Returns the context of the given define array name.
int	SymbCache_get_array_defines_num (const SymbCache_ptr self)
	Returns the number of define arrays.
int	SymbCache_get_constants_num (const SymbCache_ptr self)
	Returns the number of declared contants.
node_ptr	SymbCache_get_define_body (const SymbCache_ptr self, const node_ptr name)
	Returns the body of the given DEFINE name.
node_ptr	SymbCache_get_define_context (const SymbCache_ptr self, const node_ptr name)
	Returns the context of the given DEFINE name.
node_ptr	SymbCache_get_define_flatten_body (const SymbCache_ptr self, const node_ptr name)
	Returns the flattenized body of the given DEFINE name.
int	SymbCache_get_defines_num (const SymbCache_ptr self)
	Returns the number of DEFINEs.
NuSMVEnv_ptr	SymbCache_get_environment (const SymbCache_ptr self)
	SymbCache environment instance getter.
node_ptr	SymbCache_get_flatten_actual_parameter (const SymbCache_ptr self, const node_ptr name)
	Returns the flattenized actual parameter of the given formal parameter.
int	SymbCache_get_frozen_vars_num (const SymbCache_ptr self)
	Returns the number of declared frozen variables.
node_ptr	SymbCache_get_function_context (const SymbCache_ptr self, const node_ptr name)
	Returns the context of the given NFunction.
SymbType_ptr	SymbCache_get_function_type (const SymbCache_ptr self, const node_ptr name)
	Returns the type of a function.
int	SymbCache_get_functions_num (const SymbCache_ptr self)
	Returns the number of NFunctions.
int	SymbCache_get_input_vars_num (const SymbCache_ptr self)
	Returns the number of declared input variables.
int	SymbCache_get_parameters_num (const SymbCache_ptr self)
	Returns the number of parameters.
int	SymbCache_get_state_vars_num (const SymbCache_ptr self)
	Returns the number of declared state variables.
SymbTableType	SymbCache_get_symbol_type (const SymbCache_ptr self, const node_ptr symbol)
	Get the symbol type.
int	SymbCache_get_symbols_num (const SymbCache_ptr self)
	Returns the number of symbols.
SymbType_ptr	SymbCache_get_var_type (const SymbCache_ptr self, const node_ptr name)
	Returns the type of a given variable.
SymbType_ptr	SymbCache_get_variable_array_type (const SymbCache_ptr self, const node_ptr name)
	Returns the type of array variable, i.e. of variable_array.
int	SymbCache_get_variable_arrays_num (const SymbCache_ptr self)
	Returns the number of Symbol Types.
boolean	SymbCache_is_iter_end (const SymbCache_ptr self, const SymbTableIter *iter)
	Checks if the iterator is at it's end.
boolean	SymbCache_is_symbol_array_define (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a declared define array.
boolean	SymbCache_is_symbol_constant (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a declared constant.
boolean	SymbCache_is_symbol_declared (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is declared.
boolean	SymbCache_is_symbol_define (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a declared DEFINE.
boolean	SymbCache_is_symbol_frozen_var (const SymbCache_ptr self, const node_ptr name)
	Returns true if the variable is frozen.
boolean	SymbCache_is_symbol_function (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a declared NFunction.
boolean	SymbCache_is_symbol_input_var (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is an input variable.
boolean	SymbCache_is_symbol_parameter (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a declared formal parameter.
boolean	SymbCache_is_symbol_state_frozen_var (const SymbCache_ptr self, const node_ptr name)
	Returns true if the variable is a frozen or a state variable.
boolean	SymbCache_is_symbol_state_var (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a state variable.
boolean	SymbCache_is_symbol_var (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is either a state, a frozen or an input variable.
boolean	SymbCache_is_symbol_variable_array (const SymbCache_ptr self, const node_ptr name)
	Returns true if the given symbol is a declared variable array.
node_ptr	SymbCache_iter_get_symbol (const SymbCache_ptr self, const SymbTableIter *iter)
	Get the symbol pointed by the iterator.
void	SymbCache_iter_set_filter (const SymbCache_ptr self, SymbTableIter *iter, SymbTableIterFilterFun filter, void *arg)
	Sets the filter for an interator over the Symbol Cache symbols.
boolean	SymbCache_list_contains_input_var (const SymbCache_ptr self, const NodeList_ptr var_list)
	Returns true if var_list contains at least one input variable.
boolean	SymbCache_list_contains_state_frozen_var (const SymbCache_ptr self, const NodeList_ptr var_list)
	Returns true if var_list contains at least one state or frozen variable.
boolean	SymbCache_list_contains_undef_var (const SymbCache_ptr self, const NodeList_ptr var_list)
	Returns true if the given symbols list contains one or more undeclared variable names.
void	SymbCache_new_array_define (SymbCache_ptr self, node_ptr name, node_ptr ctx, node_ptr definition)
	Declares a new define array.
void	SymbCache_new_constant (SymbCache_ptr self, node_ptr name)
	Declares a new constant.
void	SymbCache_new_define (SymbCache_ptr self, node_ptr name, node_ptr context, node_ptr definition)
	Declares a new DEFINE.
void	SymbCache_new_frozen_var (SymbCache_ptr self, node_ptr var, SymbType_ptr type)
	Declares a new frozen variable.
void	SymbCache_new_function (SymbCache_ptr self, node_ptr name, node_ptr context, SymbType_ptr type)
	Declares a new NFunction.
void	SymbCache_new_input_var (SymbCache_ptr self, node_ptr var, SymbType_ptr type)
	Declares a new input variable.
void	SymbCache_new_parameter (SymbCache_ptr self, node_ptr formal, node_ptr context, node_ptr actual)
	Declares a new module parameter.
void	SymbCache_new_state_var (SymbCache_ptr self, node_ptr var, SymbType_ptr type)
	Declares a new state variable.
void	SymbCache_new_variable_array (SymbCache_ptr self, node_ptr name, SymbType_ptr type)
	Declares a new ARRAY var.
void	SymbCache_next_iter (const SymbCache_ptr self, SymbTableIter *iter)
	Moves the iterator over the next symbol.
void	SymbCache_redeclare_state_as_frozen_var (SymbCache_ptr self, node_ptr var)
	Redeclare a state variable as a frozen variable.
void	SymbCache_remove_constant (SymbCache_ptr self, node_ptr constant)
	Removes a constant from the cache of symbols, and from the flattener module.
void	SymbCache_remove_define (SymbCache_ptr self, node_ptr define)
	Removes a DEFINE from the cache of symbols, and from the flattener define hash.
void	SymbCache_remove_function (SymbCache_ptr self, node_ptr name)
	Removes an NFunction from the cache of symbols.
void	SymbCache_remove_parameter (SymbCache_ptr self, node_ptr formal)
	Removes a parameter from the cache of symbols.
void	SymbCache_remove_symbols (SymbCache_ptr self, const node_ptr *symbols, const unsigned int size)
	Removes all the symbols in the array.
void	SymbCache_remove_trigger (const SymbCache_ptr self, SymbTableTriggerFun trigger, SymbTableTriggerAction action)
	Removes a trigger from the symbol cache.
void	SymbCache_remove_var (SymbCache_ptr self, node_ptr var)
	Removes a variable from the cache of symbols, and from the flattener module.
void	SymbCache_remove_variable_array (SymbCache_ptr self, node_ptr symbol)
	Removes a variable array from the cache of symbols.

---

Detailed Description

The public interface of class SymbCache.

Author:

Roberto Cavada

Todo:

: Missing description

The SymbCache type An instance of class SymbCache is hold by each instance of SymbTable. This means that the life cycle of a SymbCache is never managed by the user. Furthermore, only tests on symbols are allowed to be performed by the user. All other features (e.g. creation of new symbols) are performed by SymbLayers and by SymbTable, by using a private interface

---

Friends And Related Function Documentation

void SymbCache_add_trigger	(	const SymbCache_ptr	self,
		SymbTableTriggerFun	trigger,
		SymbTableTriggerAction	action,
		void *	arg1,
		boolean	must_free_arg
	)			[related]

Adds a trigger to the symbol cache.

Adds a trigger to the symbol cache. "arg" is the argument that will be passed to function "trigger" when invoked.

must_free_arg controls if the given argument must be automatically freed when cleaning up.

If the trigger is already registered (same function and same action), it is not added again

The "action" parameter determines when "trigger" is triggered. The possibilities are:

ST_TRIGGER_SYMBOL_ADD: Triggered when a symbol is added. When the trigger is called, all informations about the symbol are already available (e.g. SymbType).

ST_TRIGGER_SYMBOL_REMOVE: Triggered when a symbol is removed. All informations about the symbol are still available when the trigger is invoked.

ST_TRIGGER_SYMBOL_REDECLARE: Triggered when a symbol that had been removed and later redeclared with the same name. All informations about the new symbol are available, while informations about the old symbol are not

See also:

SymbCache_remove_trigger

SymbCache_ptr SymbCache_create	(	SymbTable_ptr	symb_table,
		NuSMVEnv_ptr	env
	)			[related]

The SymbCache class private interface.

Author:

Roberto Cavada

Todo:

: Missing description

Class constructor Callable only by the SymbTable instance that owns self. The caller keeps the ownership of given SymbTable instance

void SymbCache_destroy

(

SymbCache_ptr

self

)

[related]

Class destructor.

Callable only by the SymbTable instance that owns self.

void SymbCache_gen_iter	(	const SymbCache_ptr	self,
		SymbTableIter *	iter,
		const 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

node_ptr SymbCache_get_actual_parameter	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the actual param of the given formal parameter.

node_ptr SymbCache_get_actual_parameter_context	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the context of the actual parameter associated with the given formal parameter.

node_ptr SymbCache_get_array_define_body	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the body of the given define array name.

node_ptr SymbCache_get_array_define_context	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the context of the given define array name.

int SymbCache_get_array_defines_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of define arrays.

int SymbCache_get_constants_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of declared contants.

node_ptr SymbCache_get_define_body	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the body of the given DEFINE name.

node_ptr SymbCache_get_define_context	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the context of the given DEFINE name.

node_ptr SymbCache_get_define_flatten_body	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the flattenized body of the given DEFINE name.

int SymbCache_get_defines_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of DEFINEs.

NuSMVEnv_ptr SymbCache_get_environment

(

const SymbCache_ptr

self

)

[related]

SymbCache environment instance getter.

SymbCache environment instance getter

node_ptr SymbCache_get_flatten_actual_parameter	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the flattenized actual parameter of the given formal parameter.

int SymbCache_get_frozen_vars_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of declared frozen variables.

node_ptr SymbCache_get_function_context	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the context of the given NFunction.

SymbType_ptr SymbCache_get_function_type	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the type of a function.

int SymbCache_get_functions_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of NFunctions.

int SymbCache_get_input_vars_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of declared input variables.

int SymbCache_get_parameters_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of parameters.

int SymbCache_get_state_vars_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of declared state variables.

SymbTableType SymbCache_get_symbol_type	(	const SymbCache_ptr	self,
		const node_ptr	symbol
	)			[related]

Get the symbol type.

Get the symbol type. The symbol must be declared in the cache

int SymbCache_get_symbols_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of symbols.

SymbType_ptr SymbCache_get_var_type	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the type of a given variable.

"name" must be a variable

SymbType_ptr SymbCache_get_variable_array_type	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns the type of array variable, i.e. of variable_array.

int SymbCache_get_variable_arrays_num

(

const SymbCache_ptr

self

)

[related]

Returns the number of Symbol Types.

boolean SymbCache_is_iter_end	(	const SymbCache_ptr	self,
		const SymbTableIter *	iter
	)			[related]

Checks if the iterator is at it's end.

Checks if the iterator is at it's end

boolean SymbCache_is_symbol_array_define	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a declared define array.

boolean SymbCache_is_symbol_constant	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a declared constant.

boolean SymbCache_is_symbol_declared	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is declared.

boolean SymbCache_is_symbol_define	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a declared DEFINE.

boolean SymbCache_is_symbol_frozen_var	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the variable is frozen.

A variable is frozen if it is known that the var cannot change its value during transitions.

boolean SymbCache_is_symbol_function	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a declared NFunction.

boolean SymbCache_is_symbol_input_var	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is an input variable.

boolean SymbCache_is_symbol_parameter	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a declared formal parameter.

boolean SymbCache_is_symbol_state_frozen_var	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the variable is a frozen or a state variable.

boolean SymbCache_is_symbol_state_var	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a state variable.

boolean SymbCache_is_symbol_var	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is either a state, a frozen or an input variable.

boolean SymbCache_is_symbol_variable_array	(	const SymbCache_ptr	self,
		const node_ptr	name
	)			[related]

Returns true if the given symbol is a declared variable array.

node_ptr SymbCache_iter_get_symbol	(	const SymbCache_ptr	self,
		const SymbTableIter *	iter
	)			[related]

Get the symbol pointed by the iterator.

Get the symbol pointed by the iterator

void SymbCache_iter_set_filter	(	const SymbCache_ptr	self,
		SymbTableIter *	iter,
		SymbTableIterFilterFun	filter,
		void *	arg
	)			[related]

Sets the filter for an interator over the Symbol Cache symbols.

Sets the filter for an interator over the Symbol Cache symbols. The iterator will be moved in order to point to a symbol that satisfies both the mask and the filter

boolean SymbCache_list_contains_input_var	(	const SymbCache_ptr	self,
		const NodeList_ptr	var_list
	)			[related]

Returns true if var_list contains at least one input variable.

The given list of variables is traversed until an input variable is found

boolean SymbCache_list_contains_state_frozen_var	(	const SymbCache_ptr	self,
		const NodeList_ptr	var_list
	)			[related]

Returns true if var_list contains at least one state or frozen variable.

The given list of variables is traversed until a state or frozen variable is found

boolean SymbCache_list_contains_undef_var	(	const SymbCache_ptr	self,
		const NodeList_ptr	var_list
	)			[related]

Returns true if the given symbols list contains one or more undeclared variable names.

Iterates through the elements in var_list checking each one to see if it is one undeclared variable.

void SymbCache_new_array_define	(	SymbCache_ptr	self,
		node_ptr	name,
		node_ptr	ctx,
		node_ptr	definition
	)			[related]

Declares a new define array.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted. Internally we use ARRAY_DEF node to recognize a define array.

void SymbCache_new_constant	(	SymbCache_ptr	self,
		node_ptr	name
	)			[related]

Declares a new constant.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted. Multiple-time declared constant are accepted, and a reference count is kept to deal with them

void SymbCache_new_define	(	SymbCache_ptr	self,
		node_ptr	name,
		node_ptr	context,
		node_ptr	definition
	)			[related]

Declares a new DEFINE.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_new_frozen_var	(	SymbCache_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Declares a new frozen variable.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

See also:

SymbCache_redeclare_state_as_frozen_var

void SymbCache_new_function	(	SymbCache_ptr	self,
		node_ptr	name,
		node_ptr	context,
		SymbType_ptr	type
	)			[related]

Declares a new NFunction.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_new_input_var	(	SymbCache_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Declares a new input variable.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_new_parameter	(	SymbCache_ptr	self,
		node_ptr	formal,
		node_ptr	context,
		node_ptr	actual
	)			[related]

Declares a new module parameter.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_new_state_var	(	SymbCache_ptr	self,
		node_ptr	var,
		SymbType_ptr	type
	)			[related]

Declares a new state variable.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_new_variable_array	(	SymbCache_ptr	self,
		node_ptr	name,
		SymbType_ptr	type
	)			[related]

Declares a new ARRAY var.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_next_iter	(	const SymbCache_ptr	self,
		SymbTableIter *	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

void SymbCache_redeclare_state_as_frozen_var	(	SymbCache_ptr	self,
		node_ptr	var
	)			[related]

Redeclare a state variable as a frozen variable.

A variable is frozen if it is known that its value cannot be changed during transitions. The given 'name' has to be already declared state variable and not yet redeclared as frozen.

See also:

SymbCache_new_frozen_var

void SymbCache_remove_constant	(	SymbCache_ptr	self,
		node_ptr	constant
	)			[related]

Removes a constant from the cache of symbols, and from the flattener module.

Removal is performed taking into account of reference counting, as constants can be shared among several layers. This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_remove_define	(	SymbCache_ptr	self,
		node_ptr	define
	)			[related]

Removes a DEFINE from the cache of symbols, and from the flattener define hash.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_remove_function	(	SymbCache_ptr	self,
		node_ptr	name
	)			[related]

Removes an NFunction from the cache of symbols.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_remove_parameter	(	SymbCache_ptr	self,
		node_ptr	formal
	)			[related]

Removes a parameter from the cache of symbols.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_remove_symbols	(	SymbCache_ptr	self,
		const node_ptr *	symbols,
		const unsigned int	size
	)			[related]

Removes all the symbols in the array.

Removes all the symbols in the array in linear time

void SymbCache_remove_trigger	(	const SymbCache_ptr	self,
		SymbTableTriggerFun	trigger,
		SymbTableTriggerAction	action
	)			[related]

Removes a trigger from the symbol cache.

Removes a trigger from the symbol cache

See also:

SymbCache_add_trigger

void SymbCache_remove_var	(	SymbCache_ptr	self,
		node_ptr	var
	)			[related]

Removes a variable from the cache of symbols, and from the flattener module.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

void SymbCache_remove_variable_array	(	SymbCache_ptr	self,
		node_ptr	symbol
	)			[related]

Removes a variable array from the cache of symbols.

This (private) method can be used only by SymbLayer, otherwise the resulting status will be corrupted.

---

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

• NuSMV/code/nusmv/core/compile/symb_table/SymbCache.h
• NuSMV/code/nusmv/core/compile/symb_table/SymbCache_private.h