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

00001 
00039 #include "calInt.h"
00040 
00041 /*---------------------------------------------------------------------------*/
00042 /* Constant declarations                                                     */
00043 /*---------------------------------------------------------------------------*/
00044 
00045 
00046 /*---------------------------------------------------------------------------*/
00047 /* Type declarations                                                         */
00048 /*---------------------------------------------------------------------------*/
00049 
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Stucture declarations                                                     */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Variable declarations                                                     */
00058 /*---------------------------------------------------------------------------*/
00059 
00060 
00061 /*---------------------------------------------------------------------------*/
00062 /* Macro declarations                                                        */
00063 /*---------------------------------------------------------------------------*/
00064 
00065 
00068 /*---------------------------------------------------------------------------*/
00069 /* Static function prototypes                                                */
00070 /*---------------------------------------------------------------------------*/
00071 
00072 
00076 /*---------------------------------------------------------------------------*/
00077 /* Definition of exported functions                                          */
00078 /*---------------------------------------------------------------------------*/
00079 
00080 /*---------------------------------------------------------------------------*/
00081 /* Definition of internal functions                                          */
00082 /*---------------------------------------------------------------------------*/
00094 int
00095 CalOpAnd(Cal_BddManager_t * bddManager,
00096          Cal_Bdd_t  F,
00097          Cal_Bdd_t  G,
00098          Cal_Bdd_t * resultBddPtr)
00099 {
00100   if(CalBddIsBddConst(F)){
00101     if(CalBddIsBddOne(bddManager, F)){
00102       *resultBddPtr = G;
00103     }
00104     else{
00105       *resultBddPtr = F;
00106     }
00107     return 1;
00108   }
00109   else if(CalBddIsBddConst(G)){
00110     if(CalBddIsBddOne(bddManager, G)){
00111       *resultBddPtr = F;
00112     }
00113     else{
00114       *resultBddPtr = G;
00115     }
00116     return 1;
00117   }
00118   else{
00119     CalBddNode_t *bddNodeF, *bddNodeG;
00120     bddNodeF = CalBddGetBddNode(F);
00121     bddNodeG = CalBddGetBddNode(G);
00122     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00123       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00124         *resultBddPtr = CalBddZero(bddManager);
00125       }
00126       else{
00127         *resultBddPtr = F;
00128       }
00129       return 1;
00130     }
00131     else{
00132       return 0;
00133     }
00134   }
00135 }
00136 
00148 int
00149 CalOpNand(Cal_BddManager_t * bddManager,
00150           Cal_Bdd_t  F,
00151           Cal_Bdd_t  G,
00152           Cal_Bdd_t * resultBddPtr)
00153 {
00154   if(CalBddIsBddConst(F)){
00155     if(CalBddIsBddOne(bddManager, F)){
00156       CalBddNot(G, *resultBddPtr);
00157     }
00158     else{
00159       CalBddNot(F, *resultBddPtr);
00160     }
00161     return 1;
00162   }
00163   else if(CalBddIsBddConst(G)){
00164     if(CalBddIsBddOne(bddManager, G)){
00165       CalBddNot(F, *resultBddPtr);
00166     }
00167     else{
00168       CalBddNot(G, *resultBddPtr);
00169     }
00170     return 1;
00171   }
00172   else{
00173     CalBddNode_t *bddNodeF, *bddNodeG;
00174     bddNodeF = CalBddGetBddNode(F);
00175     bddNodeG = CalBddGetBddNode(G);
00176     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00177       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00178         *resultBddPtr = CalBddOne(bddManager);
00179       }
00180       else{
00181         CalBddNot(F, *resultBddPtr);
00182       }
00183       return 1;
00184     }
00185     else{
00186       return 0;
00187     }
00188   }
00189 }
00190 
00202 int
00203 CalOpOr(
00204   Cal_BddManager_t * bddManager,
00205   Cal_Bdd_t  F,
00206   Cal_Bdd_t  G,
00207   Cal_Bdd_t * resultBddPtr)
00208 {
00209   if(CalBddIsBddConst(F)){
00210     if(CalBddIsBddOne(bddManager, F)){
00211       *resultBddPtr = F;
00212     }
00213     else{
00214       *resultBddPtr = G;
00215     }
00216     return 1;
00217   }
00218   else if(CalBddIsBddConst(G)){
00219     if(CalBddIsBddOne(bddManager, G)){
00220       *resultBddPtr = G;
00221     }
00222     else{
00223       *resultBddPtr = F;
00224     }
00225     return 1;
00226   }
00227   else{
00228     CalBddNode_t *bddNodeF, *bddNodeG;
00229     bddNodeF = CalBddGetBddNode(F);
00230     bddNodeG = CalBddGetBddNode(G);
00231     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00232       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00233         *resultBddPtr = CalBddOne(bddManager);
00234       }
00235       else{
00236         *resultBddPtr = F;
00237       }
00238       return 1;
00239     }
00240     else{
00241       return 0;
00242     }
00243   }
00244 }
00245 
00257 int
00258 CalOpXor(
00259   Cal_BddManager_t * bddManager,
00260   Cal_Bdd_t  F,
00261   Cal_Bdd_t  G,
00262   Cal_Bdd_t * resultBddPtr)
00263 {
00264   if(CalBddIsBddConst(F)){
00265     if(CalBddIsBddOne(bddManager, F)){
00266       CalBddNot(G, *resultBddPtr);
00267     }
00268     else{
00269       *resultBddPtr = G;
00270     }
00271     return 1;
00272   }
00273   else if(CalBddIsBddConst(G)){
00274     if(CalBddIsBddOne(bddManager, G)){
00275       CalBddNot(F, *resultBddPtr);
00276     }
00277     else{
00278       *resultBddPtr = F;
00279     }
00280     return 1;
00281   }
00282   else{
00283     CalBddNode_t *bddNodeF, *bddNodeG;
00284     bddNodeF = CalBddGetBddNode(F);
00285     bddNodeG = CalBddGetBddNode(G);
00286     if((CAL_BDD_POINTER(bddNodeF) == CAL_BDD_POINTER(bddNodeG))){
00287       if((CalAddress_t)bddNodeF ^ (CalAddress_t)bddNodeG){
00288         *resultBddPtr = CalBddOne(bddManager);
00289       }
00290       else{
00291         *resultBddPtr = CalBddZero(bddManager);
00292       }
00293       return 1;
00294     }
00295     else{
00296       return 0;
00297     }
00298   }
00299 }
00300 
00312 Cal_Bdd_t
00313 CalOpITE(
00314   Cal_BddManager_t *bddManager,
00315   Cal_Bdd_t f,
00316   Cal_Bdd_t g,
00317   Cal_Bdd_t h,
00318   CalHashTable_t **reqQueForITE)
00319 {
00320   CalBddNode_t *bddNode1, *bddNode2;
00321   int complementFlag = 0;
00322 
00323   /*
00324    * First phase: Make substitutions 
00325    * ITE(F,F,H) = ITE(F,1,H)
00326    * ITE(F,F',H) = ITE(F,0,H)
00327    * ITE(F,G,F) = ITE(F,G,0)
00328    * ITE(F,G,F') = ITE(F,G,1)
00329    */
00330   bddNode1 = CalBddGetBddNode(f);
00331   bddNode2 = CalBddGetBddNode(g);
00332   if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
00333     if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
00334       g = CalBddZero(bddManager);
00335     }
00336     else{
00337       g = CalBddOne(bddManager);
00338     }
00339   }
00340   bddNode2 = CalBddGetBddNode(h);
00341   if((CAL_BDD_POINTER(bddNode1) == CAL_BDD_POINTER(bddNode2))){
00342     if((CalAddress_t)bddNode1 ^ (CalAddress_t)bddNode2){
00343       h = CalBddOne(bddManager);
00344     }
00345     else{
00346       h = CalBddZero(bddManager);
00347     }
00348   }
00349 
00350   /*
00351    * Second phase: Fix the complement pointers.
00352    * There are 3 possible cases:
00353    * F +ve G -ve: ITE(F ,G',H ) = ITE(F ,G ,H')'
00354    * F -ve H +ve: ITE(F',G ,H ) = ITE(F ,H ,G)
00355    * F -ve H -ve: ITE(F',G ,H') = ITE(F ,H ,G')'
00356    */
00357   if(CalBddIsOutPos(f)){
00358     if(!CalBddIsOutPos(g)){
00359       CalBddNot(g, g);
00360       CalBddNot(h, h);
00361       complementFlag = 1;
00362     }
00363   }
00364   else{
00365     Cal_Bdd_t tmpBdd;
00366     CalBddNot(f, f);
00367     if(CalBddIsOutPos(h)){
00368       tmpBdd = g;
00369       g = h;
00370       h = tmpBdd;
00371     }
00372     else{
00373       tmpBdd = g;
00374       CalBddNot(h, g);
00375       CalBddNot(tmpBdd, h);
00376       complementFlag = 1;
00377     }
00378   }
00379 
00380   /*
00381    * Third phase: Check for the terminal cases; create new request if needed
00382    * ite(1,G,H) = G
00383    * ite(0,G,H) = H (impossible by construction in second phase)
00384    * ite(F,G,G) = G
00385    * ite(F,1,0) = F
00386    * ite(F,0,1) = F'(impossible by construction in second phase)
00387    */
00388   if(CalBddIsBddConst(f) || CalBddIsEqual(g, h)){
00389     CalBddUpdatePhase(g, complementFlag);
00390     return g;
00391   }
00392   else if(CalBddIsBddConst(g) && CalBddIsBddConst(h)){
00393     CalBddUpdatePhase(f, complementFlag);
00394     return f;
00395   }
00396   else{
00397     Cal_BddId_t bddId;
00398     Cal_Bdd_t result;
00399     CalBddGetMinId3(bddManager, f, g, h, bddId);
00400     CalHashTableThreeFindOrAdd(reqQueForITE[bddId], f, g, h, &result);
00401     CalBddUpdatePhase(result, complementFlag);
00402     return result;
00403   }
00404 }
00405 
00406 /*---------------------------------------------------------------------------*/
00407 /* Definition of static functions                                            */
00408 /*---------------------------------------------------------------------------*/
00409 
00410 
00411 
00412 
00413 
00414 
00415 
00416 
00417 
00418 
00419 
00420 
00421