src/bdd/cudd/cuddDecomp.c File Reference

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

Go to the source code of this file.

Data Structures

struct  Conjuncts
struct  NodeStat

Defines

#define DEPTH   5
#define THRESHOLD   10
#define NONE   0
#define PAIR_ST   1
#define PAIR_CR   2
#define G_ST   3
#define G_CR   4
#define H_ST   5
#define H_CR   6
#define BOTH_G   7
#define BOTH_H   8
#define FactorsNotStored(factors)   ((int)((long)(factors) & 01))
#define FactorsComplement(factors)   ((Conjuncts *)((long)(factors) | 01))
#define FactorsUncomplement(factors)   ((Conjuncts *)((long)(factors) ^ 01))

Functions

static NodeStat *CreateBotDist ARGS ((DdNode *node, st_table *distanceTable))
static double CountMinterms ARGS ((DdNode *node, double max, st_table *mintermTable, FILE *fp))
static void ConjunctsFree ARGS ((DdManager *dd, Conjuncts *factors))
static int PairInTables ARGS ((DdNode *g, DdNode *h, st_table *ghTable))
static Conjuncts
*CheckTablesCacheAndReturn 		ARGS ((DdNode *node, DdNode *g, DdNode *h, st_table *ghTable, st_table *cacheTable))
static Conjuncts *PickOnePair ARGS ((DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable))
static Conjuncts *CheckInTables ARGS ((DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable, int *outOfMem))
static Conjuncts *ZeroCase ARGS ((DdManager *dd, DdNode *node, Conjuncts *factorsNv, st_table *ghTable, st_table *cacheTable, int switched))
static Conjuncts *BuildConjuncts ARGS ((DdManager *dd, DdNode *node, st_table *distanceTable, st_table *cacheTable, int approxDistance, int maxLocalRef, st_table *ghTable, st_table *mintermTable))
static int cuddConjunctsAux ARGS ((DdManager *dd, DdNode *f, DdNode **c1, DdNode **c2))
int Cudd_bddApproxConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts)
int Cudd_bddApproxDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts)
int Cudd_bddIterConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts)
int Cudd_bddIterDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts)
int Cudd_bddGenConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts)
int Cudd_bddGenDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts)
int Cudd_bddVarConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts)
int Cudd_bddVarDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts)
static NodeStat * CreateBotDist (DdNode *node, st_table *distanceTable)
static double CountMinterms (DdNode *node, double max, st_table *mintermTable, FILE *fp)
static void ConjunctsFree (DdManager *dd, Conjuncts *factors)
static int PairInTables (DdNode *g, DdNode *h, st_table *ghTable)
static Conjuncts * CheckTablesCacheAndReturn (DdNode *node, DdNode *g, DdNode *h, st_table *ghTable, st_table *cacheTable)
static Conjuncts * PickOnePair (DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable)
static Conjuncts * CheckInTables (DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable, int *outOfMem)
static Conjuncts * ZeroCase (DdManager *dd, DdNode *node, Conjuncts *factorsNv, st_table *ghTable, st_table *cacheTable, int switched)
static Conjuncts * BuildConjuncts (DdManager *dd, DdNode *node, st_table *distanceTable, st_table *cacheTable, int approxDistance, int maxLocalRef, st_table *ghTable, st_table *mintermTable)
static int cuddConjunctsAux (DdManager *dd, DdNode *f, DdNode **c1, DdNode **c2)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"
static DdNode * one
static DdNode * zero
long lastTimeG

Define Documentation

#define BOTH_G   7

Definition at line 52 of file cuddDecomp.c.

#define BOTH_H   8

Definition at line 53 of file cuddDecomp.c.

#define DEPTH   5

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

FileName [cuddDecomp.c]

PackageName [cudd]

Synopsis [Functions for BDD decomposition.]

Description [External procedures included in this file:

Static procedures included in this module:

]

