abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddZddFuncs.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddZddFuncs.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Functions to manipulate covers represented as ZDDs.]
8 
9  Description [External procedures included in this module:
10  <ul>
11  <li> Cudd_zddProduct();
12  <li> Cudd_zddUnateProduct();
13  <li> Cudd_zddWeakDiv();
14  <li> Cudd_zddWeakDivF();
15  <li> Cudd_zddDivide();
16  <li> Cudd_zddDivideF();
17  <li> Cudd_zddComplement();
18  </ul>
19  Internal procedures included in this module:
20  <ul>
21  <li> cuddZddProduct();
22  <li> cuddZddUnateProduct();
23  <li> cuddZddWeakDiv();
24  <li> cuddZddWeakDivF();
25  <li> cuddZddDivide();
26  <li> cuddZddDivideF();
27  <li> cuddZddGetCofactors3()
28  <li> cuddZddGetCofactors2()
29  <li> cuddZddComplement();
30  <li> cuddZddGetPosVarIndex();
31  <li> cuddZddGetNegVarIndex();
32  <li> cuddZddGetPosVarLevel();
33  <li> cuddZddGetNegVarLevel();
34  </ul>
35  Static procedures included in this module:
36  <ul>
37  </ul>
38  ]
39 
40  SeeAlso []
41 
42  Author [In-Ho Moon]
43 
44  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
45 
46  All rights reserved.
47 
48  Redistribution and use in source and binary forms, with or without
49  modification, are permitted provided that the following conditions
50  are met:
51 
52  Redistributions of source code must retain the above copyright
53  notice, this list of conditions and the following disclaimer.
54 
55  Redistributions in binary form must reproduce the above copyright
56  notice, this list of conditions and the following disclaimer in the
57  documentation and/or other materials provided with the distribution.
58 
59  Neither the name of the University of Colorado nor the names of its
60  contributors may be used to endorse or promote products derived from
61  this software without specific prior written permission.
62 
63  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
64  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
65  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
66  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
67  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
68  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
69  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
70  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
71  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
72  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
73  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
74  POSSIBILITY OF SUCH DAMAGE.]
75 
76 ******************************************************************************/
77 
78 #include "misc/util/util_hack.h"
79 #include "cuddInt.h"
80 
81 ABC_NAMESPACE_IMPL_START
82 
83 
84 
85 /*---------------------------------------------------------------------------*/
86 /* Constant declarations */
87 /*---------------------------------------------------------------------------*/
88 
89 
90 /*---------------------------------------------------------------------------*/
91 /* Stucture declarations */
92 /*---------------------------------------------------------------------------*/
93 
94 
95 /*---------------------------------------------------------------------------*/
96 /* Type declarations */
97 /*---------------------------------------------------------------------------*/
98 
99 
100 /*---------------------------------------------------------------------------*/
101 /* Variable declarations */
102 /*---------------------------------------------------------------------------*/
103 
104 #ifndef lint
105 static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.16 2008/04/25 07:39:33 fabio Exp $";
106 #endif
107 
108 /*---------------------------------------------------------------------------*/
109 /* Macro declarations */
110 /*---------------------------------------------------------------------------*/
111 
112 
113 /**AutomaticStart*************************************************************/
114 
115 /*---------------------------------------------------------------------------*/
116 /* Static function prototypes */
117 /*---------------------------------------------------------------------------*/
118 
119 
120 /**AutomaticEnd***************************************************************/
121 
122 
123 /*---------------------------------------------------------------------------*/
124 /* Definition of exported functions */
125 /*---------------------------------------------------------------------------*/
126 
127 
128 /**Function********************************************************************
129 
130  Synopsis [Computes the product of two covers represented by ZDDs.]
131 
132  Description [Computes the product of two covers represented by
133  ZDDs. The result is also a ZDD. Returns a pointer to the result if
134  successful; NULL otherwise. The covers on which Cudd_zddProduct
135  operates use two ZDD variables for each function variable (one ZDD
136  variable for each literal of the variable). Those two ZDD variables
137  should be adjacent in the order.]
138 
139  SideEffects [None]
140 
141  SeeAlso [Cudd_zddUnateProduct]
142 
143 ******************************************************************************/
144 DdNode *
145 Cudd_zddProduct(
146  DdManager * dd,
147  DdNode * f,
148  DdNode * g)
149 {
150  DdNode *res;
151 
152  do {
153  dd->reordered = 0;
154  res = cuddZddProduct(dd, f, g);
155  } while (dd->reordered == 1);
156  return(res);
157 
158 } /* end of Cudd_zddProduct */
159 
160 
161 /**Function********************************************************************
162 
163  Synopsis [Computes the product of two unate covers.]
164 
165  Description [Computes the product of two unate covers represented as
166  ZDDs. Unate covers use one ZDD variable for each BDD
167  variable. Returns a pointer to the result if successful; NULL
168  otherwise.]
169 
170  SideEffects [None]
171 
172  SeeAlso [Cudd_zddProduct]
173 
174 ******************************************************************************/
175 DdNode *
176 Cudd_zddUnateProduct(
177  DdManager * dd,
178  DdNode * f,
179  DdNode * g)
180 {
181  DdNode *res;
182 
183  do {
184  dd->reordered = 0;
185  res = cuddZddUnateProduct(dd, f, g);
186  } while (dd->reordered == 1);
187  return(res);
188 
189 } /* end of Cudd_zddUnateProduct */
190 
191 
192 /**Function********************************************************************
193 
194  Synopsis [Applies weak division to two covers.]
195 
196  Description [Applies weak division to two ZDDs representing two
197  covers. Returns a pointer to the ZDD representing the result if
198  successful; NULL otherwise. The result of weak division depends on
199  the variable order. The covers on which Cudd_zddWeakDiv operates use
200  two ZDD variables for each function variable (one ZDD variable for
201  each literal of the variable). Those two ZDD variables should be
202  adjacent in the order.]
203 
204  SideEffects [None]
205 
206  SeeAlso [Cudd_zddDivide]
207 
208 ******************************************************************************/
209 DdNode *
210 Cudd_zddWeakDiv(
211  DdManager * dd,
212  DdNode * f,
213  DdNode * g)
214 {
215  DdNode *res;
216 
217  do {
218  dd->reordered = 0;
219  res = cuddZddWeakDiv(dd, f, g);
220  } while (dd->reordered == 1);
221  return(res);
222 
223 } /* end of Cudd_zddWeakDiv */
224 
225 
226 /**Function********************************************************************
227 
228  Synopsis [Computes the quotient of two unate covers.]
229 
230  Description [Computes the quotient of two unate covers represented
231  by ZDDs. Unate covers use one ZDD variable for each BDD
232  variable. Returns a pointer to the resulting ZDD if successful; NULL
233  otherwise.]
234 
235  SideEffects [None]
236 
237  SeeAlso [Cudd_zddWeakDiv]
238 
239 ******************************************************************************/
240 DdNode *
241 Cudd_zddDivide(
242  DdManager * dd,
243  DdNode * f,
244  DdNode * g)
245 {
246  DdNode *res;
247 
248  do {
249  dd->reordered = 0;
250  res = cuddZddDivide(dd, f, g);
251  } while (dd->reordered == 1);
252  return(res);
253 
254 } /* end of Cudd_zddDivide */
255 
256 
257 /**Function********************************************************************
258 
259  Synopsis [Modified version of Cudd_zddWeakDiv.]
260 
261  Description [Modified version of Cudd_zddWeakDiv. This function may
262  disappear in future releases.]
263 
264  SideEffects [None]
265 
266  SeeAlso [Cudd_zddWeakDiv]
267 
268 ******************************************************************************/
269 DdNode *
270 Cudd_zddWeakDivF(
271  DdManager * dd,
272  DdNode * f,
273  DdNode * g)
274 {
275  DdNode *res;
276 
277  do {
278  dd->reordered = 0;
279  res = cuddZddWeakDivF(dd, f, g);
280  } while (dd->reordered == 1);
281  return(res);
282 
283 } /* end of Cudd_zddWeakDivF */
284 
285 
286 /**Function********************************************************************
287 
288  Synopsis [Modified version of Cudd_zddDivide.]
289 
290  Description [Modified version of Cudd_zddDivide. This function may
291  disappear in future releases.]
292 
293  SideEffects [None]
294 
295  SeeAlso []
296 
297 ******************************************************************************/
298 DdNode *
299 Cudd_zddDivideF(
300  DdManager * dd,
301  DdNode * f,
302  DdNode * g)
303 {
304  DdNode *res;
305 
306  do {
307  dd->reordered = 0;
308  res = cuddZddDivideF(dd, f, g);
309  } while (dd->reordered == 1);
310  return(res);
311 
312 } /* end of Cudd_zddDivideF */
313 
314 
315 /**Function********************************************************************
316 
317  Synopsis [Computes a complement cover for a ZDD node.]
318 
319  Description [Computes a complement cover for a ZDD node. For lack of a
320  better method, we first extract the function BDD from the ZDD cover,
321  then make the complement of the ZDD cover from the complement of the
322  BDD node by using ISOP. Returns a pointer to the resulting cover if
323  successful; NULL otherwise. The result depends on current variable
324  order.]
325 
326  SideEffects [The result depends on current variable order.]
327 
328  SeeAlso []
329 
330 ******************************************************************************/
331 DdNode *
332 Cudd_zddComplement(
333  DdManager *dd,
334  DdNode *node)
335 {
336  DdNode *b, *isop, *zdd_I;
337 
338  /* Check cache */
339  zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
340  if (zdd_I)
341  return(zdd_I);
342 
343  b = Cudd_MakeBddFromZddCover(dd, node);
344  if (!b)
345  return(NULL);
346  Cudd_Ref(b);
347  isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
348  if (!isop) {
349  Cudd_RecursiveDeref(dd, b);
350  return(NULL);
351  }
352  Cudd_Ref(isop);
353  Cudd_Ref(zdd_I);
354  Cudd_RecursiveDeref(dd, b);
355  Cudd_RecursiveDeref(dd, isop);
356 
357  cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
358  Cudd_Deref(zdd_I);
359  return(zdd_I);
360 } /* end of Cudd_zddComplement */
361 
362 
363 /*---------------------------------------------------------------------------*/
364 /* Definition of internal functions */
365 /*---------------------------------------------------------------------------*/
366 
367 
368 /**Function********************************************************************
369 
370  Synopsis [Performs the recursive step of Cudd_zddProduct.]
371 
372  Description []
373 
374  SideEffects [None]
375 
376  SeeAlso [Cudd_zddProduct]
377 
378 ******************************************************************************/
379 DdNode *
380 cuddZddProduct(
381  DdManager * dd,
382  DdNode * f,
383  DdNode * g)
384 {
385  int v, top_f, top_g;
386  DdNode *tmp, *term1, *term2, *term3;
387  DdNode *f0, *f1, *fd, *g0, *g1, *gd;
388  DdNode *R0, *R1, *Rd, *N0, *N1;
389  DdNode *r;
390  DdNode *one = DD_ONE(dd);
391  DdNode *zero = DD_ZERO(dd);
392  int flag;
393  int pv, nv;
394 
395  statLine(dd);
396  if (f == zero || g == zero)
397  return(zero);
398  if (f == one)
399  return(g);
400  if (g == one)
401  return(f);
402 
403  top_f = dd->permZ[f->index];
404  top_g = dd->permZ[g->index];
405 
406  if (top_f > top_g)
407  return(cuddZddProduct(dd, g, f));
408 
409  /* Check cache */
410  r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g);
411  if (r)
412  return(r);
413 
414  v = f->index; /* either yi or zi */
415  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
416  if (flag == 1)
417  return(NULL);
418  Cudd_Ref(f1);
419  Cudd_Ref(f0);
420  Cudd_Ref(fd);
421  flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
422  if (flag == 1) {
423  Cudd_RecursiveDerefZdd(dd, f1);
424  Cudd_RecursiveDerefZdd(dd, f0);
425  Cudd_RecursiveDerefZdd(dd, fd);
426  return(NULL);
427  }
428  Cudd_Ref(g1);
429  Cudd_Ref(g0);
430  Cudd_Ref(gd);
431  pv = cuddZddGetPosVarIndex(dd, v);
432  nv = cuddZddGetNegVarIndex(dd, v);
433 
434  Rd = cuddZddProduct(dd, fd, gd);
435  if (Rd == NULL) {
436  Cudd_RecursiveDerefZdd(dd, f1);
437  Cudd_RecursiveDerefZdd(dd, f0);
438  Cudd_RecursiveDerefZdd(dd, fd);
439  Cudd_RecursiveDerefZdd(dd, g1);
440  Cudd_RecursiveDerefZdd(dd, g0);
441  Cudd_RecursiveDerefZdd(dd, gd);
442  return(NULL);
443  }
444  Cudd_Ref(Rd);
445 
446  term1 = cuddZddProduct(dd, f0, g0);
447  if (term1 == NULL) {
448  Cudd_RecursiveDerefZdd(dd, f1);
449  Cudd_RecursiveDerefZdd(dd, f0);
450  Cudd_RecursiveDerefZdd(dd, fd);
451  Cudd_RecursiveDerefZdd(dd, g1);
452  Cudd_RecursiveDerefZdd(dd, g0);
453  Cudd_RecursiveDerefZdd(dd, gd);
454  Cudd_RecursiveDerefZdd(dd, Rd);
455  return(NULL);
456  }
457  Cudd_Ref(term1);
458  term2 = cuddZddProduct(dd, f0, gd);
459  if (term2 == NULL) {
460  Cudd_RecursiveDerefZdd(dd, f1);
461  Cudd_RecursiveDerefZdd(dd, f0);
462  Cudd_RecursiveDerefZdd(dd, fd);
463  Cudd_RecursiveDerefZdd(dd, g1);
464  Cudd_RecursiveDerefZdd(dd, g0);
465  Cudd_RecursiveDerefZdd(dd, gd);
466  Cudd_RecursiveDerefZdd(dd, Rd);
467  Cudd_RecursiveDerefZdd(dd, term1);
468  return(NULL);
469  }
470  Cudd_Ref(term2);
471  term3 = cuddZddProduct(dd, fd, g0);
472  if (term3 == NULL) {
473  Cudd_RecursiveDerefZdd(dd, f1);
474  Cudd_RecursiveDerefZdd(dd, f0);
475  Cudd_RecursiveDerefZdd(dd, fd);
476  Cudd_RecursiveDerefZdd(dd, g1);
477  Cudd_RecursiveDerefZdd(dd, g0);
478  Cudd_RecursiveDerefZdd(dd, gd);
479  Cudd_RecursiveDerefZdd(dd, Rd);
480  Cudd_RecursiveDerefZdd(dd, term1);
481  Cudd_RecursiveDerefZdd(dd, term2);
482  return(NULL);
483  }
484  Cudd_Ref(term3);
485  Cudd_RecursiveDerefZdd(dd, f0);
486  Cudd_RecursiveDerefZdd(dd, g0);
487  tmp = cuddZddUnion(dd, term1, term2);
488  if (tmp == NULL) {
489  Cudd_RecursiveDerefZdd(dd, f1);
490  Cudd_RecursiveDerefZdd(dd, fd);
491  Cudd_RecursiveDerefZdd(dd, g1);
492  Cudd_RecursiveDerefZdd(dd, gd);
493  Cudd_RecursiveDerefZdd(dd, Rd);
494  Cudd_RecursiveDerefZdd(dd, term1);
495  Cudd_RecursiveDerefZdd(dd, term2);
496  Cudd_RecursiveDerefZdd(dd, term3);
497  return(NULL);
498  }
499  Cudd_Ref(tmp);
500  Cudd_RecursiveDerefZdd(dd, term1);
501  Cudd_RecursiveDerefZdd(dd, term2);
502  R0 = cuddZddUnion(dd, tmp, term3);
503  if (R0 == NULL) {
504  Cudd_RecursiveDerefZdd(dd, f1);
505  Cudd_RecursiveDerefZdd(dd, fd);
506  Cudd_RecursiveDerefZdd(dd, g1);
507  Cudd_RecursiveDerefZdd(dd, gd);
508  Cudd_RecursiveDerefZdd(dd, Rd);
509  Cudd_RecursiveDerefZdd(dd, term3);
510  Cudd_RecursiveDerefZdd(dd, tmp);
511  return(NULL);
512  }
513  Cudd_Ref(R0);
514  Cudd_RecursiveDerefZdd(dd, tmp);
515  Cudd_RecursiveDerefZdd(dd, term3);
516  N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */
517  if (N0 == NULL) {
518  Cudd_RecursiveDerefZdd(dd, f1);
519  Cudd_RecursiveDerefZdd(dd, fd);
520  Cudd_RecursiveDerefZdd(dd, g1);
521  Cudd_RecursiveDerefZdd(dd, gd);
522  Cudd_RecursiveDerefZdd(dd, Rd);
523  Cudd_RecursiveDerefZdd(dd, R0);
524  return(NULL);
525  }
526  Cudd_Ref(N0);
527  Cudd_RecursiveDerefZdd(dd, R0);
528  Cudd_RecursiveDerefZdd(dd, Rd);
529 
530  term1 = cuddZddProduct(dd, f1, g1);
531  if (term1 == NULL) {
532  Cudd_RecursiveDerefZdd(dd, f1);
533  Cudd_RecursiveDerefZdd(dd, fd);
534  Cudd_RecursiveDerefZdd(dd, g1);
535  Cudd_RecursiveDerefZdd(dd, gd);
536  Cudd_RecursiveDerefZdd(dd, N0);
537  return(NULL);
538  }
539  Cudd_Ref(term1);
540  term2 = cuddZddProduct(dd, f1, gd);
541  if (term2 == NULL) {
542  Cudd_RecursiveDerefZdd(dd, f1);
543  Cudd_RecursiveDerefZdd(dd, fd);
544  Cudd_RecursiveDerefZdd(dd, g1);
545  Cudd_RecursiveDerefZdd(dd, gd);
546  Cudd_RecursiveDerefZdd(dd, N0);
547  Cudd_RecursiveDerefZdd(dd, term1);
548  return(NULL);
549  }
550  Cudd_Ref(term2);
551  term3 = cuddZddProduct(dd, fd, g1);
552  if (term3 == NULL) {
553  Cudd_RecursiveDerefZdd(dd, f1);
554  Cudd_RecursiveDerefZdd(dd, fd);
555  Cudd_RecursiveDerefZdd(dd, g1);
556  Cudd_RecursiveDerefZdd(dd, gd);
557  Cudd_RecursiveDerefZdd(dd, N0);
558  Cudd_RecursiveDerefZdd(dd, term1);
559  Cudd_RecursiveDerefZdd(dd, term2);
560  return(NULL);
561  }
562  Cudd_Ref(term3);
563  Cudd_RecursiveDerefZdd(dd, f1);
564  Cudd_RecursiveDerefZdd(dd, g1);
565  Cudd_RecursiveDerefZdd(dd, fd);
566  Cudd_RecursiveDerefZdd(dd, gd);
567  tmp = cuddZddUnion(dd, term1, term2);
568  if (tmp == NULL) {
569  Cudd_RecursiveDerefZdd(dd, N0);
570  Cudd_RecursiveDerefZdd(dd, term1);
571  Cudd_RecursiveDerefZdd(dd, term2);
572  Cudd_RecursiveDerefZdd(dd, term3);
573  return(NULL);
574  }
575  Cudd_Ref(tmp);
576  Cudd_RecursiveDerefZdd(dd, term1);
577  Cudd_RecursiveDerefZdd(dd, term2);
578  R1 = cuddZddUnion(dd, tmp, term3);
579  if (R1 == NULL) {
580  Cudd_RecursiveDerefZdd(dd, N0);
581  Cudd_RecursiveDerefZdd(dd, term3);
582  Cudd_RecursiveDerefZdd(dd, tmp);
583  return(NULL);
584  }
585  Cudd_Ref(R1);
586  Cudd_RecursiveDerefZdd(dd, tmp);
587  Cudd_RecursiveDerefZdd(dd, term3);
588  N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */
589  if (N1 == NULL) {
590  Cudd_RecursiveDerefZdd(dd, N0);
591  Cudd_RecursiveDerefZdd(dd, R1);
592  return(NULL);
593  }
594  Cudd_Ref(N1);
595  Cudd_RecursiveDerefZdd(dd, R1);
596  Cudd_RecursiveDerefZdd(dd, N0);
597 
598  cuddCacheInsert2(dd, cuddZddProduct, f, g, N1);
599  Cudd_Deref(N1);
600  return(N1);
601 
602 } /* end of cuddZddProduct */
603 
604 
605 /**Function********************************************************************
606 
607  Synopsis [Performs the recursive step of Cudd_zddUnateProduct.]
608 
609  Description []
610 
611  SideEffects [None]
612 
613  SeeAlso [Cudd_zddUnateProduct]
614 
615 ******************************************************************************/
616 DdNode *
617 cuddZddUnateProduct(
618  DdManager * dd,
619  DdNode * f,
620  DdNode * g)
621 {
622  int v, top_f, top_g;
623  DdNode *term1, *term2, *term3, *term4;
624  DdNode *sum1, *sum2;
625  DdNode *f0, *f1, *g0, *g1;
626  DdNode *r;
627  DdNode *one = DD_ONE(dd);
628  DdNode *zero = DD_ZERO(dd);
629  int flag;
630 
631  statLine(dd);
632  if (f == zero || g == zero)
633  return(zero);
634  if (f == one)
635  return(g);
636  if (g == one)
637  return(f);
638 
639  top_f = dd->permZ[f->index];
640  top_g = dd->permZ[g->index];
641 
642  if (top_f > top_g)
643  return(cuddZddUnateProduct(dd, g, f));
644 
645  /* Check cache */
646  r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g);
647  if (r)
648  return(r);
649 
650  v = f->index; /* either yi or zi */
651  flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
652  if (flag == 1)
653  return(NULL);
654  Cudd_Ref(f1);
655  Cudd_Ref(f0);
656  flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);
657  if (flag == 1) {
658  Cudd_RecursiveDerefZdd(dd, f1);
659  Cudd_RecursiveDerefZdd(dd, f0);
660  return(NULL);
661  }
662  Cudd_Ref(g1);
663  Cudd_Ref(g0);
664 
665  term1 = cuddZddUnateProduct(dd, f1, g1);
666  if (term1 == NULL) {
667  Cudd_RecursiveDerefZdd(dd, f1);
668  Cudd_RecursiveDerefZdd(dd, f0);
669  Cudd_RecursiveDerefZdd(dd, g1);
670  Cudd_RecursiveDerefZdd(dd, g0);
671  return(NULL);
672  }
673  Cudd_Ref(term1);
674  term2 = cuddZddUnateProduct(dd, f1, g0);
675  if (term2 == NULL) {
676  Cudd_RecursiveDerefZdd(dd, f1);
677  Cudd_RecursiveDerefZdd(dd, f0);
678  Cudd_RecursiveDerefZdd(dd, g1);
679  Cudd_RecursiveDerefZdd(dd, g0);
680  Cudd_RecursiveDerefZdd(dd, term1);
681  return(NULL);
682  }
683  Cudd_Ref(term2);
684  term3 = cuddZddUnateProduct(dd, f0, g1);
685  if (term3 == NULL) {
686  Cudd_RecursiveDerefZdd(dd, f1);
687  Cudd_RecursiveDerefZdd(dd, f0);
688  Cudd_RecursiveDerefZdd(dd, g1);
689  Cudd_RecursiveDerefZdd(dd, g0);
690  Cudd_RecursiveDerefZdd(dd, term1);
691  Cudd_RecursiveDerefZdd(dd, term2);
692  return(NULL);
693  }
694  Cudd_Ref(term3);
695  term4 = cuddZddUnateProduct(dd, f0, g0);
696  if (term4 == NULL) {
697  Cudd_RecursiveDerefZdd(dd, f1);
698  Cudd_RecursiveDerefZdd(dd, f0);
699  Cudd_RecursiveDerefZdd(dd, g1);
700  Cudd_RecursiveDerefZdd(dd, g0);
701  Cudd_RecursiveDerefZdd(dd, term1);
702  Cudd_RecursiveDerefZdd(dd, term2);
703  Cudd_RecursiveDerefZdd(dd, term3);
704  return(NULL);
705  }
706  Cudd_Ref(term4);
707  Cudd_RecursiveDerefZdd(dd, f1);
708  Cudd_RecursiveDerefZdd(dd, f0);
709  Cudd_RecursiveDerefZdd(dd, g1);
710  Cudd_RecursiveDerefZdd(dd, g0);
711  sum1 = cuddZddUnion(dd, term1, term2);
712  if (sum1 == NULL) {
713  Cudd_RecursiveDerefZdd(dd, term1);
714  Cudd_RecursiveDerefZdd(dd, term2);
715  Cudd_RecursiveDerefZdd(dd, term3);
716  Cudd_RecursiveDerefZdd(dd, term4);
717  return(NULL);
718  }
719  Cudd_Ref(sum1);
720  Cudd_RecursiveDerefZdd(dd, term1);
721  Cudd_RecursiveDerefZdd(dd, term2);
722  sum2 = cuddZddUnion(dd, sum1, term3);
723  if (sum2 == NULL) {
724  Cudd_RecursiveDerefZdd(dd, term3);
725  Cudd_RecursiveDerefZdd(dd, term4);
726  Cudd_RecursiveDerefZdd(dd, sum1);
727  return(NULL);
728  }
729  Cudd_Ref(sum2);
730  Cudd_RecursiveDerefZdd(dd, sum1);
731  Cudd_RecursiveDerefZdd(dd, term3);
732  r = cuddZddGetNode(dd, v, sum2, term4);
733  if (r == NULL) {
734  Cudd_RecursiveDerefZdd(dd, term4);
735  Cudd_RecursiveDerefZdd(dd, sum2);
736  return(NULL);
737  }
738  Cudd_Ref(r);
739  Cudd_RecursiveDerefZdd(dd, sum2);
740  Cudd_RecursiveDerefZdd(dd, term4);
741 
742  cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r);
743  Cudd_Deref(r);
744  return(r);
745 
746 } /* end of cuddZddUnateProduct */
747 
748 
749 /**Function********************************************************************
750 
751  Synopsis [Performs the recursive step of Cudd_zddWeakDiv.]
752 
753  Description []
754 
755  SideEffects [None]
756 
757  SeeAlso [Cudd_zddWeakDiv]
758 
759 ******************************************************************************/
760 DdNode *
761 cuddZddWeakDiv(
762  DdManager * dd,
763  DdNode * f,
764  DdNode * g)
765 {
766  int v;
767  DdNode *one = DD_ONE(dd);
768  DdNode *zero = DD_ZERO(dd);
769  DdNode *f0, *f1, *fd, *g0, *g1, *gd;
770  DdNode *q, *tmp;
771  DdNode *r;
772  int flag;
773 
774  statLine(dd);
775  if (g == one)
776  return(f);
777  if (f == zero || f == one)
778  return(zero);
779  if (f == g)
780  return(one);
781 
782  /* Check cache. */
783  r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g);
784  if (r)
785  return(r);
786 
787  v = g->index;
788 
789  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
790  if (flag == 1)
791  return(NULL);
792  Cudd_Ref(f1);
793  Cudd_Ref(f0);
794  Cudd_Ref(fd);
795  flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
796  if (flag == 1) {
797  Cudd_RecursiveDerefZdd(dd, f1);
798  Cudd_RecursiveDerefZdd(dd, f0);
799  Cudd_RecursiveDerefZdd(dd, fd);
800  return(NULL);
801  }
802  Cudd_Ref(g1);
803  Cudd_Ref(g0);
804  Cudd_Ref(gd);
805 
806  q = g;
807 
808  if (g0 != zero) {
809  q = cuddZddWeakDiv(dd, f0, g0);
810  if (q == NULL) {
811  Cudd_RecursiveDerefZdd(dd, f1);
812  Cudd_RecursiveDerefZdd(dd, f0);
813  Cudd_RecursiveDerefZdd(dd, fd);
814  Cudd_RecursiveDerefZdd(dd, g1);
815  Cudd_RecursiveDerefZdd(dd, g0);
816  Cudd_RecursiveDerefZdd(dd, gd);
817  return(NULL);
818  }
819  Cudd_Ref(q);
820  }
821  else
822  Cudd_Ref(q);
823  Cudd_RecursiveDerefZdd(dd, f0);
824  Cudd_RecursiveDerefZdd(dd, g0);
825 
826  if (q == zero) {
827  Cudd_RecursiveDerefZdd(dd, f1);
828  Cudd_RecursiveDerefZdd(dd, g1);
829  Cudd_RecursiveDerefZdd(dd, fd);
830  Cudd_RecursiveDerefZdd(dd, gd);
831  cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
832  Cudd_Deref(q);
833  return(zero);
834  }
835 
836  if (g1 != zero) {
837  Cudd_RecursiveDerefZdd(dd, q);
838  tmp = cuddZddWeakDiv(dd, f1, g1);
839  if (tmp == NULL) {
840  Cudd_RecursiveDerefZdd(dd, f1);
841  Cudd_RecursiveDerefZdd(dd, g1);
842  Cudd_RecursiveDerefZdd(dd, fd);
843  Cudd_RecursiveDerefZdd(dd, gd);
844  return(NULL);
845  }
846  Cudd_Ref(tmp);
847  Cudd_RecursiveDerefZdd(dd, f1);
848  Cudd_RecursiveDerefZdd(dd, g1);
849  if (q == g)
850  q = tmp;
851  else {
852  q = cuddZddIntersect(dd, q, tmp);
853  if (q == NULL) {
854  Cudd_RecursiveDerefZdd(dd, fd);
855  Cudd_RecursiveDerefZdd(dd, gd);
856  return(NULL);
857  }
858  Cudd_Ref(q);
859  Cudd_RecursiveDerefZdd(dd, tmp);
860  }
861  }
862  else {
863  Cudd_RecursiveDerefZdd(dd, f1);
864  Cudd_RecursiveDerefZdd(dd, g1);
865  }
866 
867  if (q == zero) {
868  Cudd_RecursiveDerefZdd(dd, fd);
869  Cudd_RecursiveDerefZdd(dd, gd);
870  cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
871  Cudd_Deref(q);
872  return(zero);
873  }
874 
875  if (gd != zero) {
876  Cudd_RecursiveDerefZdd(dd, q);
877  tmp = cuddZddWeakDiv(dd, fd, gd);
878  if (tmp == NULL) {
879  Cudd_RecursiveDerefZdd(dd, fd);
880  Cudd_RecursiveDerefZdd(dd, gd);
881  return(NULL);
882  }
883  Cudd_Ref(tmp);
884  Cudd_RecursiveDerefZdd(dd, fd);
885  Cudd_RecursiveDerefZdd(dd, gd);
886  if (q == g)
887  q = tmp;
888  else {
889  q = cuddZddIntersect(dd, q, tmp);
890  if (q == NULL) {
891  Cudd_RecursiveDerefZdd(dd, tmp);
892  return(NULL);
893  }
894  Cudd_Ref(q);
895  Cudd_RecursiveDerefZdd(dd, tmp);
896  }
897  }
898  else {
899  Cudd_RecursiveDerefZdd(dd, fd);
900  Cudd_RecursiveDerefZdd(dd, gd);
901  }
902 
903  cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q);
904  Cudd_Deref(q);
905  return(q);
906 
907 } /* end of cuddZddWeakDiv */
908 
909 
910 /**Function********************************************************************
911 
912  Synopsis [Performs the recursive step of Cudd_zddWeakDivF.]
913 
914  Description []
915 
916  SideEffects [None]
917 
918  SeeAlso [Cudd_zddWeakDivF]
919 
920 ******************************************************************************/
921 DdNode *
922 cuddZddWeakDivF(
923  DdManager * dd,
924  DdNode * f,
925  DdNode * g)
926 {
927  int v, top_f, top_g, vf, vg;
928  DdNode *one = DD_ONE(dd);
929  DdNode *zero = DD_ZERO(dd);
930  DdNode *f0, *f1, *fd, *g0, *g1, *gd;
931  DdNode *q, *tmp;
932  DdNode *r;
933  DdNode *term1, *term0, *termd;
934  int flag;
935  int pv, nv;
936 
937  statLine(dd);
938  if (g == one)
939  return(f);
940  if (f == zero || f == one)
941  return(zero);
942  if (f == g)
943  return(one);
944 
945  /* Check cache. */
946  r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g);
947  if (r)
948  return(r);
949 
950  top_f = dd->permZ[f->index];
951  top_g = dd->permZ[g->index];
952  vf = top_f >> 1;
953  vg = top_g >> 1;
954  v = ddMin(top_f, top_g);
955 
956  if (v == top_f && vf < vg) {
957  v = f->index;
958  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
959  if (flag == 1)
960  return(NULL);
961  Cudd_Ref(f1);
962  Cudd_Ref(f0);
963  Cudd_Ref(fd);
964 
965  pv = cuddZddGetPosVarIndex(dd, v);
966  nv = cuddZddGetNegVarIndex(dd, v);
967 
968  term1 = cuddZddWeakDivF(dd, f1, g);
969  if (term1 == NULL) {
970  Cudd_RecursiveDerefZdd(dd, f1);
971  Cudd_RecursiveDerefZdd(dd, f0);
972  Cudd_RecursiveDerefZdd(dd, fd);
973  return(NULL);
974  }
975  Cudd_Ref(term1);
976  Cudd_RecursiveDerefZdd(dd, f1);
977  term0 = cuddZddWeakDivF(dd, f0, g);
978  if (term0 == NULL) {
979  Cudd_RecursiveDerefZdd(dd, f0);
980  Cudd_RecursiveDerefZdd(dd, fd);
981  Cudd_RecursiveDerefZdd(dd, term1);
982  return(NULL);
983  }
984  Cudd_Ref(term0);
985  Cudd_RecursiveDerefZdd(dd, f0);
986  termd = cuddZddWeakDivF(dd, fd, g);
987  if (termd == NULL) {
988  Cudd_RecursiveDerefZdd(dd, fd);
989  Cudd_RecursiveDerefZdd(dd, term1);
990  Cudd_RecursiveDerefZdd(dd, term0);
991  return(NULL);
992  }
993  Cudd_Ref(termd);
994  Cudd_RecursiveDerefZdd(dd, fd);
995 
996  tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
997  if (tmp == NULL) {
998  Cudd_RecursiveDerefZdd(dd, term1);
999  Cudd_RecursiveDerefZdd(dd, term0);
1000  Cudd_RecursiveDerefZdd(dd, termd);
1001  return(NULL);
1002  }
1003  Cudd_Ref(tmp);
1004  Cudd_RecursiveDerefZdd(dd, term0);
1005  Cudd_RecursiveDerefZdd(dd, termd);
1006  q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
1007  if (q == NULL) {
1008  Cudd_RecursiveDerefZdd(dd, term1);
1009  Cudd_RecursiveDerefZdd(dd, tmp);
1010  return(NULL);
1011  }
1012  Cudd_Ref(q);
1013  Cudd_RecursiveDerefZdd(dd, term1);
1014  Cudd_RecursiveDerefZdd(dd, tmp);
1015 
1016  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
1017  Cudd_Deref(q);
1018  return(q);
1019  }
1020 
1021  if (v == top_f)
1022  v = f->index;
1023  else
1024  v = g->index;
1025 
1026  flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
1027  if (flag == 1)
1028  return(NULL);
1029  Cudd_Ref(f1);
1030  Cudd_Ref(f0);
1031  Cudd_Ref(fd);
1032  flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
1033  if (flag == 1) {
1034  Cudd_RecursiveDerefZdd(dd, f1);
1035  Cudd_RecursiveDerefZdd(dd, f0);
1036  Cudd_RecursiveDerefZdd(dd, fd);
1037  return(NULL);
1038  }
1039  Cudd_Ref(g1);
1040  Cudd_Ref(g0);
1041  Cudd_Ref(gd);
1042 
1043  q = g;
1044 
1045  if (g0 != zero) {
1046  q = cuddZddWeakDivF(dd, f0, g0);
1047  if (q == NULL) {
1048  Cudd_RecursiveDerefZdd(dd, f1);
1049  Cudd_RecursiveDerefZdd(dd, f0);
1050  Cudd_RecursiveDerefZdd(dd, fd);
1051  Cudd_RecursiveDerefZdd(dd, g1);
1052  Cudd_RecursiveDerefZdd(dd, g0);
1053  Cudd_RecursiveDerefZdd(dd, gd);
1054  return(NULL);
1055  }
1056  Cudd_Ref(q);
1057  }
1058  else
1059  Cudd_Ref(q);
1060  Cudd_RecursiveDerefZdd(dd, f0);
1061  Cudd_RecursiveDerefZdd(dd, g0);
1062 
1063  if (q == zero) {
1064  Cudd_RecursiveDerefZdd(dd, f1);
1065  Cudd_RecursiveDerefZdd(dd, g1);
1066  Cudd_RecursiveDerefZdd(dd, fd);
1067  Cudd_RecursiveDerefZdd(dd, gd);
1068  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
1069  Cudd_Deref(q);
1070  return(zero);
1071  }
1072 
1073  if (g1 != zero) {
1074  Cudd_RecursiveDerefZdd(dd, q);
1075  tmp = cuddZddWeakDivF(dd, f1, g1);
1076  if (tmp == NULL) {
1077  Cudd_RecursiveDerefZdd(dd, f1);
1078  Cudd_RecursiveDerefZdd(dd, g1);
1079  Cudd_RecursiveDerefZdd(dd, fd);
1080  Cudd_RecursiveDerefZdd(dd, gd);
1081  return(NULL);
1082  }
1083  Cudd_Ref(tmp);
1084  Cudd_RecursiveDerefZdd(dd, f1);
1085  Cudd_RecursiveDerefZdd(dd, g1);
1086  if (q == g)
1087  q = tmp;
1088  else {
1089  q = cuddZddIntersect(dd, q, tmp);
1090  if (q == NULL) {
1091  Cudd_RecursiveDerefZdd(dd, fd);
1092  Cudd_RecursiveDerefZdd(dd, gd);
1093  return(NULL);
1094  }
1095  Cudd_Ref(q);
1096  Cudd_RecursiveDerefZdd(dd, tmp);
1097  }
1098  }
1099  else {
1100  Cudd_RecursiveDerefZdd(dd, f1);
1101  Cudd_RecursiveDerefZdd(dd, g1);
1102  }
1103 
1104  if (q == zero) {
1105  Cudd_RecursiveDerefZdd(dd, fd);
1106  Cudd_RecursiveDerefZdd(dd, gd);
1107  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
1108  Cudd_Deref(q);
1109  return(zero);
1110  }
1111 
1112  if (gd != zero) {
1113  Cudd_RecursiveDerefZdd(dd, q);
1114  tmp = cuddZddWeakDivF(dd, fd, gd);
1115  if (tmp == NULL) {
1116  Cudd_RecursiveDerefZdd(dd, fd);
1117  Cudd_RecursiveDerefZdd(dd, gd);
1118  return(NULL);
1119  }
1120  Cudd_Ref(tmp);
1121  Cudd_RecursiveDerefZdd(dd, fd);
1122  Cudd_RecursiveDerefZdd(dd, gd);
1123  if (q == g)
1124  q = tmp;
1125  else {
1126  q = cuddZddIntersect(dd, q, tmp);
1127  if (q == NULL) {
1128  Cudd_RecursiveDerefZdd(dd, tmp);
1129  return(NULL);
1130  }
1131  Cudd_Ref(q);
1132  Cudd_RecursiveDerefZdd(dd, tmp);
1133  }
1134  }
1135  else {
1136  Cudd_RecursiveDerefZdd(dd, fd);
1137  Cudd_RecursiveDerefZdd(dd, gd);
1138  }
1139 
1140  cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
1141  Cudd_Deref(q);
1142  return(q);
1143 
1144 } /* end of cuddZddWeakDivF */
1145 
1146 
1147 /**Function********************************************************************
1148 
1149  Synopsis [Performs the recursive step of Cudd_zddDivide.]
1150 
1151  Description []
1152 
1153  SideEffects [None]
1154 
1155  SeeAlso [Cudd_zddDivide]
1156 
1157 ******************************************************************************/
1158 DdNode *
1159 cuddZddDivide(
1160  DdManager * dd,
1161  DdNode * f,
1162  DdNode * g)
1163 {
1164  int v;
1165  DdNode *one = DD_ONE(dd);
1166  DdNode *zero = DD_ZERO(dd);
1167  DdNode *f0, *f1, *g0, *g1;
1168  DdNode *q, *r, *tmp;
1169  int flag;
1170 
1171  statLine(dd);
1172  if (g == one)
1173  return(f);
1174  if (f == zero || f == one)
1175  return(zero);
1176  if (f == g)
1177  return(one);
1178 
1179  /* Check cache. */
1180  r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g);
1181  if (r)
1182  return(r);
1183 
1184  v = g->index;
1185 
1186  flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
1187  if (flag == 1)
1188  return(NULL);
1189  Cudd_Ref(f1);
1190  Cudd_Ref(f0);
1191  flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */
1192  if (flag == 1) {
1193  Cudd_RecursiveDerefZdd(dd, f1);
1194  Cudd_RecursiveDerefZdd(dd, f0);
1195  return(NULL);
1196  }
1197  Cudd_Ref(g1);
1198  Cudd_Ref(g0);
1199 
1200  r = cuddZddDivide(dd, f1, g1);
1201  if (r == NULL) {
1202  Cudd_RecursiveDerefZdd(dd, f1);
1203  Cudd_RecursiveDerefZdd(dd, f0);
1204  Cudd_RecursiveDerefZdd(dd, g1);
1205  Cudd_RecursiveDerefZdd(dd, g0);
1206  return(NULL);
1207  }
1208  Cudd_Ref(r);
1209 
1210  if (r != zero && g0 != zero) {
1211  tmp = r;
1212  q = cuddZddDivide(dd, f0, g0);
1213  if (q == NULL) {
1214  Cudd_RecursiveDerefZdd(dd, f1);
1215  Cudd_RecursiveDerefZdd(dd, f0);
1216  Cudd_RecursiveDerefZdd(dd, g1);
1217  Cudd_RecursiveDerefZdd(dd, g0);
1218  return(NULL);
1219  }
1220  Cudd_Ref(q);
1221  r = cuddZddIntersect(dd, r, q);
1222  if (r == NULL) {
1223  Cudd_RecursiveDerefZdd(dd, f1);
1224  Cudd_RecursiveDerefZdd(dd, f0);
1225  Cudd_RecursiveDerefZdd(dd, g1);
1226  Cudd_RecursiveDerefZdd(dd, g0);
1227  Cudd_RecursiveDerefZdd(dd, q);
1228  return(NULL);
1229  }
1230  Cudd_Ref(r);
1231  Cudd_RecursiveDerefZdd(dd, q);
1232  Cudd_RecursiveDerefZdd(dd, tmp);
1233  }
1234 
1235  Cudd_RecursiveDerefZdd(dd, f1);
1236  Cudd_RecursiveDerefZdd(dd, f0);
1237  Cudd_RecursiveDerefZdd(dd, g1);
1238  Cudd_RecursiveDerefZdd(dd, g0);
1239 
1240  cuddCacheInsert2(dd, cuddZddDivide, f, g, r);
1241  Cudd_Deref(r);
1242  return(r);
1243 
1244 } /* end of cuddZddDivide */
1245 
1246 
1247 /**Function********************************************************************
1248 
1249  Synopsis [Performs the recursive step of Cudd_zddDivideF.]
1250 
1251  Description []
1252 
1253  SideEffects [None]
1254 
1255  SeeAlso [Cudd_zddDivideF]
1256 
1257 ******************************************************************************/
1258 DdNode *
1259 cuddZddDivideF(
1260  DdManager * dd,
1261  DdNode * f,
1262  DdNode * g)
1263 {
1264  int v;
1265  DdNode *one = DD_ONE(dd);
1266  DdNode *zero = DD_ZERO(dd);
1267  DdNode *f0, *f1, *g0, *g1;
1268  DdNode *q, *r, *tmp;
1269  int flag;
1270 
1271  statLine(dd);
1272  if (g == one)
1273  return(f);
1274  if (f == zero || f == one)
1275  return(zero);
1276  if (f == g)
1277  return(one);
1278 
1279  /* Check cache. */
1280  r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);
1281  if (r)
1282  return(r);
1283 
1284  v = g->index;
1285 
1286  flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
1287  if (flag == 1)
1288  return(NULL);
1289  Cudd_Ref(f1);
1290  Cudd_Ref(f0);
1291  flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */
1292  if (flag == 1) {
1293  Cudd_RecursiveDerefZdd(dd, f1);
1294  Cudd_RecursiveDerefZdd(dd, f0);
1295  return(NULL);
1296  }
1297  Cudd_Ref(g1);
1298  Cudd_Ref(g0);
1299 
1300  r = cuddZddDivideF(dd, f1, g1);
1301  if (r == NULL) {
1302  Cudd_RecursiveDerefZdd(dd, f1);
1303  Cudd_RecursiveDerefZdd(dd, f0);
1304  Cudd_RecursiveDerefZdd(dd, g1);
1305  Cudd_RecursiveDerefZdd(dd, g0);
1306  return(NULL);
1307  }
1308  Cudd_Ref(r);
1309 
1310  if (r != zero && g0 != zero) {
1311  tmp = r;
1312  q = cuddZddDivideF(dd, f0, g0);
1313  if (q == NULL) {
1314  Cudd_RecursiveDerefZdd(dd, f1);
1315  Cudd_RecursiveDerefZdd(dd, f0);
1316  Cudd_RecursiveDerefZdd(dd, g1);
1317  Cudd_RecursiveDerefZdd(dd, g0);
1318  return(NULL);
1319  }
1320  Cudd_Ref(q);
1321  r = cuddZddIntersect(dd, r, q);
1322  if (r == NULL) {
1323  Cudd_RecursiveDerefZdd(dd, f1);
1324  Cudd_RecursiveDerefZdd(dd, f0);
1325  Cudd_RecursiveDerefZdd(dd, g1);
1326  Cudd_RecursiveDerefZdd(dd, g0);
1327  Cudd_RecursiveDerefZdd(dd, q);
1328  return(NULL);
1329  }
1330  Cudd_Ref(r);
1331  Cudd_RecursiveDerefZdd(dd, q);
1332  Cudd_RecursiveDerefZdd(dd, tmp);
1333  }
1334 
1335  Cudd_RecursiveDerefZdd(dd, f1);
1336  Cudd_RecursiveDerefZdd(dd, f0);
1337  Cudd_RecursiveDerefZdd(dd, g1);
1338  Cudd_RecursiveDerefZdd(dd, g0);
1339 
1340  cuddCacheInsert2(dd, cuddZddDivideF, f, g, r);
1341  Cudd_Deref(r);
1342  return(r);
1343 
1344 } /* end of cuddZddDivideF */
1345 
1346 
1347 /**Function********************************************************************
1348 
1349  Synopsis [Computes the three-way decomposition of f w.r.t. v.]
1350 
1351  Description [Computes the three-way decomposition of function f (represented
1352  by a ZDD) wit respect to variable v. Returns 0 if successful; 1 otherwise.]
1353 
1354  SideEffects [The results are returned in f1, f0, and fd.]
1355 
1356  SeeAlso [cuddZddGetCofactors2]
1357 
1358 ******************************************************************************/
1359 int
1360 cuddZddGetCofactors3(
1361  DdManager * dd,
1362  DdNode * f,
1363  int v,
1364  DdNode ** f1,
1365  DdNode ** f0,
1366  DdNode ** fd)
1367 {
1368  DdNode *pc, *nc;
1369  DdNode *zero = DD_ZERO(dd);
1370  int top, hv, ht, pv, nv;
1371  int level;
1372 
1373  top = dd->permZ[f->index];
1374  level = dd->permZ[v];
1375  hv = level >> 1;
1376  ht = top >> 1;
1377 
1378  if (hv < ht) {
1379  *f1 = zero;
1380  *f0 = zero;
1381  *fd = f;
1382  }
1383  else {
1384  pv = cuddZddGetPosVarIndex(dd, v);
1385  nv = cuddZddGetNegVarIndex(dd, v);
1386 
1387  /* not to create intermediate ZDD node */
1388  if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
1389  pc = cuddZddSubset1(dd, f, pv);
1390  if (pc == NULL)
1391  return(1);
1392  Cudd_Ref(pc);
1393  nc = cuddZddSubset0(dd, f, pv);
1394  if (nc == NULL) {
1395  Cudd_RecursiveDerefZdd(dd, pc);
1396  return(1);
1397  }
1398  Cudd_Ref(nc);
1399 
1400  *f1 = cuddZddSubset0(dd, pc, nv);
1401  if (*f1 == NULL) {
1402  Cudd_RecursiveDerefZdd(dd, pc);
1403  Cudd_RecursiveDerefZdd(dd, nc);
1404  return(1);
1405  }
1406  Cudd_Ref(*f1);
1407  *f0 = cuddZddSubset1(dd, nc, nv);
1408  if (*f0 == NULL) {
1409  Cudd_RecursiveDerefZdd(dd, pc);
1410  Cudd_RecursiveDerefZdd(dd, nc);
1411  Cudd_RecursiveDerefZdd(dd, *f1);
1412  return(1);
1413  }
1414  Cudd_Ref(*f0);
1415 
1416  *fd = cuddZddSubset0(dd, nc, nv);
1417  if (*fd == NULL) {
1418  Cudd_RecursiveDerefZdd(dd, pc);
1419  Cudd_RecursiveDerefZdd(dd, nc);
1420  Cudd_RecursiveDerefZdd(dd, *f1);
1421  Cudd_RecursiveDerefZdd(dd, *f0);
1422  return(1);
1423  }
1424  Cudd_Ref(*fd);
1425  } else {
1426  pc = cuddZddSubset1(dd, f, nv);
1427  if (pc == NULL)
1428  return(1);
1429  Cudd_Ref(pc);
1430  nc = cuddZddSubset0(dd, f, nv);
1431  if (nc == NULL) {
1432  Cudd_RecursiveDerefZdd(dd, pc);
1433  return(1);
1434  }
1435  Cudd_Ref(nc);
1436 
1437  *f0 = cuddZddSubset0(dd, pc, pv);
1438  if (*f0 == NULL) {
1439  Cudd_RecursiveDerefZdd(dd, pc);
1440  Cudd_RecursiveDerefZdd(dd, nc);
1441  return(1);
1442  }
1443  Cudd_Ref(*f0);
1444  *f1 = cuddZddSubset1(dd, nc, pv);
1445  if (*f1 == NULL) {
1446  Cudd_RecursiveDerefZdd(dd, pc);
1447  Cudd_RecursiveDerefZdd(dd, nc);
1448  Cudd_RecursiveDerefZdd(dd, *f0);
1449  return(1);
1450  }
1451  Cudd_Ref(*f1);
1452 
1453  *fd = cuddZddSubset0(dd, nc, pv);
1454  if (*fd == NULL) {
1455  Cudd_RecursiveDerefZdd(dd, pc);
1456  Cudd_RecursiveDerefZdd(dd, nc);
1457  Cudd_RecursiveDerefZdd(dd, *f1);
1458  Cudd_RecursiveDerefZdd(dd, *f0);
1459  return(1);
1460  }
1461  Cudd_Ref(*fd);
1462  }
1463 
1464  Cudd_RecursiveDerefZdd(dd, pc);
1465  Cudd_RecursiveDerefZdd(dd, nc);
1466  Cudd_Deref(*f1);
1467  Cudd_Deref(*f0);
1468  Cudd_Deref(*fd);
1469  }
1470  return(0);
1471 
1472 } /* end of cuddZddGetCofactors3 */
1473 
1474 
1475 /**Function********************************************************************
1476 
1477  Synopsis [Computes the two-way decomposition of f w.r.t. v.]
1478 
1479  Description []
1480 
1481  SideEffects [The results are returned in f1 and f0.]
1482 
1483  SeeAlso [cuddZddGetCofactors3]
1484 
1485 ******************************************************************************/
1486 int
1487 cuddZddGetCofactors2(
1488  DdManager * dd,
1489  DdNode * f,
1490  int v,
1491  DdNode ** f1,
1492  DdNode ** f0)
1493 {
1494  *f1 = cuddZddSubset1(dd, f, v);
1495  if (*f1 == NULL)
1496  return(1);
1497  *f0 = cuddZddSubset0(dd, f, v);
1498  if (*f0 == NULL) {
1499  Cudd_RecursiveDerefZdd(dd, *f1);
1500  return(1);
1501  }
1502  return(0);
1503 
1504 } /* end of cuddZddGetCofactors2 */
1505 
1506 
1507 /**Function********************************************************************
1508 
1509  Synopsis [Computes a complement of a ZDD node.]
1510 
1511  Description [Computes the complement of a ZDD node. So far, since we
1512  couldn't find a direct way to get the complement of a ZDD cover, we first
1513  convert a ZDD cover to a BDD, then make the complement of the ZDD cover
1514  from the complement of the BDD node by using ISOP.]
1515 
1516  SideEffects [The result depends on current variable order.]
1517 
1518  SeeAlso []
1519 
1520 ******************************************************************************/
1521 DdNode *
1522 cuddZddComplement(
1523  DdManager * dd,
1524  DdNode *node)
1525 {
1526  DdNode *b, *isop, *zdd_I;
1527 
1528  /* Check cache */
1529  zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
1530  if (zdd_I)
1531  return(zdd_I);
1532 
1533  b = cuddMakeBddFromZddCover(dd, node);
1534  if (!b)
1535  return(NULL);
1536  cuddRef(b);
1537  isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
1538  if (!isop) {
1539  Cudd_RecursiveDeref(dd, b);
1540  return(NULL);
1541  }
1542  cuddRef(isop);
1543  cuddRef(zdd_I);
1544  Cudd_RecursiveDeref(dd, b);
1545  Cudd_RecursiveDeref(dd, isop);
1546 
1547  cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
1548  cuddDeref(zdd_I);
1549  return(zdd_I);
1550 } /* end of cuddZddComplement */
1551 
1552 
1553 /**Function********************************************************************
1554 
1555  Synopsis [Returns the index of positive ZDD variable.]
1556 
1557  Description [Returns the index of positive ZDD variable.]
1558 
1559  SideEffects []
1560 
1561  SeeAlso []
1562 
1563 ******************************************************************************/
1564 int
1565 cuddZddGetPosVarIndex(
1566  DdManager * dd,
1567  int index)
1568 {
1569  int pv = (index >> 1) << 1;
1570  return(pv);
1571 } /* end of cuddZddGetPosVarIndex */
1572 
1573 
1574 /**Function********************************************************************
1575 
1576  Synopsis [Returns the index of negative ZDD variable.]
1577 
1578  Description [Returns the index of negative ZDD variable.]
1579 
1580  SideEffects []
1581 
1582  SeeAlso []
1583 
1584 ******************************************************************************/
1585 int
1586 cuddZddGetNegVarIndex(
1587  DdManager * dd,
1588  int index)
1589 {
1590  int nv = index | 0x1;
1591  return(nv);
1592 } /* end of cuddZddGetPosVarIndex */
1593 
1594 
1595 /**Function********************************************************************
1596 
1597  Synopsis [Returns the level of positive ZDD variable.]
1598 
1599  Description [Returns the level of positive ZDD variable.]
1600 
1601  SideEffects []
1602 
1603  SeeAlso []
1604 
1605 ******************************************************************************/
1606 int
1607 cuddZddGetPosVarLevel(
1608  DdManager * dd,
1609  int index)
1610 {
1611  int pv = cuddZddGetPosVarIndex(dd, index);
1612  return(dd->permZ[pv]);
1613 } /* end of cuddZddGetPosVarLevel */
1614 
1615 
1616 /**Function********************************************************************
1617 
1618  Synopsis [Returns the level of negative ZDD variable.]
1619 
1620  Description [Returns the level of negative ZDD variable.]
1621 
1622  SideEffects []
1623 
1624  SeeAlso []
1625 
1626 ******************************************************************************/
1627 int
1628 cuddZddGetNegVarLevel(
1629  DdManager * dd,
1630  int index)
1631 {
1632  int nv = cuddZddGetNegVarIndex(dd, index);
1633  return(dd->permZ[nv]);
1634 } /* end of cuddZddGetNegVarLevel */
1635 
1636 
1637 ABC_NAMESPACE_IMPL_END
1638 
cuddCacheLookup2Zdd
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:610
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_zddComplement
DdNode * Cudd_zddComplement(DdManager *dd, DdNode *node)
Definition: cuddZddFuncs.c:332
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
cuddZddDivide
DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:1159
DdNode
Definition: cudd.h:278
cuddZddGetNode
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1041
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_zddProduct
DdNode * Cudd_zddProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:145
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DD_UNUSED
static ABC_NAMESPACE_IMPL_START char rcsid[] DD_UNUSED
Definition: cuddZddFuncs.c:105
cuddZddGetCofactors2
int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0)
Definition: cuddZddFuncs.c:1487
Cudd_zddWeakDiv
DdNode * Cudd_zddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:210
DdManager::permZ
int * permZ
Definition: cuddInt.h:387
cuddZddGetCofactors3
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Definition: cuddZddFuncs.c:1360
cuddZddGetPosVarLevel
int cuddZddGetPosVarLevel(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1607
Cudd_MakeBddFromZddCover
DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:203
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddZddUnateProduct
DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:617
util_hack.h
cuddZddProduct
DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:380
DdManager::reordered
int reordered
Definition: cuddInt.h:409
cuddZddGetNegVarIndex
int cuddZddGetNegVarIndex(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1586
one
static DdNode * one
Definition: cuddDecomp.c:112
cuddZddIntersect
DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:642
cuddZddWeakDiv
DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:761
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:234
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:800
Cudd_zddIsop
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:136
Cudd_zddDivideF
DdNode * Cudd_zddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:299
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddZddGetPosVarIndex
int cuddZddGetPosVarIndex(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1565
cuddZddWeakDivF
DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:922
Cudd_zddWeakDivF
DdNode * Cudd_zddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:270
Cudd_zddDivide
DdNode * Cudd_zddDivide(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:241
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
cuddZddSubset1
DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:874
cuddZddUnion
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:553
cuddZddGetNegVarLevel
int cuddZddGetNegVarLevel(DdManager *dd, int index)
Definition: cuddZddFuncs.c:1628
DdNode::index
DdHalfWord index
Definition: cudd.h:279
Cudd_zddUnateProduct
DdNode * Cudd_zddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:176
cuddZddSubset0
DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:923
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddZddDivideF
DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:1259
cuddZddComplement
DdNode * cuddZddComplement(DdManager *dd, DdNode *node)
Definition: cuddZddFuncs.c:1522
zero
static DdNode * zero
Definition: cuddApa.c:100
cuddCacheLookup1Zdd
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:664
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