BddEnc Struct Reference

BddEnc class definition derived from class BoolEncClient. More...

#include <BddEnc_private.h>

Public Member Functions
	INHERITS_FROM (BoolEncClient)
Data Fields
BddEncCache_ptr	cache
dd_reorderingtype	curr_reord_type
int	curr_reorderings
array_t *	current2next
DDMgr_ptr	dd
VarsHandler_ptr	dd_vars_hndr
boolean	enforce_constant
hash_ptr	failures_hash
add_ptr	frozen_vars_add
bdd_ptr	frozen_vars_bdd
int	frozen_vars_num
array_t *	index2name
NodeList_ptr	index_gaps
add_ptr	input_vars_add
bdd_ptr	input_vars_bdd
add_ptr	input_vars_mask_add
bdd_ptr	input_vars_mask_bdd
int	input_vars_num
hash_ptr	layer2groups
array_t *	level2index
array_t *	minterm_frozen_vars
int	minterm_frozen_vars_dim
array_t *	minterm_input_vars
int	minterm_input_vars_dim
array_t *	minterm_next_state_vars
int	minterm_next_state_vars_dim
array_t *	minterm_state_frozen_input_vars
int	minterm_state_frozen_input_vars_dim
array_t *	minterm_state_frozen_vars
int	minterm_state_frozen_vars_dim
array_t *	minterm_state_vars
int	minterm_state_vars_dim
hash_ptr	name2index
array_t *	next2current
add_ptr	next_state_vars_add
bdd_ptr	next_state_vars_bdd
OrdGroups_ptr	ord_groups
node_ptr	print_stack
int	reord_locked_num
int	reord_status
add_ptr	state_frozen_input_vars_mask_add
bdd_ptr	state_frozen_input_vars_mask_bdd
bdd_ptr	state_frozen_vars_bdd
add_ptr	state_frozen_vars_mask_add
bdd_ptr	state_frozen_vars_mask_bdd
add_ptr	state_vars_add
bdd_ptr	state_vars_bdd
int	state_vars_num
TypeChecker_ptr	type_checker
int	used_indices_frontier
Related Functions
(Note that these are not member functions.)
void	bdd_enc_deinit (BddEnc_ptr self)
void	bdd_enc_init (BddEnc_ptr self, SymbTable_ptr symb_table, BoolEnc_ptr bool_enc, VarsHandler_ptr dd_vars_hdlr, OrdGroups_ptr ord_groups)
void	bdd_enc_shuffle_variables_order (BddEnc_ptr self, NodeList_ptr vars)
node_ptr	BddEnc_add_to_expr (BddEnc_ptr self, const add_ptr add, SymbLayer_ptr det_layer)
	Converts a ADD into the corresponding (boolean) expression.
node_ptr	BddEnc_add_to_scalar_expr (BddEnc_ptr self, const add_ptr add, SymbLayer_ptr det_layer)
	Converts a ADD into the corresponding (possibly scalar) expression.
add_ptr	BddEnc_apply_input_vars_mask_add (BddEnc_ptr self, add_ptr inputs)
	Applies a mask to the given add which must contain only input variables.
BddInputs	BddEnc_apply_input_vars_mask_bdd (BddEnc_ptr self, BddInputs inputs)
	Applies a mask to the given BDD which must contain only input variables.
add_ptr	BddEnc_apply_state_frozen_input_vars_mask_add (BddEnc_ptr self, add_ptr states_inputs)
	Applies a mask to the given add which must contain frozen, state and input variables.
BddStatesInputs	BddEnc_apply_state_frozen_input_vars_mask_bdd (BddEnc_ptr self, BddStatesInputs states_inputs)
	Applies a mask to the given BDD which must contain frozen, state and input variables.
add_ptr	BddEnc_apply_state_frozen_vars_mask_add (BddEnc_ptr self, add_ptr states)
	Applies a mask to the given add which must contain only frozen and state variables.
BddStates	BddEnc_apply_state_frozen_vars_mask_bdd (BddEnc_ptr self, BddStates states)
	Applies a mask to the given BDD which must contain only frozen and state variables.
node_ptr	BddEnc_assign_symbols (BddEnc_ptr self, bdd_ptr bdd, NodeList_ptr symbols, boolean onlyRequiredSymbs, bdd_ptr *resultBdd)
	This function is similar to BddEnc_print_set_of... functions except that instead of printing values of variables, this funtion creates a list of pairs var-itsValue.
node_ptr	BddEnc_bdd_to_expr (BddEnc_ptr self, const bdd_ptr bdd)
	Converts a BDD into the corresponding (boolean) expression.
node_ptr	BddEnc_bdd_to_wff (BddEnc_ptr self, bdd_ptr bdd, NodeList_ptr vars)
	Converts a bdd into a Well Formed Formula representing it.
void	BddEnc_clean_evaluation_cache (BddEnc_ptr self)
	Clean the internal cache which contains the results of evaluation of expressions to ADD or BDD form.
array_t *	BddEnc_ComputePrimeImplicants (BddEnc_ptr self, const array_t *layer_names, bdd_ptr formula)
	Finds a set of prime implicants for a formula represented as a BDD.
add_ptr	BddEnc_constant_to_add (const BddEnc_ptr self, node_ptr constant)
	Returns the ADD leaf corresponding to the given atom.
double	BddEnc_count_inputs_of_bdd (const BddEnc_ptr self, bdd_ptr bdd)
	Return the number of inputs of a given BDD.
double	BddEnc_count_states_inputs_of_bdd (const BddEnc_ptr self, bdd_ptr bdd)
	Return the number of states inputs of a given BDD.
double	BddEnc_count_states_of_add (const BddEnc_ptr self, add_ptr add)
	Return the number of states of a given ADD.
double	BddEnc_count_states_of_bdd (const BddEnc_ptr self, bdd_ptr bdd)
	Return the number of states of a given BDD.
BddEnc_ptr	BddEnc_create (SymbTable_ptr symb_table, BoolEnc_ptr bool_enc, VarsHandler_ptr dd_vars_hndr, OrdGroups_ptr ord_groups)
	The BddEnc class constructor.
VIRTUAL void	BddEnc_destroy (BddEnc_ptr self)
	The BddEnc class destructor.
int	BddEnc_dump_addarray_davinci (BddEnc_ptr self, AddArray_ptr addarray, const char *labels, FILE outfile)
	Dumps the given AddArray in DAVINCI format.
