src/bdd/cudd/cuddUtil.c File Reference

#include "util_hack.h"
#include "cuddInt.h"

Include dependency graph for cuddUtil.c:

Defines
#define	MODULUS1 2147483563
#define	LEQA1 40014
#define	LEQQ1 53668
#define	LEQR1 12211
#define	MODULUS2 2147483399
#define	LEQA2 40692
#define	LEQQ2 52774
#define	LEQR2 3791
#define	STAB_SIZE 64
#define	STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)
#define	bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ')
Functions
static int dp2	ARGS ((DdManager dd, DdNode f, st_table *t))
static void ddPrintMintermAux	ARGS ((DdManager dd, DdNode node, int *list))
static int ddDagInt	ARGS ((DdNode *n))
static int cuddEstimateCofactor	ARGS ((DdManager dd, st_table table, DdNode node, int i, int phase, DdNode *ptr))
static DdNode *cuddUniqueLookup	ARGS ((DdManager unique, intindex, DdNode T, DdNode *E))
static int cuddEstimateCofactorSimple	ARGS ((DdNode *node, int i))
static double ddCountMintermAux	ARGS ((DdNode node, double max, DdHashTable table))
static int ddEpdCountMintermAux	ARGS ((DdNode node, EpDouble max, EpDouble epd, st_table table))
static double ddCountPathAux	ARGS ((DdNode node, st_table table))
static double ddCountPathsToNonZero	ARGS ((DdNode N, st_table table))
static void ddSupportStep	ARGS ((DdNode f, int support))
static void ddClearFlag	ARGS ((DdNode *f))
static int ddPickArbitraryMinterms	ARGS ((DdManager dd, DdNode node, int nvars, int nminterms, char **string))
static int ddPickRepresentativeCube	ARGS ((DdManager dd, DdNode node, int nvars, double weight, char string))
static enum st_retval ddEpdFree	ARGS ((char key, char value, char *arg))
int	Cudd_PrintMinterm (DdManager manager, DdNode node)
int	Cudd_bddPrintCover (DdManager dd, DdNode l, DdNode *u)
int	Cudd_PrintDebug (DdManager dd, DdNode f, int n, int pr)
int	Cudd_DagSize (DdNode *node)
int	Cudd_EstimateCofactor (DdManager dd, DdNode f, int i, int phase)
int	Cudd_EstimateCofactorSimple (DdNode *node, int i)
int	Cudd_SharingSize (DdNode **nodeArray, int n)
double	Cudd_CountMinterm (DdManager manager, DdNode node, int nvars)
double	Cudd_CountPath (DdNode *node)
int	Cudd_EpdCountMinterm (DdManager manager, DdNode node, int nvars, EpDouble *epd)
double	Cudd_CountPathsToNonZero (DdNode *node)
DdNode *	Cudd_Support (DdManager dd, DdNode f)
int *	Cudd_SupportIndex (DdManager dd, DdNode f)
int	Cudd_SupportSize (DdManager dd, DdNode f)
DdNode *	Cudd_VectorSupport (DdManager dd, DdNode *F, int n)
int *	Cudd_VectorSupportIndex (DdManager dd, DdNode *F, int n)
int	Cudd_VectorSupportSize (DdManager dd, DdNode *F, int n)
int	Cudd_ClassifySupport (DdManager dd, DdNode f, DdNode g, DdNode common, DdNode onlyF, DdNode *onlyG)
int	Cudd_CountLeaves (DdNode *node)
int	Cudd_bddPickOneCube (DdManager ddm, DdNode node, char *string)
DdNode *	Cudd_bddPickOneMinterm (DdManager dd, DdNode f, DdNode **vars, int n)
DdNode **	Cudd_bddPickArbitraryMinterms (DdManager dd, DdNode f, DdNode **vars, int n, int k)
DdNode *	Cudd_SubsetWithMaskVars (DdManager dd, DdNode f, DdNode vars, int nvars, DdNode maskVars, int mvars)
DdGen *	Cudd_FirstCube (DdManager dd, DdNode f, int *cube, CUDD_VALUE_TYPE value)
int	Cudd_NextCube (DdGen gen, int cube, CUDD_VALUE_TYPE value)
DdNode *	Cudd_bddComputeCube (DdManager dd, DdNode vars, int phase, int n)
DdNode *	Cudd_addComputeCube (DdManager dd, DdNode vars, int phase, int n)
DdNode *	Cudd_CubeArrayToBdd (DdManager dd, int array)
int	Cudd_BddToCubeArray (DdManager dd, DdNode cube, int *array)
DdGen *	Cudd_FirstNode (DdManager dd, DdNode f, DdNode **node)
int	Cudd_NextNode (DdGen gen, DdNode *node)
int	Cudd_GenFree (DdGen *gen)
int	Cudd_IsGenEmpty (DdGen *gen)
DdNode *	Cudd_IndicesToCube (DdManager dd, int array, int n)
void	Cudd_PrintVersion (FILE *fp)
double	Cudd_AverageDistance (DdManager *dd)
long	Cudd_Random ()
void	Cudd_Srandom (long seed)
double	Cudd_Density (DdManager dd, DdNode f, int nvars)
void	Cudd_OutOfMem (long size)
int	cuddP (DdManager dd, DdNode f)
enum st_retval	cuddStCountfree (char key, char value, char *arg)
int	cuddCollectNodes (DdNode f, st_table visited)
static int	dp2 (DdManager dd, DdNode f, st_table *t)
static void	ddPrintMintermAux (DdManager dd, DdNode node, int *list)
static int	ddDagInt (DdNode *n)
static int	cuddEstimateCofactor (DdManager dd, st_table table, DdNode node, int i, int phase, DdNode *ptr)
static DdNode *	cuddUniqueLookup (DdManager unique, int index, DdNode T, DdNode *E)
static int	cuddEstimateCofactorSimple (DdNode *node, int i)
static double	ddCountMintermAux (DdNode node, double max, DdHashTable table)
static double	ddCountPathAux (DdNode node, st_table table)
static int	ddEpdCountMintermAux (DdNode node, EpDouble max, EpDouble epd, st_table table)
static double	ddCountPathsToNonZero (DdNode N, st_table table)
static void	ddSupportStep (DdNode f, int support)
static void	ddClearFlag (DdNode *f)
static int	ddLeavesInt (DdNode *n)
static int	ddPickArbitraryMinterms (DdManager dd, DdNode node, int nvars, int nminterms, char **string)
static int	ddPickRepresentativeCube (DdManager dd, DdNode node, int nvars, double weight, char string)
static enum st_retval	ddEpdFree (char key, char value, char *arg)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddUtil.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"
static DdNode *	background
static DdNode *	zero
static long	cuddRand = 0
static long	cuddRand2
static long	shuffleSelect
static long	shuffleTable [STAB_SIZE]

Define Documentation

#define bang ( f ) ((Cudd_IsComplement(f)) ? '!' : ' ')

Definition at line 126 of file cuddUtil.c.

#define LEQA1 40014

Definition at line 88 of file cuddUtil.c.

#define LEQA2 40692

Definition at line 92 of file cuddUtil.c.

#define LEQQ1 53668

Definition at line 89 of file cuddUtil.c.

#define LEQQ2 52774

Definition at line 93 of file cuddUtil.c.

#define LEQR1 12211

Definition at line 90 of file cuddUtil.c.

#define LEQR2 3791

Definition at line 94 of file cuddUtil.c.

#define MODULUS1 2147483563

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

FileName [cuddUtil.c]

PackageName [cudd]

Synopsis [Utility functions.]

Description [External procedures included in this module:

Internal procedures included in this module:

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 87 of file cuddUtil.c.

#define MODULUS2 2147483399

Definition at line 91 of file cuddUtil.c.

#define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE)

Definition at line 96 of file cuddUtil.c.

#define STAB_SIZE 64

Definition at line 95 of file cuddUtil.c.

Function Documentation

static enum st_retval ddEpdFree ARGS ( (char *key, char *value, char *arg) ) [static]

static int ddPickRepresentativeCube ARGS ( (DdManager *dd, DdNode *node, int nvars, double *weight, char *string) ) [static]

static int ddPickArbitraryMinterms ARGS ( (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string) ) [static]

static void ddClearFlag ARGS ( (DdNode *f) ) [static]

static void ddSupportStep ARGS ( (DdNode *f, int *support) ) [static]

static double ddCountPathsToNonZero ARGS ( (DdNode *N, st_table *table) ) [static]

static double ddCountPathAux ARGS ( (DdNode *node, st_table *table) ) [static]

static int ddEpdCountMintermAux ARGS ( (DdNode *node, EpDouble *max, EpDouble *epd, st_table *table) ) [static]

static double ddCountMintermAux ARGS ( (DdNode *node, double max, DdHashTable *table) ) [static]

static int cuddEstimateCofactorSimple ARGS ( (DdNode *node, int i) ) [static]

static DdNode* cuddUniqueLookup ARGS ( (DdManager *unique, intindex, DdNode *T, DdNode *E) ) [static]

static int cuddEstimateCofactor ARGS ( (DdManager *dd, st_table *table, DdNode *node, int i, int phase, DdNode **ptr) ) [static]

static int ddDagInt ARGS ( (DdNode *n) ) [static]

static void ddPrintMintermAux ARGS ( (DdManager *dd, DdNode *node, int *list) ) [static]

static int dp2 ARGS ( (DdManager *dd, DdNode *f, st_table *t) ) [static]

AutomaticStart

DdNode* Cudd_addComputeCube	(	DdManager *	dd,
		DdNode **	vars,
		int *	phase,
		int	n
	)

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

Synopsis [Computes the cube of an array of ADD variables.]

Description [Computes the cube of an array of ADD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase\[i\] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [none]

SeeAlso [Cudd_bddComputeCube]

Definition at line 2010 of file cuddUtil.c.

02016 02017 02018 02019 02020 02021 02022 02023 02024 02025 02026 02027 02028 02029         } 02030 02031 02032 02033         } 02034 02035 02036 02037     } 02038 02039 02040 02041 02042

