void 
BddTrans_apply_synchronous_product(
  BddTrans_ptr  self, 
  const BddTrans_ptr  other, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube, 
  bdd_ptr  next_state_vars_cube 
)
The result goes into self and contained forward and backward cluster lists would be rescheduled. Other will remain unchanged.

Side Effects self will change

Defined in BddTrans.c 

BddTrans_ptr 
BddTrans_create(
  DdManager* dd_manager, 
  const ClusterList_ptr  clusters_bdd, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube, 
  bdd_ptr  next_state_vars_cube, 
  const TransType  trans_type, 
  const ClusterOptions_ptr  cl_options 
)
None of given arguments will become owned by self. You should destroy cl_options by yourself.

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_backward_image_state_input(
  const BddTrans_ptr  self, 
  bdd_ptr  s 
)
Returned bdd is referenced

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_backward_image_state(
  const BddTrans_ptr  self, 
  bdd_ptr  s 
)
Returned bdd is referenced

Defined in BddTrans.c 

ClusterList_ptr 
BddTrans_get_backward(
  const BddTrans_ptr  self 
)
self keeps the ownership of the returned instance.

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_forward_image_state_input(
  const BddTrans_ptr  self, 
  bdd_ptr  s 
)
Returned bdd is referenced

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_forward_image_state(
  const BddTrans_ptr  self, 
  bdd_ptr  s 
)
Returned bdd is referenced

Side Effects self keeps the ownership of the returned instance.

Defined in BddTrans.c 

ClusterList_ptr 
BddTrans_get_forward(
  const BddTrans_ptr  self 
)
self keeps the ownership of the returned instance.

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_k_backward_image_state_input(
  const BddTrans_ptr  self, 
  bdd_ptr  s, 
  int  k 
)
Returned bdd is referenced

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_k_backward_image_state(
  const BddTrans_ptr  self, 
  bdd_ptr  s, 
  int  k 
)
Returned bdd is referenced

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_k_forward_image_state_input(
  const BddTrans_ptr  self, 
  bdd_ptr  s, 
  int  k 
)
Returned bdd is referenced

Defined in BddTrans.c 

bdd_ptr 
BddTrans_get_k_forward_image_state(
  const BddTrans_ptr  self, 
  bdd_ptr  s, 
  int  k 
)
Returned bdd is referenced

Side Effects self keeps the ownership of the returned instance.

Defined in BddTrans.c 

void 
BddTrans_print_short_info(
  const BddTrans_ptr  self, 
  FILE* file 
)
Prints info about the size of each cluster in forward/backward transition relations

Defined in BddTrans.c 

ClusterIwls95_ptr 
ClusterIwls95_create(
  DdManager* dd, 
  const ClusterOptions_ptr  cl_options, 
  const double  v_c, 
  const double  w_c, 
  const double  x_c, 
  const double  y_c, 
  const double  z_c, 
  const double  min_c, 
  const double  max_c 
)
Allocates and initializes a cluster for IWLS95 alg. Please note that returned object can be casted to a cluster class instance. Use Cluster_destroy to destroy returned instance. The parameters passed to the constructor correspond to cluster options and 7 different factors (v_c, w_c, x_c, y_c, z_c, min_c and max_c) as explained in IWLS95 paper.

See Also Cluster_destroy Cluster_create
Defined in Cluster.c 

double 
ClusterIwls95_get_benefit(
  const ClusterIwls95_ptr  self 
)
Returns the value of the "benifit" variable.

Defined in Cluster.c 

boolean 
ClusterListIterator_is_end(
  const ClusterListIterator_ptr  self 
)
Use to check if iterator is at the end of list

Defined in ClusterList.c 

ClusterListIterator_ptr 
ClusterListIterator_next(
  const ClusterListIterator_ptr  self 
)
Advances the iterator by one.

Defined in ClusterList.c 

void 
ClusterList_append_cluster(
  ClusterList_ptr  self, 
  Cluster_ptr  cluster 
)
List becomes the owner of the given cluster, if the user is going to call standard destructor

Defined in ClusterList.c 

ClusterList_ptr 
ClusterList_apply_iwls95_partition(
  const ClusterList_ptr  self, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube, 
  bdd_ptr  next_state_vars_cube, 
  const ClusterOptions_ptr  cl_options 
)
This function builds the data structures to perform image computation.
This process consists of the following steps:
  1. Ordering of the clusters given as input accordingly with the heuristic described in IWLS95.
  2. Clustering of the result of previous step accordingly the threshold value stored in the option "image_cluster_size".
  3. Ordering of the result of previous step accordingly with the heuristic described in IWLS95.

