source: vis_dev/vis-2.3/src/synth/synthSimple.c @ 14

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

vis2.3
File size: 32.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthSimple.c]
4
5  PackageName [synth]
6
7  Synopsis    [Simple factorization method.]
8
9  Description []
10
11  Author      [In-Ho Moon, Balakrishna Kumthekar]
12
13  Copyright [This file was created at the University of Colorado at Boulder.
14  The University of Colorado at Boulder makes no warranty about the suitability
15  of this software for any purpose.  It is presented on an AS IS basis.]
16
17******************************************************************************/
18
19#include "synthInt.h"
20
21static char rcsid[] UNUSED = "$Id: synthSimple.c,v 1.36 2005/04/23 14:37:51 jinh Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27
28/*---------------------------------------------------------------------------*/
29/* Type declarations                                                         */
30/*---------------------------------------------------------------------------*/
31
32
33/*---------------------------------------------------------------------------*/
34/* Structure declarations                                                    */
35/*---------------------------------------------------------------------------*/
36
37
38/*---------------------------------------------------------------------------*/
39/* Variable declarations                                                     */
40/*---------------------------------------------------------------------------*/
41
42extern  int     CompMode;
43extern  int     UseMtree;
44extern  int     UseCommonDivisor;
45extern  int     TryNodeSharing;
46extern  int     Resubstitution;
47extern  int     RemainderComplement;
48extern  int     noMemoryFlag;
49extern  int     VerifyTreeMode;
50
51/**AutomaticStart*************************************************************/
52
53/*---------------------------------------------------------------------------*/
54/* Static function prototypes                                                */
55/*---------------------------------------------------------------------------*/
56
57static int CountZddLeafLiterals(bdd_manager *dd, bdd_node *node);
58
59/**AutomaticEnd***************************************************************/
60
61
62/*---------------------------------------------------------------------------*/
63/* Definition of exported functions                                          */
64/*---------------------------------------------------------------------------*/
65
66
67/*---------------------------------------------------------------------------*/
68/* Definition of internal functions                                          */
69/*---------------------------------------------------------------------------*/
70
71/**Function********************************************************************
72
73  Synopsis [Factorizes a function using a simple method.]
74
75  Description [Factorizes a function using a simple method. Here simple
76  refers that this algorithm tries to factorize just recursively. First
77  it finds a divisor, then finds quotient and remainder, and then recurs
78  for each.  The argument table consists of a pair of bdd_node and MlTree,
79  f is to be factorized, level is the depth of MlTree from top, ref returns 1
80  if new MlTree is created for f, otherwise returns 0, comp_d_tree is usually
81  NULL except when post factoring takes place(here post factoring is the
82  case to factorize a leaf node by another leaf node and a leaf node is a node
83  in which there is no divisor), comp_d_tree is a tree which is going to be
84  used as a divisor and comp_d_flag is used to indicate which node is going
85  to be used as a divisor between regular node and complement node, bring is
86  usually NULL except post factoring: when we update an already existing
87  tree by further factorization, we pass this tree to reuse it.]
88
89  SideEffects []
90
91  SeeAlso     [SynthGenericFactorTree]
92
93******************************************************************************/
94MlTree *
95SynthSimpleFactorTree(bdd_manager *dd,
96                      st_table *table,
97                      bdd_node *f,
98                      int level,
99                      int *ref,
100                      MlTree *comp_d_tree,
101                      int comp_d_flag,
102                      MlTree *bring,
103                      int verbosity)
104{
105  bdd_node      *one = bdd_read_one(dd);
106  bdd_node      *zero = bdd_read_zero(dd);
107  bdd_node      *d, *q, *r, *m;
108  MlTree        *tree, *q_tree, *d_tree, *r_tree;
109  char          message[120];
110  char          space[100];
111  MlTree        *comp_q_tree = (MlTree *)NULL;
112  MlTree        *comp_r_tree = (MlTree *)NULL;
113  int           found;
114  MlTree        *tmp_tree;
115  int           comp_flag;
116
117  if (verbosity > 1) {
118    SynthGetSpaceString(space, level * 2, 80);
119    sprintf(message, "%s[%d] in : ", space, level);
120    SynthPrintZddTreeMessage(dd, f, message);
121    sprintf(message, "%s[%d]out : ", space, level);
122  }
123
124  if (bring)
125    tree = (MlTree *)NULL;
126  else {
127    tree = SynthLookupMlTable(table, dd, f, 1, verbosity);
128    /* tree could be NULL because of reordering, or a failure to
129     * allocate memory or just that f was not in the cache.
130     * So, we would like return NULL ONLY in the case of
131     * reordering or failure to allocate memory.
132     */
133    if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
134      return(NULL);
135  }
136  if (tree) {
137    if (verbosity > 1)
138      SynthPrintMlTreeMessage(dd, tree, message);
139    *ref = 1;
140    return(tree);
141  }
142
143  if (f == one || f == zero) {
144    tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity);
145    if (!tree)
146      return(NULL);
147    tmp_tree = tree;
148    tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
149    if (!tree) {
150      if (*ref == 0)
151        SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
152      return(NULL);
153    } else if (tree != tmp_tree) {
154      *ref = 1;
155      if (comp_flag)
156        tree = MlTree_Not(tree);
157    }
158    if (verbosity > 1)
159      SynthPrintMlTreeMessage(dd, tree, message);
160    return(tree);
161  }
162
163  d_tree = (MlTree *)NULL;
164  if (comp_d_tree) {
165    if (comp_d_flag)
166      d = comp_d_tree->complement;
167    else
168      d = comp_d_tree->node;
169    if (!d)
170      return((MlTree *)NULL);
171    bdd_ref(d);
172  } else {
173    found = 0;
174    d = (* SynthGetZddDivisorFunc())(dd, f);
175    if (!d)
176      return(NULL);
177    bdd_ref(d);
178    if (TryNodeSharing) {
179      /* Here, we don't need to call bdd_ref. */
180      d = SynthFindBiggerDivisorInList(dd, table, f, d, &found,
181                                       &comp_d_flag, &comp_d_tree, verbosity);
182      if (!d)
183        return(NULL);
184    }
185    if (UseCommonDivisor && found == 0) {
186      tree = SynthGetFactorTreeWithCommonDivisor(dd, table,
187                         SynthSimpleFactorTree, f, d, level, ref, verbosity);
188      if (tree)
189        return(tree);
190      if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
191        return(NULL);
192    }
193  }
194  if (d == f) {
195    tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity);
196    if (!tree) {
197      bdd_recursive_deref_zdd(dd, d);
198      return(NULL);
199    }
200    if (verbosity > 1)
201      SynthPrintMlTreeMessage(dd, tree, message);
202    tmp_tree = tree;
203    tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
204    if (!tree) {
205      bdd_recursive_deref_zdd(dd, d);
206      return(NULL);
207    } else if (tree == tmp_tree) {
208      if (*ref == 0)
209        SynthPutMlTreeInList(dd, tree, 0);
210    } else {
211      *ref = 1;
212      if (comp_flag)
213        tree = MlTree_Not(tree);
214    }
215    bdd_recursive_deref_zdd(dd, d);
216    return(tree);
217  }
218  if (!comp_d_tree) {
219    if (st_lookup(table, (char *)d, &d_tree)) {
220      SynthSetSharedFlag(dd, d_tree);
221      if (MlTree_Regular(d_tree)->candidate) {
222        if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
223          bdd_recursive_deref_zdd(dd, d);
224          return(NULL);
225        }
226      }
227      if (MlTree_IsComplement(d_tree)) {
228        d_tree = MlTree_Regular(d_tree);
229        comp_d_tree = d_tree;
230        d_tree = (MlTree *)NULL;
231      }
232    }
233  } else {
234    if (!comp_d_flag)
235      d_tree = comp_d_tree;
236  }
237
238  q = (* SynthGetZddDivideFunc())(dd, f, d);
239  if (!q) {
240    bdd_recursive_deref_zdd(dd, d);
241    return(NULL);
242  }
243  bdd_ref(q);
244  if (comp_d_tree && q == zero) {
245    bdd_recursive_deref_zdd(dd, d);
246    bdd_recursive_deref_zdd(dd, q);
247    return((MlTree *)NULL);
248  }
249  if (q == one) {
250    bdd_recursive_deref_zdd(dd, q);
251    tree = SynthPostFactorTree(dd, table, f, q, d, bring,
252                       comp_d_tree, comp_d_flag, message, ref, verbosity);
253    bdd_recursive_deref_zdd(dd, d);
254    return(tree);
255  }
256
257  if (comp_d_tree && d_tree == comp_d_tree)
258    comp_d_tree = (MlTree *)NULL;
259
260  q_tree = (MlTree *)NULL;
261  if (st_lookup(table, (char *)q, &q_tree)) {
262    SynthSetSharedFlag(dd, q_tree);
263    if (MlTree_Regular(q_tree)->candidate) {
264      if (!SynthUseCandidate(table, dd, q_tree, verbosity)) {
265        bdd_recursive_deref_zdd(dd, d);
266        bdd_recursive_deref_zdd(dd, q);
267        return(NULL);
268      }
269    }
270    if (MlTree_IsComplement(q_tree)) {
271      q_tree = MlTree_Regular(q_tree);
272      comp_q_tree = q_tree;
273      q_tree = (MlTree *)NULL;
274    }
275  }
276
277  m = (* SynthGetZddProductFunc())(dd, d, q);
278  if (!m) {
279    bdd_recursive_deref_zdd(dd, d);
280    bdd_recursive_deref_zdd(dd, q);
281    return(NULL);
282  }
283  bdd_ref(m);
284  r = bdd_zdd_diff(dd, f, m);
285  if (!r) {
286    bdd_recursive_deref_zdd(dd, d);
287    bdd_recursive_deref_zdd(dd, q);
288    bdd_recursive_deref_zdd(dd, m);
289    return(NULL);
290  }
291  bdd_ref(r);
292
293  r_tree = (MlTree *)NULL;
294  if (st_lookup(table, (char *)r, &r_tree)) {
295    SynthSetSharedFlag(dd, r_tree);
296    if (MlTree_Regular(r_tree)->candidate) {
297      if (!SynthUseCandidate(table, dd, r_tree, verbosity)) {
298        bdd_recursive_deref_zdd(dd, d);
299        bdd_recursive_deref_zdd(dd, q);
300        bdd_recursive_deref_zdd(dd, m);
301        bdd_recursive_deref_zdd(dd, r);
302        return(NULL);
303      }
304    }
305    if (MlTree_IsComplement(r_tree)) {
306      r_tree = MlTree_Regular(r_tree);
307      comp_r_tree = r_tree;
308      r_tree = (MlTree *)NULL;
309    }
310  }
311
312  tree = SynthFactorTreeRecur(dd, table, SynthSimpleFactorTree,
313                              f, q, d, r, m, q_tree, d_tree, r_tree,
314                              comp_q_tree, comp_d_tree, comp_r_tree,
315                              bring, level, space, message, ref, verbosity);
316  bdd_recursive_deref_zdd(dd, d);
317  bdd_recursive_deref_zdd(dd, q);
318  bdd_recursive_deref_zdd(dd, m);
319  bdd_recursive_deref_zdd(dd, r);
320
321  if (VerifyTreeMode) {
322    SynthVerifyTree(dd, tree, 0);
323    SynthVerifyMlTable(dd, table);
324  }
325
326  return(tree);
327}
328
329
330/**Function********************************************************************
331
332  Synopsis [Finds a bigger divisor in divisor list.]
333
334  Description [Finds a bigger divisor in divisor list.]
335
336  SideEffects []
337
338  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]
339
340******************************************************************************/
341bdd_node *
342SynthFindBiggerDivisorInList(bdd_manager *dd,
343                             st_table *table,
344                             bdd_node *f,
345                             bdd_node *d,
346                             int *found,
347                             int *comp_d_flag,
348                             MlTree **comp_d_tree,
349                             int verbosity)
350{
351  bdd_node      *zero = bdd_read_zero(dd);
352  int           size, nSupports;
353  unsigned int  *support;
354  int           flag;
355  int           nL, nLiterals;
356  bdd_node      *candy;
357  MlTree        *cur;
358  bdd_node      *q;
359
360  nSupports = SynthGetSupportCount(dd, d);
361  size = bdd_num_zdd_vars(dd) / (sizeof(unsigned int) * 8) + 1;
362  support = ALLOC(unsigned int, size);
363  SynthGetSupportMask(dd, f, support);
364  flag = 0;
365  cur = SynthGetHeadTreeOfSize(SynthGetLiteralCount(dd, f) - 1);
366  nLiterals = CountZddLeafLiterals(dd, d);
367  if (nLiterals == -1) {
368    noMemoryFlag = 1;
369    FREE(support);
370    bdd_recursive_deref_zdd(dd, d);
371    return(NULL);
372  }
373
374  while (cur) {
375    if (cur->nLiterals < nSupports)
376      break;
377    nL = CountZddLeafLiterals(dd, cur->node);
378
379    if ((!SynthIsSubsetOfSupport(size, cur->support, support)) ||
380        nL < nLiterals) {
381      flag = 0;
382      cur = cur->next;
383      continue;
384    }
385
386    if (flag)
387      candy = cur->complement;
388    else
389      candy = cur->node;
390    q = (* SynthGetZddDivideFunc())(dd, f, candy);
391    if (!q) {
392      FREE(support);
393      bdd_recursive_deref_zdd(dd, d);
394      return(NULL);
395    }
396    bdd_ref(q);
397    bdd_recursive_deref_zdd(dd, q);
398    if (q != zero) {
399      if (MlTree_Regular(cur)->candidate) {
400        if (!SynthUseCandidate(table, dd, cur, verbosity)) {
401          FREE(support);
402          bdd_recursive_deref_zdd(dd, d);
403          return(NULL);
404        }
405      }
406      *found = 1;
407      *comp_d_flag = flag;
408      *comp_d_tree = cur;
409      bdd_recursive_deref_zdd(dd, d);
410      d = candy;
411      bdd_ref(d);
412      break;
413    }
414    if (flag == 0 && cur->complement)
415      flag = 1;
416    else {
417      cur = cur->next;
418      flag = 0;
419    }
420  }
421
422  FREE(support);
423  return(d);
424}
425
426
427/**Function********************************************************************
428
429  Synopsis [Factorizes a function with a common divisor if it exists.]
430
431  Description [Factorizes a function with a common divisor if it exists.]
432
433  SideEffects []
434
435  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]
436
437******************************************************************************/
438MlTree *
439SynthGetFactorTreeWithCommonDivisor(bdd_manager *dd,
440                                    st_table *table,
441                                    MlTree *(* factoring_func)(bdd_manager *,
442                                                               st_table *,
443                                                               bdd_node *, int,
444                                                               int *, MlTree *,
445                                                               int, MlTree *,
446                                                               int),
447                                    bdd_node *f,
448                                    bdd_node *d,
449                                    int level,
450                                    int *ref,
451                                    int verbosity)
452{
453  bdd_node      *zero = bdd_read_zero(dd);
454  bdd_node      *cd;
455  bdd_node      *q;
456  MlTree        *tree, *q_tree, *d_tree, *r_tree;
457  int           q_ref, d_ref, r_ref;
458  MlTree        *comp_q_tree = (MlTree *)NULL;
459  MlTree        *comp_d_tree = (MlTree *)NULL;
460  MlTree        *comp_r_tree = (MlTree *)NULL;
461  int           q_tree_exist;
462  MlTree        *tmp_tree;
463  char          message[120];
464  char          space[100];
465  char          comp_mess[120];
466  int           comp_flag;
467
468  q_ref = d_ref = r_ref = 0;
469
470  if (verbosity > 1) {
471    SynthGetSpaceString(space, level * 2, 80);
472    sprintf(message, "%s[%d]out : ", space, level);
473  }
474
475  cd = SynthZddCommonDivisor(dd, f);
476  if (cd) {
477    bdd_recursive_deref_zdd(dd, d);
478    d = cd;
479    bdd_ref(d);
480    q = (* SynthGetZddDivideFunc())(dd, f, d);
481    if (!q) {
482      bdd_recursive_deref_zdd(dd, d);
483      return(NULL);
484    }
485    bdd_ref(q);
486
487    d_tree = (MlTree *)NULL;
488    if (st_lookup(table, (char *)d, &d_tree)) {
489      SynthSetSharedFlag(dd, d_tree);
490      if (MlTree_Regular(d_tree)->candidate) {
491        if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
492          bdd_recursive_deref_zdd(dd, d);
493          bdd_recursive_deref_zdd(dd, q);
494          return(NULL);
495        }
496      }
497      if (MlTree_IsComplement(d_tree)) {
498        d_tree = MlTree_Regular(d_tree);
499        comp_d_tree = d_tree;
500      }
501      d_ref = 1;
502    } else {
503      d_tree = SynthFindOrCreateMlTree(table, dd, d, 1, 0, &d_ref, verbosity);
504      if (!d_tree) {
505        bdd_recursive_deref_zdd(dd, d);
506        bdd_recursive_deref_zdd(dd, q);
507        return(NULL);
508      }
509      if (MlTree_IsComplement(d_tree)) {
510        d_tree = MlTree_Regular(d_tree);
511        comp_d_tree = d_tree;
512      }
513      tmp_tree = d_tree;
514      d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
515                                           verbosity);
516      if (!d_tree) {
517        bdd_recursive_deref_zdd(dd, d);
518        bdd_recursive_deref_zdd(dd, q);
519        return(NULL);
520      } else if (d_tree == tmp_tree) {
521        if (d_ref == 0)
522          SynthPutMlTreeInList(dd, d_tree, 0);
523      } else {
524        if (comp_flag)
525          comp_d_tree = d_tree;
526        d_ref = 1;
527      }
528    }
529
530    q_tree = (MlTree *)NULL;
531    if (st_lookup(table, (char *)q, &q_tree)) {
532      SynthSetSharedFlag(dd, q_tree);
533      if (MlTree_Regular(q_tree)->candidate) {
534        if (!SynthUseCandidate(table, dd, q_tree, verbosity)) {
535          bdd_recursive_deref_zdd(dd, d);
536          bdd_recursive_deref_zdd(dd, q);
537          return(NULL);
538        }
539      }
540      if (MlTree_IsComplement(q_tree)) {
541        q_tree = MlTree_Regular(q_tree);
542        comp_q_tree = q_tree;
543        q_tree = (MlTree *)NULL;
544      }
545    }
546
547    if (verbosity > 1)
548      (void) fprintf(vis_stdout,"%s[%d] quotient\n", space, level);
549    q_tree_exist = 0;
550    if (q_tree) {
551      q_ref = 1;
552      q_tree_exist = 1;
553    } else if (comp_q_tree) {
554      q_tree = comp_q_tree;
555      q_ref = 1;
556      if (verbosity > 1) {
557        sprintf(comp_mess, "%s\t(C) : ", space);
558        SynthPrintZddTreeMessage(dd, q, comp_mess);
559      }
560    } else {
561      q_tree = (* factoring_func)(dd, table, q, level + 1,&q_ref,
562                                  NULL, 0, NULL, verbosity);
563      if (!q_tree) {
564        bdd_recursive_deref_zdd(dd, d);
565        bdd_recursive_deref_zdd(dd, q);
566        return(NULL);
567      }
568      if (MlTree_IsComplement(q_tree)) {
569        q_tree = MlTree_Regular(q_tree);
570        comp_q_tree = q_tree;
571      } else
572        bdd_ref(q_tree->node);
573    }
574    tmp_tree = q_tree;
575    q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
576                                         verbosity);
577    if (!q_tree) {
578      bdd_recursive_deref_zdd(dd, d);
579      bdd_recursive_deref_zdd(dd, q);
580      if (comp_q_tree != q_tree)
581        bdd_recursive_deref_zdd(dd, q_tree->node);
582      return(NULL);
583    } else if (q_tree != tmp_tree) {
584      if (comp_flag)
585        comp_q_tree = q_tree;
586      q_ref = 1;
587    }
588
589    r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &r_ref, verbosity);
590    if (!r_tree) {
591      bdd_recursive_deref_zdd(dd, d);
592      bdd_recursive_deref_zdd(dd, q);
593      if (comp_q_tree != q_tree)
594        bdd_recursive_deref_zdd(dd, q_tree->node);
595      return(NULL);
596    }
597    if (MlTree_IsComplement(r_tree)) {
598      r_tree = MlTree_Regular(r_tree);
599      comp_r_tree = r_tree;
600    }
601    tmp_tree = r_tree;
602    r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
603                                         verbosity);
604    if (!r_tree) {
605      bdd_recursive_deref_zdd(dd, d);
606      bdd_recursive_deref_zdd(dd, q);
607      if (comp_q_tree != q_tree)
608        bdd_recursive_deref_zdd(dd, q_tree->node);
609      return(NULL);
610    } else if (r_tree != tmp_tree) {
611      if (comp_flag)
612        comp_r_tree = r_tree;
613      r_ref = 1;
614    }
615
616    bdd_recursive_deref_zdd(dd, q);
617    bdd_recursive_deref_zdd(dd, d);
618    if ((!q_tree_exist) && (!comp_q_tree))
619      bdd_recursive_deref_zdd(dd, q_tree->node);
620
621    tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
622    if (!tree)
623      return(NULL);
624    if (*ref == 1)
625      (void) fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
626    tree->q = q_tree;
627    tree->d = d_tree;
628    tree->r = r_tree;
629    if (comp_q_tree)
630      tree->q_comp = 1;
631    if (comp_d_tree)
632      tree->d_comp = 1;
633    if (comp_r_tree)
634      tree->r_comp = 1;
635    tree->q_ref = q_ref;
636    tree->d_ref = d_ref;
637    tree->r_ref = r_ref;
638    if (verbosity > 1)
639      SynthPrintMlTreeMessage(dd, tree, message);
640    SynthPutMlTreeInList(dd, tree, 0);
641    if (VerifyTreeMode) {
642      SynthVerifyTree(dd, tree, 0);
643      SynthVerifyMlTable(dd, table);
644    }
645    return(tree);
646  } else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
647    bdd_recursive_deref_zdd(dd, d);
648  return(NULL);
649}
650
651
652/**Function********************************************************************
653
654  Synopsis [Try to factorize between leaf trees.]
655
656  Description [Try to factorize between leaf trees.]
657
658  SideEffects []
659
660  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]
661
662******************************************************************************/
663MlTree *
664SynthPostFactorTree(bdd_manager *dd,
665                    st_table *table,
666                    bdd_node *f,
667                    bdd_node *q,
668                    bdd_node *d,
669                    MlTree *bring,
670                    MlTree *comp_d_tree,
671                    int comp_d_flag,
672                    char *message,
673                    int *ref,
674                    int verbosity)
675{
676  bdd_node      *one = bdd_read_one(dd);
677  bdd_node      *r;
678  MlTree        *tree, *r_tree, *tmp_tree;
679  int           q_ref, r_ref;
680  MlTree        *comp_r_tree = (MlTree *)NULL;
681  int           comp_flag;
682
683  q_ref = r_ref = 0;
684
685  r = bdd_zdd_diff(dd, f, d);
686  if (!r)
687    return(NULL);
688  bdd_ref(r);
689  r_tree = (MlTree *)NULL;
690  if (st_lookup(table, (char *)r, &r_tree)) {
691    SynthSetSharedFlag(dd, r_tree);
692    if (MlTree_Regular(r_tree)->candidate) {
693      if (!SynthUseCandidate(table, dd, r_tree, verbosity)) {
694        bdd_recursive_deref_zdd(dd, r);
695        return(NULL);
696      }
697    }
698    if (MlTree_IsComplement(r_tree)) {
699      r_tree = MlTree_Regular(r_tree);
700      comp_r_tree = r_tree;
701    }
702    r_ref = 1;
703  } else {
704    r_tree = SynthFindOrCreateMlTree(table, dd, r, 1, 0, &r_ref, verbosity);
705    if (!r_tree) {
706      bdd_recursive_deref_zdd(dd, r);
707      return(NULL);
708    }
709    if (MlTree_IsComplement(r_tree)) {
710      comp_r_tree = MlTree_Regular(r_tree);
711      r_tree = comp_r_tree;
712    }
713    tmp_tree = r_tree;
714    r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
715                                         verbosity);
716    if (!r_tree) {
717      bdd_recursive_deref_zdd(dd, r);
718      return(NULL);
719    } else if (r_tree == tmp_tree) {
720      if (r_ref == 0)
721        SynthPutMlTreeInList(dd, r_tree, 0);
722    } else {
723      if (comp_flag)
724        comp_r_tree = r_tree;
725      r_ref = 1;
726    }
727  }
728  bdd_recursive_deref_zdd(dd, r);
729
730  if (bring)
731    tree = bring;
732  else {
733    tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
734    if (!tree)
735      return(NULL);
736    if (*ref)
737      (void)fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
738  }
739  tree->q = SynthFindOrCreateMlTree(table, dd, one, 1, 0, &q_ref, verbosity);
740  if (!tree->q)
741    return(NULL);
742  if (MlTree_IsComplement(tree->q)) {
743    tree->q = MlTree_Regular(tree->q);
744    tree->q_comp = 1;
745  }
746  tree->d = comp_d_tree;
747  tree->r = r_tree;
748  tree->d_comp = comp_d_flag;
749  if (comp_r_tree)
750    tree->r_comp = 1;
751  tree->q_ref = q_ref;
752  tree->d_ref = 1;
753  tree->r_ref = r_ref;
754  if (verbosity > 1)
755    SynthPrintMlTreeMessage(dd, tree, message);
756  if (bring)
757    bring->leaf = 0;
758  else
759    SynthPutMlTreeInList(dd, tree, 0);
760  if (VerifyTreeMode) {
761    SynthVerifyTree(dd, tree, 0);
762    SynthVerifyMlTable(dd, table);
763  }
764  return(tree);
765}
766
767
768/**Function********************************************************************
769
770  Synopsis [Recursive procedure of SynthSimpleFactorTree and
771  SynthGenericFactorTree.]
772
773  Description [Recursive procedure of SynthSimpleFactorTree and
774  SynthGenericFactorTree.]
775
776  SideEffects []
777
778  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]
779
780******************************************************************************/
781MlTree *
782SynthFactorTreeRecur(bdd_manager *dd,
783                     st_table *table,
784                     MlTree *(* factoring_func)(bdd_manager *, st_table *,
785                                                bdd_node *, int, int *,
786                                                MlTree *, int, MlTree *, int),
787                     bdd_node *f,
788                     bdd_node *q,
789                     bdd_node *d,
790                     bdd_node *r,
791                     bdd_node *m,
792                     MlTree *q_tree,
793                     MlTree *d_tree,
794                     MlTree *r_tree,
795                     MlTree *comp_q_tree,
796                     MlTree *comp_d_tree,
797                     MlTree *comp_r_tree,
798                     MlTree *bring,
799                     int level,
800                     char *space,
801                     char *message,
802                     int *ref,
803                     int verbosity)
804{
805  bdd_node      *one = bdd_read_one(dd);
806  bdd_node      *zero = bdd_read_zero(dd);
807  int           q_tree_exist, d_tree_exist, r_tree_exist;
808  MlTree        *m_tree;
809  MlTree        *tree, *tmp_tree;
810  int           q_ref, d_ref, r_ref, m_ref;
811  char          comp_mess[120];
812  int           comp_flag;
813
814  q_ref = d_ref = r_ref = 0;
815
816  if (verbosity > 1)
817    (void) fprintf(vis_stdout,"%s[%d] quotient\n", space, level);
818  q_tree_exist = 0;
819  if (q_tree) {
820    q_ref = 1;
821    q_tree_exist = 1;
822  } else if (comp_q_tree) {
823    q_tree = comp_q_tree;
824    q_ref = 1;
825    if (verbosity > 1) {
826      sprintf(comp_mess, "%s\t(C) : ", space);
827      SynthPrintZddTreeMessage(dd, q, comp_mess);
828    }
829  } else {
830    q_tree = (* factoring_func)(dd, table, q, level + 1,
831                                &q_ref, NULL, 0, NULL, verbosity);
832    if (!q_tree)
833      return(NULL);
834    if (MlTree_IsComplement(q_tree)) {
835      q_tree = MlTree_Regular(q_tree);
836      comp_q_tree = q_tree;
837    } else
838      bdd_ref(q_tree->node);
839  }
840  tmp_tree = q_tree;
841  q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
842                                       verbosity);
843  if (!q_tree) {
844    if (comp_q_tree != tmp_tree)
845      bdd_recursive_deref_zdd(dd, tmp_tree->node);
846    if (q_ref == 0)
847      SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
848    return(NULL);
849  } else if (q_tree != tmp_tree) {
850    if (comp_flag)
851      comp_q_tree = q_tree;
852    q_ref = 1;
853  }
854
855  if (verbosity > 1)
856    (void)fprintf(vis_stdout,"%s[%d] divisor\n", space, level);
857  d_tree_exist = 0;
858  if (d_tree) {
859    d_ref = 1;
860    d_tree_exist = 1;
861  } else if (comp_d_tree) {
862    d_tree = comp_d_tree;
863    d_ref = 1;
864    if (verbosity > 1) {
865      sprintf(comp_mess, "%s\t(C) : ", space);
866      SynthPrintZddTreeMessage(dd, d, comp_mess);
867    }
868  } else {
869    d_tree = (* factoring_func)(dd, table, d, level + 1, &d_ref,
870                                NULL, 0, NULL, verbosity);
871    if (!d_tree) {
872      if (comp_q_tree != q_tree)
873        bdd_recursive_deref_zdd(dd, q_tree->node);
874      if (q_ref == 0)
875        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
876      return(NULL);
877    }
878    if (MlTree_IsComplement(d_tree)) {
879      d_tree = MlTree_Regular(d_tree);
880      comp_d_tree = d_tree;
881    } else
882      bdd_ref(d_tree->node);
883  }
884  tmp_tree = d_tree;
885  d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
886                                       verbosity);
887  if (!d_tree) {
888    if (comp_q_tree != q_tree)
889      bdd_recursive_deref_zdd(dd, q_tree->node);
890    if (comp_d_tree != tmp_tree)
891      bdd_recursive_deref_zdd(dd, tmp_tree->node);
892    if (q_ref == 0)
893      SynthFreeMlTree(MlTree_Regular(q_tree), 1);
894    if (d_ref == 0)
895      SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
896    return(NULL);
897  } else if (d_tree != tmp_tree) {
898    if (comp_flag)
899      comp_d_tree = d_tree;
900    d_ref = 1;
901  }
902
903  m_tree = (MlTree *)NULL;
904  m_ref = 0;
905  if (UseMtree && m != f) {
906    m_tree = SynthFindOrCreateMlTree(table, dd, m, 0, 1, &m_ref, verbosity);
907    if (!m_tree) {
908      if (comp_q_tree != q_tree)
909        bdd_recursive_deref_zdd(dd, q_tree->node);
910      if (comp_d_tree != d_tree)
911        bdd_recursive_deref_zdd(dd, d_tree->node);
912      if (q_ref == 0)
913        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
914      if (d_ref == 0)
915        SynthFreeMlTree(MlTree_Regular(d_tree), 1);
916      return(NULL);
917    }
918    if (m_ref == 0) {
919      m_tree->q = q_tree;
920      m_tree->d = d_tree;
921      m_tree->r = (MlTree *)NULL;
922      if (comp_q_tree)
923        m_tree->q_comp = 1;
924      if (comp_d_tree)
925        m_tree->d_comp = 1;
926      m_tree->q_ref = q_ref;
927      m_tree->d_ref = d_ref;
928      m_tree->r_ref = 0;
929
930      tmp_tree = m_tree;
931      m_tree = SynthCheckAndMakeComplement(dd, table, m_tree, &comp_flag,
932                                           verbosity);
933      if (!m_tree) {
934        if (comp_q_tree != q_tree)
935          bdd_recursive_deref_zdd(dd, q_tree->node);
936        if (comp_d_tree != d_tree)
937          bdd_recursive_deref_zdd(dd, d_tree->node);
938        if (q_ref == 0)
939          SynthFreeMlTree(MlTree_Regular(q_tree), 1);
940        if (d_ref == 0)
941          SynthFreeMlTree(MlTree_Regular(d_tree), 1);
942        return(NULL);
943      } else if (m_tree == tmp_tree)
944        SynthPutMlTreeInList(dd, m_tree, 1);
945      else {
946        if (m_tree->candidate)
947          SynthPutMlTreeInList(dd, m_tree, 1);
948        else
949          m_tree = NIL(MlTree);
950      }
951      if (m_tree && VerifyTreeMode) {
952        SynthVerifyTree(dd, m_tree, 0);
953        SynthVerifyMlTable(dd, table);
954      }
955    }
956  }
957
958  if (verbosity > 1)
959    (void)fprintf(vis_stdout,"%s[%d] remainder\n", space, level);
960  r_tree_exist = 0;
961  if (r_tree) {
962    r_ref = 1;
963    r_tree_exist = 1;
964  } else if (comp_r_tree) {
965    r_tree = comp_r_tree;
966    r_ref = 1;
967    if (verbosity > 1) {
968      sprintf(comp_mess, "%s\t(C) : ", space);
969      SynthPrintZddTreeMessage(dd, r, comp_mess);
970    }
971  } else if (comp_d_tree) {
972    r_tree = (* factoring_func)(dd, table, r, level + 1,
973                                &r_ref, NULL, 0, NULL, verbosity);
974    if (!r_tree) {
975      if (comp_q_tree != q_tree)
976        bdd_recursive_deref_zdd(dd, q_tree->node);
977      if (comp_d_tree != d_tree)
978        bdd_recursive_deref_zdd(dd, d_tree->node);
979      if (q_ref == 0)
980        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
981      if (d_ref == 0)
982        SynthFreeMlTree(MlTree_Regular(d_tree), 1);
983      if (m_tree && m_ref == 0)
984        SynthFreeMlTree(MlTree_Regular(m_tree), 1);
985      return(NULL);
986    }
987    if (MlTree_IsComplement(r_tree)) {
988      r_tree = MlTree_Regular(r_tree);
989      comp_r_tree = r_tree;
990    } else
991      bdd_ref(r_tree->node);
992  } else {
993    if (Resubstitution) {
994      r_tree = (* factoring_func)(dd, table, r, level + 1,
995                                  &r_ref, d_tree, 1, NULL, verbosity);
996      if (!r_tree && (bdd_read_reordered_field(dd) || noMemoryFlag == 1)) {
997        if (comp_q_tree != q_tree)
998          bdd_recursive_deref_zdd(dd, q_tree->node);
999        if (comp_d_tree != d_tree)
1000          bdd_recursive_deref_zdd(dd, d_tree->node);
1001        if (q_ref == 0)
1002          SynthFreeMlTree(MlTree_Regular(q_tree), 1);
1003        if (d_ref == 0)
1004          SynthFreeMlTree(MlTree_Regular(d_tree), 1);
1005        if (m_tree && m_ref == 0)
1006          SynthFreeMlTree(MlTree_Regular(m_tree), 1);
1007        return(NULL);
1008      }
1009    }
1010    if (!r_tree) {
1011      r_tree = (* factoring_func)(dd, table, r, level + 1,
1012                                  &r_ref, NULL, 0, NULL, verbosity);
1013      if (!r_tree) {
1014        if (comp_q_tree != q_tree)
1015          bdd_recursive_deref_zdd(dd, q_tree->node);
1016        if (comp_d_tree != d_tree)
1017          bdd_recursive_deref_zdd(dd, d_tree->node);
1018        if (q_ref == 0)
1019          SynthFreeMlTree(MlTree_Regular(q_tree), 1);
1020        if (d_ref == 0)
1021          SynthFreeMlTree(MlTree_Regular(d_tree), 1);
1022        if (m_tree && m_ref == 0)
1023          SynthFreeMlTree(MlTree_Regular(m_tree), 1);
1024        return(NULL);
1025      }
1026    } else {
1027      if (r != one && r != zero)
1028        SynthSetSharedFlag(dd, d_tree);
1029    }
1030    if (MlTree_IsComplement(r_tree)) {
1031      r_tree = MlTree_Regular(r_tree);
1032      comp_r_tree = r_tree;
1033    } else
1034      bdd_ref(r_tree->node);
1035  }
1036  if (RemainderComplement) {
1037    tmp_tree = r_tree;
1038    r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
1039                                         verbosity);
1040    if (!r_tree) {
1041      if (comp_q_tree != q_tree)
1042        bdd_recursive_deref_zdd(dd, q_tree->node);
1043      if (comp_d_tree != d_tree)
1044        bdd_recursive_deref_zdd(dd, d_tree->node);
1045      if (comp_r_tree != tmp_tree)
1046        bdd_recursive_deref_zdd(dd, tmp_tree->node);
1047      if (q_ref == 0)
1048        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
1049      if (d_ref == 0)
1050        SynthFreeMlTree(MlTree_Regular(d_tree), 1);
1051      if (r_ref == 0)
1052        SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
1053      if (m_tree && m_ref == 0)
1054        SynthFreeMlTree(MlTree_Regular(m_tree), 1);
1055      return(NULL);
1056    } else if (r_tree != tmp_tree) {
1057      if (comp_flag)
1058        comp_r_tree = r_tree;
1059      r_ref = 1;
1060    }
1061  }
1062
1063  if ((!q_tree_exist) && (!comp_q_tree))
1064    bdd_recursive_deref_zdd(dd, q_tree->node);
1065  if ((!d_tree_exist) && (!comp_d_tree))
1066    bdd_recursive_deref_zdd(dd, d_tree->node);
1067  if ((!r_tree_exist) && (!comp_r_tree))
1068    bdd_recursive_deref_zdd(dd, r_tree->node);
1069
1070  if (bring) {
1071    tree = bring;
1072    tree->leaf = 0;
1073    tree->q = q_tree;
1074    tree->d = d_tree;
1075    tree->r = r_tree;
1076    if (comp_q_tree)
1077      tree->q_comp = 1;
1078    if (comp_d_tree)
1079      tree->d_comp = 1;
1080    if (comp_r_tree)
1081      tree->r_comp = 1;
1082    tree->q_ref = q_ref;
1083    tree->d_ref = d_ref;
1084    tree->r_ref = r_ref;
1085    if (UseMtree && m_tree && m_ref == 0) {
1086      MlTree_Regular(m_tree)->r = tree;
1087      if (m_tree->r->id == 0) {
1088        assert(0);
1089        /*
1090        if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
1091          SynthFreeMlTree(MlTree_Regular(m_tree), 1);
1092          return(NULL);
1093        }
1094        */
1095      }
1096    }
1097    if (verbosity > 1)
1098      SynthPrintMlTreeMessage(dd, tree, message);
1099    if (VerifyTreeMode) {
1100      SynthVerifyTree(dd, tree, 0);
1101      SynthVerifyMlTable(dd, table);
1102    }
1103    return(tree);
1104  }
1105
1106  tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
1107  if (!tree) {
1108    if (q_ref == 0)
1109      SynthFreeMlTree(MlTree_Regular(q_tree), 1);
1110    if (d_ref == 0)
1111      SynthFreeMlTree(MlTree_Regular(d_tree), 1);
1112    if (r_ref == 0)
1113      SynthFreeMlTree(MlTree_Regular(r_tree), 1);
1114    if (m_tree && m_ref == 0)
1115      SynthFreeMlTree(MlTree_Regular(m_tree), 1);
1116    return(NULL);
1117  }
1118  if (*ref == 1)
1119    (void)fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
1120  tree->q = q_tree;
1121  tree->d = d_tree;
1122  tree->r = r_tree;
1123  if (comp_q_tree)
1124    tree->q_comp = 1;
1125  if (comp_d_tree)
1126    tree->d_comp = 1;
1127  if (comp_r_tree)
1128    tree->r_comp = 1;
1129  tree->q_ref = q_ref;
1130  tree->d_ref = d_ref;
1131  tree->r_ref = r_ref;
1132  if (UseMtree && m_tree && m_ref == 0) {
1133    MlTree_Regular(m_tree)->r = tree;
1134    if (m_tree->r->id == 0) {
1135      assert(0);
1136      /*
1137      if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
1138        SynthFreeMlTree(MlTree_Regular(tree), 1);
1139        SynthFreeMlTree(MlTree_Regular(m_tree), 1);
1140        return(NULL);
1141      }
1142      */
1143    }
1144  }
1145  if (verbosity > 1)
1146    SynthPrintMlTreeMessage(dd, tree, message);
1147  SynthPutMlTreeInList(dd, tree, 0);
1148  if (VerifyTreeMode) {
1149    SynthVerifyTree(dd, tree, 0);
1150    SynthVerifyMlTable(dd, table);
1151  }
1152  return(tree);
1153}
1154
1155
1156/*---------------------------------------------------------------------------*/
1157/* Definition of static functions                                            */
1158/*---------------------------------------------------------------------------*/
1159
1160/**Function********************************************************************
1161
1162  Synopsis [Counts the number of literals of a leaf node.]
1163
1164  Description [Counts the number of literals of a leaf node.]
1165
1166  SideEffects []
1167
1168  SeeAlso     []
1169
1170******************************************************************************/
1171static int
1172CountZddLeafLiterals(bdd_manager *dd,
1173                     bdd_node *node)
1174{
1175  int   i, *support;
1176  int   count = 0;
1177  int   sizeZ = bdd_num_zdd_vars(dd);
1178
1179  support = ALLOC(int, sizeZ);
1180  if (!support)
1181    return(-1);
1182  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
1183  SynthZddSupportStep(bdd_regular(node), support);
1184  SynthZddClearFlag(bdd_regular(node));
1185  for (i = 0; i < sizeZ; i++) {
1186    if (support[i])
1187      count++;
1188  }
1189  FREE(support);
1190  return(count);
1191}
Note: See TracBrowser for help on using the repository browser.