class="fragment">02015 { DdNode *cube, *zero; DdNode *fn; int i; cube = DD_ONE(dd); cuddRef(cube); zero = DD_ZERO(dd); for (i = n - 1; i >= 0; i--) { if (phase == NULL || phase[i] != 0) { fn = Cudd_addIte(dd,vars[i],cube,zero); } else { fn = Cudd_addIte(dd,vars[i],zero,cube); if (fn == NULL) { Cudd_RecursiveDeref(dd,cube); return(NULL); cuddRef(fn); Cudd_RecursiveDeref(dd,cube); cube = fn; cuddDeref(cube); return(cube); } /* end of Cudd_addComputeCube */

double Cudd_AverageDistance ( DdManager * dd )

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

Synopsis [Computes the average distance between adjacent nodes.]

Description [Computes the average distance between adjacent nodes in the manager. Adjacent nodes are node pairs such that the second node is the then child, else child, or next node in the collision list.]

SideEffects [None]

SeeAlso []

Definition at line 2391 of file cuddUtil.c.

02393 {
02394     double tetotal, nexttotal;
02395     double tesubtotal, nextsubtotal;
02396     double temeasured, nextmeasured;
02397     int i, j;
02398     int slots, nvars;
02399     long diff;
02400     DdNode *scan;
02401     DdNodePtr *nodelist;
02402     DdNode *sentinel = &(dd->sentinel);
02403 
02404     nvars = dd->size;
02405     if (nvars == 0) return(0.0);
02406 
02407     /* Initialize totals. */
02408     tetotal = 0.0;
02409     nexttotal = 0.0;
02410     temeasured = 0.0;
02411     nextmeasured = 0.0;
02412 
02413     /* Scan the variable subtables. */
02414     for (i = 0; i < nvars; i++) {
02415         nodelist = dd->subtables[i].nodelist;
02416         tesubtotal = 0.0;
02417         nextsubtotal = 0.0;
02418         slots = dd->subtables[i].slots;
02419         for (j = 0; j < slots; j++) {
02420             scan = nodelist[j];
02421             while (scan != sentinel) {
02422                 diff = (long) scan - (long) cuddT(scan);
02423                 tesubtotal += (double) ddAbs(diff);
02424                 diff = (long) scan - (long) Cudd_Regular(cuddE(scan));
02425                 tesubtotal += (double) ddAbs(diff);
02426                 temeasured += 2.0;
02427                 if (scan->next != NULL) {
02428                     diff = (long) scan - (long) scan->next;
02429                     nextsubtotal += (double) ddAbs(diff);
02430                     nextmeasured += 1.0;
02431                 }
02432                 scan = scan->next;
02433             }
02434         }
02435         tetotal += tesubtotal;
02436         nexttotal += nextsubtotal;
02437     }
02438 
02439     /* Scan the constant table. */
02440     nodelist = dd->constants.nodelist;
02441     nextsubtotal = 0.0;
02442     slots = dd->constants.slots;
02443     for (j = 0; j < slots; j++) {
02444         scan = nodelist[j];
02445         while (scan != NULL) {
02446             if (scan->next != NULL) {
02447                 diff = (long) scan - (long) scan->next;
02448                 nextsubtotal += (double) ddAbs(diff);
02449                 nextmeasured += 1.0;
02450             }
02451             scan = scan->next;
02452         }
02453     }
02454     nexttotal += nextsubtotal;
02455 
02456     return((tetotal + nexttotal) / (temeasured + nextmeasured));
02457 
02458 } /* end of Cudd_AverageDistance */

DdNode* Cudd_bddComputeCube	(	DdManager *	dd,
		DdNode **	vars,
		int *	phase,
		int	n
	)

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

Synopsis [Computes the cube of an array of BDD variables.]

Description [Computes the cube of an array of BDD variables. If non-null, the phase argument indicates which literal of each variable should appear in the cube. If phase\[i\] is nonzero, then the positive literal is used. If phase is NULL, the cube is positive unate. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd]

Definition at line 1960 of file cuddUtil.c.

01965 {
01966     DdNode      *cube;
01967     DdNode      *fn;
01968     int         i;
01969 
01970     cube = DD_ONE(dd);
01971     cuddRef(cube);
01972 
01973     for (i = n - 1; i >= 0; i--) {
01974         if (phase == NULL || phase[i] != 0) {
01975             fn = Cudd_bddAnd(dd,vars[i],cube);
01976         } else {
01977             fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube);
01978         }
01979         if (fn == NULL) {
01980             Cudd_RecursiveDeref(dd,cube);
01981             return(NULL);
01982         }
01983         cuddRef(fn);
01984         Cudd_RecursiveDeref(dd,cube);
01985         cube = fn;
01986     }
01987     cuddDeref(cube);
01988 
01989     return(cube);
01990 
01991 }  /* end of Cudd_bddComputeCube */

DdNode** Cudd_bddPickArbitraryMinterms	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	n,
		int	k
	)

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

Synopsis [Picks k on-set minterms evenly distributed from given DD.]

Description [Picks k on-set minterms evenly distributed from given DD. The minterms are in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterms built by this procedure may not be contained in f. Builds an array of BDDs for the minterms and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:

It may run out of memory;
the function f may be the constant 0;
the minterms may not be contained in f.

]

SideEffects [None]

SeeAlso [Cudd_bddPickOneMinterm Cudd_bddPickOneCube]

Definition at line 1346 of file cuddUtil.c.

01352 {
01353     char **string;
01354     int i, j, l, size;
01355     int *indices;
01356     int result;
01357     DdNode **old, *neW;
01358     double minterms;
01359     char *saveString;
01360     int saveFlag, savePoint, isSame;
01361 
01362     minterms = Cudd_CountMinterm(dd,f,n);
01363     if ((double)k > minterms) {
01364         return(NULL);
01365     }
01366 
01367     size = dd->size;
01368     string = ALLOC(char *, k);
01369     if (string == NULL) {
01370         dd->errorCode = CUDD_MEMORY_OUT;
01371         return(NULL);
01372     }
01373     for (i = 0; i < k; i++) {
01374         string[i] = ALLOC(char, size + 1);
01375         if (string[i] == NULL) {
01376             for (j = 0; j < i; j++)
01377                 FREE(string[i]);
01378             FREE(string);
01379             dd->errorCode = CUDD_MEMORY_OUT;
01380             return(NULL);
01381         }
01382         for (j = 0; j < size; j++) string[i][j] = '2';
01383         string[i][size] = '\0';
01384     }
01385     indices = ALLOC(int,n);
01386     if (indices == NULL) {
01387         dd->errorCode = CUDD_MEMORY_OUT;
01388         for (i = 0; i < k; i++)
01389             FREE(string[i]);
01390         FREE(string);
01391         return(NULL);
01392     }
01393 
01394     for (i = 0; i < n; i++) {
01395         indices[i] = vars[i]->index;
01396     }
01397 
01398     result = ddPickArbitraryMinterms(dd,f,n,k,string);
01399     if (result == 0) {
01400         for (i = 0; i < k; i++)
01401             FREE(string[i]);
01402         FREE(string);
01403         FREE(indices);
01404         return(NULL);
01405     }
01406 
01407     old = ALLOC(DdNode *, k);
01408     if (old == NULL) {
01409         dd->errorCode = CUDD_MEMORY_OUT;
01410         for (i = 0; i < k; i++)
01411             FREE(string[i]);
01412         FREE(string);
01413         FREE(indices);
01414         return(NULL);
01415     }
01416     saveString = ALLOC(char, size + 1);
01417     if (saveString == NULL) {
01418         dd->errorCode = CUDD_MEMORY_OUT;
01419         for (i = 0; i < k; i++)
01420             FREE(string[i]);
01421         FREE(string);
01422         FREE(indices);
01423         FREE(old);
01424         return(NULL);
01425     }
01426     saveFlag = 0;
01427 
01428     /* Build result BDD array. */
01429     for (i = 0; i < k; i++) {
01430         isSame = 0;
01431         if (!saveFlag) {
01432             for (j = i + 1; j < k; j++) {
01433                 if (strcmp(string[i], string[j]) == 0) {
01434                     savePoint = i;
01435                     strcpy(saveString, string[i]);
01436                     saveFlag = 1;
01437                     break;
01438                 }
01439             }
01440         } else {
01441             if (strcmp(string[i], saveString) == 0) {
01442                 isSame = 1;
01443             } else {
01444                 saveFlag = 0;
01445                 for (j = i + 1; j < k; j++) {
01446                     if (strcmp(string[i], string[j]) == 0) {
01447                         savePoint = i;
01448                         strcpy(saveString, string[i]);
01449                         saveFlag = 1;
01450                         break;
01451                     }
01452                 }
01453             }
01454         }
01455         /* Randomize choice for don't cares. */
01456         for (j = 0; j < n; j++) {
01457             if (string[i][indices[j]] == '2')
01458                 string[i][indices[j]] = (Cudd_Random() & 0x20) ? '1' : '0';
01459         }
01460 
01461         while (isSame) {
01462             isSame = 0;
01463             for (j = savePoint; j < i; j++) {
01464                 if (strcmp(string[i], string[j]) == 0) {
01465                     isSame = 1;
01466                     break;
01467                 }
01468             }
01469             if (isSame) {
01470                 strcpy(string[i], saveString);
01471                 /* Randomize choice for don't cares. */
01472                 for (j = 0; j < n; j++) {
01473                     if (string[i][indices[j]] == '2') 
01474                         string[i][indices[j]] = (Cudd_Random() & 0x20) ?
01475                             '1' : '0';
01476                 }
01477             }
01478         }
01479 
01480         old[i] = Cudd_ReadOne(dd);
01481         cuddRef(old[i]);
01482 
01483         for (j = 0; j < n; j++) {
01484             if (string[i][indices[j]] == '0') {
01485                 neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
01486             } else {
01487                 neW = Cudd_bddAnd(dd,old[i],vars[j]);
01488             }
01489             if (neW == NULL) {
01490                 FREE(saveString);
01491                 for (l = 0; l < k; l++)
01492                     FREE(string[l]);
01493                 FREE(string);
01494                 FREE(indices);
01495                 for (l = 0; l <= i; l++)
01496                     Cudd_RecursiveDeref(dd,old[l]);
01497                 FREE(old);
01498                 return(NULL);
01499             }
01500             cuddRef(neW);
01501             Cudd_RecursiveDeref(dd,old[i]);
01502             old[i] = neW;
01503         }
01504 
01505         /* Test. */
01506         if (!Cudd_bddLeq(dd,old[i],f)) {
01507             FREE(saveString);
01508             for (l = 0; l < k; l++)
01509                 FREE(string[l]);
01510             FREE(string);
01511             FREE(indices);
01512             for (l = 0; l <= i; l++)
01513                 Cudd_RecursiveDeref(dd,old[l]);
01514             FREE(old);
01515             return(NULL);
01516         }
01517     }
01518 
01519     FREE(saveString);
01520     for (i = 0; i < k; i++) {
01521         cuddDeref(old[i]);
01522         FREE(string[i]);
01523     }
01524     FREE(string);
01525     FREE(indices);
01526     return(old);
01527 
01528 }  /* end of Cudd_bddPickArbitraryMinterms */

int Cudd_bddPickOneCube	(	DdManager *	ddm,
		DdNode *	node,
		char *	string
	)

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

Synopsis [Picks one on-set cube randomly from the given DD.]

Description [Picks one on-set cube randomly from the given DD. The cube is written into an array of characters. The array must have at least as many entries as there are variables. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddPickOneMinterm]

Definition at line 1174 of file cuddUtil.c.

01178 {
01179     DdNode *N, *T, *E;
01180     DdNode *one, *bzero;
01181     char   dir;
01182     int    i;
01183 
01184     if (string == NULL || node == NULL) return(0);
01185 
01186     /* The constant 0 function has no on-set cubes. */
01187     one = DD_ONE(ddm);
01188     bzero = Cudd_Not(one);
01189     if (node == bzero) return(0);
01190 
01191     for (i = 0; i < ddm->size; i++) string[i] = 2;
01192 
01193     for (;;) {
01194 
01195         if (node == one) break;
01196 
01197         N = Cudd_Regular(node);
01198 
01199         T = cuddT(N); E = cuddE(N);
01200         if (Cudd_IsComplement(node)) {
01201             T = Cudd_Not(T); E = Cudd_Not(E);
01202         }
01203         if (T == bzero) {
01204             string[N->index] = 0;
01205             node = E;
01206         } else if (E == bzero) {
01207             string[N->index] = 1;
01208             node = T;
01209         } else {
01210             dir = (char) ((Cudd_Random() & 0x2000) >> 13);
01211             string[N->index] = dir;
01212             node = dir ? T : E;
01213         }
01214     }
01215     return(1);
01216 
01217 } /* end of Cudd_bddPickOneCube */

DdNode* Cudd_bddPickOneMinterm	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	n
	)

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

Synopsis [Picks one on-set minterm randomly from the given DD.]

Description [Picks one on-set minterm randomly from the given DD. The minterm is in terms of vars. The array vars should contain at least all variables in the support of f; if this condition is not met the minterm built by this procedure may not be contained in f. Builds a BDD for the minterm and returns a pointer to it if successful; NULL otherwise. There are three reasons why the procedure may fail:

It may run out of memory;
the function f may be the constant 0;
the minterm may not be contained in f.

]

SideEffects [None]

SeeAlso [Cudd_bddPickOneCube]

Definition at line 1244 of file cuddUtil.c.

01249 {
01250     char *string;
01251     int i, size;
01252     int *indices;
01253     int result;
01254     DdNode *old, *neW;
01255 
01256     size = dd->size;
01257     string = ALLOC(char, size);
01258     if (string == NULL) {
01259         dd->errorCode = CUDD_MEMORY_OUT;
01260         return(NULL);
01261     }
01262     indices = ALLOC(int,n);
01263     if (indices == NULL) {
01264         dd->errorCode = CUDD_MEMORY_OUT;
01265         FREE(string);
01266         return(NULL);
01267     }
01268 
01269     for (i = 0; i < n; i++) {
01270         indices[i] = vars[i]->index;
01271     }
01272 
01273     result = Cudd_bddPickOneCube(dd,f,string);
01274     if (result == 0) {
01275         FREE(string);
01276         FREE(indices);
01277         return(NULL);
01278     }
01279 
01280     /* Randomize choice for don't cares. */
01281     for (i = 0; i < n; i++) {
01282         if (string[indices[i]] == 2) 
01283             string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5);
01284     }
01285 
01286     /* Build result BDD. */
01287     old = Cudd_ReadOne(dd);
01288     cuddRef(old);
01289 
01290     for (i = n-1; i >= 0; i--) {
01291         neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
01292         if (neW == NULL) {
01293             FREE(string);
01294             FREE(indices);
01295             Cudd_RecursiveDeref(dd,old);
01296             return(NULL);
01297         }
01298         cuddRef(neW);
01299         Cudd_RecursiveDeref(dd,old);
01300         old = neW;
01301     }
01302 
01303 #ifdef DD_DEBUG
01304     /* Test. */
01305     if (Cudd_bddLeq(dd,old,f)) {
01306         cuddDeref(old);
01307     } else {
01308         Cudd_RecursiveDeref(dd,old);
01309         old = NULL;
01310     }
01311 #else
01312     cuddDeref(old);
01313 #endif
01314 
01315     FREE(string);
01316     FREE(indices);
01317     return(old);
01318 
01319 }  /* end of Cudd_bddPickOneMinterm */

int Cudd_bddPrintCover	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

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

Synopsis [Prints a sum of prime implicants of a BDD.]

Description [Prints a sum of product cover for an incompletely specified function given by a lower bound and an upper bound. Each product is a prime implicant obtained by expanding the product corresponding to a path from node to the constant one. Uses the package default output file. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintMinterm]

Definition at line 212 of file cuddUtil.c.