Author [Kavita Ravi, 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 43 of file cuddDecomp.c.

#define FactorsComplement ( factors   )     ((Conjuncts *)((long)(factors) | 01))

Definition at line 91 of file cuddDecomp.c.

#define FactorsNotStored ( factors   )     ((int)((long)(factors) & 01))

Definition at line 89 of file cuddDecomp.c.

#define FactorsUncomplement ( factors   )     ((Conjuncts *)((long)(factors) ^ 01))

Definition at line 93 of file cuddDecomp.c.

#define G_CR   4

Definition at line 49 of file cuddDecomp.c.

#define G_ST   3

Definition at line 48 of file cuddDecomp.c.

#define H_CR   6

Definition at line 51 of file cuddDecomp.c.

#define H_ST   5

Definition at line 50 of file cuddDecomp.c.

#define NONE   0

Definition at line 45 of file cuddDecomp.c.

#define PAIR_CR   2

Definition at line 47 of file cuddDecomp.c.

#define PAIR_ST   1

Definition at line 46 of file cuddDecomp.c.

#define THRESHOLD   10

Definition at line 44 of file cuddDecomp.c.

Function Documentation

static int cuddConjunctsAux ARGS ( (DdManager *dd, DdNode *f, DdNode **c1, DdNode **c2)   )  [static]
static Conjuncts* BuildConjuncts ARGS ( (DdManager *dd, DdNode *node, st_table *distanceTable, st_table *cacheTable, int approxDistance, int maxLocalRef, st_table *ghTable, st_table *mintermTable)   )  [static]
static Conjuncts* ZeroCase ARGS ( (DdManager *dd, DdNode *node, Conjuncts *factorsNv, st_table *ghTable, st_table *cacheTable, int switched)   )  [static]
static Conjuncts* CheckInTables ARGS ( (DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable, int *outOfMem)   )  [static]
static Conjuncts* PickOnePair ARGS ( (DdNode *node, DdNode *g1, DdNode *h1, DdNode *g2, DdNode *h2, st_table *ghTable, st_table *cacheTable)   )  [static]
static Conjuncts* CheckTablesCacheAndReturn ARGS ( (DdNode *node, DdNode *g, DdNode *h, st_table *ghTable, st_table *cacheTable)   )  [static]
static int PairInTables ARGS ( (DdNode *g, DdNode *h, st_table *ghTable)   )  [static]
static void ConjunctsFree ARGS ( (DdManager *dd, Conjuncts *factors)   )  [static]
static double CountMinterms ARGS ( (DdNode *node, double max, st_table *mintermTable, FILE *fp)   )  [static]
static NodeStat* CreateBotDist ARGS ( (DdNode *node, st_table *distanceTable)   )  [static]

AutomaticStart

static Conjuncts* BuildConjuncts ( DdManager *  dd,
DdNode *  node,
st_table *  distanceTable,
st_table *  cacheTable,
int  approxDistance,
int  maxLocalRef,
st_table *  ghTable,
st_table *  mintermTable 
) [static]

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

Synopsis [Builds the conjuncts recursively, bottom up.]

Description [Builds the conjuncts recursively, bottom up. Constants are returned as (f, f). The cache is checked for previously computed result. The decomposition points are determined by the local reference count of this node and the longest distance from the constant. At the decomposition point, the factors returned are (f, 1). Recur on the two children. The order is determined by the heavier branch. Combine the factors of the two children and pick the one that already occurs in the gh table. Occurence in g is indicated by value 1, occurence in h by 2, occurence in both 3.]

SideEffects []

SeeAlso [cuddConjunctsAux]

Definition at line 1654 of file cuddDecomp.c.

01663 {
01664     int topid, distance;
01665     Conjuncts *factorsNv, *factorsNnv, *factors;
01666     Conjuncts *dummy;
01667     DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
01668     double minNv = 0.0, minNnv = 0.0;
01669     double *doubleDummy;
01670     int switched =0;
01671     int outOfMem;
01672     int freeNv = 0, freeNnv = 0, freeTemp;
01673     NodeStat *nodeStat;
01674     int value;
01675 
01676     /* if f is constant, return (f,f) */
01677     if (Cudd_IsConstant(node)) {
01678         factors = ALLOC(Conjuncts, 1);
01679         if (factors == NULL) {
01680             dd->errorCode = CUDD_MEMORY_OUT;
01681             return(NULL);
01682         }
01683         factors->g = node;
01684         factors->h = node;
01685         return(FactorsComplement(factors));
01686     }
01687 
01688     /* If result (a pair of conjuncts) in cache, return the factors. */
01689     if (st_lookup(cacheTable, (char *)node, (char **)&dummy)) {
01690         factors = dummy;
01691         return(factors);
01692     }
01693     
01694     /* check distance and local reference count of this node */
01695     N = Cudd_Regular(node);
01696     if (!st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) {
01697         (void) fprintf(dd->err, "Not in table, Something wrong\n");
01698         dd->errorCode = CUDD_INTERNAL_ERROR;
01699         return(NULL);
01700     }
01701     distance = nodeStat->distance;
01702 
01703     /* at or below decomposition point, return (f, 1) */
01704     if (((nodeStat->localRef > maxLocalRef*2/3) &&
01705          (distance < approxDistance*2/3)) ||
01706             (distance <= approxDistance/4)) {
01707         factors = ALLOC(Conjuncts, 1);
01708         if (factors == NULL) {
01709             dd->errorCode = CUDD_MEMORY_OUT;
01710             return(NULL);
01711         }
01712         /* alternate assigning (f,1) */
01713         value = 0;
01714         if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
01715             if (value == 3) {
01716                 if (!lastTimeG) {
01717                     factors->g = node;
01718                     factors->h = one;
01719                     lastTimeG = 1;
01720                 } else {
01721                     factors->g = one;
01722                     factors->h = node;
01723                     lastTimeG = 0; 
01724                 }
01725             } else if (value == 1) {
01726                 factors->g = node;
01727                 factors->h = one;
01728             } else {
01729                 factors->g = one;
01730                 factors->h = node;
01731             }
01732         } else if (!lastTimeG) {
01733             factors->g = node;
01734             factors->h = one;
01735             lastTimeG = 1;
01736             value = 1;
01737             if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
01738                 dd->errorCode = CUDD_MEMORY_OUT;
01739                 FREE(factors);
01740                 return NULL;
01741             }
01742         } else {
01743             factors->g = one;
01744             factors->h = node;
01745             lastTimeG = 0;
01746             value = 2;
01747             if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
01748                 dd->errorCode = CUDD_MEMORY_OUT;
01749                 FREE(factors);
01750                 return NULL;
01751             }
01752         }
01753         return(FactorsComplement(factors));
01754     }
01755     
01756     /* get the children and recur */
01757     Nv = cuddT(N);
01758     Nnv = cuddE(N);
01759     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
01760     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
01761 
01762     /* Choose which subproblem to solve first based on the number of
01763      * minterms. We go first where there are more minterms.
01764      */
01765     if (!Cudd_IsConstant(Nv)) {
01766         if (!st_lookup(mintermTable, (char *)Nv, (char **)&doubleDummy)) {
01767             (void) fprintf(dd->err, "Not in table: Something wrong\n");
01768             dd->errorCode = CUDD_INTERNAL_ERROR;
01769             return(NULL);
01770         }
01771         minNv = *doubleDummy;
01772     }
01773     
01774     if (!Cudd_IsConstant(Nnv)) {
01775         if (!st_lookup(mintermTable, (char *)Nnv, (char **)&doubleDummy)) {
01776             (void) fprintf(dd->err, "Not in table: Something wrong\n");
01777             dd->errorCode = CUDD_INTERNAL_ERROR;
01778             return(NULL);
01779         }
01780         minNnv = *doubleDummy;
01781     }
01782     
01783     if (minNv < minNnv) {
01784         temp = Nv;
01785         Nv = Nnv;
01786         Nnv = temp;
01787         switched = 1;
01788     }
01789 
01790     /* build gt, ht recursively */
01791     if (Nv != zero) {
01792         factorsNv = BuildConjuncts(dd, Nv, distanceTable,
01793                                    cacheTable, approxDistance, maxLocalRef, 
01794                                    ghTable, mintermTable);
01795         if (factorsNv == NULL) return(NULL);
01796         freeNv = FactorsNotStored(factorsNv);
01797         factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
01798         cuddRef(factorsNv->g);
01799         cuddRef(factorsNv->h);
01800         
01801         /* Deal with the zero case */
01802         if (Nnv == zero) {
01803             /* is responsible for freeing factorsNv */
01804             factors = ZeroCase(dd, node, factorsNv, ghTable,
01805                                cacheTable, switched);
01806             if (freeNv) FREE(factorsNv);
01807             return(factors);
01808         }
01809     }
01810 
01811     /* build ge, he recursively */
01812     if (Nnv != zero) {
01813         factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
01814                                     cacheTable, approxDistance, maxLocalRef,
01815                                     ghTable, mintermTable);
01816         if (factorsNnv == NULL) {
01817             Cudd_RecursiveDeref(dd, factorsNv->g);
01818             Cudd_RecursiveDeref(dd, factorsNv->h);
01819             if (freeNv) FREE(factorsNv);
01820             return(NULL);
01821         }
01822         freeNnv = FactorsNotStored(factorsNnv);
01823         factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
01824         cuddRef(factorsNnv->g);
01825         cuddRef(factorsNnv->h);
01826         
01827         /* Deal with the zero case */
01828         if (Nv == zero) {
01829             /* is responsible for freeing factorsNv */
01830             factors = ZeroCase(dd, node, factorsNnv, ghTable,
01831                                cacheTable, switched);
01832             if (freeNnv) FREE(factorsNnv);
01833             return(factors);
01834         }
01835     }
01836 
01837     /* construct the 2 pairs */
01838     /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
01839     /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
01840     if (switched) {
01841         factors = factorsNnv;
01842         factorsNnv = factorsNv;
01843         factorsNv = factors;
01844         freeTemp = freeNv;
01845         freeNv = freeNnv;
01846         freeNnv = freeTemp;
01847     }
01848 
01849     /* Build the factors for this node. */
01850     topid = N->index;
01851     topv = dd->vars[topid];
01852     
01853     g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g);
01854     if (g1 == NULL) {
01855         Cudd_RecursiveDeref(dd, factorsNv->g);
01856         Cudd_RecursiveDeref(dd, factorsNv->h);
01857         Cudd_RecursiveDeref(dd, factorsNnv->g);
01858         Cudd_RecursiveDeref(dd, factorsNnv->h);
01859         if (freeNv) FREE(factorsNv);
01860         if (freeNnv) FREE(factorsNnv);
01861         return(NULL);
01862     }
01863 
01864     cuddRef(g1);
01865 
01866     h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h);
01867     if (h1 == NULL) {
01868         Cudd_RecursiveDeref(dd, factorsNv->g);
01869         Cudd_RecursiveDeref(dd, factorsNv->h);
01870         Cudd_RecursiveDeref(dd, factorsNnv->g);
01871         Cudd_RecursiveDeref(dd, factorsNnv->h);
01872         Cudd_RecursiveDeref(dd, g1);
01873         if (freeNv) FREE(factorsNv);
01874         if (freeNnv) FREE(factorsNnv);
01875         return(NULL);
01876     }
01877 
01878     cuddRef(h1);
01879 
01880     g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h);
01881     if (g2 == NULL) {
01882         Cudd_RecursiveDeref(dd, factorsNv->h);
01883         Cudd_RecursiveDeref(dd, factorsNv->g);
01884         Cudd_RecursiveDeref(dd, factorsNnv->g);
01885         Cudd_RecursiveDeref(dd, factorsNnv->h);
01886         Cudd_RecursiveDeref(dd, g1);
01887         Cudd_RecursiveDeref(dd, h1);
01888         if (freeNv) FREE(factorsNv);
01889         if (freeNnv) FREE(factorsNnv);
01890         return(NULL);
01891     }
01892     cuddRef(g2);
01893     Cudd_RecursiveDeref(dd, factorsNv->g);
01894     Cudd_RecursiveDeref(dd, factorsNnv->h);
01895 
01896     h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g);
01897     if (h2 == NULL) {
01898         Cudd_RecursiveDeref(dd, factorsNv->g);
01899         Cudd_RecursiveDeref(dd, factorsNv->h);
01900         Cudd_RecursiveDeref(dd, factorsNnv->g);
01901         Cudd_RecursiveDeref(dd, factorsNnv->h);
01902         Cudd_RecursiveDeref(dd, g1);
01903         Cudd_RecursiveDeref(dd, h1);
01904         Cudd_RecursiveDeref(dd, g2);
01905         if (freeNv) FREE(factorsNv);
01906         if (freeNnv) FREE(factorsNnv);
01907         return(NULL);
01908     }
01909     cuddRef(h2);
01910     Cudd_RecursiveDeref(dd, factorsNv->h);
01911     Cudd_RecursiveDeref(dd, factorsNnv->g);
01912     if (freeNv) FREE(factorsNv);
01913     if (freeNnv) FREE(factorsNnv);
01914 
01915     /* check for each pair in tables and choose one */
01916     factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
01917     if (outOfMem) {
01918         dd->errorCode = CUDD_MEMORY_OUT;
01919         Cudd_RecursiveDeref(dd, g1);
01920         Cudd_RecursiveDeref(dd, h1);
01921         Cudd_RecursiveDeref(dd, g2);
01922         Cudd_RecursiveDeref(dd, h2);
01923         return(NULL);
01924     }
01925     if (factors != NULL) {
01926         if ((factors->g == g1) || (factors->g == h1)) {
01927             Cudd_RecursiveDeref(dd, g2);
01928             Cudd_RecursiveDeref(dd, h2);
01929         } else {
01930             Cudd_RecursiveDeref(dd, g1);
01931             Cudd_RecursiveDeref(dd, h1);
01932         }
01933         return(factors);
01934     }
01935 
01936     /* if not in tables, pick one pair */
01937     factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
01938     if (factors == NULL) {
01939         dd->errorCode = CUDD_MEMORY_OUT;
01940         Cudd_RecursiveDeref(dd, g1);
01941         Cudd_RecursiveDeref(dd, h1);
01942         Cudd_RecursiveDeref(dd, g2);
01943         Cudd_RecursiveDeref(dd, h2);
01944     } else {
01945         /* now free what was created and not used */
01946         if ((factors->g == g1) || (factors->g == h1)) {
01947             Cudd_RecursiveDeref(dd, g2);
01948             Cudd_RecursiveDeref(dd, h2);
01949         } else {
01950             Cudd_RecursiveDeref(dd, g1);
01951             Cudd_RecursiveDeref(dd, h1);
01952         }
01953     }
01954         
01955     return(factors);
01956     
01957 } /* end of BuildConjuncts */

