src/synth/synthDiv.c File Reference
#include "synthInt.h"
Include dependency graph for synthDiv.c:
Go to the source code of this file.
Data Structures | |
| struct | bfs_item |
| struct | bfs_list |
Defines | |
| #define | MAX_COUNT 100000000 |
Typedefs | |
| typedef struct bfs_item | BfsItem |
| typedef struct bfs_list | BfsList |
Functions | |
| static int | FindQuickDivisor (bdd_node *f, bdd_node *one, int *v) |
| bdd_node * | Synth_ZddQuickDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | Synth_ZddLeastDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | Synth_ZddMostDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | Synth_ZddLevelZeroDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | Synth_ZddCommonDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | Synth_ZddLpDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | SynthZddQuickDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | SynthZddLeastDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | SynthZddMostDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | SynthZddLevelZeroDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | SynthZddCommonDivisor (bdd_manager *dd, bdd_node *f) |
| bdd_node * | SynthZddLpDivisor (bdd_manager *dd, bdd_node *f) |
| void | SynthCountLiteralOccurrence (bdd_manager *dd, bdd_node *f, int *count) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: synthDiv.c,v 1.25 2002/09/10 05:50:52 fabio Exp $" |
Define Documentation
| #define MAX_COUNT 100000000 |
Definition at line 25 of file synthDiv.c.
Typedef Documentation
Struct**********************************************************************
Synopsis [Structure of one BFS item to count variable occurrences.]
Description [Structure of one BFS item to count variable occurrences.]
SeeAlso []
Struct**********************************************************************
Synopsis [Structure for BFS operation to count variable occurrences.]
Description [Structure for BFS operation to count variable occurrences.]
SeeAlso []
Function Documentation
| static int FindQuickDivisor | ( | bdd_node * | f, |
| bdd_node * | one, | ||
| int * | v | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Finds a ZDD node that is referred by more than one parent node in a function.]
Description [Finds a ZDD node that is referred by more than one parent node in a function. Performs a DFS from f. Whenever a node is visited, the node is marked. When a node is visited, if the node is already marked, it returns the index of the node. Uses the LSB of the next pointer as visited flag. This function returns the number of path to constant 1 from the node, and return value -1 means already found.]
SideEffects [Once this function is called, SynthZddClearFlag() should be called right after.];
SeeAlso [SynthZddClearFlag]
Definition at line 1055 of file synthDiv.c.
{
int c, ct, ce;
bdd_node *temp = bdd_read_next(f);
if (bdd_is_constant(f)) {
if (f == one)
return(1);
else
return(0);
}
if (bdd_is_complement(temp)) { /* already visited */
*v = bdd_node_read_index(f);
return(-1);
}
/* mark as visited */
bdd_set_next(f, bdd_not_bdd_node(temp));
ct = FindQuickDivisor(bdd_bdd_T(f), one, v);
if (ct == -1) /* already found */
return(-1);
else if (ct > 1) {
*v = bdd_node_read_index(f);
return(-1);
}
ce = FindQuickDivisor(bdd_bdd_E(f), one, v);
if (ce == -1) /* already found */
return(-1);
/* Add the number of path to constant 1 from two children nodes. */
c = ct + ce;
return(c);
}
Here is the caller graph for this function:
| bdd_node* Synth_ZddCommonDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Find a divisor whose literals occur in all cubes.]
Description [Find a divisor whose literals occur in all cubes. It returns a ZDD node.]
SideEffects []
SeeAlso [Synth_ZddQuickDivisor Synth_ZddMostDivisor Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddLpDivisor]
Definition at line 242 of file synthDiv.c.
{
bdd_node *res;
if (bdd_get_package_name() != CUDD) {
(void)fprintf(vis_stderr,
"** synth error: Synthesis package can be used only with CUDD package\n");
(void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
return NIL(bdd_node);
}
do {
bdd_set_reordered_field(dd, 0);
res = SynthZddCommonDivisor(dd, f);
} while (bdd_read_reordered_field(dd) == 1);
return(res);
}
Here is the call graph for this function:
| bdd_node* Synth_ZddLeastDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Finds a divisor that occurs the least frequently (but more than once) in the cubes of a cover.]
Description [Finds a divisor that occurs the least frequently (but more than once) in the cubes of a cover. It returns a ZDD node.]
SideEffects []
SeeAlso [Synth_ZddQuickDivisor Synth_ZddMostDivisor Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
Definition at line 139 of file synthDiv.c.
{
bdd_node *res;
if (bdd_get_package_name() != CUDD) {
(void)fprintf(vis_stderr,
"** synth error: Synthesis package can be used only with CUDD package\n");
(void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
return NIL(bdd_node);
}
do {
bdd_set_reordered_field(dd, 0);
res = SynthZddLeastDivisor(dd, f);
} while (bdd_read_reordered_field(dd) == 1);
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* Synth_ZddLevelZeroDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Finds a divisor that is a level-0 cokernel.]
Description [Finds a divisor that is a level-0 cokernel. It returns a ZDD node.]
SideEffects []
SeeAlso [Synth_ZddQuickDivisor Synth_ZddLeastDivisor Synth_ZddMostDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
Definition at line 208 of file synthDiv.c.
{
bdd_node *res;
if (bdd_get_package_name() != CUDD) {
(void)fprintf(vis_stderr,
"** synth error: Synthesis package can be used only with CUDD package\n");
(void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
return NIL(bdd_node);
}
do {
bdd_set_reordered_field(dd, 0);
res = SynthZddLevelZeroDivisor(dd, f);
} while (bdd_read_reordered_field(dd) == 1);
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* Synth_ZddLpDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Find a good divisor for low power.]
Description [Find a good divisor for low power. It returns a ZDD node.]
SideEffects []
SeeAlso [Synth_ZddQuickDivisor Synth_ZddMostDivisor Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor]
Definition at line 275 of file synthDiv.c.
{
bdd_node *res;
if (bdd_get_package_name() != CUDD) {
(void)fprintf(vis_stderr,
"** synth error: Synthesis package can be used only with CUDD package\n");
(void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
return NIL(bdd_node);
}
do {
bdd_set_reordered_field(dd, 0);
res = SynthZddLpDivisor(dd, f);
} while (bdd_read_reordered_field(dd) == 1);
return(res);
}
Here is the call graph for this function:
| bdd_node* Synth_ZddMostDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Finds a divisor that occurs the most frequently in the cubes of a cover.]
Description [Finds a divisor that occurs the most frequently in the cubes of a cover. It returns a ZDD node.]
SideEffects []
SeeAlso [Synth_ZddQuickDivisor Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
Definition at line 174 of file synthDiv.c.
{
bdd_node *res;
if (bdd_get_package_name() != CUDD) {
(void)fprintf(vis_stderr,
"** synth error: Synthesis package can be used only with CUDD package\n");
(void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
return NIL(bdd_node);
}
do {
bdd_set_reordered_field(dd, 0);
res = SynthZddMostDivisor(dd, f);
} while (bdd_read_reordered_field(dd) == 1);
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* Synth_ZddQuickDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Finds a divisor that occurs in more than one cube of the ZDD graph.]
Description [Finds a divisor that occurs in more than one cube of the ZDD graph. This is done in a greedy manner. It returns a ZDD node.]
SideEffects []
SeeAlso [Synth_ZddLeastDivisor Synth_ZddMostDivisor Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
Definition at line 104 of file synthDiv.c.
{
bdd_node *res;
if (bdd_get_package_name() != CUDD) {
(void)fprintf(vis_stderr,
"** synth error: Synthesis package can be used only with CUDD package\n");
(void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
return NIL(bdd_node);
}
do {
bdd_set_reordered_field(dd, 0);
res = SynthZddQuickDivisor(dd, f);
} while (bdd_read_reordered_field(dd) == 1);
return(res);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void SynthCountLiteralOccurrence | ( | bdd_manager * | dd, |
| bdd_node * | f, | ||
| int * | count | ||
| ) |
Function********************************************************************
Synopsis [Counts the number of occurrences of each variable.]
Description [Counts the number of occurrences of each variable. First, we count the number of paths to the top node for each node from top to bottom. Let this number be C_t. Initially, C_t of the top node is 1, and C_t of a node is the sum of C_t's of all predecessors of the node. Second, we count the number of paths to the constant one node from bottom to top. Let this number be C_1. Initially, C_1 of the constant one node is 1 and C_1 of the constant zero node is 0, and C_1 of a node is the sum of C_1's of two successors of the node. Third, we count the number of occurrences of variables using the C_t's and C_1's of each node. Here, let C_m of a node be C_t of the node times C_1 of then child of the node. The number of occurrences of a variable is determined by summing C_m of all nodes that belongs to the variable in the ZDD. The argument count is passed by caller, and it is an array of integer to store the number of occurrence for each variable, and the size of the array is the number of ZDD variables.]
SideEffects []
SeeAlso []
Definition at line 812 of file synthDiv.c.
{
BfsItem **level, *item, *cur_item, *next_item, *last_item;
BfsList *list, *pre_list, *cur_list, *next_list, *last_list;
BfsList *new_list, *save_last_list;
int cur_level, next_level, start_level, last_level;
int exist;
bdd_node *zero = bdd_read_zero(dd);
bdd_node *one = bdd_read_one(dd);
int i, ct, ce;
bdd_node *node;
int lv, *index, id;
int sizeZ = bdd_num_zdd_vars(dd);
if (bdd_is_constant(f))
return;
level = ALLOC(BfsItem *, sizeZ);
(void)memset((void *)level, 0, sizeof(BfsItem *) * sizeZ);
index = ALLOC(int, sizeZ);
(void)memset((void *)index, 0, sizeof(int) * sizeZ);
/* Initialize BFS by entering f in the queue. */
item = ALLOC(BfsItem, 1);
(void)memset((void *)item, 0, sizeof(BfsItem));
item->node = f;
item->reach = 1;
lv = bdd_read_zdd_level(dd,bdd_node_read_index(f));
level[lv] = item;
index[lv] = bdd_node_read_index(f);
start_level = last_level = lv;
if (!bdd_is_constant(bdd_bdd_T(f))) {
list = ALLOC(BfsList, 1);
(void)memset((void *)list, 0, sizeof(BfsList));
list->item = item;
list->child = 1;
last_list = list;
} else
list = last_list = (BfsList *)NULL;
if (!bdd_is_constant(bdd_bdd_E(f))) {
last_list = ALLOC(BfsList, 1);
(void)memset((void *)last_list, 0, sizeof(BfsList));
last_list->item = item;
last_list->child = 0;
if (list)
list->next = last_list;
else
list = last_list;
}
/* Perform the BFS. */
while (list) {
cur_level = sizeZ;
cur_list = list;
while (cur_list) {
if (cur_list->child)
id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
else
id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
next_level = bdd_read_zdd_level(dd,id);
cur_level = (cur_level < next_level) ? cur_level : next_level;
cur_list = cur_list->next;
}
last_level = cur_level;
save_last_list = last_list;
pre_list = (BfsList *)NULL;
cur_list = list;
while (cur_list) {
if (cur_list->child)
id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
else
id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
next_level = bdd_read_zdd_level(dd,id);
if (next_level != cur_level) {
pre_list = cur_list;
cur_list = cur_list->next;
continue;
}
if (cur_list->child)
node = bdd_bdd_T(cur_list->item->node);
else
node = bdd_bdd_E(cur_list->item->node);
exist = 0;
last_item = level[cur_level];
while (last_item) {
if (node == last_item->node) {
last_item->reach += cur_list->item->reach;
exist = 1;
break;
}
if (last_item->next)
last_item = last_item->next;
else
break;
}
if (exist == 0) {
item = ALLOC(BfsItem, 1);
(void)memset((void *)item, 0, sizeof(BfsItem));
item->node = node;
item->reach = cur_list->item->reach;
if (last_item)
last_item->next = item;
else {
level[cur_level] = item;
index[cur_level] = id;
}
if (!bdd_is_constant(bdd_bdd_T(node))) {
new_list = ALLOC(BfsList, 1);
(void)memset((void *)new_list, 0, sizeof(BfsList));
new_list->item = item;
new_list->child = 1;
last_list->next = new_list;
last_list = new_list;
}
if (!bdd_is_constant(bdd_bdd_E(node))) {
new_list = ALLOC(BfsList, 1);
(void)memset((void *)new_list, 0, sizeof(BfsList));
new_list->item = item;
new_list->child = 0;
last_list->next = new_list;
last_list = new_list;
}
}
next_list = cur_list->next;
if (cur_list == list && cur_list == last_list) {
FREE(cur_list);
list = next_list;
} else if (cur_list == list) {
FREE(cur_list);
pre_list = (BfsList *)NULL;
if (list == save_last_list) {
list = next_list;
next_list = (BfsList *)NULL;
} else
list = next_list;
} else if (cur_list == last_list) {
if (pre_list)
pre_list->next = cur_list->next;
FREE(cur_list);
last_list = pre_list;
} else {
if (pre_list)
pre_list->next = cur_list->next;
if (cur_list == save_last_list) {
FREE(cur_list);
next_list = (BfsList *)NULL;
} else
FREE(cur_list);
}
cur_list = next_list;
}
}
/* Compute the number of paths to the constant 1 for each node in
* bottom up fashion. Update the occurrence count of the variables.
*/
for (i = last_level; i >= start_level; i--) {
item = level[i];
while (item) {
ct = ce = 0;
if (bdd_bdd_T(item->node) == one)
ct = 1;
else {
node = bdd_bdd_T(item->node);
next_level = bdd_read_zdd_level(dd, bdd_node_read_index(node));
cur_item = level[next_level];
while (cur_item) {
if (cur_item->node == node) {
ct = cur_item->count;
break;
}
cur_item = cur_item->next;
}
}
if (bdd_bdd_E(item->node) != zero) {
node = bdd_bdd_E(item->node);
next_level = bdd_read_zdd_level(dd,
bdd_node_read_index(node));
cur_item = level[next_level];
while (cur_item) {
if (cur_item->node == node) {
ce = cur_item->count;
break;
}
cur_item = cur_item->next;
}
}
item->count = ct + ce;
count[index[i]] += ct * item->reach;
item = item->next;
}
}
/* Clean up. */
for (i = last_level; i >= start_level; i--) {
item = level[i];
while (item) {
next_item = item->next;
FREE(item);
item = next_item;
}
}
FREE(level);
FREE(index);
}
Here is the caller graph for this function:
| bdd_node* SynthZddCommonDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [The internal function of Synth_ZddCommonDivisor.]
Description [The internal function of Synth_ZddCommonDivisor.]
SideEffects []
SeeAlso [SynthZddQuickDivisor SynthZddLeastDivisor SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddLpDivisor]
Definition at line 640 of file synthDiv.c.
{
int i;
int nvars;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node, *tmp;
int nCubes;
divisor = (bdd_node *)NULL; /* NULL means no such divisor exists */
if (f == one || f == zero)
return(divisor);
nCubes = bdd_zdd_count(dd, f);
if (nCubes == 1)
return(divisor);
/* Find the literals that appear exactly as many times as there
* are cubes. These literals appear in all cubes, hence in the
* common divisor. Their product is accumulated in divisor. */
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] == nCubes) {
node = bdd_zdd_get_node(dd, i, one, zero);
if (!node) {
FREE(count);
return(NULL);
}
bdd_ref(node);
if (!divisor) {
divisor = node;
continue;
}
tmp = divisor;
divisor = (* SynthGetZddProductRecurFunc())(dd, divisor, node);
if (!divisor) {
bdd_recursive_deref_zdd(dd, tmp);
bdd_recursive_deref_zdd(dd, node);
FREE(count);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp);
bdd_recursive_deref_zdd(dd, node);
}
}
FREE(count);
if (divisor)
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SynthZddLeastDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive steps of Synth_ZddLeastDivisor.]
Description [Performs the recursive steps of Synth_ZddLeastDivisor.]
SideEffects []
SeeAlso [SynthZddQuickDivisor SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]
Definition at line 402 of file synthDiv.c.
{
int i, v;
int nvars, min_count;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node;
bdd_node *tmp1;
if (f == one || f == zero)
return(f);
/* Find the literal that occurs the least among those occuring at
* least twice.
*/
v = -1;
min_count = MAX_COUNT;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > 1 && count[i] < min_count) {
v = i;
min_count = count[i];
}
}
FREE(count);
if (v == -1) {
/* All literal appear exactly once. We are done. */
return(f);
}
/* Obtain the literal divisor from its index and divide f. */
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node) {
return(NULL);
}
bdd_ref(node);
tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
if (!tmp1) {
bdd_recursive_deref_zdd(dd, node);
return(NULL);
}
bdd_ref(tmp1);
bdd_recursive_deref_zdd(dd, node);
/* Recur on the quotient to make sure that all literals appear once. */
divisor = SynthZddLeastDivisor(dd, tmp1);
if (!divisor) {
bdd_recursive_deref_zdd(dd, tmp1);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SynthZddLevelZeroDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive steps of Synth_ZddLevelZeroDivisor.]
Description [Performs the recursive steps of Synth_ZddLevelZeroDivisor.]
SideEffects []
SeeAlso [SynthZddQuickDivisor SynthZddLeastDivisor SynthZddMostDivisor SynthZddCommonDivisor SynthZddLpDivisor]
Definition at line 556 of file synthDiv.c.
{
int i, v;
int nvars, max_count;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node;
bdd_node *tmp1, *tmp2;
if (f == one || f == zero)
return(f);
/* Find the literal that occurs the most. */
v = -1;
max_count = 1;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > max_count) {
v = i;
max_count = count[i];
}
}
FREE(count);
if (v == -1) {
/* All literal appear exactly once. We are done. */
return(f);
}
/* Obtain the literal divisor from its index and divide f. */
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node)
return(NULL);
bdd_ref(node);
tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
if (!tmp1) {
bdd_recursive_deref_zdd(dd, node);
return(NULL);
}
bdd_ref(tmp1);
bdd_recursive_deref_zdd(dd, node);
/* Factor out all literals appearing in all cubes. */
tmp2 = SynthMakeCubeFree(dd, tmp1);
if (!tmp2) {
bdd_recursive_deref_zdd(dd, tmp1);
return(NULL);
}
bdd_ref(tmp2);
bdd_recursive_deref_zdd(dd, tmp1);
/* Recur on the quotient to make sure that all literals appear once. */
divisor = SynthZddLevelZeroDivisor(dd, tmp2);
if (!divisor) {
bdd_recursive_deref_zdd(dd, tmp2);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp2);
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SynthZddLpDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive steps of Synth_ZddLpDivisor.]
Description [Performs the recursive steps of Synth_ZddLpDivisor.]
SideEffects []
SeeAlso [SynthZddQuickDivisor SynthZddLeastDivisor SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddCommonDivisor]
Definition at line 712 of file synthDiv.c.
{
int i, v;
int nvars, min_count, min_pos = 0;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node;
bdd_node *tmp1;
if (f == one || f == zero)
return(f);
/* Find the literal that occurs the least among those occuring at
* least twice.
*/
v = -1;
min_count = MAX_COUNT;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > 1 && count[i] < min_count) {
v = i;
min_count = count[i];
min_pos = i;
}
}
if (v == -1) {
/* All literal appear exactly once. We are done. */
FREE(count);
return(f);
}
/* Among the literals with minimum count, find a good one. */
v = SynthFindDivisorForLowPower(count, nvars, min_count, min_pos);
FREE(count);
if (v == -1) {
return(f);
}
/* Obtain the literal divisor from its index and divide f. */
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node)
return(NULL);
bdd_ref(node);
tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
if (!tmp1) {
bdd_recursive_deref_zdd(dd, node);
return(NULL);
}
bdd_ref(tmp1);
bdd_recursive_deref_zdd(dd, node);
/* Recur on the quotient to make sure that all literals appear once. */
divisor = SynthZddLpDivisor(dd, tmp1);
if (!divisor) {
bdd_recursive_deref_zdd(dd, tmp1);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SynthZddMostDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive steps of Synth_ZddMostDivisor.]
Description [Performs the recursive steps of Synth_ZddMostDivisor.]
SideEffects []
SeeAlso [SynthZddQuickDivisor SynthZddLeastDivisor SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]
Definition at line 480 of file synthDiv.c.
{
int i, v;
int nvars, max_count;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node;
bdd_node *tmp1;
if (f == one || f == zero)
return(f);
/* Find the literal that occurs the most. */
v = -1;
max_count = 1;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > max_count) {
v = i;
max_count = count[i];
}
}
FREE(count);
if (v == -1) {
/* All literal appear exactly once. We are done. */
return(f);
}
/* Obtain the literal divisor from its index and divide f. */
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node)
return(NULL);
bdd_ref(node);
tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
if (!tmp1) {
bdd_recursive_deref_zdd(dd, node);
return(NULL);
}
bdd_ref(tmp1);
bdd_recursive_deref_zdd(dd, node);
/* Recur on the quotient to make sure that all literals appear once. */
divisor = SynthZddMostDivisor(dd, tmp1);
if (!divisor) {
bdd_recursive_deref_zdd(dd, tmp1);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SynthZddQuickDivisor | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Performs the recursive steps of Synth_ZddQuickDivisor.]
Description [Performs the recursive steps of Synth_ZddQuickDivisor. When FindQuickDivisor fails to find a literal, the function uses as backup strategy finding the literal that occurs the least. The reason is the following. If a node has more than one parent, then it is guaranteed to appear in more than one cube. However, the converse is not true.]
SideEffects []
SeeAlso [SynthZddLeastDivisor SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]
Definition at line 318 of file synthDiv.c.
{
int i, v;
int nvars;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node;
bdd_node *tmp;
int min_count;
if (f == one || f == zero)
return(f);
/* Search for a literal appearing in at least two cubes. */
v = -1;
FindQuickDivisor(f, one, &v);
SynthZddClearFlag(f);
if (v == -1) {
/* Quick divisor not found by looking at the ZDD graph.
* Find the literal that occurs the least among those occuring
* at least twice.
*/
min_count = MAX_COUNT;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > 1 && count[i] < min_count) {
v = i;
min_count = count[i];
}
}
FREE(count);
if (v == -1) {
/* All literal appear exactly once. We are done. */
return(f);
}
}
/* Obtain the literal divisor from its index and divide f. */
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node)
return(NULL);
bdd_ref(node);
tmp = (* SynthGetZddDivideRecurFunc())(dd, f, node);
if (!tmp) {
bdd_recursive_deref_zdd(dd,node);
return(NULL);
}
bdd_ref(tmp);
bdd_recursive_deref_zdd(dd, node);
/* Recur on the quotient to make sure that all literals appear once. */
divisor = SynthZddQuickDivisor(dd, tmp);
if (!divisor) {
bdd_recursive_deref_zdd(dd,tmp);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp);
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: synthDiv.c,v 1.25 2002/09/10 05:50:52 fabio Exp $" [static] |
CFile***********************************************************************
FileName [synthDiv.c]
PackageName [synth]
Synopsis [Divisor functions.]
Author [In-Ho Moon, Balakrishna Kumthekar]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 19 of file synthDiv.c.
