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

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

library glu 2.3
File size: 11.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddAndAbs.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Combined AND and existential abstraction for BDDs]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_bddAndAbstract()
12                <li> Cudd_bddAndAbstractLimit()
13                </ul>
14            Internal procedures included in this module:
15                <ul>
16                <li> cuddBddAndAbstractRecur()
17                </ul>]
18
19  Author      [Fabio Somenzi]
20
21  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
22
23  All rights reserved.
24
25  Redistribution and use in source and binary forms, with or without
26  modification, are permitted provided that the following conditions
27  are met:
28
29  Redistributions of source code must retain the above copyright
30  notice, this list of conditions and the following disclaimer.
31
32  Redistributions in binary form must reproduce the above copyright
33  notice, this list of conditions and the following disclaimer in the
34  documentation and/or other materials provided with the distribution.
35
36  Neither the name of the University of Colorado nor the names of its
37  contributors may be used to endorse or promote products derived from
38  this software without specific prior written permission.
39
40  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
41  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
42  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
43  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
44  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
45  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
46  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
47  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
48  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
49  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
50  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
51  POSSIBILITY OF SUCH DAMAGE.]
52
53******************************************************************************/
54
55#include "util.h"
56#include "cuddInt.h"
57
58
59/*---------------------------------------------------------------------------*/
60/* Constant declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Stucture declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68
69/*---------------------------------------------------------------------------*/
70/* Type declarations                                                         */
71/*---------------------------------------------------------------------------*/
72
73
74/*---------------------------------------------------------------------------*/
75/* Variable declarations                                                     */
76/*---------------------------------------------------------------------------*/
77
78#ifndef lint
79static char rcsid[] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.19 2004/08/13 18:04:46 fabio Exp $";
80#endif
81
82
83/*---------------------------------------------------------------------------*/
84/* Macro declarations                                                        */
85/*---------------------------------------------------------------------------*/
86
87
88/**AutomaticStart*************************************************************/
89
90/*---------------------------------------------------------------------------*/
91/* Static function prototypes                                                */
92/*---------------------------------------------------------------------------*/
93
94
95/**AutomaticEnd***************************************************************/
96
97
98/*---------------------------------------------------------------------------*/
99/* Definition of exported functions                                          */
100/*---------------------------------------------------------------------------*/
101
102
103/**Function********************************************************************
104
105  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
106  variables in cube.]
107
108  Description [Takes the AND of two BDDs and simultaneously abstracts
109  the variables in cube. The variables are existentially abstracted.
110  Returns a pointer to the result is successful; NULL otherwise.
111  Cudd_bddAndAbstract implements the semiring matrix multiplication
112  algorithm for the boolean semiring.]
113
114  SideEffects [None]
115
116  SeeAlso     [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]
117
118******************************************************************************/
119DdNode *
120Cudd_bddAndAbstract(
121  DdManager * manager,
122  DdNode * f,
123  DdNode * g,
124  DdNode * cube)
125{
126    DdNode *res;
127
128    do {
129        manager->reordered = 0;
130        res = cuddBddAndAbstractRecur(manager, f, g, cube);
131    } while (manager->reordered == 1);
132    return(res);
133
134} /* end of Cudd_bddAndAbstract */
135
136
137/**Function********************************************************************
138
139  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
140  variables in cube.  Returns NULL if too many nodes are required.]
141
142  Description [Takes the AND of two BDDs and simultaneously abstracts
143  the variables in cube. The variables are existentially abstracted.
144  Returns a pointer to the result is successful; NULL otherwise.
145  In particular, if the number of new nodes created exceeds
146  <code>limit</code>, this function returns NULL.]
147
148  SideEffects [None]
149
150  SeeAlso     [Cudd_bddAndAbstract]
151
152******************************************************************************/
153DdNode *
154Cudd_bddAndAbstractLimit(
155  DdManager * manager,
156  DdNode * f,
157  DdNode * g,
158  DdNode * cube,
159  unsigned int limit)
160{
161    DdNode *res;
162    unsigned int saveLimit = manager->maxLive;
163
164    manager->maxLive = (manager->keys - manager->dead) +
165      (manager->keysZ - manager->deadZ) + limit;
166    do {
167        manager->reordered = 0;
168        res = cuddBddAndAbstractRecur(manager, f, g, cube);
169    } while (manager->reordered == 1);
170    manager->maxLive = saveLimit;
171    return(res);
172
173} /* end of Cudd_bddAndAbstractLimit */
174
175
176/*---------------------------------------------------------------------------*/
177/* Definition of internal functions                                          */
178/*---------------------------------------------------------------------------*/
179
180
181/**Function********************************************************************
182
183  Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
184  variables in cube.]
185
186  Description [Takes the AND of two BDDs and simultaneously abstracts
187  the variables in cube. The variables are existentially abstracted.
188  Returns a pointer to the result is successful; NULL otherwise.]
189
190  SideEffects [None]
191
192  SeeAlso     [Cudd_bddAndAbstract]
193
194******************************************************************************/
195DdNode *
196cuddBddAndAbstractRecur(
197  DdManager * manager,
198  DdNode * f,
199  DdNode * g,
200  DdNode * cube)
201{
202    DdNode *F, *ft, *fe, *G, *gt, *ge;
203    DdNode *one, *zero, *r, *t, *e;
204    unsigned int topf, topg, topcube, top, index;
205
206    statLine(manager);
207    one = DD_ONE(manager);
208    zero = Cudd_Not(one);
209
210    /* Terminal cases. */
211    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
212    if (f == one && g == one)   return(one);
213
214    if (cube == one) {
215        return(cuddBddAndRecur(manager, f, g));
216    }
217    if (f == one || f == g) {
218        return(cuddBddExistAbstractRecur(manager, g, cube));
219    }
220    if (g == one) {
221        return(cuddBddExistAbstractRecur(manager, f, cube));
222    }
223    /* At this point f, g, and cube are not constant. */
224
225    if (f > g) { /* Try to increase cache efficiency. */
226        DdNode *tmp = f;
227        f = g;
228        g = tmp;
229    }
230
231    /* Here we can skip the use of cuddI, because the operands are known
232    ** to be non-constant.
233    */
234    F = Cudd_Regular(f);
235    G = Cudd_Regular(g);
236    topf = manager->perm[F->index];
237    topg = manager->perm[G->index];
238    top = ddMin(topf, topg);
239    topcube = manager->perm[cube->index];
240
241    while (topcube < top) {
242        cube = cuddT(cube);
243        if (cube == one) {
244            return(cuddBddAndRecur(manager, f, g));
245        }
246        topcube = manager->perm[cube->index];
247    }
248    /* Now, topcube >= top. */
249
250    /* Check cache. */
251    if (F->ref != 1 || G->ref != 1) {
252        r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
253        if (r != NULL) {
254            return(r);
255        }
256    }
257
258    if (topf == top) {
259        index = F->index;
260        ft = cuddT(F);
261        fe = cuddE(F);
262        if (Cudd_IsComplement(f)) {
263            ft = Cudd_Not(ft);
264            fe = Cudd_Not(fe);
265        }
266    } else {
267        index = G->index;
268        ft = fe = f;
269    }
270
271    if (topg == top) {
272        gt = cuddT(G);
273        ge = cuddE(G);
274        if (Cudd_IsComplement(g)) {
275            gt = Cudd_Not(gt);
276            ge = Cudd_Not(ge);
277        }
278    } else {
279        gt = ge = g;
280    }
281
282    if (topcube == top) {       /* quantify */
283        DdNode *Cube = cuddT(cube);
284        t = cuddBddAndAbstractRecur(manager, ft, gt, Cube);
285        if (t == NULL) return(NULL);
286        /* Special case: 1 OR anything = 1. Hence, no need to compute
287        ** the else branch if t is 1. Likewise t + t * anything == t.
288        ** Notice that t == fe implies that fe does not depend on the
289        ** variables in Cube. Likewise for t == ge.
290        */
291        if (t == one || t == fe || t == ge) {
292            if (F->ref != 1 || G->ref != 1)
293                cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
294                                f, g, cube, t);
295            return(t);
296        }
297        cuddRef(t);
298        /* Special case: t + !t * anything == t + anything. */
299        if (t == Cudd_Not(fe)) {
300            e = cuddBddExistAbstractRecur(manager, ge, Cube);
301        } else if (t == Cudd_Not(ge)) {
302            e = cuddBddExistAbstractRecur(manager, fe, Cube);
303        } else {
304            e = cuddBddAndAbstractRecur(manager, fe, ge, Cube);
305        }
306        if (e == NULL) {
307            Cudd_IterDerefBdd(manager, t);
308            return(NULL);
309        }
310        if (t == e) {
311            r = t;
312            cuddDeref(t);
313        } else {
314            cuddRef(e);
315            r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
316            if (r == NULL) {
317                Cudd_IterDerefBdd(manager, t);
318                Cudd_IterDerefBdd(manager, e);
319                return(NULL);
320            }
321            r = Cudd_Not(r);
322            cuddRef(r);
323            Cudd_DelayedDerefBdd(manager, t);
324            Cudd_DelayedDerefBdd(manager, e);
325            cuddDeref(r);
326        }
327    } else {
328        t = cuddBddAndAbstractRecur(manager, ft, gt, cube);
329        if (t == NULL) return(NULL);
330        cuddRef(t);
331        e = cuddBddAndAbstractRecur(manager, fe, ge, cube);
332        if (e == NULL) {
333            Cudd_IterDerefBdd(manager, t);
334            return(NULL);
335        }
336        if (t == e) {
337            r = t;
338            cuddDeref(t);
339        } else {
340            cuddRef(e);
341            if (Cudd_IsComplement(t)) {
342                r = cuddUniqueInter(manager, (int) index,
343                                    Cudd_Not(t), Cudd_Not(e));
344                if (r == NULL) {
345                    Cudd_IterDerefBdd(manager, t);
346                    Cudd_IterDerefBdd(manager, e);
347                    return(NULL);
348                }
349                r = Cudd_Not(r);
350            } else {
351                r = cuddUniqueInter(manager,(int)index,t,e);
352                if (r == NULL) {
353                    Cudd_IterDerefBdd(manager, t);
354                    Cudd_IterDerefBdd(manager, e);
355                    return(NULL);
356                }
357            }
358            cuddDeref(e);
359            cuddDeref(t);
360        }
361    }
362
363    if (F->ref != 1 || G->ref != 1)
364        cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
365    return (r);
366
367} /* end of cuddBddAndAbstractRecur */
368
369
370/*---------------------------------------------------------------------------*/
371/* Definition of static functions                                            */
372/*---------------------------------------------------------------------------*/
373
Note: See TracBrowser for help on using the repository browser.