DependencyBase Struct Reference

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

#include <DependencyBase_private.h>

Public Member Functions
	INHERITS_FROM (NodeWalker)
Data Fields
Set_t(*	get_dependencies )(DependencyBase_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time, int time, hash_ptr dependencies_hash)
Related Functions
(Note that these are not member functions.)
void	dependency_base_deinit (DependencyBase_ptr self)
	The DependencyBase class private deinitializer.
void	dependency_base_init (DependencyBase_ptr self, const NuSMVEnv_ptr env, const char *name, int low, size_t num, boolean can_handle_null)
	The DependencyBase class private initializer.
Set_t	dependency_base_throw_get_dependencies (DependencyBase_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time, int time, hash_ptr dependencies_hash)
	This method must be called by the virtual method throw_get_dependencies to recursively get the dependencies of an expression.
DependencyBase_ptr	DependencyBase_create (const NuSMVEnv_ptr env, const char *name, int low, size_t num)
	Creates and initializes a dependency. To be usable, the dependency will have to be registered to a FormulaDependency.
VIRTUAL Set_t	DependencyBase_get_dependencies (DependencyBase_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time, int time, hash_ptr dependencies_hash)
	Get the dependencies for expr in the given context.

---

Detailed Description

Private and protected interface of class 'DependencyBase'.

Public interface of class 'DependencyBase'.

Author:

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

DependencyBase class definition derived from class NodeWalker

See also:

Base class NodeWalker

Author:

Sergio Mover

Todo:

: Missing description

Definition of the public accessor for class DependencyBase

---

Member Function Documentation

DependencyBase::INHERITS_FROM

(

NodeWalker

)

---

Friends And Related Function Documentation

void dependency_base_deinit

(

DependencyBase_ptr

self

)

[related]

The DependencyBase class private deinitializer.

The DependencyBase class private deinitializer

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

The DependencyBase class private initializer.

The DependencyBase class private initializer

See also:

DependencyBase_create

Set_t dependency_base_throw_get_dependencies	(	DependencyBase_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	formula,
		node_ptr	context,
		SymbFilterType	filter,
		boolean	preserve_time,
		int	time,
		hash_ptr	dependencies_hash
	)			[related]

This method must be called by the virtual method throw_get_dependencies to recursively get the dependencies of an expression.

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

Creates and initializes a dependency. To be usable, the dependency will have to be registered to a FormulaDependency.

To each instance it 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 the instances.

This constructor is private, as this class is virtual

VIRTUAL Set_t DependencyBase_get_dependencies	(	DependencyBase_ptr	self,
		SymbTable_ptr	symb_table,
		node_ptr	formula,
		node_ptr	context,
		SymbFilterType	filter,
		boolean	preserve_time,
		int	time,
		hash_ptr	dependencies_hash
	)			[related]

Get the dependencies for expr in the given context.

AutomaticStart

Get the dependencies for expr in the given context.

The caller (the master) has to check if the current dependency may handle the expression.

---

Field Documentation

Set_t(* DependencyBase::get_dependencies)(DependencyBase_ptr self, SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time, int time, hash_ptr dependencies_hash)

---

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

• NuSMV/code/nusmv/core/compile/dependency/DependencyBase_private.h
• NuSMV/code/nusmv/core/compile/dependency/DependencyBase.h