void
Enc_add_commands(
)
- SideEffects [
- See Also
Enc_init_encodings
void
Enc_append_bit_to_sorted_list(
SymbTable_ptr symb_table,
NodeList_ptr sorted_list,
node_ptr var,
node_ptr* sorting_cache
)
- The higher bits are added to the beginning of the
list and lower bits are added at the end. The boolean variables
are added at the beginning of the list before the bits.
A new element is added at the end of the group of equal elements,
e.g. a boolean var is added after existing boolean vars but before
the bit vars.
Parameter 'sorting_cache' is used to speed up insertion (sorting a
list will be linear instead of quadratic). Initially
'sorting_cache' has to point to a pointer which points to Nil and
sorted_list has to be an empty list. It is the invoker
responsibility to free the sorted list and cache (with free_list)
after last invoking Enc_append_bit_to_sorted_list (the same
sorting_cache and sorted_list can be used for several runs of this
function).
const char*
Enc_bdd_static_order_heuristics_to_string(
BddSohEnum value
)
- Returned string does not have to be freed
BddEnc_ptr
Enc_get_bdd_encoding(
)
-
BeEnc_ptr
Enc_get_be_encoding(
)
-
BoolEnc_ptr
Enc_get_bool_encoding(
)
-
const char*
Enc_get_valid_bdd_static_order_heuristics(
)
- Returned string does not have to be freed
const char*
Enc_get_valid_vars_ord_types(
)
- Returned string does not have to be freed
void
Enc_init_bdd_encoding(
)
- Initializes the bdd enc for this session
void
Enc_init_be_encoding(
)
- Initializes the be enc for this session
void
Enc_init_bool_encoding(
)
- Call it to initialize for the current session the
encoding, before flattening. In the current implementation, you must
call this *before* the flattening phase. After the flattening,
you must initialize the bdd encoding as well, and after you created the
boolean sexp fsm, you must reinitialize the bdd encodings by calling
Enc_reinit_bdd_encoding. Don't forget to call Enc_quit_encodings when
the session ends.
- See Also
Enc_init_bdd_encoding
Enc_reinit_bdd_encoding
Enc_quit_encodings
void
Enc_init_encodings(
)
- This function initializes only data-structures
global to all encoding.
To initialize particular incoding, you have to invoke corresponding
init-functions, such as Enc_init_bool_encoding, etc.
- See Also
Enc_init_bool_encoding
Enc_init_bdd_encoding
Enc_reinit_bdd_encoding
Enc_quit_encodings
void
Enc_quit_encodings(
)
- Call to destroy encodings, when session ends.
Enc_init_encodings had to be called before calling this function.
void
Enc_set_bdd_encoding(
BddEnc_ptr enc
)
- Set the global bdd encoding. If enc is NULL,
previously set encoder is detroyed before the new assignment
void
Enc_set_be_encoding(
BeEnc_ptr enc
)
- Set the global be encoding. If enc is NULL,
previoulsy set encoder is detroyed before the new assignment
void
Enc_set_bool_encoding(
BoolEnc_ptr benc
)
- Set the global boolean encoding. If benc is NULL
previous encoder is detroyed before the new assignment
BddSohEnum
Enc_string_to_bdd_static_order_heuristics(
const char* str
)
- BDD_STATIC_ORDER_HEURISTICS_ERROR is returned when the
string does not match the given string
VarsOrdType
Enc_string_to_vars_ord(
const char* str
)
- VARS_ORD_UNKNOWN is returned when the string does not
match the given string
const char*
Enc_vars_ord_to_string(
VarsOrdType vot
)
- Returned string does not have to be freed
void
enc_construct_bdd_order_statically(
FlatHierarchy_ptr flat_hierarchy,
OrdGroups_ptr ord_groups
)
- Shell variable vars_order_type is use to infer the initial order
to begin the analysis. Then analyzing the flattened model and using heuristics
the order is tried to improve.
The kind of heuristics to be used is defined by shell variable
bdd_static_order_heuristics.
The final order is returned in ord_groups which has to be empty at
the beginning.