source: vis_dev/glu-2.3/src/cuBdd/cuddBddAbs.c @ 13

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

library glu 2.3
File size: 20.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddBddAbs.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Quantification functions for BDDs.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_bddExistAbstract()
12                <li> Cudd_bddXorExistAbstract()
13                <li> Cudd_bddUnivAbstract()
14                <li> Cudd_bddBooleanDiff()
15                <li> Cudd_bddVarIsDependent()
16                </ul>
17        Internal procedures included in this module:
18                <ul>
19                <li> cuddBddExistAbstractRecur()
20                <li> cuddBddXorExistAbstractRecur()
21                <li> cuddBddBooleanDiffRecur()
22                </ul>
23        Static procedures included in this module:
24                <ul>
25                <li> bddCheckPositiveCube()
26                </ul>
27                ]
28
29  Author      [Fabio Somenzi]
30
31  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
32
33  All rights reserved.
34
35  Redistribution and use in source and binary forms, with or without
36  modification, are permitted provided that the following conditions
37  are met:
38
39  Redistributions of source code must retain the above copyright
40  notice, this list of conditions and the following disclaimer.
41
42  Redistributions in binary form must reproduce the above copyright
43  notice, this list of conditions and the following disclaimer in the
44  documentation and/or other materials provided with the distribution.
45
46  Neither the name of the University of Colorado nor the names of its
47  contributors may be used to endorse or promote products derived from
48  this software without specific prior written permission.
49
50  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
51  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
52  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
53  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
54  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
55  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
56  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
57  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
58  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
59  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
60  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
61  POSSIBILITY OF SUCH DAMAGE.]
62
63******************************************************************************/
64
65#include "util.h"
66#include "cuddInt.h"
67
68
69/*---------------------------------------------------------------------------*/
70/* Constant declarations                                                     */
71/*---------------------------------------------------------------------------*/
72
73
74/*---------------------------------------------------------------------------*/
75/* Stucture declarations                                                     */
76/*---------------------------------------------------------------------------*/
77
78
79/*---------------------------------------------------------------------------*/
80/* Type declarations                                                         */
81/*---------------------------------------------------------------------------*/
82
83
84/*---------------------------------------------------------------------------*/
85/* Variable declarations                                                     */
86/*---------------------------------------------------------------------------*/
87
88#ifndef lint
89static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio Exp $";
90#endif
91
92/*---------------------------------------------------------------------------*/
93/* Macro declarations                                                        */
94/*---------------------------------------------------------------------------*/
95
96
97/**AutomaticStart*************************************************************/
98
99/*---------------------------------------------------------------------------*/
100/* Static function prototypes                                                */
101/*---------------------------------------------------------------------------*/
102
103static int bddCheckPositiveCube (DdManager *manager, DdNode *cube);
104
105/**AutomaticEnd***************************************************************/
106
107
108/*---------------------------------------------------------------------------*/
109/* Definition of exported functions                                          */
110/*---------------------------------------------------------------------------*/
111
112
113/**Function********************************************************************
114
115  Synopsis [Existentially abstracts all the variables in cube from f.]
116
117  Description [Existentially abstracts all the variables in cube from f.
118  Returns the abstracted BDD if successful; NULL otherwise.]
119
120  SideEffects [None]
121
122  SeeAlso     [Cudd_bddUnivAbstract Cudd_addExistAbstract]
123
124******************************************************************************/
125DdNode *
126Cudd_bddExistAbstract(
127  DdManager * manager,
128  DdNode * f,
129  DdNode * cube)
130{
131    DdNode *res;
132
133    if (bddCheckPositiveCube(manager, cube) == 0) {
134        (void) fprintf(manager->err,
135                       "Error: Can only abstract positive cubes\n");
136        manager->errorCode = CUDD_INVALID_ARG;
137        return(NULL);
138    }
139
140    do {
141        manager->reordered = 0;
142        res = cuddBddExistAbstractRecur(manager, f, cube);
143    } while (manager->reordered == 1);
144
145    return(res);
146
147} /* end of Cudd_bddExistAbstract */
148
149
150/**Function********************************************************************
151
152  Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
153  variables in cube.]
154
155  Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
156  the variables in cube. The variables are existentially abstracted.  Returns a
157  pointer to the result is successful; NULL otherwise.]
158
159  SideEffects [None]
160
161  SeeAlso     [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]
162
163******************************************************************************/
164DdNode *
165Cudd_bddXorExistAbstract(
166  DdManager * manager,
167  DdNode * f,
168  DdNode * g,
169  DdNode * cube)
170{
171    DdNode *res;
172
173    if (bddCheckPositiveCube(manager, cube) == 0) {
174        (void) fprintf(manager->err,
175                       "Error: Can only abstract positive cubes\n");
176        manager->errorCode = CUDD_INVALID_ARG;
177        return(NULL);
178    }
179
180    do {
181        manager->reordered = 0;
182        res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
183    } while (manager->reordered == 1);
184
185    return(res);
186
187} /* end of Cudd_bddXorExistAbstract */
188
189
190/**Function********************************************************************
191
192  Synopsis    [Universally abstracts all the variables in cube from f.]
193
194  Description [Universally abstracts all the variables in cube from f.
195  Returns the abstracted BDD if successful; NULL otherwise.]
196
197  SideEffects [None]
198
199  SeeAlso     [Cudd_bddExistAbstract Cudd_addUnivAbstract]
200
201******************************************************************************/
202DdNode *
203Cudd_bddUnivAbstract(
204  DdManager * manager,
205  DdNode * f,
206  DdNode * cube)
207{
208    DdNode      *res;
209
210    if (bddCheckPositiveCube(manager, cube) == 0) {
211        (void) fprintf(manager->err,
212                       "Error: Can only abstract positive cubes\n");
213        manager->errorCode = CUDD_INVALID_ARG;
214        return(NULL);
215    }
216
217    do {
218        manager->reordered = 0;
219        res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
220    } while (manager->reordered == 1);
221    if (res != NULL) res = Cudd_Not(res);
222
223    return(res);
224
225} /* end of Cudd_bddUnivAbstract */
226
227
228/**Function********************************************************************
229
230  Synopsis    [Computes the boolean difference of f with respect to x.]
231
232  Description [Computes the boolean difference of f with respect to the
233  variable with index x.  Returns the BDD of the boolean difference if
234  successful; NULL otherwise.]
235
236  SideEffects [None]
237
238  SeeAlso     []
239
240******************************************************************************/
241DdNode *
242Cudd_bddBooleanDiff(
243  DdManager * manager,
244  DdNode * f,
245  int  x)
246{
247    DdNode *res, *var;
248
249    /* If the variable is not currently in the manager, f cannot
250    ** depend on it.
251    */
252    if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
253    var = manager->vars[x];
254
255    do {
256        manager->reordered = 0;
257        res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
258    } while (manager->reordered == 1);
259
260    return(res);
261
262} /* end of Cudd_bddBooleanDiff */
263
264
265/**Function********************************************************************
266
267  Synopsis    [Checks whether a variable is dependent on others in a
268  function.]
269
270  Description [Checks whether a variable is dependent on others in a
271  function.  Returns 1 if the variable is dependent; 0 otherwise. No
272  new nodes are created.]
273
274  SideEffects [None]
275
276  SeeAlso     []
277
278******************************************************************************/
279int
280Cudd_bddVarIsDependent(
281  DdManager *dd,                /* manager */
282  DdNode *f,                    /* function */
283  DdNode *var                   /* variable */)
284{
285    DdNode *F, *res, *zero, *ft, *fe;
286    unsigned topf, level;
287    DD_CTFP cacheOp;
288    int retval;
289
290    zero = Cudd_Not(DD_ONE(dd));
291    if (Cudd_IsConstant(f)) return(f == zero);
292
293    /* From now on f is not constant. */
294    F = Cudd_Regular(f);
295    topf = (unsigned) dd->perm[F->index];
296    level = (unsigned) dd->perm[var->index];
297
298    /* Check terminal case. If topf > index of var, f does not depend on var.
299    ** Therefore, var is not dependent in f. */
300    if (topf > level) {
301        return(0);
302    }
303
304    cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
305    res = cuddCacheLookup2(dd,cacheOp,f,var);
306    if (res != NULL) {
307        return(res != zero);
308    }
309
310    /* Compute cofactors. */
311    ft = Cudd_NotCond(cuddT(F), f != F);
312    fe = Cudd_NotCond(cuddE(F), f != F);
313
314    if (topf == level) {
315        retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
316    } else {
317        retval = Cudd_bddVarIsDependent(dd,ft,var) &&
318            Cudd_bddVarIsDependent(dd,fe,var);
319    }
320
321    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
322
323    return(retval);
324
325} /* Cudd_bddVarIsDependent */
326
327
328/*---------------------------------------------------------------------------*/
329/* Definition of internal functions                                          */
330/*---------------------------------------------------------------------------*/
331
332
333/**Function********************************************************************
334
335  Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]
336
337  Description [Performs the recursive steps of Cudd_bddExistAbstract.
338  Returns the BDD obtained by abstracting the variables
339  of cube from f if successful; NULL otherwise. It is also used by
340  Cudd_bddUnivAbstract.]
341
342  SideEffects [None]
343
344  SeeAlso     [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
345
346******************************************************************************/
347DdNode *
348cuddBddExistAbstractRecur(
349  DdManager * manager,
350  DdNode * f,
351  DdNode * cube)
352{
353    DdNode      *F, *T, *E, *res, *res1, *res2, *one;
354
355    statLine(manager);
356    one = DD_ONE(manager);
357    F = Cudd_Regular(f);
358
359    /* Cube is guaranteed to be a cube at this point. */       
360    if (cube == one || F == one) { 
361        return(f);
362    }
363    /* From now on, f and cube are non-constant. */
364
365    /* Abstract a variable that does not appear in f. */
366    while (manager->perm[F->index] > manager->perm[cube->index]) {
367        cube = cuddT(cube);
368        if (cube == one) return(f);
369    }
370
371    /* Check the cache. */
372    if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
373        return(res);
374    }
375
376    /* Compute the cofactors of f. */
377    T = cuddT(F); E = cuddE(F);
378    if (f != F) {
379        T = Cudd_Not(T); E = Cudd_Not(E);
380    }
381
382    /* If the two indices are the same, so are their levels. */
383    if (F->index == cube->index) {
384        if (T == one || E == one || T == Cudd_Not(E)) {
385            return(one);
386        }
387        res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
388        if (res1 == NULL) return(NULL);
389        if (res1 == one) {
390            if (F->ref != 1)
391                cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
392            return(one);
393        }
394        cuddRef(res1);
395        res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
396        if (res2 == NULL) {
397            Cudd_IterDerefBdd(manager,res1);
398            return(NULL);
399        }
400        cuddRef(res2);
401        res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
402        if (res == NULL) {
403            Cudd_IterDerefBdd(manager, res1);
404            Cudd_IterDerefBdd(manager, res2);
405            return(NULL);
406        }
407        res = Cudd_Not(res);
408        cuddRef(res);
409        Cudd_IterDerefBdd(manager, res1);
410        Cudd_IterDerefBdd(manager, res2);
411        if (F->ref != 1)
412            cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
413        cuddDeref(res);
414        return(res);
415    } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
416        res1 = cuddBddExistAbstractRecur(manager, T, cube);
417        if (res1 == NULL) return(NULL);
418        cuddRef(res1);
419        res2 = cuddBddExistAbstractRecur(manager, E, cube);
420        if (res2 == NULL) {
421            Cudd_IterDerefBdd(manager, res1);
422            return(NULL);
423        }
424        cuddRef(res2);
425        /* ITE takes care of possible complementation of res1 and of the
426        ** case in which res1 == res2. */
427        res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
428        if (res == NULL) {
429            Cudd_IterDerefBdd(manager, res1);
430            Cudd_IterDerefBdd(manager, res2);
431            return(NULL);
432        }
433        cuddDeref(res1);
434        cuddDeref(res2);
435        if (F->ref != 1)
436            cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
437        return(res);
438    }       
439
440} /* end of cuddBddExistAbstractRecur */
441
442
443/**Function********************************************************************
444
445  Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
446  variables in cube.]
447
448  Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
449  the variables in cube. The variables are existentially abstracted.  Returns a
450  pointer to the result is successful; NULL otherwise.]
451
452  SideEffects [None]
453
454  SeeAlso     [Cudd_bddAndAbstract]
455
456******************************************************************************/
457DdNode *
458cuddBddXorExistAbstractRecur(
459  DdManager * manager,
460  DdNode * f,
461  DdNode * g,
462  DdNode * cube)
463{
464    DdNode *F, *fv, *fnv, *G, *gv, *gnv;
465    DdNode *one, *zero, *r, *t, *e, *Cube;
466    unsigned int topf, topg, topcube, top, index;
467
468    statLine(manager);
469    one = DD_ONE(manager);
470    zero = Cudd_Not(one);
471
472    /* Terminal cases. */
473    if (f == g) {
474        return(zero);
475    }
476    if (f == Cudd_Not(g)) {
477        return(one);
478    }
479    if (cube == one) {
480        return(cuddBddXorRecur(manager, f, g));
481    }
482    if (f == one) {
483        return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
484    }
485    if (g == one) {
486        return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
487    }
488    if (f == zero) {
489        return(cuddBddExistAbstractRecur(manager, g, cube));
490    }
491    if (g == zero) {
492        return(cuddBddExistAbstractRecur(manager, f, cube));
493    }
494
495    /* At this point f, g, and cube are not constant. */
496
497    if (f > g) { /* Try to increase cache efficiency. */
498        DdNode *tmp = f;
499        f = g;
500        g = tmp;
501    }
502
503    /* Check cache. */
504    r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
505    if (r != NULL) {
506        return(r);
507    }
508
509    /* Here we can skip the use of cuddI, because the operands are known
510    ** to be non-constant.
511    */
512    F = Cudd_Regular(f);
513    topf = manager->perm[F->index];
514    G = Cudd_Regular(g);
515    topg = manager->perm[G->index];
516    top = ddMin(topf, topg);
517    topcube = manager->perm[cube->index];
518
519    if (topcube < top) {
520        return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
521    }
522    /* Now, topcube >= top. */
523
524    if (topf == top) {
525        index = F->index;
526        fv = cuddT(F);
527        fnv = cuddE(F);
528        if (Cudd_IsComplement(f)) {
529            fv = Cudd_Not(fv);
530            fnv = Cudd_Not(fnv);
531        }
532    } else {
533        index = G->index;
534        fv = fnv = f;
535    }
536
537    if (topg == top) {
538        gv = cuddT(G);
539        gnv = cuddE(G);
540        if (Cudd_IsComplement(g)) {
541            gv = Cudd_Not(gv);
542            gnv = Cudd_Not(gnv);
543        }
544    } else {
545        gv = gnv = g;
546    }
547
548    if (topcube == top) {
549        Cube = cuddT(cube);
550    } else {
551        Cube = cube;
552    }
553
554    t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
555    if (t == NULL) return(NULL);
556
557    /* Special case: 1 OR anything = 1. Hence, no need to compute
558    ** the else branch if t is 1.
559    */
560    if (t == one && topcube == top) {
561        cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
562        return(one);
563    }
564    cuddRef(t);
565
566    e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
567    if (e == NULL) {
568        Cudd_IterDerefBdd(manager, t);
569        return(NULL);
570    }
571    cuddRef(e);
572
573    if (topcube == top) {       /* abstract */
574        r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
575        if (r == NULL) {
576            Cudd_IterDerefBdd(manager, t);
577            Cudd_IterDerefBdd(manager, e);
578            return(NULL);
579        }
580        r = Cudd_Not(r);
581        cuddRef(r);
582        Cudd_IterDerefBdd(manager, t);
583        Cudd_IterDerefBdd(manager, e);
584        cuddDeref(r);
585    } else if (t == e) {
586        r = t;
587        cuddDeref(t);
588        cuddDeref(e);
589    } else {
590        if (Cudd_IsComplement(t)) {
591            r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
592            if (r == NULL) {
593                Cudd_IterDerefBdd(manager, t);
594                Cudd_IterDerefBdd(manager, e);
595                return(NULL);
596            }
597            r = Cudd_Not(r);
598        } else {
599            r = cuddUniqueInter(manager,(int)index,t,e);
600            if (r == NULL) {
601                Cudd_IterDerefBdd(manager, t);
602                Cudd_IterDerefBdd(manager, e);
603                return(NULL);
604            }
605        }
606        cuddDeref(e);
607        cuddDeref(t);
608    }
609    cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
610    return (r);
611
612} /* end of cuddBddXorExistAbstractRecur */
613
614
615/**Function********************************************************************
616
617  Synopsis    [Performs the recursive steps of Cudd_bddBoleanDiff.]
618
619  Description [Performs the recursive steps of Cudd_bddBoleanDiff.
620  Returns the BDD obtained by XORing the cofactors of f with respect to
621  var if successful; NULL otherwise. Exploits the fact that dF/dx =
622  dF'/dx.]
623
624  SideEffects [None]
625
626  SeeAlso     []
627
628******************************************************************************/
629DdNode *
630cuddBddBooleanDiffRecur(
631  DdManager * manager,
632  DdNode * f,
633  DdNode * var)
634{
635    DdNode *T, *E, *res, *res1, *res2;
636
637    statLine(manager);
638    if (cuddI(manager,f->index) > manager->perm[var->index]) {
639        /* f does not depend on var. */
640        return(Cudd_Not(DD_ONE(manager)));
641    }
642
643    /* From now on, f is non-constant. */
644
645    /* If the two indices are the same, so are their levels. */
646    if (f->index == var->index) {
647        res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
648        return(res);
649    }
650
651    /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */
652
653    /* Check the cache. */
654    res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
655    if (res != NULL) {
656        return(res);
657    }
658
659    /* Compute the cofactors of f. */
660    T = cuddT(f); E = cuddE(f);
661
662    res1 = cuddBddBooleanDiffRecur(manager, T, var);
663    if (res1 == NULL) return(NULL);
664    cuddRef(res1);
665    res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
666    if (res2 == NULL) {
667        Cudd_IterDerefBdd(manager, res1);
668        return(NULL);
669    }
670    cuddRef(res2);
671    /* ITE takes care of possible complementation of res1 and of the
672    ** case in which res1 == res2. */
673    res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
674    if (res == NULL) {
675        Cudd_IterDerefBdd(manager, res1);
676        Cudd_IterDerefBdd(manager, res2);
677        return(NULL);
678    }
679    cuddDeref(res1);
680    cuddDeref(res2);
681    cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
682    return(res);
683
684} /* end of cuddBddBooleanDiffRecur */
685
686
687/*---------------------------------------------------------------------------*/
688/* Definition of static functions                                            */
689/*---------------------------------------------------------------------------*/
690
691/**Function********************************************************************
692
693  Synopsis [Checks whether cube is an BDD representing the product of
694  positive literals.]
695
696  Description [Returns 1 in case of success; 0 otherwise.]
697
698  SideEffects [None]
699
700******************************************************************************/
701static int
702bddCheckPositiveCube(
703  DdManager * manager,
704  DdNode * cube)
705{
706    if (Cudd_IsComplement(cube)) return(0);
707    if (cube == DD_ONE(manager)) return(1);
708    if (cuddIsConstant(cube)) return(0);
709    if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
710        return(bddCheckPositiveCube(manager, cuddT(cube)));
711    }
712    return(0);
713
714} /* end of bddCheckPositiveCube */
715
Note: See TracBrowser for help on using the repository browser.