00216 {
00217     int *array;
00218     int q, result;
00219     DdNode *lb;
00220 #ifdef DD_DEBUG
00221     DdNode *cover;
00222 #endif
00223 
00224     array = ALLOC(int, Cudd_ReadSize(dd));
00225     if (array == NULL) return(0);
00226     lb = l;
00227     cuddRef(lb);
00228 #ifdef DD_DEBUG
00229     cover = Cudd_ReadLogicZero(dd);
00230     cuddRef(cover);
00231 #endif
00232     while (lb != Cudd_ReadLogicZero(dd)) {
00233         DdNode *implicant, *prime, *tmp;
00234         int length;
00235         implicant = Cudd_LargestCube(dd,lb,&length);
00236         if (implicant == NULL) {
00237             Cudd_RecursiveDeref(dd,lb);
00238             FREE(array);
00239             return(0);
00240         }
00241         cuddRef(implicant);
00242         prime = Cudd_bddMakePrime(dd,implicant,u);
00243         if (prime == NULL) {
00244             Cudd_RecursiveDeref(dd,lb);
00245             Cudd_RecursiveDeref(dd,implicant);
00246             FREE(array);
00247             return(0);
00248         }
00249         cuddRef(prime);
00250         Cudd_RecursiveDeref(dd,implicant);
00251         tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime));
00252         if (tmp == NULL) {
00253             Cudd_RecursiveDeref(dd,lb);
00254             Cudd_RecursiveDeref(dd,prime);
00255             FREE(array);
00256             return(0);
00257         }
00258         cuddRef(tmp);
00259         Cudd_RecursiveDeref(dd,lb);
00260         lb = tmp;
00261         result = Cudd_BddToCubeArray(dd,prime,array);
00262         if (result == 0) {
00263             Cudd_RecursiveDeref(dd,lb);
00264             Cudd_RecursiveDeref(dd,prime);
00265             FREE(array);
00266             return(0);
00267         }
00268         for (q = 0; q < dd->size; q++) {
00269             switch (array[q]) {
00270             case 0:
00271                 (void) fprintf(dd->out, "0");
00272                 break;
00273             case 1:
00274                 (void) fprintf(dd->out, "1");
00275                 break;
00276             case 2:
00277                 (void) fprintf(dd->out, "-");
00278                 break;
00279             default:
00280                 (void) fprintf(dd->out, "?");
00281             }
00282         }
00283         (void) fprintf(dd->out, " 1\n");
00284 #ifdef DD_DEBUG
00285         tmp = Cudd_bddOr(dd,prime,cover);
00286         if (tmp == NULL) {
00287             Cudd_RecursiveDeref(dd,cover);
00288             Cudd_RecursiveDeref(dd,lb);
00289             Cudd_RecursiveDeref(dd,prime);
00290             FREE(array);
00291             return(0);
00292         }
00293         cuddRef(tmp);
00294         Cudd_RecursiveDeref(dd,cover);
00295         cover = tmp;
00296 #endif
00297         Cudd_RecursiveDeref(dd,prime);
00298     }
00299     (void) fprintf(dd->out, "\n");
00300     Cudd_RecursiveDeref(dd,lb);
00301     FREE(array);
00302 #ifdef DD_DEBUG
00303     if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
00304         Cudd_RecursiveDeref(dd,cover);
00305         return(0);
00306     }
00307     Cudd_RecursiveDeref(dd,cover);
00308 #endif
00309     return(1);
00310 
00311 } /* end of Cudd_bddPrintCover */

int Cudd_BddToCubeArray	(	DdManager *	dd,
		DdNode *	cube,
		int *	array
	)

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

Synopsis [Builds a positional array from the BDD of a cube.]

Description [Builds a positional array from the BDD of a cube. Array must have one entry for each BDD variable. The positional array has 1 in i-th position if the variable of index i appears in true form in the cube; it has 0 in i-th position if the variable of index i appears in complemented form in the cube; finally, it has 2 in i-th position if the variable of index i does not appear in the cube. Returns 1 if successful (the BDD is indeed a cube); 0 otherwise.]

SideEffects [The result is in the array passed by reference.]

SeeAlso [Cudd_CubeArrayToBdd]

Definition at line 2110 of file cuddUtil.c.

02114 {
02115     DdNode *scan, *t, *e;
02116     int i;
02117     int size = Cudd_ReadSize(dd);
02118     DdNode *zero = Cudd_Not(DD_ONE(dd));
02119 
02120     for (i = size-1; i >= 0; i--) {
02121         array[i] = 2;
02122     }
02123     scan = cube;
02124     while (!Cudd_IsConstant(scan)) {
02125         int index = Cudd_Regular(scan)->index;
02126         cuddGetBranches(scan,&t,&e);
02127         if (t == zero) {
02128             array[index] = 0;
02129             scan = e;
02130         } else if (e == zero) {
02131             array[index] = 1;
02132             scan = t;
02133         } else {
02134             return(0);  /* cube is not a cube */
02135         }
02136     }
02137     if (scan == zero) {
02138         return(0);
02139     } else {
02140         return(1);
02141     }
02142 
02143 } /* end of Cudd_BddToCubeArray */

int Cudd_ClassifySupport	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode **	common,
		DdNode **	onlyF,
		DdNode **	onlyG
	)

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

Synopsis [Classifies the variables in the support of two DDs.]

Description [Classifies the variables in the support of two DDs f and g, depending on whther they appear in both DDs, only in f, or only in g. Returns 1 if successful; 0 otherwise.]

SideEffects [The cubes of the three classes of variables are returned as side effects.]

SeeAlso [Cudd_Support Cudd_VectorSupport]

Definition at line 1038 of file cuddUtil.c.

01045 {
01046     int *supportF, *supportG;
01047     DdNode *tmp, *var;
01048     int i,j;
01049     int size;
01050 
01051     /* Allocate and initialize support arrays for ddSupportStep. */
01052     size = ddMax(dd->size, dd->sizeZ);
01053     supportF = ALLOC(int,size);
01054     if (supportF == NULL) {
01055         dd->errorCode = CUDD_MEMORY_OUT;
01056         return(0);
01057     }
01058     supportG = ALLOC(int,size);
01059     if (supportG == NULL) {
01060         dd->errorCode = CUDD_MEMORY_OUT;
01061         FREE(supportF);
01062         return(0);
01063     }
01064     for (i = 0; i < size; i++) {
01065         supportF[i] = 0;
01066         supportG[i] = 0;
01067     }
01068 
01069     /* Compute supports and clean up markers. */
01070     ddSupportStep(Cudd_Regular(f),supportF);
01071     ddClearFlag(Cudd_Regular(f));
01072     ddSupportStep(Cudd_Regular(g),supportG);
01073     ddClearFlag(Cudd_Regular(g));
01074 
01075     /* Classify variables and create cubes. */
01076     *common = *onlyF = *onlyG = DD_ONE(dd);
01077     cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG);
01078     for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
01079         i = (j >= dd->size) ? j : dd->invperm[j];
01080         if (supportF[i] == 0 && supportG[i] == 0) continue;
01081         var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
01082         cuddRef(var);
01083         if (supportG[i] == 0) {
01084             tmp = Cudd_bddAnd(dd,*onlyF,var);
01085             if (tmp == NULL) {
01086                 Cudd_RecursiveDeref(dd,*common);
01087                 Cudd_RecursiveDeref(dd,*onlyF);
01088                 Cudd_RecursiveDeref(dd,*onlyG);
01089                 Cudd_RecursiveDeref(dd,var);
01090                 FREE(supportF); FREE(supportG);
01091                 return(0);
01092             }
01093             cuddRef(tmp);
01094             Cudd_RecursiveDeref(dd,*onlyF);
01095             *onlyF = tmp;
01096         } else if (supportF[i] == 0) {
01097             tmp = Cudd_bddAnd(dd,*onlyG,var);
01098             if (tmp == NULL) {
01099                 Cudd_RecursiveDeref(dd,*common);
01100                 Cudd_RecursiveDeref(dd,*onlyF);
01101                 Cudd_RecursiveDeref(dd,*onlyG);
01102                 Cudd_RecursiveDeref(dd,var);
01103                 FREE(supportF); FREE(supportG);
01104                 return(0);
01105             }
01106             cuddRef(tmp);
01107             Cudd_RecursiveDeref(dd,*onlyG);
01108             *onlyG = tmp;
01109         } else {
01110             tmp = Cudd_bddAnd(dd,*common,var);
01111             if (tmp == NULL) {
01112                 Cudd_RecursiveDeref(dd,*common);
01113                 Cudd_RecursiveDeref(dd,*onlyF);
01114                 Cudd_RecursiveDeref(dd,*onlyG);
01115                 Cudd_RecursiveDeref(dd,var);
01116                 FREE(supportF); FREE(supportG);
01117                 return(0);
01118             }
01119             cuddRef(tmp);
01120             Cudd_RecursiveDeref(dd,*common);
01121             *common = tmp;
01122         }
01123         Cudd_RecursiveDeref(dd,var);
01124     }
01125 
01126     FREE(supportF); FREE(supportG);
01127     cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
01128     return(1);
01129 
01130 } /* end of Cudd_ClassifySupport */

int Cudd_CountLeaves ( DdNode * node )

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

Synopsis [Counts the number of leaves in a DD.]

Description [Counts the number of leaves in a DD. Returns the number of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug]

Definition at line 1147 of file cuddUtil.c.

01149 {
01150     int i;      
01151 
01152     i = ddLeavesInt(Cudd_Regular(node));
01153     ddClearFlag(Cudd_Regular(node));
01154     return(i);
01155 
01156 } /* end of Cudd_CountLeaves */

double Cudd_CountMinterm	(	DdManager *	manager,
		DdNode *	node,
		int	nvars
	)

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

Synopsis [Counts the number of minterms of a DD.]

Description [Counts the number of minterms of a DD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug Cudd_CountPath]

Definition at line 537 of file cuddUtil.c.

00541 {
00542     double      max;
00543     DdHashTable *table;
00544     double      res;
00545     CUDD_VALUE_TYPE epsilon;
00546 
00547     background = manager->background;
00548     zero = Cudd_Not(manager->one);
00549     
00550     max = pow(2.0,(double)nvars);
00551     table = cuddHashTableInit(manager,1,2);
00552     if (table == NULL) {
00553         return((double)CUDD_OUT_OF_MEM);
00554     }
00555     epsilon = Cudd_ReadEpsilon(manager);
00556     Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0);
00557     res = ddCountMintermAux(node,max,table);
00558     cuddHashTableQuit(table);
00559     Cudd_SetEpsilon(manager,epsilon);
00560 
00561     return(res);
00562 
00563 } /* end of Cudd_CountMinterm */

double Cudd_CountPath ( DdNode * node )

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

Synopsis [Counts the number of paths of a DD.]

Description [Counts the number of paths of a DD. Paths to all terminal nodes are counted. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_CountMinterm]

Definition at line 582 of file cuddUtil.c.

00584 {
00585 
00586     st_table    *table;
00587     double      i;      
00588 
00589     table = st_init_table(st_ptrcmp,st_ptrhash);
00590     if (table == NULL) {
00591         return((double)CUDD_OUT_OF_MEM);
00592     }
00593     i = ddCountPathAux(Cudd_Regular(node),table);
00594     st_foreach(table, cuddStCountfree, NULL);
00595     st_free_table(table);
00596     return(i);
00597 
00598 } /* end of Cudd_CountPath */

double Cudd_CountPathsToNonZero ( DdNode * node )

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

Synopsis [Counts the number of paths to a non-zero terminal of a DD.]

Description [Counts the number of paths to a non-zero terminal of a DD. The path count is represented as a double, to allow for a larger number of variables. Returns the number of paths of the function rooted at node.]

SideEffects [None]

SeeAlso [Cudd_CountMinterm Cudd_CountPath]

Definition at line 666 of file cuddUtil.c.

00668 {
00669 
00670     st_table    *table;
00671     double      i;      
00672 
00673     table = st_init_table(st_ptrcmp,st_ptrhash);
00674     if (table == NULL) {
00675         return((double)CUDD_OUT_OF_MEM);
00676     }
00677     i = ddCountPathsToNonZero(node,table);
00678     st_foreach(table, cuddStCountfree, NULL);
00679     st_free_table(table);
00680     return(i);
00681 
00682 } /* end of Cudd_CountPathsToNonZero */

DdNode* Cudd_CubeArrayToBdd	(	DdManager *	dd,
		int *	array
	)

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

Synopsis [Builds the BDD of a cube from a positional array.]

Description [Builds a cube from a positional array. The array must have one integer entry for each BDD variable. If the i-th entry is 1, the variable of index i appears in true form in the cube; If the i-th entry is 0, the variable of index i appears complemented in the cube; otherwise the variable does not appear in the cube. Returns a pointer to the BDD for the cube if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]

Definition at line 2062 of file cuddUtil.c.

02065 {
02066     DdNode *cube, *var, *tmp;
02067     int i;
02068     int size = Cudd_ReadSize(dd);
02069 
02070     cube = DD_ONE(dd);
02071     cuddRef(cube);
02072     for (i = size - 1; i >= 0; i--) {
02073         if ((array[i] & ~1) == 0) {
02074             var = Cudd_bddIthVar(dd,i);
02075             tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0));
02076             if (tmp == NULL) {
02077                 Cudd_RecursiveDeref(dd,cube);
02078                 return(NULL);
02079             }
02080             cuddRef(tmp);
02081             Cudd_RecursiveDeref(dd,cube);
02082             cube = tmp;
02083         }
02084     }
02085     cuddDeref(cube);
02086     return(cube);
02087 
02088 } /* end of Cudd_CubeArrayToBdd */

int Cudd_DagSize ( DdNode * node )

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

Synopsis [Counts the number of nodes in a DD.]

Description [Counts the number of nodes in a DD. Returns the number of nodes in the graph rooted at node.]

SideEffects [None]

SeeAlso [Cudd_SharingSize Cudd_PrintDebug]

Definition at line 401 of file cuddUtil.c.

00403 {
00404     int i;      
00405 
00406     i = ddDagInt(Cudd_Regular(node));
00407     ddClearFlag(Cudd_Regular(node));
00408 
00409     return(i);
00410 
00411 } /* end of Cudd_DagSize */

double Cudd_Density	(	DdManager *	dd,
		DdNode *	f,
		int	nvars
	)

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

Synopsis [Computes the density of a BDD or ADD.]

Description [Computes the density of a BDD or ADD. The density is the ratio of the number of minterms to the number of nodes. If 0 is passed as number of variables, the number of variables existing in the manager is used. Returns the density if successful; (double) CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_CountMinterm Cudd_DagSize]

