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

00001 
00040 #include "calInt.h"
00041 
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Constant declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Type declarations                                                         */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Stucture declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 
00058 /*---------------------------------------------------------------------------*/
00059 /* Variable declarations                                                     */
00060 /*---------------------------------------------------------------------------*/
00061 
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Macro declarations                                                        */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 
00070 /*---------------------------------------------------------------------------*/
00071 /* Static function prototypes                                                */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 static int AssociationIsEqual(Cal_BddManager_t * bddManager, Cal_Bdd_t * p, Cal_Bdd_t * q);
00075 static int CheckAssoc(Cal_BddManager_t *bddManager, Cal_Bdd *assocInfo, int pairs);
00076 
00080 /*---------------------------------------------------------------------------*/
00081 /* Definition of exported functions                                          */
00082 /*---------------------------------------------------------------------------*/
00105 int
00106 Cal_AssociationInit(Cal_BddManager bddManager,
00107                     Cal_Bdd *associationInfoUserBdds,
00108                     int  pairs)
00109 {
00110   int i, numAssociations;
00111   CalAssociation_t *p, **q;
00112   Cal_Bdd_t f;
00113   Cal_Bdd_t *varAssociation;
00114   Cal_BddId_t j;
00115   long last;
00116   Cal_Bdd_t *associationInfo;
00117   
00118   if (!CheckAssoc(bddManager, associationInfoUserBdds, pairs)){
00119     return (-1);
00120   }
00121 
00122 
00123 /* First count the number of elements */
00124   for (i=0; associationInfoUserBdds[i]; i++);
00125   if (pairs)  numAssociations = i/2;
00126   else numAssociations = i;
00127   associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1);
00128   for (j=0; j < i; j++){
00129     associationInfo[j] =
00130         CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]);
00131   }
00132   associationInfo[j] = bddManager->bddNull;
00133 
00134   
00135   varAssociation = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
00136   for(i = 0; i <= bddManager->maxNumVars; i++){
00137     varAssociation[i] = bddManager->bddNull;
00138   }
00139 
00140   
00141   if(pairs){
00142     for(i = 0; i < numAssociations; i++){
00143       f = associationInfo[(i<<1)];
00144       varAssociation[CalBddGetBddId(f)] = associationInfo[(i<<1)+1];
00145     }
00146   }
00147   else{
00148     for(i = 0; i < numAssociations; i++){
00149       f=associationInfo[i];
00150       varAssociation[CalBddGetBddId(f)] = CalBddOne(bddManager);
00151     }
00152   }
00153   /* Check for existence. */
00154   for(p = bddManager->associationList; p; p = p->next){
00155     if(AssociationIsEqual(bddManager, p->varAssociation, varAssociation)){
00156         Cal_MemFree(varAssociation);
00157     Cal_MemFree(associationInfo);
00158         p->refCount++;
00159         return (p->id);
00160     }
00161   }
00162   /* Find the first unused id. */
00163   for(q = &bddManager->associationList, p = *q, i = 0;
00164       p && p->id == i; q = &p->next, p = *q, ++i){
00165   }
00166   /*p = Cal_MemAlloc(CalAssociation_t, 1);*/
00167   /*p = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/
00168   p = Cal_MemAlloc(CalAssociation_t, 1);
00169   p->id = i;
00170   p->next = *q;
00171   *q = p;
00172   p->varAssociation = varAssociation;
00173   last = -1;
00174   if(pairs){
00175     for(i = 0; i < numAssociations; i++){
00176       f = associationInfo[(i<<1)];
00177       j = CalBddGetBddIndex(bddManager, f);
00178       if((long)j > last){
00179           last = j;
00180       }
00181     }
00182   }
00183   else{
00184     for(i = 0; i < numAssociations; i++){
00185       f = associationInfo[i];
00186       j = CalBddGetBddIndex(bddManager, f);
00187       if((long)j > last){
00188           last = j;
00189       }
00190     }
00191   }
00192   p->lastBddIndex = last;
00193   p->refCount = 1;
00194   /* Protect BDDs in the association. */
00195   if(pairs){
00196     for(i = 0; i < numAssociations; i++){
00197       f = associationInfo[(i<<1)+1];
00198       CalBddIcrRefCount(f);
00199     }
00200   }
00201   Cal_MemFree(associationInfo);
00202   return p->id;
00203 }
00204 
00205 
00218 void
00219 Cal_AssociationQuit(Cal_BddManager bddManager, int  associationId)
00220 {
00221   Cal_BddId_t i;
00222   Cal_Bdd_t f;
00223   CalAssociation_t *p, **q;
00224 
00225   if(bddManager->currentAssociation->id == associationId){
00226     bddManager->currentAssociation = bddManager->tempAssociation;
00227   }
00228   for(q = &bddManager->associationList, p = *q; p; q = &p->next, p = *q){
00229     if(p->id == associationId){
00230       p->refCount--;
00231       if(!p->refCount){
00232         /* Unprotect the BDDs in the association. */
00233         for(i = 1; i <= bddManager->numVars; i++){
00234           f = p->varAssociation[i];
00235           if(!CalBddIsBddNull(bddManager, f)){
00236             CalBddDcrRefCount(f);
00237           }
00238         }
00239         *q = p->next;
00240         Cal_MemFree(p->varAssociation);
00241         /*CAL_BDD_FREE_REC(bddManager, p, CalAssociation_t);*/
00242         Cal_MemFree(p);
00243         CalCacheTableTwoFlushAssociationId(bddManager, associationId);
00244       }
00245       return;
00246     }
00247   }
00248   CalBddWarningMessage("Cal_AssociationQuit: no association with specified ID");
00249 }
00250 
00263 int
00264 Cal_AssociationSetCurrent(Cal_BddManager bddManager, int  associationId)
00265 {
00266   int oldAssociationId;
00267   CalAssociation_t *p;
00268 
00269   oldAssociationId = bddManager->currentAssociation->id;
00270   if(associationId != -1){
00271     for(p = bddManager->associationList; p; p = p->next){
00272       if(p->id == associationId){
00273         bddManager->currentAssociation = p;
00274         return (oldAssociationId);
00275       }
00276     }
00277     CalBddWarningMessage(
00278         "Cal_AssociationSetCurrent: no variable association with specified ID.\n May have been discarded during dynamic reordering.");
00279   }
00280   bddManager->currentAssociation = bddManager->tempAssociation;
00281   return oldAssociationId;
00282 }
00283 
00284 
00295 void
00296 Cal_TempAssociationAugment(Cal_BddManager bddManager,
00297                            Cal_Bdd *associationInfoUserBdds,
00298                            int  pairs)
00299 {
00300   int i, j, numAssociations;
00301   Cal_Bdd_t f;
00302   long last;
00303   Cal_Bdd_t *associationInfo;
00304   
00305   if (CheckAssoc(bddManager, associationInfoUserBdds, pairs) == 0) {
00306     return;
00307   }
00308 
00309   /*while (associationInfoUserBdds[i++]);*/
00310   for (i=0; associationInfoUserBdds[i]; i++);
00311   if (pairs) numAssociations = i/2;
00312   else numAssociations = i;
00313   associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1);
00314   for (j=0; j < i; j++){
00315     associationInfo[j] =
00316         CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]);
00317   }
00318   associationInfo[j] = bddManager->bddNull;
00319   
00320   last = bddManager->tempAssociation->lastBddIndex;
00321   if(pairs){
00322     for(i = 0; i < numAssociations; i++){
00323       f = associationInfo[(i<<1)];
00324       j = CalBddGetBddId(f);
00325       if(bddManager->idToIndex[j] > last){
00326         last = bddManager->idToIndex[j];
00327       }
00328       f = bddManager->tempAssociation->varAssociation[j];
00329       if(!CalBddIsBddNull(bddManager, f)){
00330         CalBddDcrRefCount(f);
00331       }
00332       f = associationInfo[(i<<1)+1];
00333       bddManager->tempAssociation->varAssociation[j] = f;
00334       /* Protect BDDs in the association. */
00335       CalBddIcrRefCount(f);
00336     }
00337   }
00338   else{
00339     for(i = 0; i < numAssociations; i++){
00340       f = associationInfo[i];
00341       j = CalBddGetBddId(f);
00342       if(bddManager->idToIndex[j] > last){
00343         last = bddManager->idToIndex[j];
00344       }
00345       f = bddManager->tempAssociation->varAssociation[j];
00346       if(!CalBddIsBddNull(bddManager, f)){
00347         CalBddDcrRefCount(f);
00348       }
00349       bddManager->tempAssociation->varAssociation[j] = CalBddOne(bddManager);
00350     } 
00351   }
00352   bddManager->tempAssociation->lastBddIndex = last;
00353   Cal_MemFree(associationInfo);
00354 }
00355 
00356 
00357 
00368 void
00369 Cal_TempAssociationInit(Cal_BddManager bddManager,
00370                         Cal_Bdd *associationInfoUserBdds,
00371                         int  pairs)
00372 {
00373   long i;
00374   Cal_Bdd_t f;
00375 
00376   /* Clean up old temporary association. */
00377   for(i = 1; i <= bddManager->numVars; i++){
00378     f = bddManager->tempAssociation->varAssociation[i];
00379     if(!CalBddIsBddNull(bddManager, f)){
00380       CalBddDcrRefCount(f);
00381       bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
00382     }
00383   }
00384   bddManager->tempAssociation->lastBddIndex = -1;
00385   Cal_TempAssociationAugment(bddManager, associationInfoUserBdds, pairs);
00386 }
00387 
00397 void
00398 Cal_TempAssociationQuit(Cal_BddManager bddManager)
00399 {
00400   int i;
00401   Cal_Bdd_t f;
00402 
00403   /* Clean up old temporary association. */
00404   for(i = 1; i <= bddManager->numVars; i++){
00405     f = bddManager->tempAssociation->varAssociation[i];
00406     if(!CalBddIsBddNull(bddManager, f)){
00407       CalBddDcrRefCount(f);
00408       bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
00409     }
00410   }
00411   bddManager->tempAssociation->lastBddIndex = -1;
00412 }
00413 
00414 
00415 
00416 /*---------------------------------------------------------------------------*/
00417 /* Definition of internal functions                                          */
00418 /*---------------------------------------------------------------------------*/
00430 void
00431 CalAssociationListFree(Cal_BddManager_t *  bddManager)
00432 {
00433   CalAssociation_t *assoc, *nextAssoc;
00434   
00435   for(assoc = bddManager->associationList;
00436       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00437     nextAssoc = assoc->next;
00438     Cal_MemFree(assoc->varAssociation);
00439     /*CAL_BDD_FREE_REC(bddManager, assoc, CalAssociation_t);*/
00440     Cal_MemFree(assoc);
00441   }
00442 }
00443 
00455 void
00456 CalVarAssociationRepackUpdate(Cal_BddManager_t *  bddManager,
00457                               Cal_BddId_t id)
00458 {
00459   CalAssociation_t *assoc, *nextAssoc;
00460   int i;
00461   
00462   for(assoc = bddManager->associationList;
00463       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00464     nextAssoc = assoc->next;
00465     for (i=1; i <= bddManager->numVars; i++){
00466       if (CalBddGetBddId(assoc->varAssociation[i]) == id){
00467         CalBddForward(assoc->varAssociation[i]);
00468       }
00469     }
00470   }
00471   /* fix temporary association */
00472   assoc = bddManager->tempAssociation;
00473   for (i=1; i <= bddManager->numVars; i++){
00474     if (CalBddGetBddId(assoc->varAssociation[i]) == id){
00475       CalBddForward(assoc->varAssociation[i]);
00476     }
00477   }
00478 }
00479 
00491 void
00492 CalCheckAssociationValidity(Cal_BddManager_t *  bddManager)
00493 {
00494   CalAssociation_t *assoc, *nextAssoc;
00495   int i;
00496   
00497   for(assoc = bddManager->associationList;
00498       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00499     nextAssoc = assoc->next;
00500     for (i=1; i <= bddManager->numVars; i++){
00501       Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
00502     }
00503   }
00504   /* temporary association */
00505   assoc = bddManager->tempAssociation;
00506   for (i=1; i <= bddManager->numVars; i++){
00507     Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
00508   }
00509 }
00510 
00522 void
00523 CalReorderAssociationFix(Cal_BddManager_t *bddManager)
00524 {
00525   CalAssociation_t *assoc, *nextAssoc;
00526   int i;
00527   
00528   for(assoc = bddManager->associationList;
00529       assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
00530     nextAssoc = assoc->next;
00531     for (i=1; i <= bddManager->numVars; i++){
00532         if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00533             CalBddIsForwardedTo(assoc->varAssociation[i]);
00534         }
00535     }
00536   }
00537   /* fix temporary association */
00538   assoc = bddManager->tempAssociation;
00539   for (i=1; i <= bddManager->numVars; i++){
00540       if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
00541           CalBddIsForwardedTo(assoc->varAssociation[i]);
00542       }
00543   }
00544 }
00545 
00546 /*---------------------------------------------------------------------------*/
00547 /* Definition of static functions                                            */
00548 /*---------------------------------------------------------------------------*/
00549 
00559 static int
00560 AssociationIsEqual(Cal_BddManager_t * bddManager,
00561                    Cal_Bdd_t * p,
00562                    Cal_Bdd_t * q)
00563 {
00564   int i;
00565   for(i = 1; i <= bddManager->maxNumVars; i++){
00566     if(CalBddIsEqual(p[i], q[i]) == 0){
00567       return (0);
00568     }
00569   }
00570   return (1);
00571 }
00572 
00584 static int
00585 CheckAssoc(Cal_BddManager_t *bddManager, Cal_Bdd *assocInfo, int pairs)
00586 {
00587   CalBddArrayPreProcessing(bddManager, assocInfo);
00588   if (pairs){
00589     while (assocInfo[0] && assocInfo[1]){
00590       if (CalBddTypeAux(bddManager,
00591                         CalBddGetInternalBdd(bddManager, assocInfo[0])) !=
00592           CAL_BDD_TYPE_POSVAR){  
00593             CalBddWarningMessage("CheckAssoc: first element in pair is not a positive variable"); 
00594             return (0);
00595           }
00596       assocInfo+=2;
00597     }
00598   }
00599   return (1);
00600 }
00601