-
BddEnc.c
- The BddEnc implementation
-
BddEncCache.c
- The BddEncCache class implementation
BddEnc.c
The BddEnc implementation
By: Roberto Cavada
This file contains the implementation of a wrapper of (a part
of) the BddEnc API onto the NuSMV code structure.
Only functions needed by the BddFsm are provided.
See AlsoBddEnc.h
-
BddEnc_create()
- Constructor
-
BddEnc_destroy()
- Destructor
-
BddEnc_push_status_and_reset()
- Saves the state of self. This is a feature used by
bdd-based ltl model checking. Also prepares self for a new encoding
-
BddEnc_pop_status()
- Restores the state of self previously saved with
BddEnc_push_status_and_reset. This is a feature used by bdd-based ltl
model checking
-
BddEnc_get_dd_manager()
- Gets the DD manager this encoding refers to.
-
BddEnc_get_symbolic_encoding()
-
-
BddEnc_get_state_vars_support()
- Gets the support of the set of state variables
-
BddEnc_get_next_state_vars_support()
- Gets the support of the set of next-state variables
-
BddEnc_get_input_vars_support()
- Gets the support of the set of input variables
-
BddEnc_expr_to_add()
- Returns the ADD representing the expression "v"
-
BddEnc_expr_to_bdd()
- Returns the BDD representing the expression "v"
-
BddEnc_state_var_to_next_state_var_add()
- Exchange next state variables for state variables, in
terms of ADD
-
BddEnc_next_state_var_to_state_var_add()
- Exchange state variables for next state variables in terms
of ADD
-
BddEnc_state_var_to_next_state_var()
- Exchange next state variables for state variables
-
BddEnc_next_state_var_to_state_var()
- Exchange state variables for next state variables
-
BddEnc_get_ordering()
- Return the list of variables corresponding
to the current order of variables in the encoding
-
BddEnc_print_bdd_begin()
- Call before a group of BddEnc_print_bdd calls
-
BddEnc_print_bdd_end()
- Must be called after each call to
BddEnc_print_bdd_begin
-
BddEnc_print_bdd()
- Prints the given bdd. In particular prints only the
symbols occuring in the symbols list passed to print_bdd_begin
-
BddEnc_print_set_of_states()
- Prints a set of states
-
BddEnc_print_set_of_inputs()
- Prints a set of input pairs
-
BddEnc_print_set_of_state_input_pairs()
- Prints a set of state-input pairs
-
BddEnc_print_vars_in_cube()
- Prints out the symbolic names of boolean
variables stored in a cube.
-
BddEnc_count_states_of_add()
- Return the number of states of a given ADD.
-
BddEnc_count_states_of_bdd()
- Return the number of states of a given BDD.
-
BddEnc_count_inputs_of_bdd()
- Return the number of inputs of a given BDD.
-
BddEnc_count_states_inputs_of_bdd()
- Return the number of states inputs of a given BDD.
-
BddEnc_get_minterms_of_add()
- Return the number of minterms of a given ADD.
-
BddEnc_get_minterms_of_bdd()
- Return the number of minterms of a given BDD.
-
BddEnc_pick_one_state()
- Extracts a minterm from a given BDD.
-
BddEnc_pick_one_input()
- Extracts a minterm from a given BDD.
-
BddEnc_pick_all_terms_states_inputs()
- Returns the array of All Possible Minterms
-
BddEnc_pick_all_terms_states()
- Returns the array of All Possible Minterms
-
BddEnc_pick_all_terms_inputs()
- Returns the array of All Possible Minterms
-
BddEnc_pick_one_state_rand()
- Extracts a random minterm from a given BDD.
-
BddEnc_pick_one_input_rand()
- Extracts a random minterm from a given BDD.
-
BddEnc_get_var_name_from_dd_index()
- required
-
BddEnc_get_var_index_from_name()
- Returns the DD index of the given variable
-
BddEnc_constant_to_add()
- Returns the ADD leaf corresponding to the given atom
-
BddEnc_merge()
- Merges the previously saved bdds (and other parts)
and the current encoding
-
BddEnc_eval_sign_add()
- Complements an ADD according to a flag.
-
BddEnc_eval_sign_bdd()
- Complements a BDD according to a flag.
-
BddEnc_eval_num()
- Evaluates a number in a context.
-
BddEnc_eval_constant()
- Evaluates a constant expression.
-
BddEnc_get_symbol_add()
- Given a symbol, the corresponding ADD is returned.
-
BddEnc_get_state_vars_add_list()
- Returnes a list of ADDs corresponding to the model state
vars
-
BddEnc_write_order()
- Writes on a file the variable order.
-
BddEnc_get_state_vars_mask_add()
- Returns the mask (as ADD) in terms of state
variables
-
BddEnc_get_input_vars_mask_add()
- Returns the mask (as ADD) in terms of input variables
-
BddEnc_get_state_input_vars_mask_add()
- Returns the mask (as ADD) in terms of state and
input variables
-
BddEnc_get_state_vars_mask_bdd()
- Returns the mask (as BDD) in terms of state variables
-
BddEnc_get_input_vars_mask_bdd()
- Returns the mask (as BDD) in terms of input variables
-
BddEnc_get_state_input_vars_mask_bdd()
- Returns the mask (as BDD) in terms of state and input
variables
-
BddEnc_apply_state_vars_mask_add()
- Applies a mask to the given add which must contain only
state variables
-
BddEnc_apply_input_vars_mask_add()
- Applies a mask to the given add which must contain only
input variables
-
BddEnc_apply_state_input_vars_mask_add()
- Applies a mask to the given add which must contain
state and input variables
-
BddEnc_apply_state_vars_mask_bdd()
- Applies a mask to the given BDD which must contain only
state variables
-
BddEnc_apply_input_vars_mask_bdd()
- Applies a mask to the given BDD which must contain only
input variables
-
BddEnc_apply_state_input_vars_mask_bdd()
- Applies a mask to the given BDD which must contain
state and input variables
-
BddEnc_get_var_name_mask()
- Given a variable name, returns the mask of its encoding
-
BddEnc_get_var_encoding_mask()
- Given a variable encoding, returns the correponding mask
-
bdd_enc_init()
- Partial initializer. Call BddEnc_encode_vars to
complete
-
bdd_enc_deinit()
- Private method called by the destructor
-
bdd_enc_add_input_var_to_minterm_vars()
- Adds an input variable to the array necessary to
extract minterms from a BDD.
-
bdd_enc_add_state_var_to_minterm_vars()
- Adds an input variable to the array necessary to
extract minterms from a BDD.
-
bdd_enc_add_next_state_var_to_minterm_vars()
- Adds an input variable to the array necessary to
extract minterms from a BDD.
-
bdd_enc_add_state_var()
- Adds a new boolean variable to the DD package.
-
bdd_enc_add_input_var()
- Adds a new boolean variable to the DD package.
-
bdd_enc_set_input_variables_add()
- Private method. Set internal members
-
bdd_enc_accumulate_input_variables_cube()
-
-
bdd_enc_set_state_variables_add()
- Private method. Set internal members
-
bdd_enc_accumulate_state_variables_cube()
-
-
bdd_enc_set_next_state_variables_add()
- Private method. Set internal members
-
bdd_enc_accumulate_next_state_variables_cube()
-
-
bdd_enc_get_input_variables_add()
- Private accessor
-
bdd_enc_get_state_variables_add()
- Private accessor
-
bdd_enc_get_next_state_variables_add()
- Private accessor
-
bdd_enc_eval()
- Given an expression the corresponding ADD is
returned back.
-
bdd_enc_eval_recur_case_atom()
- Performs the recursive step of the
eval
function.
-
bdd_enc_eval_recur_case_dot_array()
-
-
bdd_enc_eval_recur()
-
-
bdd_enc_unary_op()
- Applies unary operation.
-
bdd_enc_binary_op()
- Applies binary operation.
-
bdd_enc_ternary_op()
- Applies ternary operation.
-
bdd_enc_quaternary_op()
- Applies quaternary operation.
-
bdd_enc_if_then_else_op()
- Evaluates if_then_else expressions returning
the ADD representing IF ifarg THEN thenarg ELSE elsarg.
-
bdd_enc_pre_encode()
-
-
bdd_enc_begin_group()
- Call *before* adding one or more new variables.
Then, call end_group
-
bdd_enc_end_group()
- Call to create a variables group
-
hash_bdd_free()
- Private service
-
hash_node_free()
- Private service
-
bdd_enc_get_var_mask_add_recur()
- Calculates the mask of the var encoding passed as
argument
-
bdd_enc_get_vars_list_mask()
- Given a list of variables, it returns the corresponding
mask
BddEncCache.c
The BddEncCache class implementation
By: Roberto Cavada
See AlsoBddEncCache.h
-
BddEncCache_create()
-
-
BddEncCache_destroy()
-
-
()
- Saves and reset the given hash member
-
BddEncCache_push_status_and_reset()
-
-
()
- Saves and reset the given hash member
-
BddEncCache_pop_status()
-
-
BddEncCache_new_constant()
-
-
BddEncCache_is_constant_defined()
-
-
BddEncCache_lookup_constant()
- Returns the ADD corresponding to the given constant, or
NULL if not defined
-
BddEncCache_new_var()
-
-
BddEncCache_is_var_defined()
-
-
BddEncCache_lookup_var()
-
-
BddEncCache_set_definition()
-
-
BddEncCache_get_definition()
-
-
BddEncCache_set_evaluation()
-
-
BddEncCache_get_evaluation()
-
-
bdd_enc_cache_init()
- Private initializer
-
bdd_enc_cache_deinit()
- Private deinitializer
-
hash_free_add_evaluating()
- Private micro function used when destroying caches of
adds
-
hash_dup_add()
- Private micro function used when copying caches of adds
Last updated on 2005/07/18 15h:58