BddTrans_apply_synchronous_product()
Performs the synchronous product between two trans
BddTrans_create()
Builds the transition relation
BddTrans_get_backward_image_state_input()
Computes the backward image by existentially quantifying over both state and input variables.
BddTrans_get_backward_image_state()
Computes the backward image by existentially quantifying over state variables only.
BddTrans_get_backward()
Returns backward transition relation.
BddTrans_get_forward_image_state_input()
Computes the forward image by existentially quantifying over both state and input variables.
BddTrans_get_forward_image_state()
Computes the forward image by existentially quantifying over state variables only.
BddTrans_get_forward()
Returns forward transition relation.
BddTrans_get_k_backward_image_state_input()
Computes the k backward image by existentially quantifying over both state and input variables.
BddTrans_get_k_backward_image_state()
Computes the k backward image by existentially quantifying over state variables only.
BddTrans_get_k_forward_image_state_input()
Computes the k forward image by existentially quantifying over both state and input variables.
BddTrans_get_k_forward_image_state()
Computes the k forward image by existentially quantifying over state variables only.
BddTrans_print_short_info()
Prints short info associated to a Trans
ClusterIwls95_create()
"ClusterIwls95" Class constructor.
ClusterIwls95_get_benefit()
Returns the value of the "benifit" variable.
ClusterListIterator_is_end()
Use to check if iterator is at the end of list
ClusterListIterator_next()
Use to iterate a list
ClusterList_append_cluster()
Appends given cluster to the list
ClusterList_apply_iwls95_partition()
Orders the clusters according to the IWLS95 algo. to perform image computation.
ClusterList_apply_monolithic()
It returns a monolithic transition cluster corresponding to the cluster list of the "self".
ClusterList_apply_synchronous_product()
Performs the synchronous product between two cluster lists
ClusterList_apply_threshold()
It returns a threshold based cluster list corresponding to the cluster list of the "self".
ClusterList_begin()
Returns an Iterator to iterate the self.
ClusterList_build_schedule()
It builds the quantification schedule of the variables inside the clusters of the "self".
ClusterList_check_equality()
Returns true if two clusters list are logically equivalent
ClusterList_check_schedule()
Check the schedule for self. Call after you applied the schedule
ClusterList_copy()
Returns a copy of the "self".
ClusterList_create()
Class ClusterList Constructor.
ClusterList_destroy()
ClusterList Class dectructor.
ClusterList_get_clusters_cube()
Computes the cube of the set of support of all the clusters
ClusterList_get_cluster()
Returns the cluster kept at the position given by the iterator
ClusterList_get_image_state_input()
Computes the image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.
ClusterList_get_image_state()
Computes the image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.
ClusterList_get_k_image_state_input()
Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.
ClusterList_get_k_image_state()
Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.
ClusterList_get_monolithic_bdd()
Returns the monolithic bdd corresponding to the "self".
ClusterList_length()
Returns the number of the clusters stored in "self".
ClusterList_prepend_cluster()
Prepends given cluster to the list
ClusterList_print_short_info()
Prints size of each cluster of the "self"
ClusterList_remove_cluster()
Deletes every occurrence of the given cluster from the self.
ClusterList_reverse()
Reverses the list of clusters.
ClusterList_set_cluster()
Sets the cluster of the "self" at the position given by iterator "iter" to cluster "cluster".
ClusterOptions_clusters_appended()
Returns true if clusters must be appended, false if clusters must be prepended
ClusterOptions_create()
"ClusterOptions" class constructor.
ClusterOptions_destroy()
ClusterOption class destructor.
ClusterOptions_get_cluster_size()
Returns the cluster_size field.
ClusterOptions_get_threshold()
Returns the threshold field.
ClusterOptions_get_w1()
Retrieves the parameter w1.
ClusterOptions_get_w2()
Retrieves the parameter w2.
ClusterOptions_get_w3()
Retrieves the parameter w3.
ClusterOptions_get_w4()
Retrieves the parameter w4.
ClusterOptions_is_affinity()
Checks whether Affinity is enabled.
ClusterOptions_is_iwls95_preorder()
Checks whether preordering is enabled.
ClusterOptions_print()
Prints all the cluster options inside the specified file.
Cluster_create()
The "Cluster" class constructor.
Cluster_get_quantification_state_input()
Returns a pointer to the list of variables (both state and input vars) to be quantified.
Cluster_get_quantification_state()
Returns a pointer to the list of variables (state vars only) to be quantified
Cluster_get_trans()
Retrives the clusterized transition relation of the self .
Cluster_is_equal()
Checks if two clusters are equal
Cluster_set_quantification_state_input()
Sets the list of variables (both state and input vars) to be quantified inside the cluster.
Cluster_set_quantification_state()
Sets the list of variables (state vars only) to be quantified inside the cluster
Cluster_set_trans()
Sets the transition relation inside the cluster
af_support_pair_create()
Allocates a pair
bdd_trans_copy()
Copy constructor
bdd_trans_debug_partitioned()
Checks the equality between given Monolithic and Partitioned transition relations.
cluster_copy_aux()
It helps to copy the given cluster.
cluster_copy()
Copies the given cluster.
cluster_deinit()
Deinitializes the cluster.
cluster_finalize()
Finalize a cluster.
cluster_init()
Initializes the cluster with default values.
cluster_iwls95_copy_aux()
It helps to copy iwls95 cluster.
cluster_iwls95_copy()
Copies iwls95 cluster.
cluster_iwls95_deinit()
Deinitialized Iwls95 cluster.
cluster_iwls95_finalize()
Finalize iwls95 cluster.
cluster_iwls95_init()
Initializes Iwls95 cluster.
cluster_list_apply_iwls95_info()
It applies iwls95 info passed as parameters to a copy of the "self" and returns it.
cluster_list_apply_threshold_affinity()
OPTIMIZED affinity clustering
cluster_list_apply_threshold()
Forms the clusters of relations based on BDD size heuristic
cluster_list_copy()
Dups a given list of clusters, copying clusters depending on the value in weak_copy
cluster_list_destroy_weak()
private function to weakly destroy the "self"
cluster_list_get_supp_Q_Ci()
Computes the set Supp_Q_Ci.
cluster_list_iwls95_order()
It orders a copy of the "self" according to the IWLS95 algorithm and returns the copy.
clusterlist_affinity_move_clusters()
Copy over threshold clusters in result list or in support list & heap.
clusterlist_build_schedule_recur()
Helps to compute the quantification schedule
compute_bdd_affinity()
Compute the Affinity of two BDD clusters.
compute_bdd_affinity()
Compute the Affinity of two BDD clusters.
support_list_del()
Delete a cluster in support list.
support_list_entry_create()
Allocates an af_support_list_entry
support_list_heap_add()
Add a new entry in support list and new pairs in heap.
()
Computes the image from a given set of states "s".
()
Number of allowed clusters whose BDD size is below the partitioning threshold while using affinity.
()
Use to compute the k image from a given set of states "s".

Last updated on 2010/11/03 21h:54