source: vis_dev/glu-2.3/src/cuBdd/cuddZddSetop.c @ 104

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

library glu 2.3
File size: 27.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddSetop.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Set operations on ZDDs.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_zddIte()
12                    <li> Cudd_zddUnion()
13                    <li> Cudd_zddIntersect()
14                    <li> Cudd_zddDiff()
15                    <li> Cudd_zddDiffConst()
16                    <li> Cudd_zddSubset1()
17                    <li> Cudd_zddSubset0()
18                    <li> Cudd_zddChange()
19                    </ul>
20               Internal procedures included in this module:
21                    <ul>
22                    <li> cuddZddIte()
23                    <li> cuddZddUnion()
24                    <li> cuddZddIntersect()
25                    <li> cuddZddDiff()
26                    <li> cuddZddChangeAux()
27                    <li> cuddZddSubset1()
28                    <li> cuddZddSubset0()
29                    </ul>
30               Static procedures included in this module:
31                    <ul>
32                    <li> zdd_subset1_aux()
33                    <li> zdd_subset0_aux()
34                    <li> zddVarToConst()
35                    </ul>
36              ]
37
38  SeeAlso     []
39
40  Author      [Hyong-Kyoon Shin, In-Ho Moon]
41
42  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
43
44  All rights reserved.
45
46  Redistribution and use in source and binary forms, with or without
47  modification, are permitted provided that the following conditions
48  are met:
49
50  Redistributions of source code must retain the above copyright
51  notice, this list of conditions and the following disclaimer.
52
53  Redistributions in binary form must reproduce the above copyright
54  notice, this list of conditions and the following disclaimer in the
55  documentation and/or other materials provided with the distribution.
56
57  Neither the name of the University of Colorado nor the names of its
58  contributors may be used to endorse or promote products derived from
59  this software without specific prior written permission.
60
61  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72  POSSIBILITY OF SUCH DAMAGE.]
73
74******************************************************************************/
75
76#include "util.h"
77#include "cuddInt.h"
78
79/*---------------------------------------------------------------------------*/
80/* Constant declarations                                                     */
81/*---------------------------------------------------------------------------*/
82
83
84/*---------------------------------------------------------------------------*/
85/* Stucture declarations                                                     */
86/*---------------------------------------------------------------------------*/
87
88
89/*---------------------------------------------------------------------------*/
90/* Type declarations                                                         */
91/*---------------------------------------------------------------------------*/
92
93
94/*---------------------------------------------------------------------------*/
95/* Variable declarations                                                     */
96/*---------------------------------------------------------------------------*/
97
98#ifndef lint
99static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $";
100#endif
101
102/*---------------------------------------------------------------------------*/
103/* Macro declarations                                                        */
104/*---------------------------------------------------------------------------*/
105
106#ifdef __cplusplus
107extern "C" {
108#endif
109
110/**AutomaticStart*************************************************************/
111
112/*---------------------------------------------------------------------------*/
113/* Static function prototypes                                                */
114/*---------------------------------------------------------------------------*/
115
116static DdNode * zdd_subset1_aux (DdManager *zdd, DdNode *P, DdNode *zvar);
117static DdNode * zdd_subset0_aux (DdManager *zdd, DdNode *P, DdNode *zvar);
118static void zddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty);
119
120/**AutomaticEnd***************************************************************/
121
122#ifdef __cplusplus
123}
124#endif
125
126/*---------------------------------------------------------------------------*/
127/* Definition of exported functions                                          */
128/*---------------------------------------------------------------------------*/
129
130
131/**Function********************************************************************
132
133  Synopsis [Computes the ITE of three ZDDs.]
134
135  Description [Computes the ITE of three ZDDs. Returns a pointer to the
136  result if successful; NULL otherwise.]
137
138  SideEffects [None]
139
140  SeeAlso     []
141
142******************************************************************************/
143DdNode *
144Cudd_zddIte(
145  DdManager * dd,
146  DdNode * f,
147  DdNode * g,
148  DdNode * h)
149{
150    DdNode *res;
151
152    do {
153        dd->reordered = 0;
154        res = cuddZddIte(dd, f, g, h);
155    } while (dd->reordered == 1);
156    return(res);
157
158} /* end of Cudd_zddIte */
159
160
161/**Function********************************************************************
162
163  Synopsis [Computes the union of two ZDDs.]
164
165  Description [Computes the union of two ZDDs. Returns a pointer to the
166  result if successful; NULL otherwise.]
167
168  SideEffects [None]
169
170  SeeAlso     []
171
172******************************************************************************/
173DdNode *
174Cudd_zddUnion(
175  DdManager * dd,
176  DdNode * P,
177  DdNode * Q)
178{
179    DdNode *res;
180
181    do {
182        dd->reordered = 0;
183        res = cuddZddUnion(dd, P, Q);
184    } while (dd->reordered == 1);
185    return(res);
186
187} /* end of Cudd_zddUnion */
188
189
190/**Function********************************************************************
191
192  Synopsis [Computes the intersection of two ZDDs.]
193
194  Description [Computes the intersection of two ZDDs. Returns a pointer to
195  the result if successful; NULL otherwise.]
196
197  SideEffects [None]
198
199  SeeAlso     []
200
201******************************************************************************/
202DdNode *
203Cudd_zddIntersect(
204  DdManager * dd,
205  DdNode * P,
206  DdNode * Q)
207{
208    DdNode *res;
209
210    do {
211        dd->reordered = 0;
212        res = cuddZddIntersect(dd, P, Q);
213    } while (dd->reordered == 1);
214    return(res);
215
216} /* end of Cudd_zddIntersect */
217
218
219/**Function********************************************************************
220
221  Synopsis [Computes the difference of two ZDDs.]
222
223  Description [Computes the difference of two ZDDs. Returns a pointer to the
224  result if successful; NULL otherwise.]
225
226  SideEffects [None]
227
228  SeeAlso     [Cudd_zddDiffConst]
229
230******************************************************************************/
231DdNode *
232Cudd_zddDiff(
233  DdManager * dd,
234  DdNode * P,
235  DdNode * Q)
236{
237    DdNode *res;
238
239    do {
240        dd->reordered = 0;
241        res = cuddZddDiff(dd, P, Q);
242    } while (dd->reordered == 1);
243    return(res);
244
245} /* end of Cudd_zddDiff */
246
247
248/**Function********************************************************************
249
250  Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
251
252  Description [Inclusion test for ZDDs (P implies Q). No new nodes are
253  generated by this procedure. Returns empty if true;
254  a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
255
256  SideEffects [None]
257
258  SeeAlso     [Cudd_zddDiff]
259
260******************************************************************************/
261DdNode *
262Cudd_zddDiffConst(
263  DdManager * zdd,
264  DdNode * P,
265  DdNode * Q)
266{
267    int         p_top, q_top;
268    DdNode      *empty = DD_ZERO(zdd), *t, *res;
269    DdManager   *table = zdd;
270
271    statLine(zdd);
272    if (P == empty)
273        return(empty);
274    if (Q == empty)
275        return(P);
276    if (P == Q)
277        return(empty);
278
279    /* Check cache.  The cache is shared by cuddZddDiff(). */
280    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
281    if (res != NULL)
282        return(res);
283
284    if (cuddIsConstant(P))
285        p_top = P->index;
286    else
287        p_top = zdd->permZ[P->index];
288    if (cuddIsConstant(Q))
289        q_top = Q->index;
290    else
291        q_top = zdd->permZ[Q->index];
292    if (p_top < q_top) {
293        res = DD_NON_CONSTANT;
294    } else if (p_top > q_top) {
295        res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
296    } else {
297        t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
298        if (t != empty)
299            res = DD_NON_CONSTANT;
300        else
301            res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
302    }
303
304    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
305
306    return(res);
307
308} /* end of Cudd_zddDiffConst */
309
310
311/**Function********************************************************************
312
313  Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
314
315  Description [Computes the positive cofactor of a ZDD w.r.t. a
316  variable. In terms of combinations, the result is the set of all
317  combinations in which the variable is asserted. Returns a pointer to
318  the result if successful; NULL otherwise.]
319
320  SideEffects [None]
321
322  SeeAlso     [Cudd_zddSubset0]
323
324******************************************************************************/
325DdNode *
326Cudd_zddSubset1(
327  DdManager * dd,
328  DdNode * P,
329  int  var)
330{
331    DdNode      *r;
332
333    do {
334        dd->reordered = 0;
335        r = cuddZddSubset1(dd, P, var);
336    } while (dd->reordered == 1);
337
338    return(r);
339
340} /* end of Cudd_zddSubset1 */
341
342
343/**Function********************************************************************
344
345  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
346
347  Description [Computes the negative cofactor of a ZDD w.r.t. a
348  variable. In terms of combinations, the result is the set of all
349  combinations in which the variable is negated. Returns a pointer to
350  the result if successful; NULL otherwise.]
351
352  SideEffects [None]
353
354  SeeAlso     [Cudd_zddSubset1]
355
356******************************************************************************/
357DdNode *
358Cudd_zddSubset0(
359  DdManager * dd,
360  DdNode * P,
361  int  var)
362{
363    DdNode      *r;
364
365    do {
366        dd->reordered = 0;
367        r = cuddZddSubset0(dd, P, var);
368    } while (dd->reordered == 1);
369
370    return(r);
371
372} /* end of Cudd_zddSubset0 */
373
374
375/**Function********************************************************************
376
377  Synopsis [Substitutes a variable with its complement in a ZDD.]
378
379  Description [Substitutes a variable with its complement in a ZDD.
380  returns a pointer to the result if successful; NULL otherwise.]
381
382  SideEffects [None]
383
384  SeeAlso     []
385
386******************************************************************************/
387DdNode *
388Cudd_zddChange(
389  DdManager * dd,
390  DdNode * P,
391  int  var)
392{
393    DdNode      *res;
394
395    if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
396   
397    do {
398        dd->reordered = 0;
399        res = cuddZddChange(dd, P, var);
400    } while (dd->reordered == 1);
401    return(res);
402
403} /* end of Cudd_zddChange */
404
405
406/*---------------------------------------------------------------------------*/
407/* Definition of internal functions                                          */
408/*---------------------------------------------------------------------------*/
409
410
411/**Function********************************************************************
412
413  Synopsis    [Performs the recursive step of Cudd_zddIte.]
414
415  Description []
416
417  SideEffects [None]
418
419  SeeAlso     []
420
421******************************************************************************/
422DdNode *
423cuddZddIte(
424  DdManager * dd,
425  DdNode * f,
426  DdNode * g,
427  DdNode * h)
428{
429    DdNode *tautology, *empty;
430    DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
431    unsigned int topf,topg,toph,v,top;
432    int index;
433
434    statLine(dd);
435    /* Trivial cases. */
436    /* One variable cases. */
437    if (f == (empty = DD_ZERO(dd))) {   /* ITE(0,G,H) = H */
438        return(h);
439    }
440    topf = cuddIZ(dd,f->index);
441    topg = cuddIZ(dd,g->index);
442    toph = cuddIZ(dd,h->index);
443    v = ddMin(topg,toph);
444    top  = ddMin(topf,v);
445
446    tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
447    if (f == tautology) {                       /* ITE(1,G,H) = G */
448        return(g);
449    }
450
451    /* From now on, f is known to not be a constant. */
452    zddVarToConst(f,&g,&h,tautology,empty);
453
454    /* Check remaining one variable cases. */
455    if (g == h) {                       /* ITE(F,G,G) = G */
456        return(g);
457    }
458
459    if (g == tautology) {                       /* ITE(F,1,0) = F */
460        if (h == empty) return(f);
461    }
462
463    /* Check cache. */
464    r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
465    if (r != NULL) {
466        return(r);
467    }
468
469    /* Recompute these because they may have changed in zddVarToConst. */
470    topg = cuddIZ(dd,g->index);
471    toph = cuddIZ(dd,h->index);
472    v = ddMin(topg,toph);
473
474    if (topf < v) {
475        r = cuddZddIte(dd,cuddE(f),g,h);
476        if (r == NULL) return(NULL);
477    } else if (topf > v) {
478        if (topg > v) {
479            Gvn = g;
480            index = h->index;
481        } else {
482            Gvn = cuddE(g);
483            index = g->index;
484        }
485        if (toph > v) {
486            Hv = empty; Hvn = h;
487        } else {
488            Hv = cuddT(h); Hvn = cuddE(h);
489        }
490        e = cuddZddIte(dd,f,Gvn,Hvn);
491        if (e == NULL) return(NULL);
492        cuddRef(e);
493        r = cuddZddGetNode(dd,index,Hv,e);
494        if (r == NULL) {
495            Cudd_RecursiveDerefZdd(dd,e);
496            return(NULL);
497        }
498        cuddDeref(e);
499    } else {
500        index = f->index;
501        if (topg > v) {
502            Gv = empty; Gvn = g;
503        } else {
504            Gv = cuddT(g); Gvn = cuddE(g);
505        }
506        if (toph > v) {
507            Hv = empty; Hvn = h;
508        } else {
509            Hv = cuddT(h); Hvn = cuddE(h);
510        }
511        e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
512        if (e == NULL) return(NULL);
513        cuddRef(e);
514        t = cuddZddIte(dd,cuddT(f),Gv,Hv);
515        if (t == NULL) {
516            Cudd_RecursiveDerefZdd(dd,e);
517            return(NULL);
518        }
519        cuddRef(t);
520        r = cuddZddGetNode(dd,index,t,e);
521        if (r == NULL) {
522            Cudd_RecursiveDerefZdd(dd,e);
523            Cudd_RecursiveDerefZdd(dd,t);
524            return(NULL);
525        }
526        cuddDeref(t);
527        cuddDeref(e);
528    }
529
530    cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
531
532    return(r);
533
534} /* end of cuddZddIte */
535
536
537/**Function********************************************************************
538
539  Synopsis [Performs the recursive step of Cudd_zddUnion.]
540
541  Description []
542
543  SideEffects [None]
544
545  SeeAlso     []
546
547******************************************************************************/
548DdNode *
549cuddZddUnion(
550  DdManager * zdd,
551  DdNode * P,
552  DdNode * Q)
553{
554    int         p_top, q_top;
555    DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
556    DdManager   *table = zdd;
557
558    statLine(zdd);
559    if (P == empty)
560        return(Q);
561    if (Q == empty)
562        return(P);
563    if (P == Q)
564        return(P);
565
566    /* Check cache */
567    res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
568    if (res != NULL)
569        return(res);
570
571    if (cuddIsConstant(P))
572        p_top = P->index;
573    else
574        p_top = zdd->permZ[P->index];
575    if (cuddIsConstant(Q))
576        q_top = Q->index;
577    else
578        q_top = zdd->permZ[Q->index];
579    if (p_top < q_top) {
580        e = cuddZddUnion(zdd, cuddE(P), Q);
581        if (e == NULL) return (NULL);
582        cuddRef(e);
583        res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
584        if (res == NULL) {
585            Cudd_RecursiveDerefZdd(table, e);
586            return(NULL);
587        }
588        cuddDeref(e);
589    } else if (p_top > q_top) {
590        e = cuddZddUnion(zdd, P, cuddE(Q));
591        if (e == NULL) return(NULL);
592        cuddRef(e);
593        res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
594        if (res == NULL) {
595            Cudd_RecursiveDerefZdd(table, e);
596            return(NULL);
597        }
598        cuddDeref(e);
599    } else {
600        t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
601        if (t == NULL) return(NULL);
602        cuddRef(t);
603        e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
604        if (e == NULL) {
605            Cudd_RecursiveDerefZdd(table, t);
606            return(NULL);
607        }
608        cuddRef(e);
609        res = cuddZddGetNode(zdd, P->index, t, e);
610        if (res == NULL) {
611            Cudd_RecursiveDerefZdd(table, t);
612            Cudd_RecursiveDerefZdd(table, e);
613            return(NULL);
614        }
615        cuddDeref(t);
616        cuddDeref(e);
617    }
618
619    cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
620
621    return(res);
622
623} /* end of cuddZddUnion */
624
625
626/**Function********************************************************************
627
628  Synopsis [Performs the recursive step of Cudd_zddIntersect.]
629
630  Description []
631
632  SideEffects [None]
633
634  SeeAlso     []
635
636******************************************************************************/
637DdNode *
638cuddZddIntersect(
639  DdManager * zdd,
640  DdNode * P,
641  DdNode * Q)
642{
643    int         p_top, q_top;
644    DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
645    DdManager   *table = zdd;
646
647    statLine(zdd);
648    if (P == empty)
649        return(empty);
650    if (Q == empty)
651        return(empty);
652    if (P == Q)
653        return(P);
654
655    /* Check cache. */
656    res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
657    if (res != NULL)
658        return(res);
659
660    if (cuddIsConstant(P))
661        p_top = P->index;
662    else
663        p_top = zdd->permZ[P->index];
664    if (cuddIsConstant(Q))
665        q_top = Q->index;
666    else
667        q_top = zdd->permZ[Q->index];
668    if (p_top < q_top) {
669        res = cuddZddIntersect(zdd, cuddE(P), Q);
670        if (res == NULL) return(NULL);
671    } else if (p_top > q_top) {
672        res = cuddZddIntersect(zdd, P, cuddE(Q));
673        if (res == NULL) return(NULL);
674    } else {
675        t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
676        if (t == NULL) return(NULL);
677        cuddRef(t);
678        e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
679        if (e == NULL) {
680            Cudd_RecursiveDerefZdd(table, t);
681            return(NULL);
682        }
683        cuddRef(e);
684        res = cuddZddGetNode(zdd, P->index, t, e);
685        if (res == NULL) {
686            Cudd_RecursiveDerefZdd(table, t);
687            Cudd_RecursiveDerefZdd(table, e);
688            return(NULL);
689        }
690        cuddDeref(t);
691        cuddDeref(e);
692    }
693
694    cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
695
696    return(res);
697
698} /* end of cuddZddIntersect */
699
700
701/**Function********************************************************************
702
703  Synopsis [Performs the recursive step of Cudd_zddDiff.]
704
705  Description []
706
707  SideEffects [None]
708
709  SeeAlso     []
710
711******************************************************************************/
712DdNode *
713cuddZddDiff(
714  DdManager * zdd,
715  DdNode * P,
716  DdNode * Q)
717{
718    int         p_top, q_top;
719    DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
720    DdManager   *table = zdd;
721
722    statLine(zdd);
723    if (P == empty)
724        return(empty);
725    if (Q == empty)
726        return(P);
727    if (P == Q)
728        return(empty);
729
730    /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
731    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
732    if (res != NULL && res != DD_NON_CONSTANT)
733        return(res);
734
735    if (cuddIsConstant(P))
736        p_top = P->index;
737    else
738        p_top = zdd->permZ[P->index];
739    if (cuddIsConstant(Q))
740        q_top = Q->index;
741    else
742        q_top = zdd->permZ[Q->index];
743    if (p_top < q_top) {
744        e = cuddZddDiff(zdd, cuddE(P), Q);
745        if (e == NULL) return(NULL);
746        cuddRef(e);
747        res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
748        if (res == NULL) {
749            Cudd_RecursiveDerefZdd(table, e);
750            return(NULL);
751        }
752        cuddDeref(e);
753    } else if (p_top > q_top) {
754        res = cuddZddDiff(zdd, P, cuddE(Q));
755        if (res == NULL) return(NULL);
756    } else {
757        t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
758        if (t == NULL) return(NULL);
759        cuddRef(t);
760        e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
761        if (e == NULL) {
762            Cudd_RecursiveDerefZdd(table, t);
763            return(NULL);
764        }
765        cuddRef(e);
766        res = cuddZddGetNode(zdd, P->index, t, e);
767        if (res == NULL) {
768            Cudd_RecursiveDerefZdd(table, t);
769            Cudd_RecursiveDerefZdd(table, e);
770            return(NULL);
771        }
772        cuddDeref(t);
773        cuddDeref(e);
774    }
775
776    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
777
778    return(res);
779
780} /* end of cuddZddDiff */
781
782
783/**Function********************************************************************
784
785  Synopsis [Performs the recursive step of Cudd_zddChange.]
786
787  Description []
788
789  SideEffects [None]
790
791  SeeAlso     []
792
793******************************************************************************/
794DdNode *
795cuddZddChangeAux(
796  DdManager * zdd,
797  DdNode * P,
798  DdNode * zvar)
799{
800    int         top_var, level;
801    DdNode      *res, *t, *e;
802    DdNode      *base = DD_ONE(zdd);
803    DdNode      *empty = DD_ZERO(zdd);
804
805    statLine(zdd);
806    if (P == empty)
807        return(empty);
808    if (P == base)
809        return(zvar);
810
811    /* Check cache. */
812    res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
813    if (res != NULL)
814        return(res);
815
816    top_var = zdd->permZ[P->index];
817    level = zdd->permZ[zvar->index];
818
819    if (top_var > level) {
820        res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
821        if (res == NULL) return(NULL);
822    } else if (top_var == level) {
823        res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
824        if (res == NULL) return(NULL);
825    } else {
826        t = cuddZddChangeAux(zdd, cuddT(P), zvar);
827        if (t == NULL) return(NULL);
828        cuddRef(t);
829        e = cuddZddChangeAux(zdd, cuddE(P), zvar);
830        if (e == NULL) {
831            Cudd_RecursiveDerefZdd(zdd, t);
832            return(NULL);
833        }
834        cuddRef(e);
835        res = cuddZddGetNode(zdd, P->index, t, e);
836        if (res == NULL) {
837            Cudd_RecursiveDerefZdd(zdd, t);
838            Cudd_RecursiveDerefZdd(zdd, e);
839            return(NULL);
840        }
841        cuddDeref(t);
842        cuddDeref(e);
843    }
844
845    cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
846
847    return(res);
848
849} /* end of cuddZddChangeAux */
850
851
852/**Function********************************************************************
853
854  Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
855
856  Description [Computes the positive cofactor of a ZDD w.r.t. a
857  variable. In terms of combinations, the result is the set of all
858  combinations in which the variable is asserted. Returns a pointer to
859  the result if successful; NULL otherwise. cuddZddSubset1 performs
860  the same function as Cudd_zddSubset1, but does not restart if
861  reordering has taken place. Therefore it can be called from within a
862  recursive procedure.]
863
864  SideEffects [None]
865
866  SeeAlso     [cuddZddSubset0 Cudd_zddSubset1]
867
868******************************************************************************/
869DdNode *
870cuddZddSubset1(
871  DdManager * dd,
872  DdNode * P,
873  int  var)
874{
875    DdNode      *zvar, *r;
876    DdNode      *base, *empty;
877
878    base = DD_ONE(dd);
879    empty = DD_ZERO(dd);
880
881    zvar = cuddUniqueInterZdd(dd, var, base, empty);
882    if (zvar == NULL) {
883        return(NULL);
884    } else {
885        cuddRef(zvar);
886        r = zdd_subset1_aux(dd, P, zvar);
887        if (r == NULL) {
888            Cudd_RecursiveDerefZdd(dd, zvar);
889            return(NULL);
890        }
891        cuddRef(r);
892        Cudd_RecursiveDerefZdd(dd, zvar);
893    }
894
895    cuddDeref(r);
896    return(r);
897
898} /* end of cuddZddSubset1 */
899
900
901/**Function********************************************************************
902
903  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
904
905  Description [Computes the negative cofactor of a ZDD w.r.t. a
906  variable. In terms of combinations, the result is the set of all
907  combinations in which the variable is negated. Returns a pointer to
908  the result if successful; NULL otherwise. cuddZddSubset0 performs
909  the same function as Cudd_zddSubset0, but does not restart if
910  reordering has taken place. Therefore it can be called from within a
911  recursive procedure.]
912
913  SideEffects [None]
914
915  SeeAlso     [cuddZddSubset1 Cudd_zddSubset0]
916
917******************************************************************************/
918DdNode *
919cuddZddSubset0(
920  DdManager * dd,
921  DdNode * P,
922  int  var)
923{
924    DdNode      *zvar, *r;
925    DdNode      *base, *empty;
926
927    base = DD_ONE(dd);
928    empty = DD_ZERO(dd);
929
930    zvar = cuddUniqueInterZdd(dd, var, base, empty);
931    if (zvar == NULL) {
932        return(NULL);
933    } else {
934        cuddRef(zvar);
935        r = zdd_subset0_aux(dd, P, zvar);
936        if (r == NULL) {
937            Cudd_RecursiveDerefZdd(dd, zvar);
938            return(NULL);
939        }
940        cuddRef(r);
941        Cudd_RecursiveDerefZdd(dd, zvar);
942    }
943
944    cuddDeref(r);
945    return(r);
946
947} /* end of cuddZddSubset0 */
948
949
950/**Function********************************************************************
951
952  Synopsis [Substitutes a variable with its complement in a ZDD.]
953
954  Description [Substitutes a variable with its complement in a ZDD.
955  returns a pointer to the result if successful; NULL
956  otherwise. cuddZddChange performs the same function as
957  Cudd_zddChange, but does not restart if reordering has taken
958  place. Therefore it can be called from within a recursive
959  procedure.]
960
961  SideEffects [None]
962
963  SeeAlso     [Cudd_zddChange]
964
965******************************************************************************/
966DdNode *
967cuddZddChange(
968  DdManager * dd,
969  DdNode * P,
970  int  var)
971{
972    DdNode      *zvar, *res;
973
974    zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
975    if (zvar == NULL) return(NULL);
976    cuddRef(zvar);
977
978    res = cuddZddChangeAux(dd, P, zvar);
979    if (res == NULL) {
980        Cudd_RecursiveDerefZdd(dd,zvar);
981        return(NULL);
982    }
983    cuddRef(res);
984    Cudd_RecursiveDerefZdd(dd,zvar);
985    cuddDeref(res);
986    return(res);
987
988} /* end of cuddZddChange */
989
990
991/*---------------------------------------------------------------------------*/
992/* Definition of static functions                                            */
993/*---------------------------------------------------------------------------*/
994
995
996/**Function********************************************************************
997
998  Synopsis [Performs the recursive step of Cudd_zddSubset1.]
999
1000  Description []
1001
1002  SideEffects [None]
1003
1004  SeeAlso     []
1005
1006******************************************************************************/
1007static DdNode *
1008zdd_subset1_aux(
1009  DdManager * zdd,
1010  DdNode * P,
1011  DdNode * zvar)
1012{
1013    int         top_var, level;
1014    DdNode      *res, *t, *e;
1015    DdNode      *empty;
1016
1017    statLine(zdd);
1018    empty = DD_ZERO(zdd);
1019
1020    /* Check cache. */
1021    res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
1022    if (res != NULL)
1023        return(res);
1024
1025    if (cuddIsConstant(P)) {
1026        res = empty;
1027        cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
1028        return(res);
1029    }
1030
1031    top_var = zdd->permZ[P->index];
1032    level = zdd->permZ[zvar->index];
1033
1034    if (top_var > level) {
1035        res = empty;
1036    } else if (top_var == level) {
1037        res = cuddT(P);
1038    } else {
1039        t = zdd_subset1_aux(zdd, cuddT(P), zvar);
1040        if (t == NULL) return(NULL);
1041        cuddRef(t);
1042        e = zdd_subset1_aux(zdd, cuddE(P), zvar);
1043        if (e == NULL) {
1044            Cudd_RecursiveDerefZdd(zdd, t);
1045            return(NULL);
1046        }
1047        cuddRef(e);
1048        res = cuddZddGetNode(zdd, P->index, t, e);
1049        if (res == NULL) {
1050            Cudd_RecursiveDerefZdd(zdd, t);
1051            Cudd_RecursiveDerefZdd(zdd, e);
1052            return(NULL);
1053        }
1054        cuddDeref(t);
1055        cuddDeref(e);
1056    }
1057
1058    cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
1059
1060    return(res);
1061
1062} /* end of zdd_subset1_aux */
1063
1064
1065/**Function********************************************************************
1066
1067  Synopsis [Performs the recursive step of Cudd_zddSubset0.]
1068
1069  Description []
1070
1071  SideEffects [None]
1072
1073  SeeAlso     []
1074
1075******************************************************************************/
1076static DdNode *
1077zdd_subset0_aux(
1078  DdManager * zdd,
1079  DdNode * P,
1080  DdNode * zvar)
1081{
1082    int         top_var, level;
1083    DdNode      *res, *t, *e;
1084
1085    statLine(zdd);
1086
1087    /* Check cache. */
1088    res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
1089    if (res != NULL)
1090        return(res);
1091
1092    if (cuddIsConstant(P)) {
1093        res = P;
1094        cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
1095        return(res);
1096    }
1097
1098    top_var = zdd->permZ[P->index];
1099    level = zdd->permZ[zvar->index];
1100
1101    if (top_var > level) {
1102        res = P;
1103    }
1104    else if (top_var == level) {
1105        res = cuddE(P);
1106    }
1107    else {
1108        t = zdd_subset0_aux(zdd, cuddT(P), zvar);
1109        if (t == NULL) return(NULL);
1110        cuddRef(t);
1111        e = zdd_subset0_aux(zdd, cuddE(P), zvar);
1112        if (e == NULL) {
1113            Cudd_RecursiveDerefZdd(zdd, t);
1114            return(NULL);
1115        }
1116        cuddRef(e);
1117        res = cuddZddGetNode(zdd, P->index, t, e);
1118        if (res == NULL) {
1119            Cudd_RecursiveDerefZdd(zdd, t);
1120            Cudd_RecursiveDerefZdd(zdd, e);
1121            return(NULL);
1122        }
1123        cuddDeref(t);
1124        cuddDeref(e);
1125    }
1126
1127    cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
1128
1129    return(res);
1130
1131} /* end of zdd_subset0_aux */
1132
1133
1134/**Function********************************************************************
1135
1136  Synopsis    [Replaces variables with constants if possible (part of
1137  canonical form).]
1138
1139  Description []
1140
1141  SideEffects [None]
1142
1143  SeeAlso     []
1144
1145******************************************************************************/
1146static void
1147zddVarToConst(
1148  DdNode * f,
1149  DdNode ** gp,
1150  DdNode ** hp,
1151  DdNode * base,
1152  DdNode * empty)
1153{
1154    DdNode *g = *gp;
1155    DdNode *h = *hp;
1156
1157    if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
1158        *gp = base;
1159    }
1160
1161    if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
1162        *hp = empty;
1163    }
1164
1165} /* end of zddVarToConst */
1166
Note: See TracBrowser for help on using the repository browser.