src/cuBdd/cuddAddAbs.c File Reference

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

Go to the source code of this file.

Functions

static int addCheckPositiveCube (DdManager *manager, DdNode *cube)
DdNode * Cudd_addExistAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddAddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $"
static DdNode * two

Function Documentation

static int addCheckPositiveCube ( DdManager *  manager,
DdNode *  cube 
) [static]

AutomaticStart

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

Synopsis [Checks whether cube is an ADD representing the product of positive literals.]

Description [Checks whether cube is an ADD representing the product of positive literals. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 566 of file cuddAddAbs.c.

00569 {
00570     if (Cudd_IsComplement(cube)) return(0);
00571     if (cube == DD_ONE(manager)) return(1);
00572     if (cuddIsConstant(cube)) return(0);
00573     if (cuddE(cube) == DD_ZERO(manager)) {
00574         return(addCheckPositiveCube(manager, cuddT(cube)));
00575     }
00576     return(0);
00577 
00578 } /* end of addCheckPositiveCube */

DdNode* Cudd_addExistAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

AutomaticEnd Function********************************************************************

Synopsis [Existentially Abstracts all the variables in cube from f.]

Description [Abstracts all the variables in cube from f by summing over all possible values taken by the variables. Returns the abstracted ADD.]

SideEffects [None]

SeeAlso [Cudd_addUnivAbstract Cudd_bddExistAbstract Cudd_addOrAbstract]

Definition at line 125 of file cuddAddAbs.c.

00129 {
00130     DdNode *res;
00131 
00132     two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
00133     if (two == NULL) return(NULL);
00134     cuddRef(two);
00135 
00136     if (addCheckPositiveCube(manager, cube) == 0) {
00137         (void) fprintf(manager->err,"Error: Can only abstract cubes");
00138         return(NULL);
00139     }
00140 
00141     do {
00142         manager->reordered = 0;
00143         res = cuddAddExistAbstractRecur(manager, f, cube);
00144     } while (manager->reordered == 1);
00145 
00146     if (res == NULL) {
00147         Cudd_RecursiveDeref(manager,two);
00148         return(NULL);
00149     }
00150     cuddRef(res);
00151     Cudd_RecursiveDeref(manager,two);
00152     cuddDeref(res);
00153 
00154     return(res);
00155 
00156 } /* end of Cudd_addExistAbstract */

DdNode* Cudd_addOrAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Disjunctively abstracts all the variables in cube from the 0-1 ADD f.]

Description [Abstracts all the variables in cube from the 0-1 ADD f by taking the disjunction over all possible values taken by the variables. Returns the abstracted ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract]

Definition at line 212 of file cuddAddAbs.c.

00216 {
00217     DdNode *res;
00218 
00219     if (addCheckPositiveCube(manager, cube) == 0) {
00220         (void) fprintf(manager->err,"Error: Can only abstract cubes");
00221         return(NULL);
00222     }
00223 
00224     do {
00225         manager->reordered = 0;
00226         res = cuddAddOrAbstractRecur(manager, f, cube);
00227     } while (manager->reordered == 1);
00228     return(res);
00229 
00230 } /* end of Cudd_addOrAbstract */

DdNode* Cudd_addUnivAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Universally Abstracts all the variables in cube from f.]

Description [Abstracts all the variables in cube from f by taking the product over all possible values taken by the variable. Returns the abstracted ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addExistAbstract Cudd_bddUnivAbstract Cudd_addOrAbstract]

Definition at line 174 of file cuddAddAbs.c.

00178 {
00179     DdNode              *res;
00180 
00181     if (addCheckPositiveCube(manager, cube) == 0) {
00182         (void) fprintf(manager->err,"Error:  Can only abstract cubes");
00183         return(NULL);
00184     }
00185 
00186     do {
00187         manager->reordered = 0;
00188         res = cuddAddUnivAbstractRecur(manager, f, cube);
00189     } while (manager->reordered == 1);
00190 
00191     return(res);
00192 
00193 } /* end of Cudd_addUnivAbstract */

DdNode* cuddAddExistAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive step of Cudd_addExistAbstract.]

