abc70930: src/opt/fxu/fxuPair.c Source File

00001 
00019 #include "fxuInt.h"
00020 
00024 
00025 #define MAX_PRIMES      304
00026 
00027 static s_Primes[MAX_PRIMES] =
00028 {
00029         2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 
00030         41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 
00031         97, 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 
00032         157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223, 
00033         227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 
00034         283, 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 
00035         367, 373, 379, 383, 389, 397, 401, 409, 419, 421, 431, 433, 
00036         439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 
00037         509, 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 
00038         599, 601, 607, 613, 617, 619, 631, 641, 643, 647, 653, 659, 
00039         661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 
00040         751, 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 
00041         829, 839, 853, 857, 859, 863, 877, 881, 883, 887, 907, 911, 
00042         919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, 
00043         1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 
00044         1087, 1091, 1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 
00045         1171, 1181, 1187, 1193, 1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 
00046         1259, 1277, 1279, 1283, 1289, 1291, 1297, 1301, 1303, 1307, 1319, 1321, 
00047         1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 1427, 1429, 1433, 1439, 
00048         1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 1499, 1511, 
00049         1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, 
00050         1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 
00051         1697, 1699, 1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 
00052         1787, 1789, 1801, 1811, 1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 
00053         1879, 1889, 1901, 1907, 1913, 1931, 1933, 1949, 1951, 1973, 1979, 1987, 
00054         1993, 1997, 1999, 2003 
00055 };
00056 
00060 
00072 void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
00073 {
00074         Fxu_Lit * pLit1, * pLit2;
00075         Fxu_Cube * pCubeTemp;
00076 
00077         // walk through the cubes to determine 
00078         // the one that has higher first variable
00079         pLit1 = (*ppCube1)->lLits.pHead;
00080         pLit2 = (*ppCube2)->lLits.pHead;
00081         while ( 1 )
00082         {
00083                 if ( pLit1->iVar == pLit2->iVar )
00084                 {
00085                         pLit1 = pLit1->pHNext;
00086                         pLit2 = pLit2->pHNext;
00087                         continue;
00088                 }
00089                 assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
00090                 if ( pLit1->iVar > pLit2->iVar )
00091                 { // swap the cubes
00092                         pCubeTemp = *ppCube1;
00093                         *ppCube1  = *ppCube2;
00094                         *ppCube2  = pCubeTemp;
00095                 }
00096                 break;
00097         }
00098 }
00099 
00111 void Fxu_PairCanonicize2( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
00112 {
00113         Fxu_Cube * pCubeTemp;
00114     // canonicize the pair by ordering the cubes
00115         if ( (*ppCube1)->iCube > (*ppCube2)->iCube )
00116         { // swap the cubes
00117                 pCubeTemp = *ppCube1;
00118                 *ppCube1  = *ppCube2;
00119                 *ppCube2  = pCubeTemp;
00120     }
00121 }
00122 
00134 unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], int nVarsC1, int nVarsC2 )
00135 {
00136         int Offset1 = 100, Offset2 = 200, i;
00137         unsigned Key;
00138         // compute the hash key
00139         Key = 0;
00140     for ( i = 0; i < nVarsC1; i++ )
00141         Key ^= s_Primes[Offset1+i] * piVarsC1[i];
00142     for ( i = 0; i < nVarsC2; i++ )
00143         Key ^= s_Primes[Offset2+i] * piVarsC2[i];
00144         return Key;
00145 }
00146 
00161 unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2, 
00162                          int * pnBase, int * pnLits1, int * pnLits2 )
00163 {
00164         int Offset1 = 100, Offset2 = 200;
00165     int nBase, nLits1, nLits2;
00166         Fxu_Lit * pLit1, * pLit2;
00167         unsigned Key;
00168 
00169         // compute the hash key
00170         Key    = 0;
00171         nLits1 = 0;
00172         nLits2 = 0;
00173         nBase  = 0;
00174         pLit1  = pCube1->lLits.pHead;
00175         pLit2  = pCube2->lLits.pHead;
00176         while ( 1 )
00177         {
00178                 if ( pLit1 && pLit2 )
00179                 {
00180                         if ( pLit1->iVar == pLit2->iVar )
00181                         { // ensure cube-free
00182                                 pLit1 = pLit1->pHNext;
00183                                 pLit2 = pLit2->pHNext;
00184                                 // add this literal to the base
00185                                 nBase++;
00186                         }
00187                         else if ( pLit1->iVar < pLit2->iVar )
00188                         {
00189                                 Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
00190                                 pLit1 = pLit1->pHNext;
00191                                 nLits1++;
00192                         }
00193                         else
00194                         {
00195                                 Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
00196                                 pLit2 = pLit2->pHNext;
00197                                 nLits2++;
00198                         }
00199                 }
00200                 else if ( pLit1 && !pLit2 )
00201                 {
00202                         Key  ^= s_Primes[Offset1+nLits1] * pLit1->iVar;
00203                         pLit1 = pLit1->pHNext;
00204                         nLits1++;
00205                 }
00206                 else if ( !pLit1 && pLit2 )
00207                 {
00208                         Key  ^= s_Primes[Offset2+nLits2] * pLit2->iVar;
00209                         pLit2 = pLit2->pHNext;
00210                         nLits2++;
00211                 }
00212                 else
00213                         break;
00214         }
00215     *pnBase  = nBase;
00216     *pnLits1 = nLits1;
00217     *pnLits2 = nLits2;
00218         return Key;
00219 }
00220 
00233 int Fxu_PairCompare( Fxu_Pair * pPair1, Fxu_Pair * pPair2 )
00234 {
00235         Fxu_Lit * pD1C1, * pD1C2;
00236         Fxu_Lit * pD2C1, * pD2C2;
00237         int TopVar1, TopVar2;
00238         int Code;
00239 
00240         if ( pPair1->nLits1 != pPair2->nLits1 )
00241                 return 0;
00242         if ( pPair1->nLits2 != pPair2->nLits2 )
00243                 return 0;
00244 
00245         pD1C1 = pPair1->pCube1->lLits.pHead;
00246         pD1C2 = pPair1->pCube2->lLits.pHead;
00247 
00248         pD2C1 = pPair2->pCube1->lLits.pHead;
00249         pD2C2 = pPair2->pCube2->lLits.pHead;
00250 
00251         Code  = pD1C1? 8: 0;
00252         Code |= pD1C2? 4: 0;
00253         Code |= pD2C1? 2: 0;
00254         Code |= pD2C2? 1: 0;
00255         assert( Code == 15 );
00256 
00257         while ( 1 )
00258         {
00259                 switch ( Code )
00260                 {
00261                 case 0:  // -- --      NULL   NULL     NULL   NULL 
00262                         return 1;
00263                 case 1:  // -- -1      NULL   NULL     NULL   pD2C2
00264                         return 0;
00265                 case 2:  // -- 1-      NULL   NULL     pD2C1  NULL 
00266                         return 0;
00267                 case 3:  // -- 11      NULL   NULL     pD2C1  pD2C2
00268                         if ( pD2C1->iVar != pD2C2->iVar )
00269                                 return 0;
00270                         pD2C1 = pD2C1->pHNext;
00271                         pD2C2 = pD2C2->pHNext;
00272                         break;
00273                 case 4:  // -1 --      NULL   pD1C2    NULL   NULL 
00274                         return 0;
00275                 case 5:  // -1 -1      NULL   pD1C2    NULL   pD2C2
00276                         if ( pD1C2->iVar != pD2C2->iVar )
00277                                 return 0;
00278                         pD1C2 = pD1C2->pHNext;
00279                         pD2C2 = pD2C2->pHNext;
00280                         break;
00281                 case 6:  // -1 1-      NULL   pD1C2    pD2C1  NULL 
00282                         return 0;
00283                 case 7:  // -1 11      NULL   pD1C2    pD2C1  pD2C2
00284                         TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
00285                         if ( TopVar2 == pD1C2->iVar )
00286                         {
00287                                 if ( pD2C1->iVar <= pD2C2->iVar )
00288                                         return 0;
00289                                 pD1C2 = pD1C2->pHNext;
00290                                 pD2C2 = pD2C2->pHNext;
00291                         }
00292                         else if ( TopVar2 < pD1C2->iVar )
00293                         {
00294                                 if ( pD2C1->iVar != pD2C2->iVar )
00295                                         return 0;
00296                                 pD2C1 = pD2C1->pHNext;
00297                                 pD2C2 = pD2C2->pHNext;
00298                         }
00299                         else
00300                                 return 0;
00301                         break;
00302                 case 8:  // 1- --      pD1C1  NULL     NULL   NULL 
00303                         return 0;
00304                 case 9:  // 1- -1      pD1C1  NULL     NULL   pD2C2
00305                         return 0;
00306                 case 10: // 1- 1-      pD1C1  NULL     pD2C1  NULL 
00307                         if ( pD1C1->iVar != pD2C1->iVar )
00308                                 return 0;
00309                         pD1C1 = pD1C1->pHNext;
00310                         pD2C1 = pD2C1->pHNext;
00311                         break;
00312                 case 11: // 1- 11      pD1C1  NULL     pD2C1  pD2C2
00313                         TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
00314                         if ( TopVar2 == pD1C1->iVar )
00315                         {
00316                                 if ( pD2C1->iVar >= pD2C2->iVar )
00317                                         return 0;
00318                                 pD1C1 = pD1C1->pHNext;
00319                                 pD2C1 = pD2C1->pHNext;
00320                         }
00321                         else if ( TopVar2 < pD1C1->iVar )
00322                         {
00323                                 if ( pD2C1->iVar != pD2C2->iVar )
00324                                         return 0;
00325                                 pD2C1 = pD2C1->pHNext;
00326                                 pD2C2 = pD2C2->pHNext;
00327                         }
00328                         else
00329                                 return 0;
00330                         break;
00331                 case 12: // 11 --      pD1C1  pD1C2    NULL   NULL 
00332                         if ( pD1C1->iVar != pD1C2->iVar )
00333                                 return 0;
00334                         pD1C1 = pD1C1->pHNext;
00335                         pD1C2 = pD1C2->pHNext;
00336                         break;
00337                 case 13: // 11 -1      pD1C1  pD1C2    NULL   pD2C2
00338                         TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
00339                         if ( TopVar1 == pD2C2->iVar )
00340                         {
00341                                 if ( pD1C1->iVar <= pD1C2->iVar )
00342                                         return 0;
00343                                 pD1C2 = pD1C2->pHNext;
00344                                 pD2C2 = pD2C2->pHNext;
00345                         }
00346                         else if ( TopVar1 < pD2C2->iVar )
00347                         {
00348                                 if ( pD1C1->iVar != pD1C2->iVar )
00349                                         return 0;
00350                                 pD1C1 = pD1C1->pHNext;
00351                                 pD1C2 = pD1C2->pHNext;
00352                         }
00353                         else
00354                                 return 0;
00355                         break;
00356                 case 14: // 11 1-      pD1C1  pD1C2    pD2C1  NULL 
00357                         TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
00358                         if ( TopVar1 == pD2C1->iVar )
00359                         {
00360                                 if ( pD1C1->iVar >= pD1C2->iVar )
00361                                         return 0;
00362                                 pD1C1 = pD1C1->pHNext;
00363                                 pD2C1 = pD2C1->pHNext;
00364                         }
00365                         else if ( TopVar1 < pD2C1->iVar )
00366                         {
00367                                 if ( pD1C1->iVar != pD1C2->iVar )
00368                                         return 0;
00369                                 pD1C1 = pD1C1->pHNext;
00370                                 pD1C2 = pD1C2->pHNext;
00371                         }
00372                         else
00373                                 return 0;
00374                         break;
00375                 case 15: // 11 11      pD1C1  pD1C2    pD2C1  pD2C2
00376                         TopVar1 = Fxu_Min( pD1C1->iVar, pD1C2->iVar );
00377                         TopVar2 = Fxu_Min( pD2C1->iVar, pD2C2->iVar );
00378                         if ( TopVar1 == TopVar2 )
00379                         {
00380                                 if ( pD1C1->iVar == pD1C2->iVar )
00381                                 {
00382                                         if ( pD2C1->iVar != pD2C2->iVar )
00383                                                 return 0;
00384                                         pD1C1 = pD1C1->pHNext;
00385                                         pD1C2 = pD1C2->pHNext;
00386                                         pD2C1 = pD2C1->pHNext;
00387                                         pD2C2 = pD2C2->pHNext;
00388                                 }
00389                                 else
00390                                 {
00391                                         if ( pD2C1->iVar == pD2C2->iVar )
00392                                                 return 0;
00393                                         if ( pD1C1->iVar < pD1C2->iVar )
00394                                         {
00395                                                 if ( pD2C1->iVar > pD2C2->iVar )
00396                                                         return 0;
00397                                                 pD1C1 = pD1C1->pHNext;
00398                                                 pD2C1 = pD2C1->pHNext;
00399                                         }
00400                                         else
00401                                         {
00402                                                 if ( pD2C1->iVar < pD2C2->iVar )
00403                                                         return 0;
00404                                                 pD1C2 = pD1C2->pHNext;
00405                                                 pD2C2 = pD2C2->pHNext;
00406                                         }
00407                                 }
00408                         }
00409                         else if ( TopVar1 < TopVar2 )
00410                         {
00411                                 if ( pD1C1->iVar != pD1C2->iVar )
00412                                         return 0;
00413                                 pD1C1 = pD1C1->pHNext;
00414                                 pD1C2 = pD1C2->pHNext;
00415                         }
00416                         else 
00417                         {
00418                                 if ( pD2C1->iVar != pD2C2->iVar )
00419                                         return 0;
00420                                 pD2C1 = pD2C1->pHNext;
00421                                 pD2C2 = pD2C2->pHNext;
00422                         }
00423                         break;
00424                 default:
00425                         assert( 0 );
00426                         break;
00427                 }
00428 
00429                 Code  = pD1C1? 8: 0;
00430                 Code |= pD1C2? 4: 0;
00431                 Code |= pD2C1? 2: 0;
00432                 Code |= pD2C2? 1: 0;
00433         }
00434         return 1;
00435 }
00436 
00437 
00449 void Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes )
00450 {
00451     int k;
00452 //    assert( pVar->nCubes == 0 );
00453     pVar->nCubes  = nCubes;
00454         // allocate memory for all the pairs
00455         pVar->ppPairs    = ALLOC( Fxu_Pair **, nCubes );
00456         pVar->ppPairs[0] = ALLOC( Fxu_Pair *,  nCubes * nCubes );
00457     memset( pVar->ppPairs[0], 0, sizeof(Fxu_Pair *) * nCubes * nCubes );
00458     for ( k = 1; k < nCubes; k++ )
00459         pVar->ppPairs[k] = pVar->ppPairs[k-1] + nCubes;
00460 }
00461 
00473 void Fxu_PairClearStorage( Fxu_Cube * pCube )
00474 {
00475     Fxu_Var * pVar;
00476         int i;
00477     pVar = pCube->pVar;
00478         for ( i = 0; i < pVar->nCubes; i++ )
00479         {
00480                 pVar->ppPairs[pCube->iCube][i] = NULL;
00481                 pVar->ppPairs[i][pCube->iCube] = NULL;
00482         }
00483 }
00484 
00496 void Fxu_PairFreeStorage( Fxu_Var * pVar )
00497 {
00498     if ( pVar->ppPairs )
00499     {
00500         FREE( pVar->ppPairs[0] );
00501         FREE( pVar->ppPairs );
00502     }
00503 }
00504 
00516 Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 )
00517 {
00518     Fxu_Pair * pPair;
00519         assert( pCube1->pVar == pCube2->pVar );
00520         pPair = MEM_ALLOC_FXU( p, Fxu_Pair, 1 );
00521         memset( pPair, 0, sizeof(Fxu_Pair) );
00522         pPair->pCube1 = pCube1;
00523         pPair->pCube2 = pCube2;
00524         pPair->iCube1 = pCube1->iCube;
00525         pPair->iCube2 = pCube2->iCube;
00526     return pPair;
00527 }
00528 
00540 void Fxu_PairAdd( Fxu_Pair * pPair )
00541 {
00542     Fxu_Var * pVar;
00543 
00544     pVar = pPair->pCube1->pVar;
00545         assert( pVar == pPair->pCube2->pVar );
00546 
00547         pVar->ppPairs[pPair->iCube1][pPair->iCube2] = pPair;
00548         pVar->ppPairs[pPair->iCube2][pPair->iCube1] = pPair;
00549 }
00550 
00554 
00555