/**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.] ******************************************************************************/ #include "synthInt.h" static char rcsid[] UNUSED = "$Id: synthFactor.c,v 1.49 2005/04/23 14:37:51 jinh Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ typedef struct ml_size_list { int size; /* the number of literals */ char *string; /* string of the size to put into st_table */ struct ml_size_list *next; } MlSizeList; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ 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, *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; /* ** 0 : nothing ** 1 : incrementally ** 2 : recursively after each factorization ** 3 : 2 & dump blif file with bdds */ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Returns the variable ZddProductFunc.] Description [Returns the variable ZddProductFunc.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_node * (* SynthGetZddProductFunc(void))(bdd_manager *, bdd_node *, bdd_node *) { return(ZddProductFunc); } /**Function******************************************************************** Synopsis [Returns the variable ZddProductRecurFunc.] Description [Returns the variable ZddProductRecurFunc.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_node * (* SynthGetZddProductRecurFunc(void))(bdd_manager *, bdd_node *, bdd_node *) { return(ZddProductRecurFunc); } /**Function******************************************************************** Synopsis [Returns the variable ZddDivideFunc.] Description [Returns the variable ZddDivideFunc.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_node * (* SynthGetZddDivideFunc(void))(bdd_manager *, bdd_node *, bdd_node *) { return(ZddDivideFunc); } /**Function******************************************************************** Synopsis [Returns the variable ZddDivideRecurFunc.] Description [Returns the variable ZddDivideRecurFunc.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_node * (* SynthGetZddDivideRecurFunc(void))(bdd_manager *, bdd_node *, bdd_node *) { return(ZddDivideRecurFunc); } /**Function******************************************************************** Synopsis [Returns the variable ZddDivisorFunc.] Description [Returns the variable ZddDivisorFunc.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_node * (* SynthGetZddDivisorFunc(void))(bdd_manager *, bdd_node *) { return(ZddDivisorFunc); } /**Function******************************************************************** Synopsis [Sets the variable ZddDivisorFunc.] Description [Sets the variable ZddDivisorFunc.] SideEffects [] SeeAlso [] ******************************************************************************/ void SynthSetZddDivisorFunc(int mode) { if (mode == 0) ZddDivisorFunc = Synth_ZddQuickDivisor; else if (mode == 1) ZddDivisorFunc = Synth_ZddLeastDivisor; else if (mode == 2) ZddDivisorFunc = Synth_ZddMostDivisor; else ZddDivisorFunc = Synth_ZddLevelZeroDivisor; } /**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 [] ******************************************************************************/ void SynthGetSpaceString(char *string, int n, int max) { int i; if (n >= max - 1) n = max - 2; for (i = 0; i < n; i++) string[i] = ' '; string[n] = '\0'; } /**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 [] ******************************************************************************/ MlTree * SynthLookupMlTable(st_table *table, bdd_manager *dd, bdd_node *node, int candidate, int verbosity) { 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); } /**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 [] ******************************************************************************/ int SynthUseCandidate(st_table *table, bdd_manager *dd, MlTree *m_tree, int verbosity) { 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); } /**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 [] ******************************************************************************/ MlTree * SynthFindOrCreateMlTree(st_table *table, bdd_manager *dd, bdd_node *f, int leaf, int candidate, int *ref, int verbosity) { 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); } /**Function******************************************************************** Synopsis [Initializes global variables and tables for factorization.] Description [Initializes global variables and tables for factorization.] SideEffects [] SeeAlso [] ******************************************************************************/ void SynthInitMlTable(void) { NumTree = 1; MlTreeHead = NIL(MlTree); MlSizeHead = NIL(MlSizeList); HeadListTable = st_init_table(strcmp, st_strhash); TailListTable = st_init_table(strcmp, st_strhash); } /**Function******************************************************************** Synopsis [Dereferences each node of the node-tree table.] Description [Dereferences each node of the node-tree table.] SideEffects [] SeeAlso [] ******************************************************************************/ void SynthClearMlTable(bdd_manager *dd, st_table *table) { 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); } /**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 [] ******************************************************************************/ void SynthPutMlTreeInList(bdd_manager *dd, MlTree *tree, int candidate) { 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(); } /**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 [] ******************************************************************************/ MlTree * SynthGetHeadTreeOfSize(int size) { 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); } /**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 [] ******************************************************************************/ MlTree * SynthCheckAndMakeComplement(bdd_manager *dd, st_table *table, MlTree *tree, int *comp_flag, int verbosity) { 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); } /**Function******************************************************************** Synopsis [Sets the shared field of tree to 1.] Description [Sets the shared field of tree to 1.] SideEffects [] SeeAlso [] ******************************************************************************/ void SynthSetSharedFlag(bdd_manager *dd, MlTree *tree) { 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; } /**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 [] ******************************************************************************/ 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) { 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); } /**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 [] ******************************************************************************/ void SynthUpdateRefOfParent(MlTree *top) { 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; } } /**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 [] ******************************************************************************/ void SynthVerifyTree(bdd_manager *dd, MlTree *tree, int flag) { 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); } /**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 [] ******************************************************************************/ void SynthVerifyMlTable(bdd_manager *dd, st_table *table) { 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); } } } } /**Function******************************************************************** Synopsis [Prints all tree lists.] Description [Prints all tree lists. Used for debugging.] SideEffects [] SeeAlso [] ******************************************************************************/ void SynthPrintTreeList(MlTree *list) { 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; } } /**Function******************************************************************** Synopsis [Prints all leaf tree lists.] Description [Prints all leaf tree lists. Used for debugging.] SideEffects [] SeeAlso [] ******************************************************************************/ void SynthPrintLeafList(MlTree *list) { 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; } } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ static MlTree * ResolveConflictNode(bdd_manager *dd, st_table *table, MlTree *tree1, MlTree *tree2, int comp_flag, int verbosity) { 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); } /**Function******************************************************************** Synopsis [Deletes the tree nodes due to conflict.] Description [Deletes the tree nodes due to conflict.] SideEffects [] SeeAlso [] ******************************************************************************/ static void DeleteMlTree(bdd_manager *dd, st_table *table, MlTree *kill_tree, MlTree *live_tree, int deref, int comp_flag) { 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); } /**Function******************************************************************** Synopsis [Unlinks a tree from the list.] Description [Unlinks a tree from the list.] SideEffects [] SeeAlso [] ******************************************************************************/ static void UnlinkMlTree(MlTree *kill_tree) { 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; } } /**Function******************************************************************** Synopsis [Deletes a tree from the size list.] Description [Deletes a tree from the size list.] SideEffects [] SeeAlso [] ******************************************************************************/ static void DeleteMlSizeList(MlTree *tree) { 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; } } /**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 [] ******************************************************************************/ static int InsertMlTable(st_table *table, bdd_node *node, MlTree *tree) { 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); } /**Function******************************************************************** Synopsis [Makes the complement of a ZDD node.] Description [Makes the complement of a ZDD node.] SideEffects [] SeeAlso [] ******************************************************************************/ static bdd_node * MakeComplementOfZddCover(bdd_manager *dd, bdd_node *node, int verbosity) { 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); } /**Function******************************************************************** Synopsis [Returns a string containing a given integer value.] Description [Returns a string containing a given integer value.] SideEffects [] SeeAlso [] ******************************************************************************/ static char * GetIntString(int v) { char string[12]; char *ret; sprintf(string, "%d", v); ret = (char *)ALLOC(char, strlen(string) + 1); strcpy(ret, string); return(ret); } /**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 [] ******************************************************************************/ static void VerifyTreeList(void) { 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; } }