NuSMV/code/nusmv/core/compile/dependency/FormulaDependency_private.h File Reference

#include "nusmv/core/compile/dependency/FormulaDependency.h"
#include "nusmv/core/node/MasterNodeWalker.h"
#include "nusmv/core/node/MasterNodeWalker_private.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/defs.h"
#include "nusmv/core/utils/Tuple5.h"

Go to the source code of this file.

Data Structures
struct	FormulaDependency
	Private and protected interface of class 'FormulaDependency'. More...
Defines
#define	BUILDING_DEP_SET   (Set_t)-10
	Indicates that the dependency computation is ongoing.
#define	EMPTY_DEP_SET   (Set_t)-11
	Indicates that the dependency is empty.
#define	IS_VALID_SET(set)
	True if the set is not NULL or equal the fake sets used as placeholder.
#define	NO_DEP_SET   (Set_t)-12
	Indicates that no dependency has been yet computed.
Functions
void	formula_dependency_close_define_hash (hash_ptr dep_hash, node_ptr key, Set_t value)
	Insertion function for dependencies_hash.
void	formula_dependency_insert_hash (hash_ptr dep_hash, node_ptr key, Set_t value)
	Insertion function for dependencies_hash.
Set_t	formula_dependency_lookup_hash (hash_ptr dep_hash, node_ptr key)
	Lookup function for dependencies_hash.
void	formula_dependency_mk_hash_key (node_ptr e, node_ptr c, SymbFilterType filter, boolean preserve_time, int time, Tuple5_ptr key)
	Make the hash key used by dependencies_hash.

---

Define Documentation

#define BUILDING_DEP_SET   (Set_t)-10

Indicates that the dependency computation is ongoing.

The value used during the building of dependencies of defined symbols to keep track that compuation is ongoing to discover circular definitions.

#define EMPTY_DEP_SET   (Set_t)-11

Indicates that the dependency is empty.

#define IS_VALID_SET

(

set

)

Value:

(EMPTY_DEP_SET != set &&                         \
   BUILDING_DEP_SET != set &&                      \
   NO_DEP_SET != set &&                            \
   (Set_t)NULL != set)

True if the set is not NULL or equal the fake sets used as placeholder.

#define NO_DEP_SET   (Set_t)-12

Indicates that no dependency has been yet computed.

---

Function Documentation

void formula_dependency_close_define_hash	(	hash_ptr	dep_hash,
		node_ptr	key,
		Set_t	value
	)

Insertion function for dependencies_hash.

To be called after the dependencies of the define represented by key has been full computed. Replace the placeholder BUILDING_DEP_SET with the result. Assumes the key to be already in the table. Take a Tuple5_ptr set with Tuple5_init() (memorized on the stack) and use it to replace the associated valued in the hash.

void formula_dependency_insert_hash	(	hash_ptr	dep_hash,
		node_ptr	key,
		Set_t	value
	)

Insertion function for dependencies_hash.

Take a Tuple5_ptr set with Tuple5_init() (memorized on the stack), allocates it and insert it in the hash table. Assumes the key not be already in the table.

Set_t formula_dependency_lookup_hash	(	hash_ptr	dep_hash,
		node_ptr	key
	)

Lookup function for dependencies_hash.

void formula_dependency_mk_hash_key	(	node_ptr	e,
		node_ptr	c,
		SymbFilterType	filter,
		boolean	preserve_time,
		int	time,
		Tuple5_ptr	key
	)

Make the hash key used by dependencies_hash.

The Tuple5 has to freed by the caller