static Conjuncts* CheckInTables ( DdNode *  node,
DdNode *  g1,
DdNode *  h1,
DdNode *  g2,
DdNode *  h2,
st_table *  ghTable,
st_table *  cacheTable,
int *  outOfMem 
) [static]

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

Synopsis [Check if the two pairs exist in the table, If any of the conjuncts do exist, store in the cache and return the corresponding pair.]

Description [Check if the two pairs exist in the table. If any of the conjuncts do exist, store in the cache and return the corresponding pair.]

SideEffects []

SeeAlso [ZeroCase BuildConjuncts]

Definition at line 1186 of file cuddDecomp.c.

01195 {
01196     int pairValue1,  pairValue2;
01197     Conjuncts *factors;
01198     int value;
01199     
01200     *outOfMem = 0;
01201 
01202     /* check existence of pair in table */
01203     pairValue1 = PairInTables(g1, h1, ghTable);
01204     pairValue2 = PairInTables(g2, h2, ghTable);
01205 
01206     /* if none of the 4 exist in the gh tables, return NULL */
01207     if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
01208         return NULL;
01209     }
01210     
01211     factors = ALLOC(Conjuncts, 1);
01212     if (factors == NULL) {
01213         *outOfMem = 1;
01214         return NULL;
01215     }
01216 
01217     /* pairs that already exist in the table get preference. */
01218     if (pairValue1 == PAIR_ST) {
01219         factors->g = g1;
01220         factors->h = h1;
01221     } else if (pairValue2 == PAIR_ST) {
01222         factors->g = g2;
01223         factors->h = h2;
01224     } else if (pairValue1 == PAIR_CR) {
01225         factors->g = h1;
01226         factors->h = g1;
01227     } else if (pairValue2 == PAIR_CR) {
01228         factors->g = h2;
01229         factors->h = g2;
01230     } else if (pairValue1 == G_ST) {
01231         /* g exists in the table, h is not found in either table */
01232         factors->g = g1;
01233         factors->h = h1;
01234         if (h1 != one) {
01235             value = 2;
01236             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
01237                           (char *)(long)value) == ST_OUT_OF_MEM) {
01238                 *outOfMem = 1;
01239                 FREE(factors);
01240                 return(NULL);
01241             }
01242         }
01243     } else if (pairValue1 == BOTH_G) {
01244         /* g and h are  found in the g table */
01245         factors->g = g1;
01246         factors->h = h1;
01247         if (h1 != one) {
01248             value = 3;
01249             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
01250                           (char *)(long)value) == ST_OUT_OF_MEM) {
01251                 *outOfMem = 1;
01252                 FREE(factors);
01253                 return(NULL);
01254             }
01255         }
01256     } else if (pairValue1 == H_ST) {
01257         /* h exists in the table, g is not found in either table */
01258         factors->g = g1;
01259         factors->h = h1;
01260         if (g1 != one) {
01261             value = 1;
01262             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
01263                           (char *)(long)value) == ST_OUT_OF_MEM) {
01264                 *outOfMem = 1;
01265                 FREE(factors);
01266                 return(NULL);
01267             }
01268         }
01269     } else if (pairValue1 == BOTH_H) {
01270         /* g and h are  found in the h table */
01271         factors->g = g1;
01272         factors->h = h1;
01273         if (g1 != one) {
01274             value = 3;
01275             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
01276                           (char *)(long)value) == ST_OUT_OF_MEM) {
01277                 *outOfMem = 1;
01278                 FREE(factors);
01279                 return(NULL);
01280             }
01281         }
01282     } else if (pairValue2 == G_ST) {
01283         /* g exists in the table, h is not found in either table */
01284         factors->g = g2;
01285         factors->h = h2;
01286         if (h2 != one) {
01287             value = 2;
01288             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
01289                           (char *)(long)value) == ST_OUT_OF_MEM) {
01290                 *outOfMem = 1;
01291                 FREE(factors);
01292                 return(NULL);
01293             }
01294         }
01295     } else if  (pairValue2 == BOTH_G) {
01296         /* g and h are  found in the g table */
01297         factors->g = g2;
01298         factors->h = h2;
01299         if (h2 != one) {
01300             value = 3;
01301             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
01302                           (char *)(long)value) == ST_OUT_OF_MEM) {
01303                 *outOfMem = 1;
01304                 FREE(factors);
01305                 return(NULL);
01306             }
01307         }
01308     } else if (pairValue2 == H_ST) { 
01309         /* h exists in the table, g is not found in either table */
01310         factors->g = g2;
01311         factors->h = h2;
01312         if (g2 != one) {
01313             value = 1;
01314             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
01315                           (char *)(long)value) == ST_OUT_OF_MEM) {
01316                 *outOfMem = 1;
01317                 FREE(factors);
01318                 return(NULL);
01319             }
01320         }
01321     } else if (pairValue2 == BOTH_H) {
01322         /* g and h are  found in the h table */
01323         factors->g = g2;
01324         factors->h = h2;
01325         if (g2 != one) {
01326             value = 3;
01327             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
01328                           (char *)(long)value) == ST_OUT_OF_MEM) {
01329                 *outOfMem = 1;
01330                 FREE(factors);
01331                 return(NULL);
01332             }
01333         }
01334     } else if (pairValue1 == G_CR) {
01335         /* g found in h table and h in none */
01336         factors->g = h1;
01337         factors->h = g1;
01338         if (h1 != one) {
01339             value = 1;
01340             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
01341                           (char *)(long)value) == ST_OUT_OF_MEM) {
01342                 *outOfMem = 1;
01343                 FREE(factors);
01344                 return(NULL);
01345             }
01346         }
01347     } else if (pairValue1 == H_CR) {
01348         /* h found in g table and g in none */
01349         factors->g = h1;
01350         factors->h = g1;
01351         if (g1 != one) {
01352             value = 2;
01353             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
01354                           (char *)(long)value) == ST_OUT_OF_MEM) {
01355                 *outOfMem = 1;
01356                 FREE(factors);
01357                 return(NULL);
01358             }
01359         }
01360     } else if (pairValue2 == G_CR) {
01361         /* g found in h table and h in none */
01362         factors->g = h2;
01363         factors->h = g2;
01364         if (h2 != one) {
01365             value = 1;
01366             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
01367                           (char *)(long)value) == ST_OUT_OF_MEM) {
01368                 *outOfMem = 1;
01369                 FREE(factors);
01370                 return(NULL);
01371             }
01372         }
01373     } else if (pairValue2 == H_CR) {
01374         /* h found in g table and g in none */
01375         factors->g = h2;
01376         factors->h = g2;
01377         if (g2 != one) {
01378             value = 2;
01379             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
01380                           (char *)(long)value) == ST_OUT_OF_MEM) {
01381                 *outOfMem = 1;
01382                 FREE(factors);
01383                 return(NULL);
01384             }
01385         }
01386     }
01387     
01388     /* Store factors in cache table for later use. */
01389     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
01390             ST_OUT_OF_MEM) {
01391         *outOfMem = 1;
01392         FREE(factors);
01393         return(NULL);
01394     }
01395     return factors;
01396 } /* end of CheckInTables */

static Conjuncts* CheckTablesCacheAndReturn ( DdNode *  node,
DdNode *  g,
DdNode *  h,
st_table *  ghTable,
st_table *  cacheTable 
) [static]

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

Synopsis [Check the tables for the existence of pair and return one combination, cache the result.]

Description [Check the tables for the existence of pair and return one combination, cache the result. The assumption is that one of the conjuncts is already in the tables.]

SideEffects [g and h referenced for the cache]

SeeAlso [ZeroCase]

Definition at line 963 of file cuddDecomp.c.

