glu-2.2: src/cuBdd/cuddDecomp.c Source File

00001 
00064 #include "util.h"
00065 #include "cuddInt.h"
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Constant declarations                                                     */
00069 /*---------------------------------------------------------------------------*/
00070 #define DEPTH 5
00071 #define THRESHOLD 10
00072 #define NONE 0
00073 #define PAIR_ST 1
00074 #define PAIR_CR 2
00075 #define G_ST 3
00076 #define G_CR 4
00077 #define H_ST 5
00078 #define H_CR 6
00079 #define BOTH_G 7
00080 #define BOTH_H 8
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Stucture declarations                                                     */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 /*---------------------------------------------------------------------------*/
00087 /* Type declarations                                                         */
00088 /*---------------------------------------------------------------------------*/
00089 typedef struct Conjuncts {
00090     DdNode *g;
00091     DdNode *h;
00092 } Conjuncts;
00093 
00094 typedef struct  NodeStat {
00095     int distance;
00096     int localRef;
00097 } NodeStat;
00098 
00099 
00100 /*---------------------------------------------------------------------------*/
00101 /* Variable declarations                                                     */
00102 /*---------------------------------------------------------------------------*/
00103 
00104 #ifndef lint
00105 static char rcsid[] DD_UNUSED = "$Id: cuddDecomp.c,v 1.44 2004/08/13 18:04:47 fabio Exp $";
00106 #endif
00107 
00108 static  DdNode  *one, *zero;
00109 long lastTimeG;
00110 
00111 /*---------------------------------------------------------------------------*/
00112 /* Macro declarations                                                        */
00113 /*---------------------------------------------------------------------------*/
00114 
00115 
00116 #define FactorsNotStored(factors)  ((int)((long)(factors) & 01))
00117 
00118 #define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))
00119 
00120 #define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))
00121 
00124 /*---------------------------------------------------------------------------*/
00125 /* Static function prototypes                                                */
00126 /*---------------------------------------------------------------------------*/
00127 
00128 static NodeStat * CreateBotDist (DdNode * node, st_table * distanceTable);
00129 static double CountMinterms (DdNode * node, double max, st_table * mintermTable, FILE *fp);
00130 static void ConjunctsFree (DdManager * dd, Conjuncts * factors);
00131 static int PairInTables (DdNode * g, DdNode * h, st_table * ghTable);
00132 static Conjuncts * CheckTablesCacheAndReturn (DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable);
00133 static Conjuncts * PickOnePair (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable);
00134 static Conjuncts * CheckInTables (DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem);
00135 static Conjuncts * ZeroCase (DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched);
00136 static Conjuncts * BuildConjuncts (DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable);
00137 static int cuddConjunctsAux (DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2);
00138 
00142 /*---------------------------------------------------------------------------*/
00143 /* Definition of exported functions                                          */
00144 /*---------------------------------------------------------------------------*/
00145 
00146 
00170 int
00171 Cudd_bddApproxConjDecomp(
00172   DdManager * dd /* manager */,
00173   DdNode * f /* function to be decomposed */,
00174   DdNode *** conjuncts /* address of the first factor */)
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 */
00246 
00247 
00268 int
00269 Cudd_bddApproxDisjDecomp(
00270   DdManager * dd /* manager */,
00271   DdNode * f /* function to be decomposed */,
00272   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00283 
00284 
00308 int
00309 Cudd_bddIterConjDecomp(
00310   DdManager * dd /* manager */,
00311   DdNode * f /* function to be decomposed */,
00312   DdNode *** conjuncts /* address of the array of conjuncts */)
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 */
00429 
00430 
00451 int
00452 Cudd_bddIterDisjDecomp(
00453   DdManager * dd /* manager */,
00454   DdNode * f /* function to be decomposed */,
00455   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00466 
00467 
00491 int
00492 Cudd_bddGenConjDecomp(
00493   DdManager * dd /* manager */,
00494   DdNode * f /* function to be decomposed */,
00495   DdNode *** conjuncts /* address of the array of conjuncts */)
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 */
00548 
00549 
00570 int
00571 Cudd_bddGenDisjDecomp(
00572   DdManager * dd /* manager */,
00573   DdNode * f /* function to be decomposed */,
00574   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00585 
00586 
00610 int
00611 Cudd_bddVarConjDecomp(
00612   DdManager * dd /* manager */,
00613   DdNode * f /* function to be decomposed */,
00614   DdNode *** conjuncts /* address of the array of conjuncts */)
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 */
00703 
00704 
00728 int
00729 Cudd_bddVarDisjDecomp(
00730   DdManager * dd /* manager */,
00731   DdNode * f /* function to be decomposed */,
00732   DdNode *** disjuncts /* address of the array of the disjuncts */)
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 */
00743 
00744 
00745 /*---------------------------------------------------------------------------*/
00746 /* Definition of internal functions                                          */
00747 /*---------------------------------------------------------------------------*/
00748 
00749 /*---------------------------------------------------------------------------*/
00750 /* Definition of static functions                                            */
00751 /*---------------------------------------------------------------------------*/
00752 
00753 
00767 static NodeStat *
00768 CreateBotDist(
00769   DdNode * node,
00770   st_table * distanceTable)
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 */
00822 
00823 
00836 static double
00837 CountMinterms(
00838   DdNode * node,
00839   double  max,
00840   st_table * mintermTable,
00841   FILE *fp)
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 */
00886 
00887 
00899 static void
00900 ConjunctsFree(
00901   DdManager * dd,
00902   Conjuncts * factors)
00903 {
00904     Cudd_RecursiveDeref(dd, factors->g);
00905     Cudd_RecursiveDeref(dd, factors->h);
00906     FREE(factors);
00907     return;
00908 
00909 } /* end of ConjunctsFree */
00910 
00911 
00939 static int
00940 PairInTables(
00941   DdNode * g,
00942   DdNode * h,
00943   st_table * ghTable)
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 */
00973 
00974 
00989 static Conjuncts *
00990 CheckTablesCacheAndReturn(
00991   DdNode * node,
00992   DdNode * g,
00993   DdNode * h,
00994   st_table * ghTable,
00995   st_table * cacheTable)
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 */
01078         
01094 static Conjuncts *
01095 PickOnePair(
01096   DdNode * node,
01097   DdNode * g1,
01098   DdNode * h1,
01099   DdNode * g2,
01100   DdNode * h2,
01101   st_table * ghTable,
01102   st_table * cacheTable)
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 */
01196 
01197 
01212 static Conjuncts *
01213 CheckInTables(
01214   DdNode * node,
01215   DdNode * g1,
01216   DdNode * h1,
01217   DdNode * g2,
01218   DdNode * h2,
01219   st_table * ghTable,
01220   st_table * cacheTable,
01221   int * outOfMem)
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 */
01424 
01425 
01426 
01442 static Conjuncts *
01443 ZeroCase(
01444   DdManager * dd,
01445   DdNode * node,
01446   Conjuncts * factorsNv,
01447   st_table * ghTable,
01448   st_table * cacheTable,
01449   int switched)
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 */
01659 
01660 
01680 static Conjuncts *
01681 BuildConjuncts(
01682   DdManager * dd,
01683   DdNode * node,
01684   st_table * distanceTable,
01685   st_table * cacheTable,
01686   int approxDistance,
01687   int maxLocalRef,
01688   st_table * ghTable,
01689   st_table * mintermTable)
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 */
01985 
01986 
02000 static int
02001 cuddConjunctsAux(
02002   DdManager * dd,
02003   DdNode * f,
02004   DdNode ** c1,
02005   DdNode ** c2)
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 */