BddEncCache Struct Reference

The Bdd encoding cache interface. More...

#include <BddEncCache.h>

Related Functions
(Note that these are not member functions.)
void	BddEncCache_clean_evaluation (BddEncCache_ptr self)
	Cleans up the cache from all the evaluated expressions.
void	BddEncCache_clean_evaluation_about (BddEncCache_ptr self, NodeList_ptr symbs)
	Cleans those hashed entries that are about a symbol that is being removed.
BddEncCache_ptr	BddEncCache_create (SymbTable_ptr symb_table, DDMgr_ptr dd)
	Class constructor.
void	BddEncCache_destroy (BddEncCache_ptr self)
	Class destructor.
AddArray_ptr	BddEncCache_get_evaluation (BddEncCache_ptr self, node_ptr expr)
	Retrieve the evaluation of a given symbol, as an array of ADD.
boolean	BddEncCache_is_boolean_var_encoded (const BddEncCache_ptr self, node_ptr var_name)
	Returns true whether the given boolean variable has been encoded.
boolean	BddEncCache_is_constant_encoded (const BddEncCache_ptr self, node_ptr constant)
	Returns true whether the given constant has been encoded.
add_ptr	BddEncCache_lookup_boolean_var (const BddEncCache_ptr self, node_ptr var_name)
	Retrieves the add associated with the given boolean variable, if previously encoded.
add_ptr	BddEncCache_lookup_constant (const BddEncCache_ptr self, node_ptr constant)
	Returns the ADD corresponding to the given constant, or NULL if not defined.
void	BddEncCache_new_boolean_var (BddEncCache_ptr self, node_ptr var_name, add_ptr var_add)
	Call this to insert the encoding for a given boolean variable.
void	BddEncCache_new_constant (BddEncCache_ptr self, node_ptr constant, add_ptr constant_add)
	Call to associate given constant to the relative add.
void	BddEncCache_remove_boolean_var (BddEncCache_ptr self, node_ptr var_name)
	Removes the given variable from the internal hash.
void	BddEncCache_remove_constant (BddEncCache_ptr self, node_ptr constant)
	Removes the given constant from the internal hash.
void	BddEncCache_remove_evaluation (BddEncCache_ptr self, node_ptr expr)
	This method is used to remove the result of evaluation of an expression.
void	BddEncCache_set_evaluation (BddEncCache_ptr self, node_ptr expr, AddArray_ptr add_array)
	This method is used to remember the result of evaluation, i.e. to keep the association between the expression in node_ptr form and its ADD representation.

---

Detailed Description

The Bdd encoding cache interface.

Author:

Roberto Cavada This interface and relative class is intended to be used exclusively by the BddEnc class

The BddEncCache type The BddEncCache type

---

Friends And Related Function Documentation

void BddEncCache_clean_evaluation

(

BddEncCache_ptr

self

)

[related]

Cleans up the cache from all the evaluated expressions.

Note that hashed encoding of boolean variables and constants (added by BddEncCache_new_boolean_var and BddEncCache_new_constant, resp.) remains intact.

void BddEncCache_clean_evaluation_about	(	BddEncCache_ptr	self,
		NodeList_ptr	symbs
	)			[related]

Cleans those hashed entries that are about a symbol that is being removed.

This is called by the BddEnc class when a layer is begin removed and the cache has to be cleaned up

BddEncCache_ptr BddEncCache_create	(	SymbTable_ptr	symb_table,
		DDMgr_ptr	dd
	)			[related]

Class constructor.

void BddEncCache_destroy

(

BddEncCache_ptr

self

)

[related]

Class destructor.

AddArray_ptr BddEncCache_get_evaluation	(	BddEncCache_ptr	self,
		node_ptr	expr
	)			[related]

Retrieve the evaluation of a given symbol, as an array of ADD.

If given symbol has not been evaluated, NULL is returned. If the evaluation is in the process, BDD_ENC_EVALUATING is returned. Otherwise an array of ADD is returned.

The returned array must be destroyed by the invoker!

NB: For all expressions except of the Word type the returned array can contain only one element. NB: If NuSMV option enable_sexp2bdd_caching is unset to 0 then the hash may be empty.

boolean BddEncCache_is_boolean_var_encoded	(	const BddEncCache_ptr	self,
		node_ptr	var_name
	)			[related]

Returns true whether the given boolean variable has been encoded.

boolean BddEncCache_is_constant_encoded	(	const BddEncCache_ptr	self,
		node_ptr	constant
	)			[related]

Returns true whether the given constant has been encoded.

add_ptr BddEncCache_lookup_boolean_var	(	const BddEncCache_ptr	self,
		node_ptr	var_name
	)			[related]

Retrieves the add associated with the given boolean variable, if previously encoded.

Returned add is referenced. NULL is returned if the variable is not encoded.

add_ptr BddEncCache_lookup_constant	(	const BddEncCache_ptr	self,
		node_ptr	constant
	)			[related]

Returns the ADD corresponding to the given constant, or NULL if not defined.

Returned ADD is referenced, NULL is returned if the given constant is not currently encoded

void BddEncCache_new_boolean_var	(	BddEncCache_ptr	self,
		node_ptr	var_name,
		add_ptr	var_add
	)			[related]

Call this to insert the encoding for a given boolean variable.

void BddEncCache_new_constant	(	BddEncCache_ptr	self,
		node_ptr	constant,
		add_ptr	constant_add
	)			[related]

Call to associate given constant to the relative add.

This methods adds the given constant only if it does not exist already, otherwise it only increments a reference counter, to be used when the constant is removed later.

void BddEncCache_remove_boolean_var	(	BddEncCache_ptr	self,
		node_ptr	var_name
	)			[related]

Removes the given variable from the internal hash.

void BddEncCache_remove_constant	(	BddEncCache_ptr	self,
		node_ptr	constant
	)			[related]

Removes the given constant from the internal hash.

void BddEncCache_remove_evaluation	(	BddEncCache_ptr	self,
		node_ptr	expr
	)			[related]

This method is used to remove the result of evaluation of an expression.

If a given node_ptr is associated already with some AddArray then the array is freed. Otherwise nothing happens

void BddEncCache_set_evaluation	(	BddEncCache_ptr	self,
		node_ptr	expr,
		AddArray_ptr	add_array
	)			[related]

This method is used to remember the result of evaluation, i.e. to keep the association between the expression in node_ptr form and its ADD representation.

The provided array of ADD will belong to "self" and will be freed during destruction of the class or setting a new value for the same node_ptr.

NOTE: if NuSMV option "enable_sexp2bdd_caching" is unset to 0 then no result is kept and the provided add_array is immediately freed

---

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

• NuSMV/code/nusmv/core/enc/bdd/BddEncCache.h