Defined in ClusterList.c 

ClusterList_ptr 
ClusterList_apply_monolithic(
  const ClusterList_ptr  self 
)
"self" remains unchanged.

Defined in ClusterList.c 

void 
ClusterList_apply_synchronous_product(
  ClusterList_ptr  self, 
  const ClusterList_ptr  other 
)
All clusters into other are simply appended to "self". The result goes into "self", no changes on other. The scheduling is not performed at this step

Side Effects self will change

Defined in ClusterList.c 

ClusterList_ptr 
ClusterList_apply_threshold(
  const ClusterList_ptr  self, 
  const ClusterOptions_ptr  cl_options 
)
"self" remains unchanged.

Defined in ClusterList.c 

ClusterListIterator_ptr 
ClusterList_begin(
  const ClusterList_ptr  self 
)
Returns an Iterator to iterate the self.

Defined in ClusterList.c 

void 
ClusterList_build_schedule(
  ClusterList_ptr  self, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube 
)
It builds the quantification schedule of the variables inside the clusters of the "self".

Defined in ClusterList.c 

boolean 
ClusterList_check_equality(
  const ClusterList_ptr  self, 
  const ClusterList_ptr  other 
)
It compares BDDs not Clusters.

Defined in ClusterList.c 

boolean 
ClusterList_check_schedule(
  const ClusterList_ptr  self 
)
Let Ci and Ti be the ith cube and relation in the list. The schedule is correct iff
  1. For all Tj: j > i, S(Tj) and S(Ci) do not intersect, i.e., the variables which are quantified in Ci should not appear in the Tj for j>i.

where S(T) is the set of support of the BDD T. Returns true if the schedule is correct, false otherwise. This function is implemented for checking the correctness of the clustering algorithm only.
This function returns true if schedule is correct, false otherwise.

Defined in ClusterList.c 

ClusterList_ptr 
ClusterList_copy(
  const ClusterList_ptr  self 
)
Duplicates self and each cluster inside it.

Defined in ClusterList.c 

ClusterList_ptr 
ClusterList_create(
  DdManager* dd 
)
The reference to DdManager passed here is internally stored but self does not become owner of it.

Defined in ClusterList.c 

void 
ClusterList_destroy(
  ClusterList_ptr  self 
)
Destroys the cluster list and all cluster instances inside it.

Defined in ClusterList.c 

bdd_ptr 
ClusterList_get_clusters_cube(
  const ClusterList_ptr  self 
)
Given a list of clusters, it computes their set of support. Returned bdd is referenced.

Defined in ClusterList.c 

Cluster_ptr 
ClusterList_get_cluster(
  const ClusterList_ptr  self, 
  const ClusterListIterator_ptr  iter 
)
self keeps the ownership of the returned cluster

Defined in ClusterList.c 

bdd_ptr 
ClusterList_get_image_state_input(
  const ClusterList_ptr  self, 
  bdd_ptr  s 
)
Returned bdd is referenced

Defined in ClusterList.c 

bdd_ptr 
ClusterList_get_image_state(
  const ClusterList_ptr  self, 
  bdd_ptr  s 
)
Returned bdd is referenced

Defined in ClusterList.c 

bdd_ptr 
ClusterList_get_k_image_state_input(
  const ClusterList_ptr  self, 
  bdd_ptr  s, 
  int  k 
)
Returned bdd is referenced

Defined in ClusterList.c 

bdd_ptr 
ClusterList_get_k_image_state(
  const ClusterList_ptr  self, 
  bdd_ptr  s, 
  int  k 
)
Returned bdd is referenced

Defined in ClusterList.c 

bdd_ptr 
ClusterList_get_monolithic_bdd(
  const ClusterList_ptr  self 
)
The returned bdd is referenced

Defined in ClusterList.c 

int 
ClusterList_length(
  const ClusterList_ptr  self 
)
Returns the number of the clusters stored in "self".

Defined in ClusterList.c 

void 
ClusterList_prepend_cluster(
  ClusterList_ptr  self, 
  Cluster_ptr  cluster 
)
List becomes the owner of the given cluster

