src/cuBdd/cuddAndAbs.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddAndAbs.c:

Go to the source code of this file.

Functions

DdNode * Cudd_bddAndAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
DdNode * Cudd_bddAndAbstractLimit (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit)
DdNode * cuddBddAndAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.19 2004/08/13 18:04:46 fabio Exp $"

Function Documentation

DdNode* Cudd_bddAndAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
DdNode *  cube 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube.]

Description [Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise. Cudd_bddAndAbstract implements the semiring matrix multiplication algorithm for the boolean semiring.]

SideEffects [None]

SeeAlso [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]

Definition at line 120 of file cuddAndAbs.c.

00125 {
00126     DdNode *res;
00127 
00128     do {
00129         manager->reordered = 0;
00130         res = cuddBddAndAbstractRecur(manager, f, g, cube);
00131     } while (manager->reordered == 1);
00132     return(res);
00133 
00134 } /* end of Cudd_bddAndAbstract */

DdNode* Cudd_bddAndAbstractLimit ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
DdNode *  cube,
unsigned int  limit 
)

Function********************************************************************

Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube. Returns NULL if too many nodes are required.]

Description [Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise. In particular, if the number of new nodes created exceeds limit, this function returns NULL.]

SideEffects [None]

SeeAlso [Cudd_bddAndAbstract]

Definition at line 154 of file cuddAndAbs.c.

00160 {
00161     DdNode *res;
00162     unsigned int saveLimit = manager->maxLive;
00163 
00164     manager->maxLive = (manager->keys - manager->dead) +
00165       (manager->keysZ - manager->deadZ) + limit;
00166     do {
00167         manager->reordered = 0;
00168         res = cuddBddAndAbstractRecur(manager, f, g, cube);
00169     } while (manager->reordered == 1);
00170     manager->maxLive = saveLimit;
00171     return(res);
00172 
00173 } /* end of Cudd_bddAndAbstractLimit */

DdNode* cuddBddAndAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
DdNode *  cube 
)

Function********************************************************************

Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube.]

Description [Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddAndAbstract]

Definition at line 196 of file cuddAndAbs.c.

