source: vis_dev/vis-2.3/src/synth/synthDiv.c @ 23

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

vis2.3

File size: 29.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthDiv.c]
4
5  PackageName [synth]
6
7  Synopsis    [Divisor 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: synthDiv.c,v 1.25 2002/09/10 05:50:52 fabio Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25#define MAX_COUNT       100000000 /* just chosen for a very large number */
26
27/*---------------------------------------------------------------------------*/
28/* Type declarations                                                         */
29/*---------------------------------------------------------------------------*/
30
31
32/*---------------------------------------------------------------------------*/
33/* Structure declarations                                                    */
34/*---------------------------------------------------------------------------*/
35
36/**Struct**********************************************************************
37
38  Synopsis    [Structure of one BFS item to count variable occurrences.]
39
40  Description [Structure of one BFS item to count variable occurrences.]
41
42  SeeAlso     []
43
44******************************************************************************/
45typedef struct  bfs_item {
46  int                   reach; /* number of path from top node */
47  int                   count; /* number of path to constant 1 */
48  bdd_node              *node; /* ZDD node */
49  struct bfs_item       *next;
50} BfsItem;
51
52/**Struct**********************************************************************
53
54  Synopsis    [Structure for BFS operation to count variable occurrences.]
55
56  Description [Structure for BFS operation to count variable occurrences.]
57
58  SeeAlso     []
59
60******************************************************************************/
61typedef struct  bfs_list {
62  struct bfs_item       *item;
63  int                   child; /* 1 : T, 0 : E */
64  struct bfs_list       *next;
65} BfsList;
66
67
68/*---------------------------------------------------------------------------*/
69/* Variable declarations                                                     */
70/*---------------------------------------------------------------------------*/
71
72
73/**AutomaticStart*************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Static function prototypes                                                */
77/*---------------------------------------------------------------------------*/
78
79static int FindQuickDivisor(bdd_node *f, bdd_node *one, int *v);
80
81/**AutomaticEnd***************************************************************/
82
83
84/*---------------------------------------------------------------------------*/
85/* Definition of exported functions                                          */
86/*---------------------------------------------------------------------------*/
87
88
89/**Function********************************************************************
90
91  Synopsis [Finds a divisor that occurs in more than one cube of the ZDD
92  graph.]
93
94  Description [Finds a divisor that occurs in more than one cube of the ZDD
95  graph. This is done in a greedy manner. It returns a ZDD node.]
96
97  SideEffects []
98
99  SeeAlso     [Synth_ZddLeastDivisor Synth_ZddMostDivisor
100  Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
101
102******************************************************************************/
103bdd_node *
104Synth_ZddQuickDivisor(bdd_manager *dd,
105                      bdd_node *f)
106{
107  bdd_node      *res;
108
109  if (bdd_get_package_name() != CUDD) {
110    (void)fprintf(vis_stderr,
111      "** synth error: Synthesis package can be used only with CUDD package\n");
112    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
113    return NIL(bdd_node);
114  }
115
116  do {
117    bdd_set_reordered_field(dd, 0);
118    res = SynthZddQuickDivisor(dd, f);
119  } while (bdd_read_reordered_field(dd) == 1);
120  return(res);
121}
122
123
124/**Function********************************************************************
125
126  Synopsis [Finds a divisor that occurs the least frequently (but more
127  than once) in the cubes of a cover.]
128
129  Description [Finds a divisor that occurs the least frequently (but more
130  than once) in the cubes of a cover. It returns a ZDD node.]
131
132  SideEffects []
133
134  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddMostDivisor
135  Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
136
137******************************************************************************/
138bdd_node *
139Synth_ZddLeastDivisor(bdd_manager *dd,
140                      bdd_node *f)
141{
142  bdd_node      *res;
143
144  if (bdd_get_package_name() != CUDD) {
145    (void)fprintf(vis_stderr,
146      "** synth error: Synthesis package can be used only with CUDD package\n");
147    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
148    return NIL(bdd_node);
149  }
150
151  do {
152    bdd_set_reordered_field(dd, 0);
153    res = SynthZddLeastDivisor(dd, f);
154  } while (bdd_read_reordered_field(dd) == 1);
155  return(res);
156}
157
158
159/**Function********************************************************************
160
161  Synopsis [Finds a divisor that occurs the most frequently in the cubes
162  of a cover.]
163
164  Description [Finds a divisor that occurs the most frequently in the cubes
165  of a cover. It returns a ZDD node.]
166
167  SideEffects []
168
169  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddLeastDivisor
170  Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
171
172******************************************************************************/
173bdd_node *
174Synth_ZddMostDivisor(bdd_manager *dd,
175                     bdd_node *f)
176{
177  bdd_node      *res;
178
179  if (bdd_get_package_name() != CUDD) {
180    (void)fprintf(vis_stderr,
181      "** synth error: Synthesis package can be used only with CUDD package\n");
182    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
183    return NIL(bdd_node);
184  }
185
186  do {
187    bdd_set_reordered_field(dd, 0);
188    res = SynthZddMostDivisor(dd, f);
189  } while (bdd_read_reordered_field(dd) == 1);
190  return(res);
191}
192
193
194/**Function********************************************************************
195
196  Synopsis    [Finds a divisor that is a level-0 cokernel.]
197
198  Description [Finds a divisor that is a level-0 cokernel. It returns a
199  ZDD node.]
200
201  SideEffects []
202
203  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddLeastDivisor
204  Synth_ZddMostDivisor Synth_ZddCommonDivisor Synth_ZddLpDivisor]
205
206******************************************************************************/
207bdd_node *
208Synth_ZddLevelZeroDivisor(bdd_manager *dd,
209                          bdd_node *f)
210{
211  bdd_node      *res;
212
213  if (bdd_get_package_name() != CUDD) {
214    (void)fprintf(vis_stderr,
215      "** synth error: Synthesis package can be used only with CUDD package\n");
216    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
217    return NIL(bdd_node);
218  }
219
220  do {
221    bdd_set_reordered_field(dd, 0);
222    res = SynthZddLevelZeroDivisor(dd, f);
223  } while (bdd_read_reordered_field(dd) == 1);
224  return(res);
225}
226
227
228/**Function********************************************************************
229
230  Synopsis    [Find a divisor whose literals occur in all cubes.]
231
232  Description [Find a divisor whose literals occur in all cubes. It
233  returns a ZDD node.]
234
235  SideEffects []
236
237  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddMostDivisor
238  Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddLpDivisor]
239
240******************************************************************************/
241bdd_node *
242Synth_ZddCommonDivisor(bdd_manager *dd,
243                       bdd_node *f)
244{
245  bdd_node      *res;
246
247  if (bdd_get_package_name() != CUDD) {
248    (void)fprintf(vis_stderr,
249      "** synth error: Synthesis package can be used only with CUDD package\n");
250    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
251    return NIL(bdd_node);
252  }
253
254  do {
255    bdd_set_reordered_field(dd, 0);
256    res = SynthZddCommonDivisor(dd, f);
257  } while (bdd_read_reordered_field(dd) == 1);
258  return(res);
259}
260
261
262/**Function********************************************************************
263
264  Synopsis    [Find a good divisor for low power.]
265
266  Description [Find a good divisor for low power. It returns a ZDD
267  node.]
268
269  SideEffects []
270
271  SeeAlso     [Synth_ZddQuickDivisor Synth_ZddMostDivisor
272  Synth_ZddLeastDivisor Synth_ZddLevelZeroDivisor Synth_ZddCommonDivisor]
273******************************************************************************/
274bdd_node *
275Synth_ZddLpDivisor(bdd_manager *dd,
276                   bdd_node *f)
277{
278  bdd_node      *res;
279
280  if (bdd_get_package_name() != CUDD) {
281    (void)fprintf(vis_stderr,
282      "** synth error: Synthesis package can be used only with CUDD package\n");
283    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
284    return NIL(bdd_node);
285  }
286
287  do {
288    bdd_set_reordered_field(dd, 0);
289    res = SynthZddLpDivisor(dd, f);
290  } while (bdd_read_reordered_field(dd) == 1);
291  return(res);
292}
293
294
295/*---------------------------------------------------------------------------*/
296/* Definition of internal functions                                          */
297/*---------------------------------------------------------------------------*/
298
299
300/**Function********************************************************************
301
302  Synopsis    [Performs the recursive steps of Synth_ZddQuickDivisor.]
303
304  Description [Performs the recursive steps of Synth_ZddQuickDivisor.
305  When FindQuickDivisor fails to find a literal, the function uses as
306  backup strategy finding the literal that occurs the least. The reason
307  is the following. If a node has more than one parent, then it is
308  guaranteed to appear in more than one cube. However, the converse is not
309  true.]
310
311  SideEffects []
312
313  SeeAlso     [SynthZddLeastDivisor SynthZddMostDivisor
314  SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]
315
316******************************************************************************/
317bdd_node *
318SynthZddQuickDivisor(bdd_manager *dd,
319                     bdd_node *f)
320{
321  int           i, v;
322  int           nvars;
323  int           *count;
324  bdd_node      *one = bdd_read_one(dd);
325  bdd_node      *zero = bdd_read_zero(dd);
326  bdd_node      *divisor, *node;
327  bdd_node      *tmp;
328  int           min_count;
329
330  if (f == one || f == zero)
331    return(f);
332
333  /* Search for a literal appearing in at least two cubes. */
334  v = -1;
335  FindQuickDivisor(f, one, &v);
336  SynthZddClearFlag(f);
337
338  if (v == -1) {
339    /* Quick divisor not found by looking at the ZDD graph.
340     * Find the literal that occurs the least among those occuring
341     * at least twice.
342     */
343    min_count = MAX_COUNT;
344    nvars = bdd_num_zdd_vars(dd);
345    count = ALLOC(int, nvars);
346    (void)memset((void *)count, 0, sizeof(int) * nvars);
347    SynthCountLiteralOccurrence(dd, f, count);
348    for (i = 0; i < nvars; i++) {
349      if (count[i] > 1 && count[i] < min_count) {
350        v = i;
351        min_count = count[i];
352      }
353    }
354    FREE(count);
355    if (v == -1) {
356      /* All literal appear exactly once. We are done. */
357      return(f);
358    }
359  }
360
361  /* Obtain the literal divisor from its index and divide f. */
362  node = bdd_zdd_get_node(dd, v, one, zero);
363  if (!node)
364    return(NULL);
365  bdd_ref(node);
366
367  tmp = (* SynthGetZddDivideRecurFunc())(dd, f, node);
368  if (!tmp) {
369    bdd_recursive_deref_zdd(dd,node);
370    return(NULL);
371  }
372  bdd_ref(tmp);
373  bdd_recursive_deref_zdd(dd, node);
374
375  /* Recur on the quotient to make sure that all literals appear once. */
376  divisor = SynthZddQuickDivisor(dd, tmp);
377  if (!divisor) {
378    bdd_recursive_deref_zdd(dd,tmp);
379    return(NULL);
380  }
381  bdd_ref(divisor);
382  bdd_recursive_deref_zdd(dd, tmp);
383
384  bdd_deref(divisor);
385  return(divisor);
386}
387
388
389/**Function********************************************************************
390
391  Synopsis    [Performs the recursive steps of Synth_ZddLeastDivisor.]
392
393  Description [Performs the recursive steps of Synth_ZddLeastDivisor.]
394
395  SideEffects []
396
397  SeeAlso     [SynthZddQuickDivisor SynthZddMostDivisor
398  SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]
399
400******************************************************************************/
401bdd_node *
402SynthZddLeastDivisor(bdd_manager *dd,
403                     bdd_node *f)
404{
405  int           i, v;
406  int           nvars, min_count;
407  int           *count;
408  bdd_node      *one = bdd_read_one(dd);
409  bdd_node      *zero = bdd_read_zero(dd);
410  bdd_node      *divisor, *node;
411  bdd_node      *tmp1;
412
413  if (f == one || f == zero)
414    return(f);
415
416  /* Find the literal that occurs the least among those occuring at
417   * least twice.
418   */
419  v = -1;
420  min_count = MAX_COUNT;
421  nvars = bdd_num_zdd_vars(dd);
422  count = ALLOC(int, nvars);
423  (void)memset((void *)count, 0, sizeof(int) * nvars);
424  SynthCountLiteralOccurrence(dd, f, count);
425  for (i = 0; i < nvars; i++) {
426    if (count[i] > 1 && count[i] < min_count) {
427      v = i;
428      min_count = count[i];
429    }
430  }
431  FREE(count);
432
433  if (v == -1) {
434    /* All literal appear exactly once. We are done. */
435    return(f);
436  }
437
438  /* Obtain the literal divisor from its index and divide f. */
439  node = bdd_zdd_get_node(dd, v, one, zero);
440  if (!node) {
441    return(NULL);
442  }
443  bdd_ref(node);
444
445  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
446  if (!tmp1) {
447    bdd_recursive_deref_zdd(dd, node);
448    return(NULL);
449  }
450  bdd_ref(tmp1);
451  bdd_recursive_deref_zdd(dd, node);
452
453  /* Recur on the quotient to make sure that all literals appear once. */
454  divisor = SynthZddLeastDivisor(dd, tmp1);
455  if (!divisor) {
456    bdd_recursive_deref_zdd(dd, tmp1);
457    return(NULL);
458  }
459  bdd_ref(divisor);
460  bdd_recursive_deref_zdd(dd, tmp1);
461
462  bdd_deref(divisor);
463  return(divisor);
464}
465
466
467/**Function********************************************************************
468
469  Synopsis    [Performs the recursive steps of Synth_ZddMostDivisor.]
470
471  Description [Performs the recursive steps of Synth_ZddMostDivisor.]
472
473  SideEffects []
474
475  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
476  SynthZddLevelZeroDivisor SynthZddCommonDivisor SynthZddLpDivisor]
477
478******************************************************************************/
479bdd_node *
480SynthZddMostDivisor(bdd_manager *dd,
481                    bdd_node *f)
482{
483  int           i, v;
484  int           nvars, max_count;
485  int           *count;
486  bdd_node      *one = bdd_read_one(dd);
487  bdd_node      *zero = bdd_read_zero(dd);
488  bdd_node      *divisor, *node;
489  bdd_node      *tmp1;
490
491  if (f == one || f == zero)
492    return(f);
493
494  /* Find the literal that occurs the most. */
495  v = -1;
496  max_count = 1;
497  nvars = bdd_num_zdd_vars(dd);
498  count = ALLOC(int, nvars);
499  (void)memset((void *)count, 0, sizeof(int) * nvars);
500  SynthCountLiteralOccurrence(dd, f, count);
501  for (i = 0; i < nvars; i++) {
502    if (count[i] > max_count) {
503      v = i;
504      max_count = count[i];
505    }
506  }
507
508  FREE(count);
509
510  if (v == -1) {
511    /* All literal appear exactly once. We are done. */
512    return(f);
513  }
514
515  /* Obtain the literal divisor from its index and divide f. */
516  node = bdd_zdd_get_node(dd, v, one, zero);
517  if (!node)
518    return(NULL);
519  bdd_ref(node);
520
521  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
522  if (!tmp1) {
523    bdd_recursive_deref_zdd(dd, node);
524    return(NULL);
525  }
526  bdd_ref(tmp1);
527  bdd_recursive_deref_zdd(dd, node);
528
529  /* Recur on the quotient to make sure that all literals appear once. */
530  divisor = SynthZddMostDivisor(dd, tmp1);
531  if (!divisor) {
532    bdd_recursive_deref_zdd(dd, tmp1);
533    return(NULL);
534  }
535  bdd_ref(divisor);
536  bdd_recursive_deref_zdd(dd, tmp1);
537
538  bdd_deref(divisor);
539  return(divisor);
540}
541
542
543/**Function********************************************************************
544
545  Synopsis    [Performs the recursive steps of Synth_ZddLevelZeroDivisor.]
546
547  Description [Performs the recursive steps of Synth_ZddLevelZeroDivisor.]
548
549  SideEffects []
550
551  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
552  SynthZddMostDivisor SynthZddCommonDivisor SynthZddLpDivisor]
553
554******************************************************************************/
555bdd_node *
556SynthZddLevelZeroDivisor(bdd_manager *dd,
557                         bdd_node *f)
558{
559  int           i, v;
560  int           nvars, max_count;
561  int           *count;
562  bdd_node      *one = bdd_read_one(dd);
563  bdd_node      *zero = bdd_read_zero(dd);
564  bdd_node      *divisor, *node;
565  bdd_node      *tmp1, *tmp2;
566
567  if (f == one || f == zero)
568    return(f);
569
570  /* Find the literal that occurs the most. */
571  v = -1;
572  max_count = 1;
573  nvars = bdd_num_zdd_vars(dd);
574  count = ALLOC(int, nvars);
575  (void)memset((void *)count, 0, sizeof(int) * nvars);
576  SynthCountLiteralOccurrence(dd, f, count);
577  for (i = 0; i < nvars; i++) {
578    if (count[i] > max_count) {
579      v = i;
580      max_count = count[i];
581    }
582  }
583
584  FREE(count);
585
586  if (v == -1) {
587    /* All literal appear exactly once. We are done. */
588    return(f);
589  }
590
591  /* Obtain the literal divisor from its index and divide f. */
592  node = bdd_zdd_get_node(dd, v, one, zero);
593  if (!node)
594    return(NULL);
595  bdd_ref(node);
596
597  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
598  if (!tmp1) {
599    bdd_recursive_deref_zdd(dd, node);
600    return(NULL);
601  }
602  bdd_ref(tmp1);
603  bdd_recursive_deref_zdd(dd, node);
604
605  /* Factor out all literals appearing in all cubes. */
606  tmp2 = SynthMakeCubeFree(dd, tmp1);
607  if (!tmp2) {
608    bdd_recursive_deref_zdd(dd, tmp1);
609    return(NULL);
610  }
611  bdd_ref(tmp2);
612  bdd_recursive_deref_zdd(dd, tmp1);
613
614  /* Recur on the quotient to make sure that all literals appear once. */
615  divisor = SynthZddLevelZeroDivisor(dd, tmp2);
616  if (!divisor) {
617    bdd_recursive_deref_zdd(dd, tmp2);
618    return(NULL);
619  }
620  bdd_ref(divisor);
621  bdd_recursive_deref_zdd(dd, tmp2);
622
623  bdd_deref(divisor);
624  return(divisor);
625}
626
627/**Function********************************************************************
628
629  Synopsis    [The internal function of Synth_ZddCommonDivisor.]
630
631  Description [The internal function of Synth_ZddCommonDivisor.]
632
633  SideEffects []
634
635  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
636  SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddLpDivisor]
637
638******************************************************************************/
639bdd_node *
640SynthZddCommonDivisor(bdd_manager *dd,
641                      bdd_node *f)
642{
643  int           i;
644  int           nvars;
645  int           *count;
646  bdd_node      *one = bdd_read_one(dd);
647  bdd_node      *zero = bdd_read_zero(dd);
648  bdd_node      *divisor, *node, *tmp;
649  int           nCubes;
650
651  divisor = (bdd_node *)NULL;   /* NULL means no such divisor exists */
652  if (f == one || f == zero)
653    return(divisor);
654
655  nCubes = bdd_zdd_count(dd, f);
656  if (nCubes == 1)
657    return(divisor);
658
659  /* Find the literals that appear exactly as many times as there
660   * are cubes. These literals appear in all cubes, hence in the
661   * common divisor. Their product is accumulated in divisor. */
662  nvars = bdd_num_zdd_vars(dd);
663  count = ALLOC(int, nvars);
664  (void)memset((void *)count, 0, sizeof(int) * nvars);
665  SynthCountLiteralOccurrence(dd, f, count);
666  for (i = 0; i < nvars; i++) {
667    if (count[i] == nCubes) {
668      node = bdd_zdd_get_node(dd, i, one, zero);
669      if (!node) {
670        FREE(count);
671        return(NULL);
672      }
673      bdd_ref(node);
674      if (!divisor) {
675        divisor = node;
676        continue;
677      }
678      tmp = divisor;
679      divisor = (* SynthGetZddProductRecurFunc())(dd, divisor, node);
680      if (!divisor) {
681        bdd_recursive_deref_zdd(dd, tmp);
682        bdd_recursive_deref_zdd(dd, node);
683        FREE(count);
684        return(NULL);
685      }
686      bdd_ref(divisor);
687      bdd_recursive_deref_zdd(dd, tmp);
688      bdd_recursive_deref_zdd(dd, node);
689    }
690  }
691  FREE(count);
692
693  if (divisor)
694    bdd_deref(divisor);
695  return(divisor);
696}
697
698
699/**Function********************************************************************
700
701  Synopsis    [Performs the recursive steps of Synth_ZddLpDivisor.]
702
703  Description [Performs the recursive steps of Synth_ZddLpDivisor.]
704
705  SideEffects []
706
707  SeeAlso     [SynthZddQuickDivisor SynthZddLeastDivisor
708  SynthZddMostDivisor SynthZddLevelZeroDivisor SynthZddCommonDivisor]
709
710******************************************************************************/
711bdd_node *
712SynthZddLpDivisor(bdd_manager *dd,
713                  bdd_node *f)
714{
715  int           i, v;
716  int           nvars, min_count, min_pos = 0;
717  int           *count;
718  bdd_node      *one = bdd_read_one(dd);
719  bdd_node      *zero = bdd_read_zero(dd);
720  bdd_node      *divisor, *node;
721  bdd_node      *tmp1;
722
723  if (f == one || f == zero)
724    return(f);
725
726  /* Find the literal that occurs the least among those occuring at
727   * least twice.
728   */
729  v = -1;
730  min_count = MAX_COUNT;
731  nvars = bdd_num_zdd_vars(dd);
732  count = ALLOC(int, nvars);
733  (void)memset((void *)count, 0, sizeof(int) * nvars);
734
735  SynthCountLiteralOccurrence(dd, f, count);
736  for (i = 0; i < nvars; i++) {
737    if (count[i] > 1 && count[i] < min_count) {
738      v = i;
739      min_count = count[i];
740      min_pos = i;
741    }
742  }
743  if (v == -1) {
744    /* All literal appear exactly once. We are done. */
745    FREE(count);
746    return(f);
747  }
748
749  /* Among the literals with minimum count, find a good one. */
750  v = SynthFindDivisorForLowPower(count, nvars, min_count, min_pos);
751
752  FREE(count);
753
754  if (v == -1) {
755    return(f);
756  }
757
758  /* Obtain the literal divisor from its index and divide f. */
759  node = bdd_zdd_get_node(dd, v, one, zero);
760  if (!node)
761    return(NULL);
762  bdd_ref(node);
763
764  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
765  if (!tmp1) {
766    bdd_recursive_deref_zdd(dd, node);
767    return(NULL);
768  }
769  bdd_ref(tmp1);
770  bdd_recursive_deref_zdd(dd, node);
771
772  /* Recur on the quotient to make sure that all literals appear once. */
773  divisor = SynthZddLpDivisor(dd, tmp1);
774  if (!divisor) {
775    bdd_recursive_deref_zdd(dd, tmp1);
776    return(NULL);
777  }
778  bdd_ref(divisor);
779  bdd_recursive_deref_zdd(dd, tmp1);
780
781  bdd_deref(divisor);
782  return(divisor);
783}
784
785
786/**Function********************************************************************
787
788  Synopsis    [Counts the number of occurrences of each variable.]
789
790  Description [Counts the number of occurrences of each variable.
791  First, we count the number of paths to the top node for each node from
792  top to bottom. Let this number be C_t. Initially, C_t of the top node
793  is 1, and C_t of a node is the sum of C_t's of all predecessors of the
794  node. Second, we count the number of paths to the constant one node from
795  bottom to top. Let this number be C_1. Initially, C_1 of the constant one
796  node is 1 and C_1 of the constant zero node is 0, and C_1 of a node is the
797  sum of C_1's of two successors of the node. Third, we count the number of
798  occurrences of variables using the C_t's and C_1's of each node. Here, let
799  C_m of a node be C_t of the node times C_1 of then child of the node.
800  The number of occurrences of a variable is determined by summing C_m of all
801  nodes that belongs to the variable in the ZDD. The argument count is
802  passed by caller, and it is an array of integer to store the number of
803  occurrence for each variable, and the size of the array is the number
804  of ZDD variables.]
805
806  SideEffects []
807
808  SeeAlso     []
809
810******************************************************************************/
811void
812SynthCountLiteralOccurrence(bdd_manager *dd,
813                            bdd_node *f,
814                            int *count)
815{
816  BfsItem       **level, *item, *cur_item, *next_item, *last_item;
817  BfsList       *list, *pre_list, *cur_list, *next_list, *last_list;
818  BfsList       *new_list, *save_last_list;
819  int           cur_level, next_level, start_level, last_level;
820  int           exist;
821  bdd_node      *zero = bdd_read_zero(dd);
822  bdd_node      *one = bdd_read_one(dd);
823  int           i, ct, ce;
824  bdd_node      *node;
825  int           lv, *index, id;
826  int           sizeZ = bdd_num_zdd_vars(dd);
827
828  if (bdd_is_constant(f))
829    return;
830
831  level = ALLOC(BfsItem *, sizeZ);
832  (void)memset((void *)level, 0, sizeof(BfsItem *) * sizeZ);
833  index = ALLOC(int, sizeZ);
834  (void)memset((void *)index, 0, sizeof(int) * sizeZ);
835
836  /* Initialize BFS by entering f in the queue. */
837  item = ALLOC(BfsItem, 1);
838  (void)memset((void *)item, 0, sizeof(BfsItem));
839  item->node = f;
840  item->reach = 1;
841  lv = bdd_read_zdd_level(dd,bdd_node_read_index(f));
842  level[lv] = item;
843  index[lv] = bdd_node_read_index(f);
844  start_level = last_level = lv;
845
846  if (!bdd_is_constant(bdd_bdd_T(f))) {
847    list = ALLOC(BfsList, 1);
848    (void)memset((void *)list, 0, sizeof(BfsList));
849    list->item = item;
850    list->child = 1;
851    last_list = list;
852  } else
853    list = last_list = (BfsList *)NULL;
854  if (!bdd_is_constant(bdd_bdd_E(f))) {
855    last_list = ALLOC(BfsList, 1);
856    (void)memset((void *)last_list, 0, sizeof(BfsList));
857    last_list->item = item;
858    last_list->child = 0;
859    if (list)
860      list->next = last_list;
861    else
862      list = last_list;
863  }
864
865  /* Perform the BFS. */
866  while (list) {
867    cur_level = sizeZ;
868    cur_list = list;
869    while (cur_list) {
870      if (cur_list->child)
871        id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
872      else
873        id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
874      next_level = bdd_read_zdd_level(dd,id);
875      cur_level = (cur_level < next_level) ? cur_level : next_level;
876      cur_list = cur_list->next;
877    }
878    last_level = cur_level;
879    save_last_list = last_list;
880
881    pre_list = (BfsList *)NULL;
882    cur_list = list;
883    while (cur_list) {
884      if (cur_list->child)
885        id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
886      else
887        id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
888      next_level = bdd_read_zdd_level(dd,id);
889
890      if (next_level != cur_level) {
891        pre_list = cur_list;
892        cur_list = cur_list->next;
893        continue;
894      }
895
896      if (cur_list->child)
897        node = bdd_bdd_T(cur_list->item->node);
898      else
899        node = bdd_bdd_E(cur_list->item->node);
900
901      exist = 0;
902      last_item = level[cur_level];
903      while (last_item) {
904        if (node == last_item->node) {
905          last_item->reach += cur_list->item->reach;
906          exist = 1;
907          break;
908        }
909        if (last_item->next)
910          last_item = last_item->next;
911        else
912          break;
913      }
914
915      if (exist == 0) {
916        item = ALLOC(BfsItem, 1);
917        (void)memset((void *)item, 0, sizeof(BfsItem));
918        item->node = node;
919        item->reach = cur_list->item->reach;
920        if (last_item)
921          last_item->next = item;
922        else {
923          level[cur_level] = item;
924          index[cur_level] = id;
925        }
926
927        if (!bdd_is_constant(bdd_bdd_T(node))) {
928          new_list = ALLOC(BfsList, 1);
929          (void)memset((void *)new_list, 0, sizeof(BfsList));
930          new_list->item = item;
931          new_list->child = 1;
932          last_list->next = new_list;
933          last_list = new_list;
934        }
935        if (!bdd_is_constant(bdd_bdd_E(node))) {
936          new_list = ALLOC(BfsList, 1);
937          (void)memset((void *)new_list, 0, sizeof(BfsList));
938          new_list->item = item;
939          new_list->child = 0;
940          last_list->next = new_list;
941          last_list = new_list;
942        }
943      }
944
945      next_list = cur_list->next;
946      if (cur_list == list && cur_list == last_list) {
947        FREE(cur_list);
948        list = next_list;
949      } else if (cur_list == list) {
950        FREE(cur_list);
951        pre_list = (BfsList *)NULL;
952        if (list == save_last_list) {
953          list = next_list;
954          next_list = (BfsList *)NULL;
955        } else
956          list = next_list;
957      } else if (cur_list == last_list) {
958        if (pre_list)
959          pre_list->next = cur_list->next;
960        FREE(cur_list);
961        last_list = pre_list;
962      } else {
963        if (pre_list)
964          pre_list->next = cur_list->next;
965        if (cur_list == save_last_list) {
966          FREE(cur_list);
967          next_list = (BfsList *)NULL;
968        } else
969          FREE(cur_list);
970      }
971
972      cur_list = next_list;
973    }
974  }
975
976  /* Compute the number of paths to the constant 1 for each node in
977   * bottom up fashion. Update the occurrence count of the variables.
978   */
979  for (i = last_level; i >= start_level; i--) {
980    item = level[i];
981    while (item) {
982      ct = ce = 0;
983      if (bdd_bdd_T(item->node) == one)
984        ct = 1;
985      else {
986        node = bdd_bdd_T(item->node);
987        next_level = bdd_read_zdd_level(dd, bdd_node_read_index(node));
988        cur_item = level[next_level];
989        while (cur_item) {
990          if (cur_item->node == node) {
991            ct = cur_item->count;
992            break;
993          }
994          cur_item = cur_item->next;
995        }
996      }
997      if (bdd_bdd_E(item->node) != zero) {
998        node = bdd_bdd_E(item->node);
999        next_level = bdd_read_zdd_level(dd,
1000                                        bdd_node_read_index(node));
1001        cur_item = level[next_level];
1002        while (cur_item) {
1003          if (cur_item->node == node) {
1004            ce = cur_item->count;
1005            break;
1006          }
1007          cur_item = cur_item->next;
1008        }
1009      }
1010      item->count = ct + ce;
1011      count[index[i]] += ct * item->reach;
1012      item = item->next;
1013    }
1014  }
1015
1016  /* Clean up. */
1017  for (i = last_level; i >= start_level; i--) {
1018    item = level[i];
1019    while (item) {
1020      next_item = item->next;
1021      FREE(item);
1022      item = next_item;
1023    }
1024  }
1025
1026  FREE(level);
1027  FREE(index);
1028}
1029
1030
1031/*---------------------------------------------------------------------------*/
1032/* Definition of static functions                                            */
1033/*---------------------------------------------------------------------------*/
1034
1035
1036/**Function********************************************************************
1037
1038  Synopsis [Finds a ZDD node that is referred by more than one parent
1039  node in a function.]
1040
1041  Description [Finds a ZDD node that is referred by more than one parent
1042  node in a function. Performs a DFS from f. Whenever a node is visited,
1043  the node is marked. When a node is visited, if the node is already marked,
1044  it returns the index of the node. Uses the LSB of the next pointer as
1045  visited flag. This function returns the number of path to constant 1 from
1046  the node, and return value -1 means already found.]
1047
1048  SideEffects [Once this function is called, SynthZddClearFlag() should
1049  be called right after.];
1050
1051  SeeAlso     [SynthZddClearFlag]
1052
1053******************************************************************************/
1054static int
1055FindQuickDivisor(bdd_node *f,
1056                 bdd_node *one,
1057                 int *v)
1058{
1059  int           c, ct, ce;
1060  bdd_node      *temp = bdd_read_next(f);
1061
1062  if (bdd_is_constant(f)) {
1063    if (f == one)
1064      return(1);
1065    else
1066      return(0);
1067  }
1068
1069  if (bdd_is_complement(temp)) { /* already visited */
1070    *v = bdd_node_read_index(f);
1071    return(-1);
1072  }
1073  /* mark as visited */
1074  bdd_set_next(f, bdd_not_bdd_node(temp));
1075
1076  ct = FindQuickDivisor(bdd_bdd_T(f), one, v);
1077  if (ct == -1) /* already found */
1078    return(-1);
1079  else if (ct > 1) {
1080    *v = bdd_node_read_index(f);
1081    return(-1);
1082  }
1083
1084  ce = FindQuickDivisor(bdd_bdd_E(f), one, v);
1085  if (ce == -1) /* already found */
1086    return(-1);
1087
1088  /* Add the number of path to constant 1 from two children nodes. */
1089  c = ct + ce;
1090  return(c);
1091}
Note: See TracBrowser for help on using the repository browser.