00969 {
00970     int pairValue;
00971     int value;
00972     Conjuncts *factors;
00973     
00974     value = 0;
00975     /* check tables */
00976     pairValue = PairInTables(g, h, ghTable);
00977     assert(pairValue != NONE);
00978     /* if both dont exist in table, we know one exists(either g or h).
00979      * Therefore store the other and proceed
00980      */
00981     factors = ALLOC(Conjuncts, 1);
00982     if (factors == NULL) return(NULL);
00983     if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
00984         if (g != one) {
00985             value = 0;
00986             if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
00987                 value |= 1;
00988             } else {
00989                 value = 1;
00990             }
00991             if (st_insert(ghTable, (char *)Cudd_Regular(g),
00992                           (char *)(long)value) == ST_OUT_OF_MEM) {
00993                 return(NULL);
00994             }
00995         }
00996         factors->g = g;
00997         factors->h = h;
00998     } else  if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
00999         if (h != one) {
01000             value = 0;
01001             if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
01002                 value |= 2;
01003             } else {
01004                 value = 2;
01005             }
01006             if (st_insert(ghTable, (char *)Cudd_Regular(h),
01007                           (char *)(long)value) == ST_OUT_OF_MEM) {
01008                 return(NULL);
01009             }
01010         }
01011         factors->g = g;
01012         factors->h = h;
01013     } else if (pairValue == H_CR) {
01014         if (g != one) {
01015             value = 2;
01016             if (st_insert(ghTable, (char *)Cudd_Regular(g),
01017                           (char *)(long)value) == ST_OUT_OF_MEM) {
01018                 return(NULL);
01019             }
01020         }
01021         factors->g = h;
01022         factors->h = g;
01023     } else if (pairValue == G_CR) {
01024         if (h != one) {
01025             value = 1;
01026             if (st_insert(ghTable, (char *)Cudd_Regular(h),
01027                           (char *)(long)value) == ST_OUT_OF_MEM) {
01028                 return(NULL);
01029             }
01030         }
01031         factors->g = h;
01032         factors->h = g;
01033     } else if (pairValue == PAIR_CR) {
01034     /* pair exists in table */
01035         factors->g = h;
01036         factors->h = g;
01037     } else if (pairValue == PAIR_ST) {
01038         factors->g = g;
01039         factors->h = h;
01040     }
01041             
01042     /* cache the result for this node */
01043     if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
01044         FREE(factors);
01045         return(NULL);
01046     }
01047 
01048     return(factors);
01049 
01050 } /* end of CheckTablesCacheAndReturn */

static void ConjunctsFree ( DdManager *  dd,
Conjuncts *  factors 
) [static]

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

Synopsis [Free factors structure]

Description []

SideEffects [None]

SeeAlso []

Definition at line 873 of file cuddDecomp.c.

00876 {
00877     Cudd_RecursiveDeref(dd, factors->g);
00878     Cudd_RecursiveDeref(dd, factors->h);
00879     FREE(factors);
00880     return;
00881 
00882 } /* end of ConjunctsFree */

static double CountMinterms ( DdNode *  node,
double  max,
st_table *  mintermTable,
FILE *  fp 
) [static]

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

Synopsis [Count the number of minterms of each node ina a BDD and store it in a hash table.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 810 of file cuddDecomp.c.

00815 {
00816     DdNode *N, *Nv, *Nnv;
00817     double min, minNv, minNnv;
00818     double *dummy;
00819 
00820     N = Cudd_Regular(node);
00821 
00822     if (cuddIsConstant(N)) {
00823         if (node == zero) {
00824             return(0);
00825         } else {
00826             return(max);
00827         }
00828     }
00829 
00830     /* Return the entry in the table if found. */
00831     if (st_lookup(mintermTable, (char *)node, (char **)&dummy)) {
00832         min = *dummy;
00833         return(min);
00834     }
00835 
00836     Nv = cuddT(N);
00837     Nnv = cuddE(N);
00838     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
00839     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
00840 
00841     /* Recur on the children. */
00842     minNv = CountMinterms(Nv, max, mintermTable, fp);
00843     if (minNv == -1.0) return(-1.0);
00844     minNnv = CountMinterms(Nnv, max, mintermTable, fp);
00845     if (minNnv == -1.0) return(-1.0);
00846     min = minNv / 2.0 + minNnv / 2.0;
00847     /* store 
00848      */
00849 
00850     dummy = ALLOC(double, 1);
00851     if (dummy == NULL) return(-1.0);
00852     *dummy = min;
00853     if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
00854         (void) fprintf(fp, "st table insert failed\n");
00855     }
00856     return(min);
00857 
00858 } /* end of CountMinterms */

static NodeStat* CreateBotDist ( DdNode *  node,
st_table *  distanceTable 
) [static]

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

Synopsis [Get longest distance of node from constant.]

Description [Get longest distance of node from constant. Returns the distance of the root from the constant if successful; CUDD_OUT_OF_MEM otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 741 of file cuddDecomp.c.

00744 {
00745     DdNode *N, *Nv, *Nnv;
00746     int distance, distanceNv, distanceNnv;
00747     NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv;
00748 
00749 #if 0
00750     if (Cudd_IsConstant(node)) {
00751         return(0);
00752     }
00753 #endif
00754     
00755     /* Return the entry in the table if found. */
00756     N = Cudd_Regular(node);
00757     if (st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) {
00758         nodeStat->localRef++;
00759         return(nodeStat);
00760     }
00761 
00762     Nv = cuddT(N);
00763     Nnv = cuddE(N);
00764     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
00765     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
00766 
00767     /* Recur on the children. */
00768     nodeStatNv = CreateBotDist(Nv, distanceTable);
00769     if (nodeStatNv == NULL) return(NULL);
00770     distanceNv = nodeStatNv->distance;
00771 
00772     nodeStatNnv = CreateBotDist(Nnv, distanceTable);
00773     if (nodeStatNnv == NULL) return(NULL);
00774     distanceNnv = nodeStatNnv->distance;
00775     /* Store max distance from constant; note sometimes this distance
00776     ** may be to 0.
00777     */
00778     distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);
00779 
00780     nodeStat = ALLOC(NodeStat, 1);
00781     if (nodeStat == NULL) {
00782         return(0);
00783     }
00784     nodeStat->distance = distance;
00785     nodeStat->localRef = 1;
00786     
00787     if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
00788         ST_OUT_OF_MEM) {
00789         return(0);
00790 
00791     }
00792     return(nodeStat);
00793 
00794 } /* end of CreateBotDist */

int Cudd_bddApproxConjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  conjuncts 
)

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

Synopsis [Performs two-way conjunctive decomposition of a BDD.]

Description [Performs two-way conjunctive decomposition of a BDD. This procedure owes its name to the use of supersetting to obtain an initial factor of the given function. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The conjuncts produced by this procedure tend to be imbalanced.]

SideEffects [The factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox Cudd_bddSqueeze Cudd_bddLICompaction]

Definition at line 144 of file cuddDecomp.c.

00148 {
00149     DdNode *superset1, *superset2, *glocal, *hlocal;
00150     int nvars = Cudd_SupportSize(dd,f);
00151 
00152     /* Find a tentative first factor by overapproximation and minimization. */
00153     superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0);
00154     if (superset1 == NULL) return(0);
00155     cuddRef(superset1);
00156     superset2 = Cudd_bddSqueeze(dd,f,superset1);
00157     if (superset2 == NULL) {
00158         Cudd_RecursiveDeref(dd,superset1);
00159         return(0);
00160     }
00161     cuddRef(superset2);
00162     Cudd_RecursiveDeref(dd,superset1);
00163 
00164     /* Compute the second factor by minimization. */
00165     hlocal = Cudd_bddLICompaction(dd,f,superset2);
00166     if (hlocal == NULL) {
00167         Cudd_RecursiveDeref(dd,superset2);
00168         return(0);
00169     }
00170     cuddRef(hlocal);
00171 
00172     /* Refine the first factor by minimization. If h turns out to be f, this
00173     ** step guarantees that g will be 1. */
00174     glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
00175     if (glocal == NULL) {
00176         Cudd_RecursiveDeref(dd,superset2);
00177         Cudd_RecursiveDeref(dd,hlocal);
00178         return(0);
00179     }
00180     cuddRef(glocal);
00181     Cudd_RecursiveDeref(dd,superset2);
00182 
00183     if (glocal != DD_ONE(dd)) {
00184         if (hlocal != DD_ONE(dd)) {
00185             *conjuncts = ALLOC(DdNode *,2);
00186             if (*conjuncts == NULL) {
00187                 Cudd_RecursiveDeref(dd,glocal);
00188                 Cudd_RecursiveDeref(dd,hlocal);
00189                 dd->errorCode = CUDD_MEMORY_OUT;
00190                 return(0);
00191             }
00192             (*conjuncts)[0] = glocal;
00193             (*conjuncts)[1] = hlocal;
00194             return(2);
00195         } else {
00196             Cudd_RecursiveDeref(dd,hlocal);
00197             *conjuncts = ALLOC(DdNode *,1);
00198             if (*conjuncts == NULL) {
00199                 Cudd_RecursiveDeref(dd,glocal);
00200                 dd->errorCode = CUDD_MEMORY_OUT;
00201                 return(0);
00202             }
00203             (*conjuncts)[0] = glocal;
00204             return(1);
00205         }
00206     } else {
00207         Cudd_RecursiveDeref(dd,glocal);
00208         *conjuncts = ALLOC(DdNode *,1);
00209         if (*conjuncts == NULL) {
00210             Cudd_RecursiveDeref(dd,hlocal);
00211             dd->errorCode = CUDD_MEMORY_OUT;
00212             return(0);
00213         }
00214         (*conjuncts)[0] = hlocal;
00215         return(1);
00216     }
00217 
00218 } /* end of Cudd_bddApproxConjDecomp */

