src/cuBdd/cuddDecomp.c File Reference

#include "util.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 (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)
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)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $"
static DdNode * one
static DdNode * zero
long lastTimeG

Define Documentation

#define BOTH_G   7

Definition at line 79 of file cuddDecomp.c.

#define BOTH_H   8

Definition at line 80 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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

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

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

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

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

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

Definition at line 70 of file cuddDecomp.c.

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

Definition at line 118 of file cuddDecomp.c.

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

Definition at line 116 of file cuddDecomp.c.

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

Definition at line 120 of file cuddDecomp.c.

#define G_CR   4

Definition at line 76 of file cuddDecomp.c.

#define G_ST   3

Definition at line 75 of file cuddDecomp.c.

#define H_CR   6

Definition at line 78 of file cuddDecomp.c.

#define H_ST   5

Definition at line 77 of file cuddDecomp.c.

#define NONE   0

Definition at line 72 of file cuddDecomp.c.

#define PAIR_CR   2

Definition at line 74 of file cuddDecomp.c.

#define PAIR_ST   1

Definition at line 73 of file cuddDecomp.c.

#define THRESHOLD   10

Definition at line 71 of file cuddDecomp.c.

Function Documentation

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 1681 of file cuddDecomp.c.

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

01222 {
01223     int pairValue1,  pairValue2;
01224     Conjuncts *factors;
01225     int value;
01226     
01227     *outOfMem = 0;
01228 
01229     /* check existence of pair in table */
01230     pairValue1 = PairInTables(g1, h1, ghTable);
01231     pairValue2 = PairInTables(g2, h2, ghTable);
01232 
01233     /* if none of the 4 exist in the gh tables, return NULL */
01234     if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
01235         return NULL;
01236     }
01237     
01238     factors = ALLOC(Conjuncts, 1);
01239     if (factors == NULL) {
01240         *outOfMem = 1;
01241         return NULL;
01242     }
01243 
01244     /* pairs that already exist in the table get preference. */
01245     if (pairValue1 == PAIR_ST) {
01246         factors->g = g1;
01247         factors->h = h1;
01248     } else if (pairValue2 == PAIR_ST) {
01249         factors->g = g2;
01250         factors->h = h2;
01251     } else if (pairValue1 == PAIR_CR) {
01252         factors->g = h1;
01253         factors->h = g1;
01254     } else if (pairValue2 == PAIR_CR) {
01255         factors->g = h2;
01256         factors->h = g2;
01257     } else if (pairValue1 == G_ST) {
01258         /* g exists in the table, h is not found in either table */
01259         factors->g = g1;
01260         factors->h = h1;
01261         if (h1 != one) {
01262             value = 2;
01263             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
01264                           (char *)(long)value) == ST_OUT_OF_MEM) {
01265                 *outOfMem = 1;
01266                 FREE(factors);
01267                 return(NULL);
01268             }
01269         }
01270     } else if (pairValue1 == BOTH_G) {
01271         /* g and h are  found in the g table */
01272         factors->g = g1;
01273         factors->h = h1;
01274         if (h1 != one) {
01275             value = 3;
01276             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
01277                           (char *)(long)value) == ST_OUT_OF_MEM) {
01278                 *outOfMem = 1;
01279                 FREE(factors);
01280                 return(NULL);
01281             }
01282         }
01283     } else if (pairValue1 == H_ST) {
01284         /* h exists in the table, g is not found in either table */
01285         factors->g = g1;
01286         factors->h = h1;
01287         if (g1 != one) {
01288             value = 1;
01289             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
01290                           (char *)(long)value) == ST_OUT_OF_MEM) {
01291                 *outOfMem = 1;
01292                 FREE(factors);
01293                 return(NULL);
01294             }
01295         }
01296     } else if (pairValue1 == BOTH_H) {
01297         /* g and h are  found in the h table */
01298         factors->g = g1;
01299         factors->h = h1;
01300         if (g1 != one) {
01301             value = 3;
01302             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
01303                           (char *)(long)value) == ST_OUT_OF_MEM) {
01304                 *outOfMem = 1;
01305                 FREE(factors);
01306                 return(NULL);
01307             }
01308         }
01309     } else if (pairValue2 == G_ST) {
01310         /* g exists in the table, h is not found in either table */
01311         factors->g = g2;
01312         factors->h = h2;
01313         if (h2 != one) {
01314             value = 2;
01315             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
01316                           (char *)(long)value) == ST_OUT_OF_MEM) {
01317                 *outOfMem = 1;
01318                 FREE(factors);
01319                 return(NULL);
01320             }
01321         }
01322     } else if  (pairValue2 == BOTH_G) {
01323         /* g and h are  found in the g table */
01324         factors->g = g2;
01325         factors->h = h2;
01326         if (h2 != one) {
01327             value = 3;
01328             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
01329                           (char *)(long)value) == ST_OUT_OF_MEM) {
01330                 *outOfMem = 1;
01331                 FREE(factors);
01332                 return(NULL);
01333             }
01334         }
01335     } else if (pairValue2 == H_ST) { 
01336         /* h exists in the table, g is not found in either table */
01337         factors->g = g2;
01338         factors->h = h2;
01339         if (g2 != one) {
01340             value = 1;
01341             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
01342                           (char *)(long)value) == ST_OUT_OF_MEM) {
01343                 *outOfMem = 1;
01344                 FREE(factors);
01345                 return(NULL);
01346             }
01347         }
01348     } else if (pairValue2 == BOTH_H) {
01349         /* g and h are  found in the h table */
01350         factors->g = g2;
01351         factors->h = h2;
01352         if (g2 != one) {
01353             value = 3;
01354             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
01355                           (char *)(long)value) == ST_OUT_OF_MEM) {
01356                 *outOfMem = 1;
01357                 FREE(factors);
01358                 return(NULL);
01359             }
01360         }
01361     } else if (pairValue1 == G_CR) {
01362         /* g found in h table and h in none */
01363         factors->g = h1;
01364         factors->h = g1;
01365         if (h1 != one) {
01366             value = 1;
01367             if (st_insert(ghTable, (char *)Cudd_Regular(h1),
01368                           (char *)(long)value) == ST_OUT_OF_MEM) {
01369                 *outOfMem = 1;
01370                 FREE(factors);
01371                 return(NULL);
01372             }
01373         }
01374     } else if (pairValue1 == H_CR) {
01375         /* h found in g table and g in none */
01376         factors->g = h1;
01377         factors->h = g1;
01378         if (g1 != one) {
01379             value = 2;
01380             if (st_insert(ghTable, (char *)Cudd_Regular(g1),
01381                           (char *)(long)value) == ST_OUT_OF_MEM) {
01382                 *outOfMem = 1;
01383                 FREE(factors);
01384                 return(NULL);
01385             }
01386         }
01387     } else if (pairValue2 == G_CR) {
01388         /* g found in h table and h in none */
01389         factors->g = h2;
01390         factors->h = g2;
01391         if (h2 != one) {
01392             value = 1;
01393             if (st_insert(ghTable, (char *)Cudd_Regular(h2),
01394                           (char *)(long)value) == ST_OUT_OF_MEM) {
01395                 *outOfMem = 1;
01396                 FREE(factors);
01397                 return(NULL);
01398             }
01399         }
01400     } else if (pairValue2 == H_CR) {
01401         /* h found in g table and g in none */
01402         factors->g = h2;
01403         factors->h = g2;
01404         if (g2 != one) {
01405             value = 2;
01406             if (st_insert(ghTable, (char *)Cudd_Regular(g2),
01407                           (char *)(long)value) == ST_OUT_OF_MEM) {
01408                 *outOfMem = 1;
01409                 FREE(factors);
01410                 return(NULL);
01411             }
01412         }
01413     }
01414     
01415     /* Store factors in cache table for later use. */
01416     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
01417             ST_OUT_OF_MEM) {
01418         *outOfMem = 1;
01419         FREE(factors);
01420         return(NULL);
01421     }
01422     return factors;
01423 } /* 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 990 of file cuddDecomp.c.

00996 {
00997     int pairValue;
00998     int value;
00999     Conjuncts *factors;
01000     
01001     value = 0;
01002     /* check tables */
01003     pairValue = PairInTables(g, h, ghTable);
01004     assert(pairValue != NONE);
01005     /* if both dont exist in table, we know one exists(either g or h).
01006      * Therefore store the other and proceed
01007      */
01008     factors = ALLOC(Conjuncts, 1);
01009     if (factors == NULL) return(NULL);
01010     if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
01011         if (g != one) {
01012             value = 0;
01013             if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
01014                 value |= 1;
01015             } else {
01016                 value = 1;
01017             }
01018             if (st_insert(ghTable, (char *)Cudd_Regular(g),
01019                           (char *)(long)value) == ST_OUT_OF_MEM) {
01020                 return(NULL);
01021             }
01022         }
01023         factors->g = g;
01024         factors->h = h;
01025     } else  if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
01026         if (h != one) {
01027             value = 0;
01028             if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
01029                 value |= 2;
01030             } else {
01031                 value = 2;
01032             }
01033             if (st_insert(ghTable, (char *)Cudd_Regular(h),
01034                           (char *)(long)value) == ST_OUT_OF_MEM) {
01035                 return(NULL);
01036             }
01037         }
01038         factors->g = g;
01039         factors->h = h;
01040     } else if (pairValue == H_CR) {
01041         if (g != one) {
01042             value = 2;
01043             if (st_insert(ghTable, (char *)Cudd_Regular(g),
01044                           (char *)(long)value) == ST_OUT_OF_MEM) {
01045                 return(NULL);
01046             }
01047         }
01048         factors->g = h;
01049         factors->h = g;
01050     } else if (pairValue == G_CR) {
01051         if (h != one) {
01052             value = 1;
01053             if (st_insert(ghTable, (char *)Cudd_Regular(h),
01054                           (char *)(long)value) == ST_OUT_OF_MEM) {
01055                 return(NULL);
01056             }
01057         }
01058         factors->g = h;
01059         factors->h = g;
01060     } else if (pairValue == PAIR_CR) {
01061     /* pair exists in table */
01062         factors->g = h;
01063         factors->h = g;
01064     } else if (pairValue == PAIR_ST) {
01065         factors->g = g;
01066         factors->h = h;
01067     }
01068             
01069     /* cache the result for this node */
01070     if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
01071         FREE(factors);
01072         return(NULL);
01073     }
01074 
01075     return(factors);
01076 
01077 } /* end of CheckTablesCacheAndReturn */

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

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