Defined in ClusterList.c 

void 
ClusterList_print_short_info(
  const ClusterList_ptr  self, 
  FILE* file 
)
Prints size of each cluster of the "self"

Defined in ClusterList.c 

int 
ClusterList_remove_cluster(
  ClusterList_ptr  self, 
  Cluster_ptr  cluster 
)
Returns the number of removed occurrences. Clusters found won't be destroyed, simply their references will be removed from the list

Defined in ClusterList.c 

void 
ClusterList_reverse(
  ClusterList_ptr  self 
)
Reverses the list of clusters.

Defined in ClusterList.c 

void 
ClusterList_set_cluster(
  ClusterList_ptr  self, 
  const ClusterListIterator_ptr  iter, 
  Cluster_ptr  cluster 
)
Sets the cluster of the "self" at the position given by iterator "iter" to cluster "cluster".

Defined in ClusterList.c 

boolean 
ClusterOptions_clusters_appended(
  const ClusterOptions_ptr  self 
)
Returns true if clusters must be appended, false if clusters must be prepended

Defined in ClusterOptions.c 

ClusterOptions_ptr 
ClusterOptions_create(
  OptsHandler_ptr  opt 
)
Creates a ClusterOptions instance.

Defined in ClusterOptions.c 

void 
ClusterOptions_destroy(
  ClusterOptions_ptr  self 
)
ClusterOption class destructor.

Defined in ClusterOptions.c 

int 
ClusterOptions_get_cluster_size(
  const ClusterOptions_ptr  self 
)
Returns the cluster_size field.

Defined in ClusterOptions.c 

int 
ClusterOptions_get_threshold(
  const ClusterOptions_ptr  self 
)
Returns the threshold field.

Defined in ClusterOptions.c 

int 
ClusterOptions_get_w1(
  const ClusterOptions_ptr  self 
)
According to the IWLS95 paper parameter w1 represents the weight attached to the R^1_c( =v_c/w_c) factor.

Defined in ClusterOptions.c 

int 
ClusterOptions_get_w2(
  const ClusterOptions_ptr  self 
)
According to the IWLS95 paper parameter w2 represents the weight attached to the R^2_c( =w_c/x_c) factor.

Defined in ClusterOptions.c 

int 
ClusterOptions_get_w3(
  const ClusterOptions_ptr  self 
)
According to the IWLS95 paper parameter w3 represents the weight attached to the R^3_c( =y_c/z_c) factor.

Defined in ClusterOptions.c 

int 
ClusterOptions_get_w4(
  const ClusterOptions_ptr  self 
)
According to the IWLS95 paper parameter w4 represents the weight attached to the R^4_c( =min_c/max_c) factor.

Defined in ClusterOptions.c 

boolean 
ClusterOptions_is_affinity(
  const ClusterOptions_ptr  self 
)
Checks whether Affinity is enabled.

Defined in ClusterOptions.c 

boolean 
ClusterOptions_is_iwls95_preorder(
  const ClusterOptions_ptr  self 
)
Checks whether preordering is enabled.

Defined in ClusterOptions.c 

void 
ClusterOptions_print(
  const ClusterOptions_ptr  self, 
  FILE* file 
)
Prints all the cluster options inside the specified file.

Defined in ClusterOptions.c 

Cluster_ptr 
Cluster_create(
  DdManager* dd 
)
Allocates and initializes a cluster.

See Also Object_destroy
Defined in Cluster.c 

bdd_ptr 
Cluster_get_quantification_state_input(
  const Cluster_ptr  self 
)
Returns a pointer to the list of variables to be quantified respect to the transition relation inside the cluster. Returned bdd is referenced.

Defined in Cluster.c 

bdd_ptr 
Cluster_get_quantification_state(
  const Cluster_ptr  self 
)
Returned value is referenced

Defined in Cluster.c 

bdd_ptr 
Cluster_get_trans(
  const Cluster_ptr  self 
)
Returned bdd will be referenced

Defined in Cluster.c 

boolean 
Cluster_is_equal(
  const Cluster_ptr  self, 
  const Cluster_ptr  other 
)
Notice that the check is performed only using the "curr_cluster" field of the Cluster class.

Defined in Cluster.c 

void 
Cluster_set_quantification_state_input(
  Cluster_ptr  self, 
  DdManager* dd, 
  bdd_ptr  new 
)
Given value will be referenced

