glu-2.2: src/calBdd/calBddSatisfy.c Source File

00001 
00041 #include "calInt.h"
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Constant declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 /*---------------------------------------------------------------------------*/
00048 /* Type declarations                                                         */
00049 /*---------------------------------------------------------------------------*/
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Stucture declarations                                                     */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Variable declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Macro declarations                                                        */
00061 /*---------------------------------------------------------------------------*/
00062 
00063 
00066 /*---------------------------------------------------------------------------*/
00067 /* Static function prototypes                                                */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 static Cal_Bdd_t BddSatisfyStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f);
00071 static Cal_Bdd_t BddSatisfySupportStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_BddId_t * support);
00072 static int IndexCmp(const void * p1, const void * p2);
00073 static double BddSatisfyingFractionStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, CalHashTable_t * hashTable);
00074 
00077 /*---------------------------------------------------------------------------*/
00078 /* Definition of exported functions                                          */
00079 /*---------------------------------------------------------------------------*/
00080 
00096 Cal_Bdd
00097 Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd  fUserBdd)
00098 {
00099   Cal_Bdd_t f;
00100   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00101     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00102     if(CalBddIsBddZero(bddManager, f)){
00103       CalBddWarningMessage("Cal_BddSatisfy: argument is false");
00104       return (fUserBdd);
00105     }
00106     f = BddSatisfyStep(bddManager, f);
00107     return CalBddGetExternalBdd(bddManager, f);
00108   }
00109   return (Cal_Bdd) 0;
00110 }
00111 
00112 
00130 Cal_Bdd
00131 Cal_BddSatisfySupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00132 {
00133   Cal_BddId_t *support, *p;
00134   long i;
00135   Cal_Bdd_t result;
00136   Cal_Bdd_t f;
00137   
00138   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00139     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00140     if(CalBddIsBddZero(bddManager, f)){
00141       CalBddWarningMessage("Cal_BddSatisfySupport: argument is false");
00142       return (fUserBdd);
00143     }
00144     support = Cal_MemAlloc(Cal_BddId_t, bddManager->numVars+1);
00145     for(i = 1, p = support; i <= bddManager->numVars; i++){
00146       if(!CalBddIsBddNull(bddManager,
00147           bddManager->currentAssociation->varAssociation[i])){
00148         *p = bddManager->idToIndex[i];
00149         ++p;
00150       }
00151     }
00152     *p = 0;
00153     qsort(support, (unsigned)(p - support), sizeof(Cal_BddId_t), IndexCmp);
00154     while(p != support){
00155       --p;
00156       *p = bddManager->indexToId[*p];
00157     }
00158     result = BddSatisfySupportStep(bddManager, f, support);
00159     Cal_MemFree(support);
00160     return CalBddGetExternalBdd(bddManager, result);
00161   }
00162   return (Cal_Bdd) 0;
00163 }
00164 
00178 double
00179 Cal_BddSatisfyingFraction(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00180 {
00181   double fraction;
00182   CalHashTable_t *hashTable;
00183   Cal_Bdd_t f;
00184   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00185     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00186     hashTable = CalHashTableOneInit(bddManager, sizeof(double));
00187     fraction = BddSatisfyingFractionStep(bddManager, f, hashTable);
00188     CalHashTableOneQuit(hashTable);
00189     return fraction;
00190   }
00191   return 0.0;
00192 }
00193 
00194 /*---------------------------------------------------------------------------*/
00195 /* Definition of internal functions                                          */
00196 /*---------------------------------------------------------------------------*/
00197 
00198 /*---------------------------------------------------------------------------*/
00199 /* Definition of static functions                                            */
00200 /*---------------------------------------------------------------------------*/
00201 
00216 static Cal_Bdd_t
00217 BddSatisfyStep(
00218   Cal_BddManager_t * bddManager,
00219   Cal_Bdd_t  f)
00220 {
00221   Cal_Bdd_t tempBdd;
00222   Cal_Bdd_t result;
00223 
00224   if(CalBddIsBddConst(f)){
00225     return (f);
00226   }
00227   CalBddGetThenBdd(f, tempBdd);
00228   if(CalBddIsBddZero(bddManager, tempBdd)){
00229     CalBddGetElseBdd(f, tempBdd);
00230     tempBdd = BddSatisfyStep(bddManager, tempBdd);
00231     if(!CalUniqueTableForIdFindOrAdd(bddManager,
00232         bddManager->uniqueTable[CalBddGetBddId(f)],
00233         CalBddZero(bddManager), tempBdd, &result)){
00234       CalBddIcrRefCount(tempBdd);
00235     }
00236   }
00237   else{
00238     tempBdd = BddSatisfyStep(bddManager, tempBdd);
00239     if(!CalUniqueTableForIdFindOrAdd(bddManager,
00240         bddManager->uniqueTable[CalBddGetBddId(f)],
00241         tempBdd, CalBddZero(bddManager), &result)){
00242       CalBddIcrRefCount(tempBdd);
00243     }
00244   }
00245   return (result);
00246 }
00247 
00248 
00262 static Cal_Bdd_t
00263 BddSatisfySupportStep(
00264   Cal_BddManager_t * bddManager,
00265   Cal_Bdd_t  f,
00266   Cal_BddId_t * support)
00267 {
00268   Cal_Bdd_t tempBdd;
00269   Cal_Bdd_t result;
00270 
00271   if(!*support){
00272     return BddSatisfyStep(bddManager, f);
00273   }
00274   if(CalBddGetBddIndex(bddManager, f) <= bddManager->idToIndex[*support]){
00275     if(CalBddGetBddId(f) == *support){
00276         ++support;
00277     }
00278     CalBddGetThenBdd(f, tempBdd);
00279     if(CalBddIsBddZero(bddManager, tempBdd)){
00280       CalBddGetElseBdd(f, tempBdd);
00281       tempBdd = BddSatisfySupportStep(bddManager, tempBdd, support);
00282       if(!CalUniqueTableForIdFindOrAdd(bddManager,
00283           bddManager->uniqueTable[CalBddGetBddId(f)],
00284           CalBddZero(bddManager), tempBdd, &result)){
00285         CalBddIcrRefCount(tempBdd);
00286       }
00287     }
00288     else{
00289       tempBdd = BddSatisfySupportStep(bddManager, tempBdd, support);
00290       if(!CalUniqueTableForIdFindOrAdd(bddManager,
00291           bddManager->uniqueTable[CalBddGetBddId(f)],
00292           tempBdd, CalBddZero(bddManager), &result)){
00293         CalBddIcrRefCount(tempBdd);
00294       }
00295     }
00296   }
00297   else{
00298     tempBdd = BddSatisfySupportStep(bddManager, f, support+1);
00299     if(!CalUniqueTableForIdFindOrAdd(bddManager,
00300         bddManager->uniqueTable[*support],
00301         CalBddZero(bddManager), tempBdd, &result)){
00302       CalBddIcrRefCount(tempBdd);
00303     }
00304   }
00305   return (result);
00306 }
00307 
00308 
00320 static int
00321 IndexCmp(const void * p1, const void * p2)
00322 {
00323   Cal_BddIndex_t i1, i2;
00324 
00325   i1 = *(Cal_BddId_t *)p1;
00326   i2 = *(Cal_BddId_t *)p2;
00327   if(i1 < i2){
00328     return (-1);
00329   }
00330   if(i1 > i2){
00331     return (1);
00332   }
00333   return (0);
00334 }
00335 
00347 static double
00348 BddSatisfyingFractionStep(
00349   Cal_BddManager_t * bddManager,
00350   Cal_Bdd_t  f,
00351   CalHashTable_t * hashTable)
00352 {
00353   double *resultPtr, result;
00354   Cal_Bdd_t thenBdd, elseBdd;
00355 
00356   if(CalBddIsBddConst(f)){
00357     if(CalBddIsBddZero(bddManager, f)){
00358       return 0.0;
00359     }
00360     return 1.0;
00361   }
00362   if(CalHashTableOneLookup(hashTable, f, (char **)&resultPtr)){
00363     return (*resultPtr);
00364   }
00365   CalBddGetThenBdd(f, thenBdd);
00366   CalBddGetElseBdd(f, elseBdd);
00367   result = 
00368       0.5 * BddSatisfyingFractionStep(bddManager, thenBdd, hashTable) +
00369       0.5 * BddSatisfyingFractionStep(bddManager, elseBdd, hashTable);
00370   CalHashTableOneInsert(hashTable, f, (char *)&result);
00371   return (result);
00372 }
00373