Synopsis [Free factors structure]

Description []

SideEffects [None]

SeeAlso []

Definition at line 900 of file cuddDecomp.c.

00903 {
00904     Cudd_RecursiveDeref(dd, factors->g);
00905     Cudd_RecursiveDeref(dd, factors->h);
00906     FREE(factors);
00907     return;
00908 
00909 } /* 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 837 of file cuddDecomp.c.

00842 {
00843     DdNode *N, *Nv, *Nnv;
00844     double min, minNv, minNnv;
00845     double *dummy;
00846 
00847     N = Cudd_Regular(node);
00848 
00849     if (cuddIsConstant(N)) {
00850         if (node == zero) {
00851             return(0);
00852         } else {
00853             return(max);
00854         }
00855     }
00856 
00857     /* Return the entry in the table if found. */
00858     if (st_lookup(mintermTable, node, &dummy)) {
00859         min = *dummy;
00860         return(min);
00861     }
00862 
00863     Nv = cuddT(N);
00864     Nnv = cuddE(N);
00865     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
00866     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
00867 
00868     /* Recur on the children. */
00869     minNv = CountMinterms(Nv, max, mintermTable, fp);
00870     if (minNv == -1.0) return(-1.0);
00871     minNnv = CountMinterms(Nnv, max, mintermTable, fp);
00872     if (minNnv == -1.0) return(-1.0);
00873     min = minNv / 2.0 + minNnv / 2.0;
00874     /* store 
00875      */
00876 
00877     dummy = ALLOC(double, 1);
00878     if (dummy == NULL) return(-1.0);
00879     *dummy = min;
00880     if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
00881         (void) fprintf(fp, "st table insert failed\n");
00882     }
00883     return(min);
00884 
00885 } /* end of CountMinterms */

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