00201 {
00202     DdNode *F, *ft, *fe, *G, *gt, *ge;
00203     DdNode *one, *zero, *r, *t, *e;
00204     unsigned int topf, topg, topcube, top, index;
00205 
00206     statLine(manager);
00207     one = DD_ONE(manager);
00208     zero = Cudd_Not(one);
00209 
00210     /* Terminal cases. */
00211     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00212     if (f == one && g == one)   return(one);
00213 
00214     if (cube == one) {
00215         return(cuddBddAndRecur(manager, f, g));
00216     }
00217     if (f == one || f == g) {
00218         return(cuddBddExistAbstractRecur(manager, g, cube));
00219     }
00220     if (g == one) {
00221         return(cuddBddExistAbstractRecur(manager, f, cube));
00222     }
00223     /* At this point f, g, and cube are not constant. */
00224 
00225     if (f > g) { /* Try to increase cache efficiency. */
00226         DdNode *tmp = f;
00227         f = g;
00228         g = tmp;
00229     }
00230 
00231     /* Here we can skip the use of cuddI, because the operands are known
00232     ** to be non-constant.
00233     */
00234     F = Cudd_Regular(f);
00235     G = Cudd_Regular(g);
00236     topf = manager->perm[F->index];
00237     topg = manager->perm[G->index];
00238     top = ddMin(topf, topg);
00239     topcube = manager->perm[cube->index];
00240 
00241     while (topcube < top) {
00242         cube = cuddT(cube);
00243         if (cube == one) {
00244             return(cuddBddAndRecur(manager, f, g));
00245         }
00246         topcube = manager->perm[cube->index];
00247     }
00248     /* Now, topcube >= top. */
00249 
00250     /* Check cache. */
00251     if (F->ref != 1 || G->ref != 1) {
00252         r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
00253         if (r != NULL) {
00254             return(r);
00255         }
00256     }
00257 
00258     if (topf == top) {
00259         index = F->index;
00260         ft = cuddT(F);
00261         fe = cuddE(F);
00262         if (Cudd_IsComplement(f)) {
00263             ft = Cudd_Not(ft);
00264             fe = Cudd_Not(fe);
00265         }
00266     } else {
00267         index = G->index;
00268         ft = fe = f;
00269     }
00270 
00271     if (topg == top) {
00272         gt = cuddT(G);
00273         ge = cuddE(G);
00274         if (Cudd_IsComplement(g)) {
00275             gt = Cudd_Not(gt);
00276             ge = Cudd_Not(ge);
00277         }
00278     } else {
00279         gt = ge = g;
00280     }
00281 
00282     if (topcube == top) {       /* quantify */
00283         DdNode *Cube = cuddT(cube);
00284         t = cuddBddAndAbstractRecur(manager, ft, gt, Cube);
00285         if (t == NULL) return(NULL);
00286         /* Special case: 1 OR anything = 1. Hence, no need to compute
00287         ** the else branch if t is 1. Likewise t + t * anything == t.
00288         ** Notice that t == fe implies that fe does not depend on the
00289         ** variables in Cube. Likewise for t == ge.
00290         */
00291         if (t == one || t == fe || t == ge) {
00292             if (F->ref != 1 || G->ref != 1)
00293                 cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
00294                                 f, g, cube, t);
00295             return(t);
00296         }
00297         cuddRef(t);
00298         /* Special case: t + !t * anything == t + anything. */
00299         if (t == Cudd_Not(fe)) {
00300             e = cuddBddExistAbstractRecur(manager, ge, Cube);
00301         } else if (t == Cudd_Not(ge)) {
00302             e = cuddBddExistAbstractRecur(manager, fe, Cube);
00303         } else {
00304             e = cuddBddAndAbstractRecur(manager, fe, ge, Cube);
00305         }
00306         if (e == NULL) {
00307             Cudd_IterDerefBdd(manager, t);
00308             return(NULL);
00309         }
00310         if (t == e) {
00311             r = t;
00312             cuddDeref(t);
00313         } else {
00314             cuddRef(e);
00315             r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
00316             if (r == NULL) {
00317                 Cudd_IterDerefBdd(manager, t);
00318                 Cudd_IterDerefBdd(manager, e);
00319                 return(NULL);
00320             }
00321             r = Cudd_Not(r);
00322             cuddRef(r);
00323             Cudd_DelayedDerefBdd(manager, t);
00324             Cudd_DelayedDerefBdd(manager, e);
00325             cuddDeref(r);
00326         }
00327     } else {
00328         t = cuddBddAndAbstractRecur(manager, ft, gt, cube);
00329         if (t == NULL) return(NULL);
00330         cuddRef(t);
00331         e = cuddBddAndAbstractRecur(manager, fe, ge, cube);
00332         if (e == NULL) {
00333             Cudd_IterDerefBdd(manager, t);
00334             return(NULL);
00335         }
00336         if (t == e) {
00337             r = t;
00338             cuddDeref(t);
00339         } else {
00340             cuddRef(e);
00341             if (Cudd_IsComplement(t)) {
00342                 r = cuddUniqueInter(manager, (int) index,
00343                                     Cudd_Not(t), Cudd_Not(e));
00344                 if (r == NULL) {
00345                     Cudd_IterDerefBdd(manager, t);
00346                     Cudd_IterDerefBdd(manager, e);
00347                     return(NULL);
00348                 }
00349                 r = Cudd_Not(r);
00350             } else {
00351                 r = cuddUniqueInter(manager,(int)index,t,e);
00352                 if (r == NULL) {
00353                     Cudd_IterDerefBdd(manager, t);
00354                     Cudd_IterDerefBdd(manager, e);
00355                     return(NULL);
00356                 }
00357             }
00358             cuddDeref(e);
00359             cuddDeref(t);
00360         }
00361     }
00362 
00363     if (F->ref != 1 || G->ref != 1)
00364         cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
00365     return (r);
00366 
00367 } /* end of cuddBddAndAbstractRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.19 2004/08/13 18:04:46 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddAndAbs.c]

PackageName [cudd]

Synopsis [Combined AND and existential abstraction for BDDs]

Description [External procedures included in this module:

Internal procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 79 of file cuddAndAbs.c.

Generated on Tue Jan 12 13:57:17 2010 for glu-2.2 by  doxygen 1.6.1