Description [Performs the recursive step of Cudd_addExistAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 252 of file cuddAddAbs.c.

00256 {
00257     DdNode      *T, *E, *res, *res1, *res2, *zero;
00258 
00259     statLine(manager);
00260     zero = DD_ZERO(manager);
00261 
00262     /* Cube is guaranteed to be a cube at this point. */        
00263     if (f == zero || cuddIsConstant(cube)) {  
00264         return(f);
00265     }
00266 
00267     /* Abstract a variable that does not appear in f => multiply by 2. */
00268     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00269         res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube));
00270         if (res1 == NULL) return(NULL);
00271         cuddRef(res1);
00272         /* Use the "internal" procedure to be alerted in case of
00273         ** dynamic reordering. If dynamic reordering occurs, we
00274         ** have to abort the entire abstraction.
00275         */
00276         res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two);
00277         if (res == NULL) {
00278             Cudd_RecursiveDeref(manager,res1);
00279             return(NULL);
00280         }
00281         cuddRef(res);
00282         Cudd_RecursiveDeref(manager,res1);
00283         cuddDeref(res);
00284         return(res);
00285     }
00286 
00287     if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) {
00288         return(res);
00289     }
00290 
00291     T = cuddT(f);
00292     E = cuddE(f);
00293 
00294     /* If the two indices are the same, so are their levels. */
00295     if (f->index == cube->index) {
00296         res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube));
00297         if (res1 == NULL) return(NULL);
00298         cuddRef(res1);
00299         res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube));
00300         if (res2 == NULL) {
00301             Cudd_RecursiveDeref(manager,res1);
00302             return(NULL);
00303         }
00304         cuddRef(res2);
00305         res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2);
00306         if (res == NULL) {
00307             Cudd_RecursiveDeref(manager,res1);
00308             Cudd_RecursiveDeref(manager,res2);
00309             return(NULL);
00310         }
00311         cuddRef(res);
00312         Cudd_RecursiveDeref(manager,res1);
00313         Cudd_RecursiveDeref(manager,res2);
00314         cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
00315         cuddDeref(res);
00316         return(res);
00317     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00318         res1 = cuddAddExistAbstractRecur(manager, T, cube);
00319         if (res1 == NULL) return(NULL);
00320         cuddRef(res1);
00321         res2 = cuddAddExistAbstractRecur(manager, E, cube);
00322         if (res2 == NULL) {
00323             Cudd_RecursiveDeref(manager,res1);
00324             return(NULL);
00325         }
00326         cuddRef(res2);
00327         res = (res1 == res2) ? res1 :
00328             cuddUniqueInter(manager, (int) f->index, res1, res2);
00329         if (res == NULL) {
00330             Cudd_RecursiveDeref(manager,res1);
00331             Cudd_RecursiveDeref(manager,res2);
00332             return(NULL);
00333         }
00334         cuddDeref(res1);
00335         cuddDeref(res2);
00336         cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res);
00337         return(res);
00338     }       
00339 
00340 } /* end of cuddAddExistAbstractRecur */

DdNode* cuddAddOrAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive step of Cudd_addOrAbstract.]

Description [Performs the recursive step of Cudd_addOrAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 465 of file cuddAddAbs.c.

00469 {
00470     DdNode      *T, *E, *res, *res1, *res2, *one;
00471 
00472     statLine(manager);
00473     one = DD_ONE(manager);
00474 
00475     /* Cube is guaranteed to be a cube at this point. */
00476     if (cuddIsConstant(f) || cube == one) {  
00477         return(f);
00478     }
00479 
00480     /* Abstract a variable that does not appear in f. */
00481     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00482         res = cuddAddOrAbstractRecur(manager, f, cuddT(cube));
00483         return(res);
00484     }
00485 
00486     if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) {
00487         return(res);
00488     }
00489 
00490     T = cuddT(f);
00491     E = cuddE(f);
00492 
00493     /* If the two indices are the same, so are their levels. */
00494     if (f->index == cube->index) {
00495         res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube));
00496         if (res1 == NULL) return(NULL);
00497         cuddRef(res1);
00498         if (res1 != one) {
00499             res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube));
00500             if (res2 == NULL) {
00501                 Cudd_RecursiveDeref(manager,res1);
00502                 return(NULL);
00503             }
00504             cuddRef(res2);
00505             res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2);
00506             if (res == NULL) {
00507                 Cudd_RecursiveDeref(manager,res1);
00508                 Cudd_RecursiveDeref(manager,res2);
00509                 return(NULL);
00510             }
00511             cuddRef(res);
00512             Cudd_RecursiveDeref(manager,res1);
00513             Cudd_RecursiveDeref(manager,res2);
00514         } else {
00515             res = res1;
00516         }
00517         cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
00518         cuddDeref(res);
00519         return(res);
00520     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00521         res1 = cuddAddOrAbstractRecur(manager, T, cube);
00522         if (res1 == NULL) return(NULL);
00523         cuddRef(res1);
00524         res2 = cuddAddOrAbstractRecur(manager, E, cube);
00525         if (res2 == NULL) {
00526             Cudd_RecursiveDeref(manager,res1);
00527             return(NULL);
00528         }
00529         cuddRef(res2);
00530         res = (res1 == res2) ? res1 :
00531             cuddUniqueInter(manager, (int) f->index, res1, res2);
00532         if (res == NULL) {
00533             Cudd_RecursiveDeref(manager,res1);
00534             Cudd_RecursiveDeref(manager,res2);
00535             return(NULL);
00536         }
00537         cuddDeref(res1);
00538         cuddDeref(res2);
00539         cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res);
00540         return(res);
00541     }
00542 
00543 } /* end of cuddAddOrAbstractRecur */

