abc70930: src/bdd/cudd/cuddDecomp.c Source File

00001 
00037 #include "util_hack.h"
00038 #include "cuddInt.h"
00039 
00040 /*---------------------------------------------------------------------------*/
00041 /* Constant declarations                                                     */
00042 /*---------------------------------------------------------------------------*/
00043 #define DEPTH 5
00044 #define THRESHOLD 10
00045 #define NONE 0
00046 #define PAIR_ST 1
00047 #define PAIR_CR 2
00048 #define G_ST 3
00049 #define G_CR 4
00050 #define H_ST 5
00051 #define H_CR 6
00052 #define BOTH_G 7
00053 #define BOTH_H 8
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Stucture declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Type declarations                                                         */
00061 /*---------------------------------------------------------------------------*/
00062 typedef struct Conjuncts {
00063     DdNode *g;
00064     DdNode *h;
00065 } Conjuncts;
00066 
00067 typedef struct  NodeStat {
00068     int distance;
00069     int localRef;
00070 } NodeStat;
00071 
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Variable declarations                                                     */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 #ifndef lint
00078 static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
00079 #endif
00080 
00081 static  DdNode  *one, *zero;
00082 long lastTimeG;
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Macro declarations                                                        */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00089 #define FactorsNotStored(factors)  ((int)((long)(factors) & 01))
00090 
00091 #define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))
00092 
00093 #define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))
00094 
00097 /*---------------------------------------------------------------------------*/
00098 /* Static function prototypes                                                */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 static NodeStat * CreateBotDist ARGS((DdNode * node, st_table * distanceTable));
00102 static double CountMinterms ARGS((DdNode * node, double max, st_table * mintermTable, FILE *fp));
00103 static void ConjunctsFree ARGS((DdManager * dd, Conjuncts * factors));
00104 static int PairInTables ARGS((DdNode * g, DdNode * h, st_table * ghTable));
00105 static Conjuncts * CheckTablesCacheAndReturn ARGS((DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable));
00106 static Conjuncts * PickOnePair ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable));
00107 static Conjuncts * CheckInTables ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem));
00108 static Conjuncts * ZeroCase ARGS((DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched));
00109 static Conjuncts * BuildConjuncts ARGS((DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable));
00110 static int cuddConjunctsAux ARGS((DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2));
00111 
00115 /*---------------------------------------------------------------------------*/
00116 /* Definition of exported functions                                          */
00117 /*---------------------------------------------------------------------------*/
00118 
00119 
00143 int
00144 Cudd_bddApproxConjDecomp(
00145   DdManager * dd /* manager */,
00146   DdNode * f /* function to be decomposed */,
00147   DdNode *** conjuncts /* address of the first factor */)
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 */
00219 
00220 
00241 int
00242 Cudd_bddApproxDisjDecomp(
00243   DdManager * dd /* manager */,
00244   DdNode * f /* function to be decomposed */,
00245   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00256 
00257 
00281 int
00282 Cudd_bddIterConjDecomp(
00283   DdManager * dd /* manager */,
00284   DdNode * f /* function to be decomposed */,
00285   DdNode *** conjuncts /* address of the array of conjuncts */)
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 */
00402 
00403 
00424 int
00425 Cudd_bddIterDisjDecomp(
00426   DdManager * dd /* manager */,
00427   DdNode * f /* function to be decomposed */,
00428   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00439 
00440 
00464 int
00465 Cudd_bddGenConjDecomp(
00466   DdManager * dd /* manager */,
00467   DdNode * f /* function to be decomposed */,
00468   DdNode *** conjuncts /* address of the array of conjuncts */)
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 */
00521 
00522 
00543 int
00544 Cudd_bddGenDisjDecomp(
00545   DdManager * dd /* manager */,
00546   DdNode * f /* function to be decomposed */,
00547   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00558 
00559 
00583 int
00584 Cudd_bddVarConjDecomp(
00585   DdManager * dd /* manager */,
00586   DdNode * f /* function to be decomposed */,
00587   DdNode *** conjuncts /* address of the array of conjuncts */)
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 */
00676 
00677 
00701 int
00702 Cudd_bddVarDisjDecomp(
00703   DdManager * dd /* manager */,
00704   DdNode * f /* function to be decomposed */,
00705   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00716 
00717 
00718 /*---------------------------------------------------------------------------*/
00719 /* Definition of internal functions                                          */
00720 /*---------------------------------------------------------------------------*/
00721 
00722 /*---------------------------------------------------------------------------*/
00723 /* Definition of static functions                                            */
00724 /*---------------------------------------------------------------------------*/
00725 
00726 
00740 static NodeStat *
00741 CreateBotDist(
00742   DdNode * node,
00743   st_table * distanceTable)
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 */
00795 
00796 
00809 static double
00810 CountMinterms(
00811   DdNode * node,
00812   double  max,
00813   st_table * mintermTable,
00814   FILE *fp)
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 */
00859 
00860 
00872 static void
00873 ConjunctsFree(
00874   DdManager * dd,
00875   Conjuncts * factors)
00876 {
00877     Cudd_RecursiveDeref(dd, factors->g);
00878     Cudd_RecursiveDeref(dd, factors->h);
00879     FREE(factors);
00880     return;
00881 
00882 } /* end of ConjunctsFree */
00883 
00884 
00912 static int
00913 PairInTables(
00914   DdNode * g,
00915   DdNode * h,
00916   st_table * ghTable)
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 */
00946 
00947 
00962 static Conjuncts *
00963 CheckTablesCacheAndReturn(
00964   DdNode * node,
00965   DdNode * g,
00966   DdNode * h,
00967   st_table * ghTable,
00968   st_table * cacheTable)
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 */
01051         
01067 static Conjuncts *
01068 PickOnePair(
01069   DdNode * node,
01070   DdNode * g1,
01071   DdNode * h1,
01072   DdNode * g2,
01073   DdNode * h2,
01074   st_table * ghTable,
01075   st_table * cacheTable)
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 */
01169 
01170 
01185 static Conjuncts *
01186 CheckInTables(
01187   DdNode * node,
01188   DdNode * g1,
01189   DdNode * h1,
01190   DdNode * g2,
01191   DdNode * h2,
01192   st_table * ghTable,
01193   st_table * cacheTable,
01194   int * outOfMem)
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 */
01397 
01398 
01399 
01415 static Conjuncts *
01416 ZeroCase(
01417   DdManager * dd,
01418   DdNode * node,
01419   Conjuncts * factorsNv,
01420   st_table * ghTable,
01421   st_table * cacheTable,
01422   int switched)
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 */
01632 
01633 
01653 static Conjuncts *
01654 BuildConjuncts(
01655   DdManager * dd,
01656   DdNode * node,
01657   st_table * distanceTable,
01658   st_table * cacheTable,
01659   int approxDistance,
01660   int maxLocalRef,
01661   st_table * ghTable,
01662   st_table * mintermTable)
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 */
01958 
01959 
01973 static int
01974 cuddConjunctsAux(
01975   DdManager * dd,
01976   DdNode * f,
01977   DdNode ** c1,
01978   DdNode ** c2)
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 */