int	BddEnc_dump_addarray_dot (BddEnc_ptr self, AddArray_ptr addarray, const char *labels, FILE outfile)
	Dumps the given AddArray in DOT format.
int	BddEnc_dump_expr (const BddEnc_ptr self, const node_ptr parsed_expr, const char str_constr, const t_format format, FILE outfile)
	Dumps an expression in the specified output format.
add_ptr	BddEnc_eval_constant (BddEnc_ptr self, Expr_ptr expr, node_ptr context)
	Evaluates a constant expression.
int	BddEnc_eval_num (BddEnc_ptr self, node_ptr e, node_ptr context)
	Evaluates a number in a context.
add_ptr	BddEnc_eval_sign_add (BddEnc_ptr self, add_ptr a, int flag)
	Complements an ADD according to a flag.
bdd_ptr	BddEnc_eval_sign_bdd (BddEnc_ptr self, bdd_ptr a, int flag)
	Complements a BDD according to a flag.
add_ptr	BddEnc_expr_to_add (BddEnc_ptr self, const Expr_ptr expr, const node_ptr context)
	Returns the ADD representing the expression expr, in the given context.
AddArray_ptr	BddEnc_expr_to_addarray (BddEnc_ptr self, const Expr_ptr expr, const node_ptr context)
	Returns the ADD array representing the expression expr, in the given context.
bdd_ptr	BddEnc_expr_to_bdd (BddEnc_ptr self, const Expr_ptr expr, const node_ptr context)
	Returns the BDD representing the expression expr, in the given contex.
void	BddEnc_force_order (BddEnc_ptr self, OrdGroups_ptr new_po_grps)
	Forces a variable ordering in the BDD encoding.
void	BddEnc_force_order_from_file (BddEnc_ptr self, FILE *orderfile)
	Forces a variable ordering in the BDD encoding reading it from a file.
DDMgr_ptr	BddEnc_get_dd_manager (const BddEnc_ptr self)
VarsHandler_ptr	BddEnc_get_dd_vars_handler (const BddEnc_ptr self)
BddVarSet_ptr	BddEnc_get_frozen_vars_cube (const BddEnc_ptr self)
	Gets the support of the set of frozen variables.
BddVarSet_ptr	BddEnc_get_input_vars_cube (const BddEnc_ptr self)
	Gets the support of the set of input variables.
add_ptr	BddEnc_get_input_vars_mask_add (BddEnc_ptr self)
	Returns the mask (as an ADD) in terms of input variables.
bdd_ptr	BddEnc_get_input_vars_mask_bdd (BddEnc_ptr self)
	Returns the mask (as BDD) in terms of input variables.
BddVarSet_ptr	BddEnc_get_layer_vars_cube (const BddEnc_ptr self, SymbLayer_ptr layer, SymbFilterType vt)
	Given a layer the function produces a cube of all layer's variables.
double	BddEnc_get_minterms_of_add (const BddEnc_ptr self, add_ptr add)
	Return the number of minterms of a given ADD.
double	BddEnc_get_minterms_of_bdd (const BddEnc_ptr self, bdd_ptr bdd)
	Return the number of minterms of a given BDD.
BddVarSet_ptr	BddEnc_get_next_state_vars_cube (const BddEnc_ptr self)
	Gets the support of the set of next-state variables.
OrdGroups_ptr	BddEnc_get_ord_groups (const BddEnc_ptr self)
	Returns the internally used order that was specified when creating the instance. Order is used when committing a layer and when forcing a reordering.
int	BddEnc_get_reordering_count (const BddEnc_ptr self)
	Returns the number of reorderings that have been carried out since either the self construction or the last call to method reset_reordering_count.
add_ptr	BddEnc_get_state_frozen_input_vars_mask_add (BddEnc_ptr self)
	Returns the mask (as ADD) in terms of state, frozen and input variables.
bdd_ptr	BddEnc_get_state_frozen_input_vars_mask_bdd (BddEnc_ptr self)
	Returns the mask (as BDD) in terms of frozen, state and input variables.
BddVarSet_ptr	BddEnc_get_state_frozen_vars_cube (const BddEnc_ptr self)
	Gets the support of the set of state and frozen variables.
add_ptr	BddEnc_get_state_frozen_vars_mask_add (BddEnc_ptr self)
	Returns the mask (as an ADD) in terms of frozen and state variables.
bdd_ptr	BddEnc_get_state_frozen_vars_mask_bdd (BddEnc_ptr self)
	Returns the mask (as BDD) in terms of frozen and state variables.
BddVarSet_ptr	BddEnc_get_state_next_state_frozen_vars_cube (const BddEnc_ptr self)
	Gets the support of the set of state, next state and frozen variables.
BddVarSet_ptr	BddEnc_get_state_vars_cube (const BddEnc_ptr self)
	Gets the support of the set of state variables.
AddArray_ptr	BddEnc_get_symbol_add (BddEnc_ptr self, node_ptr name)
	Given a variable, define or process constant the corresponding ADD array is returned.
BddVarSet_ptr	BddEnc_get_unfiltered_vars_cube (const BddEnc_ptr self, Set_t vars)
	Given a set of variables the function produces a cube of all of them.
int	BddEnc_get_var_index_from_name (const BddEnc_ptr self, node_ptr name)
	Returns the DD index of the given variable.
add_ptr	BddEnc_get_var_mask (BddEnc_ptr self, node_ptr var_name)
	Given a variable, it returns the mask of its encoding.
node_ptr	BddEnc_get_var_name_from_index (const BddEnc_ptr self, int index)
	Given a variable index, this method return the symbolic name of the correpsonding variable.
NodeList_ptr	BddEnc_get_var_ordering (const BddEnc_ptr self, const VarOrderingType ord_type)
BddVarSet_ptr	BddEnc_get_vars_cube (const BddEnc_ptr self, Set_t vars, SymbFilterType vt)
	Given a set of variables the function produces a cube of them filtering out some of them.
NodeList_ptr	BddEnc_get_vars_in_cube (const BddEnc_ptr self, bdd_ptr cube, node_ptr list_of_sym, boolean include_next)
	Returns the symbolic names of boolean variables stored in a cube.
boolean	BddEnc_has_var_at_index (const BddEnc_ptr self, int index)
	Given a variable index, this method return true iff the given variable belongs to the encoder.
boolean	BddEnc_is_var_in_cube (const BddEnc_ptr self, node_ptr name, add_ptr cube)
	Returns true if the variable is in the cube and false otherwise.