Definition at line 2580 of file cuddUtil.c.

02584 {
02585     double minterms;
02586     int nodes;
02587     double density;
02588 
02589     if (nvars == 0) nvars = dd->size;
02590     minterms = Cudd_CountMinterm(dd,f,nvars);
02591     if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms);
02592     nodes = Cudd_DagSize(f);
02593     density = minterms / (double) nodes;
02594     return(density);
02595 
02596 } /* end of Cudd_Density */

int Cudd_EpdCountMinterm	(	DdManager *	manager,
		DdNode *	node,
		int	nvars,
		EpDouble *	epd
	)

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

Synopsis [Counts the number of minterms of a DD with extended precision.]

Description [Counts the number of minterms of a DD with extended precision. The function is assumed to depend on nvars variables. The minterm count is represented as an EpDouble, to allow any number of variables. Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug Cudd_CountPath]

Definition at line 616 of file cuddUtil.c.

00621 {
00622     EpDouble    max, tmp;
00623     st_table    *table;
00624     int         status;
00625 
00626     background = manager->background;
00627     zero = Cudd_Not(manager->one);
00628     
00629     EpdPow2(nvars, &max);
00630     table = st_init_table(EpdCmp, st_ptrhash);
00631     if (table == NULL) {
00632         EpdMakeZero(epd, 0);
00633         return(CUDD_OUT_OF_MEM);
00634     }
00635     status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table);
00636     st_foreach(table, ddEpdFree, NULL);
00637     st_free_table(table);
00638     if (status == CUDD_OUT_OF_MEM) {
00639         EpdMakeZero(epd, 0);
00640         return(CUDD_OUT_OF_MEM);
00641     }
00642     if (Cudd_IsComplement(node)) {
00643         EpdSubtract3(&max, epd, &tmp);
00644         EpdCopy(&tmp, epd);
00645     }
00646     return(0);
00647 
00648 } /* end of Cudd_EpdCountMinterm */

int Cudd_EstimateCofactor	(	DdManager *	dd,
		DdNode *	f,
		int	i,
		int	phase
	)

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

Synopsis [Estimates the number of nodes in a cofactor of a DD.]

Description [Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in a cofactor of the graph rooted at node with respect to the variable whose index is i. In case of failure, returns CUDD_OUT_OF_MEM. This function uses a refinement of the algorithm of Cabodi et al. (ICCAD96). The refinement allows the procedure to account for part of the recombination that may occur in the part of the cofactor above the cofactoring variable. This procedure does no create any new node. It does keep a small table of results; therefore itmay run out of memory. If this is a concern, one should use Cudd_EstimateCofactorSimple, which is faster, does not allocate any memory, but is less accurate.]

SideEffects [None]

SeeAlso [Cudd_DagSize Cudd_EstimateCofactorSimple]

Definition at line 436 of file cuddUtil.c.

00440                     : positive; 0: negative */
00441   )
00442 {
00443     int val;
00444     DdNode *ptr;
00445     st_table *table;
00446 
00447     table = st_init_table(st_ptrcmp,st_ptrhash);
00448     if (table == NULL) return(CUDD_OUT_OF_MEM);
00449     val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr);
00450     ddClearFlag(Cudd_Regular(f));
00451     st_free_table(table);
00452 
00453     return(val);
00454 
00455 } /* end of Cudd_EstimateCofactor */

int Cudd_EstimateCofactorSimple	(	DdNode *	node,
		int	i
	)

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

Synopsis [Estimates the number of nodes in a cofactor of a DD.]

Description [Estimates the number of nodes in a cofactor of a DD. Returns an estimate of the number of nodes in the positive cofactor of the graph rooted at node with respect to the variable whose index is i. This procedure implements with minor changes the algorithm of Cabodi et al. (ICCAD96). It does not allocate any memory, it does not change the state of the manager, and it is fast. However, it has been observed to overestimate the size of the cofactor by as much as a factor of 2.]

SideEffects [None]

SeeAlso [Cudd_DagSize]

Definition at line 476 of file cuddUtil.c.

00479 {
00480     int val;    
00481 
00482     val = cuddEstimateCofactorSimple(Cudd_Regular(node),i);
00483     ddClearFlag(Cudd_Regular(node));
00484 
00485     return(val);
00486 
00487 } /* end of Cudd_EstimateCofactorSimple */

DdGen* Cudd_FirstCube	(	DdManager *	dd,
		DdNode *	f,
		int **	cube,
		CUDD_VALUE_TYPE *	value
	)

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

Synopsis [Finds the first cube of a decision diagram.]

Description [Defines an iterator on the onset of a decision diagram and finds its first cube. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.

A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a disjoint cover of the function associated with the diagram. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.

For each cube, a value is also returned. This value is always 1 for a BDD, while it may be different from 1 for an ADD. For BDDs, the offset is the set of cubes whose value is the logical zero. For ADDs, the offset is the set of cubes whose value is the background value. The cubes of the offset are not enumerated.]

SideEffects [The first cube and its value are returned as side effects.]

SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstNode]

Definition at line 1744 of file cuddUtil.c.

01749 {
01750     DdGen *gen;
01751     DdNode *top, *treg, *next, *nreg, *prev, *preg;
01752     int i;
01753     int nvars;
01754 
01755     /* Sanity Check. */
01756     if (dd == NULL || f == NULL) return(NULL);
01757 
01758     /* Allocate generator an initialize it. */
01759     gen = ALLOC(DdGen,1);
01760     if (gen == NULL) {
01761         dd->errorCode = CUDD_MEMORY_OUT;
01762         return(NULL);
01763     }
01764 
01765     gen->manager = dd;
01766     gen->type = CUDD_GEN_CUBES;
01767     gen->status = CUDD_GEN_EMPTY;
01768     gen->gen.cubes.cube = NULL;
01769     gen->gen.cubes.value = DD_ZERO_VAL;
01770     gen->stack.sp = 0;
01771     gen->stack.stack = NULL;
01772     gen->node = NULL;
01773 
01774     nvars = dd->size;
01775     gen->gen.cubes.cube = ALLOC(int,nvars);
01776     if (gen->gen.cubes.cube == NULL) {
01777         dd->errorCode = CUDD_MEMORY_OUT;
01778         FREE(gen);
01779         return(NULL);
01780     }
01781     for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
01782 
01783     /* The maximum stack depth is one plus the number of variables.
01784     ** because a path may have nodes at all levels, including the
01785     ** constant level.
01786     */
01787     gen->stack.stack = ALLOC(DdNode *, nvars+1);
01788     if (gen->stack.stack == NULL) {
01789         dd->errorCode = CUDD_MEMORY_OUT;
01790         FREE(gen->gen.cubes.cube);
01791         FREE(gen);
01792         return(NULL);
01793     }
01794     for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
01795 
01796     /* Find the first cube of the onset. */
01797     gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
01798 
01799     while (1) {
01800         top = gen->stack.stack[gen->stack.sp-1];
01801         treg = Cudd_Regular(top);
01802         if (!cuddIsConstant(treg)) {
01803             /* Take the else branch first. */
01804             gen->gen.cubes.cube[treg->index] = 0;
01805             next = cuddE(treg);
01806             if (top != treg) next = Cudd_Not(next);
01807             gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
01808         } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
01809             /* Backtrack */
01810             while (1) {
01811                 if (gen->stack.sp == 1) {
01812                     /* The current node has no predecessor. */
01813                     gen->status = CUDD_GEN_EMPTY;
01814                     gen->stack.sp--;
01815                     goto done;
01816                 }
01817                 prev = gen->stack.stack[gen->stack.sp-2];
01818                 preg = Cudd_Regular(prev);
01819                 nreg = cuddT(preg);
01820                 if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
01821                 if (next != top) { /* follow the then branch next */
01822                     gen->gen.cubes.cube[preg->index] = 1;
01823                     gen->stack.stack[gen->stack.sp-1] = next;
01824                     break;
01825                 }
01826                 /* Pop the stack and try again. */
01827                 gen->gen.cubes.cube[preg->index] = 2;
01828                 gen->stack.sp--;
01829                 top = gen->stack.stack[gen->stack.sp-1];
01830                 treg = Cudd_Regular(top);
01831             }
01832         } else {
01833             gen->status = CUDD_GEN_NONEMPTY;
01834             gen->gen.cubes.value = cuddV(top);
01835             goto done;
01836         }
01837     }
01838 
01839 done:
01840     *cube = gen->gen.cubes.cube;
01841     *value = gen->gen.cubes.value;
01842     return(gen);
01843 
01844 } /* end of Cudd_FirstCube */

DdGen* Cudd_FirstNode	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	node
	)

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

Synopsis [Finds the first node of a decision diagram.]

Description [Defines an iterator on the nodes of a decision diagram and finds its first node. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.]

SideEffects [The first node is returned as a side effect.]

SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube]

Definition at line 2162 of file cuddUtil.c.

02166 {
02167     DdGen *gen;
02168     int retval;
02169 
02170     /* Sanity Check. */
02171     if (dd == NULL || f == NULL) return(NULL);
02172 
02173     /* Allocate generator an initialize it. */
02174     gen = ALLOC(DdGen,1);
02175     if (gen == NULL) {
02176         dd->errorCode = CUDD_MEMORY_OUT;
02177         return(NULL);
02178     }
02179 
02180     gen->manager = dd;
02181     gen->type = CUDD_GEN_NODES;
02182     gen->status = CUDD_GEN_EMPTY;
02183     gen->gen.nodes.visited = NULL;
02184     gen->gen.nodes.stGen = NULL;
02185     gen->stack.sp = 0;
02186     gen->stack.stack = NULL;
02187     gen->node = NULL;
02188 
02189     gen->gen.nodes.visited = st_init_table(st_ptrcmp,st_ptrhash);
02190     if (gen->gen.nodes.visited == NULL) {
02191         FREE(gen);
02192         return(NULL);
02193     }
02194 
02195     /* Collect all the nodes in a st table for later perusal. */
02196     retval = cuddCollectNodes(Cudd_Regular(f),gen->gen.nodes.visited);
02197     if (retval == 0) {
02198         st_free_table(gen->gen.nodes.visited);
02199         FREE(gen);
02200         return(NULL);
02201     }
02202 
02203     /* Initialize the st table generator. */
02204     gen->gen.nodes.stGen = st_init_gen(gen->gen.nodes.visited);
02205     if (gen->gen.nodes.stGen == NULL) {
02206         st_free_table(gen->gen.nodes.visited);
02207         FREE(gen);
02208         return(NULL);
02209     }
02210 
02211     /* Find the first node. */
02212     retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
02213     if (retval != 0) {
02214         gen->status = CUDD_GEN_NONEMPTY;
02215         *node = gen->node;
02216     }
02217 
02218     return(gen);
02219 
02220 } /* end of Cudd_FirstNode */

int Cudd_GenFree ( DdGen * gen )

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

Synopsis [Frees a CUDD generator.]

Description [Frees a CUDD generator. Always returns 0, so that it can be used in mis-like foreach constructs.]

SideEffects [None]

SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]

Definition at line 2270 of file cuddUtil.c.

02272 {
02273 
02274     if (gen == NULL) return(0);
02275     switch (gen->type) {
02276     case CUDD_GEN_CUBES:
02277     case CUDD_GEN_ZDD_PATHS:
02278         FREE(gen->gen.cubes.cube);
02279         FREE(gen->stack.stack);
02280         break;
02281     case CUDD_GEN_NODES:
02282         st_free_gen(gen->gen.nodes.stGen);
02283         st_free_table(gen->gen.nodes.visited);
02284         break;
02285     default:
02286         return(0);
02287     }
02288     FREE(gen);
02289     return(0);
02290 
02291 } /* end of Cudd_GenFree */

DdNode* Cudd_IndicesToCube	(	DdManager *	dd,
		int *	array,
		int	n
	)

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

Synopsis [Builds a cube of BDD variables from an array of indices.]

Description [Builds a cube of BDD variables from an array of indices. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddComputeCube Cudd_CubeArrayToBdd]

Definition at line 2330 of file cuddUtil.c.

02334 {
02335     DdNode *cube, *tmp;
02336     int i;
02337 
02338     cube = DD_ONE(dd);
02339     cuddRef(cube);
02340     for (i = n - 1; i >= 0; i--) {
02341         tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube);
02342         if (tmp == NULL) {
02343             Cudd_RecursiveDeref(dd,cube);
02344             return(NULL);
02345         }
02346         cuddRef(tmp);
02347         Cudd_RecursiveDeref(dd,cube);
02348         cube = tmp;
02349     }
02350 
02351     cuddDeref(cube);
02352     return(cube);
02353 
02354 } /* end of Cudd_IndicesToCube */

int Cudd_IsGenEmpty ( DdGen * gen )

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

Synopsis [Queries the status of a generator.]

Description [Queries the status of a generator. Returns 1 if the generator is empty or NULL; 0 otherswise.]

SideEffects [None]

SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree]

Definition at line 2308 of file cuddUtil.c.

02310 {
02311     if (gen == NULL) return(1);
02312     return(gen->status == CUDD_GEN_EMPTY);
02313 
02314 } /* end of Cudd_IsGenEmpty */

int Cudd_NextCube	(	DdGen *	gen,
		int **	cube,
		CUDD_VALUE_TYPE *	value
	)

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

Synopsis [Generates the next cube of a decision diagram onset.]

Description [Generates the next cube of a decision diagram onset, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]

SideEffects [The cube and its value are returned as side effects. The generator is modified.]

SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty Cudd_NextNode]

Definition at line 1863 of file cuddUtil.c.

01867 {
01868     DdNode *top, *treg, *next, *nreg, *prev, *preg;
01869     DdManager *dd = gen->manager;
01870 
01871     /* Backtrack from previously reached terminal node. */
01872     while (1) {
01873         if (gen->stack.sp == 1) {
01874             /* The current node has no predecessor. */
01875             gen->status = CUDD_GEN_EMPTY;
01876             gen->stack.sp--;
01877             goto done;
01878         }
01879         top = gen->stack.stack[gen->stack.sp-1];
01880         treg = Cudd_Regular(top);
01881         prev = gen->stack.stack[gen->stack.sp-2];
01882         preg = Cudd_Regular(prev);
01883         nreg = cuddT(preg);
01884         if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
01885         if (next != top) { /* follow the then branch next */
01886             gen->gen.cubes.cube[preg->index] = 1;
01887             gen->stack.stack[gen->stack.sp-1] = next;
01888             break;
01889         }
01890         /* Pop the stack and try again. */
01891         gen->gen.cubes.cube[preg->index] = 2;
01892         gen->stack.sp--;
01893     }
01894 
01895     while (1) {
01896         top = gen->stack.stack[gen->stack.sp-1];
01897         treg = Cudd_Regular(top);
01898         if (!cuddIsConstant(treg)) {
01899             /* Take the else branch first. */
01900             gen->gen.cubes.cube[treg->index] = 0;
01901             next = cuddE(treg);
01902             if (top != treg) next = Cudd_Not(next);
01903             gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
01904         } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
01905             /* Backtrack */
01906             while (1) {
01907                 if (gen->stack.sp == 1) {
01908                     /* The current node has no predecessor. */
01909                     gen->status = CUDD_GEN_EMPTY;
01910                     gen->stack.sp--;
01911                     goto done;
01912                 }
01913                 prev = gen->stack.stack[gen->stack.sp-2];
01914                 preg = Cudd_Regular(prev);
01915                 nreg = cuddT(preg);
01916                 if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
01917                 if (next != top) { /* follow the then branch next */
01918                     gen->gen.cubes.cube[preg->index] = 1;
01919                     gen->stack.stack[gen->stack.sp-1] = next;
01920                     break;
01921                 }
01922                 /* Pop the stack and try again. */
01923                 gen->gen.cubes.cube[preg->index] = 2;
01924                 gen->stack.sp--;
01925                 top = gen->stack.stack[gen->stack.sp-1];
01926                 treg = Cudd_Regular(top);
01927             }
01928         } else {
01929             gen->status = CUDD_GEN_NONEMPTY;
01930             gen->gen.cubes.value = cuddV(top);
01931             goto done;
01932         }
01933     }
01934 
01935 done:
01936     if (gen->status == CUDD_GEN_EMPTY) return(0);
01937     *cube = gen->gen.cubes.cube;
01938     *value = gen->gen.cubes.value;
01939     return(1);
01940 
01941 } /* end of Cudd_NextCube */

int Cudd_NextNode	(	DdGen *	gen,
		DdNode **	node
	)

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

Synopsis [Finds the next node of a decision diagram.]

Description [Finds the node of a decision diagram, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]

SideEffects [The next node is returned as a side effect.]

SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube]

Definition at line 2237 of file cuddUtil.c.

02240 {
02241     int retval;
02242 
02243     /* Find the next node. */
02244     retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL);
02245     if (retval == 0) {
02246         gen->status = CUDD_GEN_EMPTY;
02247     } else {
02248         *node = gen->node;
02249     }
02250 
02251     return(retval);
02252 
02253 } /* end of Cudd_NextNode */

void Cudd_OutOfMem ( long size )

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

Synopsis [Warns that a memory allocation failed.]

Description [Warns that a memory allocation failed. This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, the allocation of memory to enlarge the computed table.]

SideEffects [None]

SeeAlso []

Definition at line 2615 of file cuddUtil.c.

02617 {
02618     (void) fflush(stdout);
02619     (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size);
02620     return;
02621 
02622 } /* end of Cudd_OutOfMem */

int Cudd_PrintDebug	(	DdManager *	dd,
		DdNode *	f,
		int	n,
		int	pr
	)

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

Synopsis [Prints to the standard output a DD and its statistics.]

