source: vis_dev/vis-2.3/src/synth/synthFactor.c @ 30

Last change on this file since 30 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 50.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthFactor.c]
4
5  PackageName [synth]
6
7  Synopsis    [Multilevel optimization functions.]
8
9  Author      [In-Ho Moon, Balakrishna Kumthekar]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "synthInt.h"
18
19static char rcsid[] UNUSED = "$Id: synthFactor.c,v 1.49 2005/04/23 14:37:51 jinh Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25
26/*---------------------------------------------------------------------------*/
27/* Type declarations                                                         */
28/*---------------------------------------------------------------------------*/
29
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35/**Struct**********************************************************************
36
37  Synopsis    [Structure of a linked list to keep the sizes of trees.]
38
39  Description [Structure of a linked list to keep the sizes of trees.
40  The size is in terms of number of literals of a tree. This is used for
41  fast insertion of a tree into the multi-level tree list.]
42
43  SeeAlso     []
44
45******************************************************************************/
46typedef struct ml_size_list {
47    int                 size;   /* the number of literals */
48    char                *string; /* string of the size to put into st_table */
49    struct ml_size_list *next;
50} MlSizeList;
51
52/*---------------------------------------------------------------------------*/
53/* Variable declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56static  bdd_node        *(* ZddProductFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product;
57static  bdd_node        *(* ZddProductRecurFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product_recur;
58static  bdd_node        *(* ZddDivideFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div;
59static  bdd_node        *(* ZddDivideRecurFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div_recur;
60static  bdd_node        *(* ZddDivisorFunc)(bdd_manager *, bdd_node *) = Synth_ZddQuickDivisor;
61static  int             NumTree;
62static  int             ResolveConflictMode = 0;
63static  st_table        *HeadListTable, *TailListTable;
64static  MlTree          *MlTreeHead;
65static  MlSizeList      *MlSizeHead;
66
67int             UseMtree = 1;
68int             UseCommonDivisor = 1;
69int             TryNodeSharing = 0;
70int             Resubstitution = 1;
71int             RemainderComplement = 0;
72int             noMemoryFlag = 0;
73int             VerifyTreeMode = 0;
74                /*
75                ** 0 : nothing
76                ** 1 : incrementally
77                ** 2 : recursively after each factorization
78                ** 3 : 2 & dump blif file with bdds
79                */
80
81/**AutomaticStart*************************************************************/
82
83/*---------------------------------------------------------------------------*/
84/* Static function prototypes                                                */
85/*---------------------------------------------------------------------------*/
86
87static MlTree * ResolveConflictNode(bdd_manager *dd, st_table *table, MlTree *tree1, MlTree *tree2, int comp_flag, int verbosity);
88static void DeleteMlTree(bdd_manager *dd, st_table *table, MlTree *kill_tree, MlTree *live_tree, int deref, int comp_flag);
89static void UnlinkMlTree(MlTree *kill_tree);
90static void DeleteMlSizeList(MlTree *tree);
91static int InsertMlTable(st_table *table, bdd_node *node, MlTree *tree);
92static bdd_node * MakeComplementOfZddCover(bdd_manager *dd, bdd_node *node, int verbosity);
93static char * GetIntString(int v);
94static void VerifyTreeList(void);
95
96/**AutomaticEnd***************************************************************/
97
98
99/*---------------------------------------------------------------------------*/
100/* Definition of exported functions                                          */
101/*---------------------------------------------------------------------------*/
102
103
104
105/*---------------------------------------------------------------------------*/
106/* Definition of internal functions                                          */
107/*---------------------------------------------------------------------------*/
108
109
110/**Function********************************************************************
111
112  Synopsis [Returns the variable ZddProductFunc.]
113
114  Description [Returns the variable ZddProductFunc.]
115
116  SideEffects []
117
118  SeeAlso     []
119
120******************************************************************************/
121bdd_node        *
122(* SynthGetZddProductFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
123{
124    return(ZddProductFunc);
125}
126
127
128/**Function********************************************************************
129
130  Synopsis [Returns the variable ZddProductRecurFunc.]
131
132  Description [Returns the variable ZddProductRecurFunc.]
133
134  SideEffects []
135
136  SeeAlso     []
137
138******************************************************************************/
139bdd_node        *
140(* SynthGetZddProductRecurFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
141{
142    return(ZddProductRecurFunc);
143}
144
145
146/**Function********************************************************************
147
148  Synopsis [Returns the variable ZddDivideFunc.]
149
150  Description [Returns the variable ZddDivideFunc.]
151
152  SideEffects []
153
154  SeeAlso     []
155
156******************************************************************************/
157bdd_node        *
158(* SynthGetZddDivideFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
159{
160    return(ZddDivideFunc);
161}
162
163
164/**Function********************************************************************
165
166  Synopsis [Returns the variable ZddDivideRecurFunc.]
167
168  Description [Returns the variable ZddDivideRecurFunc.]
169
170  SideEffects []
171
172  SeeAlso     []
173
174******************************************************************************/
175bdd_node        *
176(* SynthGetZddDivideRecurFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
177{
178    return(ZddDivideRecurFunc);
179}
180
181
182/**Function********************************************************************
183
184  Synopsis [Returns the variable ZddDivisorFunc.]
185
186  Description [Returns the variable ZddDivisorFunc.]
187
188  SideEffects []
189
190  SeeAlso     []
191
192******************************************************************************/
193bdd_node        *
194(* SynthGetZddDivisorFunc(void))(bdd_manager *, bdd_node *)
195{
196    return(ZddDivisorFunc);
197}
198
199
200/**Function********************************************************************
201
202  Synopsis [Sets the variable ZddDivisorFunc.]
203
204  Description [Sets the variable ZddDivisorFunc.]
205
206  SideEffects []
207
208  SeeAlso     []
209
210******************************************************************************/
211void
212SynthSetZddDivisorFunc(int mode)
213{
214  if (mode == 0)
215    ZddDivisorFunc = Synth_ZddQuickDivisor;
216  else if (mode == 1)
217    ZddDivisorFunc = Synth_ZddLeastDivisor;
218  else if (mode == 2)
219    ZddDivisorFunc = Synth_ZddMostDivisor;
220  else
221    ZddDivisorFunc = Synth_ZddLevelZeroDivisor;
222}
223
224
225/**Function********************************************************************
226
227  Synopsis [Sets the first n characters of string to spaces.]
228
229  Description [Sets the first n characters of string to spaces. n should
230  be less than max.]
231
232  SideEffects []
233
234  SeeAlso     []
235
236******************************************************************************/
237void
238SynthGetSpaceString(char *string,
239                    int n,
240                    int max)
241{
242  int   i;
243
244  if (n >= max - 1)
245    n = max - 2;
246
247  for (i = 0; i < n; i++)
248    string[i] = ' ';
249  string[n] = '\0';
250}
251
252
253/**Function********************************************************************
254
255  Synopsis [Looks up the node-tree table to see if the node exists.]
256
257  Description [Looks up the node-tree table to see if the node exists.
258  If node exists in node-tree table, it returns the tree. Otherwise it
259  returns NULL. If the tree is a candidate, the tree is changed to
260  regular one.]
261
262  SideEffects []
263
264  SeeAlso     []
265
266******************************************************************************/
267MlTree  *
268SynthLookupMlTable(st_table *table,
269                   bdd_manager *dd,
270                   bdd_node *node,
271                   int candidate,
272                   int verbosity)
273{
274  MlTree        *tree, *m_tree;
275  int           flag;
276
277  flag = st_lookup(table, (char *)node, &tree);
278  if (flag) {
279    if (MlTree_Regular(tree)->candidate) {
280      m_tree = MlTree_Regular(tree);
281      if (candidate) {
282        if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
283          return(NULL);
284        }
285      }
286    }
287    if (candidate)
288      SynthSetSharedFlag(dd, tree);
289    return(tree);
290  }
291
292  return((MlTree *)NULL);
293}
294
295
296/**Function********************************************************************
297
298  Synopsis [Makes a candidate tree node a real node.]
299
300  Description [Makes a candidate tree node a real node. If successful,
301  it returns 1, otherwise it returns 0. A candidate is a extra tree that
302  keeps a function of 'quotient * divisor'. This candidate can be a
303  regular tree when it is shared.]
304
305  SideEffects []
306
307  SeeAlso     []
308
309******************************************************************************/
310int
311SynthUseCandidate(st_table *table,
312                  bdd_manager *dd,
313                  MlTree *m_tree,
314                  int verbosity)
315{
316  MlTree        *parent, *c_tree, *tmp_tree;
317  bdd_node      *one = bdd_read_one(dd);
318  bdd_node      *zero = bdd_read_zero(dd);
319  int           ref;
320  int           comp_flag;
321
322  m_tree = MlTree_Regular(m_tree);
323  if (!m_tree->r) {
324    (void) fprintf(vis_stdout,
325                   "** synth fatal: Internal error in synthesize_network.\n");
326    (void) fprintf(vis_stdout,
327                 "** synth fatal: Please report this bug to VIS developers.\n");
328    return (0);
329  }
330  parent = m_tree->r;
331  m_tree->r = (MlTree *)NULL;
332  m_tree->candidate = 0;
333  c_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref, verbosity);
334  if (!c_tree)
335    return (0);
336  if (MlTree_IsComplement(c_tree)) {
337    c_tree = MlTree_Regular(c_tree);
338    m_tree->r_comp = 1;
339  }
340  tmp_tree = c_tree;
341  c_tree = SynthCheckAndMakeComplement(dd, table, c_tree,
342                                       &comp_flag, verbosity);
343  if (!c_tree)
344    return (0);
345  else if (c_tree != tmp_tree) {
346    if (comp_flag)
347        m_tree->r_comp = 1;
348    ref = 1;
349  }
350  m_tree->r = c_tree;
351  m_tree->r_ref = ref;
352  parent->q = m_tree;
353  parent->q_ref = 0;
354  parent->q_comp = 0;
355  c_tree = SynthFindOrCreateMlTree(table, dd, one, 1, 0, &ref, verbosity);
356  if (!c_tree)
357    return (0);
358  if (MlTree_IsComplement(c_tree)) {
359    c_tree = MlTree_Regular(c_tree);
360    parent->d_comp = 1;
361  } else
362    parent->d_comp = 0;
363  parent->d = c_tree;
364  parent->d_ref = ref;
365  m_tree->id = NumTree;
366  NumTree++;
367  if (verbosity > 1)
368    (void)fprintf(vis_stdout, "** synth info: Used candidate %d.\n",
369                  m_tree->id);
370  if (VerifyTreeMode) {
371    SynthVerifyTree(dd, parent, 0);
372    SynthVerifyTree(dd, m_tree, 0);
373    SynthVerifyMlTable(dd, table);
374  }
375  return(1);
376}
377
378
379/**Function********************************************************************
380
381  Synopsis [Looks up the node-tree table first; if f is found, it returns the
382  existing tree, otherwise it creates a new tree.]
383
384  Description [Looks up the node-tree table first, if f is found, it
385  returns the existing tree, otherwise it creates a new tree. The
386  return value of this function will be NULL only when reordering
387  takes place or memory allocation fails in InsertMlTable.]
388
389  SideEffects []
390
391  SeeAlso     []
392
393******************************************************************************/
394MlTree  *
395SynthFindOrCreateMlTree(st_table *table,
396                        bdd_manager *dd,
397                        bdd_node *f,
398                        int leaf,
399                        int candidate,
400                        int *ref,
401                        int verbosity)
402{
403  MlTree        *tree;
404  bdd_node      *one = bdd_read_one(dd);
405  bdd_node      *zero = bdd_read_zero(dd);
406
407  tree = SynthLookupMlTable(table, dd, f, 1, verbosity);
408  if (tree) {
409    if (MlTree_Regular(tree)->candidate) {
410      if (!SynthUseCandidate(table, dd, tree, verbosity)) {
411        return(NULL);
412      }
413      SynthSetSharedFlag(dd, tree);
414    }
415    *ref = 1;
416    return(tree);
417  } else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
418    return(NULL);
419
420  tree = ALLOC(MlTree, 1);
421  if (!tree) {
422    noMemoryFlag = 1;
423    return(NULL);
424  }
425  (void)memset((void *)tree, 0, sizeof(MlTree));
426  tree->node = f;
427  bdd_ref(f);
428  tree->leaf = leaf;
429  if (bdd_bdd_T(f) == one && bdd_bdd_E(f) == zero)
430    tree->pi = 1;
431  if (candidate)
432    tree->candidate = 1;
433  if (!tree->candidate) {
434    tree->id = NumTree;
435    NumTree++;
436  }
437  if (!InsertMlTable(table, f, tree)) {
438    bdd_recursive_deref_zdd(dd, f);
439    FREE(tree);
440    return NULL;
441  }
442  *ref = 0;
443
444  return(tree);
445}
446
447
448/**Function********************************************************************
449
450  Synopsis    [Initializes global variables and tables for factorization.]
451
452  Description [Initializes global variables and tables for factorization.]
453
454  SideEffects []
455
456  SeeAlso     []
457
458******************************************************************************/
459void
460SynthInitMlTable(void)
461{
462  NumTree = 1;
463  MlTreeHead = NIL(MlTree);
464  MlSizeHead = NIL(MlSizeList);
465  HeadListTable = st_init_table(strcmp, st_strhash);
466  TailListTable = st_init_table(strcmp, st_strhash);
467}
468
469
470/**Function********************************************************************
471
472  Synopsis [Dereferences each node of the node-tree table.]
473
474  Description [Dereferences each node of the node-tree table.]
475
476  SideEffects []
477
478  SeeAlso     []
479
480******************************************************************************/
481void
482SynthClearMlTable(bdd_manager *dd,
483                  st_table *table)
484{
485  st_generator  *gen;
486  bdd_node              *k;
487  MlTree                *r;
488  MlSizeList            *l, *next;
489
490  st_foreach_item(table, gen, (&k), (&r)) {
491    bdd_recursive_deref_zdd(dd, k);
492    if (!MlTree_IsComplement(r))
493      SynthFreeMlTree(r, 0);
494  }
495
496  NumTree = 1;
497  MlTreeHead = NIL(MlTree);
498
499  st_free_table(HeadListTable);
500  st_free_table(TailListTable);
501  HeadListTable = TailListTable = NIL(st_table);
502
503  l = MlSizeHead;
504  while (l) {
505    next = l->next;
506    FREE(l->string);
507    FREE(l);
508    l = next;
509  }
510  MlSizeHead = NIL(MlSizeList);
511}
512
513
514/**Function********************************************************************
515
516  Synopsis [Puts a new tree into MlTree list.]
517
518  Description [Puts a new tree into MlTree list. This tree list is used
519  for sharing. Basically MlTree is a linked list sorted by the number of
520  literals of trees and the head tree has the largest literals. Just to
521  increase insertion time, MlSizeList and HeadListTable and TailListTable
522  are used. MlSizeList tells what sizes of trees exist in MlTree list,
523  and since many trees with same number of literals may exist,
524  HeadListTable and TailListTable keep first and last tree with a given
525  number of literals.]
526
527  SideEffects []
528
529  SeeAlso     []
530
531******************************************************************************/
532void
533SynthPutMlTreeInList(bdd_manager *dd,
534                     MlTree *tree,
535                     int candidate)
536{
537  int           i;
538  int           word, size;
539  unsigned int  *mask;
540  int           top;
541  MlTree        *last;
542  MlSizeList    *list, *pre_list, *new_list;
543
544  word = sizeof(int) * 8;
545  size = bdd_num_zdd_vars(dd) / word + 1;
546
547  if (candidate) {
548    tree->nLiterals = tree->q->nLiterals + tree->d->nLiterals;
549
550    mask = ALLOC(unsigned int, size);
551    for (i = 0; i < size; i++)
552      mask[i] = tree->q->support[i] | tree->d->support[i];
553    tree->support = mask;
554  } else {
555    if (tree->nLiterals == 0) {
556      top = tree->top;
557      tree->top = 1;
558      tree->nLiterals = SynthCountMlLiteral(dd, tree, 0);
559      tree->top = top;
560    }
561
562    if (!tree->support) {
563      mask = ALLOC(unsigned int, size);
564      (void)memset((void *)mask, 0, size * sizeof(int));
565      SynthGetSupportMask(dd, tree->node, mask);
566      tree->support = mask;
567    }
568  }
569
570  if ((!MlTreeHead) || (tree->nLiterals > MlTreeHead->nLiterals)) {
571    tree->next = MlTreeHead;
572    MlTreeHead = tree;
573
574    list = ALLOC(MlSizeList, 1);
575    list->size = tree->nLiterals;
576    list->string = GetIntString(list->size);
577    list->next = MlSizeHead;
578    MlSizeHead = list;
579
580    st_insert(HeadListTable, list->string, (char *)tree);
581    st_insert(TailListTable, list->string, (char *)tree);
582  } else {
583    pre_list = NIL(MlSizeList);
584    list = MlSizeHead;
585    while (list) {
586      if (tree->nLiterals == list->size) {
587        if (list == MlSizeHead) {
588          tree->next = MlTreeHead;
589          MlTreeHead = tree;
590          st_insert(HeadListTable, list->string, (char *)tree);
591        } else {
592          st_lookup(TailListTable, list->string, (&last));
593          tree->next = last->next;
594          last->next = tree;
595          st_insert(TailListTable, list->string, (char *)tree);
596        }
597        break;
598      } else if (tree->nLiterals > list->size) {
599        st_lookup(TailListTable, pre_list->string, (&last));
600        tree->next = last->next;
601        last->next = tree;
602
603        new_list = ALLOC(MlSizeList, 1);
604        new_list->size = tree->nLiterals;
605        new_list->string = GetIntString(new_list->size);
606        new_list->next = list;
607        pre_list->next = new_list;
608
609        st_insert(HeadListTable, new_list->string, (char *)tree);
610        st_insert(TailListTable, new_list->string, (char *)tree);
611        break;
612      } else if (!list->next) {
613        st_lookup(TailListTable, list->string, (&last));
614        tree->next = NIL(MlTree);
615        last->next = tree;
616
617        new_list = ALLOC(MlSizeList, 1);
618        new_list->size = tree->nLiterals;
619        new_list->string = GetIntString(new_list->size);
620        new_list->next = NIL(MlSizeList);
621        list->next = new_list;
622
623        st_insert(HeadListTable, new_list->string, (char *)tree);
624        st_insert(TailListTable, new_list->string, (char *)tree);
625        break;
626      }
627      pre_list = list;
628      list = list->next;
629    }
630  }
631
632  if (VerifyTreeMode)
633    VerifyTreeList();
634}
635
636
637/**Function********************************************************************
638
639  Synopsis [Returns first tree that has the given size in list.]
640
641  Description [Returns first tree that has the given size in tree list, if
642  the given size exists in size list. Otherwise it returns NULL.]
643
644  SideEffects []
645
646  SeeAlso     []
647
648******************************************************************************/
649MlTree  *
650SynthGetHeadTreeOfSize(int size)
651{
652  MlTree        *head;
653  MlSizeList    *list;
654
655  list = MlSizeHead;
656  while (list) {
657    if (size == list->size) {
658      st_lookup(HeadListTable, list->string, (&head));
659      return(head);
660    } else if (size > list->size)
661      return(NULL);
662    list = list->next;
663  }
664  return(NULL);
665}
666
667
668/**Function********************************************************************
669
670  Synopsis [Makes complement node of a tree if it does not exist.]
671
672  Description [Makes complement node of a tree if it does not exist.
673  If successful, it returns the same tree or another tree which already
674  has the complemented node. In the latter case, it is called a conflict
675  and the two trees are merged into the other tree, this is called
676  resolution. If not successful, it returns NULL. If the complement
677  already exists, the tree is just returned.]
678
679  SideEffects []
680
681  SeeAlso     []
682
683******************************************************************************/
684MlTree  *
685SynthCheckAndMakeComplement(bdd_manager *dd,
686                            st_table *table,
687                            MlTree *tree,
688                            int *comp_flag,
689                            int verbosity)
690{
691  bdd_node      *c;
692  MlTree        *c_tree, *new_;
693
694  if (MlTree_IsComplement(tree))
695    return(tree);
696
697  *comp_flag = 0;
698  if (!tree->complement) {
699    c = MakeComplementOfZddCover(dd, tree->node, verbosity);
700    if (!c)
701      return(NULL);
702    bdd_ref(c);
703    c_tree = SynthLookupMlTable(table, dd, (char *)c, 0, verbosity);
704    if (c_tree) {
705      MlTree *m_tree = MlTree_Regular(c_tree);
706      if (MlTree_Regular(tree)->candidate &&
707          MlTree_Regular(c_tree)->candidate) {
708        /*
709        **       tree     m_tree
710        **         |\      /|
711        **         |   \/   |
712        **         | /    \ |
713        **         q        d
714        **/
715
716        if (ResolveConflictMode == 0 || c_tree == m_tree ||
717            tree->nLiterals <= m_tree->nLiterals) {
718          /* throw away m_tree and assign c to tree->complement */
719          UnlinkMlTree(m_tree);
720          bdd_recursive_deref_zdd(dd, m_tree->node);
721          bdd_recursive_deref_zdd(dd, m_tree->complement);
722          st_delete(table, (char **)(&m_tree->node), NIL(char *));
723          st_delete(table, (char **)(&m_tree->complement), NIL(char *));
724          if (m_tree->support)
725            FREE(m_tree->support);
726          FREE(m_tree);
727          tree->complement = c;
728          if (!InsertMlTable(table, c, MlTree_Not(tree))) {
729            tree->complement = NIL(bdd_node);
730            bdd_recursive_deref_zdd(dd, c);
731            return(NULL);
732          }
733        } else if (c_tree != m_tree) {
734          /* takes m_tree's contents and throws away m_tree */
735          UnlinkMlTree(tree);
736          UnlinkMlTree(m_tree);
737          bdd_recursive_deref_zdd(dd, tree->node);
738          st_delete(table, (char **)(&tree->node), NIL(char *));
739          if (tree->support)
740            FREE(tree->support);
741          memcpy(tree, m_tree, sizeof(MlTree));
742          FREE(m_tree);
743          tree->complement = c;
744          if (!InsertMlTable(table, tree->node, tree)) 
745            return(NULL);
746          if (!InsertMlTable(table, tree->complement, MlTree_Not(tree))) 
747            return(NULL);
748        } else { /* It never happens at this time,
749                  * the case(c_tree == m_tree) is already taken care of.
750                  * But, it should be implemented to improve
751                  * in the future.
752                  */
753        }
754        if (VerifyTreeMode) {
755          SynthVerifyTree(dd, tree, 0);
756          SynthVerifyMlTable(dd, table);
757        }
758        return(tree);
759      } else if (MlTree_Regular(tree)->candidate) {
760        /*
761        **       tree     m_tree
762        **         |\      /|\
763        **         |   \/   |   \
764        **         | /    \ |      \
765        **         q        d        r
766        **/
767
768        if (tree->r == m_tree) {
769          if (c_tree == m_tree)
770            *comp_flag = 1;
771          else
772            *comp_flag = 0;
773
774          if (ResolveConflictMode == 0 || c_tree == m_tree ||
775              m_tree->nLiterals <= tree->nLiterals) {
776            /* throw away tree and returns m_tree */
777            bdd_recursive_deref_zdd(dd, c);
778            UnlinkMlTree(tree);
779            bdd_recursive_deref_zdd(dd, tree->node);
780            st_delete(table, (char **)(&m_tree->node), NIL(char *));
781            if (tree->support)
782              FREE(tree->support);
783            FREE(tree);
784          } else if (c_tree != m_tree) {
785            /*
786            **      tree->complement = m_tree->complement
787            **
788            **       tree     m_tree
789            **         |\      /|\
790            **         |   \/   |   \
791            **         | /    \ |      \
792            **         q        d        r
793            **/
794
795            MlTree      *r_tree, *tmp_tree;
796            int         r_comp;
797            int         ref;
798            bdd_node    *zero = bdd_read_zero(dd);
799
800            /* takes tree's contents and throw away tree and m_tree->r */
801
802            bdd_recursive_deref_zdd(dd, c);
803            r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref,
804                                             verbosity);
805            if (!r_tree)
806              return(NULL);
807            if (MlTree_IsComplement(r_tree)) {
808              r_tree = MlTree_Regular(r_tree);
809              m_tree->r_comp = 1;
810            }
811            tmp_tree = r_tree;
812            r_tree = SynthCheckAndMakeComplement(dd, table, r_tree,
813                                                 &r_comp, verbosity);
814            if (!r_tree)
815              return(NULL);
816            else if (r_tree != tmp_tree) {
817              if (r_comp)
818                m_tree->r_comp = 1;
819              ref = 1;
820            }
821            tree->r = r_tree;
822            tree->r_ref = ref;
823            tree->id = m_tree->id;
824            tree->candidate = 0;
825
826            bdd_recursive_deref_zdd(dd, m_tree->node);
827            bdd_recursive_deref_zdd(dd, m_tree->complement);
828            st_delete(table, (char **)(&m_tree->node), NIL(char *));
829            st_delete(table, (char **)(&m_tree->complement), NIL(char *));
830            UnlinkMlTree(m_tree);
831            if (m_tree->support)
832              FREE(m_tree->support);
833            ref = m_tree->r_ref;
834            r_tree = m_tree->r;
835            memcpy(m_tree, tree, sizeof(MlTree));
836            FREE(tree);
837            SynthPutMlTreeInList(dd, m_tree, 0);
838
839            if (ref) {
840              if (r_tree->shared)
841                DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
842            } else
843              DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
844          } else { /* It never happens at this time,
845                    * the case(c_tree == m_tree) is already taken care of.
846                    * But, it should be implemented to improve
847                    * in the future.
848                    */
849          }
850          if (VerifyTreeMode) {
851            SynthVerifyTree(dd, m_tree, 0);
852            SynthVerifyMlTable(dd, table);
853          }
854          return(m_tree);
855        }
856        if (!SynthUseCandidate(table, dd, tree, verbosity)) {
857          bdd_recursive_deref_zdd(dd, c);
858          return(NULL);
859        }
860        SynthSetSharedFlag(dd, tree);
861      } else if (MlTree_Regular(c_tree)->candidate) {
862        if (m_tree->r == tree) {
863          /*
864          **      m_tree     tree
865          **         |\      /|\
866          **         |   \/   |   \
867          **         | /    \ |      \
868          **         q        d        r
869          **/
870
871          if (ResolveConflictMode == 0 || c_tree == m_tree ||
872              tree->nLiterals <= m_tree->nLiterals) {
873            /* throw away m_tree and assign c to tree->complement */
874            UnlinkMlTree(m_tree);
875            bdd_recursive_deref_zdd(dd, m_tree->node);
876            bdd_recursive_deref_zdd(dd, m_tree->complement);
877            st_delete(table, (char **)(&m_tree->node), NIL(char *));
878            st_delete(table, (char **)(&m_tree->complement), NIL(char *));
879            if (m_tree->support)
880              FREE(m_tree->support);
881            FREE(m_tree);
882            tree->complement = c;
883            if (!InsertMlTable(table, c, MlTree_Not(tree))) {
884              tree->complement = NIL(bdd_node);
885              bdd_recursive_deref_zdd(dd, c);
886              return(NULL);
887            }
888          } else if (c_tree != m_tree) {
889            /*
890            **      tree->complement = m_tree->complement
891            **
892            **      m_tree     tree
893            **         |\      /|\
894            **         |   \/   |   \
895            **         | /    \ |      \
896            **         q        d        r
897            **/
898
899            MlTree      *r_tree, *tmp_tree;
900            int         r_comp;
901            int         ref;
902            bdd_node    *zero = bdd_read_zero(dd);
903
904            /* takes m_tree's contents and throw away m_tree and tree->r */
905
906            bdd_recursive_deref_zdd(dd, c);
907            r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref,
908                                             verbosity);
909            if (!r_tree)
910              return(NULL);
911            if (MlTree_IsComplement(r_tree)) {
912              r_tree = MlTree_Regular(r_tree);
913              m_tree->r_comp = 1;
914            }
915            tmp_tree = r_tree;
916            r_tree = SynthCheckAndMakeComplement(dd, table, r_tree,
917                                                 &r_comp, verbosity);
918            if (!r_tree)
919              return(NULL);
920            else if (r_tree != tmp_tree) {
921              if (r_comp)
922                m_tree->r_comp = 1;
923              ref = 1;
924            }
925            m_tree->r = r_tree;
926            m_tree->r_ref = ref;
927            m_tree->id = tree->id;
928            m_tree->candidate = 0;
929
930            bdd_recursive_deref_zdd(dd, tree->node);
931            st_delete(table, (char **)(&tree->node), NIL(char *));
932            UnlinkMlTree(tree);
933            if (tree->support)
934              FREE(tree->support);
935            ref = tree->r_ref;
936            r_tree = tree->r;
937            memcpy(tree, m_tree, sizeof(MlTree));
938            FREE(m_tree);
939            SynthPutMlTreeInList(dd, tree, 0);
940
941            if (ref) {
942              if (r_tree->shared)
943                DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
944            } else
945              DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
946          } else { /* It never happens at this time,
947                    * the case(c_tree == m_tree) is already taken care of.
948                    * But, it should be implemented to improve
949                    * in the future.
950                    */
951            /*
952            **      tree->complement = m_tree->node
953            **
954            **      m_tree     tree
955            **         |\      /|\
956            **         |   \/   |   \
957            **         | /    \ |      \
958            **         q        d        r
959            **/
960          }
961          return(tree);
962        }
963        if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
964          bdd_recursive_deref_zdd(dd, c);
965          return(NULL);
966        }
967        SynthSetSharedFlag(dd, m_tree);
968      }
969
970      bdd_recursive_deref_zdd(dd, c);
971      if (c_tree == m_tree)
972        *comp_flag = 1;
973      else
974        *comp_flag = 0;
975
976      if (verbosity)
977        (void) fprintf(vis_stdout, "** synth warning: Duplicate entry ...\n");
978      new_ = ResolveConflictNode(dd, table, c_tree, tree, *comp_flag, verbosity);
979      if (verbosity)
980        (void) fprintf(vis_stdout, "** synth info: Conflict was resolved.\n");
981      if (VerifyTreeMode) {
982        SynthVerifyTree(dd, new_, 0);
983        SynthVerifyMlTable(dd, table);
984      }
985      return(new_);
986    } else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) {
987      bdd_recursive_deref_zdd(dd, c);
988      return(NULL);
989    }
990    tree->complement = c;
991    if (!InsertMlTable(table, c, MlTree_Not(tree))) {
992      tree->complement = NIL(bdd_node);
993      bdd_recursive_deref_zdd(dd, c);
994      return NULL;
995    }
996  }
997  return(tree);
998}
999
1000
1001/**Function********************************************************************
1002
1003  Synopsis [Sets the shared field of tree to 1.]
1004
1005  Description [Sets the shared field of tree to 1.]
1006
1007  SideEffects []
1008
1009  SeeAlso     []
1010
1011******************************************************************************/
1012void
1013SynthSetSharedFlag(bdd_manager *dd,
1014                   MlTree *tree)
1015{
1016  MlTree        *t;
1017  bdd_node      *one = bdd_read_one(dd);
1018  bdd_node      *zero = bdd_read_zero(dd);
1019
1020  t = MlTree_Regular(tree);
1021  if (t->node == zero || t->node == one)
1022    return;
1023  if (t->pi == 0)
1024    t->shared = 1;
1025}
1026
1027
1028/**Function********************************************************************
1029
1030  Synopsis [Factorizes leaf nodes of MlTree.]
1031
1032  Description [Factorizes leaf nodes of MlTree. A leaf node of MlTree
1033  can not be factorized by itself. This function tries to factorize
1034  among all leaf nodes. A leaf node can be divided by another leaf
1035  node. If successful, it returns 0, otherwise it returns 1 due to lack
1036  of memory.]
1037
1038  SideEffects []
1039
1040  SeeAlso     []
1041
1042******************************************************************************/
1043int
1044SynthPostFactoring(bdd_manager *dd,
1045                   st_table *table,
1046                   MlTree *(* factoring_func)(bdd_manager *, st_table *,
1047                                              bdd_node *, int, int *, MlTree *,
1048                                              int, MlTree *, int),
1049                   int verbosity)
1050{
1051  MlTree        *cur, *candy;
1052  int           ref;
1053  bdd_node      *q;
1054  bdd_node      *zero = bdd_read_zero(dd);
1055
1056  if (VerifyTreeMode) {
1057    SynthVerifyMlTable(dd, table);
1058    VerifyTreeList();
1059  }
1060
1061  cur = MlTreeHead;
1062  while (cur) {
1063    if (cur->leaf) {
1064      if (cur->nLiterals < 2)
1065        break;
1066      candy = cur->next;
1067      while (candy) {
1068        if (candy->nLiterals == 1)
1069          break;
1070        else if (candy->leaf == 0 ||
1071                 candy->nLiterals == cur->nLiterals) {
1072          candy = candy->next;
1073          continue;
1074        }
1075
1076        q = (* ZddDivideFunc)(dd, cur->node, candy->node);
1077        if (!q)
1078          return(1);
1079        bdd_ref(q);
1080        /* Even though we deref q, it still exists as a
1081         * pointer and beyond this point, we use it only to
1082         * check if it is zero or not.
1083         */
1084        bdd_recursive_deref_zdd(dd,q);
1085        if (q != zero) {
1086          (void) (* factoring_func)(dd, table, cur->node,
1087                                    0, &ref, candy, 0, cur, verbosity);
1088          if (VerifyTreeMode) {
1089            SynthVerifyTree(dd, cur, 0);
1090            SynthVerifyMlTable(dd, table);
1091            VerifyTreeList();
1092          }
1093          if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
1094            return(1);
1095
1096          SynthSetSharedFlag(dd, candy);
1097          break;
1098        } else {
1099          q = (* ZddDivideFunc)(dd, cur->node, 
1100                                candy->complement);
1101          if (!q)
1102            return(1);
1103          bdd_ref(q);
1104          /* Even though we deref q, it still exists as a
1105           * pointer and beyond this point, we use it only
1106           * to check if it is zero or not.
1107           */
1108          bdd_recursive_deref_zdd(dd,q);
1109          if (q != zero) {
1110            (void) (* factoring_func)(dd, table, cur->node, 0,
1111                                      &ref, candy, 1, cur, verbosity);
1112            if (VerifyTreeMode) {
1113              SynthVerifyTree(dd, cur, 0);
1114              SynthVerifyMlTable(dd, table);
1115              VerifyTreeList();
1116            }
1117            if (bdd_read_reordered_field(dd) || noMemoryFlag == 1 )
1118              return(1);
1119            SynthSetSharedFlag(dd, candy);
1120            break;
1121          }
1122        }
1123        candy = candy->next;
1124      }
1125    }
1126    cur = cur->next;
1127  }
1128  return(0);
1129}
1130
1131
1132/**Function********************************************************************
1133
1134  Synopsis    [Updates the ref field of all parent nodes whose one child
1135  is top.]
1136
1137  Description [Updates the ref field of all parent nodes whose one child
1138  is top.]
1139
1140  SideEffects []
1141
1142  SeeAlso     []
1143
1144******************************************************************************/
1145void
1146SynthUpdateRefOfParent(MlTree *top)
1147{
1148  MlTree        *cur;
1149
1150  cur = MlTreeHead;
1151  while (cur) {
1152    if (cur->q == top)
1153      cur->q_ref = 1;
1154    else if (cur->d == top)
1155      cur->d_ref = 1;
1156    else if (cur->r == top)
1157      cur->r_ref = 1;
1158    cur = cur->next;
1159  }
1160}
1161
1162
1163/**Function********************************************************************
1164
1165  Synopsis    [Verifies whether in a tree everything is correct.]
1166
1167  Description [Verifies whether in a tree everything is correct.
1168  Used for debugging. The argument flag is used to control verifying
1169  recursively.]
1170
1171  SideEffects []
1172
1173  SeeAlso     []
1174
1175******************************************************************************/
1176void
1177SynthVerifyTree(bdd_manager *dd,
1178                MlTree *tree,
1179                int flag)
1180{
1181  bdd_node      *node, *comp;
1182  bdd_node      *q, *d, *r, *f, *m;
1183  int           bdd_diff;
1184
1185  if (flag && !tree->leaf) {
1186    if (!tree->q_ref)
1187      SynthVerifyTree(dd, tree->q, flag);
1188    if (!tree->d_ref)
1189      SynthVerifyTree(dd, tree->d, flag);
1190    if (!tree->r_ref)
1191      SynthVerifyTree(dd, tree->r, flag);
1192  }
1193
1194  node = bdd_make_bdd_from_zdd_cover(dd, tree->node);
1195  if (!node)
1196    return;
1197  bdd_ref(node);
1198  if (tree->complement) {
1199    comp = bdd_make_bdd_from_zdd_cover(dd, tree->complement);
1200    if (!comp) {
1201      bdd_recursive_deref(dd, node);
1202      return;
1203    }
1204    bdd_ref(comp);
1205   
1206    if (node != bdd_not_bdd_node(comp)) {
1207      (void) fprintf(vis_stdout,
1208        "** synth error: Invalid complement node in tree [%d].\n", tree->id);
1209    }
1210   
1211    bdd_recursive_deref(dd, comp);
1212  }
1213
1214  if (tree->leaf) {
1215    if (tree->q) {
1216      (void) fprintf(vis_stdout,
1217             "** synth error: q exists in leaf tree [%d].\n", tree->id);
1218    }
1219    if (tree->d) {
1220      (void) fprintf(vis_stdout,
1221             "** synth error: d exists in leaf tree [%d].\n", tree->id);
1222    }
1223    if (tree->r) {
1224      (void) fprintf(vis_stdout,
1225             "** synth error: r exists in leaf tree [%d].\n", tree->id);
1226    }
1227    if (tree->q_ref) {
1228      (void) fprintf(vis_stdout,
1229             "** synth error: q_ref = 1 in leaf tree [%d].\n", tree->id);
1230    }
1231    if (tree->d_ref) {
1232      (void) fprintf(vis_stdout,
1233             "** synth error: d_ref = 1 in leaf tree [%d].\n", tree->id);
1234    }
1235    if (tree->r_ref) {
1236      (void) fprintf(vis_stdout,
1237             "** synth error: r_ref = 1 in leaf tree [%d].\n", tree->id);
1238    }
1239    if (tree->q_comp) {
1240      (void) fprintf(vis_stdout,
1241             "** synth error: q_comp = 1 in leaf tree [%d].\n", tree->id);
1242    }
1243    if (tree->d_comp) {
1244      (void) fprintf(vis_stdout,
1245             "** synth error: d_comp = 1 in leaf tree [%d].\n", tree->id);
1246    }
1247    if (tree->r_comp) {
1248      (void) fprintf(vis_stdout,
1249             "** synth error: r_comp = 1 in leaf tree [%d].\n", tree->id);
1250    }
1251    bdd_recursive_deref(dd, node);
1252    return;
1253  }
1254  else {
1255    if (tree->pi) {
1256      (void) fprintf(vis_stdout,
1257             "** synth error: pi = 1 in non-leaf tree [%d].\n", tree->id);
1258    }
1259  }
1260
1261  if (!tree->q) {
1262    (void) fprintf(vis_stdout,
1263                   "** synth error: no q in tree [%d].\n", tree->id);
1264    bdd_recursive_deref(dd, node);
1265    return;
1266  }
1267  if (tree->q_comp)
1268    q = bdd_make_bdd_from_zdd_cover(dd, tree->q->complement);
1269  else
1270    q = bdd_make_bdd_from_zdd_cover(dd, tree->q->node);
1271  if (!q) {
1272    (void) fprintf(vis_stdout,
1273                   "** synth error: no q node in tree [%d].\n", tree->id);
1274    bdd_recursive_deref(dd, node);
1275    return;
1276  }
1277  bdd_ref(q);
1278  if (!tree->d) {
1279    (void) fprintf(vis_stdout,
1280                   "** synth error: no d in tree [%d].\n", tree->id);
1281    bdd_recursive_deref(dd, node);
1282    bdd_recursive_deref(dd, q);
1283    return;
1284  }
1285  if (tree->d_comp)
1286    d = bdd_make_bdd_from_zdd_cover(dd, tree->d->complement);
1287  else
1288    d = bdd_make_bdd_from_zdd_cover(dd, tree->d->node);
1289  if (!d) {
1290    (void) fprintf(vis_stdout,
1291                   "** synth error: no d node in tree [%d].\n", tree->id);
1292    bdd_recursive_deref(dd, node);
1293    bdd_recursive_deref(dd, q);
1294    return;
1295  }
1296  bdd_ref(d);
1297  if (!tree->candidate) {
1298    if (!tree->r) {
1299      (void) fprintf(vis_stdout,
1300                     "** synth error: no r in tree [%d].\n", tree->id);
1301      bdd_recursive_deref(dd, node);
1302      bdd_recursive_deref(dd, q);
1303      bdd_recursive_deref(dd, d);
1304      return;
1305    }
1306    if (tree->r_comp)
1307      r = bdd_make_bdd_from_zdd_cover(dd, tree->r->complement);
1308    else
1309      r = bdd_make_bdd_from_zdd_cover(dd, tree->r->node);
1310    if (!r) {
1311      (void) fprintf(vis_stdout,
1312                     "** synth error: no r node in tree [%d].\n", tree->id);
1313      bdd_recursive_deref(dd, node);
1314      bdd_recursive_deref(dd, q);
1315      bdd_recursive_deref(dd, d);
1316      return;
1317    }
1318    bdd_ref(r);
1319   
1320    m = bdd_bdd_and(dd, q, d);
1321    if (!m) {
1322      bdd_recursive_deref(dd, node);
1323      bdd_recursive_deref(dd, q);
1324      bdd_recursive_deref(dd, d);
1325      bdd_recursive_deref(dd, r);
1326      return;
1327    }
1328    bdd_ref(m);
1329    bdd_recursive_deref(dd, q);
1330    bdd_recursive_deref(dd, d);
1331    f = bdd_bdd_or(dd, m, r);
1332    if (!f) {
1333      bdd_recursive_deref(dd, node);
1334      bdd_recursive_deref(dd, r);
1335      bdd_recursive_deref(dd, m);
1336      return;
1337    }
1338    bdd_ref(f);
1339    bdd_recursive_deref(dd, r);
1340    bdd_recursive_deref(dd, m);
1341  } else {
1342    f = bdd_bdd_and(dd, q, d);
1343    if (!f) {
1344      bdd_recursive_deref(dd, node);
1345      bdd_recursive_deref(dd, q);
1346      bdd_recursive_deref(dd, d);
1347      return;
1348    }
1349    bdd_ref(f);
1350    bdd_recursive_deref(dd, q);
1351    bdd_recursive_deref(dd, d);
1352  }
1353  if (!f) {
1354    bdd_recursive_deref(dd, node);
1355    return;
1356  }
1357
1358  if (f == node)
1359    bdd_diff = 0;
1360  else
1361    bdd_diff = 1;
1362
1363  bdd_recursive_deref(dd, f);
1364  bdd_recursive_deref(dd, node);
1365
1366  if (tree->comp)
1367    node = tree->complement;
1368  else
1369    node = tree->node;
1370  if (tree->q_comp)
1371    q = tree->q->complement;
1372  else
1373    q = tree->q->node;
1374  if (tree->d_comp)
1375    d = tree->d->complement;
1376  else
1377    d = tree->d->node;
1378  if (!tree->candidate) {
1379    if (tree->r_comp)
1380      r = tree->r->complement;
1381    else
1382      r = tree->r->node;
1383    m = (* SynthGetZddProductFunc())(dd, d, q);
1384    if (!m)
1385      return;
1386    bdd_ref(m);
1387    f = bdd_zdd_union(dd, m, r);
1388    if (!f) {
1389      bdd_recursive_deref_zdd(dd, m);
1390      return;
1391    }
1392    bdd_ref(f);
1393    bdd_recursive_deref_zdd(dd, m);
1394  } else {
1395    f = (* SynthGetZddProductFunc())(dd, d, q);
1396    if (!f)
1397      return;
1398    bdd_ref(f);
1399  }
1400  if (f != node) {
1401    if (bdd_diff) {
1402      (void) fprintf(vis_stdout,
1403             "** synth error: BDD & ZDD f != qd+r in tree [%d - 0x%lx].\n",
1404             tree->id, (unsigned long)tree);
1405    }
1406    else {
1407      (void) fprintf(vis_stdout,
1408                     "Warning : ZDD f != qd+r in tree [%d - 0x%lx].\n",
1409                     tree->id, (unsigned long)tree);
1410    }
1411  }
1412  else if (bdd_diff) {
1413    (void) fprintf(vis_stdout,
1414                   "** synth error: BDD f != qd+r in tree [%d - 0x%lx].\n",
1415                   tree->id, (unsigned long)tree);
1416  }
1417  bdd_recursive_deref_zdd(dd, f);
1418}
1419
1420
1421/**Function********************************************************************
1422
1423  Synopsis    [Verifies the node-tree table to see whether everything is
1424  correct.]
1425
1426  Description [Verifies the node-tree table to see whether everything is
1427  correct. Used for debugging]
1428
1429  SideEffects []
1430
1431  SeeAlso     []
1432
1433******************************************************************************/
1434void
1435SynthVerifyMlTable(bdd_manager *dd,
1436                   st_table *table)
1437{
1438  st_generator  *gen;
1439  bdd_node              *node;
1440  MlTree                *tree, *reg;
1441
1442  st_foreach_item(table, gen, (&node), (&tree)) {
1443    reg = MlTree_Regular(tree);
1444    if ((reg == tree && node != reg->node) ||
1445        (reg != tree && node != reg->complement)) {
1446      (void) fprintf(vis_stdout,
1447                     "** synth error: wrong node in tree [%d].\n", reg->id);
1448    }
1449    tree = reg;
1450    if (tree->id >= NumTree) {
1451      (void) fprintf(vis_stdout,
1452                     "** synth error: wrong id in tree [%d].\n", tree->id);
1453    }
1454    if (!tree->leaf) {
1455      if (!tree->d) {
1456        (void) fprintf(vis_stdout,
1457               "** synth error: d doesn't exist in tree [%d].\n", tree->id);
1458      }
1459      if (!tree->q) {
1460        (void) fprintf(vis_stdout,
1461               "** synth error: q doesn't exist in tree [%d].\n", tree->id);
1462      }
1463      if (!tree->r && !tree->candidate) {
1464        (void) fprintf(vis_stdout,
1465               "** synth error: r doesn't exist in tree [%d].\n", tree->id);
1466      }
1467    }
1468  }
1469}
1470
1471
1472/**Function********************************************************************
1473
1474  Synopsis [Prints all tree lists.]
1475
1476  Description [Prints all tree lists. Used for debugging.]
1477
1478  SideEffects []
1479
1480  SeeAlso     []
1481
1482******************************************************************************/
1483void
1484SynthPrintTreeList(MlTree *list)
1485{
1486  MlTree *cur = list;
1487  if (!cur)
1488    cur = MlTreeHead;
1489  while (cur) {
1490    printf("%d (%d) - %d [0x%lx]\n", cur->id, cur->nLiterals,
1491           cur->leaf, (unsigned long)cur);
1492    cur = cur->next;
1493  }
1494}
1495
1496
1497/**Function********************************************************************
1498
1499  Synopsis [Prints all leaf tree lists.]
1500
1501  Description [Prints all leaf tree lists. Used for debugging.]
1502
1503  SideEffects []
1504
1505  SeeAlso     []
1506
1507******************************************************************************/
1508void
1509SynthPrintLeafList(MlTree *list)
1510{
1511  MlTree *cur = list;
1512  if (!cur)
1513    cur = MlTreeHead;
1514  while (cur) {
1515    if (cur->leaf)
1516      printf("%d (%d) [0x%lx]\n", cur->id, cur->nLiterals, (unsigned long)cur);
1517    cur = cur->next;
1518  }
1519}
1520
1521
1522/*---------------------------------------------------------------------------*/
1523/* Definition of static functions                                            */
1524/*---------------------------------------------------------------------------*/
1525
1526
1527/**Function********************************************************************
1528
1529  Synopsis [Resolves the conflict nodes that can be merged.]
1530
1531  Description [Resolves the conflict nodes that can be merged. One tree
1532  has a regular node, the other tree has the complement of the node.
1533  This case is called conflict. And these two trees are merged into one,
1534  and this is called resolution. It happens because by default the
1535  complement of remainder is not computed since it is very expensive.]
1536
1537  SideEffects []
1538
1539  SeeAlso     []
1540
1541******************************************************************************/
1542static MlTree *
1543ResolveConflictNode(bdd_manager *dd,
1544                    st_table *table,
1545                    MlTree *tree1,
1546                    MlTree *tree2,
1547                    int comp_flag,
1548                    int verbosity)
1549{
1550  MlTree        *live_tree, *kill_tree;
1551
1552  if (MlTree_IsComplement(tree1))
1553    tree1 = MlTree_Regular(tree1);
1554  if (MlTree_IsComplement(tree2))
1555    tree2 = MlTree_Regular(tree2);
1556
1557  if (verbosity) {
1558    if (tree1->complement || tree2->complement)
1559      (void) fprintf(vis_stdout, "** synth warning: real conflict.\n");
1560  }
1561
1562  if (ResolveConflictMode == 0) {
1563    live_tree = tree1;
1564    kill_tree = tree2;
1565  } else {
1566    if (tree1->nLiterals > tree2->nLiterals) {
1567      live_tree = tree2;
1568      kill_tree = tree1;
1569    } else {
1570      live_tree = tree1;
1571      kill_tree = tree2;
1572    }
1573  }
1574
1575  if (!live_tree->complement) {
1576    if (comp_flag)
1577      live_tree->complement = kill_tree->node;
1578    else
1579      live_tree->complement = kill_tree->complement;
1580    bdd_ref(live_tree->complement);
1581    bdd_recursive_deref_zdd(dd, kill_tree->node);
1582    st_delete(table, (char **)(&kill_tree->node), NIL(char *));
1583    if (kill_tree->complement) {
1584        bdd_recursive_deref_zdd(dd, kill_tree->complement);
1585        st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
1586    }
1587    st_insert(table, (char *)live_tree->complement,
1588              (char *)MlTree_Not(live_tree));
1589  } else {
1590    bdd_recursive_deref_zdd(dd, kill_tree->node);
1591    st_delete(table, (char **)(&kill_tree->node), NIL(char *));
1592    if (kill_tree->complement) {
1593        bdd_recursive_deref_zdd(dd, kill_tree->complement);
1594        st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
1595    }
1596  }
1597
1598  DeleteMlTree(dd, table, kill_tree, live_tree, 0, comp_flag);
1599  SynthSetSharedFlag(dd, live_tree);
1600
1601  if (VerifyTreeMode) {
1602    SynthVerifyTree(dd, live_tree, 0);
1603    SynthVerifyMlTable(dd, table);
1604    VerifyTreeList();
1605  }
1606
1607  return(live_tree);
1608}
1609
1610
1611/**Function********************************************************************
1612
1613  Synopsis [Deletes the tree nodes due to conflict.]
1614
1615  Description [Deletes the tree nodes due to conflict.]
1616
1617  SideEffects []
1618
1619  SeeAlso     []
1620
1621******************************************************************************/
1622static void
1623DeleteMlTree(bdd_manager *dd,
1624             st_table *table,
1625             MlTree *kill_tree,
1626             MlTree *live_tree,
1627             int deref,
1628             int comp_flag)
1629{
1630  MlTree        *cur, *pre, *next;
1631  int           ref;
1632
1633  if (kill_tree->shared && deref) {
1634    ref = 0;
1635    cur = MlTreeHead;
1636    while (cur) {
1637      if (cur == kill_tree) {
1638        cur = cur->next;
1639        continue;
1640      }
1641      if (cur->q == kill_tree)
1642        ref++;
1643      else if (cur->d == kill_tree)
1644        ref++;
1645      else if (cur->r == kill_tree)
1646        ref++;
1647      cur = cur->next;
1648    }
1649
1650    if (ref == 1)
1651      kill_tree->shared = 0;
1652    return;
1653  }
1654
1655  DeleteMlSizeList(kill_tree);
1656
1657  if (kill_tree->id == NumTree - 1)
1658    NumTree--;
1659  if (deref) {
1660    bdd_recursive_deref_zdd(dd, kill_tree->node);
1661    st_delete(table, (char **)(&kill_tree->node), NIL(char *));
1662    if (kill_tree->complement) {
1663        bdd_recursive_deref_zdd(dd, kill_tree->complement);
1664        st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
1665    }
1666  }
1667  pre = NIL(MlTree);
1668  cur = MlTreeHead;
1669  while (cur) {
1670    if (cur == kill_tree) {
1671      next = cur->next;
1672      if (pre)
1673        pre->next = next;
1674      else
1675        MlTreeHead = next;
1676      cur = next;
1677      if (!live_tree)
1678        break;
1679    } else {
1680      if (live_tree) {
1681        if (cur->q == kill_tree) {
1682          if (comp_flag)
1683            cur->q_comp ^= 01;
1684          cur->q = live_tree;
1685          cur->q_ref = 1;
1686          if (VerifyTreeMode)
1687            SynthVerifyTree(dd, cur, 0);
1688        } else if (cur->d == kill_tree) {
1689          if (comp_flag)
1690            cur->d_comp ^= 01;
1691          cur->d = live_tree;
1692          cur->d_ref = 1;
1693          if (VerifyTreeMode)
1694            SynthVerifyTree(dd, cur, 0);
1695        } else if (cur->r == kill_tree) {
1696          if (comp_flag)
1697            cur->r_comp ^= 01;
1698          cur->r = live_tree;
1699          cur->r_ref = 1;
1700          if (VerifyTreeMode)
1701            SynthVerifyTree(dd, cur, 0);
1702        }
1703      }
1704      pre = cur;
1705      cur = cur->next;
1706    }
1707  }
1708
1709  if (kill_tree->leaf == 0) {
1710    if (kill_tree->q_ref) {
1711      if (kill_tree->q->shared)
1712        DeleteMlTree(dd, table, kill_tree->q, NULL, 1, 0);
1713    } else
1714      DeleteMlTree(dd, table, kill_tree->q, NULL, 1, 0);
1715    if (kill_tree->d_ref) {
1716      if (kill_tree->d->shared)
1717        DeleteMlTree(dd, table, kill_tree->d, NULL, 1, 0);
1718    } else
1719      DeleteMlTree(dd, table, kill_tree->d, NULL, 1, 0);
1720    if (kill_tree->r_ref) {
1721      if (kill_tree->r->shared)
1722        DeleteMlTree(dd, table, kill_tree->r, NULL, 1, 0);
1723    } else
1724      DeleteMlTree(dd, table, kill_tree->r, NULL, 1, 0);
1725  }
1726
1727  if (kill_tree->support)
1728    FREE(kill_tree->support);
1729  FREE(kill_tree);
1730}
1731
1732
1733/**Function********************************************************************
1734
1735  Synopsis [Unlinks a tree from the list.]
1736
1737  Description [Unlinks a tree from the list.]
1738
1739  SideEffects []
1740
1741  SeeAlso     []
1742
1743******************************************************************************/
1744static void
1745UnlinkMlTree(MlTree *kill_tree)
1746{
1747  MlTree        *cur, *pre;
1748
1749  DeleteMlSizeList(kill_tree);
1750
1751  pre = (MlTree *)NULL;
1752  cur = MlTreeHead;
1753  while (cur) {
1754    if (cur == kill_tree) {
1755        if (pre)
1756          pre->next = cur->next;
1757        else
1758          MlTreeHead = cur->next;
1759        break;
1760    }
1761    pre = cur;
1762    cur = cur->next;
1763  }
1764}
1765
1766
1767/**Function********************************************************************
1768
1769  Synopsis [Deletes a tree from the size list.]
1770
1771  Description [Deletes a tree from the size list.]
1772
1773  SideEffects []
1774
1775  SeeAlso     []
1776
1777******************************************************************************/
1778static void
1779DeleteMlSizeList(MlTree *tree)
1780{
1781  MlTree        *head, *tail, *cur, *pre;
1782  MlSizeList    *list, *pre_list;
1783  int           size;
1784
1785  size = tree->nLiterals;
1786  pre_list = NIL(MlSizeList);
1787  list = MlSizeHead;
1788  while (list) {
1789    if (size == list->size) {
1790      st_lookup(HeadListTable, list->string, (&head));
1791      st_lookup(TailListTable, list->string, (&tail));
1792      if (head == tail) {
1793        assert(tree == head);
1794        if (pre_list)
1795          pre_list->next = list->next;
1796        else
1797          MlSizeHead = list->next;
1798        st_delete(HeadListTable, (char **)&list->string, NIL(char *));
1799        st_delete(TailListTable, (char **)&list->string, NIL(char *));
1800        FREE(list->string);
1801        FREE(list);
1802      } else {
1803        pre = NIL(MlTree);
1804        cur = head;
1805        while (cur) {
1806          if (cur == tree) {
1807            if (cur == head) {
1808              st_delete(HeadListTable, (char **)&list->string, NIL(char *));
1809              st_insert(HeadListTable, list->string, (char *)cur->next);
1810            } else if (cur == tail) {
1811              st_delete(TailListTable, (char **)&list->string, NIL(char *));
1812              st_insert(TailListTable, list->string, (char *)pre);
1813            }
1814            break;
1815          }
1816          pre = cur;
1817          cur = cur->next;
1818        }
1819      }
1820      break;
1821    } else if (size > list->size)
1822      break;
1823    pre_list = list;
1824    list = list->next;
1825  }
1826}
1827
1828
1829/**Function********************************************************************
1830
1831  Synopsis [Inserts a new node-tree pair into the node-tree table.]
1832
1833  Description [Inserts a new node-tree pair into the node-tree table.]
1834
1835  SideEffects []
1836
1837  SeeAlso     []
1838
1839******************************************************************************/
1840static int
1841InsertMlTable(st_table *table,
1842              bdd_node *node,
1843              MlTree *tree)
1844{
1845  int           flag;
1846
1847  flag = st_insert(table, (char *)node, (char *)tree);
1848  if (flag == ST_OUT_OF_MEM) {
1849    (void) fprintf(vis_stdout,"** synth error: Out of Memory.\n");
1850    noMemoryFlag = 1;
1851    return (0);
1852  } else if (flag == 1)
1853    (void) fprintf(vis_stdout, "** synth warning: Duplicate entry.\n");
1854  return(1);
1855}
1856
1857
1858/**Function********************************************************************
1859
1860  Synopsis [Makes the complement of a ZDD node.]
1861
1862  Description [Makes the complement of a ZDD node.]
1863
1864  SideEffects []
1865
1866  SeeAlso     []
1867
1868******************************************************************************/
1869static bdd_node *
1870MakeComplementOfZddCover(bdd_manager *dd,
1871                         bdd_node *node,
1872                         int verbosity)
1873{
1874  bdd_node      *comp;
1875
1876  if (verbosity > 1) {
1877    (void) fprintf(vis_stdout,"*****\n");
1878    SynthPrintZddTreeMessage(dd, node, "R : ");
1879  }
1880
1881  comp = bdd_zdd_complement(dd, node);
1882  if (!comp)
1883    return(NULL);
1884
1885  if (verbosity > 1) {
1886    SynthPrintZddTreeMessage(dd, comp, "C : ");
1887    (void) fprintf(vis_stdout,"*****\n");
1888  }
1889
1890  return(comp);
1891}
1892
1893
1894/**Function********************************************************************
1895
1896  Synopsis [Returns a string containing a given integer value.]
1897
1898  Description [Returns a string containing a given integer value.]
1899
1900  SideEffects []
1901
1902  SeeAlso     []
1903
1904******************************************************************************/
1905static  char *
1906GetIntString(int v)
1907{
1908  char  string[12];
1909  char  *ret;
1910
1911  sprintf(string, "%d", v);
1912  ret = (char *)ALLOC(char, strlen(string) + 1);
1913  strcpy(ret, string);
1914  return(ret);
1915}
1916
1917
1918/**Function********************************************************************
1919
1920  Synopsis [Verify all tree lists to see whether all is correct.]
1921
1922  Description [Verify all tree lists to see whether all is correct.
1923  Used for debugging.]
1924
1925  SideEffects []
1926
1927  SeeAlso     []
1928
1929******************************************************************************/
1930static void
1931VerifyTreeList(void)
1932{
1933  int           count;
1934  MlTree        *cur, *candy;
1935
1936  cur = MlTreeHead;
1937  while (cur) {
1938    count = 0;
1939    candy = cur->next;
1940    if (candy && candy->nLiterals > cur->nLiterals) {
1941      (void) fprintf(vis_stdout,
1942             "** synth error: predecessor[%d]'s size < successor[%d]'s size.\n",
1943                     cur->id, candy->id);
1944    }
1945    while (candy) {
1946      if (cur->id != 0) {
1947        if (candy->id == cur->id && candy != cur) {
1948          (void) fprintf(vis_stdout,
1949                 "** synth error: same id already exists [%d].\n", cur->id);
1950          break;
1951        }
1952      }
1953      if (candy == cur) {
1954        if (count > 0) {
1955          (void) fprintf(vis_stdout,
1956                 "** synth error: same address already exists [%d - 0x%lx].\n",
1957                         cur->id, (unsigned long)cur);
1958          break;
1959        }
1960        count++;
1961      }
1962      candy = candy->next;
1963    }
1964    cur = cur->next;
1965  }
1966}
Note: See TracBrowser for help on using the repository browser.