MasterCompileFlattener Struct Reference

Private and protected interface of class 'MasterCompileFlattener'. More...

#include <MasterCompileFlattener_private.h>

Public Member Functions
	INHERITS_FROM (MasterNodeWalker)
Related Functions
(Note that these are not member functions.)
void	master_compile_flattener_deinit (MasterCompileFlattener_ptr self)
	The MasterCompileFlattener class private deinitializer.
node_ptr	master_compile_flattener_flatten (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr sexp, node_ptr context, MasterCompileFlattener_def_mode def_mode)
	Recursive function for flattenig a sexp.
hash_ptr	master_compile_flattener_get_def_hash (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table)
	Get the hash of the defines.
node_ptr	master_compile_flattener_get_definition (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr name, MasterCompileFlattener_def_mode def_mode)
	Gets the flattened version of an atom.
void	master_compile_flattener_init (MasterCompileFlattener_ptr self, const NuSMVEnv_ptr env)
	The MasterCompileFlattener class private initializer.
MasterCompileFlattener_ptr	MasterCompileFlattener_create (const NuSMVEnv_ptr env)
	The MasterCompileFlattener class constructor.
void	MasterCompileFlattener_destroy (MasterCompileFlattener_ptr self)
	The MasterCompileFlattener class destructor.
node_ptr	MasterCompileFlattener_flatten (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table, node_ptr sexp, node_ptr context)
	Builds the flattened version of an expression.
node_ptr	MasterCompileFlattener_flatten_expand_define (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table, node_ptr sexp, node_ptr context)
	Flattens an expression and expands defined symbols.
node_ptr	MasterCompileFlattener_get_definition (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table, node_ptr sexp, MasterCompileFlattener_def_mode mode)
	Gets the flattened version of an atom.
void	MasterCompileFlattener_remove_define_info (MasterCompileFlattener_ptr self, SymbTable_ptr symb_table, node_ptr name)
	Remove the information associated to name from the define hash.

Detailed Description

Private and protected interface of class 'MasterCompileFlattener'.

Public interface of class 'MasterCompileFlattener'.

Author:: Sergio Mover This file can be included only by derived and friend classes

MasterCompileFlattener class definition derived from class MasterNodeWalker

See also:: Base class MasterNodeWalker

Author:: Sergio Mover

Todo:: : Missing description

Definition of the public accessor for class MasterCompileFlattener

Member Function Documentation

MasterCompileFlattener::INHERITS_FROM ( MasterNodeWalker )

Friends And Related Function Documentation

void master_compile_flattener_deinit ( MasterCompileFlattener_ptr self ) [related]

The MasterCompileFlattener class private deinitializer.

The MasterCompileFlattener class private deinitializer

See also:: MasterCompileFlattener_destroy

node_ptr master_compile_flattener_flatten	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table,
		hash_ptr	def_hash,
		node_ptr	sexp,
		node_ptr	context,
		MasterCompileFlattener_def_mode	def_mode
	)			`[related]`

Recursive function for flattenig a sexp.

The function changes its behavior depending on the value of mode:

Flattener_Get_Def_Mode: in this mode, the defines in the expression are returned as-is (i.e. they are not expanded!)
Flattener_Expand_Def_Mode: in this mode, all the defines found in the formula will be expanded.

DOCUMENTATION ABOUT ARRAY:

In NuSMV ARRAY has 2 meanings, it can be a part of identifier (which we call identifier-with-brackets) or a part of expression. For example, VAR v[5] : boolean; declares a new identifier-with-brackets v[5] where [5] is a part of identifier. Thus v[d], where d is a define equal to 5, is not a valid identifier as well as v[4+1] or v, whereas v[5] is valid.

For "VAR v : array 1..5 of boolean;" v[5] is identifier (array elements are declared in symbol table) v[d] is not, but both are valid expressions.

This difference is important for code, e.g. DEFINE d := v; INVARSPEC d[5]; If v[5] is declared as individual identifier this code is invalid because v is not declared whereas if v is an array the code becomes valid.

Flattener additionally makes every ARRAY-expression normalized. For example, d[i+1] is changed to case i+1=0 : v[0]; i+1=1 : v[1]; ... FAILURE; esac. Such a way every v[N] become a legal identifier wrt symbol table. Note that above normalization is done independent if defines are set to be expanded or not.

NOTE: arrays of modules are not supported. Thus ARRAY before DOT can be legal only through identifier-with-brackets declaration, e.g. for v[3].b to be valid it is necessary to declare v[3] as module instance.

NOTE: currently this function applies find_atom to the constants and IDs and new_node to operations nodes. If this approach changes then internal function ltl_rewrite_input has to be changed as well. Thus, the returned expression may be NOT NORMALIZED!

See also:: Compile_FlattenSexp Compile_FlattenSexpExpandDefine

hash_ptr master_compile_flattener_get_def_hash	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table
	)			`[related]`

Get the hash of the defines.

node_ptr master_compile_flattener_get_definition	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table,
		hash_ptr	def_hash,
		node_ptr	name,
		MasterCompileFlattener_def_mode	def_mode
	)			`[related]`

Gets the flattened version of an atom.

Gets the flattened version of an atom. If the atom is a define then it is expanded. If the definition mode is set to "expand", then the expanded flattened version is returned, otherwise, the atom is returned.

The flatten_def_hash is modified in order to memoize previously computed definition expansion.

void master_compile_flattener_init	(	MasterCompileFlattener_ptr	self,
		const NuSMVEnv_ptr	env
	)			`[related]`

The MasterCompileFlattener class private initializer.

The MasterCompileFlattener class private initializer

See also:: MasterCompileFlattener_create

MasterCompileFlattener_ptr MasterCompileFlattener_create ( const NuSMVEnv_ptr env ) [related]

The MasterCompileFlattener class constructor.

AutomaticStart

The MasterCompileFlattener class constructor

See also:: MasterCompileFlattener_destroy

void MasterCompileFlattener_destroy ( MasterCompileFlattener_ptr self ) [related]

The MasterCompileFlattener class destructor.

The MasterCompileFlattener class destructor

See also:: MasterCompileFlattener_create

node_ptr MasterCompileFlattener_flatten	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	sexp,
		node_ptr	context
	)			`[related]`

Builds the flattened version of an expression.

Builds the flattened version of an expression. It does not expand defined symbols with the corresponding body.

node_ptr MasterCompileFlattener_flatten_expand_define	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	sexp,
		node_ptr	context
	)			`[related]`

Flattens an expression and expands defined symbols.

New entries may be added to flatten_def_hash changes

node_ptr MasterCompileFlattener_get_definition	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	sexp,
		MasterCompileFlattener_def_mode	mode
	)			`[related]`

Gets the flattened version of an atom.

Gets the flattened version of an atom. If the atom is a define then it is expanded. If the definition mode is set to "expand", then the expanded flattened version is returned, otherwise, the atom is returned.

The flatten_def_hash is modified in order to memoize previously computed definition expansion.

void MasterCompileFlattener_remove_define_info	(	MasterCompileFlattener_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	name
	)			`[related]`

Remove the information associated to name from the define hash.

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

NuSMV/code/nusmv/core/compile/flattening/MasterCompileFlattener_private.h
NuSMV/code/nusmv/core/compile/flattening/MasterCompileFlattener.h

MasterCompileFlattener Struct Reference

Public Member Functions

Related Functions

Detailed Description

Member Function Documentation

Friends And Related Function Documentation