FlattenerBase Struct Reference

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

#include <FlattenerBase_private.h>

Public Member Functions
	INHERITS_FROM (NodeWalker)
Data Fields
node_ptr(*	flatten )(FlattenerBase_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr sexp, node_ptr context, MasterCompileFlattener_def_mode mode)
Related Functions
(Note that these are not member functions.)
void	flattener_base_deinit (FlattenerBase_ptr self)
	The FlattenerBase class private deinitializer.
node_ptr	flattener_base_flatten (FlattenerBase_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr sexp, node_ptr context, MasterCompileFlattener_def_mode mode)
	Flatten the given node.
void	flattener_base_init (FlattenerBase_ptr self, const NuSMVEnv_ptr env, const char *name, int low, size_t num, boolean can_handle_null)
	The FlattenerBase class private initializer.
node_ptr	flattener_base_throw_flatten (FlattenerBase_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr sexp, node_ptr context, MasterCompileFlattener_def_mode mode)
	This method must be called by the virtual method throw_flatten to recursively flatten sexp.
FlattenerBase_ptr	FlattenerBase_create (const NuSMVEnv_ptr env, const char *name, int low, size_t num)
	Creates and initializes a flattener. To be usable, the flattener will have to be registered to a MasterCompileFlattener.
VIRTUAL node_ptr	FlattenerBase_flatten (FlattenerBase_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr sexp, node_ptr context, MasterCompileFlattener_def_mode mode)
	Flattens the given expression with the given context.

---

Detailed Description

Private and protected interface of class 'FlattenerBase'.

Public interface of class 'FlattenerBase'.

Author:

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

FlattenerBase class definition derived from class NodeWalker

See also:

Base class NodeWalker

Author:

Sergio Mover

Todo:

: Missing description

Definition of the public accessor for class FlattenerBase

---

Member Function Documentation

FlattenerBase::INHERITS_FROM

(

NodeWalker

)

---

Friends And Related Function Documentation

void flattener_base_deinit

(

FlattenerBase_ptr

self

)

[related]

The FlattenerBase class private deinitializer.

The FlattenerBase class private deinitializer

node_ptr flattener_base_flatten	(	FlattenerBase_ptr	self,
		SymbTable_ptr	symb_table,
		hash_ptr	def_hash,
		node_ptr	sexp,
		node_ptr	context,
		MasterCompileFlattener_def_mode	mode
	)			[related]

Flatten the given node.

void flattener_base_init	(	FlattenerBase_ptr	self,
		const NuSMVEnv_ptr	env,
		const char *	name,
		int	low,
		size_t	num,
		boolean	can_handle_null
	)			[related]

The FlattenerBase class private initializer.

The FlattenerBase class private initializer

See also:

FlattenerBase_create

node_ptr flattener_base_throw_flatten	(	FlattenerBase_ptr	self,
		SymbTable_ptr	symb_table,
		hash_ptr	def_hash,
		node_ptr	sexp,
		node_ptr	context,
		MasterCompileFlattener_def_mode	mode
	)			[related]

This method must be called by the virtual method throw_flatten to recursively flatten sexp.

FlattenerBase_ptr FlattenerBase_create	(	const NuSMVEnv_ptr	env,
		const char *	name,
		int	low,
		size_t	num
	)			[related]

Creates and initializes a flattener. To be usable, the flattener will have to be registered to a MasterCompileFlattener.

To each flattener is associated a partition of consecutive indices over the symbols set. The lowest index of the partition is given through the parameter low, while num is the partition size. Name is used to easily identify printer instances.

This constructor is private, as this class is virtual

VIRTUAL node_ptr FlattenerBase_flatten	(	FlattenerBase_ptr	self,
		SymbTable_ptr	symb_table,
		hash_ptr	def_hash,
		node_ptr	sexp,
		node_ptr	context,
		MasterCompileFlattener_def_mode	mode
	)			[related]

Flattens the given expression with the given context.

AutomaticStart

Flattens the given expression with the given context.

The caller (the master) has to check if the current flattener may handle sexp.

---

Field Documentation

node_ptr(* FlattenerBase::flatten)(FlattenerBase_ptr self, SymbTable_ptr symb_table, hash_ptr def_hash, node_ptr sexp, node_ptr context, MasterCompileFlattener_def_mode mode)

---

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

• NuSMV/code/nusmv/core/compile/flattening/FlattenerBase_private.h
• NuSMV/code/nusmv/core/compile/flattening/FlattenerBase.h