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

Last change on this file since 76 was 14, checked in by cecile, 15 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.