Description [Prints to the standard output a DD and its statistics. The statistics include the number of nodes, the number of leaves, and the number of minterms. (The number of minterms is the number of assignments to the variables that cause the function to be different from the logical zero (for BDDs) and from the background value (for ADDs.) The statistics are printed if pr > 0. Specifically:

pr = 0 : prints nothing
pr = 1 : prints counts of nodes and minterms
pr = 2 : prints counts + disjoint sum of product
pr = 3 : prints counts + list of nodes
pr > 3 : prints counts + disjoint sum of product + list of nodes

For the purpose of counting the number of minterms, the function is supposed to depend on n variables. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm Cudd_PrintMinterm]

Definition at line 341 of file cuddUtil.c.

00346 {
00347     DdNode *azero, *bzero;
00348     int    nodes;
00349     int    leaves;
00350     double minterms;
00351     int    retval = 1;
00352 
00353     if (f == NULL) {
00354         (void) fprintf(dd->out,": is the NULL DD\n");
00355         (void) fflush(dd->out);
00356         return(0);
00357     }
00358     azero = DD_ZERO(dd);
00359     bzero = Cudd_Not(DD_ONE(dd));
00360     if ((f == azero || f == bzero) && pr > 0){
00361        (void) fprintf(dd->out,": is the zero DD\n");
00362        (void) fflush(dd->out);
00363        return(1);
00364     }
00365     if (pr > 0) {
00366         nodes = Cudd_DagSize(f);
00367         if (nodes == CUDD_OUT_OF_MEM) retval = 0;
00368         leaves = Cudd_CountLeaves(f);
00369         if (leaves == CUDD_OUT_OF_MEM) retval = 0;
00370         minterms = Cudd_CountMinterm(dd, f, n);
00371         if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
00372         (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n",
00373                        nodes, leaves, minterms);
00374         if (pr > 2) {
00375             if (!cuddP(dd, f)) retval = 0;
00376         }
00377         if (pr == 2 || pr > 3) {
00378             if (!Cudd_PrintMinterm(dd,f)) retval = 0;
00379             (void) fprintf(dd->out,"\n");
00380         }
00381         (void) fflush(dd->out);
00382     }
00383     return(retval);
00384 
00385 } /* end of Cudd_PrintDebug */

int Cudd_PrintMinterm	(	DdManager *	manager,
		DdNode *	node
	)

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

Synopsis [Prints a disjoint sum of products.]

Description [Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node to a leaf node different from the logical zero, and different from the background value. Uses the package default output file. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug Cudd_bddPrintCover]

Definition at line 175 of file cuddUtil.c.

00178 {
00179     int         i, *list;
00180 
00181     background = manager->background;
00182     zero = Cudd_Not(manager->one);
00183     list = ALLOC(int,manager->size);
00184     if (list == NULL) {
00185         manager->errorCode = CUDD_MEMORY_OUT;
00186         return(0);
00187     }
00188     for (i = 0; i < manager->size; i++) list[i] = 2;
00189     ddPrintMintermAux(manager,node,list);
00190     FREE(list);
00191     return(1);
00192 
00193 } /* end of Cudd_PrintMinterm */

void Cudd_PrintVersion ( FILE * fp )

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

Synopsis [Prints the package version number.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 2369 of file cuddUtil.c.

02371 {
02372     (void) fprintf(fp, "%s\n", CUDD_VERSION);
02373 
02374 } /* end of Cudd_PrintVersion */

long Cudd_Random ( )

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

Synopsis [Portable random number generator.]

Description [Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The random generator can be explicitly initialized by calling Cudd_Srandom. If no explicit initialization is performed, then the seed 1 is assumed.]

SideEffects [None]

SeeAlso [Cudd_Srandom]

Definition at line 2479 of file cuddUtil.c.

02481 {
02482     int i;      /* index in the shuffle table */
02483     long int w; /* work variable */
02484 
02485     /* cuddRand == 0 if the geneartor has not been initialized yet. */
02486     if (cuddRand == 0) Cudd_Srandom(1);
02487 
02488     /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding
02489     ** overflows by Schrage's method.
02490     */
02491     w          = cuddRand / LEQQ1;
02492     cuddRand   = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
02493     cuddRand  += (cuddRand < 0) * MODULUS1;
02494 
02495     /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding
02496     ** overflows by Schrage's method.
02497     */
02498     w          = cuddRand2 / LEQQ2;
02499     cuddRand2  = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2;
02500     cuddRand2 += (cuddRand2 < 0) * MODULUS2;
02501 
02502     /* cuddRand is shuffled with the Bays-Durham algorithm.
02503     ** shuffleSelect and cuddRand2 are combined to generate the output.
02504     */
02505 
02506     /* Pick one element from the shuffle table; "i" will be in the range
02507     ** from 0 to STAB_SIZE-1.
02508     */
02509     i = (int) (shuffleSelect / STAB_DIV);
02510     /* Mix the element of the shuffle table with the current iterate of
02511     ** the second sub-generator, and replace the chosen element of the
02512     ** shuffle table with the current iterate of the first sub-generator.
02513     */
02514     shuffleSelect   = shuffleTable[i] - cuddRand2;
02515     shuffleTable[i] = cuddRand;
02516     shuffleSelect  += (shuffleSelect < 1) * (MODULUS1 - 1);
02517     /* Since shuffleSelect != 0, and we want to be able to return 0,
02518     ** here we subtract 1 before returning.
02519     */
02520     return(shuffleSelect - 1);
02521 
02522 } /* end of Cudd_Random */

int Cudd_SharingSize	(	DdNode **	nodeArray,
		int	n
	)

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

Synopsis [Counts the number of nodes in an array of DDs.]

Description [Counts the number of nodes in an array of DDs. Shared nodes are counted only once. Returns the total number of nodes.]

SideEffects [None]

SeeAlso [Cudd_DagSize]

Definition at line 503 of file cuddUtil.c.

00506 {
00507     int i,j;    
00508 
00509     i = 0;
00510     for (j = 0; j < n; j++) {
00511         i += ddDagInt(Cudd_Regular(nodeArray[j]));
00512     }
00513     for (j = 0; j < n; j++) {
00514         ddClearFlag(Cudd_Regular(nodeArray[j]));
00515     }
00516     return(i);
00517 
00518 } /* end of Cudd_SharingSize */

void Cudd_Srandom ( long seed )

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

Synopsis [Initializer for the portable random number generator.]

Description [Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.]

SideEffects [None]

SeeAlso [Cudd_Random]

Definition at line 2542 of file cuddUtil.c.

02544 {
02545     int i;
02546 
02547     if (seed < 0)       cuddRand = -seed;
02548     else if (seed == 0) cuddRand = 1;
02549     else                cuddRand = seed;
02550     cuddRand2 = cuddRand;
02551     /* Load the shuffle table (after 11 warm-ups). */
02552     for (i = 0; i < STAB_SIZE + 11; i++) {
02553         long int w;
02554         w = cuddRand / LEQQ1;
02555         cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1;
02556         cuddRand += (cuddRand < 0) * MODULUS1;
02557         shuffleTable[i % STAB_SIZE] = cuddRand;
02558     }
02559     shuffleSelect = shuffleTable[1 % STAB_SIZE];
02560 
02561 } /* end of Cudd_Srandom */

DdNode* Cudd_SubsetWithMaskVars	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vars,
		int	nvars,
		DdNode **	maskVars,
		int	mvars
	)

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

Synopsis [Extracts a subset from a BDD.]

Description [Extracts a subset from a BDD in the following procedure. 1. Compute the weight for each mask variable by counting the number of minterms for both positive and negative cofactors of the BDD with respect to each mask variable. (weight = positive - negative) 2. Find a representative cube of the BDD by using the weight. From the top variable of the BDD, for each variable, if the weight is greater than 0.0, choose THEN branch, othereise ELSE branch, until meeting the constant 1. 3. Quantify out the variables not in maskVars from the representative cube and if a variable in maskVars is don't care, replace the variable with a constant(1 or 0) depending on the weight. 4. Make a subset of the BDD by multiplying with the modified cube.]

SideEffects [None]

SeeAlso []

Definition at line 1554 of file cuddUtil.c.

01561 {
01562     double      *weight;
01563     char        *string;
01564     int         i, size;
01565     int         *indices, *mask;
01566     int         result;
01567     DdNode      *zero, *cube, *newCube, *subset;
01568     DdNode      *cof;
01569 
01570     DdNode      *support;
01571     support = Cudd_Support(dd,f);
01572     cuddRef(support);
01573     Cudd_RecursiveDeref(dd,support);
01574 
01575     zero = Cudd_Not(dd->one);
01576     size = dd->size;
01577     
01578     weight = ALLOC(double,size);
01579     if (weight == NULL) {
01580         dd->errorCode = CUDD_MEMORY_OUT;
01581         return(NULL);
01582     }
01583     for (i = 0; i < size; i++) {
01584         weight[i] = 0.0;
01585     }
01586     for (i = 0; i < mvars; i++) {
01587         cof = Cudd_Cofactor(dd, f, maskVars[i]);
01588         cuddRef(cof);
01589         weight[i] = Cudd_CountMinterm(dd, cof, nvars);
01590         Cudd_RecursiveDeref(dd,cof);
01591 
01592         cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
01593         cuddRef(cof);
01594         weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
01595         Cudd_RecursiveDeref(dd,cof);
01596     }
01597 
01598     string = ALLOC(char, size + 1);
01599     if (string == NULL) {
01600         dd->errorCode = CUDD_MEMORY_OUT;
01601         return(NULL);
01602     }
01603     mask = ALLOC(int, size);
01604     if (mask == NULL) {
01605         dd->errorCode = CUDD_MEMORY_OUT;
01606         FREE(string);
01607         return(NULL);
01608     }
01609     for (i = 0; i < size; i++) {
01610         string[i] = '2';
01611         mask[i] = 0;
01612     }
01613     string[size] = '\0';
01614     indices = ALLOC(int,nvars);
01615     if (indices == NULL) {
01616         dd->errorCode = CUDD_MEMORY_OUT;
01617         FREE(string);
01618         FREE(mask);
01619         return(NULL);
01620     }
01621     for (i = 0; i < nvars; i++) {
01622         indices[i] = vars[i]->index;
01623     }
01624 
01625     result = ddPickRepresentativeCube(dd,f,nvars,weight,string);
01626     if (result == 0) {
01627         FREE(string);
01628         FREE(mask);
01629         FREE(indices);
01630         return(NULL);
01631     }
01632 
01633     cube = Cudd_ReadOne(dd);
01634     cuddRef(cube);
01635     zero = Cudd_Not(Cudd_ReadOne(dd));
01636     for (i = 0; i < nvars; i++) {
01637         if (string[indices[i]] == '0') {
01638             newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
01639         } else if (string[indices[i]] == '1') {
01640             newCube = Cudd_bddIte(dd,cube,vars[i],zero);
01641         } else
01642             continue;
01643         if (newCube == NULL) {
01644             FREE(string);
01645             FREE(mask);
01646             FREE(indices);
01647             Cudd_RecursiveDeref(dd,cube);
01648             return(NULL);
01649         }
01650         cuddRef(newCube);
01651         Cudd_RecursiveDeref(dd,cube);
01652         cube = newCube;
01653     }
01654     Cudd_RecursiveDeref(dd,cube);
01655 
01656     for (i = 0; i < mvars; i++) {
01657         mask[maskVars[i]->index] = 1;
01658     }
01659     for (i = 0; i < nvars; i++) {
01660         if (mask[indices[i]]) {
01661             if (string[indices[i]] == '2') {
01662                 if (weight[indices[i]] >= 0.0)
01663                     string[indices[i]] = '1';
01664                 else
01665                     string[indices[i]] = '0';
01666             }
01667         } else {
01668             string[indices[i]] = '2';
01669         }
01670     }
01671 
01672     cube = Cudd_ReadOne(dd);
01673     cuddRef(cube);
01674     zero = Cudd_Not(Cudd_ReadOne(dd));
01675 
01676     /* Build result BDD. */
01677     for (i = 0; i < nvars; i++) {
01678         if (string[indices[i]] == '0') {
01679             newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
01680         } else if (string[indices[i]] == '1') {
01681             newCube = Cudd_bddIte(dd,cube,vars[i],zero);
01682         } else
01683             continue;
01684         if (newCube == NULL) {
01685             FREE(string);
01686             FREE(mask);
01687             FREE(indices);
01688             Cudd_RecursiveDeref(dd,cube);
01689             return(NULL);
01690         }
01691         cuddRef(newCube);
01692         Cudd_RecursiveDeref(dd,cube);
01693         cube = newCube;
01694     }
01695 
01696     subset = Cudd_bddAnd(dd,f,cube);
01697     cuddRef(subset);
01698     Cudd_RecursiveDeref(dd,cube);
01699 
01700     /* Test. */
01701     if (Cudd_bddLeq(dd,subset,f)) {
01702         cuddDeref(subset);
01703     } else {
01704         Cudd_RecursiveDeref(dd,subset);
01705         subset = NULL;
01706     }
01707 
01708     FREE(string);
01709     FREE(mask);
01710     FREE(indices);
01711     FREE(weight);
01712     return(subset);
01713 
01714 } /* end of Cudd_SubsetWithMaskVars */

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

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

Synopsis [Finds the variables on which a DD depends.]

Description [Finds the variables on which a DD depends. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 699 of file cuddUtil.c.

00702 {
00703     int *support;
00704     DdNode *res, *tmp, *var;
00705     int i,j;
00706     int size;
00707 
00708     /* Allocate and initialize support array for ddSupportStep. */
00709     size = ddMax(dd->size, dd->sizeZ);
00710     support = ALLOC(int,size);
00711     if (support == NULL) {
00712         dd->errorCode = CUDD_MEMORY_OUT;
00713         return(NULL);
00714     }
00715     for (i = 0; i < size; i++) {
00716         support[i] = 0;
00717     }
00718 
00719     /* Compute support and clean up markers. */
00720     ddSupportStep(Cudd_Regular(f),support);
00721     ddClearFlag(Cudd_Regular(f));
00722 
00723     /* Transform support from array to cube. */
00724     do {
00725         dd->reordered = 0;
00726         res = DD_ONE(dd);
00727         cuddRef(res);
00728         for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
00729             i = (j >= dd->size) ? j : dd->invperm[j];
00730             if (support[i] == 1) {
00731                 var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
00732                 cuddRef(var);
00733                 tmp = cuddBddAndRecur(dd,res,var);
00734                 if (tmp == NULL) {
00735                     Cudd_RecursiveDeref(dd,res);
00736                     Cudd_RecursiveDeref(dd,var);
00737                     res = NULL;
00738                     break;
00739                 }
00740                 cuddRef(tmp);
00741                 Cudd_RecursiveDeref(dd,res);
00742                 Cudd_RecursiveDeref(dd,var);
00743                 res = tmp;
00744             }
00745         }
00746     } while (dd->reordered == 1);
00747 
00748     FREE(support);
00749     if (res != NULL) cuddDeref(res);
00750     return(res);
00751 
00752 } /* end of Cudd_Support */

int* Cudd_SupportIndex	(	DdManager *	dd,
		DdNode *	f
	)

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

Synopsis [Finds the variables on which a DD depends.]

Description [Finds the variables on which a DD depends. Returns an index array of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 768 of file cuddUtil.c.

00771 {
00772     int *support;
00773     int i;
00774     int size;
00775 
00776     /* Allocate and initialize support array for ddSupportStep. */
00777     size = ddMax(dd->size, dd->sizeZ);
00778     support = ALLOC(int,size);
00779     if (support == NULL) {
00780         dd->errorCode = CUDD_MEMORY_OUT;
00781         return(NULL);
00782     }
00783     for (i = 0; i < size; i++) {
00784         support[i] = 0;
00785     }
00786 
00787     /* Compute support and clean up markers. */
00788     ddSupportStep(Cudd_Regular(f),support);
00789     ddClearFlag(Cudd_Regular(f));
00790 
00791     return(support);
00792 
00793 } /* end of Cudd_SupportIndex */

int Cudd_SupportSize	(	DdManager *	dd,
		DdNode *	f
	)

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

Synopsis [Counts the variables on which a DD depends.]

Description [Counts the variables on which a DD depends. Returns the number of the variables if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support]

Definition at line 810 of file cuddUtil.c.

00813 {
00814     int *support;
00815     int i;
00816     int size;
00817     int count;
00818 
00819     /* Allocate and initialize support array for ddSupportStep. */
00820     size = ddMax(dd->size, dd->sizeZ);
00821     support = ALLOC(int,size);
00822     if (support == NULL) {
00823         dd->errorCode = CUDD_MEMORY_OUT;
00824         return(CUDD_OUT_OF_MEM);
00825     }
00826     for (i = 0; i < size; i++) {
00827         support[i] = 0;
00828     }
00829 
00830     /* Compute support and clean up markers. */
00831     ddSupportStep(Cudd_Regular(f),support);
00832     ddClearFlag(Cudd_Regular(f));
00833 
00834     /* Count support variables. */
00835     count = 0;
00836     for (i = 0; i < size; i++) {
00837         if (support[i] == 1) count++;
00838     }
00839 
00840     FREE(support);
00841     return(count);
00842 
00843 } /* end of Cudd_SupportSize */

DdNode* Cudd_VectorSupport	(	DdManager *	dd,
		DdNode **	F,
		int	n
	)

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

Synopsis [Finds the variables on which a set of DDs depends.]

Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support Cudd_ClassifySupport]

Definition at line 861 of file cuddUtil.c.

00865 {
00866     int *support;
00867     DdNode *res, *tmp, *var;
00868     int i,j;
00869     int size;
00870 
00871     /* Allocate and initialize support array for ddSupportStep. */
00872     size = ddMax(dd->size, dd->sizeZ);
00873     support = ALLOC(int,size);
00874     if (support == NULL) {
00875         dd->errorCode = CUDD_MEMORY_OUT;
00876         return(NULL);
00877     }
00878     for (i = 0; i < size; i++) {
00879         support[i] = 0;
00880     }
00881 
00882     /* Compute support and clean up markers. */
00883     for (i = 0; i < n; i++) {
00884         ddSupportStep(Cudd_Regular(F[i]),support);
00885     }
00886     for (i = 0; i < n; i++) {
00887         ddClearFlag(Cudd_Regular(F[i]));
00888     }
00889 
00890     /* Transform support from array to cube. */
00891     res = DD_ONE(dd);
00892     cuddRef(res);
00893     for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */
00894         i = (j >= dd->size) ? j : dd->invperm[j];
00895         if (support[i] == 1) {
00896             var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
00897             cuddRef(var);
00898             tmp = Cudd_bddAnd(dd,res,var);
00899             if (tmp == NULL) {
00900                 Cudd_RecursiveDeref(dd,res);
00901                 Cudd_RecursiveDeref(dd,var);
00902                 FREE(support);
00903                 return(NULL);
00904             }
00905             cuddRef(tmp);
00906             Cudd_RecursiveDeref(dd,res);
00907             Cudd_RecursiveDeref(dd,var);
00908             res = tmp;
00909         }
00910     }
00911 
00912     FREE(support);
00913     cuddDeref(res);
00914     return(res);
00915 
00916 } /* end of Cudd_VectorSupport */

int* Cudd_VectorSupportIndex	(	DdManager *	dd,
		DdNode **	F,
		int	n
	)

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

Synopsis [Finds the variables on which a set of DDs depends.]

Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns an index array of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 933 of file cuddUtil.c.

00937 {
00938     int *support;
00939     int i;
00940     int size;
00941 
00942     /* Allocate and initialize support array for ddSupportStep. */
00943     size = ddMax(dd->size, dd->sizeZ);
00944     support = ALLOC(int,size);
00945     if (support == NULL) {
00946         dd->errorCode = CUDD_MEMORY_OUT;
00947         return(NULL);
00948     }
00949     for (i = 0; i < size; i++) {
00950         support[i] = 0;
00951     }
00952 
00953     /* Compute support and clean up markers. */
00954     for (i = 0; i < n; i++) {
00955         ddSupportStep(Cudd_Regular(F[i]),support);
00956     }
00957     for (i = 0; i < n; i++) {
00958         ddClearFlag(Cudd_Regular(F[i]));
00959     }
00960 
00961     return(support);
00962 
00963 } /* end of Cudd_VectorSupportIndex */

int Cudd_VectorSupportSize	(	DdManager *	dd,
		DdNode **	F,
		int	n
	)

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

Synopsis [Counts the variables on which a set of DDs depends.]

Description [Counts the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns the number of the variables if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso [Cudd_VectorSupport Cudd_SupportSize]

Definition at line 981 of file cuddUtil.c.

00985 {
00986     int *support;
00987     int i;
00988     int size;
00989     int count;
00990 
00991     /* Allocate and initialize support array for ddSupportStep. */
00992     size = ddMax(dd->size, dd->sizeZ);
00993     support = ALLOC(int,size);
00994     if (support == NULL) {
00995         dd->errorCode = CUDD_MEMORY_OUT;
00996         return(CUDD_OUT_OF_MEM);
00997     }
00998     for (i = 0; i < size; i++) {
00999         support[i] = 0;
01000     }
01001 
01002     /* Compute support and clean up markers. */
01003     for (i = 0; i < n; i++) {
01004         ddSupportStep(Cudd_Regular(F[i]),support);
01005     }
01006     for (i = 0; i < n; i++) {
01007         ddClearFlag(Cudd_Regular(F[i]));
01008     }
01009 
01010     /* Count vriables in support. */
01011     count = 0;
01012     for (i = 0; i < size; i++) {
01013         if (support[i] == 1) count++;
01014     }
01015 
01016     FREE(support);
01017     return(count);
01018 
01019 } /* end of Cudd_VectorSupportSize */

int cuddCollectNodes	(	DdNode *	f,
		st_table *	visited
	)

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

Synopsis [Recursively collects all the nodes of a DD in a symbol table.]

Description [Traverses the BDD f and collects all its nodes in a symbol table. f is assumed to be a regular pointer and cuddCollectNodes guarantees this assumption in the recursive calls. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 2703 of file cuddUtil.c.

02706 {
02707     DdNode      *T, *E;
02708     int         retval;
02709 
02710 #ifdef DD_DEBUG
02711     assert(!Cudd_IsComplement(f));
02712 #endif
02713 
02714     /* If already visited, nothing to do. */
02715     if (st_is_member(visited, (char *) f) == 1)
02716         return(1);
02717 
02718     /* Check for abnormal condition that should never happen. */
02719     if (f == NULL)
02720         return(0);
02721 
02722     /* Mark node as visited. */
02723     if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
02724         return(0);
02725 
02726     /* Check terminal case. */
02727     if (cuddIsConstant(f))
02728         return(1);
02729 
02730     /* Recursive calls. */
02731     T = cuddT(f);
02732     retval = cuddCollectNodes(T,visited);
02733     if (retval != 1) return(retval);
02734     E = Cudd_Regular(cuddE(f));
02735     retval = cuddCollectNodes(E,visited);
02736     return(retval);
02737 
02738 } /* end of cuddCollectNodes */

static int cuddEstimateCofactor	(	DdManager *	dd,
		st_table *	table,
		DdNode *	node,
		int	i,
		int	phase,
		DdNode **	ptr
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_CofactorEstimate.]

Description [Performs the recursive step of Cudd_CofactorEstimate. Returns an estimate of the number of nodes in the DD of a cofactor of node. Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.]

SideEffects [None]

SeeAlso []

Definition at line 2939 of file cuddUtil.c.

02946 {
02947     int tval, eval, val;
02948     DdNode *ptrT, *ptrE;
02949 
02950     if (Cudd_IsComplement(node->next)) {
02951         if (!st_lookup(table,(char *)node,(char **)ptr)) {
02952             st_add_direct(table,(char *)node,(char *)node);
02953             *ptr = node;
02954         }
02955         return(0);
02956     }
02957     node->next = Cudd_Not(node->next);
02958     if (cuddIsConstant(node)) {
02959         *ptr = node;
02960         if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM)
02961             return(CUDD_OUT_OF_MEM);
02962         return(1);
02963     }
02964     if ((int) node->index == i) {
02965         if (phase == 1) {
02966             *ptr = cuddT(node);
02967             val = ddDagInt(cuddT(node));
02968         } else {
02969             *ptr = cuddE(node);
02970             val = ddDagInt(Cudd_Regular(cuddE(node)));
02971         }
02972         if (node->ref > 1) {
02973             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
02974                 ST_OUT_OF_MEM)
02975                 return(CUDD_OUT_OF_MEM);
02976         }
02977         return(val);
02978     }
02979     if (dd->perm[node->index] > dd->perm[i]) {
02980         *ptr = node;
02981         tval = ddDagInt(cuddT(node));
02982         eval = ddDagInt(Cudd_Regular(cuddE(node)));
02983         if (node->ref > 1) {
02984             if (st_add_direct(table,(char *)node,(char *)node) ==
02985                 ST_OUT_OF_MEM)
02986                 return(CUDD_OUT_OF_MEM);
02987         }
02988         val = 1 + tval + eval;
02989         return(val);
02990     }
02991     tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT);
02992     eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i,
02993                                 phase,&ptrE);
02994     ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node)));
02995     if (ptrT == ptrE) {         /* recombination */
02996         *ptr = ptrT;
02997         val = tval;
02998         if (node->ref > 1) {
02999             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
03000                     ST_OUT_OF_MEM)
03001                 return(CUDD_OUT_OF_MEM);
03002         }
03003     } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) &&
03004                (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) {
03005         if (Cudd_IsComplement((*ptr)->next)) {
03006             val = 0;
03007         } else {
03008             val = 1 + tval + eval;
03009         }
03010         if (node->ref > 1) {
03011             if (st_add_direct(table,(char *)node,(char *)*ptr) ==
03012                     ST_OUT_OF_MEM)
03013                 return(CUDD_OUT_OF_MEM);
03014         }
03015     } else {
03016         *ptr = node;
03017         val = 1 + tval + eval;
03018     }
03019     return(val);
03020 
03021 } /* end of cuddEstimateCofactor */