int Cudd_bddApproxDisjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  disjuncts 
)

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

Synopsis [Performs two-way disjunctive decomposition of a BDD.]

Description [Performs two-way disjunctive decomposition of a BDD. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The disjuncts produced by this procedure tend to be imbalanced.]

SideEffects [The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]

Definition at line 242 of file cuddDecomp.c.

00246 {
00247     int result, i;
00248 
00249     result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
00250     for (i = 0; i < result; i++) {
00251         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00252     }
00253     return(result);
00254 
00255 } /* end of Cudd_bddApproxDisjDecomp */

int Cudd_bddGenConjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  conjuncts 
)

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

Synopsis [Performs two-way conjunctive decomposition of a BDD.]

Description [Performs two-way conjunctive decomposition of a BDD. This procedure owes its name to the fact tht it generalizes the decomposition based on the cofactors with respect to one variable. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The conjuncts produced by this procedure tend to be balanced.]

SideEffects [The two factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp]

Definition at line 465 of file cuddDecomp.c.

00469 {
00470     int result;
00471     DdNode *glocal, *hlocal;
00472 
00473     one = DD_ONE(dd);
00474     zero = Cudd_Not(one);
00475     
00476     do {
00477         dd->reordered = 0;
00478         result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
00479     } while (dd->reordered == 1);
00480 
00481     if (result == 0) {
00482         return(0);
00483     }
00484 
00485     if (glocal != one) {
00486         if (hlocal != one) {
00487             *conjuncts = ALLOC(DdNode *,2);
00488             if (*conjuncts == NULL) {
00489                 Cudd_RecursiveDeref(dd,glocal);
00490                 Cudd_RecursiveDeref(dd,hlocal);
00491                 dd->errorCode = CUDD_MEMORY_OUT;
00492                 return(0);
00493             }
00494             (*conjuncts)[0] = glocal;
00495             (*conjuncts)[1] = hlocal;
00496             return(2);
00497         } else {
00498             Cudd_RecursiveDeref(dd,hlocal);
00499             *conjuncts = ALLOC(DdNode *,1);
00500             if (*conjuncts == NULL) {
00501                 Cudd_RecursiveDeref(dd,glocal);
00502                 dd->errorCode = CUDD_MEMORY_OUT;
00503                 return(0);
00504             }
00505             (*conjuncts)[0] = glocal;
00506             return(1);
00507         }
00508     } else {
00509         Cudd_RecursiveDeref(dd,glocal);
00510         *conjuncts = ALLOC(DdNode *,1);
00511         if (*conjuncts == NULL) {
00512             Cudd_RecursiveDeref(dd,hlocal);
00513             dd->errorCode = CUDD_MEMORY_OUT;
00514             return(0);
00515         }
00516         (*conjuncts)[0] = hlocal;
00517         return(1);
00518     }
00519 
00520 } /* end of Cudd_bddGenConjDecomp */

int Cudd_bddGenDisjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  disjuncts 
)

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

Synopsis [Performs two-way disjunctive decomposition of a BDD.]

Description [Performs two-way disjunctive decomposition of a BDD. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The disjuncts produced by this procedure tend to be balanced.]

SideEffects [The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp]

Definition at line 544 of file cuddDecomp.c.

00548 {
00549     int result, i;
00550 
00551     result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
00552     for (i = 0; i < result; i++) {
00553         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00554     }
00555     return(result);
00556 
00557 } /* end of Cudd_bddGenDisjDecomp */

int Cudd_bddIterConjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  conjuncts 
)

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

Synopsis [Performs two-way conjunctive decomposition of a BDD.]

Description [Performs two-way conjunctive decomposition of a BDD. This procedure owes its name to the iterated use of supersetting to obtain a factor of the given function. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The conjuncts produced by this procedure tend to be imbalanced.]

SideEffects [The factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox Cudd_bddSqueeze Cudd_bddLICompaction]

Definition at line 282 of file cuddDecomp.c.

00286 {
00287     DdNode *superset1, *superset2, *old[2], *res[2];
00288     int sizeOld, sizeNew;
00289     int nvars = Cudd_SupportSize(dd,f);
00290 
00291     old[0] = DD_ONE(dd);
00292     cuddRef(old[0]);
00293     old[1] = f;
00294     cuddRef(old[1]);
00295     sizeOld = Cudd_SharingSize(old,2);
00296 
00297     do {
00298         /* Find a tentative first factor by overapproximation and
00299         ** minimization. */
00300         superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
00301         if (superset1 == NULL) {
00302             Cudd_RecursiveDeref(dd,old[0]);
00303             Cudd_RecursiveDeref(dd,old[1]);
00304             return(0);
00305         }
00306         cuddRef(superset1);
00307         superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
00308         if (superset2 == NULL) {
00309             Cudd_RecursiveDeref(dd,old[0]);
00310             Cudd_RecursiveDeref(dd,old[1]);
00311             Cudd_RecursiveDeref(dd,superset1);
00312             return(0);
00313         }
00314         cuddRef(superset2);
00315         Cudd_RecursiveDeref(dd,superset1);
00316         res[0] = Cudd_bddAnd(dd,old[0],superset2);
00317         if (res[0] == NULL) {
00318             Cudd_RecursiveDeref(dd,superset2);
00319             Cudd_RecursiveDeref(dd,old[0]);
00320             Cudd_RecursiveDeref(dd,old[1]);
00321             return(0);
00322         }
00323         cuddRef(res[0]);
00324         Cudd_RecursiveDeref(dd,superset2);
00325         if (res[0] == old[0]) {
00326             Cudd_RecursiveDeref(dd,res[0]);
00327             break;      /* avoid infinite loop */
00328         }
00329 
00330         /* Compute the second factor by minimization. */
00331         res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
00332         if (res[1] == NULL) {
00333             Cudd_RecursiveDeref(dd,old[0]);
00334             Cudd_RecursiveDeref(dd,old[1]);
00335             return(0);
00336         }
00337         cuddRef(res[1]);
00338 
00339         sizeNew = Cudd_SharingSize(res,2);
00340         if (sizeNew <= sizeOld) {
00341             Cudd_RecursiveDeref(dd,old[0]);
00342             old[0] = res[0];
00343             Cudd_RecursiveDeref(dd,old[1]);
00344             old[1] = res[1];
00345             sizeOld = sizeNew;
00346         } else {
00347             Cudd_RecursiveDeref(dd,res[0]);
00348             Cudd_RecursiveDeref(dd,res[1]);
00349             break;
00350         }
00351 
00352     } while (1);
00353 
00354     /* Refine the first factor by minimization. If h turns out to
00355     ** be f, this step guarantees that g will be 1. */
00356     superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
00357     if (superset1 == NULL) {
00358         Cudd_RecursiveDeref(dd,old[0]);
00359         Cudd_RecursiveDeref(dd,old[1]);
00360         return(0);
00361     }
00362     cuddRef(superset1);
00363     Cudd_RecursiveDeref(dd,old[0]);
00364     old[0] = superset1;
00365 
00366     if (old[0] != DD_ONE(dd)) {
00367         if (old[1] != DD_ONE(dd)) {
00368             *conjuncts = ALLOC(DdNode *,2);
00369             if (*conjuncts == NULL) {
00370                 Cudd_RecursiveDeref(dd,old[0]);
00371                 Cudd_RecursiveDeref(dd,old[1]);
00372                 dd->errorCode = CUDD_MEMORY_OUT;
00373                 return(0);
00374             }
00375             (*conjuncts)[0] = old[0];
00376             (*conjuncts)[1] = old[1];
00377             return(2);
00378         } else {
00379             Cudd_RecursiveDeref(dd,old[1]);
00380             *conjuncts = ALLOC(DdNode *,1);
00381             if (*conjuncts == NULL) {
00382                 Cudd_RecursiveDeref(dd,old[0]);
00383                 dd->errorCode = CUDD_MEMORY_OUT;
00384                 return(0);
00385             }
00386             (*conjuncts)[0] = old[0];
00387             return(1);
00388         }
00389     } else {
00390         Cudd_RecursiveDeref(dd,old[0]);
00391         *conjuncts = ALLOC(DdNode *,1);
00392         if (*conjuncts == NULL) {
00393             Cudd_RecursiveDeref(dd,old[1]);
00394             dd->errorCode = CUDD_MEMORY_OUT;
00395             return(0);
00396         }
00397         (*conjuncts)[0] = old[1];
00398         return(1);
00399     }
00400 
00401 } /* end of Cudd_bddIterConjDecomp */

