source: vis_dev/glu-2.3/src/cuBdd/cuddZddFuncs.c @ 76

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

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