Defined in Cluster.c 

void 
Cluster_set_quantification_state(
  Cluster_ptr  self, 
  DdManager* dd, 
  bdd_ptr  new 
)
Given value will be referenced

Defined in Cluster.c 

void 
Cluster_set_trans(
  Cluster_ptr  self, 
  DdManager* dd, 
  bdd_ptr  current 
)
The given bdd will be referenced. Previously stored bdd will be released

Defined in Cluster.c 

static af_support_pair* 
af_support_pair_create(
    
)
Allocates a pair

Defined in ClusterList.c 

static Object_ptr 
bdd_trans_copy(
  const Object_ptr  object 
)
Return a copy of the self.

Defined in BddTrans.c 

static boolean 
bdd_trans_debug_partitioned(
  const BddTrans_ptr  self, 
  const ClusterList_ptr  basic_clusters, 
  FILE* file 
)
It checks the equality in terms of transition relation and quantification schedule.

Defined in BddTrans.c 

static void 
cluster_copy_aux(
  const Cluster_ptr  self, 
  Cluster_ptr  copy 
)
It helps to copy the given cluster.

See Also cluster_copy
Defined in Cluster.c 

static Object_ptr 
cluster_copy(
  const Object_ptr  object 
)
It is the callback function that the copy constructor virtually calls.

See Also cluster_copy_aux
Defined in Cluster.c 

static void 
cluster_deinit(
  Cluster_ptr  self, 
  DdManager* dd 
)
Releases the contained bdds.

Defined in Cluster.c 

static void 
cluster_finalize(
  Object_ptr  object, 
  void* arg 
)
Finalize a cluster.

Defined in Cluster.c 

static void 
cluster_init(
  Cluster_ptr  self, 
  DdManager* dd 
)
Initializes the cluster with default values.

Defined in Cluster.c 

static void 
cluster_iwls95_copy_aux(
  const ClusterIwls95_ptr  self, 
  ClusterIwls95_ptr  copy 
)
It helps to copy iwls95 cluster.

See Also cluster_iwls95_copy
Defined in Cluster.c 

static Object_ptr 
cluster_iwls95_copy(
  const Object_ptr  object 
)
Callback function that copy constructor virtually calls to copy an instance of iwls95 cluster.

See Also cluster_iwls95_copy_aux
Defined in Cluster.c 

static void 
cluster_iwls95_deinit(
  ClusterIwls95_ptr  self, 
  DdManager* dd 
)
Deinitialized Iwls95 cluster.

Defined in Cluster.c 

static void 
cluster_iwls95_finalize(
  Object_ptr  object, 
  void* arg 
)
The virtual destructor calls this method to destroy the instance self.

Defined in Cluster.c 

static void 
cluster_iwls95_init(
  ClusterIwls95_ptr  self, 
  DdManager* dd, 
  const ClusterOptions_ptr  cl_options, 
  const double  v_c, 
  const double  w_c, 
  const double  x_c, 
  const double  y_c, 
  const double  z_c, 
  const double  min_c, 
  const double  max_c 
)
The parameters passed to this private function correspond to cluster options and different factors (v_c, w_c, x_c, y_c, z_c, min_c and max_c) as explained in IWLS95 paper.

Defined in Cluster.c 

static ClusterList_ptr 
cluster_list_apply_iwls95_info(
  const ClusterList_ptr  self, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube, 
  bdd_ptr  next_state_vars_cube, 
  const ClusterOptions_ptr  cl_options 
)
"self" remains unchanged.

Defined in ClusterList.c 

static ClusterList_ptr 
cluster_list_apply_threshold_affinity(
  const ClusterList_ptr  self, 
  const int  threshold, 
  const boolean  append 
)
This function aggregate clusters conjoining clusters that have highest affinity measure until they exceeds the specified threshold.
Remark: The number of clusters in self whose BDD size is below the threshold has a drammatic impact on the performance of this function. Indeed, the size of the heap used to order pair of clusters w.r.t. their affinity measure is proportional to the combination of N elements of class 2: C(N,K) = N!*(K!*(N-K)!).

Defined in ClusterList.c 

static ClusterList_ptr 
cluster_list_apply_threshold(
  const ClusterList_ptr  self, 
  const int  threshold, 
  const boolean  append 
)
The clusters are formed by taking the product in order. Once the BDD size of the current cluster reaches a threshold, a new cluster is created. It takes the value of "threshold" as parameter and returns the cluster of relation based on BDD size heuristic.