bdd_ptr	BddEnc_next_state_var_to_state_var (const BddEnc_ptr self, bdd_ptr bdd)
	Exchange state variables for next state variables.
add_ptr	BddEnc_next_state_var_to_state_var_add (const BddEnc_ptr self, add_ptr add)
	Exchange state variables for next state variables in terms of ADD.
boolean	BddEnc_pick_all_terms_inputs (const BddEnc_ptr self, bdd_ptr bdd, bdd_ptr *result_array, const int array_len)
	Returns the array of All Possible Minterms.
boolean	BddEnc_pick_all_terms_states (const BddEnc_ptr self, bdd_ptr bdd, bdd_ptr *result_array, const int array_len)
	Returns the array of All Possible Minterms.
boolean	BddEnc_pick_all_terms_states_inputs (const BddEnc_ptr self, bdd_ptr bdd, bdd_ptr *result_array, const int array_len)
	Returns the array of All Possible Minterms.
bdd_ptr	BddEnc_pick_one_input (const BddEnc_ptr self, bdd_ptr inputs)
	Extracts a minterm from a given BDD.
bdd_ptr	BddEnc_pick_one_input_rand (const BddEnc_ptr self, bdd_ptr inputs)
	Extracts a random minterm from a given BDD.
bdd_ptr	BddEnc_pick_one_input_state (const BddEnc_ptr self, bdd_ptr inputs_states)
	Extracts a minterm over input/state variables from a given BDD.
bdd_ptr	BddEnc_pick_one_input_state_rand (const BddEnc_ptr self, bdd_ptr inputs_states)
	Extracts a random minterm from a given BDD.
bdd_ptr	BddEnc_pick_one_state (const BddEnc_ptr self, bdd_ptr states)
	Extracts a minterm from a given BDD.
bdd_ptr	BddEnc_pick_one_state_rand (const BddEnc_ptr self, bdd_ptr states)
	Extracts a random minterm from a given BDD.
int	BddEnc_print_bdd (BddEnc_ptr self, bdd_ptr bdd, VPFBEFNNV p_fun, OStream_ptr file, void *arg)
	Prints the given bdd. In particular prints only the symbols occuring in the symbols list passed to print_bdd_begin. Individual assignments may be printed using a user-defined function, passed as a parameter.
void	BddEnc_print_bdd_begin (BddEnc_ptr self, NodeList_ptr symbols, boolean changes_only)
	Call before a group of BddEnc_print_bdd calls.
void	BddEnc_print_bdd_end (BddEnc_ptr self)
	Must be called after each call to BddEnc_print_bdd_begin.
void	BddEnc_print_bdd_wff (BddEnc_ptr self, bdd_ptr bdd, NodeList_ptr vars, boolean do_sharing, boolean do_indent, int start_at_column, OStream_ptr out)
	Prints a BDD as a Well Formed Formula using optional sharing.
void	BddEnc_print_formula_info (BddEnc_ptr self, Expr_ptr formula, boolean print_models, boolean print_formula, OStream_ptr out)
	Prints statistical information of a formula.
void	BddEnc_print_set_of_inputs (BddEnc_ptr self, bdd_ptr inputs, boolean changes_only, VPFBEFNNV p_fun, OStream_ptr file, void *arg)
	Prints a set of input pairs. Individual assignments may be printed using a user-defined function, passed as a parameter.
void	BddEnc_print_set_of_state_input_pairs (BddEnc_ptr self, bdd_ptr state_input_pairs, boolean changes_only, VPFBEFNNV p_fun, OStream_ptr file, void *arg)
	Prints a set of state-input pairs. Individual assignments may be printed using a user-defined function, passed as a parameter.
void	BddEnc_print_set_of_states (BddEnc_ptr self, bdd_ptr states, boolean changes_only, boolean print_defines, VPFBEFNNV p_fun, OStream_ptr file, void *arg)
	Prints a set of states. Individual assignments may be printed using a user-defined function, passed as a parameter.
void	BddEnc_print_set_of_trans_models (BddEnc_ptr self, bdd_ptr state_input_pairs, OStream_ptr file)
	Prints a set of models for given trans.
void	BddEnc_print_vars_in_cube (BddEnc_ptr self, bdd_ptr cube, node_ptr list_of_sym, OStream_ptr file)
	Prints out the symbolic names of boolean variables stored in a cube.
void	BddEnc_reset_reordering_count (BddEnc_ptr self)
	Resets the reordering count. The value returned by any following call to method get_reordering_count will be relative to the moment this method had been called.
bdd_ptr	BddEnc_state_var_to_next_state_var (const BddEnc_ptr self, bdd_ptr bdd)
	Exchange next state variables for state variables.
add_ptr	BddEnc_state_var_to_next_state_var_add (const BddEnc_ptr self, add_ptr add)
	Exchange next state variables for state variables, in terms of ADD.
int	BddEnc_write_var_ordering (const BddEnc_ptr self, const char *oo_filename, const VarOrderingType dump_type)
	Writes on a file the variable order.

Detailed Description

BddEnc class definition derived from class BoolEncClient.

Public interface of class 'BddEnc'.

See also:: Base class BoolEncClient

Author:: Roberto Cavada Encoder for bdds, derived from class BoolEncClient

Definition of the public accessor for class BddEnc

Member Function Documentation

BddEnc::INHERITS_FROM ( BoolEncClient )

Friends And Related Function Documentation

void bdd_enc_deinit ( BddEnc_ptr self ) [related]

Todo:

void bdd_enc_init	(	BddEnc_ptr	self,
		SymbTable_ptr	symb_table,
		BoolEnc_ptr	bool_enc,
		VarsHandler_ptr	dd_vars_hdlr,
		OrdGroups_ptr	ord_groups
	)			`[related]`

Todo:

void bdd_enc_shuffle_variables_order	(	BddEnc_ptr	self,
		NodeList_ptr	vars
	)			`[related]`

Todo:

node_ptr BddEnc_add_to_expr	(	BddEnc_ptr	self,
		const add_ptr	add,
		SymbLayer_ptr	det_layer
	)			`[related]`

Converts a ADD into the corresponding (boolean) expression.

Takes an ADD with leaves FALSE, TRUE, or {FALSE,TRUE}.

The case of {FALSE,TRUE} leaves is determinized if a valid layer is passed, otherwise it is preserved.

Important: if a valid determinization layer is given, the layer cannot be alreay commited to the encoder, and will have to be possibly committed later if the returned expression is intended to be used by this encoder in terms of ADD or BDD.