int Cudd_bddIterDisjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  disjuncts 
)

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

Synopsis [Performs two-way disjunctive decomposition of a BDD.]

Description [Performs two-way disjunctive decomposition of a BDD. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise. The disjuncts produced by this procedure tend to be imbalanced.]

SideEffects [The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]

Definition at line 425 of file cuddDecomp.c.

00429 {
00430     int result, i;
00431 
00432     result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
00433     for (i = 0; i < result; i++) {
00434         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00435     }
00436     return(result);
00437 
00438 } /* end of Cudd_bddIterDisjDecomp */

int Cudd_bddVarConjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  conjuncts 
)

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

Synopsis [Performs two-way conjunctive decomposition of a BDD.]

Description [Conjunctively decomposes one BDD according to a variable. If f is the function of the BDD and x is the variable, the decomposition is (f+x)(f+x'). The variable is chosen so as to balance the sizes of the two conjuncts and to keep them small. Returns the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.]

SideEffects [The two factors are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp]

Definition at line 584 of file cuddDecomp.c.

00588 {
00589     int best;
00590     int min;
00591     DdNode *support, *scan, *var, *glocal, *hlocal;
00592 
00593     /* Find best cofactoring variable. */
00594     support = Cudd_Support(dd,f);
00595     if (support == NULL) return(0);
00596     if (Cudd_IsConstant(support)) {
00597         *conjuncts = ALLOC(DdNode *,1);
00598         if (*conjuncts == NULL) {
00599             dd->errorCode = CUDD_MEMORY_OUT;
00600             return(0);
00601         }
00602         (*conjuncts)[0] = f;
00603         cuddRef((*conjuncts)[0]);
00604         return(1);
00605     }
00606     cuddRef(support);
00607     min = 1000000000;
00608     best = -1;
00609     scan = support;
00610     while (!Cudd_IsConstant(scan)) {
00611         int i = scan->index;
00612         int est1 = Cudd_EstimateCofactor(dd,f,i,1);
00613         int est0 = Cudd_EstimateCofactor(dd,f,i,0);
00614         /* Minimize the size of the larger of the two cofactors. */
00615         int est = (est1 > est0) ? est1 : est0;
00616         if (est < min) {
00617             min = est;
00618             best = i;
00619         }
00620         scan = cuddT(scan);
00621     }
00622 #ifdef DD_DEBUG
00623     assert(best >= 0 && best < dd->size);
00624 #endif
00625     Cudd_RecursiveDeref(dd,support);
00626 
00627     var = Cudd_bddIthVar(dd,best);
00628     glocal = Cudd_bddOr(dd,f,var);
00629     if (glocal == NULL) {
00630         return(0);
00631     }
00632     cuddRef(glocal);
00633     hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
00634     if (hlocal == NULL) {
00635         Cudd_RecursiveDeref(dd,glocal);
00636         return(0);
00637     }
00638     cuddRef(hlocal);
00639 
00640     if (glocal != DD_ONE(dd)) {
00641         if (hlocal != DD_ONE(dd)) {
00642             *conjuncts = ALLOC(DdNode *,2);
00643             if (*conjuncts == NULL) {
00644                 Cudd_RecursiveDeref(dd,glocal);
00645                 Cudd_RecursiveDeref(dd,hlocal);
00646                 dd->errorCode = CUDD_MEMORY_OUT;
00647                 return(0);
00648             }
00649             (*conjuncts)[0] = glocal;
00650             (*conjuncts)[1] = hlocal;
00651             return(2);
00652         } else {
00653             Cudd_RecursiveDeref(dd,hlocal);
00654             *conjuncts = ALLOC(DdNode *,1);
00655             if (*conjuncts == NULL) {
00656                 Cudd_RecursiveDeref(dd,glocal);
00657                 dd->errorCode = CUDD_MEMORY_OUT;
00658                 return(0);
00659             }
00660             (*conjuncts)[0] = glocal;
00661             return(1);
00662         }
00663     } else {
00664         Cudd_RecursiveDeref(dd,glocal);
00665         *conjuncts = ALLOC(DdNode *,1);
00666         if (*conjuncts == NULL) {
00667             Cudd_RecursiveDeref(dd,hlocal);
00668             dd->errorCode = CUDD_MEMORY_OUT;
00669             return(0);
00670         }
00671         (*conjuncts)[0] = hlocal;
00672         return(1);
00673     }
00674 
00675 } /* end of Cudd_bddVarConjDecomp */

int Cudd_bddVarDisjDecomp ( DdManager *  dd,
DdNode *  f,
DdNode ***  disjuncts 
)

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

Synopsis [Performs two-way disjunctive decomposition of a BDD.]

Description [Performs two-way disjunctive decomposition of a BDD according to a variable. If f is the function of the BDD and x is the variable, the decomposition is f*x + f*x'. The variable is chosen so as to balance the sizes of the two disjuncts and to keep them small. Returns the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.]

SideEffects [The two disjuncts are returned in an array as side effects. The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.]

SeeAlso [Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp]

Definition at line 702 of file cuddDecomp.c.

00706 {
00707     int result, i;
00708 
00709     result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
00710     for (i = 0; i < result; i++) {
00711         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00712     }
00713     return(result);
00714 
00715 } /* end of Cudd_bddVarDisjDecomp */

static int cuddConjunctsAux ( DdManager *  dd,
DdNode *  f,
DdNode **  c1,
DdNode **  c2 
) [static]

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

Synopsis [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.]

Description [Procedure to compute two conjunctive factors of f and place in *c1 and *c2. Sets up the required data - table of distances from the constant and local reference count. Also minterm table. ]

SideEffects []

SeeAlso []

Definition at line 1974 of file cuddDecomp.c.

01979 {
01980     st_table *distanceTable = NULL;
01981     st_table *cacheTable = NULL;
01982     st_table *mintermTable = NULL;
01983     st_table *ghTable = NULL;
01984     st_generator *stGen;
01985     char *key, *value;
01986     Conjuncts *factors;
01987     int distance, approxDistance;
01988     double max, minterms;
01989     int freeFactors;
01990     NodeStat *nodeStat;
01991     int maxLocalRef;
01992     
01993     /* initialize */
01994     *c1 = NULL;
01995     *c2 = NULL;
01996 
01997     /* initialize distances table */
01998     distanceTable = st_init_table(st_ptrcmp,st_ptrhash);
01999     if (distanceTable == NULL) goto outOfMem;
02000     
02001     /* make the entry for the constant */
02002     nodeStat = ALLOC(NodeStat, 1);
02003     if (nodeStat == NULL) goto outOfMem;
02004     nodeStat->distance = 0;
02005     nodeStat->localRef = 1;
02006     if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) {
02007         goto outOfMem;
02008     }
02009 
02010     /* Count node distances from constant. */
02011     nodeStat = CreateBotDist(f, distanceTable);
02012     if (nodeStat == NULL) goto outOfMem;
02013 
02014     /* set the distance for the decomposition points */
02015     approxDistance = (DEPTH < nodeStat->distance) ? nodeStat->distance : DEPTH;
02016     distance = nodeStat->distance;
02017 
02018     if (distance < approxDistance) {
02019         /* Too small to bother. */
02020         *c1 = f;
02021         *c2 = DD_ONE(dd);
02022         cuddRef(*c1); cuddRef(*c2);
02023         stGen = st_init_gen(distanceTable);
02024         if (stGen == NULL) goto outOfMem;
02025         while(st_gen(stGen, (char **)&key, (char **)&value)) {
02026             FREE(value);
02027         }
02028         st_free_gen(stGen); stGen = NULL;
02029         st_free_table(distanceTable);
02030         return(1);
02031     }
02032 
02033     /* record the maximum local reference count */
02034     maxLocalRef = 0;
02035     stGen = st_init_gen(distanceTable);
02036     if (stGen == NULL) goto outOfMem;
02037     while(st_gen(stGen, (char **)&key, (char **)&value)) {
02038         nodeStat = (NodeStat *)value;
02039         maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
02040             nodeStat->localRef : maxLocalRef;
02041     }
02042     st_free_gen(stGen); stGen = NULL;
02043 
02044             
02045     /* Count minterms for each node. */
02046     max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
02047     mintermTable = st_init_table(st_ptrcmp,st_ptrhash);
02048     if (mintermTable == NULL) goto outOfMem;
02049     minterms = CountMinterms(f, max, mintermTable, dd->err);
02050     if (minterms == -1.0) goto outOfMem;
02051     
02052     lastTimeG = Cudd_Random() & 1;
02053     cacheTable = st_init_table(st_ptrcmp, st_ptrhash);
02054     if (cacheTable == NULL) goto outOfMem;
02055     ghTable = st_init_table(st_ptrcmp, st_ptrhash);
02056     if (ghTable == NULL) goto outOfMem;
02057 
02058     /* Build conjuncts. */
02059     factors = BuildConjuncts(dd, f, distanceTable, cacheTable,
02060                              approxDistance, maxLocalRef, ghTable, mintermTable);
02061     if (factors == NULL) goto outOfMem;
02062 
02063     /* free up tables */
02064     stGen = st_init_gen(distanceTable);
02065     if (stGen == NULL) goto outOfMem;
02066     while(st_gen(stGen, (char **)&key, (char **)&value)) {
02067         FREE(value);
02068     }
02069     st_free_gen(stGen); stGen = NULL;
02070     st_free_table(distanceTable); distanceTable = NULL;
02071     st_free_table(ghTable); ghTable = NULL;
02072     
02073     stGen = st_init_gen(mintermTable);
02074     if (stGen == NULL) goto outOfMem;
02075     while(st_gen(stGen, (char **)&key, (char **)&value)) {
02076         FREE(value);
02077     }
02078     st_free_gen(stGen); stGen = NULL;
02079     st_free_table(mintermTable); mintermTable = NULL;
02080 
02081     freeFactors = FactorsNotStored(factors);
02082     factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
02083     if (factors != NULL) {
02084         *c1 = factors->g;
02085         *c2 = factors->h;
02086         cuddRef(*c1);
02087         cuddRef(*c2);
02088         if (freeFactors) FREE(factors);
02089         
02090 #if 0    
02091         if ((*c1 == f) && (!Cudd_IsConstant(f))) {
02092             assert(*c2 == one);
02093         }
02094         if ((*c2 == f) && (!Cudd_IsConstant(f))) {
02095             assert(*c1 == one);
02096         }
02097         
02098         if ((*c1 != one) && (!Cudd_IsConstant(f))) {
02099             assert(!Cudd_bddLeq(dd, *c2, *c1));
02100         }
02101         if ((*c2 != one) && (!Cudd_IsConstant(f))) {
02102             assert(!Cudd_bddLeq(dd, *c1, *c2));
02103         }
02104 #endif
02105     }
02106 
02107     stGen = st_init_gen(cacheTable);
02108     if (stGen == NULL) goto outOfMem;
02109     while(st_gen(stGen, (char **)&key, (char **)&value)) {
02110         ConjunctsFree(dd, (Conjuncts *)value);
02111     }
02112     st_free_gen(stGen); stGen = NULL;
02113 
02114     st_free_table(cacheTable); cacheTable = NULL;
02115 
02116     return(1);
02117 
02118 outOfMem:
02119     if (distanceTable != NULL) {
02120         stGen = st_init_gen(distanceTable);
02121         if (stGen == NULL) goto outOfMem;
02122         while(st_gen(stGen, (char **)&key, (char **)&value)) {
02123             FREE(value);
02124         }
02125         st_free_gen(stGen); stGen = NULL;
02126         st_free_table(distanceTable); distanceTable = NULL;
02127     }
02128     if (mintermTable != NULL) {
02129         stGen = st_init_gen(mintermTable);
02130         if (stGen == NULL) goto outOfMem;
02131         while(st_gen(stGen, (char **)&key, (char **)&value)) {
02132             FREE(value);
02133         }
02134         st_free_gen(stGen); stGen = NULL;
02135         st_free_table(mintermTable); mintermTable = NULL;
02136     }
02137     if (ghTable != NULL) st_free_table(ghTable);
02138     if (cacheTable != NULL) {
02139         stGen = st_init_gen(cacheTable);
02140         if (stGen == NULL) goto outOfMem;
02141         while(st_gen(stGen, (char **)&key, (char **)&value)) {
02142             ConjunctsFree(dd, (Conjuncts *)value);
02143         }
02144         st_free_gen(stGen); stGen = NULL;
02145         st_free_table(cacheTable); cacheTable = NULL;
02146     }
02147     dd->errorCode = CUDD_MEMORY_OUT;
02148     return(0);
02149 
02150 } /* end of cuddConjunctsAux */

static int PairInTables ( DdNode *  g,
DdNode *  h,
st_table *  ghTable 
) [static]

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

Synopsis [Check whether the given pair is in the tables.]

Description [.Check whether the given pair is in the tables. gTable and hTable are combined. absence in both is indicated by 0, presence in gTable is indicated by 1, presence in hTable by 2 and presence in both by 3. The values returned by this function are PAIR_ST, PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE. PAIR_ST implies g in gTable and h in hTable PAIR_CR implies g in hTable and h in gTable G_ST implies g in gTable and h not in any table G_CR implies g in hTable and h not in any table H_ST implies h in hTable and g not in any table H_CR implies h in gTable and g not in any table BOTH_G implies both in gTable BOTH_H implies both in hTable NONE implies none in table; ]

SideEffects []

SeeAlso [CheckTablesCacheAndReturn CheckInTables]

Definition at line 913 of file cuddDecomp.c.

00917 {
00918     int valueG, valueH, gPresent, hPresent;
00919 
00920     valueG = valueH = gPresent = hPresent = 0;
00921     
00922     gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
00923     hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
00924 
00925     if (!gPresent && !hPresent) return(NONE);
00926 
00927     if (!hPresent) {
00928         if (valueG & 1) return(G_ST);
00929         if (valueG & 2) return(G_CR);
00930     }
00931     if (!gPresent) {
00932         if (valueH & 1) return(H_CR);
00933         if (valueH & 2) return(H_ST);
00934     }
00935     /* both in tables */
00936     if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
00937     if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
00938     
00939     if (valueG & 1) {
00940         return(BOTH_G);
00941     } else {
00942         return(BOTH_H);
00943     }
00944     
00945 } /* end of PairInTables */

static Conjuncts* PickOnePair ( DdNode *  node,
DdNode *  g1,
DdNode *  h1,
DdNode *  g2,
DdNode *  h2,
st_table *  ghTable,
st_table *  cacheTable 
) [static]

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

Synopsis [Check the tables for the existence of pair and return one combination, store in cache.]

Description [Check the tables for the existence of pair and return one combination, store in cache. The pair that has more pointers to it is picked. An approximation of the number of local pointers is made by taking the reference count of the pairs sent. ]

SideEffects []

SeeAlso [ZeroCase BuildConjuncts]

Definition at line 1068 of file cuddDecomp.c.

01076 {
01077     int value;
01078     Conjuncts *factors;
01079     int oneRef, twoRef;
01080     
01081     factors = ALLOC(Conjuncts, 1);
01082     if (factors == NULL) return(NULL);
01083 
01084     /* count the number of pointers to pair 2 */
01085     if (h2 == one) {
01086         twoRef = (Cudd_Regular(g2))->ref;
01087     } else if (g2 == one) {
01088         twoRef = (Cudd_Regular(h2))->ref;
01089     } else {
01090         twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
01091     }
01092 
01093     /* count the number of pointers to pair 1 */
01094     if (h1 == one) {
01095         oneRef  = (Cudd_Regular(g1))->ref;
01096     } else if (g1 == one) {
01097         oneRef  = (Cudd_Regular(h1))->ref;
01098     } else {
01099         oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
01100     }
01101 
01102     /* pick the pair with higher reference count */
01103     if (oneRef >= twoRef) {
01104         factors->g = g1;
01105         factors->h = h1;
01106     } else {
01107         factors->g = g2;
01108         factors->h = h2;
01109     }
01110     
01111     /*
01112      * Store computed factors in respective tables to encourage
01113      * recombination.
01114      */
01115     if (factors->g != one) {
01116         /* insert g in htable */
01117         value = 0;
01118         if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
01119             if (value == 2) {
01120                 value |= 1;
01121                 if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
01122                               (char *)(long)value) == ST_OUT_OF_MEM) {
01123                     FREE(factors);
01124                     return(NULL);
01125                 }
01126             }
01127         } else {
01128             value = 1;
01129             if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
01130                           (char *)(long)value) == ST_OUT_OF_MEM) {
01131                 FREE(factors);
01132                 return(NULL);
01133             }
01134         }
01135     }
01136 
01137     if (factors->h != one) {
01138         /* insert h in htable */
01139         value = 0;
01140         if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
01141             if (value == 1) {
01142                 value |= 2;
01143                 if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
01144                               (char *)(long)value) == ST_OUT_OF_MEM) {
01145                     FREE(factors);
01146                     return(NULL);
01147                 }
01148             }       
01149         } else {
01150             value = 2;
01151             if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
01152                           (char *)(long)value) == ST_OUT_OF_MEM) {
01153                 FREE(factors);
01154                 return(NULL);
01155             }
01156         }
01157     }
01158     
01159     /* Store factors in cache table for later use. */
01160     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
01161             ST_OUT_OF_MEM) {
01162         FREE(factors);
01163         return(NULL);
01164     }
01165 
01166     return(factors);
01167 
01168 } /* end of PickOnePair */

