src/bdd/cudd/cuddEssent.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddEssent.c:

Go to the source code of this file.

Functions

static DdNode *ddFindEssentialRecur ARGS ((DdManager *dd, DdNode *f))
DdNode * Cudd_FindEssential (DdManager *dd, DdNode *f)
int Cudd_bddIsVarEssential (DdManager *manager, DdNode *f, int id, int phase)
static DdNode * ddFindEssentialRecur (DdManager *dd, DdNode *f)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddEssent.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"

Function Documentation

static DdNode* ddFindEssentialRecur ARGS ( (DdManager *dd, DdNode *f)   )  [static]

AutomaticStart

int Cudd_bddIsVarEssential ( DdManager *  manager,
DdNode *  f,
int  id,
int  phase 
)

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

Synopsis [Determines whether a given variable is essential with a given phase in a BDD.]

Description [Determines whether a given variable is essential with a given phase in a BDD. Uses Cudd_bddIteConstant. Returns 1 if phase == 1 and f-->x_id, or if phase == 0 and f-->x_id'.]

SideEffects [None]

SeeAlso [Cudd_FindEssential]

Definition at line 117 of file cuddEssent.c.

00122 {
00123     DdNode      *var;
00124     int         res;
00125     DdNode      *one, *zero;
00126 
00127     one = DD_ONE(manager);
00128     zero = Cudd_Not(one);
00129 
00130     var = cuddUniqueInter(manager, id, one, zero);
00131 
00132     var = Cudd_NotCond(var,phase == 0);
00133 
00134     res = Cudd_bddIteConstant(manager, Cudd_Not(f), one, var) == one;
00135 
00136     return(res);
00137 
00138 } /* end of Cudd_bddIsVarEssential */

DdNode* Cudd_FindEssential ( DdManager *  dd,
DdNode *  f 
)

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

Synopsis [Finds the essential variables of a DD.]

Description [Returns the cube of the essential variables. A positive literal means that the variable must be set to 1 for the function to be 1. A negative literal means that the variable must be set to 0 for the function to be 1. Returns a pointer to the cube BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddIsVarEssential]

Definition at line 87 of file cuddEssent.c.

00090 {
00091     DdNode *res;
00092 
00093     do {
00094         dd->reordered = 0;
00095         res = ddFindEssentialRecur(dd,f);
00096     } while (dd->reordered == 1);
00097     return(res);
00098 
00099 } /* end of Cudd_FindEssential */

static DdNode* ddFindEssentialRecur ( DdManager *  dd,
DdNode *  f 
) [static]

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

Synopsis [Implements the recursive step of Cudd_FindEssential.]

Description [Implements the recursive step of Cudd_FindEssential. Returns a pointer to the cube BDD if successful; NULL otherwise.]

SideEffects [None]

Definition at line 162 of file cuddEssent.c.

00165 {
00166     DdNode      *T, *E, *F;
00167     DdNode      *essT, *essE, *res;
00168     int         index;
00169     DdNode      *one, *lzero, *azero;
00170 
00171     one = DD_ONE(dd);
00172     F = Cudd_Regular(f);
00173     /* If f is constant the set of essential variables is empty. */
00174     if (cuddIsConstant(F)) return(one);
00175 
00176     res = cuddCacheLookup1(dd,Cudd_FindEssential,f);
00177     if (res != NULL) {
00178         return(res);
00179     }
00180 
00181     lzero = Cudd_Not(one);
00182     azero = DD_ZERO(dd);
00183     /* Find cofactors: here f is non-constant. */
00184     T = cuddT(F);
00185     E = cuddE(F);
00186     if (Cudd_IsComplement(f)) {
00187         T = Cudd_Not(T); E = Cudd_Not(E);
00188     }
00189 
00190     index = F->index;
00191     if (Cudd_IsConstant(T) && T != lzero && T != azero) {
00192         /* if E is zero, index is essential, otherwise there are no
00193         ** essentials, because index is not essential and no other variable
00194         ** can be, since setting index = 1 makes the function constant and
00195         ** different from 0.
00196         */
00197         if (E == lzero || E == azero) {
00198             res = dd->vars[index];
00199         } else {
00200             res = one;
00201         }
00202     } else if (T == lzero || T == azero) {
00203         if (Cudd_IsConstant(E)) { /* E cannot be zero here */
00204             res = Cudd_Not(dd->vars[index]);
00205         } else { /* E == non-constant */
00206             /* find essentials in the else branch */
00207             essE = ddFindEssentialRecur(dd,E);
00208             if (essE == NULL) {
00209                 return(NULL);
00210             }
00211             cuddRef(essE);
00212 
00213             /* add index to the set with negative phase */
00214             res = cuddUniqueInter(dd,index,one,Cudd_Not(essE));
00215             if (res == NULL) {
00216                 Cudd_RecursiveDeref(dd,essE);
00217                 return(NULL);
00218             }
00219             res = Cudd_Not(res);
00220             cuddDeref(essE);
00221         }
00222     } else { /* T == non-const */
00223         if (E == lzero || E == azero) {
00224             /* find essentials in the then branch */
00225             essT = ddFindEssentialRecur(dd,T);
00226             if (essT == NULL) {
00227                 return(NULL);
00228             }
00229             cuddRef(essT);
00230 
00231             /* add index to the set with positive phase */
00232             /* use And because essT may be complemented */
00233             res = cuddBddAndRecur(dd,dd->vars[index],essT);
00234             if (res == NULL) {
00235                 Cudd_RecursiveDeref(dd,essT);
00236                 return(NULL);
00237             }
00238             cuddDeref(essT);
00239         } else if (!Cudd_IsConstant(E)) {
00240             /* if E is a non-zero constant there are no essentials
00241             ** because T is non-constant.
00242             */
00243             essT = ddFindEssentialRecur(dd,T);
00244             if (essT == NULL) {
00245                 return(NULL);
00246             }
00247             if (essT == one) {
00248                 res = one;
00249             } else {
00250                 cuddRef(essT);
00251                 essE = ddFindEssentialRecur(dd,E);
00252                 if (essE == NULL) {
00253                     Cudd_RecursiveDeref(dd,essT);
00254                     return(NULL);
00255                 }
00256                 cuddRef(essE);
00257 
00258                 /* res = intersection(essT, essE) */
00259                 res = cuddBddLiteralSetIntersectionRecur(dd,essT,essE);
00260                 if (res == NULL) {
00261                     Cudd_RecursiveDeref(dd,essT);
00262                     Cudd_RecursiveDeref(dd,essE);
00263                     return(NULL);
00264                 }
00265                 cuddRef(res);
00266                 Cudd_RecursiveDeref(dd,essT);
00267                 Cudd_RecursiveDeref(dd,essE);
00268                 cuddDeref(res);
00269             }
00270         } else {        /* E is a non-zero constant */
00271             res = one;
00272         }
00273     }
00274 
00275     cuddCacheInsert1(dd,Cudd_FindEssential, f, res);
00276     return(res);
00277 
00278 } /* end of ddFindEssentialRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddEssent.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static]

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

FileName [cuddEssent.c]

PackageName [cudd]

Synopsis [Functions for the detection of essential variables.]

Description [External procedures included in this file:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 48 of file cuddEssent.c.

Generated on Tue Jan 5 12:18:54 2010 for abc70930 by  doxygen 1.6.1