static int cuddEstimateCofactorSimple	(	DdNode *	node,
		int	i
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_CofactorEstimateSimple.]

Description [Performs the recursive step of Cudd_CofactorEstimateSimple. Returns an estimate of the number of nodes in the DD of the positive cofactor of node. Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.]

SideEffects [None]

SeeAlso []

Definition at line 3096 of file cuddUtil.c.

03099 {
03100     int tval, eval;
03101 
03102     if (Cudd_IsComplement(node->next)) {
03103         return(0);
03104     }
03105     node->next = Cudd_Not(node->next);
03106     if (cuddIsConstant(node)) {
03107         return(1);
03108     }
03109     tval = cuddEstimateCofactorSimple(cuddT(node),i);
03110     if ((int) node->index == i) return(tval);
03111     eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i);
03112     return(1 + tval + eval);
03113 
03114 } /* end of cuddEstimateCofactorSimple */

int cuddP	(	DdManager *	dd,
		DdNode *	f
	)

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

Synopsis [Prints a DD to the standard output. One line per node is printed.]

Description [Prints a DD to the standard output. One line per node is printed. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [Cudd_PrintDebug]

Definition at line 2644 of file cuddUtil.c.

02647 {
02648     int retval;
02649     st_table *table = st_init_table(st_ptrcmp,st_ptrhash);
02650 
02651     if (table == NULL) return(0);
02652 
02653     retval = dp2(dd,f,table);
02654     st_free_table(table);
02655     (void) fputc('\n',dd->out);
02656     return(retval);
02657 
02658 } /* end of cuddP */

enum st_retval cuddStCountfree	(	char *	key,
		char *	value,
		char *	arg
	)

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

Synopsis [Frees the memory used to store the minterm counts recorded in the visited table.]

Description [Frees the memory used to store the minterm counts recorded in the visited table. Returns ST_CONTINUE.]

SideEffects [None]

Definition at line 2673 of file cuddUtil.c.

02677 {
02678     double      *d;
02679 
02680     d = (double *)value;
02681     FREE(d);
02682     return(ST_CONTINUE);
02683 
02684 } /* end of cuddStCountfree */

static DdNode* cuddUniqueLookup	(	DdManager *	unique,
		int	index,
		DdNode *	T,
		DdNode *	E
	)			`[static]`

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

Synopsis [Checks the unique table for the existence of an internal node.]

Description [Checks the unique table for the existence of an internal node. Returns a pointer to the node if it is in the table; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddUniqueInter]

Definition at line 3037 of file cuddUtil.c.

03042 {
03043     int posn;
03044     unsigned int level;
03045     DdNodePtr *nodelist;
03046     DdNode *looking;
03047     DdSubtable *subtable;
03048 
03049     if (index >= unique->size) {
03050         return(NULL);
03051     }
03052 
03053     level = unique->perm[index];
03054     subtable = &(unique->subtables[level]);
03055 
03056 #ifdef DD_DEBUG
03057     assert(level < (unsigned) cuddI(unique,T->index));
03058     assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
03059 #endif
03060 
03061     posn = ddHash(T, E, subtable->shift);
03062     nodelist = subtable->nodelist;
03063     looking = nodelist[posn];
03064 
03065     while (T < cuddT(looking)) {
03066         looking = Cudd_Regular(looking->next);
03067     }
03068     while (T == cuddT(looking) && E < cuddE(looking)) {
03069         looking = Cudd_Regular(looking->next);
03070     }
03071     if (cuddT(looking) == T && cuddE(looking) == E) {
03072         return(looking);
03073     }
03074 
03075     return(NULL);
03076 
03077 } /* end of cuddUniqueLookup */

static void ddClearFlag ( DdNode * f ) [static]

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

Synopsis [Performs a DFS from f, clearing the LSB of the next pointers.]

Description []

SideEffects [None]

SeeAlso [ddSupportStep ddDagInt]

Definition at line 3434 of file cuddUtil.c.

03436 {
03437     if (!Cudd_IsComplement(f->next)) {
03438         return;
03439     }
03440     /* Clear visited flag. */
03441     f->next = Cudd_Regular(f->next);
03442     if (cuddIsConstant(f)) {
03443         return;
03444     }
03445     ddClearFlag(cuddT(f));
03446     ddClearFlag(Cudd_Regular(cuddE(f)));
03447     return;
03448 
03449 } /* end of ddClearFlag */

static double ddCountMintermAux	(	DdNode *	node,
		double	max,
		DdHashTable *	table
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_CountMinterm.]

Description [Performs the recursive step of Cudd_CountMinterm. It is based on the following identity. Let |f| be the number of minterms of f. Then: <xmp> |f| = (|f0|+|f1|)/2 </xmp> where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff. Returns the number of minterms of the function rooted at node.]

SideEffects [None]

Definition at line 3136 of file cuddUtil.c.

03140 {
03141     DdNode      *N, *Nt, *Ne;
03142     double      min, minT, minE;
03143     DdNode      *res;
03144 
03145     N = Cudd_Regular(node);
03146 
03147     if (cuddIsConstant(N)) {
03148         if (node == background || node == zero) {
03149             return(0.0);
03150         } else {
03151             return(max);
03152         }
03153     }
03154     if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
03155         min = cuddV(res);
03156         if (res->ref == 0) {
03157             table->manager->dead++;
03158             table->manager->constants.dead++;
03159         }
03160         return(min);
03161     }
03162 
03163     Nt = cuddT(N); Ne = cuddE(N);
03164     if (Cudd_IsComplement(node)) {
03165         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
03166     }
03167 
03168     minT = ddCountMintermAux(Nt,max,table);
03169     if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03170     minT *= 0.5;
03171     minE = ddCountMintermAux(Ne,max,table);
03172     if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03173     minE *= 0.5;
03174     min = minT + minE;
03175 
03176     if (N->ref != 1) {
03177         ptrint fanout = (ptrint) N->ref;
03178         cuddSatDec(fanout);
03179         res = cuddUniqueConst(table->manager,min);
03180         if (!cuddHashTableInsert1(table,node,res,fanout)) {
03181             cuddRef(res); Cudd_RecursiveDeref(table->manager, res);
03182             return((double)CUDD_OUT_OF_MEM);
03183         }
03184     }
03185 
03186     return(min);
03187 
03188 } /* end of ddCountMintermAux */

static double ddCountPathAux	(	DdNode *	node,
		st_table *	table
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_CountPath.]

Description [Performs the recursive step of Cudd_CountPath. It is based on the following identity. Let |f| be the number of paths of f. Then: <xmp> |f| = |f0|+|f1| </xmp> where f0 and f1 are the two cofactors of f. Uses the identity |f'| = |f|, to improve the utilization of the (local) cache. Returns the number of paths of the function rooted at node.]

SideEffects [None]

Definition at line 3209 of file cuddUtil.c.

03212 {
03213 
03214     DdNode      *Nv, *Nnv;
03215     double      paths, *ppaths, paths1, paths2;
03216     double      *dummy;
03217 
03218 
03219     if (cuddIsConstant(node)) {
03220         return(1.0);
03221     }
03222     if (st_lookup(table, (char *)node, (char **)&dummy)) {
03223         paths = *dummy;
03224         return(paths);
03225     }
03226 
03227     Nv = cuddT(node); Nnv = cuddE(node);
03228 
03229     paths1 = ddCountPathAux(Nv,table);
03230     if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03231     paths2 = ddCountPathAux(Cudd_Regular(Nnv),table);
03232     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03233     paths = paths1 + paths2;
03234     
03235     ppaths = ALLOC(double,1);
03236     if (ppaths == NULL) {
03237         return((double)CUDD_OUT_OF_MEM);
03238     }
03239 
03240     *ppaths = paths;
03241 
03242     if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
03243         FREE(ppaths);
03244         return((double)CUDD_OUT_OF_MEM);
03245     }
03246     return(paths);
03247 
03248 } /* end of ddCountPathAux */

static double ddCountPathsToNonZero	(	DdNode *	N,
		st_table *	table
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_CountPathsToNonZero.]

Description [Performs the recursive step of Cudd_CountPathsToNonZero. It is based on the following identity. Let |f| be the number of paths of f. Then: <xmp> |f| = |f0|+|f1| </xmp> where f0 and f1 are the two cofactors of f. Returns the number of paths of the function rooted at node.]

SideEffects [None]

Definition at line 3344 of file cuddUtil.c.

03347 {
03348 
03349     DdNode      *node, *Nt, *Ne;
03350     double      paths, *ppaths, paths1, paths2;
03351     double      *dummy;
03352 
03353     node = Cudd_Regular(N);
03354     if (cuddIsConstant(node)) {
03355         return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL));
03356     }
03357     if (st_lookup(table, (char *)N, (char **)&dummy)) {
03358         paths = *dummy;
03359         return(paths);
03360     }
03361 
03362     Nt = cuddT(node); Ne = cuddE(node);
03363     if (node != N) {
03364         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
03365     }
03366 
03367     paths1 = ddCountPathsToNonZero(Nt,table);
03368     if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03369     paths2 = ddCountPathsToNonZero(Ne,table);
03370     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
03371     paths = paths1 + paths2;
03372 
03373     ppaths = ALLOC(double,1);
03374     if (ppaths == NULL) {
03375         return((double)CUDD_OUT_OF_MEM);
03376     }
03377 
03378     *ppaths = paths;
03379 
03380     if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
03381         FREE(ppaths);
03382         return((double)CUDD_OUT_OF_MEM);
03383     }
03384     return(paths);
03385 
03386 } /* end of ddCountPathsToNonZero */

static int ddDagInt ( DdNode * n ) [static]

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

Synopsis [Performs the recursive step of Cudd_DagSize.]

Description [Performs the recursive step of Cudd_DagSize. Returns the number of nodes in the graph rooted at n.]

SideEffects [None]

Definition at line 2904 of file cuddUtil.c.