Recurs down on the structure of the ADD, and maps each non terminal node into an if-then-else expression, maps FALSE and TRUE terminal nodes into true and false expressions, and maps {FALSE,TRUE} into a newly introduced variable to determinize the expression.

A new boolean variable can be declared within det_layer

See also:: bdd_enc_add2expr_recur

node_ptr BddEnc_add_to_scalar_expr	(	BddEnc_ptr	self,
		const add_ptr	add,
		SymbLayer_ptr	det_layer
	)			`[related]`

Converts a ADD into the corresponding (possibly scalar) expression.

Takes an ADD and converts it to the corresponding scalar expression.

Non deterministic leaves will be determinized only if a valid layer is passed. Important: if a valid determinization layer is given, the layer cannot be alreay commited to the encoder, and will have to be possibly committed later if the returned expression is intended to be used by this encoder in terms of ADD or BDD.

Recurs down on the structure of the ADD, and maps each non terminal node into an if-then-else expression

A new scalar variable may be declared within det_layer

See also:: bdd_enc_add2expr_recur

add_ptr BddEnc_apply_input_vars_mask_add	(	BddEnc_ptr	self,
		add_ptr	inputs
	)			`[related]`

Applies a mask to the given add which must contain only input variables.

Returned add is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

BddInputs BddEnc_apply_input_vars_mask_bdd	(	BddEnc_ptr	self,
		BddInputs	inputs
	)			`[related]`

Applies a mask to the given BDD which must contain only input variables.

Returned bdd is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

add_ptr BddEnc_apply_state_frozen_input_vars_mask_add	(	BddEnc_ptr	self,
		add_ptr	states_inputs
	)			`[related]`

Applies a mask to the given add which must contain frozen, state and input variables.

Returned add is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

BddStatesInputs BddEnc_apply_state_frozen_input_vars_mask_bdd	(	BddEnc_ptr	self,
		BddStatesInputs	states_inputs
	)			`[related]`

Applies a mask to the given BDD which must contain frozen, state and input variables.

Returned bdd is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

add_ptr BddEnc_apply_state_frozen_vars_mask_add	(	BddEnc_ptr	self,
		add_ptr	states
	)			`[related]`

Applies a mask to the given add which must contain only frozen and state variables.

Returned add is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

BddStates BddEnc_apply_state_frozen_vars_mask_bdd	(	BddEnc_ptr	self,
		BddStates	states
	)			`[related]`

Applies a mask to the given BDD which must contain only frozen and state variables.

Returned bdd is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

node_ptr BddEnc_assign_symbols	(	BddEnc_ptr	self,
		bdd_ptr	bdd,
		NodeList_ptr	symbols,
		boolean	onlyRequiredSymbs,
		bdd_ptr *	resultBdd
	)			`[related]`

This function is similar to BddEnc_print_set_of... functions except that instead of printing values of variables, this funtion creates a list of pairs var-itsValue.

This functions takes a BDD and a list of symbols (variables or defines, both can be wrapped in NEXT), and returns a list of (symb, symb_value) which makes BDD not false (input BDD) should not be false constant). Returned list is a list of AND nodes with Nil at the end. Every element is a EQUAL node with symbol on the left and its value on the right.

Order of symbols in the returned list is the same of provided symbols list. If parameter 'onlyRequiredSymbs' is true then symbols whose values are not constrained by provided BDD will be skipped. Otherwise, some legal arbitrary values for such symbols will be created and returned list will contain all the symbols from 'symbols'.

If parameter resultAssignment is not null pointer, then it returns the produced assignments in the form of BDD, i.e. a conjunct of all generated equations "symbol = itsValue".

The input BDD may or may not be a complete assignment. The invoker should free the returned list (with free_list) and returned BDD (if any). Note, that EQUAL nodes should not be freed/modified as created with find_node.

node_ptr BddEnc_bdd_to_expr	(	BddEnc_ptr	self,
		const bdd_ptr	bdd
	)			`[related]`

Converts a BDD into the corresponding (boolean) expression.

See also:: bdd_enc_add2expr_recur

node_ptr BddEnc_bdd_to_wff	(	BddEnc_ptr	self,
		bdd_ptr	bdd,
		NodeList_ptr	vars
	)			`[related]`

Converts a bdd into a Well Formed Formula representing it.

A new expression is built, that represents the formula given as the input bdd.

The list of variables is used to compute the scalar essentials. Note that only the following kinds of variables are allowed in this list.

1. Pure booleans (i.e. not part of an encoding) 2. Finite scalars (both ranged and words).

