abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddZddIsop.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddZddIsop.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Functions to find irredundant SOP covers as ZDDs from BDDs.]
8 
9  Description [External procedures included in this module:
10  <ul>
11  <li> Cudd_bddIsop()
12  <li> Cudd_zddIsop()
13  <li> Cudd_MakeBddFromZddCover()
14  </ul>
15  Internal procedures included in this module:
16  <ul>
17  <li> cuddBddIsop()
18  <li> cuddZddIsop()
19  <li> cuddMakeBddFromZddCover()
20  </ul>
21  Static procedures included in this module:
22  <ul>
23  </ul>
24  ]
25 
26  SeeAlso []
27 
28  Author [In-Ho Moon]
29 
30  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
31 
32  All rights reserved.
33 
34  Redistribution and use in source and binary forms, with or without
35  modification, are permitted provided that the following conditions
36  are met:
37 
38  Redistributions of source code must retain the above copyright
39  notice, this list of conditions and the following disclaimer.
40 
41  Redistributions in binary form must reproduce the above copyright
42  notice, this list of conditions and the following disclaimer in the
43  documentation and/or other materials provided with the distribution.
44 
45  Neither the name of the University of Colorado nor the names of its
46  contributors may be used to endorse or promote products derived from
47  this software without specific prior written permission.
48 
49  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60  POSSIBILITY OF SUCH DAMAGE.]
61 
62 ******************************************************************************/
63 
64 #include "misc/util/util_hack.h"
65 #include "cuddInt.h"
66 
67 ABC_NAMESPACE_IMPL_START
68 
69 
70 
71 /*---------------------------------------------------------------------------*/
72 /* Constant declarations */
73 /*---------------------------------------------------------------------------*/
74 
75 
76 /*---------------------------------------------------------------------------*/
77 /* Stucture declarations */
78 /*---------------------------------------------------------------------------*/
79 
80 
81 /*---------------------------------------------------------------------------*/
82 /* Type declarations */
83 /*---------------------------------------------------------------------------*/
84 
85 
86 /*---------------------------------------------------------------------------*/
87 /* Variable declarations */
88 /*---------------------------------------------------------------------------*/
89 
90 #ifndef lint
91 static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio Exp $";
92 #endif
93 
94 /*---------------------------------------------------------------------------*/
95 /* Macro declarations */
96 /*---------------------------------------------------------------------------*/
97 
98 
99 /**AutomaticStart*************************************************************/
100 
101 /*---------------------------------------------------------------------------*/
102 /* Static function prototypes */
103 /*---------------------------------------------------------------------------*/
104 
105 
106 /**AutomaticEnd***************************************************************/
107 
108 /*---------------------------------------------------------------------------*/
109 /* Definition of exported functions */
110 /*---------------------------------------------------------------------------*/
111 
112 /**Function********************************************************************
113 
114  Synopsis [Computes an ISOP in ZDD form from BDDs.]
115 
116  Description [Computes an irredundant sum of products (ISOP) in ZDD
117  form from BDDs. The two BDDs L and U represent the lower bound and
118  the upper bound, respectively, of the function. The ISOP uses two
119  ZDD variables for each BDD variable: One for the positive literal,
120  and one for the negative literal. These two variables should be
121  adjacent in the ZDD order. The two ZDD variables corresponding to
122  BDD variable <code>i</code> should have indices <code>2i</code> and
123  <code>2i+1</code>. The result of this procedure depends on the
124  variable order. If successful, Cudd_zddIsop returns the BDD for
125  the function chosen from the interval. The ZDD representing the
126  irredundant cover is returned as a side effect in zdd_I. In case of
127  failure, NULL is returned.]
128 
129  SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on
130  successful return.]
131 
132  SeeAlso [Cudd_bddIsop Cudd_zddVarsFromBddVars]
133 
134 ******************************************************************************/
135 DdNode *
136 Cudd_zddIsop(
137  DdManager * dd,
138  DdNode * L,
139  DdNode * U,
140  DdNode ** zdd_I)
141 {
142  DdNode *res;
143  int autoDynZ;
144 
145  autoDynZ = dd->autoDynZ;
146  dd->autoDynZ = 0;
147 
148  do {
149  dd->reordered = 0;
150  res = cuddZddIsop(dd, L, U, zdd_I);
151  } while (dd->reordered == 1);
152  dd->autoDynZ = autoDynZ;
153  return(res);
154 
155 } /* end of Cudd_zddIsop */
156 
157 
158 /**Function********************************************************************
159 
160  Synopsis [Computes a BDD in the interval between L and U with a
161  simple sum-of-produuct cover.]
162 
163  Description [Computes a BDD in the interval between L and U with a
164  simple sum-of-produuct cover. This procedure is similar to
165  Cudd_zddIsop, but it does not return the ZDD for the cover. Returns
166  a pointer to the BDD if successful; NULL otherwise.]
167 
168  SideEffects [None]
169 
170  SeeAlso [Cudd_zddIsop]
171 
172 ******************************************************************************/
173 DdNode *
174 Cudd_bddIsop(
175  DdManager * dd,
176  DdNode * L,
177  DdNode * U)
178 {
179  DdNode *res;
180 
181  do {
182  dd->reordered = 0;
183  res = cuddBddIsop(dd, L, U);
184  } while (dd->reordered == 1);
185  return(res);
186 
187 } /* end of Cudd_bddIsop */
188 
189 
190 /**Function********************************************************************
191 
192  Synopsis [Converts a ZDD cover to a BDD graph.]
193 
194  Description [Converts a ZDD cover to a BDD graph. If successful, it
195  returns a BDD node, otherwise it returns NULL.]
196 
197  SideEffects []
198 
199  SeeAlso [cuddMakeBddFromZddCover]
200 
201 ******************************************************************************/
202 DdNode *
203 Cudd_MakeBddFromZddCover(
204  DdManager * dd,
205  DdNode * node)
206 {
207  DdNode *res;
208 
209  do {
210  dd->reordered = 0;
211  res = cuddMakeBddFromZddCover(dd, node);
212  } while (dd->reordered == 1);
213  return(res);
214 } /* end of Cudd_MakeBddFromZddCover */
215 
216 
217 /*---------------------------------------------------------------------------*/
218 /* Definition of internal functions */
219 /*---------------------------------------------------------------------------*/
220 
221 
222 /**Function********************************************************************
223 
224  Synopsis [Performs the recursive step of Cudd_zddIsop.]
225 
226  Description []
227 
228  SideEffects [None]
229 
230  SeeAlso [Cudd_zddIsop]
231 
232 ******************************************************************************/
233 DdNode *
234 cuddZddIsop(
235  DdManager * dd,
236  DdNode * L,
237  DdNode * U,
238  DdNode ** zdd_I)
239 {
240  DdNode *one = DD_ONE(dd);
241  DdNode *zero = Cudd_Not(one);
242  DdNode *zdd_one = DD_ONE(dd);
243  DdNode *zdd_zero = DD_ZERO(dd);
244  int v, top_l, top_u;
245  DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
246  DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
247  DdNode *Isub0, *Isub1, *Id;
248  DdNode *zdd_Isub0, *zdd_Isub1, *zdd_Id;
249  DdNode *x;
250  DdNode *term0, *term1, *sum;
251  DdNode *Lv, *Uv, *Lnv, *Unv;
252  DdNode *r, *y, *z;
253  int index;
254  DD_CTFP cacheOp;
255 
256  statLine(dd);
257  if (L == zero) {
258  *zdd_I = zdd_zero;
259  return(zero);
260  }
261  if (U == one) {
262  *zdd_I = zdd_one;
263  return(one);
264  }
265 
266  if (U == zero || L == one) {
267  printf("*** ERROR : illegal condition for ISOP (U < L).\n");
268  exit(1);
269  }
270 
271  /* Check the cache. We store two results for each recursive call.
272  ** One is the BDD, and the other is the ZDD. Both are needed.
273  ** Hence we need a double hit in the cache to terminate the
274  ** recursion. Clearly, collisions may evict only one of the two
275  ** results. */
276  cacheOp = (DD_CTFP) cuddZddIsop;
277  r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
278  if (r) {
279  *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
280  if (*zdd_I)
281  return(r);
282  else {
283  /* The BDD result may have been dead. In that case
284  ** cuddCacheLookup2 would have called cuddReclaim,
285  ** whose effects we now have to undo. */
286  cuddRef(r);
287  Cudd_RecursiveDeref(dd, r);
288  }
289  }
290 
291  top_l = dd->perm[Cudd_Regular(L)->index];
292  top_u = dd->perm[Cudd_Regular(U)->index];
293  v = ddMin(top_l, top_u);
294 
295  /* Compute cofactors. */
296  if (top_l == v) {
297  index = Cudd_Regular(L)->index;
298  Lv = Cudd_T(L);
299  Lnv = Cudd_E(L);
300  if (Cudd_IsComplement(L)) {
301  Lv = Cudd_Not(Lv);
302  Lnv = Cudd_Not(Lnv);
303  }
304  }
305  else {
306  index = Cudd_Regular(U)->index;
307  Lv = Lnv = L;
308  }
309 
310  if (top_u == v) {
311  Uv = Cudd_T(U);
312  Unv = Cudd_E(U);
313  if (Cudd_IsComplement(U)) {
314  Uv = Cudd_Not(Uv);
315  Unv = Cudd_Not(Unv);
316  }
317  }
318  else {
319  Uv = Unv = U;
320  }
321 
322  Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
323  if (Lsub0 == NULL)
324  return(NULL);
325  Cudd_Ref(Lsub0);
326  Usub0 = Unv;
327  Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
328  if (Lsub1 == NULL) {
329  Cudd_RecursiveDeref(dd, Lsub0);
330  return(NULL);
331  }
332  Cudd_Ref(Lsub1);
333  Usub1 = Uv;
334 
335  Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
336  if (Isub0 == NULL) {
337  Cudd_RecursiveDeref(dd, Lsub0);
338  Cudd_RecursiveDeref(dd, Lsub1);
339  return(NULL);
340  }
341  /*
342  if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
343  (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
344  dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
345  printf("*** ERROR : illegal permutation in ZDD. ***\n");
346  }
347  */
348  Cudd_Ref(Isub0);
349  Cudd_Ref(zdd_Isub0);
350  Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
351  if (Isub1 == NULL) {
352  Cudd_RecursiveDeref(dd, Lsub0);
353  Cudd_RecursiveDeref(dd, Lsub1);
354  Cudd_RecursiveDeref(dd, Isub0);
355  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
356  return(NULL);
357  }
358  /*
359  if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
360  (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
361  dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
362  printf("*** ERROR : illegal permutation in ZDD. ***\n");
363  }
364  */
365  Cudd_Ref(Isub1);
366  Cudd_Ref(zdd_Isub1);
367  Cudd_RecursiveDeref(dd, Lsub0);
368  Cudd_RecursiveDeref(dd, Lsub1);
369 
370  Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
371  if (Lsuper0 == NULL) {
372  Cudd_RecursiveDeref(dd, Isub0);
373  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
374  Cudd_RecursiveDeref(dd, Isub1);
375  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
376  return(NULL);
377  }
378  Cudd_Ref(Lsuper0);
379  Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
380  if (Lsuper1 == NULL) {
381  Cudd_RecursiveDeref(dd, Isub0);
382  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
383  Cudd_RecursiveDeref(dd, Isub1);
384  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
385  Cudd_RecursiveDeref(dd, Lsuper0);
386  return(NULL);
387  }
388  Cudd_Ref(Lsuper1);
389  Usuper0 = Unv;
390  Usuper1 = Uv;
391 
392  /* Ld = Lsuper0 + Lsuper1 */
393  Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
394  if (Ld == NULL) {
395  Cudd_RecursiveDeref(dd, Isub0);
396  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
397  Cudd_RecursiveDeref(dd, Isub1);
398  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
399  Cudd_RecursiveDeref(dd, Lsuper0);
400  Cudd_RecursiveDeref(dd, Lsuper1);
401  return(NULL);
402  }
403  Ld = Cudd_Not(Ld);
404  Cudd_Ref(Ld);
405  /* Ud = Usuper0 * Usuper1 */
406  Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
407  if (Ud == NULL) {
408  Cudd_RecursiveDeref(dd, Isub0);
409  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
410  Cudd_RecursiveDeref(dd, Isub1);
411  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
412  Cudd_RecursiveDeref(dd, Lsuper0);
413  Cudd_RecursiveDeref(dd, Lsuper1);
414  Cudd_RecursiveDeref(dd, Ld);
415  return(NULL);
416  }
417  Cudd_Ref(Ud);
418  Cudd_RecursiveDeref(dd, Lsuper0);
419  Cudd_RecursiveDeref(dd, Lsuper1);
420 
421  Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
422  if (Id == NULL) {
423  Cudd_RecursiveDeref(dd, Isub0);
424  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
425  Cudd_RecursiveDeref(dd, Isub1);
426  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
427  Cudd_RecursiveDeref(dd, Ld);
428  Cudd_RecursiveDeref(dd, Ud);
429  return(NULL);
430  }
431  /*
432  if ((!cuddIsConstant(Cudd_Regular(Id))) &&
433  (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
434  dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
435  printf("*** ERROR : illegal permutation in ZDD. ***\n");
436  }
437  */
438  Cudd_Ref(Id);
439  Cudd_Ref(zdd_Id);
440  Cudd_RecursiveDeref(dd, Ld);
441  Cudd_RecursiveDeref(dd, Ud);
442 
443  x = cuddUniqueInter(dd, index, one, zero);
444  if (x == NULL) {
445  Cudd_RecursiveDeref(dd, Isub0);
446  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
447  Cudd_RecursiveDeref(dd, Isub1);
448  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
449  Cudd_RecursiveDeref(dd, Id);
450  Cudd_RecursiveDerefZdd(dd, zdd_Id);
451  return(NULL);
452  }
453  Cudd_Ref(x);
454  /* term0 = x * Isub0 */
455  term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
456  if (term0 == NULL) {
457  Cudd_RecursiveDeref(dd, Isub0);
458  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
459  Cudd_RecursiveDeref(dd, Isub1);
460  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
461  Cudd_RecursiveDeref(dd, Id);
462  Cudd_RecursiveDerefZdd(dd, zdd_Id);
463  Cudd_RecursiveDeref(dd, x);
464  return(NULL);
465  }
466  Cudd_Ref(term0);
467  Cudd_RecursiveDeref(dd, Isub0);
468  /* term1 = x * Isub1 */
469  term1 = cuddBddAndRecur(dd, x, Isub1);
470  if (term1 == NULL) {
471  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
472  Cudd_RecursiveDeref(dd, Isub1);
473  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
474  Cudd_RecursiveDeref(dd, Id);
475  Cudd_RecursiveDerefZdd(dd, zdd_Id);
476  Cudd_RecursiveDeref(dd, x);
477  Cudd_RecursiveDeref(dd, term0);
478  return(NULL);
479  }
480  Cudd_Ref(term1);
481  Cudd_RecursiveDeref(dd, x);
482  Cudd_RecursiveDeref(dd, Isub1);
483  /* sum = term0 + term1 */
484  sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
485  if (sum == NULL) {
486  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
487  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
488  Cudd_RecursiveDeref(dd, Id);
489  Cudd_RecursiveDerefZdd(dd, zdd_Id);
490  Cudd_RecursiveDeref(dd, term0);
491  Cudd_RecursiveDeref(dd, term1);
492  return(NULL);
493  }
494  sum = Cudd_Not(sum);
495  Cudd_Ref(sum);
496  Cudd_RecursiveDeref(dd, term0);
497  Cudd_RecursiveDeref(dd, term1);
498  /* r = sum + Id */
499  r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
500  r = Cudd_NotCond(r, r != NULL);
501  if (r == NULL) {
502  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
503  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
504  Cudd_RecursiveDeref(dd, Id);
505  Cudd_RecursiveDerefZdd(dd, zdd_Id);
506  Cudd_RecursiveDeref(dd, sum);
507  return(NULL);
508  }
509  Cudd_Ref(r);
510  Cudd_RecursiveDeref(dd, sum);
511  Cudd_RecursiveDeref(dd, Id);
512 
513  if (zdd_Isub0 != zdd_zero) {
514  z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
515  if (z == NULL) {
516  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
517  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
518  Cudd_RecursiveDerefZdd(dd, zdd_Id);
519  Cudd_RecursiveDeref(dd, r);
520  return(NULL);
521  }
522  }
523  else {
524  z = zdd_Id;
525  }
526  Cudd_Ref(z);
527  if (zdd_Isub1 != zdd_zero) {
528  y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
529  if (y == NULL) {
530  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
531  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
532  Cudd_RecursiveDerefZdd(dd, zdd_Id);
533  Cudd_RecursiveDeref(dd, r);
534  Cudd_RecursiveDerefZdd(dd, z);
535  return(NULL);
536  }
537  }
538  else
539  y = z;
540  Cudd_Ref(y);
541 
542  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
543  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
544  Cudd_RecursiveDerefZdd(dd, zdd_Id);
545  Cudd_RecursiveDerefZdd(dd, z);
546 
547  cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
548  cuddCacheInsert2(dd, cacheOp, L, U, y);
549 
550  Cudd_Deref(r);
551  Cudd_Deref(y);
552  *zdd_I = y;
553  /*
554  if (Cudd_Regular(r)->index != y->index / 2) {
555  printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
556  }
557  */
558  return(r);
559 
560 } /* end of cuddZddIsop */
561 
562 
563 /**Function********************************************************************
564 
565  Synopsis [Performs the recursive step of Cudd_bddIsop.]
566 
567  Description []
568 
569  SideEffects [None]
570 
571  SeeAlso [Cudd_bddIsop]
572 
573 ******************************************************************************/
574 DdNode *
575 cuddBddIsop(
576  DdManager * dd,
577  DdNode * L,
578  DdNode * U)
579 {
580  DdNode *one = DD_ONE(dd);
581  DdNode *zero = Cudd_Not(one);
582  int v, top_l, top_u;
583  DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
584  DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
585  DdNode *Isub0, *Isub1, *Id;
586  DdNode *x;
587  DdNode *term0, *term1, *sum;
588  DdNode *Lv, *Uv, *Lnv, *Unv;
589  DdNode *r;
590  int index;
591 
592  statLine(dd);
593  if (L == zero)
594  return(zero);
595  if (U == one)
596  return(one);
597 
598  /* Check cache */
599  r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
600  if (r)
601  return(r);
602 
603  top_l = dd->perm[Cudd_Regular(L)->index];
604  top_u = dd->perm[Cudd_Regular(U)->index];
605  v = ddMin(top_l, top_u);
606 
607  /* Compute cofactors */
608  if (top_l == v) {
609  index = Cudd_Regular(L)->index;
610  Lv = Cudd_T(L);
611  Lnv = Cudd_E(L);
612  if (Cudd_IsComplement(L)) {
613  Lv = Cudd_Not(Lv);
614  Lnv = Cudd_Not(Lnv);
615  }
616  }
617  else {
618  index = Cudd_Regular(U)->index;
619  Lv = Lnv = L;
620  }
621 
622  if (top_u == v) {
623  Uv = Cudd_T(U);
624  Unv = Cudd_E(U);
625  if (Cudd_IsComplement(U)) {
626  Uv = Cudd_Not(Uv);
627  Unv = Cudd_Not(Unv);
628  }
629  }
630  else {
631  Uv = Unv = U;
632  }
633 
634  Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
635  if (Lsub0 == NULL)
636  return(NULL);
637  Cudd_Ref(Lsub0);
638  Usub0 = Unv;
639  Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
640  if (Lsub1 == NULL) {
641  Cudd_RecursiveDeref(dd, Lsub0);
642  return(NULL);
643  }
644  Cudd_Ref(Lsub1);
645  Usub1 = Uv;
646 
647  Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
648  if (Isub0 == NULL) {
649  Cudd_RecursiveDeref(dd, Lsub0);
650  Cudd_RecursiveDeref(dd, Lsub1);
651  return(NULL);
652  }
653  Cudd_Ref(Isub0);
654  Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
655  if (Isub1 == NULL) {
656  Cudd_RecursiveDeref(dd, Lsub0);
657  Cudd_RecursiveDeref(dd, Lsub1);
658  Cudd_RecursiveDeref(dd, Isub0);
659  return(NULL);
660  }
661  Cudd_Ref(Isub1);
662  Cudd_RecursiveDeref(dd, Lsub0);
663  Cudd_RecursiveDeref(dd, Lsub1);
664 
665  Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
666  if (Lsuper0 == NULL) {
667  Cudd_RecursiveDeref(dd, Isub0);
668  Cudd_RecursiveDeref(dd, Isub1);
669  return(NULL);
670  }
671  Cudd_Ref(Lsuper0);
672  Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
673  if (Lsuper1 == NULL) {
674  Cudd_RecursiveDeref(dd, Isub0);
675  Cudd_RecursiveDeref(dd, Isub1);
676  Cudd_RecursiveDeref(dd, Lsuper0);
677  return(NULL);
678  }
679  Cudd_Ref(Lsuper1);
680  Usuper0 = Unv;
681  Usuper1 = Uv;
682 
683  /* Ld = Lsuper0 + Lsuper1 */
684  Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
685  Ld = Cudd_NotCond(Ld, Ld != NULL);
686  if (Ld == NULL) {
687  Cudd_RecursiveDeref(dd, Isub0);
688  Cudd_RecursiveDeref(dd, Isub1);
689  Cudd_RecursiveDeref(dd, Lsuper0);
690  Cudd_RecursiveDeref(dd, Lsuper1);
691  return(NULL);
692  }
693  Cudd_Ref(Ld);
694  Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
695  if (Ud == NULL) {
696  Cudd_RecursiveDeref(dd, Isub0);
697  Cudd_RecursiveDeref(dd, Isub1);
698  Cudd_RecursiveDeref(dd, Lsuper0);
699  Cudd_RecursiveDeref(dd, Lsuper1);
700  Cudd_RecursiveDeref(dd, Ld);
701  return(NULL);
702  }
703  Cudd_Ref(Ud);
704  Cudd_RecursiveDeref(dd, Lsuper0);
705  Cudd_RecursiveDeref(dd, Lsuper1);
706 
707  Id = cuddBddIsop(dd, Ld, Ud);
708  if (Id == NULL) {
709  Cudd_RecursiveDeref(dd, Isub0);
710  Cudd_RecursiveDeref(dd, Isub1);
711  Cudd_RecursiveDeref(dd, Ld);
712  Cudd_RecursiveDeref(dd, Ud);
713  return(NULL);
714  }
715  Cudd_Ref(Id);
716  Cudd_RecursiveDeref(dd, Ld);
717  Cudd_RecursiveDeref(dd, Ud);
718 
719  x = cuddUniqueInter(dd, index, one, zero);
720  if (x == NULL) {
721  Cudd_RecursiveDeref(dd, Isub0);
722  Cudd_RecursiveDeref(dd, Isub1);
723  Cudd_RecursiveDeref(dd, Id);
724  return(NULL);
725  }
726  Cudd_Ref(x);
727  term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
728  if (term0 == NULL) {
729  Cudd_RecursiveDeref(dd, Isub0);
730  Cudd_RecursiveDeref(dd, Isub1);
731  Cudd_RecursiveDeref(dd, Id);
732  Cudd_RecursiveDeref(dd, x);
733  return(NULL);
734  }
735  Cudd_Ref(term0);
736  Cudd_RecursiveDeref(dd, Isub0);
737  term1 = cuddBddAndRecur(dd, x, Isub1);
738  if (term1 == NULL) {
739  Cudd_RecursiveDeref(dd, Isub1);
740  Cudd_RecursiveDeref(dd, Id);
741  Cudd_RecursiveDeref(dd, x);
742  Cudd_RecursiveDeref(dd, term0);
743  return(NULL);
744  }
745  Cudd_Ref(term1);
746  Cudd_RecursiveDeref(dd, x);
747  Cudd_RecursiveDeref(dd, Isub1);
748  /* sum = term0 + term1 */
749  sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
750  sum = Cudd_NotCond(sum, sum != NULL);
751  if (sum == NULL) {
752  Cudd_RecursiveDeref(dd, Id);
753  Cudd_RecursiveDeref(dd, term0);
754  Cudd_RecursiveDeref(dd, term1);
755  return(NULL);
756  }
757  Cudd_Ref(sum);
758  Cudd_RecursiveDeref(dd, term0);
759  Cudd_RecursiveDeref(dd, term1);
760  /* r = sum + Id */
761  r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
762  r = Cudd_NotCond(r, r != NULL);
763  if (r == NULL) {
764  Cudd_RecursiveDeref(dd, Id);
765  Cudd_RecursiveDeref(dd, sum);
766  return(NULL);
767  }
768  Cudd_Ref(r);
769  Cudd_RecursiveDeref(dd, sum);
770  Cudd_RecursiveDeref(dd, Id);
771 
772  cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
773 
774  Cudd_Deref(r);
775  return(r);
776 
777 } /* end of cuddBddIsop */
778 
779 
780 /**Function********************************************************************
781 
782  Synopsis [Converts a ZDD cover to a BDD graph.]
783 
784  Description [Converts a ZDD cover to a BDD graph. If successful, it
785  returns a BDD node, otherwise it returns NULL. It is a recursive
786  algorithm as the following. First computes 3 cofactors of a ZDD cover;
787  f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.
788  Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v
789  is the variable which has the index of the top node of the ZDD cover.
790  In this case, since the index of v can be larger than either one of T or
791  one of E, cuddUniqueInterIVO is called, here IVO stands for
792  independent variable ordering.]
793 
794  SideEffects []
795 
796  SeeAlso [Cudd_MakeBddFromZddCover]
797 
798 ******************************************************************************/
799 DdNode *
800 cuddMakeBddFromZddCover(
801  DdManager * dd,
802  DdNode * node)
803 {
804  DdNode *neW;
805  int v;
806  DdNode *f1, *f0, *fd;
807  DdNode *b1, *b0, *bd;
808  DdNode *T, *E;
809 
810  statLine(dd);
811  if (node == dd->one)
812  return(dd->one);
813  if (node == dd->zero)
814  return(Cudd_Not(dd->one));
815 
816  /* Check cache */
817  neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
818  if (neW)
819  return(neW);
820 
821  v = Cudd_Regular(node)->index; /* either yi or zi */
822  if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
823  Cudd_Ref(f1);
824  Cudd_Ref(f0);
825  Cudd_Ref(fd);
826 
827  b1 = cuddMakeBddFromZddCover(dd, f1);
828  if (!b1) {
829  Cudd_RecursiveDerefZdd(dd, f1);
830  Cudd_RecursiveDerefZdd(dd, f0);
831  Cudd_RecursiveDerefZdd(dd, fd);
832  return(NULL);
833  }
834  Cudd_Ref(b1);
835  b0 = cuddMakeBddFromZddCover(dd, f0);
836  if (!b0) {
837  Cudd_RecursiveDerefZdd(dd, f1);
838  Cudd_RecursiveDerefZdd(dd, f0);
839  Cudd_RecursiveDerefZdd(dd, fd);
840  Cudd_RecursiveDeref(dd, b1);
841  return(NULL);
842  }
843  Cudd_Ref(b0);
844  Cudd_RecursiveDerefZdd(dd, f1);
845  Cudd_RecursiveDerefZdd(dd, f0);
846  if (fd != dd->zero) {
847  bd = cuddMakeBddFromZddCover(dd, fd);
848  if (!bd) {
849  Cudd_RecursiveDerefZdd(dd, fd);
850  Cudd_RecursiveDeref(dd, b1);
851  Cudd_RecursiveDeref(dd, b0);
852  return(NULL);
853  }
854  Cudd_Ref(bd);
855  Cudd_RecursiveDerefZdd(dd, fd);
856 
857  T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
858  if (!T) {
859  Cudd_RecursiveDeref(dd, b1);
860  Cudd_RecursiveDeref(dd, b0);
861  Cudd_RecursiveDeref(dd, bd);
862  return(NULL);
863  }
864  T = Cudd_NotCond(T, T != NULL);
865  Cudd_Ref(T);
866  Cudd_RecursiveDeref(dd, b1);
867  E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
868  if (!E) {
869  Cudd_RecursiveDeref(dd, b0);
870  Cudd_RecursiveDeref(dd, bd);
871  Cudd_RecursiveDeref(dd, T);
872  return(NULL);
873  }
874  E = Cudd_NotCond(E, E != NULL);
875  Cudd_Ref(E);
876  Cudd_RecursiveDeref(dd, b0);
877  Cudd_RecursiveDeref(dd, bd);
878  }
879  else {
880  Cudd_RecursiveDerefZdd(dd, fd);
881  T = b1;
882  E = b0;
883  }
884 
885  if (Cudd_IsComplement(T)) {
886  neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
887  if (!neW) {
888  Cudd_RecursiveDeref(dd, T);
889  Cudd_RecursiveDeref(dd, E);
890  return(NULL);
891  }
892  neW = Cudd_Not(neW);
893  }
894  else {
895  neW = cuddUniqueInterIVO(dd, v / 2, T, E);
896  if (!neW) {
897  Cudd_RecursiveDeref(dd, T);
898  Cudd_RecursiveDeref(dd, E);
899  return(NULL);
900  }
901  }
902  Cudd_Ref(neW);
903  Cudd_RecursiveDeref(dd, T);
904  Cudd_RecursiveDeref(dd, E);
905 
906  cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
907  Cudd_Deref(neW);
908  return(neW);
909 
910 } /* end of cuddMakeBddFromZddCover */
911 
912 
913 /*---------------------------------------------------------------------------*/
914 /* Definition of static functions */
915 /*---------------------------------------------------------------------------*/
916 
917 
918 ABC_NAMESPACE_IMPL_END
919 
cuddZddGetNodeIVO
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
Definition: cuddTable.c:1074
cuddCacheLookup2Zdd
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:610
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
exit
VOID_HACK exit()
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
Cudd_T
#define Cudd_T(node)
Definition: cudd.h:440
Cudd_E
#define Cudd_E(node)
Definition: cudd.h:455
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
b1
#define b1
Definition: extraBdd.h:76
DdManager::zero
DdNode * zero
Definition: cuddInt.h:346
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DD_CTFP
DdNode *(* DD_CTFP)(DdManager *, DdNode *, DdNode *)
Definition: cudd.h:321
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:800
DD_UNUSED
static ABC_NAMESPACE_IMPL_START char rcsid[] DD_UNUSED
Definition: cuddZddIsop.c:91
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
util_hack.h
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:234
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
DdManager::reordered
int reordered
Definition: cuddInt.h:409
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
one
static DdNode * one
Definition: cuddDecomp.c:112
cuddUniqueInterIVO
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1304
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cudd_zddIsop
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:136
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddZddGetCofactors3
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Definition: cuddZddFuncs.c:1360
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cudd_MakeBddFromZddCover
DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:203
b0
#define b0
Definition: extraBdd.h:75
DdManager::one
DdNode * one
Definition: cuddInt.h:345
cuddBddIsop
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:575
DdManager::autoDynZ
int autoDynZ
Definition: cuddInt.h:417
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddIsop
DdNode * Cudd_bddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:174
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
DdManager::perm
int * perm
Definition: cuddInt.h:386
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
zero
static DdNode * zero
Definition: cuddApa.c:100
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927