Defined in ClusterList.c 

static ClusterList_ptr 
cluster_list_copy(
  const ClusterList_ptr  self, 
  const boolean  weak_copy 
)
If weak_copy is true (internal use only) copied list must be destroyed by calling the weak private destructor cluster_list_destroy_weak

See Also cluster_list_destroy_weak
Defined in ClusterList.c 

static void 
cluster_list_destroy_weak(
  ClusterList_ptr  self 
)
private function to weakly destroy the "self"

Defined in ClusterList.c 

static bdd_ptr 
cluster_list_get_supp_Q_Ci(
  const ClusterList_ptr  self, 
  const Cluster_ptr  Ci 
)
Computes the set of present an primary input variables that belong to the set of support of cluster Ci, and do not belong to the set of support of each cluster Cj, for j != i and Cj belonging to the set of the not yet ordered clusters. The set Supp_Q_Ci is formally defined as: Supp_Q_Ci = {v in (PS U PI) / v notin S(T_Cj), Cj != Ci, Cj in Q}

Defined in ClusterList.c 

static ClusterList_ptr 
cluster_list_iwls95_order(
  const ClusterList_ptr  self, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube, 
  bdd_ptr  next_state_vars_cube, 
  const ClusterOptions_ptr  cl_options 
)
"self" remains unchanged.

Defined in ClusterList.c 

static int 
clusterlist_affinity_move_clusters(
  const ClusterList_ptr  self, 
  ClusterList_ptr  new_list, 
  const int  threshold, 
  const boolean  append, 
  node_ptr* list_ref, 
  heap  _heap 
)
It doesn't modify the input list.

Defined in ClusterList.c 

static void 
clusterlist_build_schedule_recur(
  ClusterList_ptr  self, 
  const ClusterListIterator_ptr  iter, 
  const bdd_ptr  s_cube, 
  const bdd_ptr  si_cube, 
  bdd_ptr* acc_s, 
  bdd_ptr* acc_si 
)
Auxiliary recursive private function that computes the quantification schedule. The acc_s and acc_si must be freed by the caller.

Side Effects acc_s and acc_si are modified and must be freed by the caller.

Defined in ClusterList.c 

static double 
compute_bdd_affinity(
  DdManager* dd, 
  bdd_ptr  a, 
  bdd_ptr  b 
)
Compute the Affinity between two BDDs. This is an alternative definition to the one suggested by by Moon, Hachtel, Somenzi in BBT paper.

Defined in ClusterList.c 

static void 
support_list_del(
  af_support_list_entry* asle 
)
Delete a cluster in support list.

Defined in ClusterList.c 

static af_support_list_entry* 
support_list_entry_create(
    
)
Allocates an af_support_list_entry

Defined in ClusterList.c 

static node_ptr 
support_list_heap_add(
  node_ptr  list, 
  heap  _heap, 
  DdManager* dd, 
  Cluster_ptr  cluster 
)
Pairs with a dead cluster are skipped

Defined in ClusterList.c 

 
(
    
)
Compute the Affinity between two BDD clusters as suggested by Moon, Hachtel, Somenzi in BBT paper. Affinity is the ratio between the number of shared variables and the number of the union of all variables (intersection/union)

Defined in ClusterList.c 

 
(
    
)
The parameters passed to this function includes pointer to "self", set of states "s", and a function pointer that retrives from any cluster in "self" a cube of variables for existential quantification.

Defined in ClusterList.c 

 
(
    
)
This number specifies the number of clusters whose BDD size is below the partitioning threshold. If the number of clusters whose size is below the partitioning threshold exceeds this limit, then clustering via affinity is not performed (too expensive) and "simple" clustering is performed. With this value the initial size of the heap used by the clustering via affinity is 100!/(2*(100-2)!) = 4950, i.e. the combination of N=100 elements in pair: C(N,2). Allowing larger numbers is possible, but can lead to enourmous consumption of memory.

See Also ClusterList_apply_threshold cluster_list_apply_threshold_affinity
Defined in ClusterList.c 

 
(
    
)
The parameters passed to this function includes pointer to "self", set of states "s", value "k", and a function pointer that retrives from any cluster in "self" a cube of variables for existential quantification.

Defined in ClusterList.c
Last updated on 2011/04/06 21h:12