source: vis_dev/glu-2.3/src/cuBdd/cuddZddPort.c @ 23

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

library glu 2.3
File size: 10.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddPort.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions that translate BDDs to ZDDs.]
8
9  Description [External procedures included in this module:
10                    <ul>
11                    <li> Cudd_zddPortFromBdd()
12                    <li> Cudd_zddPortToBdd()
13                    </ul>
14               Internal procedures included in this module:
15                    <ul>
16                    </ul>
17               Static procedures included in this module:
18                    <ul>
19                    <li> zddPortFromBddStep()
20                    <li> zddPortToBddStep()
21                    </ul>
22              ]
23
24  SeeAlso     []
25
26  Author      [Hyong-kyoon Shin, In-Ho Moon]
27
28  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
29
30  All rights reserved.
31
32  Redistribution and use in source and binary forms, with or without
33  modification, are permitted provided that the following conditions
34  are met:
35
36  Redistributions of source code must retain the above copyright
37  notice, this list of conditions and the following disclaimer.
38
39  Redistributions in binary form must reproduce the above copyright
40  notice, this list of conditions and the following disclaimer in the
41  documentation and/or other materials provided with the distribution.
42
43  Neither the name of the University of Colorado nor the names of its
44  contributors may be used to endorse or promote products derived from
45  this software without specific prior written permission.
46
47  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
48  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
49  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
50  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
51  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
52  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
53  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
54  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
55  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
56  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
57  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
58  POSSIBILITY OF SUCH DAMAGE.]
59
60******************************************************************************/
61
62#include "util.h"
63#include "cuddInt.h"
64
65/*---------------------------------------------------------------------------*/
66/* Constant declarations                                                     */
67/*---------------------------------------------------------------------------*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Stucture declarations                                                     */
72/*---------------------------------------------------------------------------*/
73
74
75/*---------------------------------------------------------------------------*/
76/* Type declarations                                                         */
77/*---------------------------------------------------------------------------*/
78
79
80/*---------------------------------------------------------------------------*/
81/* Variable declarations                                                     */
82/*---------------------------------------------------------------------------*/
83
84#ifndef lint
85static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $";
86#endif
87
88/*---------------------------------------------------------------------------*/
89/* Macro declarations                                                        */
90/*---------------------------------------------------------------------------*/
91
92
93/**AutomaticStart*************************************************************/
94
95/*---------------------------------------------------------------------------*/
96/* Static function prototypes                                                */
97/*---------------------------------------------------------------------------*/
98
99static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected);
100static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth);
101
102/**AutomaticEnd***************************************************************/
103
104
105/*---------------------------------------------------------------------------*/
106/* Definition of exported functions                                          */
107/*---------------------------------------------------------------------------*/
108
109
110/**Function********************************************************************
111
112  Synopsis [Converts a BDD into a ZDD.]
113
114  Description [Converts a BDD into a ZDD. This function assumes that
115  there is a one-to-one correspondence between the BDD variables and the
116  ZDD variables, and that the variable order is the same for both types
117  of variables. These conditions are established if the ZDD variables
118  are created by one call to Cudd_zddVarsFromBddVars with multiplicity =
119  1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]
120
121  SideEffects [None]
122
123  SeeAlso     [Cudd_zddVarsFromBddVars]
124
125******************************************************************************/
126DdNode *
127Cudd_zddPortFromBdd(
128  DdManager * dd,
129  DdNode * B)
130{
131    DdNode *res;
132
133    do {
134        dd->reordered = 0;
135        res = zddPortFromBddStep(dd,B,0);
136    } while (dd->reordered == 1);
137
138    return(res);
139
140} /* end of Cudd_zddPortFromBdd */
141
142
143/**Function********************************************************************
144
145  Synopsis [Converts a ZDD into a BDD.]
146
147  Description [Converts a ZDD into a BDD. Returns a pointer to the resulting
148  ZDD if successful; NULL otherwise.]
149
150  SideEffects [None]
151
152  SeeAlso     [Cudd_zddPortFromBdd]
153
154******************************************************************************/
155DdNode *
156Cudd_zddPortToBdd(
157  DdManager * dd,
158  DdNode * f)
159{
160    DdNode *res;
161
162    do {
163        dd->reordered = 0;
164        res = zddPortToBddStep(dd,f,0);
165    } while (dd->reordered == 1);
166
167    return(res);
168
169} /* end of Cudd_zddPortToBdd */
170
171
172/*---------------------------------------------------------------------------*/
173/* Definition of internal functions                                          */
174/*---------------------------------------------------------------------------*/
175
176/*---------------------------------------------------------------------------*/
177/* Definition of static functions                                            */
178/*---------------------------------------------------------------------------*/
179
180
181/**Function********************************************************************
182
183  Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]
184
185  Description []
186
187  SideEffects [None]
188
189  SeeAlso     []
190
191******************************************************************************/
192static DdNode *
193zddPortFromBddStep(
194  DdManager * dd,
195  DdNode * B,
196  int  expected)
197{
198    DdNode      *res, *prevZdd, *t, *e;
199    DdNode      *Breg, *Bt, *Be;
200    int         id, level;
201
202    statLine(dd);
203    /* Terminal cases. */
204    if (B == Cudd_Not(DD_ONE(dd)))
205        return(DD_ZERO(dd));
206    if (B == DD_ONE(dd)) {
207        if (expected >= dd->sizeZ) {
208            return(DD_ONE(dd));
209        } else {
210            return(dd->univ[expected]);
211        }
212    }
213
214    Breg = Cudd_Regular(B);
215
216    /* Computed table look-up. */
217    res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
218    if (res != NULL) {
219        level = cuddI(dd,Breg->index);
220        /* Adding DC vars. */
221        if (expected < level) {
222            /* Add suppressed variables. */
223            cuddRef(res);
224            for (level--; level >= expected; level--) {
225                prevZdd = res;
226                id = dd->invperm[level];
227                res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
228                if (res == NULL) {
229                    Cudd_RecursiveDerefZdd(dd, prevZdd);
230                    return(NULL);
231                }
232                cuddRef(res);
233                Cudd_RecursiveDerefZdd(dd, prevZdd);
234            }
235            cuddDeref(res);
236        }
237        return(res);
238    }   /* end of cache look-up */
239
240    if (Cudd_IsComplement(B)) {
241        Bt = Cudd_Not(cuddT(Breg));
242        Be = Cudd_Not(cuddE(Breg));
243    } else {
244        Bt = cuddT(Breg);
245        Be = cuddE(Breg);
246    }
247
248    id = Breg->index;
249    level = cuddI(dd,id);
250    t = zddPortFromBddStep(dd, Bt, level+1);
251    if (t == NULL) return(NULL);
252    cuddRef(t);
253    e = zddPortFromBddStep(dd, Be, level+1);
254    if (e == NULL) {
255        Cudd_RecursiveDerefZdd(dd, t);
256        return(NULL);
257    }
258    cuddRef(e);
259    res = cuddZddGetNode(dd, id, t, e);
260    if (res == NULL) {
261        Cudd_RecursiveDerefZdd(dd, t);
262        Cudd_RecursiveDerefZdd(dd, e);
263        return(NULL);
264    }
265    cuddRef(res);
266    Cudd_RecursiveDerefZdd(dd, t);
267    Cudd_RecursiveDerefZdd(dd, e);
268
269    cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
270
271    for (level--; level >= expected; level--) {
272        prevZdd = res;
273        id = dd->invperm[level];
274        res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
275        if (res == NULL) {
276            Cudd_RecursiveDerefZdd(dd, prevZdd);
277            return(NULL);
278        }
279        cuddRef(res);
280        Cudd_RecursiveDerefZdd(dd, prevZdd);
281    }
282
283    cuddDeref(res);
284    return(res);
285
286} /* end of zddPortFromBddStep */
287
288
289/**Function********************************************************************
290
291  Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]
292
293  Description []
294
295  SideEffects [None]
296
297  SeeAlso     []
298
299******************************************************************************/
300static DdNode *
301zddPortToBddStep(
302  DdManager * dd /* manager */,
303  DdNode * f /* ZDD to be converted */,
304  int  depth /* recursion depth */)
305{
306    DdNode *one, *zero, *T, *E, *res, *var;
307    unsigned int index;
308    unsigned int level;
309
310    statLine(dd);
311    one = DD_ONE(dd);
312    zero = DD_ZERO(dd);
313    if (f == zero) return(Cudd_Not(one));
314
315    if (depth == dd->sizeZ) return(one);
316
317    index = dd->invpermZ[depth];
318    level = cuddIZ(dd,f->index);
319    var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
320    if (var == NULL) return(NULL);
321    cuddRef(var);
322
323    if (level > (unsigned) depth) {
324        E = zddPortToBddStep(dd,f,depth+1);
325        if (E == NULL) {
326            Cudd_RecursiveDeref(dd,var);
327            return(NULL);
328        }
329        cuddRef(E);
330        res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
331        if (res == NULL) {
332            Cudd_RecursiveDeref(dd,var);
333            Cudd_RecursiveDeref(dd,E);
334            return(NULL);
335        }
336        cuddRef(res);
337        Cudd_RecursiveDeref(dd,var);
338        Cudd_RecursiveDeref(dd,E);
339        cuddDeref(res);
340        return(res);
341    }
342
343    res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
344    if (res != NULL) {
345        Cudd_RecursiveDeref(dd,var);
346        return(res);
347    }
348
349    T = zddPortToBddStep(dd,cuddT(f),depth+1);
350    if (T == NULL) {
351        Cudd_RecursiveDeref(dd,var);
352        return(NULL);
353    }
354    cuddRef(T);
355    E = zddPortToBddStep(dd,cuddE(f),depth+1);
356    if (E == NULL) {
357        Cudd_RecursiveDeref(dd,var);
358        Cudd_RecursiveDeref(dd,T);
359        return(NULL);
360    }
361    cuddRef(E);
362
363    res = cuddBddIteRecur(dd,var,T,E);
364    if (res == NULL) {
365        Cudd_RecursiveDeref(dd,var);
366        Cudd_RecursiveDeref(dd,T);
367        Cudd_RecursiveDeref(dd,E);
368        return(NULL);
369    }
370    cuddRef(res);
371    Cudd_RecursiveDeref(dd,var);
372    Cudd_RecursiveDeref(dd,T);
373    Cudd_RecursiveDeref(dd,E);
374    cuddDeref(res);
375
376    cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
377
378    return(res);
379
380} /* end of zddPortToBddStep */
381
Note: See TracBrowser for help on using the repository browser.