static Conjuncts* ZeroCase ( DdManager *  dd,
DdNode *  node,
Conjuncts *  factorsNv,
st_table *  ghTable,
st_table *  cacheTable,
int  switched 
) [static]

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

Synopsis [If one child is zero, do explicitly what Restrict does or better]

Description [If one child is zero, do explicitly what Restrict does or better. First separate a variable and its child in the base case. In case of a cube times a function, separate the cube and function. As a last resort, look in tables.]

SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed because it is freed above.]

SeeAlso [BuildConjuncts]

Definition at line 1416 of file cuddDecomp.c.

01423 {
01424     int topid;
01425     DdNode *g, *h, *g1, *g2, *h1, *h2, *x, *N, *G, *H, *Gv, *Gnv;
01426     DdNode *Hv, *Hnv;
01427     int value;
01428     int outOfMem;
01429     Conjuncts *factors;
01430     
01431     /* get var at this node */
01432     N = Cudd_Regular(node);
01433     topid = N->index;
01434     x = dd->vars[topid];
01435     x = (switched) ? Cudd_Not(x): x;
01436     cuddRef(x);
01437 
01438     /* Seprate variable and child */
01439     if (factorsNv->g == one) {
01440         Cudd_RecursiveDeref(dd, factorsNv->g);
01441         factors = ALLOC(Conjuncts, 1);
01442         if (factors == NULL) {
01443             dd->errorCode = CUDD_MEMORY_OUT;
01444             Cudd_RecursiveDeref(dd, factorsNv->h);
01445             Cudd_RecursiveDeref(dd, x);
01446             return(NULL);
01447         }
01448         factors->g = x;
01449         factors->h = factorsNv->h;
01450         /* cache the result*/
01451         if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
01452             dd->errorCode = CUDD_MEMORY_OUT;
01453             Cudd_RecursiveDeref(dd, factorsNv->h); 
01454             Cudd_RecursiveDeref(dd, x);
01455             FREE(factors);
01456             return NULL;
01457         }
01458         
01459         /* store  x in g table, the other node is already in the table */
01460         if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
01461             value |= 1;
01462         } else {
01463             value = 1;
01464         }
01465         if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
01466             dd->errorCode = CUDD_MEMORY_OUT;
01467             return NULL;
01468         }
01469         return(factors);
01470     }
01471     
01472     /* Seprate variable and child */
01473     if (factorsNv->h == one) {
01474         Cudd_RecursiveDeref(dd, factorsNv->h);
01475         factors = ALLOC(Conjuncts, 1);
01476         if (factors == NULL) {
01477             dd->errorCode = CUDD_MEMORY_OUT;
01478             Cudd_RecursiveDeref(dd, factorsNv->g);
01479             Cudd_RecursiveDeref(dd, x);
01480             return(NULL);
01481         }
01482         factors->g = factorsNv->g;
01483         factors->h = x;
01484         /* cache the result. */
01485         if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
01486             dd->errorCode = CUDD_MEMORY_OUT;
01487             Cudd_RecursiveDeref(dd, factorsNv->g);
01488             Cudd_RecursiveDeref(dd, x);
01489             FREE(factors);
01490             return(NULL);
01491         }
01492         /* store x in h table,  the other node is already in the table */
01493         if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
01494             value |= 2;
01495         } else {
01496             value = 2;
01497         }
01498         if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
01499             dd->errorCode = CUDD_MEMORY_OUT;
01500             return NULL;
01501         }
01502         return(factors);
01503     }
01504 
01505     G = Cudd_Regular(factorsNv->g);
01506     Gv = cuddT(G);
01507     Gnv = cuddE(G);
01508     Gv = Cudd_NotCond(Gv, Cudd_IsComplement(node));
01509     Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node));
01510     /* if the child below is a variable */
01511     if ((Gv == zero) || (Gnv == zero)) {
01512         h = factorsNv->h;
01513         g = cuddBddAndRecur(dd, x, factorsNv->g);
01514         if (g != NULL)  cuddRef(g);
01515         Cudd_RecursiveDeref(dd, factorsNv->g); 
01516         Cudd_RecursiveDeref(dd, x);
01517         if (g == NULL) {
01518             Cudd_RecursiveDeref(dd, factorsNv->h); 
01519             return NULL;
01520         }
01521         /* CheckTablesCacheAndReturn responsible for allocating
01522          * factors structure., g,h referenced for cache store  the
01523          */
01524         factors = CheckTablesCacheAndReturn(node,
01525                                             g,
01526                                             h,
01527                                             ghTable,
01528                                             cacheTable);
01529         if (factors == NULL) {
01530             dd->errorCode = CUDD_MEMORY_OUT;
01531             Cudd_RecursiveDeref(dd, g);
01532             Cudd_RecursiveDeref(dd, h);
01533         }
01534         return(factors); 
01535     }
01536 
01537     H = Cudd_Regular(factorsNv->h);
01538     Hv = cuddT(H);
01539     Hnv = cuddE(H);
01540     Hv = Cudd_NotCond(Hv, Cudd_IsComplement(node));
01541     Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node));
01542     /* if the child below is a variable */
01543     if ((Hv == zero) || (Hnv == zero)) {
01544         g = factorsNv->g;
01545         h = cuddBddAndRecur(dd, x, factorsNv->h);
01546         if (h!= NULL) cuddRef(h);
01547         Cudd_RecursiveDeref(dd, factorsNv->h);
01548         Cudd_RecursiveDeref(dd, x);
01549         if (h == NULL) {
01550             Cudd_RecursiveDeref(dd, factorsNv->g);
01551             return NULL;
01552         }
01553         /* CheckTablesCacheAndReturn responsible for allocating
01554          * factors structure.g,h referenced for table store 
01555          */
01556         factors = CheckTablesCacheAndReturn(node,
01557                                             g,
01558                                             h,
01559                                             ghTable,
01560                                             cacheTable);
01561         if (factors == NULL) {
01562             dd->errorCode = CUDD_MEMORY_OUT;
01563             Cudd_RecursiveDeref(dd, g);
01564             Cudd_RecursiveDeref(dd, h);
01565         }
01566         return(factors); 
01567     }
01568 
01569     /* build g1 = x*g; h1 = h */
01570     /* build g2 = g; h2 = x*h */
01571     Cudd_RecursiveDeref(dd, x);
01572     h1 = factorsNv->h;
01573     g1 = cuddBddAndRecur(dd, x, factorsNv->g);
01574     if (g1 != NULL) cuddRef(g1);
01575     if (g1 == NULL) {
01576         Cudd_RecursiveDeref(dd, factorsNv->g); 
01577         Cudd_RecursiveDeref(dd, factorsNv->h);
01578         return NULL;
01579     }
01580     
01581     g2 = factorsNv->g;
01582     h2 = cuddBddAndRecur(dd, x, factorsNv->h);
01583     if (h2 != NULL) cuddRef(h2);
01584     if (h2 == NULL) {
01585         Cudd_RecursiveDeref(dd, factorsNv->h);
01586         Cudd_RecursiveDeref(dd, factorsNv->g);
01587         return NULL;
01588     }
01589 
01590     /* check whether any pair is in tables */
01591     factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
01592     if (outOfMem) {
01593         dd->errorCode = CUDD_MEMORY_OUT;
01594         Cudd_RecursiveDeref(dd, g1);
01595         Cudd_RecursiveDeref(dd, h1);
01596         Cudd_RecursiveDeref(dd, g2);
01597         Cudd_RecursiveDeref(dd, h2);
01598         return NULL;
01599     }
01600     if (factors != NULL) {
01601         if ((factors->g == g1) || (factors->g == h1)) {
01602             Cudd_RecursiveDeref(dd, g2);
01603             Cudd_RecursiveDeref(dd, h2);
01604         } else {
01605             Cudd_RecursiveDeref(dd, g1);
01606             Cudd_RecursiveDeref(dd, h1);
01607         }
01608         return factors;
01609     }
01610 
01611     /* check for each pair in tables and choose one */
01612     factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
01613     if (factors == NULL) {
01614         dd->errorCode = CUDD_MEMORY_OUT;
01615         Cudd_RecursiveDeref(dd, g1);
01616         Cudd_RecursiveDeref(dd, h1);
01617         Cudd_RecursiveDeref(dd, g2);
01618         Cudd_RecursiveDeref(dd, h2);
01619     } else {
01620         /* now free what was created and not used */
01621         if ((factors->g == g1) || (factors->g == h1)) {
01622             Cudd_RecursiveDeref(dd, g2);
01623             Cudd_RecursiveDeref(dd, h2);
01624         } else {
01625             Cudd_RecursiveDeref(dd, g1);
01626             Cudd_RecursiveDeref(dd, h1);
01627         }
01628     }
01629         
01630     return(factors);
01631 } /* end of ZeroCase */

Variable Documentation

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

Definition at line 78 of file cuddDecomp.c.

long lastTimeG

Definition at line 82 of file cuddDecomp.c.

DdNode* one [static]

Definition at line 81 of file cuddDecomp.c.

DdNode * zero [static]

Definition at line 81 of file cuddDecomp.c.

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