source: vis_dev/glu-2.3/src/cuBdd/cuddClip.c @ 88

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

library glu 2.3
File size: 16.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddClip.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Clipping functions.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_bddClippingAnd()
12                <li> Cudd_bddClippingAndAbstract()
13                </ul>
14       Internal procedures included in this module:
15                <ul>
16                <li> cuddBddClippingAnd()
17                <li> cuddBddClippingAndAbstract()
18                </ul>
19       Static procedures included in this module:
20                <ul>
21                <li> cuddBddClippingAndRecur()
22                <li> cuddBddClipAndAbsRecur()
23                </ul>
24
25  SeeAlso     []
26
27  Author      [Fabio Somenzi]
28
29  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
30
31  All rights reserved.
32
33  Redistribution and use in source and binary forms, with or without
34  modification, are permitted provided that the following conditions
35  are met:
36
37  Redistributions of source code must retain the above copyright
38  notice, this list of conditions and the following disclaimer.
39
40  Redistributions in binary form must reproduce the above copyright
41  notice, this list of conditions and the following disclaimer in the
42  documentation and/or other materials provided with the distribution.
43
44  Neither the name of the University of Colorado nor the names of its
45  contributors may be used to endorse or promote products derived from
46  this software without specific prior written permission.
47
48  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
49  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
50  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
51  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
52  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
53  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
54  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
55  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
56  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
57  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
58  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
59  POSSIBILITY OF SUCH DAMAGE.]
60
61******************************************************************************/
62
63#include "util.h"
64#include "cuddInt.h"
65
66
67/*---------------------------------------------------------------------------*/
68/* Constant declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Stucture declarations                                                     */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Type declarations                                                         */
79/*---------------------------------------------------------------------------*/
80
81/*---------------------------------------------------------------------------*/
82/* Variable declarations                                                     */
83/*---------------------------------------------------------------------------*/
84
85#ifndef lint
86static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
87#endif
88
89/*---------------------------------------------------------------------------*/
90/* Macro declarations                                                        */
91/*---------------------------------------------------------------------------*/
92
93
94/**AutomaticStart*************************************************************/
95
96/*---------------------------------------------------------------------------*/
97/* Static function prototypes                                                */
98/*---------------------------------------------------------------------------*/
99
100static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
101static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
102
103/**AutomaticEnd***************************************************************/
104
105
106/*---------------------------------------------------------------------------*/
107/* Definition of exported functions                                          */
108/*---------------------------------------------------------------------------*/
109
110
111/**Function********************************************************************
112
113  Synopsis    [Approximates the conjunction of two BDDs f and g.]
114
115  Description [Approximates the conjunction of two BDDs f and g. Returns a
116  pointer to the resulting BDD if successful; NULL if the intermediate
117  result blows up.]
118
119  SideEffects [None]
120
121  SeeAlso     [Cudd_bddAnd]
122
123******************************************************************************/
124DdNode *
125Cudd_bddClippingAnd(
126  DdManager * dd /* manager */,
127  DdNode * f /* first conjunct */,
128  DdNode * g /* second conjunct */,
129  int  maxDepth /* maximum recursion depth */,
130  int  direction /* under (0) or over (1) approximation */)
131{
132    DdNode *res;
133
134    do {
135        dd->reordered = 0;
136        res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
137    } while (dd->reordered == 1);
138    return(res);
139
140} /* end of Cudd_bddClippingAnd */
141
142
143/**Function********************************************************************
144
145  Synopsis    [Approximates the conjunction of two BDDs f and g and
146  simultaneously abstracts the variables in cube.]
147
148  Description [Approximates the conjunction of two BDDs f and g and
149  simultaneously abstracts the variables in cube. The variables are
150  existentially abstracted. Returns a pointer to the resulting BDD if
151  successful; NULL if the intermediate result blows up.]
152
153  SideEffects [None]
154
155  SeeAlso     [Cudd_bddAndAbstract Cudd_bddClippingAnd]
156
157******************************************************************************/
158DdNode *
159Cudd_bddClippingAndAbstract(
160  DdManager * dd /* manager */,
161  DdNode * f /* first conjunct */,
162  DdNode * g /* second conjunct */,
163  DdNode * cube /* cube of variables to be abstracted */,
164  int  maxDepth /* maximum recursion depth */,
165  int  direction /* under (0) or over (1) approximation */)
166{
167    DdNode *res;
168
169    do {
170        dd->reordered = 0;
171        res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
172    } while (dd->reordered == 1);
173    return(res);
174
175} /* end of Cudd_bddClippingAndAbstract */
176
177
178/*---------------------------------------------------------------------------*/
179/* Definition of internal functions                                          */
180/*---------------------------------------------------------------------------*/
181
182
183/**Function********************************************************************
184
185  Synopsis    [Approximates the conjunction of two BDDs f and g.]
186
187  Description [Approximates the conjunction of two BDDs f and g. Returns a
188  pointer to the resulting BDD if successful; NULL if the intermediate
189  result blows up.]
190
191  SideEffects [None]
192
193  SeeAlso     [Cudd_bddClippingAnd]
194
195******************************************************************************/
196DdNode *
197cuddBddClippingAnd(
198  DdManager * dd /* manager */,
199  DdNode * f /* first conjunct */,
200  DdNode * g /* second conjunct */,
201  int  maxDepth /* maximum recursion depth */,
202  int  direction /* under (0) or over (1) approximation */)
203{
204    DdNode *res;
205
206    res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
207
208    return(res);
209
210} /* end of cuddBddClippingAnd */
211
212
213/**Function********************************************************************
214
215  Synopsis    [Approximates the conjunction of two BDDs f and g and
216  simultaneously abstracts the variables in cube.]
217
218  Description [Approximates the conjunction of two BDDs f and g and
219  simultaneously abstracts the variables in cube. Returns a
220  pointer to the resulting BDD if successful; NULL if the intermediate
221  result blows up.]
222
223  SideEffects [None]
224
225  SeeAlso     [Cudd_bddClippingAndAbstract]
226
227******************************************************************************/
228DdNode *
229cuddBddClippingAndAbstract(
230  DdManager * dd /* manager */,
231  DdNode * f /* first conjunct */,
232  DdNode * g /* second conjunct */,
233  DdNode * cube /* cube of variables to be abstracted */,
234  int  maxDepth /* maximum recursion depth */,
235  int  direction /* under (0) or over (1) approximation */)
236{
237    DdNode *res;
238
239    res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
240
241    return(res);
242
243} /* end of cuddBddClippingAndAbstract */
244
245
246/*---------------------------------------------------------------------------*/
247/* Definition of static functions                                            */
248/*---------------------------------------------------------------------------*/
249
250
251/**Function********************************************************************
252
253  Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]
254
255  Description [Implements the recursive step of Cudd_bddClippingAnd by taking
256  the conjunction of two BDDs.  Returns a pointer to the result is
257  successful; NULL otherwise.]
258
259  SideEffects [None]
260
261  SeeAlso     [cuddBddClippingAnd]
262
263******************************************************************************/
264static DdNode *
265cuddBddClippingAndRecur(
266  DdManager * manager,
267  DdNode * f,
268  DdNode * g,
269  int  distance,
270  int  direction)
271{
272    DdNode *F, *ft, *fe, *G, *gt, *ge;
273    DdNode *one, *zero, *r, *t, *e;
274    unsigned int topf, topg, index;
275    DD_CTFP cacheOp;
276
277    statLine(manager);
278    one = DD_ONE(manager);
279    zero = Cudd_Not(one);
280
281    /* Terminal cases. */
282    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
283    if (f == g || g == one) return(f);
284    if (f == one) return(g);
285    if (distance == 0) {
286        /* One last attempt at returning the right result. We sort of
287        ** cheat by calling Cudd_bddLeq. */
288        if (Cudd_bddLeq(manager,f,g)) return(f);
289        if (Cudd_bddLeq(manager,g,f)) return(g);
290        if (direction == 1) {
291            if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
292                Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
293        }
294        return(Cudd_NotCond(one,(direction == 0)));
295    }
296
297    /* At this point f and g are not constant. */
298    distance--;
299
300    /* Check cache. Try to increase cache efficiency by sorting the
301    ** pointers. */
302    if (f > g) {
303        DdNode *tmp = f;
304        f = g; g = tmp;
305    }
306    F = Cudd_Regular(f);
307    G = Cudd_Regular(g);
308    cacheOp = (DD_CTFP)
309        (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
310    if (F->ref != 1 || G->ref != 1) {
311        r = cuddCacheLookup2(manager, cacheOp, f, g);
312        if (r != NULL) return(r);
313    }
314
315    /* Here we can skip the use of cuddI, because the operands are known
316    ** to be non-constant.
317    */
318    topf = manager->perm[F->index];
319    topg = manager->perm[G->index];
320
321    /* Compute cofactors. */
322    if (topf <= topg) {
323        index = F->index;
324        ft = cuddT(F);
325        fe = cuddE(F);
326        if (Cudd_IsComplement(f)) {
327            ft = Cudd_Not(ft);
328            fe = Cudd_Not(fe);
329        }
330    } else {
331        index = G->index;
332        ft = fe = f;
333    }
334
335    if (topg <= topf) {
336        gt = cuddT(G);
337        ge = cuddE(G);
338        if (Cudd_IsComplement(g)) {
339            gt = Cudd_Not(gt);
340            ge = Cudd_Not(ge);
341        }
342    } else {
343        gt = ge = g;
344    }
345
346    t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
347    if (t == NULL) return(NULL);
348    cuddRef(t);
349    e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
350    if (e == NULL) {
351        Cudd_RecursiveDeref(manager, t);
352        return(NULL);
353    }
354    cuddRef(e);
355
356    if (t == e) {
357        r = t;
358    } else {
359        if (Cudd_IsComplement(t)) {
360            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
361            if (r == NULL) {
362                Cudd_RecursiveDeref(manager, t);
363                Cudd_RecursiveDeref(manager, e);
364                return(NULL);
365            }
366            r = Cudd_Not(r);
367        } else {
368            r = cuddUniqueInter(manager,(int)index,t,e);
369            if (r == NULL) {
370                Cudd_RecursiveDeref(manager, t);
371                Cudd_RecursiveDeref(manager, e);
372                return(NULL);
373            }
374        }
375    }
376    cuddDeref(e);
377    cuddDeref(t);
378    if (F->ref != 1 || G->ref != 1)
379        cuddCacheInsert2(manager, cacheOp, f, g, r);
380    return(r);
381
382} /* end of cuddBddClippingAndRecur */
383
384
385/**Function********************************************************************
386
387  Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
388  variables in cube.]
389
390  Description [Approximates the AND of two BDDs and simultaneously
391  abstracts the variables in cube. The variables are existentially
392  abstracted.  Returns a pointer to the result is successful; NULL
393  otherwise.]
394
395  SideEffects [None]
396
397  SeeAlso     [Cudd_bddClippingAndAbstract]
398
399******************************************************************************/
400static DdNode *
401cuddBddClipAndAbsRecur(
402  DdManager * manager,
403  DdNode * f,
404  DdNode * g,
405  DdNode * cube,
406  int  distance,
407  int  direction)
408{
409    DdNode *F, *ft, *fe, *G, *gt, *ge;
410    DdNode *one, *zero, *r, *t, *e, *Cube;
411    unsigned int topf, topg, topcube, top, index;
412    ptruint cacheTag;
413
414    statLine(manager);
415    one = DD_ONE(manager);
416    zero = Cudd_Not(one);
417
418    /* Terminal cases. */
419    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
420    if (f == one && g == one)   return(one);
421    if (cube == one) {
422        return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
423    }
424    if (f == one || f == g) {
425        return (cuddBddExistAbstractRecur(manager, g, cube));
426    }
427    if (g == one) {
428        return (cuddBddExistAbstractRecur(manager, f, cube));
429    }
430    if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
431
432    /* At this point f, g, and cube are not constant. */
433    distance--;
434
435    /* Check cache. */
436    if (f > g) { /* Try to increase cache efficiency. */
437        DdNode *tmp = f;
438        f = g; g = tmp;
439    }
440    F = Cudd_Regular(f);
441    G = Cudd_Regular(g);
442    cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
443        DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
444    if (F->ref != 1 || G->ref != 1) {
445        r = cuddCacheLookup(manager, cacheTag,
446                            f, g, cube);
447        if (r != NULL) {
448            return(r);
449        }
450    }
451
452    /* Here we can skip the use of cuddI, because the operands are known
453    ** to be non-constant.
454    */
455    topf = manager->perm[F->index];
456    topg = manager->perm[G->index];
457    top = ddMin(topf, topg);
458    topcube = manager->perm[cube->index];
459
460    if (topcube < top) {
461        return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
462                                      distance, direction));
463    }
464    /* Now, topcube >= top. */
465
466    if (topf == top) {
467        index = F->index;
468        ft = cuddT(F);
469        fe = cuddE(F);
470        if (Cudd_IsComplement(f)) {
471            ft = Cudd_Not(ft);
472            fe = Cudd_Not(fe);
473        }
474    } else {
475        index = G->index;
476        ft = fe = f;
477    }
478
479    if (topg == top) {
480        gt = cuddT(G);
481        ge = cuddE(G);
482        if (Cudd_IsComplement(g)) {
483            gt = Cudd_Not(gt);
484            ge = Cudd_Not(ge);
485        }
486    } else {
487        gt = ge = g;
488    }
489
490    if (topcube == top) {
491        Cube = cuddT(cube);
492    } else {
493        Cube = cube;
494    }
495
496    t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
497    if (t == NULL) return(NULL);
498
499    /* Special case: 1 OR anything = 1. Hence, no need to compute
500    ** the else branch if t is 1.
501    */
502    if (t == one && topcube == top) {
503        if (F->ref != 1 || G->ref != 1)
504            cuddCacheInsert(manager, cacheTag, f, g, cube, one);
505        return(one);
506    }
507    cuddRef(t);
508
509    e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
510    if (e == NULL) {
511        Cudd_RecursiveDeref(manager, t);
512        return(NULL);
513    }
514    cuddRef(e);
515
516    if (topcube == top) {       /* abstract */
517        r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
518                                    distance, (direction == 0));
519        if (r == NULL) {
520            Cudd_RecursiveDeref(manager, t);
521            Cudd_RecursiveDeref(manager, e);
522            return(NULL);
523        }
524        r = Cudd_Not(r);
525        cuddRef(r);
526        Cudd_RecursiveDeref(manager, t);
527        Cudd_RecursiveDeref(manager, e);
528        cuddDeref(r);
529    } else if (t == e) {
530        r = t;
531        cuddDeref(t);
532        cuddDeref(e);
533    } else {
534        if (Cudd_IsComplement(t)) {
535            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
536            if (r == NULL) {
537                Cudd_RecursiveDeref(manager, t);
538                Cudd_RecursiveDeref(manager, e);
539                return(NULL);
540            }
541            r = Cudd_Not(r);
542        } else {
543            r = cuddUniqueInter(manager,(int)index,t,e);
544            if (r == NULL) {
545                Cudd_RecursiveDeref(manager, t);
546                Cudd_RecursiveDeref(manager, e);
547                return(NULL);
548            }
549        }
550        cuddDeref(e);
551        cuddDeref(t);
552    }
553    if (F->ref != 1 || G->ref != 1)
554        cuddCacheInsert(manager, cacheTag, f, g, cube, r);
555    return (r);
556
557} /* end of cuddBddClipAndAbsRecur */
558
Note: See TracBrowser for help on using the repository browser.