source: vis_dev/vis-2.3/src/synth/synthGen.c @ 35

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

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