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.


Last updated on 2011/04/06 21h:16