DdNode* cuddAddUnivAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive step of Cudd_addUnivAbstract.]

Description [Performs the recursive step of Cudd_addUnivAbstract. Returns the ADD obtained by abstracting the variables of cube from f, if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 357 of file cuddAddAbs.c.

00361 {
00362     DdNode      *T, *E, *res, *res1, *res2, *one, *zero;
00363 
00364     statLine(manager);
00365     one = DD_ONE(manager);
00366     zero = DD_ZERO(manager);
00367 
00368     /* Cube is guaranteed to be a cube at this point.
00369     ** zero and one are the only constatnts c such that c*c=c.
00370     */
00371     if (f == zero || f == one || cube == one) {  
00372         return(f);
00373     }
00374 
00375     /* Abstract a variable that does not appear in f. */
00376     if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
00377         res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
00378         if (res1 == NULL) return(NULL);
00379         cuddRef(res1);
00380         /* Use the "internal" procedure to be alerted in case of
00381         ** dynamic reordering. If dynamic reordering occurs, we
00382         ** have to abort the entire abstraction.
00383         */
00384         res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
00385         if (res == NULL) {
00386             Cudd_RecursiveDeref(manager,res1);
00387             return(NULL);
00388         }
00389         cuddRef(res);
00390         Cudd_RecursiveDeref(manager,res1);
00391         cuddDeref(res);
00392         return(res);
00393     }
00394 
00395     if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
00396         return(res);
00397     }
00398 
00399     T = cuddT(f);
00400     E = cuddE(f);
00401 
00402     /* If the two indices are the same, so are their levels. */
00403     if (f->index == cube->index) {
00404         res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
00405         if (res1 == NULL) return(NULL);
00406         cuddRef(res1);
00407         res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
00408         if (res2 == NULL) {
00409             Cudd_RecursiveDeref(manager,res1);
00410             return(NULL);
00411         }
00412         cuddRef(res2);
00413         res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
00414         if (res == NULL) {
00415             Cudd_RecursiveDeref(manager,res1);
00416             Cudd_RecursiveDeref(manager,res2);
00417             return(NULL);
00418         }
00419         cuddRef(res);
00420         Cudd_RecursiveDeref(manager,res1);
00421         Cudd_RecursiveDeref(manager,res2);
00422         cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
00423         cuddDeref(res);
00424         return(res);
00425     } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
00426         res1 = cuddAddUnivAbstractRecur(manager, T, cube);
00427         if (res1 == NULL) return(NULL);
00428         cuddRef(res1);
00429         res2 = cuddAddUnivAbstractRecur(manager, E, cube);
00430         if (res2 == NULL) {
00431             Cudd_RecursiveDeref(manager,res1);
00432             return(NULL);
00433         }
00434         cuddRef(res2);
00435         res = (res1 == res2) ? res1 :
00436             cuddUniqueInter(manager, (int) f->index, res1, res2);
00437         if (res == NULL) {
00438             Cudd_RecursiveDeref(manager,res1);
00439             Cudd_RecursiveDeref(manager,res2);
00440             return(NULL);
00441         }
00442         cuddDeref(res1);
00443         cuddDeref(res2);
00444         cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
00445         return(res);
00446     }
00447 
00448 } /* end of cuddAddUnivAbstractRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $" [static]

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

FileName [cuddAddAbs.c]

PackageName [cudd]

Synopsis [Quantification functions for ADDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static 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 85 of file cuddAddAbs.c.

DdNode* two [static]

Definition at line 88 of file cuddAddAbs.c.

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