src/synth/synthFactor.c File Reference
#include "synthInt.h"
Include dependency graph for synthFactor.c:
Go to the source code of this file.
Data Structures | |
| struct | ml_size_list |
Typedefs | |
| typedef struct ml_size_list | MlSizeList |
Functions | |
| static MlTree * | ResolveConflictNode (bdd_manager *dd, st_table *table, MlTree *tree1, MlTree *tree2, int comp_flag, int verbosity) |
| static void | DeleteMlTree (bdd_manager *dd, st_table *table, MlTree *kill_tree, MlTree *live_tree, int deref, int comp_flag) |
| static void | UnlinkMlTree (MlTree *kill_tree) |
| static void | DeleteMlSizeList (MlTree *tree) |
| static int | InsertMlTable (st_table *table, bdd_node *node, MlTree *tree) |
| static bdd_node * | MakeComplementOfZddCover (bdd_manager *dd, bdd_node *node, int verbosity) |
| static char * | GetIntString (int v) |
| static void | VerifyTreeList (void) |
| void | SynthSetZddDivisorFunc (int mode) |
| void | SynthGetSpaceString (char *string, int n, int max) |
| MlTree * | SynthLookupMlTable (st_table *table, bdd_manager *dd, bdd_node *node, int candidate, int verbosity) |
| int | SynthUseCandidate (st_table *table, bdd_manager *dd, MlTree *m_tree, int verbosity) |
| MlTree * | SynthFindOrCreateMlTree (st_table *table, bdd_manager *dd, bdd_node *f, int leaf, int candidate, int *ref, int verbosity) |
| void | SynthInitMlTable (void) |
| void | SynthClearMlTable (bdd_manager *dd, st_table *table) |
| void | SynthPutMlTreeInList (bdd_manager *dd, MlTree *tree, int candidate) |
| MlTree * | SynthGetHeadTreeOfSize (int size) |
| MlTree * | SynthCheckAndMakeComplement (bdd_manager *dd, st_table *table, MlTree *tree, int *comp_flag, int verbosity) |
| void | SynthSetSharedFlag (bdd_manager *dd, MlTree *tree) |
| int | SynthPostFactoring (bdd_manager *dd, st_table *table, MlTree *(*factoring_func)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int), int verbosity) |
| void | SynthUpdateRefOfParent (MlTree *top) |
| void | SynthVerifyTree (bdd_manager *dd, MlTree *tree, int flag) |
| void | SynthVerifyMlTable (bdd_manager *dd, st_table *table) |
| void | SynthPrintTreeList (MlTree *list) |
| void | SynthPrintLeafList (MlTree *list) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: synthFactor.c,v 1.49 2005/04/23 14:37:51 jinh Exp $" |
| static bdd_node *(* | ZddProductFunc )(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product |
| static bdd_node *(* | ZddProductRecurFunc )(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product_recur |
| static bdd_node *(* | ZddDivideFunc )(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div |
| static bdd_node *(* | ZddDivideRecurFunc )(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div_recur |
| static bdd_node *(* | ZddDivisorFunc )(bdd_manager *, bdd_node *) = Synth_ZddQuickDivisor |
| static int | NumTree |
| static int | ResolveConflictMode = 0 |
| static st_table * | HeadListTable |
| static st_table * | TailListTable |
| static MlTree * | MlTreeHead |
| static MlSizeList * | MlSizeHead |
| int | UseMtree = 1 |
| int | UseCommonDivisor = 1 |
| int | TryNodeSharing = 0 |
| int | Resubstitution = 1 |
| int | RemainderComplement = 0 |
| int | noMemoryFlag = 0 |
| int | VerifyTreeMode = 0 |
| bdd_node *(*)(bdd_manager *, bdd_node *, bdd_node *) | SynthGetZddProductFunc (void) |
| bdd_node *(*)(bdd_manager *, bdd_node *, bdd_node *) | SynthGetZddProductRecurFunc (void) |
| bdd_node *(*)(bdd_manager *, bdd_node *, bdd_node *) | SynthGetZddDivideFunc (void) |
| bdd_node *(*)(bdd_manager *, bdd_node *, bdd_node *) | SynthGetZddDivideRecurFunc (void) |
| bdd_node *(*)(bdd_manager *, bdd_node *) | SynthGetZddDivisorFunc (void) |
Typedef Documentation
| typedef struct ml_size_list MlSizeList |
Struct**********************************************************************
Synopsis [Structure of a linked list to keep the sizes of trees.]
Description [Structure of a linked list to keep the sizes of trees. The size is in terms of number of literals of a tree. This is used for fast insertion of a tree into the multi-level tree list.]
SeeAlso []
Function Documentation
| static void DeleteMlSizeList | ( | MlTree * | tree | ) | [static] |
Function********************************************************************
Synopsis [Deletes a tree from the size list.]
Description [Deletes a tree from the size list.]
SideEffects []
SeeAlso []
Definition at line 1779 of file synthFactor.c.
{
MlTree *head, *tail, *cur, *pre;
MlSizeList *list, *pre_list;
int size;
size = tree->nLiterals;
pre_list = NIL(MlSizeList);
list = MlSizeHead;
while (list) {
if (size == list->size) {
st_lookup(HeadListTable, list->string, (&head));
st_lookup(TailListTable, list->string, (&tail));
if (head == tail) {
assert(tree == head);
if (pre_list)
pre_list->next = list->next;
else
MlSizeHead = list->next;
st_delete(HeadListTable, (char **)&list->string, NIL(char *));
st_delete(TailListTable, (char **)&list->string, NIL(char *));
FREE(list->string);
FREE(list);
} else {
pre = NIL(MlTree);
cur = head;
while (cur) {
if (cur == tree) {
if (cur == head) {
st_delete(HeadListTable, (char **)&list->string, NIL(char *));
st_insert(HeadListTable, list->string, (char *)cur->next);
} else if (cur == tail) {
st_delete(TailListTable, (char **)&list->string, NIL(char *));
st_insert(TailListTable, list->string, (char *)pre);
}
break;
}
pre = cur;
cur = cur->next;
}
}
break;
} else if (size > list->size)
break;
pre_list = list;
list = list->next;
}
}
Here is the caller graph for this function:
| static void DeleteMlTree | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| MlTree * | kill_tree, | ||
| MlTree * | live_tree, | ||
| int | deref, | ||
| int | comp_flag | ||
| ) | [static] |
Function********************************************************************
Synopsis [Deletes the tree nodes due to conflict.]
Description [Deletes the tree nodes due to conflict.]
SideEffects []
SeeAlso []
Definition at line 1623 of file synthFactor.c.
{
MlTree *cur, *pre, *next;
int ref;
if (kill_tree->shared && deref) {
ref = 0;
cur = MlTreeHead;
while (cur) {
if (cur == kill_tree) {
cur = cur->next;
continue;
}
if (cur->q == kill_tree)
ref++;
else if (cur->d == kill_tree)
ref++;
else if (cur->r == kill_tree)
ref++;
cur = cur->next;
}
if (ref == 1)
kill_tree->shared = 0;
return;
}
DeleteMlSizeList(kill_tree);
if (kill_tree->id == NumTree - 1)
NumTree--;
if (deref) {
bdd_recursive_deref_zdd(dd, kill_tree->node);
st_delete(table, (char **)(&kill_tree->node), NIL(char *));
if (kill_tree->complement) {
bdd_recursive_deref_zdd(dd, kill_tree->complement);
st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
}
}
pre = NIL(MlTree);
cur = MlTreeHead;
while (cur) {
if (cur == kill_tree) {
next = cur->next;
if (pre)
pre->next = next;
else
MlTreeHead = next;
cur = next;
if (!live_tree)
break;
} else {
if (live_tree) {
if (cur->q == kill_tree) {
if (comp_flag)
cur->q_comp ^= 01;
cur->q = live_tree;
cur->q_ref = 1;
if (VerifyTreeMode)
SynthVerifyTree(dd, cur, 0);
} else if (cur->d == kill_tree) {
if (comp_flag)
cur->d_comp ^= 01;
cur->d = live_tree;
cur->d_ref = 1;
if (VerifyTreeMode)
SynthVerifyTree(dd, cur, 0);
} else if (cur->r == kill_tree) {
if (comp_flag)
cur->r_comp ^= 01;
cur->r = live_tree;
cur->r_ref = 1;
if (VerifyTreeMode)
SynthVerifyTree(dd, cur, 0);
}
}
pre = cur;
cur = cur->next;
}
}
if (kill_tree->leaf == 0) {
if (kill_tree->q_ref) {
if (kill_tree->q->shared)
DeleteMlTree(dd, table, kill_tree->q, NULL, 1, 0);
} else
DeleteMlTree(dd, table, kill_tree->q, NULL, 1, 0);
if (kill_tree->d_ref) {
if (kill_tree->d->shared)
DeleteMlTree(dd, table, kill_tree->d, NULL, 1, 0);
} else
DeleteMlTree(dd, table, kill_tree->d, NULL, 1, 0);
if (kill_tree->r_ref) {
if (kill_tree->r->shared)
DeleteMlTree(dd, table, kill_tree->r, NULL, 1, 0);
} else
DeleteMlTree(dd, table, kill_tree->r, NULL, 1, 0);
}
if (kill_tree->support)
FREE(kill_tree->support);
FREE(kill_tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static char * GetIntString | ( | int | v | ) | [static] |
Function********************************************************************
Synopsis [Returns a string containing a given integer value.]
Description [Returns a string containing a given integer value.]
SideEffects []
SeeAlso []
Definition at line 1906 of file synthFactor.c.
{
char string[12];
char *ret;
sprintf(string, "%d", v);
ret = (char *)ALLOC(char, strlen(string) + 1);
strcpy(ret, string);
return(ret);
}
Here is the caller graph for this function:
| static int InsertMlTable | ( | st_table * | table, |
| bdd_node * | node, | ||
| MlTree * | tree | ||
| ) | [static] |
Function********************************************************************
Synopsis [Inserts a new node-tree pair into the node-tree table.]
Description [Inserts a new node-tree pair into the node-tree table.]
SideEffects []
SeeAlso []
Definition at line 1841 of file synthFactor.c.
{
int flag;
flag = st_insert(table, (char *)node, (char *)tree);
if (flag == ST_OUT_OF_MEM) {
(void) fprintf(vis_stdout,"** synth error: Out of Memory.\n");
noMemoryFlag = 1;
return (0);
} else if (flag == 1)
(void) fprintf(vis_stdout, "** synth warning: Duplicate entry.\n");
return(1);
}
Here is the caller graph for this function:
| static bdd_node * MakeComplementOfZddCover | ( | bdd_manager * | dd, |
| bdd_node * | node, | ||
| int | verbosity | ||
| ) | [static] |
Function********************************************************************
Synopsis [Makes the complement of a ZDD node.]
Description [Makes the complement of a ZDD node.]
SideEffects []
SeeAlso []
Definition at line 1870 of file synthFactor.c.
{
bdd_node *comp;
if (verbosity > 1) {
(void) fprintf(vis_stdout,"*****\n");
SynthPrintZddTreeMessage(dd, node, "R : ");
}
comp = bdd_zdd_complement(dd, node);
if (!comp)
return(NULL);
if (verbosity > 1) {
SynthPrintZddTreeMessage(dd, comp, "C : ");
(void) fprintf(vis_stdout,"*****\n");
}
return(comp);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static MlTree * ResolveConflictNode | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| MlTree * | tree1, | ||
| MlTree * | tree2, | ||
| int | comp_flag, | ||
| int | verbosity | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Resolves the conflict nodes that can be merged.]
Description [Resolves the conflict nodes that can be merged. One tree has a regular node, the other tree has the complement of the node. This case is called conflict. And these two trees are merged into one, and this is called resolution. It happens because by default the complement of remainder is not computed since it is very expensive.]
SideEffects []
SeeAlso []
Definition at line 1543 of file synthFactor.c.
{
MlTree *live_tree, *kill_tree;
if (MlTree_IsComplement(tree1))
tree1 = MlTree_Regular(tree1);
if (MlTree_IsComplement(tree2))
tree2 = MlTree_Regular(tree2);
if (verbosity) {
if (tree1->complement || tree2->complement)
(void) fprintf(vis_stdout, "** synth warning: real conflict.\n");
}
if (ResolveConflictMode == 0) {
live_tree = tree1;
kill_tree = tree2;
} else {
if (tree1->nLiterals > tree2->nLiterals) {
live_tree = tree2;
kill_tree = tree1;
} else {
live_tree = tree1;
kill_tree = tree2;
}
}
if (!live_tree->complement) {
if (comp_flag)
live_tree->complement = kill_tree->node;
else
live_tree->complement = kill_tree->complement;
bdd_ref(live_tree->complement);
bdd_recursive_deref_zdd(dd, kill_tree->node);
st_delete(table, (char **)(&kill_tree->node), NIL(char *));
if (kill_tree->complement) {
bdd_recursive_deref_zdd(dd, kill_tree->complement);
st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
}
st_insert(table, (char *)live_tree->complement,
(char *)MlTree_Not(live_tree));
} else {
bdd_recursive_deref_zdd(dd, kill_tree->node);
st_delete(table, (char **)(&kill_tree->node), NIL(char *));
if (kill_tree->complement) {
bdd_recursive_deref_zdd(dd, kill_tree->complement);
st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
}
}
DeleteMlTree(dd, table, kill_tree, live_tree, 0, comp_flag);
SynthSetSharedFlag(dd, live_tree);
if (VerifyTreeMode) {
SynthVerifyTree(dd, live_tree, 0);
SynthVerifyMlTable(dd, table);
VerifyTreeList();
}
return(live_tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthCheckAndMakeComplement | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| MlTree * | tree, | ||
| int * | comp_flag, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Makes complement node of a tree if it does not exist.]
Description [Makes complement node of a tree if it does not exist. If successful, it returns the same tree or another tree which already has the complemented node. In the latter case, it is called a conflict and the two trees are merged into the other tree, this is called resolution. If not successful, it returns NULL. If the complement already exists, the tree is just returned.]
SideEffects []
SeeAlso []
Definition at line 685 of file synthFactor.c.
{
bdd_node *c;
MlTree *c_tree, *new_;
if (MlTree_IsComplement(tree))
return(tree);
*comp_flag = 0;
if (!tree->complement) {
c = MakeComplementOfZddCover(dd, tree->node, verbosity);
if (!c)
return(NULL);
bdd_ref(c);
c_tree = SynthLookupMlTable(table, dd, (char *)c, 0, verbosity);
if (c_tree) {
MlTree *m_tree = MlTree_Regular(c_tree);
if (MlTree_Regular(tree)->candidate &&
MlTree_Regular(c_tree)->candidate) {
/*
** tree m_tree
** |\ /|
** | \/ |
** | / \ |
** q d
**/
if (ResolveConflictMode == 0 || c_tree == m_tree ||
tree->nLiterals <= m_tree->nLiterals) {
/* throw away m_tree and assign c to tree->complement */
UnlinkMlTree(m_tree);
bdd_recursive_deref_zdd(dd, m_tree->node);
bdd_recursive_deref_zdd(dd, m_tree->complement);
st_delete(table, (char **)(&m_tree->node), NIL(char *));
st_delete(table, (char **)(&m_tree->complement), NIL(char *));
if (m_tree->support)
FREE(m_tree->support);
FREE(m_tree);
tree->complement = c;
if (!InsertMlTable(table, c, MlTree_Not(tree))) {
tree->complement = NIL(bdd_node);
bdd_recursive_deref_zdd(dd, c);
return(NULL);
}
} else if (c_tree != m_tree) {
/* takes m_tree's contents and throws away m_tree */
UnlinkMlTree(tree);
UnlinkMlTree(m_tree);
bdd_recursive_deref_zdd(dd, tree->node);
st_delete(table, (char **)(&tree->node), NIL(char *));
if (tree->support)
FREE(tree->support);
memcpy(tree, m_tree, sizeof(MlTree));
FREE(m_tree);
tree->complement = c;
if (!InsertMlTable(table, tree->node, tree))
return(NULL);
if (!InsertMlTable(table, tree->complement, MlTree_Not(tree)))
return(NULL);
} else { /* It never happens at this time,
* the case(c_tree == m_tree) is already taken care of.
* But, it should be implemented to improve
* in the future.
*/
}
if (VerifyTreeMode) {
SynthVerifyTree(dd, tree, 0);
SynthVerifyMlTable(dd, table);
}
return(tree);
} else if (MlTree_Regular(tree)->candidate) {
/*
** tree m_tree
** |\ /|\
** | \/ | \
** | / \ | \
** q d r
**/
if (tree->r == m_tree) {
if (c_tree == m_tree)
*comp_flag = 1;
else
*comp_flag = 0;
if (ResolveConflictMode == 0 || c_tree == m_tree ||
m_tree->nLiterals <= tree->nLiterals) {
/* throw away tree and returns m_tree */
bdd_recursive_deref_zdd(dd, c);
UnlinkMlTree(tree);
bdd_recursive_deref_zdd(dd, tree->node);
st_delete(table, (char **)(&m_tree->node), NIL(char *));
if (tree->support)
FREE(tree->support);
FREE(tree);
} else if (c_tree != m_tree) {
/*
** tree->complement = m_tree->complement
**
** tree m_tree
** |\ /|\
** | \/ | \
** | / \ | \
** q d r
**/
MlTree *r_tree, *tmp_tree;
int r_comp;
int ref;
bdd_node *zero = bdd_read_zero(dd);
/* takes tree's contents and throw away tree and m_tree->r */
bdd_recursive_deref_zdd(dd, c);
r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref,
verbosity);
if (!r_tree)
return(NULL);
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
m_tree->r_comp = 1;
}
tmp_tree = r_tree;
r_tree = SynthCheckAndMakeComplement(dd, table, r_tree,
&r_comp, verbosity);
if (!r_tree)
return(NULL);
else if (r_tree != tmp_tree) {
if (r_comp)
m_tree->r_comp = 1;
ref = 1;
}
tree->r = r_tree;
tree->r_ref = ref;
tree->id = m_tree->id;
tree->candidate = 0;
bdd_recursive_deref_zdd(dd, m_tree->node);
bdd_recursive_deref_zdd(dd, m_tree->complement);
st_delete(table, (char **)(&m_tree->node), NIL(char *));
st_delete(table, (char **)(&m_tree->complement), NIL(char *));
UnlinkMlTree(m_tree);
if (m_tree->support)
FREE(m_tree->support);
ref = m_tree->r_ref;
r_tree = m_tree->r;
memcpy(m_tree, tree, sizeof(MlTree));
FREE(tree);
SynthPutMlTreeInList(dd, m_tree, 0);
if (ref) {
if (r_tree->shared)
DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
} else
DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
} else { /* It never happens at this time,
* the case(c_tree == m_tree) is already taken care of.
* But, it should be implemented to improve
* in the future.
*/
}
if (VerifyTreeMode) {
SynthVerifyTree(dd, m_tree, 0);
SynthVerifyMlTable(dd, table);
}
return(m_tree);
}
if (!SynthUseCandidate(table, dd, tree, verbosity)) {
bdd_recursive_deref_zdd(dd, c);
return(NULL);
}
SynthSetSharedFlag(dd, tree);
} else if (MlTree_Regular(c_tree)->candidate) {
if (m_tree->r == tree) {
/*
** m_tree tree
** |\ /|\
** | \/ | \
** | / \ | \
** q d r
**/
if (ResolveConflictMode == 0 || c_tree == m_tree ||
tree->nLiterals <= m_tree->nLiterals) {
/* throw away m_tree and assign c to tree->complement */
UnlinkMlTree(m_tree);
bdd_recursive_deref_zdd(dd, m_tree->node);
bdd_recursive_deref_zdd(dd, m_tree->complement);
st_delete(table, (char **)(&m_tree->node), NIL(char *));
st_delete(table, (char **)(&m_tree->complement), NIL(char *));
if (m_tree->support)
FREE(m_tree->support);
FREE(m_tree);
tree->complement = c;
if (!InsertMlTable(table, c, MlTree_Not(tree))) {
tree->complement = NIL(bdd_node);
bdd_recursive_deref_zdd(dd, c);
return(NULL);
}
} else if (c_tree != m_tree) {
/*
** tree->complement = m_tree->complement
**
** m_tree tree
** |\ /|\
** | \/ | \
** | / \ | \
** q d r
**/
MlTree *r_tree, *tmp_tree;
int r_comp;
int ref;
bdd_node *zero = bdd_read_zero(dd);
/* takes m_tree's contents and throw away m_tree and tree->r */
bdd_recursive_deref_zdd(dd, c);
r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref,
verbosity);
if (!r_tree)
return(NULL);
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
m_tree->r_comp = 1;
}
tmp_tree = r_tree;
r_tree = SynthCheckAndMakeComplement(dd, table, r_tree,
&r_comp, verbosity);
if (!r_tree)
return(NULL);
else if (r_tree != tmp_tree) {
if (r_comp)
m_tree->r_comp = 1;
ref = 1;
}
m_tree->r = r_tree;
m_tree->r_ref = ref;
m_tree->id = tree->id;
m_tree->candidate = 0;
bdd_recursive_deref_zdd(dd, tree->node);
st_delete(table, (char **)(&tree->node), NIL(char *));
UnlinkMlTree(tree);
if (tree->support)
FREE(tree->support);
ref = tree->r_ref;
r_tree = tree->r;
memcpy(tree, m_tree, sizeof(MlTree));
FREE(m_tree);
SynthPutMlTreeInList(dd, tree, 0);
if (ref) {
if (r_tree->shared)
DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
} else
DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
} else { /* It never happens at this time,
* the case(c_tree == m_tree) is already taken care of.
* But, it should be implemented to improve
* in the future.
*/
/*
** tree->complement = m_tree->node
**
** m_tree tree
** |\ /|\
** | \/ | \
** | / \ | \
** q d r
**/
}
return(tree);
}
if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, c);
return(NULL);
}
SynthSetSharedFlag(dd, m_tree);
}
bdd_recursive_deref_zdd(dd, c);
if (c_tree == m_tree)
*comp_flag = 1;
else
*comp_flag = 0;
if (verbosity)
(void) fprintf(vis_stdout, "** synth warning: Duplicate entry ...\n");
new_ = ResolveConflictNode(dd, table, c_tree, tree, *comp_flag, verbosity);
if (verbosity)
(void) fprintf(vis_stdout, "** synth info: Conflict was resolved.\n");
if (VerifyTreeMode) {
SynthVerifyTree(dd, new_, 0);
SynthVerifyMlTable(dd, table);
}
return(new_);
} else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) {
bdd_recursive_deref_zdd(dd, c);
return(NULL);
}
tree->complement = c;
if (!InsertMlTable(table, c, MlTree_Not(tree))) {
tree->complement = NIL(bdd_node);
bdd_recursive_deref_zdd(dd, c);
return NULL;
}
}
return(tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void SynthClearMlTable | ( | bdd_manager * | dd, |
| st_table * | table | ||
| ) |
Function********************************************************************
Synopsis [Dereferences each node of the node-tree table.]
Description [Dereferences each node of the node-tree table.]
SideEffects []
SeeAlso []
Definition at line 482 of file synthFactor.c.
{
st_generator *gen;
bdd_node *k;
MlTree *r;
MlSizeList *l, *next;
st_foreach_item(table, gen, (&k), (&r)) {
bdd_recursive_deref_zdd(dd, k);
if (!MlTree_IsComplement(r))
SynthFreeMlTree(r, 0);
}
NumTree = 1;
MlTreeHead = NIL(MlTree);
st_free_table(HeadListTable);
st_free_table(TailListTable);
HeadListTable = TailListTable = NIL(st_table);
l = MlSizeHead;
while (l) {
next = l->next;
FREE(l->string);
FREE(l);
l = next;
}
MlSizeHead = NIL(MlSizeList);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthFindOrCreateMlTree | ( | st_table * | table, |
| bdd_manager * | dd, | ||
| bdd_node * | f, | ||
| int | leaf, | ||
| int | candidate, | ||
| int * | ref, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Looks up the node-tree table first; if f is found, it returns the existing tree, otherwise it creates a new tree.]
Description [Looks up the node-tree table first, if f is found, it returns the existing tree, otherwise it creates a new tree. The return value of this function will be NULL only when reordering takes place or memory allocation fails in InsertMlTable.]
SideEffects []
SeeAlso []
Definition at line 395 of file synthFactor.c.
{
MlTree *tree;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
tree = SynthLookupMlTable(table, dd, f, 1, verbosity);
if (tree) {
if (MlTree_Regular(tree)->candidate) {
if (!SynthUseCandidate(table, dd, tree, verbosity)) {
return(NULL);
}
SynthSetSharedFlag(dd, tree);
}
*ref = 1;
return(tree);
} else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
return(NULL);
tree = ALLOC(MlTree, 1);
if (!tree) {
noMemoryFlag = 1;
return(NULL);
}
(void)memset((void *)tree, 0, sizeof(MlTree));
tree->node = f;
bdd_ref(f);
tree->leaf = leaf;
if (bdd_bdd_T(f) == one && bdd_bdd_E(f) == zero)
tree->pi = 1;
if (candidate)
tree->candidate = 1;
if (!tree->candidate) {
tree->id = NumTree;
NumTree++;
}
if (!InsertMlTable(table, f, tree)) {
bdd_recursive_deref_zdd(dd, f);
FREE(tree);
return NULL;
}
*ref = 0;
return(tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthGetHeadTreeOfSize | ( | int | size | ) |
Function********************************************************************
Synopsis [Returns first tree that has the given size in list.]
Description [Returns first tree that has the given size in tree list, if the given size exists in size list. Otherwise it returns NULL.]
SideEffects []
SeeAlso []
Definition at line 650 of file synthFactor.c.
{
MlTree *head;
MlSizeList *list;
list = MlSizeHead;
while (list) {
if (size == list->size) {
st_lookup(HeadListTable, list->string, (&head));
return(head);
} else if (size > list->size)
return(NULL);
list = list->next;
}
return(NULL);
}
Here is the caller graph for this function:
| void SynthGetSpaceString | ( | char * | string, |
| int | n, | ||
| int | max | ||
| ) |
Function********************************************************************
Synopsis [Sets the first n characters of string to spaces.]
Description [Sets the first n characters of string to spaces. n should be less than max.]
SideEffects []
SeeAlso []
Definition at line 238 of file synthFactor.c.
{
int i;
if (n >= max - 1)
n = max - 2;
for (i = 0; i < n; i++)
string[i] = ' ';
string[n] = '\0';
}
Here is the caller graph for this function:
| void SynthInitMlTable | ( | void | ) |
Function********************************************************************
Synopsis [Initializes global variables and tables for factorization.]
Description [Initializes global variables and tables for factorization.]
SideEffects []
SeeAlso []
Definition at line 460 of file synthFactor.c.
{
NumTree = 1;
MlTreeHead = NIL(MlTree);
MlSizeHead = NIL(MlSizeList);
HeadListTable = st_init_table(strcmp, st_strhash);
TailListTable = st_init_table(strcmp, st_strhash);
}
Here is the caller graph for this function:
| MlTree* SynthLookupMlTable | ( | st_table * | table, |
| bdd_manager * | dd, | ||
| bdd_node * | node, | ||
| int | candidate, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Looks up the node-tree table to see if the node exists.]
Description [Looks up the node-tree table to see if the node exists. If node exists in node-tree table, it returns the tree. Otherwise it returns NULL. If the tree is a candidate, the tree is changed to regular one.]
SideEffects []
SeeAlso []
Definition at line 268 of file synthFactor.c.
{
MlTree *tree, *m_tree;
int flag;
flag = st_lookup(table, (char *)node, &tree);
if (flag) {
if (MlTree_Regular(tree)->candidate) {
m_tree = MlTree_Regular(tree);
if (candidate) {
if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
return(NULL);
}
}
}
if (candidate)
SynthSetSharedFlag(dd, tree);
return(tree);
}
return((MlTree *)NULL);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int SynthPostFactoring | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| MlTree *(*)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int) | factoring_func, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Factorizes leaf nodes of MlTree.]
Description [Factorizes leaf nodes of MlTree. A leaf node of MlTree can not be factorized by itself. This function tries to factorize among all leaf nodes. A leaf node can be divided by another leaf node. If successful, it returns 0, otherwise it returns 1 due to lack of memory.]
SideEffects []
SeeAlso []
Definition at line 1044 of file synthFactor.c.
{
MlTree *cur, *candy;
int ref;
bdd_node *q;
bdd_node *zero = bdd_read_zero(dd);
if (VerifyTreeMode) {
SynthVerifyMlTable(dd, table);
VerifyTreeList();
}
cur = MlTreeHead;
while (cur) {
if (cur->leaf) {
if (cur->nLiterals < 2)
break;
candy = cur->next;
while (candy) {
if (candy->nLiterals == 1)
break;
else if (candy->leaf == 0 ||
candy->nLiterals == cur->nLiterals) {
candy = candy->next;
continue;
}
q = (* ZddDivideFunc)(dd, cur->node, candy->node);
if (!q)
return(1);
bdd_ref(q);
/* Even though we deref q, it still exists as a
* pointer and beyond this point, we use it only to
* check if it is zero or not.
*/
bdd_recursive_deref_zdd(dd,q);
if (q != zero) {
(void) (* factoring_func)(dd, table, cur->node,
0, &ref, candy, 0, cur, verbosity);
if (VerifyTreeMode) {
SynthVerifyTree(dd, cur, 0);
SynthVerifyMlTable(dd, table);
VerifyTreeList();
}
if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
return(1);
SynthSetSharedFlag(dd, candy);
break;
} else {
q = (* ZddDivideFunc)(dd, cur->node,
candy->complement);
if (!q)
return(1);
bdd_ref(q);
/* Even though we deref q, it still exists as a
* pointer and beyond this point, we use it only
* to check if it is zero or not.
*/
bdd_recursive_deref_zdd(dd,q);
if (q != zero) {
(void) (* factoring_func)(dd, table, cur->node, 0,
&ref, candy, 1, cur, verbosity);
if (VerifyTreeMode) {
SynthVerifyTree(dd, cur, 0);
SynthVerifyMlTable(dd, table);
VerifyTreeList();
}
if (bdd_read_reordered_field(dd) || noMemoryFlag == 1 )
return(1);
SynthSetSharedFlag(dd, candy);
break;
}
}
candy = candy->next;
}
}
cur = cur->next;
}
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void SynthPrintLeafList | ( | MlTree * | list | ) |
Function********************************************************************
Synopsis [Prints all leaf tree lists.]
Description [Prints all leaf tree lists. Used for debugging.]
SideEffects []
SeeAlso []
Definition at line 1509 of file synthFactor.c.
{
MlTree *cur = list;
if (!cur)
cur = MlTreeHead;
while (cur) {
if (cur->leaf)
printf("%d (%d) [0x%lx]\n", cur->id, cur->nLiterals, (unsigned long)cur);
cur = cur->next;
}
}
| void SynthPrintTreeList | ( | MlTree * | list | ) |
Function********************************************************************
Synopsis [Prints all tree lists.]
Description [Prints all tree lists. Used for debugging.]
SideEffects []
SeeAlso []
Definition at line 1484 of file synthFactor.c.
{
MlTree *cur = list;
if (!cur)
cur = MlTreeHead;
while (cur) {
printf("%d (%d) - %d [0x%lx]\n", cur->id, cur->nLiterals,
cur->leaf, (unsigned long)cur);
cur = cur->next;
}
}
| void SynthPutMlTreeInList | ( | bdd_manager * | dd, |
| MlTree * | tree, | ||
| int | candidate | ||
| ) |
Function********************************************************************
Synopsis [Puts a new tree into MlTree list.]
Description [Puts a new tree into MlTree list. This tree list is used for sharing. Basically MlTree is a linked list sorted by the number of literals of trees and the head tree has the largest literals. Just to increase insertion time, MlSizeList and HeadListTable and TailListTable are used. MlSizeList tells what sizes of trees exist in MlTree list, and since many trees with same number of literals may exist, HeadListTable and TailListTable keep first and last tree with a given number of literals.]
SideEffects []
SeeAlso []
Definition at line 533 of file synthFactor.c.
{
int i;
int word, size;
unsigned int *mask;
int top;
MlTree *last;
MlSizeList *list, *pre_list, *new_list;
word = sizeof(int) * 8;
size = bdd_num_zdd_vars(dd) / word + 1;
if (candidate) {
tree->nLiterals = tree->q->nLiterals + tree->d->nLiterals;
mask = ALLOC(unsigned int, size);
for (i = 0; i < size; i++)
mask[i] = tree->q->support[i] | tree->d->support[i];
tree->support = mask;
} else {
if (tree->nLiterals == 0) {
top = tree->top;
tree->top = 1;
tree->nLiterals = SynthCountMlLiteral(dd, tree, 0);
tree->top = top;
}
if (!tree->support) {
mask = ALLOC(unsigned int, size);
(void)memset((void *)mask, 0, size * sizeof(int));
SynthGetSupportMask(dd, tree->node, mask);
tree->support = mask;
}
}
if ((!MlTreeHead) || (tree->nLiterals > MlTreeHead->nLiterals)) {
tree->next = MlTreeHead;
MlTreeHead = tree;
list = ALLOC(MlSizeList, 1);
list->size = tree->nLiterals;
list->string = GetIntString(list->size);
list->next = MlSizeHead;
MlSizeHead = list;
st_insert(HeadListTable, list->string, (char *)tree);
st_insert(TailListTable, list->string, (char *)tree);
} else {
pre_list = NIL(MlSizeList);
list = MlSizeHead;
while (list) {
if (tree->nLiterals == list->size) {
if (list == MlSizeHead) {
tree->next = MlTreeHead;
MlTreeHead = tree;
st_insert(HeadListTable, list->string, (char *)tree);
} else {
st_lookup(TailListTable, list->string, (&last));
tree->next = last->next;
last->next = tree;
st_insert(TailListTable, list->string, (char *)tree);
}
break;
} else if (tree->nLiterals > list->size) {
st_lookup(TailListTable, pre_list->string, (&last));
tree->next = last->next;
last->next = tree;
new_list = ALLOC(MlSizeList, 1);
new_list->size = tree->nLiterals;
new_list->string = GetIntString(new_list->size);
new_list->next = list;
pre_list->next = new_list;
st_insert(HeadListTable, new_list->string, (char *)tree);
st_insert(TailListTable, new_list->string, (char *)tree);
break;
} else if (!list->next) {
st_lookup(TailListTable, list->string, (&last));
tree->next = NIL(MlTree);
last->next = tree;
new_list = ALLOC(MlSizeList, 1);
new_list->size = tree->nLiterals;
new_list->string = GetIntString(new_list->size);
new_list->next = NIL(MlSizeList);
list->next = new_list;
st_insert(HeadListTable, new_list->string, (char *)tree);
st_insert(TailListTable, new_list->string, (char *)tree);
break;
}
pre_list = list;
list = list->next;
}
}
if (VerifyTreeMode)
VerifyTreeList();
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void SynthSetSharedFlag | ( | bdd_manager * | dd, |
| MlTree * | tree | ||
| ) |
Function********************************************************************
Synopsis [Sets the shared field of tree to 1.]
Description [Sets the shared field of tree to 1.]
SideEffects []
SeeAlso []
Definition at line 1013 of file synthFactor.c.
{
MlTree *t;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
t = MlTree_Regular(tree);
if (t->node == zero || t->node == one)
return;
if (t->pi == 0)
t->shared = 1;
}
Here is the caller graph for this function:
| void SynthSetZddDivisorFunc | ( | int | mode | ) |
Function********************************************************************
Synopsis [Sets the variable ZddDivisorFunc.]
Description [Sets the variable ZddDivisorFunc.]
SideEffects []
SeeAlso []
Definition at line 212 of file synthFactor.c.
{
if (mode == 0)
ZddDivisorFunc = Synth_ZddQuickDivisor;
else if (mode == 1)
ZddDivisorFunc = Synth_ZddLeastDivisor;
else if (mode == 2)
ZddDivisorFunc = Synth_ZddMostDivisor;
else
ZddDivisorFunc = Synth_ZddLevelZeroDivisor;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void SynthUpdateRefOfParent | ( | MlTree * | top | ) |
Function********************************************************************
Synopsis [Updates the ref field of all parent nodes whose one child is top.]
Description [Updates the ref field of all parent nodes whose one child is top.]
SideEffects []
SeeAlso []
Definition at line 1146 of file synthFactor.c.
{
MlTree *cur;
cur = MlTreeHead;
while (cur) {
if (cur->q == top)
cur->q_ref = 1;
else if (cur->d == top)
cur->d_ref = 1;
else if (cur->r == top)
cur->r_ref = 1;
cur = cur->next;
}
}
Here is the caller graph for this function:
| int SynthUseCandidate | ( | st_table * | table, |
| bdd_manager * | dd, | ||
| MlTree * | m_tree, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Makes a candidate tree node a real node.]
Description [Makes a candidate tree node a real node. If successful, it returns 1, otherwise it returns 0. A candidate is a extra tree that keeps a function of 'quotient * divisor'. This candidate can be a regular tree when it is shared.]
SideEffects []
SeeAlso []
Definition at line 311 of file synthFactor.c.
{
MlTree *parent, *c_tree, *tmp_tree;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
int ref;
int comp_flag;
m_tree = MlTree_Regular(m_tree);
if (!m_tree->r) {
(void) fprintf(vis_stdout,
"** synth fatal: Internal error in synthesize_network.\n");
(void) fprintf(vis_stdout,
"** synth fatal: Please report this bug to VIS developers.\n");
return (0);
}
parent = m_tree->r;
m_tree->r = (MlTree *)NULL;
m_tree->candidate = 0;
c_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref, verbosity);
if (!c_tree)
return (0);
if (MlTree_IsComplement(c_tree)) {
c_tree = MlTree_Regular(c_tree);
m_tree->r_comp = 1;
}
tmp_tree = c_tree;
c_tree = SynthCheckAndMakeComplement(dd, table, c_tree,
&comp_flag, verbosity);
if (!c_tree)
return (0);
else if (c_tree != tmp_tree) {
if (comp_flag)
m_tree->r_comp = 1;
ref = 1;
}
m_tree->r = c_tree;
m_tree->r_ref = ref;
parent->q = m_tree;
parent->q_ref = 0;
parent->q_comp = 0;
c_tree = SynthFindOrCreateMlTree(table, dd, one, 1, 0, &ref, verbosity);
if (!c_tree)
return (0);
if (MlTree_IsComplement(c_tree)) {
c_tree = MlTree_Regular(c_tree);
parent->d_comp = 1;
} else
parent->d_comp = 0;
parent->d = c_tree;
parent->d_ref = ref;
m_tree->id = NumTree;
NumTree++;
if (verbosity > 1)
(void)fprintf(vis_stdout, "** synth info: Used candidate %d.\n",
m_tree->id);
if (VerifyTreeMode) {
SynthVerifyTree(dd, parent, 0);
SynthVerifyTree(dd, m_tree, 0);
SynthVerifyMlTable(dd, table);
}
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void SynthVerifyMlTable | ( | bdd_manager * | dd, |
| st_table * | table | ||
| ) |
Function********************************************************************
Synopsis [Verifies the node-tree table to see whether everything is correct.]
Description [Verifies the node-tree table to see whether everything is correct. Used for debugging]
SideEffects []
SeeAlso []
Definition at line 1435 of file synthFactor.c.
{
st_generator *gen;
bdd_node *node;
MlTree *tree, *reg;
st_foreach_item(table, gen, (&node), (&tree)) {
reg = MlTree_Regular(tree);
if ((reg == tree && node != reg->node) ||
(reg != tree && node != reg->complement)) {
(void) fprintf(vis_stdout,
"** synth error: wrong node in tree [%d].\n", reg->id);
}
tree = reg;
if (tree->id >= NumTree) {
(void) fprintf(vis_stdout,
"** synth error: wrong id in tree [%d].\n", tree->id);
}
if (!tree->leaf) {
if (!tree->d) {
(void) fprintf(vis_stdout,
"** synth error: d doesn't exist in tree [%d].\n", tree->id);
}
if (!tree->q) {
(void) fprintf(vis_stdout,
"** synth error: q doesn't exist in tree [%d].\n", tree->id);
}
if (!tree->r && !tree->candidate) {
(void) fprintf(vis_stdout,
"** synth error: r doesn't exist in tree [%d].\n", tree->id);
}
}
}
}
Here is the caller graph for this function:
| void SynthVerifyTree | ( | bdd_manager * | dd, |
| MlTree * | tree, | ||
| int | flag | ||
| ) |
Function********************************************************************
Synopsis [Verifies whether in a tree everything is correct.]
Description [Verifies whether in a tree everything is correct. Used for debugging. The argument flag is used to control verifying recursively.]
SideEffects []
SeeAlso []
Definition at line 1177 of file synthFactor.c.
{
bdd_node *node, *comp;
bdd_node *q, *d, *r, *f, *m;
int bdd_diff;
if (flag && !tree->leaf) {
if (!tree->q_ref)
SynthVerifyTree(dd, tree->q, flag);
if (!tree->d_ref)
SynthVerifyTree(dd, tree->d, flag);
if (!tree->r_ref)
SynthVerifyTree(dd, tree->r, flag);
}
node = bdd_make_bdd_from_zdd_cover(dd, tree->node);
if (!node)
return;
bdd_ref(node);
if (tree->complement) {
comp = bdd_make_bdd_from_zdd_cover(dd, tree->complement);
if (!comp) {
bdd_recursive_deref(dd, node);
return;
}
bdd_ref(comp);
if (node != bdd_not_bdd_node(comp)) {
(void) fprintf(vis_stdout,
"** synth error: Invalid complement node in tree [%d].\n", tree->id);
}
bdd_recursive_deref(dd, comp);
}
if (tree->leaf) {
if (tree->q) {
(void) fprintf(vis_stdout,
"** synth error: q exists in leaf tree [%d].\n", tree->id);
}
if (tree->d) {
(void) fprintf(vis_stdout,
"** synth error: d exists in leaf tree [%d].\n", tree->id);
}
if (tree->r) {
(void) fprintf(vis_stdout,
"** synth error: r exists in leaf tree [%d].\n", tree->id);
}
if (tree->q_ref) {
(void) fprintf(vis_stdout,
"** synth error: q_ref = 1 in leaf tree [%d].\n", tree->id);
}
if (tree->d_ref) {
(void) fprintf(vis_stdout,
"** synth error: d_ref = 1 in leaf tree [%d].\n", tree->id);
}
if (tree->r_ref) {
(void) fprintf(vis_stdout,
"** synth error: r_ref = 1 in leaf tree [%d].\n", tree->id);
}
if (tree->q_comp) {
(void) fprintf(vis_stdout,
"** synth error: q_comp = 1 in leaf tree [%d].\n", tree->id);
}
if (tree->d_comp) {
(void) fprintf(vis_stdout,
"** synth error: d_comp = 1 in leaf tree [%d].\n", tree->id);
}
if (tree->r_comp) {
(void) fprintf(vis_stdout,
"** synth error: r_comp = 1 in leaf tree [%d].\n", tree->id);
}
bdd_recursive_deref(dd, node);
return;
}
else {
if (tree->pi) {
(void) fprintf(vis_stdout,
"** synth error: pi = 1 in non-leaf tree [%d].\n", tree->id);
}
}
if (!tree->q) {
(void) fprintf(vis_stdout,
"** synth error: no q in tree [%d].\n", tree->id);
bdd_recursive_deref(dd, node);
return;
}
if (tree->q_comp)
q = bdd_make_bdd_from_zdd_cover(dd, tree->q->complement);
else
q = bdd_make_bdd_from_zdd_cover(dd, tree->q->node);
if (!q) {
(void) fprintf(vis_stdout,
"** synth error: no q node in tree [%d].\n", tree->id);
bdd_recursive_deref(dd, node);
return;
}
bdd_ref(q);
if (!tree->d) {
(void) fprintf(vis_stdout,
"** synth error: no d in tree [%d].\n", tree->id);
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, q);
return;
}
if (tree->d_comp)
d = bdd_make_bdd_from_zdd_cover(dd, tree->d->complement);
else
d = bdd_make_bdd_from_zdd_cover(dd, tree->d->node);
if (!d) {
(void) fprintf(vis_stdout,
"** synth error: no d node in tree [%d].\n", tree->id);
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, q);
return;
}
bdd_ref(d);
if (!tree->candidate) {
if (!tree->r) {
(void) fprintf(vis_stdout,
"** synth error: no r in tree [%d].\n", tree->id);
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, q);
bdd_recursive_deref(dd, d);
return;
}
if (tree->r_comp)
r = bdd_make_bdd_from_zdd_cover(dd, tree->r->complement);
else
r = bdd_make_bdd_from_zdd_cover(dd, tree->r->node);
if (!r) {
(void) fprintf(vis_stdout,
"** synth error: no r node in tree [%d].\n", tree->id);
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, q);
bdd_recursive_deref(dd, d);
return;
}
bdd_ref(r);
m = bdd_bdd_and(dd, q, d);
if (!m) {
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, q);
bdd_recursive_deref(dd, d);
bdd_recursive_deref(dd, r);
return;
}
bdd_ref(m);
bdd_recursive_deref(dd, q);
bdd_recursive_deref(dd, d);
f = bdd_bdd_or(dd, m, r);
if (!f) {
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, r);
bdd_recursive_deref(dd, m);
return;
}
bdd_ref(f);
bdd_recursive_deref(dd, r);
bdd_recursive_deref(dd, m);
} else {
f = bdd_bdd_and(dd, q, d);
if (!f) {
bdd_recursive_deref(dd, node);
bdd_recursive_deref(dd, q);
bdd_recursive_deref(dd, d);
return;
}
bdd_ref(f);
bdd_recursive_deref(dd, q);
bdd_recursive_deref(dd, d);
}
if (!f) {
bdd_recursive_deref(dd, node);
return;
}
if (f == node)
bdd_diff = 0;
else
bdd_diff = 1;
bdd_recursive_deref(dd, f);
bdd_recursive_deref(dd, node);
if (tree->comp)
node = tree->complement;
else
node = tree->node;
if (tree->q_comp)
q = tree->q->complement;
else
q = tree->q->node;
if (tree->d_comp)
d = tree->d->complement;
else
d = tree->d->node;
if (!tree->candidate) {
if (tree->r_comp)
r = tree->r->complement;
else
r = tree->r->node;
m = (* SynthGetZddProductFunc())(dd, d, q);
if (!m)
return;
bdd_ref(m);
f = bdd_zdd_union(dd, m, r);
if (!f) {
bdd_recursive_deref_zdd(dd, m);
return;
}
bdd_ref(f);
bdd_recursive_deref_zdd(dd, m);
} else {
f = (* SynthGetZddProductFunc())(dd, d, q);
if (!f)
return;
bdd_ref(f);
}
if (f != node) {
if (bdd_diff) {
(void) fprintf(vis_stdout,
"** synth error: BDD & ZDD f != qd+r in tree [%d - 0x%lx].\n",
tree->id, (unsigned long)tree);
}
else {
(void) fprintf(vis_stdout,
"Warning : ZDD f != qd+r in tree [%d - 0x%lx].\n",
tree->id, (unsigned long)tree);
}
}
else if (bdd_diff) {
(void) fprintf(vis_stdout,
"** synth error: BDD f != qd+r in tree [%d - 0x%lx].\n",
tree->id, (unsigned long)tree);
}
bdd_recursive_deref_zdd(dd, f);
}
Here is the caller graph for this function:
| static void UnlinkMlTree | ( | MlTree * | kill_tree | ) | [static] |
Function********************************************************************
Synopsis [Unlinks a tree from the list.]
Description [Unlinks a tree from the list.]
SideEffects []
SeeAlso []
Definition at line 1745 of file synthFactor.c.
{
MlTree *cur, *pre;
DeleteMlSizeList(kill_tree);
pre = (MlTree *)NULL;
cur = MlTreeHead;
while (cur) {
if (cur == kill_tree) {
if (pre)
pre->next = cur->next;
else
MlTreeHead = cur->next;
break;
}
pre = cur;
cur = cur->next;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void VerifyTreeList | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Verify all tree lists to see whether all is correct.]
Description [Verify all tree lists to see whether all is correct. Used for debugging.]
SideEffects []
SeeAlso []
Definition at line 1931 of file synthFactor.c.
{
int count;
MlTree *cur, *candy;
cur = MlTreeHead;
while (cur) {
count = 0;
candy = cur->next;
if (candy && candy->nLiterals > cur->nLiterals) {
(void) fprintf(vis_stdout,
"** synth error: predecessor[%d]'s size < successor[%d]'s size.\n",
cur->id, candy->id);
}
while (candy) {
if (cur->id != 0) {
if (candy->id == cur->id && candy != cur) {
(void) fprintf(vis_stdout,
"** synth error: same id already exists [%d].\n", cur->id);
break;
}
}
if (candy == cur) {
if (count > 0) {
(void) fprintf(vis_stdout,
"** synth error: same address already exists [%d - 0x%lx].\n",
cur->id, (unsigned long)cur);
break;
}
count++;
}
candy = candy->next;
}
cur = cur->next;
}
}
Here is the caller graph for this function:
Variable Documentation
st_table* HeadListTable [static] |
Definition at line 63 of file synthFactor.c.
MlSizeList* MlSizeHead [static] |
Definition at line 65 of file synthFactor.c.
MlTree* MlTreeHead [static] |
Definition at line 64 of file synthFactor.c.
| int noMemoryFlag = 0 |
Definition at line 72 of file synthFactor.c.
int NumTree [static] |
Definition at line 61 of file synthFactor.c.
| int RemainderComplement = 0 |
Definition at line 71 of file synthFactor.c.
int ResolveConflictMode = 0 [static] |
Definition at line 62 of file synthFactor.c.
| int Resubstitution = 1 |
Definition at line 70 of file synthFactor.c.
| bdd_node*(* )(bdd_manager *, bdd_node *, bdd_node *) SynthGetZddDivideFunc(void) |
Function********************************************************************
Synopsis [Returns the variable ZddDivideFunc.]
Description [Returns the variable ZddDivideFunc.]
SideEffects []
SeeAlso []
Definition at line 158 of file synthFactor.c.
{
return(ZddDivideFunc);
}
| bdd_node*(* )(bdd_manager *, bdd_node *, bdd_node *) SynthGetZddDivideRecurFunc(void) |
Function********************************************************************
Synopsis [Returns the variable ZddDivideRecurFunc.]
Description [Returns the variable ZddDivideRecurFunc.]
SideEffects []
SeeAlso []
Definition at line 176 of file synthFactor.c.
{
return(ZddDivideRecurFunc);
}
| bdd_node*(* )(bdd_manager *, bdd_node *) SynthGetZddDivisorFunc(void) |
Function********************************************************************
Synopsis [Returns the variable ZddDivisorFunc.]
Description [Returns the variable ZddDivisorFunc.]
SideEffects []
SeeAlso []
Definition at line 194 of file synthFactor.c.
{
return(ZddDivisorFunc);
}
| bdd_node*(* )(bdd_manager *, bdd_node *, bdd_node *) SynthGetZddProductFunc(void) |
AutomaticEnd Function********************************************************************
Synopsis [Returns the variable ZddProductFunc.]
Description [Returns the variable ZddProductFunc.]
SideEffects []
SeeAlso []
Definition at line 122 of file synthFactor.c.
{
return(ZddProductFunc);
}
| bdd_node*(* )(bdd_manager *, bdd_node *, bdd_node *) SynthGetZddProductRecurFunc(void) |
Function********************************************************************
Synopsis [Returns the variable ZddProductRecurFunc.]
Description [Returns the variable ZddProductRecurFunc.]
SideEffects []
SeeAlso []
Definition at line 140 of file synthFactor.c.
{
return(ZddProductRecurFunc);
}
| st_table * TailListTable |
Definition at line 63 of file synthFactor.c.
| int TryNodeSharing = 0 |
Definition at line 69 of file synthFactor.c.
char rcsid [] UNUSED = "$Id: synthFactor.c,v 1.49 2005/04/23 14:37:51 jinh Exp $" [static] |
CFile***********************************************************************
FileName [synthFactor.c]
PackageName [synth]
Synopsis [Multilevel optimization 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 synthFactor.c.
| int UseCommonDivisor = 1 |
Definition at line 68 of file synthFactor.c.
| int UseMtree = 1 |
Definition at line 67 of file synthFactor.c.
| int VerifyTreeMode = 0 |
Definition at line 73 of file synthFactor.c.
bdd_node*(* ZddDivideFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div [static] |
Definition at line 58 of file synthFactor.c.
bdd_node*(* ZddDivideRecurFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div_recur [static] |
Definition at line 59 of file synthFactor.c.
bdd_node*(* ZddDivisorFunc)(bdd_manager *, bdd_node *) = Synth_ZddQuickDivisor [static] |
Definition at line 60 of file synthFactor.c.
bdd_node*(* ZddProductFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product [static] |
Definition at line 56 of file synthFactor.c.
bdd_node*(* ZddProductRecurFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product_recur [static] |
Definition at line 57 of file synthFactor.c.