State, frozen and input variables are all allowed, no NEXT. (It will be part of this function's responsibility to add state variables' NEXTs as needed.

none

See also:: Bddenc_print_wff_bdd

void BddEnc_clean_evaluation_cache ( BddEnc_ptr self ) [related]

Clean the internal cache which contains the results of evaluation of expressions to ADD or BDD form.

NB: NuSMV option "enable_sexp2bdd_caching" allows to disable the cache completely

array_t * BddEnc_ComputePrimeImplicants	(	BddEnc_ptr	self,
		const array_t *	layer_names,
		bdd_ptr	formula
	)			`[related]`

Finds a set of prime implicants for a formula represented as a BDD.

Finds the set of prime implicants of a BDD b. Each element of the resulting array is a prime implicant of the BDD b. The prime implicant is represented as a list of pairs

(: <vname>

)

The meaning is that the variable <vname> is equal to

, i.e. <vname> =

. A further post-process of the result can write it in a better way, expecially for non boolean variables, where several prime implicants can be combined by writing complex predicates instead of simple equalities.

The list of layers can be declared for instance as:

char ** layers = {MODEL_LAYER_NAME, "BA_ABSTRACTION", NULL};

Where MODEL_LAYER_NAME is the name of the model layer, "BA_ABSTRACTION" is the name of a new user created layer. Very inportant is the NULL at the end to terminate the list.

This function needs more comment

None

add_ptr BddEnc_constant_to_add	(	const BddEnc_ptr	self,
		node_ptr	constant
	)			`[related]`

Returns the ADD leaf corresponding to the given atom.

Returns the ADD leaf corresponding to the given atom, if defined, NULL otherwise. The returned ADD - if any - is referenced. If the inner flag enforce_constant is set,

Suppose to have a declaration of this kind:

   VAR
   condition : {idle, stopped}

then in the constant hash for the atom idle there is the corresponding leaf ADD, i.e. the ADD whose value is the symbol idle.

double BddEnc_count_inputs_of_bdd	(	const BddEnc_ptr	self,
		bdd_ptr	bdd
	)			`[related]`

Return the number of inputs of a given BDD.

Return the number of inputs represented by a BDD.

double BddEnc_count_states_inputs_of_bdd	(	const BddEnc_ptr	self,
		bdd_ptr	bdd
	)			`[related]`

Return the number of states inputs of a given BDD.

Return the number of states inputs represented by a BDD. Note: states are represented by state and frozen variables

double BddEnc_count_states_of_add	(	const BddEnc_ptr	self,
		add_ptr	add
	)			`[related]`

Return the number of states of a given ADD.

Return the number of minterms (i.e. states) represented by an ADD. Note: states are represented by state and frozen variables

double BddEnc_count_states_of_bdd	(	const BddEnc_ptr	self,
		bdd_ptr	bdd
	)			`[related]`

Return the number of states of a given BDD.

Return the number of states represented by a BDD. Note: states are represented by state and frozen variables.

BddEnc_ptr BddEnc_create	(	SymbTable_ptr	symb_table,
		BoolEnc_ptr	bool_enc,
		VarsHandler_ptr	dd_vars_hndr,
		OrdGroups_ptr	ord_groups
	)			`[related]`

The BddEnc class constructor.

AutomaticStart

The BddEnc class constructor. ord_groups can be NULL if ordering is not used. self become the owner of the given ord_groups instance

See also:: BddEnc_destroy

VIRTUAL void BddEnc_destroy ( BddEnc_ptr self ) [related]

The BddEnc class destructor.

The BddEnc class destructor

See also:: BddEnc_create

int BddEnc_dump_addarray_davinci	(	BddEnc_ptr	self,
		AddArray_ptr	addarray,
		const char **	labels,
		FILE *	outfile
	)			`[related]`

Dumps the given AddArray in DAVINCI format.

Labels is an array of strings to be used as roots labels. The size of the array must be equal to the size of the AddArray. Returns 0 in case of success, 1 otherwise

int BddEnc_dump_addarray_dot	(	BddEnc_ptr	self,
		AddArray_ptr	addarray,
		const char **	labels,
		FILE *	outfile
	)			`[related]`

Dumps the given AddArray in DOT format.

Labels is an array of strings to be used as roots labels. The size of the array must be equal to the size of the AddArray. Returns 0 in case of success, 1 otherwise

int BddEnc_dump_expr	(	const BddEnc_ptr	self,
		const node_ptr	parsed_expr,
		const char *	str_constr,
		const t_format	format,
		FILE *	outfile
	)			`[related]`

Dumps an expression in the specified output format.

type check the expression, then convers to bdd and dumps

add_ptr BddEnc_eval_constant	(	BddEnc_ptr	self,
		Expr_ptr	expr,
		node_ptr	context
	)			`[related]`

Evaluates a constant expression.

Evaluate a constant expression. If the expression does not evaluate to a constant, then an internal error is generated. Returned add is referenced.

See also:: eval eval_num

int BddEnc_eval_num	(	BddEnc_ptr	self,
		node_ptr	e,
		node_ptr	context
	)			`[related]`

Evaluates a number in a context.

Evaluate the NUMBER represented by e in context context. NUMBERS can be encoded in different ways in different processes.

See also:: bdd_enc_eval

add_ptr BddEnc_eval_sign_add	(	BddEnc_ptr	self,
		add_ptr	a,
		int	flag
	)			`[related]`

Complements an ADD according to a flag.

Given the ADD a, this function returns the negation of ADD a or a itself according the value of flag. If flag = -1 then returns not a, else returns a. It is important that the ADD is a FALSE/TRUE ADD (i.e. it has only FALSE or TRUE as leaf).

See also:: bdd_enc_eval

bdd_ptr BddEnc_eval_sign_bdd	(	BddEnc_ptr	self,
		bdd_ptr	a,
		int	flag
	)			`[related]`

Complements a BDD according to a flag.

Given the BDD a, this function returns the negation of BDD a or a itself according the value of flag. If flag = -1 then returns not a, else returns a. It is important that the BDD has only FALSE or TRUE as leaves.

add_ptr BddEnc_expr_to_add	(	BddEnc_ptr	self,
		const Expr_ptr	expr,
		const node_ptr	context
	)			`[related]`

Returns the ADD representing the expression expr, in the given context.

Returned add is referenced. A NULL value of the provided expression (expr) corresponds to a true ADD returned as result.

NOTE: Mostly expressions must be type checked before being evaluated. For example, use TypeChecker_is_expression_wellformed to type check generated expression. FSM should be checked with TypeCheckingPkg_check_constrains, and a property should be checked with TypeCheckingPkg_check_property

AddArray_ptr BddEnc_expr_to_addarray	(	BddEnc_ptr	self,
		const Expr_ptr	expr,
		const node_ptr	context
	)			`[related]`

Returns the ADD array representing the expression expr, in the given context.

Each element of the returned add array is referenced. A NULL value of the provided expression (expr) corresponds to a true ADD array returned as result.

The returned array will belong to the invoker.

NOTE: Mostly expressions must be type checked before being evaluated. For example, use TypeChecker_is_expression_wellformed to type check generated expression. FSM should be checked with TypeCheckingPkg_check_constrains, and a property should be checked with TypeCheckingPkg_check_property

bdd_ptr BddEnc_expr_to_bdd	(	BddEnc_ptr	self,
		const Expr_ptr	expr,
		const node_ptr	context
	)			`[related]`

Returns the BDD representing the expression expr, in the given contex.

Returned bdd is referenced.

NOTE: Mostly expressions must be type checked before being evaluated. For example, use TypeChecker_is_expression_wellformed to type check generated expression. FSM should be checked with TypeCheckingPkg_check_constrains, and a property should be checked with TypeCheckingPkg_check_property

void BddEnc_force_order	(	BddEnc_ptr	self,
		OrdGroups_ptr	new_po_grps
	)			`[related]`

Forces a variable ordering in the BDD encoding.

It takes an OrdGroups structure representing the possibly partial ordering and the routine complete it with the possible missing variables. It is assumed all the variables in the given ordering group have been previously allocated within the BDD package.

void BddEnc_force_order_from_file	(	BddEnc_ptr	self,
		FILE *	orderfile
	)			`[related]`

Forces a variable ordering in the BDD encoding reading it from a file.

It reads an order file and then forces it within the BDD package. The order file may be partial. Thanks to BddEnc_force_order the ordering is completed with the possible missing variables.

See also:: BddEnc_force_order

DDMgr_ptr BddEnc_get_dd_manager ( const BddEnc_ptr self ) [related]

Gets the DD manager this encoding refers to.

VarsHandler_ptr BddEnc_get_dd_vars_handler ( const BddEnc_ptr self ) [related]

Gets the DD vars handler this encoding refers to.

BddVarSet_ptr BddEnc_get_frozen_vars_cube ( const BddEnc_ptr self ) [related]

Gets the support of the set of frozen variables.

Returned bdd is referenced, the caller must free it after it is no longer used. Result is cached if not previously converted from internal ADD representation. Returns NULL if an error occurred.

BddVarSet_ptr BddEnc_get_input_vars_cube ( const BddEnc_ptr self ) [related]

Gets the support of the set of input variables.

Returned bdd is referenced, the caller must free it after it is no longer used. Result is cached if not previously converted from internal ADD representation. Returns NULL if an error occurred.

add_ptr BddEnc_get_input_vars_mask_add ( BddEnc_ptr self ) [related]

Returns the mask (as an ADD) in terms of input variables.

Returned add is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

bdd_ptr BddEnc_get_input_vars_mask_bdd ( BddEnc_ptr self ) [related]

Returns the mask (as BDD) in terms of input variables.

Returned bdd is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

BddVarSet_ptr BddEnc_get_layer_vars_cube	(	const BddEnc_ptr	self,
		SymbLayer_ptr	layer,
		SymbFilterType	vt
	)			`[related]`

Given a layer the function produces a cube of all layer's variables.

vt can be a combination of VFT_CURRENT, VFT_NEXT, VFT_FROZEN, VFT_INPUT (see SymbFilterType for combination shortcuts). Returned bdd is referenced, the caller must free it after it is no longer used.

double BddEnc_get_minterms_of_add	(	const BddEnc_ptr	self,
		add_ptr	add
	)			`[related]`

Return the number of minterms of a given ADD.

Return the number of minterms represented by a ADD.

double BddEnc_get_minterms_of_bdd	(	const BddEnc_ptr	self,
		bdd_ptr	bdd
	)			`[related]`

Return the number of minterms of a given BDD.

Return the number of minterms represented by a BDD.

BddVarSet_ptr BddEnc_get_next_state_vars_cube ( const BddEnc_ptr self ) [related]

Gets the support of the set of next-state variables.

Returned bdd is referenced, the caller must free it after it is no longer used. Result is cached if not previously converted from internal ADD representation. Returns NULL if an error occurred.

OrdGroups_ptr BddEnc_get_ord_groups ( const BddEnc_ptr self ) [related]

Returns the internally used order that was specified when creating the instance. Order is used when committing a layer and when forcing a reordering.

Can be NULL. The returned instance belongs to self. Do not change it if you do not know well what you are doing.

int BddEnc_get_reordering_count ( const BddEnc_ptr self ) [related]

Returns the number of reorderings that have been carried out since either the self construction or the last call to method reset_reordering_count.

Returns the number of reorderings performed by CUDD since the instance creation, or since the last call to method reset_reordering_count. Explicit and auto-triggered reorderings are counted. Notice that forced ordering due to layers commitment may increment the orderings count.

See also:: BddEnc_reset_reordering_count

add_ptr BddEnc_get_state_frozen_input_vars_mask_add ( BddEnc_ptr self ) [related]

Returns the mask (as ADD) in terms of state, frozen and input variables.

Returned add is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

bdd_ptr BddEnc_get_state_frozen_input_vars_mask_bdd ( BddEnc_ptr self ) [related]

Returns the mask (as BDD) in terms of frozen, state and input variables.

Returned bdd is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

BddVarSet_ptr BddEnc_get_state_frozen_vars_cube ( const BddEnc_ptr self ) [related]

Gets the support of the set of state and frozen variables.

The result is a conjunct of BddEnc_get_state_vars_cube and BddEnc_get_frozen_vars_cube.

Returned bdd is referenced, the caller must free it after it is no longer used. Result is cached if not previously converted from internal ADD representation. Returns NULL if an error occurred.

add_ptr BddEnc_get_state_frozen_vars_mask_add ( BddEnc_ptr self ) [related]

Returns the mask (as an ADD) in terms of frozen and state variables.

Returned add is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

bdd_ptr BddEnc_get_state_frozen_vars_mask_bdd ( BddEnc_ptr self ) [related]

Returns the mask (as BDD) in terms of frozen and state variables.

Returned bdd is referenced. Calculated mask will be cached for future use. The mask will be applicable only to variable that occur within the layers committed to self

BddVarSet_ptr BddEnc_get_state_next_state_frozen_vars_cube ( const BddEnc_ptr self ) [related]

Gets the support of the set of state, next state and frozen variables.

The result is a conjunction of BddEnc_get_state_frozen_vars_cube and BddEnc_get_next_state_vars_cube.

Returned bdd is referenced, the caller must free it after it is no longer used. Returns NULL if an error occurred.

BddVarSet_ptr BddEnc_get_state_vars_cube ( const BddEnc_ptr self ) [related]

Gets the support of the set of state variables.

Returned bdd is referenced, the caller must free it after it is no longer used. Result is cached if not previously converted from internal ADD representation. Returns NULL if an error occurred.

AddArray_ptr BddEnc_get_symbol_add	(	BddEnc_ptr	self,
		node_ptr	name
	)			`[related]`

Given a variable, define or process constant the corresponding ADD array is returned.

Given an identifier (as an expanded identifier name), this function returns the ADD array of its definition, or NULL if not defined. If the variable is of a Word type then the returned array may contain several elements (ADDs). For all other kinds of expressions only one element can be in the array. Errors occurs if the identifier is a define which is circularly declared. The returned array will belong to the invoker.

See also:: BddEnc_expr_to_add

BddVarSet_ptr BddEnc_get_unfiltered_vars_cube	(	const BddEnc_ptr	self,
		Set_t	vars
	)			`[related]`

Given a set of variables the function produces a cube of all of them.

this function is similar to BddEnc_get_vars_cube with 2 differences: 1. all variables in 'vars' are put into the result cube 2. in order to compute next-state variable bits of variable V 'vars' has to contain NEXT(V).

Returned bdd is referenced, the caller must free it after it is no longer used.

int BddEnc_get_var_index_from_name	(	const BddEnc_ptr	self,
		node_ptr	name
	)			`[related]`

Returns the DD index of the given variable.

The input variable should be boolean

required

See also:: BddEnc_get_var_name_from_index

add_ptr BddEnc_get_var_mask	(	BddEnc_ptr	self,
		node_ptr	var_name
	)			`[related]`

Given a variable, it returns the mask of its encoding.

Returns the mask that removes repetitions of leaves in a variable encoding. Returned ADD is referenced. Automatic reordering, if enabled, is temporary disabled during this computation.

node_ptr BddEnc_get_var_name_from_index	(	const BddEnc_ptr	self,
		int	index
	)			`[related]`

Given a variable index, this method return the symbolic name of the correpsonding variable.

required

See also:: BddEnc_get_var_index_from_name

NodeList_ptr BddEnc_get_var_ordering	(	const BddEnc_ptr	self,
		const VarOrderingType	ord_type
	)			`[related]`

Todo:

BddVarSet_ptr BddEnc_get_vars_cube	(	const BddEnc_ptr	self,
		Set_t	vars,
		SymbFilterType	vt
	)			`[related]`

Given a set of variables the function produces a cube of them filtering out some of them.

vt is a filter and can be a combination of VFT_CURRENT, VFT_NEXT, VFT_FROZEN, VFT_INPUT (see SymbFilterType for combination shortcuts). vars has to contain variables only without NEXT or anything else. E.g. if vars contains state var V and vt includes VFT_CURRENT and VFT_NEXT then the result will contains both current and next bits of V.

Returned bdd is referenced, the caller must free it after it is no longer used.

NodeList_ptr BddEnc_get_vars_in_cube	(	const BddEnc_ptr	self,
		bdd_ptr	cube,
		node_ptr	list_of_sym,
		boolean	include_next
	)			`[related]`

Returns the symbolic names of boolean variables stored in a cube.

Given a cube of boolean BDD variables, this function returns the list of symbolic names of the corresponding variables. If NEXT variables are also found in the cube, and include_next is true, NEXT variables will be also checked, even if not occurring explicitly in the input list.

Returned list must be disposed by the caller.

boolean BddEnc_has_var_at_index	(	const BddEnc_ptr	self,
		int	index
	)			`[related]`

Given a variable index, this method return true iff the given variable belongs to the encoder.

required

See also:: BddEnc_get_var_name_from_index

boolean BddEnc_is_var_in_cube	(	const BddEnc_ptr	self,
		node_ptr	name,
		add_ptr	cube
	)			`[related]`

Returns true if the variable is in the cube and false otherwise.

Parameter name is a fully-resolved name of variable. The cube of this variable is subtracted from the cube given in 'cube' parameter, and the result is compared with the original 'cube'. If they are different then at least a part (one bit, for example) of the variable is in the input cube. Therefore true is returned.

bdd_ptr BddEnc_next_state_var_to_state_var	(	const BddEnc_ptr	self,
		bdd_ptr	bdd
	)			`[related]`

Exchange state variables for next state variables.

Given a BDD whose variables are NEXT-STATE variables, returns an isomorphic BDD where STATE variables have been substituted for the corrisponding STATE variables

add_ptr BddEnc_next_state_var_to_state_var_add	(	const BddEnc_ptr	self,
		add_ptr	add
	)			`[related]`

Exchange state variables for next state variables in terms of ADD.

Given an ADD whose variables are NEXT-STATE variables, returns an isomorphic ADD where STATE variables have been substituted for the corrisponding STATE variables

boolean BddEnc_pick_all_terms_inputs	(	const BddEnc_ptr	self,
		bdd_ptr	bdd,
		bdd_ptr *	result_array,
		const int	array_len
	)			`[related]`

Returns the array of All Possible Minterms.

Takes a minterm and returns an array of all its terms, according to internally kept vars. Notice that the array of the result has to be previously allocated, and its size must be greater or equal the number of the minterms. The returned array contains referenced BDD so it is necessary to dereference them after their use. Returns true if an error occurred

result_array will change

See also:: bdd_pick_all_terms

boolean BddEnc_pick_all_terms_states	(	const BddEnc_ptr	self,
		bdd_ptr	bdd,
		bdd_ptr *	result_array,
		const int	array_len
	)			`[related]`

Returns the array of All Possible Minterms.

Takes a minterm and returns an array of all its terms, according to internally kept vars. Notice that the array of the result has to be previously allocated, and its size must be greater or equal the number of the minterms. The returned array contains referenced BDD so it is necessary to dereference them after their use. Returns true if an error occurred.

Note: states are represented by state and frozen variables.

result_array will change

See also:: bdd_pick_all_terms

boolean BddEnc_pick_all_terms_states_inputs	(	const BddEnc_ptr	self,
		bdd_ptr	bdd,
		bdd_ptr *	result_array,
		const int	array_len
	)			`[related]`

Returns the array of All Possible Minterms.

Takes a minterm and returns an array of all its terms, according to internally kept vars. Notice that the array of the result has to be previously allocated, and its size must be greater or equal the number of the minterms. The returned array contains referenced BDDs so it is necessary to dereference them after their use. Returns true if an error occurred.

Note: states are represented by state and frozen variables.

result_array will change

See also:: bdd_pick_all_terms

bdd_ptr BddEnc_pick_one_input	(	const BddEnc_ptr	self,
		bdd_ptr	inputs
	)			`[related]`

Extracts a minterm from a given BDD.

Extracts a minterm from a given BDD. Returned bdd is referenced

See also:: bdd_pick_one_minterm

bdd_ptr BddEnc_pick_one_input_rand	(	const BddEnc_ptr	self,
		bdd_ptr	inputs
	)			`[related]`

Extracts a random minterm from a given BDD.

Extracts a random minterm from a given BDD. Returned bdd is referenced

See also:: bdd_pick_one_minterm_rand

bdd_ptr BddEnc_pick_one_input_state	(	const BddEnc_ptr	self,
		bdd_ptr	inputs_states
	)			`[related]`

Extracts a minterm over input/state variables from a given BDD.

Extracts a minterm from a given BDD. Returned bdd is referenced. Note: input-states are represented by input, state and frozen variables.

See also:: bdd_pick_one_minterm, BddEnc_pick_one_state, BddEnc_pick_one_input

bdd_ptr BddEnc_pick_one_input_state_rand	(	const BddEnc_ptr	self,
		bdd_ptr	inputs_states
	)			`[related]`

Extracts a random minterm from a given BDD.

Extracts a random minterm from a given BDD. Returned bdd is referenced.

Note: input-states are represented by input, state and frozen variables.

See also:: bdd_pick_one_minterm_rand, BddEnc_pick_one_input_rand, BddEnc_pick_one_state_rand

bdd_ptr BddEnc_pick_one_state	(	const BddEnc_ptr	self,
		bdd_ptr	states
	)			`[related]`

Extracts a minterm from a given BDD.

Extracts a minterm from a given BDD. Returned bdd is referenced. Note: states are represented by state and frozen variables.

See also:: bdd_pick_one_minterm

bdd_ptr BddEnc_pick_one_state_rand	(	const BddEnc_ptr	self,
		bdd_ptr	states
	)			`[related]`

Extracts a random minterm from a given BDD.

Extracts a random minterm from a given BDD. Returned bdd is referenced.

Note: states are represented by state and frozen variables.

See also:: bdd_pick_one_minterm_rand

int BddEnc_print_bdd	(	BddEnc_ptr	self,
		bdd_ptr	bdd,
		VPFBEFNNV	p_fun,
		OStream_ptr	file,
		void *	arg
	)			`[related]`

Prints the given bdd. In particular prints only the symbols occuring in the symbols list passed to print_bdd_begin. Individual assignments may be printed using a user-defined function, passed as a parameter.

Before calling this method, you must call print_bdd_begin. Then you can call this method once or more, but eventually you will have to call print_bdd_end to commit. Returns the number of symbols actually printed

void BddEnc_print_bdd_begin	(	BddEnc_ptr	self,
		NodeList_ptr	symbols,
		boolean	changes_only
	)			`[related]`

Call before a group of BddEnc_print_bdd calls.

This sets some fileds used by BddEnc_print_bdd. Also clears the table used when printing only changed states. After having called BddEnc_print_bdd, call BddEnc_print_bdd_end. If changes_only is true, than only state and frozen variables which assume a different value from the previous printed one are printed out.

void BddEnc_print_bdd_end ( BddEnc_ptr self ) [related]

Must be called after each call to BddEnc_print_bdd_begin.

Must be called after each call to BddEnc_print_bdd_begin, in order to clean up some internal structure

void BddEnc_print_bdd_wff	(	BddEnc_ptr	self,
		bdd_ptr	bdd,
		NodeList_ptr	vars,
		boolean	do_sharing,
		boolean	do_indent,
		int	start_at_column,
		OStream_ptr	out
	)			`[related]`

Prints a BDD as a Well Formed Formula using optional sharing.

The bdd representing the formula to be printed is first converted to a wff.

If sharing is required optimizations are performed on the printout.

If indentation is required, the start_at_column integer offset is used to determine the starting indenting offset to print the expression.

prints the expression on the given stream.

See also:: BddEnc_bdd_to_wff

void BddEnc_print_formula_info	(	BddEnc_ptr	self,
		Expr_ptr	formula,
		boolean	print_models,
		boolean	print_formula,
		OStream_ptr	out
	)			`[related]`

Prints statistical information of a formula.

Prints statistical information about a given formula. It is computed taking care of the encoding and of the indifferent variables in the encoding.

void BddEnc_print_set_of_inputs	(	BddEnc_ptr	self,
		bdd_ptr	inputs,
		boolean	changes_only,
		VPFBEFNNV	p_fun,
		OStream_ptr	file,
		void *	arg
	)			`[related]`

Prints a set of input pairs. Individual assignments may be printed using a user-defined function, passed as a parameter.

void BddEnc_print_set_of_state_input_pairs	(	BddEnc_ptr	self,
		bdd_ptr	state_input_pairs,
		boolean	changes_only,
		VPFBEFNNV	p_fun,
		OStream_ptr	file,
		void *	arg
	)			`[related]`

Prints a set of state-input pairs. Individual assignments may be printed using a user-defined function, passed as a parameter.

Note: states are represented by state and frozen variables

void BddEnc_print_set_of_states	(	BddEnc_ptr	self,
		bdd_ptr	states,
		boolean	changes_only,
		boolean	print_defines,
		VPFBEFNNV	p_fun,
		OStream_ptr	file,
		void *	arg
	)			`[related]`

Prints a set of states. Individual assignments may be printed using a user-defined function, passed as a parameter.

Note: states are represented by state and frozen variables

void BddEnc_print_set_of_trans_models	(	BddEnc_ptr	self,
		bdd_ptr	state_input_pairs,
		OStream_ptr	file
	)			`[related]`

Prints a set of models for given trans.

none

void BddEnc_print_vars_in_cube	(	BddEnc_ptr	self,
		bdd_ptr	cube,
		node_ptr	list_of_sym,
		OStream_ptr	file
	)			`[related]`

Prints out the symbolic names of boolean variables stored in a cube.

Given a cube of boolean BDD variables, this function prints out the symbolic names of the corresponding variables. The symbolic name of the variables to be printed out are listed in list_of_sym.

None

void BddEnc_reset_reordering_count ( BddEnc_ptr self ) [related]

Resets the reordering count. The value returned by any following call to method get_reordering_count will be relative to the moment this method had been called.

See also:: BddEnc_get_reordering_count

bdd_ptr BddEnc_state_var_to_next_state_var	(	const BddEnc_ptr	self,
		bdd_ptr	bdd
	)			`[related]`

Exchange next state variables for state variables.

Given a BDD whose variables are STATE variables, returns an isomorphic BDD where NEXT-STATE variables have been substituted for the corrisponding STATE variables

add_ptr BddEnc_state_var_to_next_state_var_add	(	const BddEnc_ptr	self,
		add_ptr	add
	)			`[related]`

Exchange next state variables for state variables, in terms of ADD.

Given an ADD whose variables are STATE variables, returns an isomorphic ADD where NEXT-STATE variables have been substituted for the corrisponding STATE variables

int BddEnc_write_var_ordering	(	const BddEnc_ptr	self,
		const char *	oo_filename,
		const VarOrderingType	dump_type
	)			`[related]`

Writes on a file the variable order.

This function writes the variable order currently in use in the system in the specified output file. The file generated as output can be used as input order file for next computations. If the specified output file is an empty string ("" or NULL, see util_is_string_null) output is redirected to stdout. The output content depends on the value of dump_type, and can be either pure scalar (for backward compatibility) or single bits

Ownership of "output_order_file_name" is taken, unless it is the value returned by get_output_order_file