AutomaticStart

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 768 of file cuddDecomp.c.

00771 {
00772     DdNode *N, *Nv, *Nnv;
00773     int distance, distanceNv, distanceNnv;
00774     NodeStat *nodeStat, *nodeStatNv, *nodeStatNnv;
00775 
00776 #if 0
00777     if (Cudd_IsConstant(node)) {
00778         return(0);
00779     }
00780 #endif
00781     
00782     /* Return the entry in the table if found. */
00783     N = Cudd_Regular(node);
00784     if (st_lookup(distanceTable, N, &nodeStat)) {
00785         nodeStat->localRef++;
00786         return(nodeStat);
00787     }
00788 
00789     Nv = cuddT(N);
00790     Nnv = cuddE(N);
00791     Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
00792     Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
00793 
00794     /* Recur on the children. */
00795     nodeStatNv = CreateBotDist(Nv, distanceTable);
00796     if (nodeStatNv == NULL) return(NULL);
00797     distanceNv = nodeStatNv->distance;
00798 
00799     nodeStatNnv = CreateBotDist(Nnv, distanceTable);
00800     if (nodeStatNnv == NULL) return(NULL);
00801     distanceNnv = nodeStatNnv->distance;
00802     /* Store max distance from constant; note sometimes this distance
00803     ** may be to 0.
00804     */
00805     distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);
00806 
00807     nodeStat = ALLOC(NodeStat, 1);
00808     if (nodeStat == NULL) {
00809         return(0);
00810     }
00811     nodeStat->distance = distance;
00812     nodeStat->localRef = 1;
00813     
00814     if (st_insert(distanceTable, (char *)N, (char *)nodeStat) ==
00815         ST_OUT_OF_MEM) {
00816         return(0);
00817 
00818     }
00819     return(nodeStat);
00820 
00821 } /* 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 171 of file cuddDecomp.c.

00175 {
00176     DdNode *superset1, *superset2, *glocal, *hlocal;
00177     int nvars = Cudd_SupportSize(dd,f);
00178 
00179     /* Find a tentative first factor by overapproximation and minimization. */
00180     superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0);
00181     if (superset1 == NULL) return(0);
00182     cuddRef(superset1);
00183     superset2 = Cudd_bddSqueeze(dd,f,superset1);
00184     if (superset2 == NULL) {
00185         Cudd_RecursiveDeref(dd,superset1);
00186         return(0);
00187     }
00188     cuddRef(superset2);
00189     Cudd_RecursiveDeref(dd,superset1);
00190 
00191     /* Compute the second factor by minimization. */
00192     hlocal = Cudd_bddLICompaction(dd,f,superset2);
00193     if (hlocal == NULL) {
00194         Cudd_RecursiveDeref(dd,superset2);
00195         return(0);
00196     }
00197     cuddRef(hlocal);
00198 
00199     /* Refine the first factor by minimization. If h turns out to be f, this
00200     ** step guarantees that g will be 1. */
00201     glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
00202     if (glocal == NULL) {
00203         Cudd_RecursiveDeref(dd,superset2);
00204         Cudd_RecursiveDeref(dd,hlocal);
00205         return(0);
00206     }
00207     cuddRef(glocal);
00208     Cudd_RecursiveDeref(dd,superset2);
00209 
00210     if (glocal != DD_ONE(dd)) {
00211         if (hlocal != DD_ONE(dd)) {
00212             *conjuncts = ALLOC(DdNode *,2);
00213             if (*conjuncts == NULL) {
00214                 Cudd_RecursiveDeref(dd,glocal);
00215                 Cudd_RecursiveDeref(dd,hlocal);
00216                 dd->errorCode = CUDD_MEMORY_OUT;
00217                 return(0);
00218             }
00219             (*conjuncts)[0] = glocal;
00220             (*conjuncts)[1] = hlocal;
00221             return(2);
00222         } else {
00223             Cudd_RecursiveDeref(dd,hlocal);
00224             *conjuncts = ALLOC(DdNode *,1);
00225             if (*conjuncts == NULL) {
00226                 Cudd_RecursiveDeref(dd,glocal);
00227                 dd->errorCode = CUDD_MEMORY_OUT;
00228                 return(0);
00229             }
00230             (*conjuncts)[0] = glocal;
00231             return(1);
00232         }
00233     } else {
00234         Cudd_RecursiveDeref(dd,glocal);
00235         *conjuncts = ALLOC(DdNode *,1);
00236         if (*conjuncts == NULL) {
00237             Cudd_RecursiveDeref(dd,hlocal);
00238             dd->errorCode = CUDD_MEMORY_OUT;
00239             return(0);
00240         }
00241         (*conjuncts)[0] = hlocal;
00242         return(1);
00243     }
00244 
00245 } /* 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 269 of file cuddDecomp.c.

00273 {
00274     int result, i;
00275 
00276     result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
00277     for (i = 0; i < result; i++) {
00278         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00279     }
00280     return(result);
00281 
00282 } /* 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 492 of file cuddDecomp.c.

00496 {
00497     int result;
00498     DdNode *glocal, *hlocal;
00499 
00500     one = DD_ONE(dd);
00501     zero = Cudd_Not(one);
00502     
00503     do {
00504         dd->reordered = 0;
00505         result = cuddConjunctsAux(dd, f, &glocal, &hlocal);
00506     } while (dd->reordered == 1);
00507 
00508     if (result == 0) {
00509         return(0);
00510     }
00511 
00512     if (glocal != one) {
00513         if (hlocal != one) {
00514             *conjuncts = ALLOC(DdNode *,2);
00515             if (*conjuncts == NULL) {
00516                 Cudd_RecursiveDeref(dd,glocal);
00517                 Cudd_RecursiveDeref(dd,hlocal);
00518                 dd->errorCode = CUDD_MEMORY_OUT;
00519                 return(0);
00520             }
00521             (*conjuncts)[0] = glocal;
00522             (*conjuncts)[1] = hlocal;
00523             return(2);
00524         } else {
00525             Cudd_RecursiveDeref(dd,hlocal);
00526             *conjuncts = ALLOC(DdNode *,1);
00527             if (*conjuncts == NULL) {
00528                 Cudd_RecursiveDeref(dd,glocal);
00529                 dd->errorCode = CUDD_MEMORY_OUT;
00530                 return(0);
00531             }
00532             (*conjuncts)[0] = glocal;
00533             return(1);
00534         }
00535     } else {
00536         Cudd_RecursiveDeref(dd,glocal);
00537         *conjuncts = ALLOC(DdNode *,1);
00538         if (*conjuncts == NULL) {
00539             Cudd_RecursiveDeref(dd,hlocal);
00540             dd->errorCode = CUDD_MEMORY_OUT;
00541             return(0);
00542         }
00543         (*conjuncts)[0] = hlocal;
00544         return(1);
00545     }
00546 
00547 } /* 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 571 of file cuddDecomp.c.

00575 {
00576     int result, i;
00577 
00578     result = Cudd_bddGenConjDecomp(dd,Cudd_Not(f),disjuncts);
00579     for (i = 0; i < result; i++) {
00580         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00581     }
00582     return(result);
00583 
00584 } /* 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 309 of file cuddDecomp.c.

00313 {
00314     DdNode *superset1, *superset2, *old[2], *res[2];
00315     int sizeOld, sizeNew;
00316     int nvars = Cudd_SupportSize(dd,f);
00317 
00318     old[0] = DD_ONE(dd);
00319     cuddRef(old[0]);
00320     old[1] = f;
00321     cuddRef(old[1]);
00322     sizeOld = Cudd_SharingSize(old,2);
00323 
00324     do {
00325         /* Find a tentative first factor by overapproximation and
00326         ** minimization. */
00327         superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
00328         if (superset1 == NULL) {
00329             Cudd_RecursiveDeref(dd,old[0]);
00330             Cudd_RecursiveDeref(dd,old[1]);
00331             return(0);
00332         }
00333         cuddRef(superset1);
00334         superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
00335         if (superset2 == NULL) {
00336             Cudd_RecursiveDeref(dd,old[0]);
00337             Cudd_RecursiveDeref(dd,old[1]);
00338             Cudd_RecursiveDeref(dd,superset1);
00339             return(0);
00340         }
00341         cuddRef(superset2);
00342         Cudd_RecursiveDeref(dd,superset1);
00343         res[0] = Cudd_bddAnd(dd,old[0],superset2);
00344         if (res[0] == NULL) {
00345             Cudd_RecursiveDeref(dd,superset2);
00346             Cudd_RecursiveDeref(dd,old[0]);
00347             Cudd_RecursiveDeref(dd,old[1]);
00348             return(0);
00349         }
00350         cuddRef(res[0]);
00351         Cudd_RecursiveDeref(dd,superset2);
00352         if (res[0] == old[0]) {
00353             Cudd_RecursiveDeref(dd,res[0]);
00354             break;      /* avoid infinite loop */
00355         }
00356 
00357         /* Compute the second factor by minimization. */
00358         res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
00359         if (res[1] == NULL) {
00360             Cudd_RecursiveDeref(dd,old[0]);
00361             Cudd_RecursiveDeref(dd,old[1]);
00362             return(0);
00363         }
00364         cuddRef(res[1]);
00365 
00366         sizeNew = Cudd_SharingSize(res,2);
00367         if (sizeNew <= sizeOld) {
00368             Cudd_RecursiveDeref(dd,old[0]);
00369             old[0] = res[0];
00370             Cudd_RecursiveDeref(dd,old[1]);
00371             old[1] = res[1];
00372             sizeOld = sizeNew;
00373         } else {
00374             Cudd_RecursiveDeref(dd,res[0]);
00375             Cudd_RecursiveDeref(dd,res[1]);
00376             break;
00377         }
00378 
00379     } while (1);
00380 
00381     /* Refine the first factor by minimization. If h turns out to
00382     ** be f, this step guarantees that g will be 1. */
00383     superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
00384     if (superset1 == NULL) {
00385         Cudd_RecursiveDeref(dd,old[0]);
00386         Cudd_RecursiveDeref(dd,old[1]);
00387         return(0);
00388     }
00389     cuddRef(superset1);
00390     Cudd_RecursiveDeref(dd,old[0]);
00391     old[0] = superset1;
00392 
00393     if (old[0] != DD_ONE(dd)) {
00394         if (old[1] != DD_ONE(dd)) {
00395             *conjuncts = ALLOC(DdNode *,2);
00396             if (*conjuncts == NULL) {
00397                 Cudd_RecursiveDeref(dd,old[0]);
00398                 Cudd_RecursiveDeref(dd,old[1]);
00399                 dd->errorCode = CUDD_MEMORY_OUT;
00400                 return(0);
00401             }
00402             (*conjuncts)[0] = old[0];
00403             (*conjuncts)[1] = old[1];
00404             return(2);
00405         } else {
00406             Cudd_RecursiveDeref(dd,old[1]);
00407             *conjuncts = ALLOC(DdNode *,1);
00408             if (*conjuncts == NULL) {
00409                 Cudd_RecursiveDeref(dd,old[0]);
00410                 dd->errorCode = CUDD_MEMORY_OUT;
00411                 return(0);
00412             }
00413             (*conjuncts)[0] = old[0];
00414             return(1);
00415         }
00416     } else {
00417         Cudd_RecursiveDeref(dd,old[0]);
00418         *conjuncts = ALLOC(DdNode *,1);
00419         if (*conjuncts == NULL) {
00420             Cudd_RecursiveDeref(dd,old[1]);
00421             dd->errorCode = CUDD_MEMORY_OUT;
00422             return(0);
00423         }
00424         (*conjuncts)[0] = old[1];
00425         return(1);
00426     }
00427 
00428 } /* 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 452 of file cuddDecomp.c.

00456 {
00457     int result, i;
00458 
00459     result = Cudd_bddIterConjDecomp(dd,Cudd_Not(f),disjuncts);
00460     for (i = 0; i < result; i++) {
00461         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00462     }
00463     return(result);
00464 
00465 } /* 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 611 of file cuddDecomp.c.

00615 {
00616     int best;
00617     int min;
00618     DdNode *support, *scan, *var, *glocal, *hlocal;
00619 
00620     /* Find best cofactoring variable. */
00621     support = Cudd_Support(dd,f);
00622     if (support == NULL) return(0);
00623     if (Cudd_IsConstant(support)) {
00624         *conjuncts = ALLOC(DdNode *,1);
00625         if (*conjuncts == NULL) {
00626             dd->errorCode = CUDD_MEMORY_OUT;
00627             return(0);
00628         }
00629         (*conjuncts)[0] = f;
00630         cuddRef((*conjuncts)[0]);
00631         return(1);
00632     }
00633     cuddRef(support);
00634     min = 1000000000;
00635     best = -1;
00636     scan = support;
00637     while (!Cudd_IsConstant(scan)) {
00638         int i = scan->index;
00639         int est1 = Cudd_EstimateCofactor(dd,f,i,1);
00640         int est0 = Cudd_EstimateCofactor(dd,f,i,0);
00641         /* Minimize the size of the larger of the two cofactors. */
00642         int est = (est1 > est0) ? est1 : est0;
00643         if (est < min) {
00644             min = est;
00645             best = i;
00646         }
00647         scan = cuddT(scan);
00648     }
00649 #ifdef DD_DEBUG
00650     assert(best >= 0 && best < dd->size);
00651 #endif
00652     Cudd_RecursiveDeref(dd,support);
00653 
00654     var = Cudd_bddIthVar(dd,best);
00655     glocal = Cudd_bddOr(dd,f,var);
00656     if (glocal == NULL) {
00657         return(0);
00658     }
00659     cuddRef(glocal);
00660     hlocal = Cudd_bddOr(dd,f,Cudd_Not(var));
00661     if (hlocal == NULL) {
00662         Cudd_RecursiveDeref(dd,glocal);
00663         return(0);
00664     }
00665     cuddRef(hlocal);
00666 
00667     if (glocal != DD_ONE(dd)) {
00668         if (hlocal != DD_ONE(dd)) {
00669             *conjuncts = ALLOC(DdNode *,2);
00670             if (*conjuncts == NULL) {
00671                 Cudd_RecursiveDeref(dd,glocal);
00672                 Cudd_RecursiveDeref(dd,hlocal);
00673                 dd->errorCode = CUDD_MEMORY_OUT;
00674                 return(0);
00675             }
00676             (*conjuncts)[0] = glocal;
00677             (*conjuncts)[1] = hlocal;
00678             return(2);
00679         } else {
00680             Cudd_RecursiveDeref(dd,hlocal);
00681             *conjuncts = ALLOC(DdNode *,1);
00682             if (*conjuncts == NULL) {
00683                 Cudd_RecursiveDeref(dd,glocal);
00684                 dd->errorCode = CUDD_MEMORY_OUT;
00685                 return(0);
00686             }
00687             (*conjuncts)[0] = glocal;
00688             return(1);
00689         }
00690     } else {
00691         Cudd_RecursiveDeref(dd,glocal);
00692         *conjuncts = ALLOC(DdNode *,1);
00693         if (*conjuncts == NULL) {
00694             Cudd_RecursiveDeref(dd,hlocal);
00695             dd->errorCode = CUDD_MEMORY_OUT;
00696             return(0);
00697         }
00698         (*conjuncts)[0] = hlocal;
00699         return(1);
00700     }
00701 
00702 } /* 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 729 of file cuddDecomp.c.

00733 {
00734     int result, i;
00735 
00736     result = Cudd_bddVarConjDecomp(dd,Cudd_Not(f),disjuncts);
00737     for (i = 0; i < result; i++) {
00738         (*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
00739     }
00740     return(result);
00741 
00742 } /* 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 2001 of file cuddDecomp.c.

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

00944 {
00945     int valueG, valueH, gPresent, hPresent;
00946 
00947     valueG = valueH = gPresent = hPresent = 0;
00948     
00949     gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
00950     hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);
00951 
00952     if (!gPresent && !hPresent) return(NONE);
00953 
00954     if (!hPresent) {
00955         if (valueG & 1) return(G_ST);
00956         if (valueG & 2) return(G_CR);
00957     }
00958     if (!gPresent) {
00959         if (valueH & 1) return(H_CR);
00960         if (valueH & 2) return(H_ST);
00961     }
00962     /* both in tables */
00963     if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
00964     if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
00965     
00966     if (valueG & 1) {
00967         return(BOTH_G);
00968     } else {
00969         return(BOTH_H);
00970     }
00971     
00972 } /* 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 1095 of file cuddDecomp.c.

01103 {
01104     int value;
01105     Conjuncts *factors;
01106     int oneRef, twoRef;
01107     
01108     factors = ALLOC(Conjuncts, 1);
01109     if (factors == NULL) return(NULL);
01110 
01111     /* count the number of pointers to pair 2 */
01112     if (h2 == one) {
01113         twoRef = (Cudd_Regular(g2))->ref;
01114     } else if (g2 == one) {
01115         twoRef = (Cudd_Regular(h2))->ref;
01116     } else {
01117         twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
01118     }
01119 
01120     /* count the number of pointers to pair 1 */
01121     if (h1 == one) {
01122         oneRef  = (Cudd_Regular(g1))->ref;
01123     } else if (g1 == one) {
01124         oneRef  = (Cudd_Regular(h1))->ref;
01125     } else {
01126         oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
01127     }
01128 
01129     /* pick the pair with higher reference count */
01130     if (oneRef >= twoRef) {
01131         factors->g = g1;
01132         factors->h = h1;
01133     } else {
01134         factors->g = g2;
01135         factors->h = h2;
01136     }
01137     
01138     /*
01139      * Store computed factors in respective tables to encourage
01140      * recombination.
01141      */
01142     if (factors->g != one) {
01143         /* insert g in htable */
01144         value = 0;
01145         if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
01146             if (value == 2) {
01147                 value |= 1;
01148                 if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
01149                               (char *)(long)value) == ST_OUT_OF_MEM) {
01150                     FREE(factors);
01151                     return(NULL);
01152                 }
01153             }
01154         } else {
01155             value = 1;
01156             if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
01157                           (char *)(long)value) == ST_OUT_OF_MEM) {
01158                 FREE(factors);
01159                 return(NULL);
01160             }
01161         }
01162     }
01163 
01164     if (factors->h != one) {
01165         /* insert h in htable */
01166         value = 0;
01167         if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
01168             if (value == 1) {
01169                 value |= 2;
01170                 if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
01171                               (char *)(long)value) == ST_OUT_OF_MEM) {
01172                     FREE(factors);
01173                     return(NULL);
01174                 }
01175             }       
01176         } else {
01177             value = 2;
01178             if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
01179                           (char *)(long)value) == ST_OUT_OF_MEM) {
01180                 FREE(factors);
01181                 return(NULL);
01182             }
01183         }
01184     }
01185     
01186     /* Store factors in cache table for later use. */
01187     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
01188             ST_OUT_OF_MEM) {
01189         FREE(factors);
01190         return(NULL);
01191     }
01192 
01193     return(factors);
01194 
01195 } /* 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 1443 of file cuddDecomp.c.

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

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $" [static]

Definition at line 105 of file cuddDecomp.c.

long lastTimeG

Definition at line 109 of file cuddDecomp.c.

DdNode* one [static]

Definition at line 108 of file cuddDecomp.c.

DdNode * zero [static]

Definition at line 108 of file cuddDecomp.c.

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