02906 {
02907     int tval, eval;
02908 
02909     if (Cudd_IsComplement(n->next)) {
02910         return(0);
02911     }
02912     n->next = Cudd_Not(n->next);
02913     if (cuddIsConstant(n)) {
02914         return(1);
02915     }
02916     tval = ddDagInt(cuddT(n));
02917     eval = ddDagInt(Cudd_Regular(cuddE(n)));
02918     return(1 + tval + eval);
02919 
02920 } /* end of ddDagInt */

static int ddEpdCountMintermAux	(	DdNode *	node,
		EpDouble *	max,
		EpDouble *	epd,
		st_table *	table
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_CountMinterm.]

Description [Performs the recursive step of Cudd_CountMinterm. It is based on the following identity. Let |f| be the number of minterms of f. Then: <xmp> |f| = (|f0|+|f1|)/2 </xmp> where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff. Returns the number of minterms of the function rooted at node.]

SideEffects [None]

Definition at line 3270 of file cuddUtil.c.

03275 {
03276     DdNode      *Nt, *Ne;
03277     EpDouble    *min, minT, minE;
03278     EpDouble    *res;
03279     int         status;
03280 
03281     if (cuddIsConstant(node)) {
03282         if (node == background || node == zero) {
03283             EpdMakeZero(epd, 0);
03284         } else {
03285             EpdCopy(max, epd);
03286         }
03287         return(0);
03288     }
03289     if (node->ref != 1 && st_lookup(table, (char *)node, (char **)&res)) {
03290         EpdCopy(res, epd);
03291         return(0);
03292     }
03293 
03294     Nt = cuddT(node); Ne = cuddE(node);
03295     if (Cudd_IsComplement(node)) {
03296         Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne);
03297     }
03298 
03299     status = ddEpdCountMintermAux(Nt,max,&minT,table);
03300     if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
03301     EpdMultiply(&minT, (double)0.5);
03302     status = ddEpdCountMintermAux(Ne,max,&minE,table);
03303     if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
03304     if (Cudd_IsComplement(Ne)) {
03305         EpdSubtract3(max, &minE, epd);
03306         EpdCopy(epd, &minE);
03307     }
03308     EpdMultiply(&minE, (double)0.5);
03309     EpdAdd3(&minT, &minE, epd);
03310 
03311     if (node->ref > 1) {
03312         min = EpdAlloc();
03313         if (!min)
03314             return(CUDD_OUT_OF_MEM);
03315         EpdCopy(epd, min);
03316         if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) {
03317             EpdFree(min);
03318             return(CUDD_OUT_OF_MEM);
03319         }
03320     }
03321 
03322     return(0);
03323 
03324 } /* end of ddEpdCountMintermAux */

static enum st_retval ddEpdFree	(	char *	key,
		char *	value,
		char *	arg
	)			`[static]`

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

Synopsis [Frees the memory used to store the minterm counts recorded in the visited table.]

Description [Frees the memory used to store the minterm counts recorded in the visited table. Returns ST_CONTINUE.]

SideEffects [None]

Definition at line 3622 of file cuddUtil.c.

03626 {
03627     EpDouble    *epd;
03628 
03629     epd = (EpDouble *) value;
03630     EpdFree(epd);
03631     return(ST_CONTINUE);
03632 
03633 } /* end of ddEpdFree */

static int ddLeavesInt ( DdNode * n ) [static]

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

Synopsis [Performs the recursive step of Cudd_CountLeaves.]

Description [Performs the recursive step of Cudd_CountLeaves. Returns the number of leaves in the DD rooted at n.]

SideEffects [None]

SeeAlso [Cudd_CountLeaves]

Definition at line 3465 of file cuddUtil.c.

03467 {
03468     int tval, eval;
03469 
03470     if (Cudd_IsComplement(n->next)) {
03471         return(0);
03472     }
03473     n->next = Cudd_Not(n->next);
03474     if (cuddIsConstant(n)) {
03475         return(1);
03476     }
03477     tval = ddLeavesInt(cuddT(n));
03478     eval = ddLeavesInt(Cudd_Regular(cuddE(n)));
03479     return(tval + eval);
03480 
03481 } /* end of ddLeavesInt */

static int ddPickArbitraryMinterms	(	DdManager *	dd,
		DdNode *	node,
		int	nvars,
		int	nminterms,
		char **	string
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]

Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms. Returns 1 if successful; 0 otherwise.]

SideEffects [none]

SeeAlso [Cudd_bddPickArbitraryMinterms]

Definition at line 3497 of file cuddUtil.c.

03503 {
03504     DdNode *N, *T, *E;
03505     DdNode *one, *bzero;
03506     int    i, t, result;
03507     double min1, min2;
03508 
03509     if (string == NULL || node == NULL) return(0);
03510 
03511     /* The constant 0 function has no on-set cubes. */
03512     one = DD_ONE(dd);
03513     bzero = Cudd_Not(one);
03514     if (nminterms == 0 || node == bzero) return(1);
03515     if (node == one) {
03516         return(1);
03517     }
03518 
03519     N = Cudd_Regular(node);
03520     T = cuddT(N); E = cuddE(N);
03521     if (Cudd_IsComplement(node)) {
03522         T = Cudd_Not(T); E = Cudd_Not(E);
03523     }
03524 
03525     min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0;
03526     if (min1 == (double)CUDD_OUT_OF_MEM) return(0);
03527     min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0;
03528     if (min2 == (double)CUDD_OUT_OF_MEM) return(0);
03529 
03530     t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5);
03531     for (i = 0; i < t; i++)
03532         string[i][N->index] = '1';
03533     for (i = t; i < nminterms; i++)
03534         string[i][N->index] = '0';
03535 
03536     result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]);
03537     if (result == 0)
03538         return(0);
03539     result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]);
03540     return(result);
03541 
03542 } /* end of ddPickArbitraryMinterms */

static int ddPickRepresentativeCube	(	DdManager *	dd,
		DdNode *	node,
		int	nvars,
		double *	weight,
		char *	string
	)			`[static]`

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

Synopsis [Finds a representative cube of a BDD.]

Description [Finds a representative cube of a BDD with the weight of each variable. From the top variable, if the weight is greater than or equal to 0.0, choose THEN branch unless the child is the constant 0. Otherwise, choose ELSE branch unless the child is the constant 0.]

SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube]

Definition at line 3558 of file cuddUtil.c.

03564 {
03565     DdNode *N, *T, *E;
03566     DdNode *one, *bzero;
03567 
03568     if (string == NULL || node == NULL) return(0);
03569 
03570     /* The constant 0 function has no on-set cubes. */
03571     one = DD_ONE(dd);
03572     bzero = Cudd_Not(one);
03573     if (node == bzero) return(0);
03574 
03575     if (node == DD_ONE(dd)) return(1);
03576 
03577     for (;;) {
03578         N = Cudd_Regular(node);
03579         if (N == one)
03580             break;
03581         T = cuddT(N);
03582         E = cuddE(N);
03583         if (Cudd_IsComplement(node)) {
03584             T = Cudd_Not(T);
03585             E = Cudd_Not(E);
03586         }
03587         if (weight[N->index] >= 0.0) {
03588             if (T == bzero) {
03589                 node = E;
03590                 string[N->index] = '0';
03591             } else {
03592                 node = T;
03593                 string[N->index] = '1';
03594             }
03595         } else {
03596             if (E == bzero) {
03597                 node = T;
03598                 string[N->index] = '1';
03599             } else {
03600                 node = E;
03601                 string[N->index] = '0';
03602             }
03603         }
03604     }
03605     return(1);
03606 
03607 } /* end of ddPickRepresentativeCube */

static void ddPrintMintermAux	(	DdManager *	dd,
		DdNode *	node,
		int *	list
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_PrintMinterm.]

Description []

SideEffects [None]

Definition at line 2850 of file cuddUtil.c.

02854 {
02855     DdNode      *N,*Nv,*Nnv;
02856     int         i,v,index;
02857 
02858     N = Cudd_Regular(node);
02859 
02860     if (cuddIsConstant(N)) {
02861         /* Terminal case: Print one cube based on the current recursion
02862         ** path, unless we have reached the background value (ADDs) or
02863         ** the logical zero (BDDs).
02864         */
02865         if (node != background && node != zero) {
02866             for (i = 0; i < dd->size; i++) {
02867                 v = list[i];
02868                 if (v == 0) (void) fprintf(dd->out,"0");
02869                 else if (v == 1) (void) fprintf(dd->out,"1");
02870                 else (void) fprintf(dd->out,"-");
02871             }
02872             (void) fprintf(dd->out," % g\n", cuddV(node));
02873         }
02874     } else {
02875         Nv  = cuddT(N);
02876         Nnv = cuddE(N);
02877         if (Cudd_IsComplement(node)) {
02878             Nv  = Cudd_Not(Nv);
02879             Nnv = Cudd_Not(Nnv);
02880         }
02881         index = N->index;
02882         list[index] = 0;
02883         ddPrintMintermAux(dd,Nnv,list); 
02884         list[index] = 1;
02885         ddPrintMintermAux(dd,Nv,list);
02886         list[index] = 2;
02887     }
02888     return;
02889 
02890 } /* end of ddPrintMintermAux */

static void ddSupportStep	(	DdNode *	f,
		int *	support
	)			`[static]`

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

Synopsis [Performs the recursive step of Cudd_Support.]

Description [Performs the recursive step of Cudd_Support. Performs a DFS from f. The support is accumulated in supp as a side effect. Uses the LSB of the then pointer as visited flag.]

SideEffects [None]

SeeAlso [ddClearFlag]

Definition at line 3403 of file cuddUtil.c.

03406 {
03407     if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) {
03408         return;
03409     }
03410 
03411     support[f->index] = 1;
03412     ddSupportStep(cuddT(f),support);
03413     ddSupportStep(Cudd_Regular(cuddE(f)),support);
03414     /* Mark as visited. */
03415     f->next = Cudd_Not(f->next);
03416     return;
03417 
03418 } /* end of ddSupportStep */

static int dp2	(	DdManager *	dd,
		DdNode *	f,
		st_table *	t
	)			`[static]`

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

Synopsis [Performs the recursive step of cuddP.]

Description [Performs the recursive step of cuddP. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 2757 of file cuddUtil.c.

02761 {
02762     DdNode *g, *n, *N;
02763     int T,E;
02764     
02765     if (f == NULL) {
02766         return(0);
02767     }
02768     g = Cudd_Regular(f);
02769     if (cuddIsConstant(g)) {
02770 #if SIZEOF_VOID_P == 8
02771         (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f),
02772                 (unsigned long) g / (unsigned long) sizeof(DdNode),cuddV(g));
02773 #else
02774         (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f),
02775                 (unsigned) g / (unsigned) sizeof(DdNode),cuddV(g));
02776 #endif
02777         return(1);
02778     }
02779     if (st_is_member(t,(char *) g) == 1) {
02780         return(1);
02781     }
02782     if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM)
02783         return(0);
02784 #ifdef DD_STATS
02785 #if SIZEOF_VOID_P == 8
02786     (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f),
02787                 (unsigned long) g / (unsigned long) sizeof(DdNode), g->index, g->ref);
02788 #else
02789     (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f),
02790                 (unsigned) g / (unsigned) sizeof(DdNode),g->index,g->ref);
02791 #endif
02792 #else
02793 #if SIZEOF_VOID_P == 8
02794     (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\t", bang(f),
02795                 (unsigned long) g / (unsigned long) sizeof(DdNode),g->index);
02796 #else
02797     (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\t", bang(f),
02798                 (unsigned) g / (unsigned) sizeof(DdNode),g->index);
02799 #endif
02800 #endif
02801     n = cuddT(g);
02802     if (cuddIsConstant(n)) {
02803         (void) fprintf(dd->out,"T = %-9g\t",cuddV(n));
02804         T = 1;
02805     } else {
02806 #if SIZEOF_VOID_P == 8
02807         (void) fprintf(dd->out,"T = 0x%lx\t",(unsigned long) n / (unsigned long) sizeof(DdNode));
02808 #else
02809         (void) fprintf(dd->out,"T = 0x%x\t",(unsigned) n / (unsigned) sizeof(DdNode));
02810 #endif
02811         T = 0;
02812     }
02813 
02814     n = cuddE(g);
02815     N = Cudd_Regular(n);
02816     if (cuddIsConstant(N)) {
02817         (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N));
02818         E = 1;
02819     } else {
02820 #if SIZEOF_VOID_P == 8
02821         (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (unsigned long) N/(unsigned long) sizeof(DdNode));
02822 #else
02823         (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (unsigned) N/(unsigned) sizeof(DdNode));
02824 #endif
02825         E = 0;
02826     }
02827     if (E == 0) {
02828         if (dp2(dd,N,t) == 0)
02829             return(0);
02830     }
02831     if (T == 0) {
02832         if (dp2(dd,cuddT(g),t) == 0)
02833             return(0);
02834     }
02835     return(1);
02836 
02837 } /* end of dp2 */

Variable Documentation

DdNode* background [static]

Definition at line 115 of file cuddUtil.c.

long cuddRand = 0 [static]

Definition at line 117 of file cuddUtil.c.

long cuddRand2 [static]

Definition at line 118 of file cuddUtil.c.

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

Definition at line 112 of file cuddUtil.c.

long shuffleSelect [static]

Definition at line 119 of file cuddUtil.c.

long shuffleTable[STAB_SIZE] [static]

Definition at line 120 of file cuddUtil.c.

DdNode * zero [static]

Definition at line 115 of file cuddUtil.c.

src/bdd/cudd/cuddUtil.c File Reference

Defines

Functions

Variables

Define Documentation

Function Documentation

Variable Documentation