src/misc/extra/extraUtilTruth.c File Reference

#include "extra.h"
Include dependency graph for extraUtilTruth.c:

Go to the source code of this file.

Functions

unsigned ** Extra_TruthElementary (int nVars)
void Extra_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
void Extra_TruthSwapAdjacentVars2 (unsigned *pIn, unsigned *pOut, int nVars, int Start)
void Extra_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
void Extra_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase)
int Extra_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
int Extra_TruthSupportSize (unsigned *pTruth, int nVars)
int Extra_TruthSupport (unsigned *pTruth, int nVars)
void Extra_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
void Extra_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
void Extra_TruthExist (unsigned *pTruth, int nVars, int iVar)
void Extra_TruthForall (unsigned *pTruth, int nVars, int iVar)
void Extra_TruthMux (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
int Extra_TruthVarsSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1)
int Extra_TruthVarsAntiSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1)
void Extra_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
int Extra_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
void Extra_TruthCountOnesInCofs (unsigned *pTruth, int nVars, short *pStore)
unsigned Extra_TruthHash (unsigned *pIn, int nWords)
unsigned Extra_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm, short *pStore)

Variables

static unsigned s_VarMasks [5][2]

Function Documentation

void Extra_TruthChangePhase ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Changes phase of the function w.r.t. one variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 716 of file extraUtilTruth.c.

00717 {
00718     int nWords = Extra_TruthWordNum( nVars );
00719     int i, k, Step;
00720     unsigned Temp;
00721 
00722     assert( iVar < nVars );
00723     switch ( iVar )
00724     {
00725     case 0:
00726         for ( i = 0; i < nWords; i++ )
00727             pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
00728         return;
00729     case 1:
00730         for ( i = 0; i < nWords; i++ )
00731             pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
00732         return;
00733     case 2:
00734         for ( i = 0; i < nWords; i++ )
00735             pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
00736         return;
00737     case 3:
00738         for ( i = 0; i < nWords; i++ )
00739             pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
00740         return;
00741     case 4:
00742         for ( i = 0; i < nWords; i++ )
00743             pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
00744         return;
00745     default:
00746         Step = (1 << (iVar - 5));
00747         for ( k = 0; k < nWords; k += 2*Step )
00748         {
00749             for ( i = 0; i < Step; i++ )
00750             {
00751                 Temp = pTruth[i];
00752                 pTruth[i] = pTruth[Step+i];
00753                 pTruth[Step+i] = Temp;
00754             }
00755             pTruth += 2*Step;
00756         }
00757         return;
00758     }
00759 }

void Extra_TruthCofactor0 ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 447 of file extraUtilTruth.c.

00448 {
00449     int nWords = Extra_TruthWordNum( nVars );
00450     int i, k, Step;
00451 
00452     assert( iVar < nVars );
00453     switch ( iVar )
00454     {
00455     case 0:
00456         for ( i = 0; i < nWords; i++ )
00457             pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
00458         return;
00459     case 1:
00460         for ( i = 0; i < nWords; i++ )
00461             pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
00462         return;
00463     case 2:
00464         for ( i = 0; i < nWords; i++ )
00465             pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00466         return;
00467     case 3:
00468         for ( i = 0; i < nWords; i++ )
00469             pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
00470         return;
00471     case 4:
00472         for ( i = 0; i < nWords; i++ )
00473             pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
00474         return;
00475     default:
00476         Step = (1 << (iVar - 5));
00477         for ( k = 0; k < nWords; k += 2*Step )
00478         {
00479             for ( i = 0; i < Step; i++ )
00480                 pTruth[Step+i] = pTruth[i];
00481             pTruth += 2*Step;
00482         }
00483         return;
00484     }
00485 }

void Extra_TruthCofactor1 ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 396 of file extraUtilTruth.c.

00397 {
00398     int nWords = Extra_TruthWordNum( nVars );
00399     int i, k, Step;
00400 
00401     assert( iVar < nVars );
00402     switch ( iVar )
00403     {
00404     case 0:
00405         for ( i = 0; i < nWords; i++ )
00406             pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
00407         return;
00408     case 1:
00409         for ( i = 0; i < nWords; i++ )
00410             pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
00411         return;
00412     case 2:
00413         for ( i = 0; i < nWords; i++ )
00414             pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
00415         return;
00416     case 3:
00417         for ( i = 0; i < nWords; i++ )
00418             pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
00419         return;
00420     case 4:
00421         for ( i = 0; i < nWords; i++ )
00422             pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
00423         return;
00424     default:
00425         Step = (1 << (iVar - 5));
00426         for ( k = 0; k < nWords; k += 2*Step )
00427         {
00428             for ( i = 0; i < Step; i++ )
00429                 pTruth[i] = pTruth[Step+i];
00430             pTruth += 2*Step;
00431         }
00432         return;
00433     }
00434 }

void Extra_TruthCountOnesInCofs ( unsigned *  pTruth,
int  nVars,
short *  pStore 
)

Function*************************************************************

Synopsis [Counts the number of 1's in each cofactor.]

Description [The resulting numbers are stored in the array of shorts, whose length is 2*nVars. The number of 1's is counted in a different space than the original function. For example, if the function depends on k variables, the cofactors are assumed to depend on k-1 variables.]

SideEffects []

SeeAlso []

Definition at line 825 of file extraUtilTruth.c.

00826 {
00827     int nWords = Extra_TruthWordNum( nVars );
00828     int i, k, Counter;
00829     memset( pStore, 0, sizeof(short) * 2 * nVars );
00830     if ( nVars <= 5 )
00831     {
00832         if ( nVars > 0 )
00833         {
00834             pStore[2*0+0] = Extra_WordCountOnes( pTruth[0] & 0x55555555 );
00835             pStore[2*0+1] = Extra_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
00836         }
00837         if ( nVars > 1 )
00838         {
00839             pStore[2*1+0] = Extra_WordCountOnes( pTruth[0] & 0x33333333 );
00840             pStore[2*1+1] = Extra_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
00841         }
00842         if ( nVars > 2 )
00843         {
00844             pStore[2*2+0] = Extra_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
00845             pStore[2*2+1] = Extra_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
00846         }
00847         if ( nVars > 3 )
00848         {
00849             pStore[2*3+0] = Extra_WordCountOnes( pTruth[0] & 0x00FF00FF );
00850             pStore[2*3+1] = Extra_WordCountOnes( pTruth[0] & 0xFF00FF00 );
00851         }
00852         if ( nVars > 4 )
00853         {
00854             pStore[2*4+0] = Extra_WordCountOnes( pTruth[0] & 0x0000FFFF );
00855             pStore[2*4+1] = Extra_WordCountOnes( pTruth[0] & 0xFFFF0000 );
00856         }
00857         return;
00858     }
00859     // nVars >= 6
00860     // count 1's for all other variables
00861     for ( k = 0; k < nWords; k++ )
00862     {
00863         Counter = Extra_WordCountOnes( pTruth[k] );
00864         for ( i = 5; i < nVars; i++ )
00865             if ( k & (1 << (i-5)) )
00866                 pStore[2*i+1] += Counter;
00867             else
00868                 pStore[2*i+0] += Counter;
00869     }
00870     // count 1's for the first five variables
00871     for ( k = 0; k < nWords/2; k++ )
00872     {
00873         pStore[2*0+0] += Extra_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
00874         pStore[2*0+1] += Extra_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >>  1) );
00875         pStore[2*1+0] += Extra_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
00876         pStore[2*1+1] += Extra_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >>  2) );
00877         pStore[2*2+0] += Extra_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
00878         pStore[2*2+1] += Extra_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >>  4) );
00879         pStore[2*3+0] += Extra_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
00880         pStore[2*3+1] += Extra_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >>  8) );
00881         pStore[2*4+0] += Extra_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
00882         pStore[2*4+1] += Extra_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
00883         pTruth += 2;
00884     }
00885 }

unsigned** Extra_TruthElementary ( int  nVars  ) 

AutomaticStart AutomaticEnd Function*************************************************************

Synopsis [Derive elementary truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 74 of file extraUtilTruth.c.

00075 {
00076     unsigned ** pRes;
00077     int i, k, nWords;
00078     nWords = Extra_TruthWordNum(nVars);
00079     pRes = (unsigned **)Extra_ArrayAlloc( nVars, nWords, 4 );
00080     for ( i = 0; i < nVars; i++ )
00081     {
00082         if ( i < 5 )
00083         {
00084             for ( k = 0; k < nWords; k++ )
00085                 pRes[i][k] = s_VarMasks[i][1];
00086         }
00087         else
00088         {
00089             for ( k = 0; k < nWords; k++ )
00090                 if ( k & (1 << (i-5)) )
00091                     pRes[i][k] = ~(unsigned)0;
00092                 else
00093                     pRes[i][k] = 0;
00094         }
00095     }
00096     return pRes;
00097 }

void Extra_TruthExist ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file extraUtilTruth.c.

00500 {
00501     int nWords = Extra_TruthWordNum( nVars );
00502     int i, k, Step;
00503 
00504     assert( iVar < nVars );
00505     switch ( iVar )
00506     {
00507     case 0:
00508         for ( i = 0; i < nWords; i++ )
00509             pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00510         return;
00511     case 1:
00512         for ( i = 0; i < nWords; i++ )
00513             pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00514         return;
00515     case 2:
00516         for ( i = 0; i < nWords; i++ )
00517             pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00518         return;
00519     case 3:
00520         for ( i = 0; i < nWords; i++ )
00521             pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00522         return;
00523     case 4:
00524         for ( i = 0; i < nWords; i++ )
00525             pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00526         return;
00527     default:
00528         Step = (1 << (iVar - 5));
00529         for ( k = 0; k < nWords; k += 2*Step )
00530         {
00531             for ( i = 0; i < Step; i++ )
00532             {
00533                 pTruth[i]     |= pTruth[Step+i];
00534                 pTruth[Step+i] = pTruth[i];
00535             }
00536             pTruth += 2*Step;
00537         }
00538         return;
00539     }
00540 }

void Extra_TruthForall ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 553 of file extraUtilTruth.c.

00554 {
00555     int nWords = Extra_TruthWordNum( nVars );
00556     int i, k, Step;
00557 
00558     assert( iVar < nVars );
00559     switch ( iVar )
00560     {
00561     case 0:
00562         for ( i = 0; i < nWords; i++ )
00563             pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00564         return;
00565     case 1:
00566         for ( i = 0; i < nWords; i++ )
00567             pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00568         return;
00569     case 2:
00570         for ( i = 0; i < nWords; i++ )
00571             pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00572         return;
00573     case 3:
00574         for ( i = 0; i < nWords; i++ )
00575             pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00576         return;
00577     case 4:
00578         for ( i = 0; i < nWords; i++ )
00579             pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00580         return;
00581     default:
00582         Step = (1 << (iVar - 5));
00583         for ( k = 0; k < nWords; k += 2*Step )
00584         {
00585             for ( i = 0; i < Step; i++ )
00586             {
00587                 pTruth[i]     &= pTruth[Step+i];
00588                 pTruth[Step+i] = pTruth[i];
00589             }
00590             pTruth += 2*Step;
00591         }
00592         return;
00593     }
00594 }

unsigned Extra_TruthHash ( unsigned *  pIn,
int  nWords 
)

Function*************************************************************

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 899 of file extraUtilTruth.c.

00900 {
00901     // The 1,024 smallest prime numbers used to compute the hash value
00902     // http://www.math.utah.edu/~alfeld/math/primelist.html
00903     static int HashPrimes[1024] = { 2, 3, 5, 
00904     7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 
00905     101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, 
00906     193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, 
00907     293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401, 
00908     409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509, 
00909     521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631, 
00910     641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751, 
00911     757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877, 
00912     881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, 
00913     1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091, 
00914     1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193, 
00915     1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291, 
00916     1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 
00917     1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 
00918     1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, 
00919     1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699, 
00920     1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811, 
00921     1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931, 
00922     1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029, 
00923     2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137, 
00924     2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267, 
00925     2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357, 
00926     2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459, 
00927     2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593, 
00928     2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693, 
00929     2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791, 
00930     2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903, 
00931     2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023, 
00932     3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167, 
00933     3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271, 
00934     3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373, 
00935     3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511, 
00936     3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607, 
00937     3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709, 
00938     3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833, 
00939     3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931, 
00940     3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057, 
00941     4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177, 
00942     4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283, 
00943     4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423, 
00944     4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547, 
00945     4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657, 
00946     4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789, 
00947     4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931, 
00948     4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011, 
00949     5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147, 
00950     5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279, 
00951     5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413, 
00952     5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507, 
00953     5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647, 
00954     5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743, 
00955     5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857, 
00956     5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007, 
00957     6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121, 
00958     6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247, 
00959     6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343, 
00960     6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473, 
00961     6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607, 
00962     6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733, 
00963     6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857, 
00964     6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971, 
00965     6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103, 
00966     7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229, 
00967     7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369, 
00968     7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517, 
00969     7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 
00970     7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 
00971     7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, 
00972     7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
00973     8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
00974     8147, 8161 };
00975     int i;
00976     unsigned uHashKey;
00977     assert( nWords <= 1024 );
00978     uHashKey = 0;
00979     for ( i = 0; i < nWords; i++ )
00980         uHashKey ^= HashPrimes[i] * pIn[i];
00981     return uHashKey;
00982 }

int Extra_TruthMinCofSuppOverlap ( unsigned *  pTruth,
int  nVars,
int *  pVarMin 
)

Function*************************************************************

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 772 of file extraUtilTruth.c.

00773 {
00774     static unsigned uCofactor[16];
00775     int i, ValueCur, ValueMin, VarMin;
00776     unsigned uSupp0, uSupp1;
00777     int nVars0, nVars1;
00778     assert( nVars <= 9 );
00779     ValueMin = 32;
00780     VarMin   = -1;
00781     for ( i = 0; i < nVars; i++ )
00782     {
00783         // get negative cofactor
00784         Extra_TruthCopy( uCofactor, pTruth, nVars );
00785         Extra_TruthCofactor0( uCofactor, nVars, i );
00786         uSupp0 = Extra_TruthSupport( uCofactor, nVars );
00787         nVars0 = Extra_WordCountOnes( uSupp0 );
00788 //Extra_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
00789         // get positive cofactor
00790         Extra_TruthCopy( uCofactor, pTruth, nVars );
00791         Extra_TruthCofactor1( uCofactor, nVars, i );
00792         uSupp1 = Extra_TruthSupport( uCofactor, nVars );
00793         nVars1 = Extra_WordCountOnes( uSupp1 );
00794 //Extra_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
00795         // get the number of common vars
00796         ValueCur = Extra_WordCountOnes( uSupp0 & uSupp1 );
00797         if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
00798         {
00799             ValueMin = ValueCur;
00800             VarMin = i;
00801         }
00802         if ( ValueMin == 0 )
00803             break;
00804     }
00805     if ( pVarMin )
00806         *pVarMin = VarMin;
00807     return ValueMin;
00808 }

void Extra_TruthMux ( unsigned *  pOut,
unsigned *  pCof0,
unsigned *  pCof1,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 608 of file extraUtilTruth.c.

00609 {
00610     int nWords = Extra_TruthWordNum( nVars );
00611     int i, k, Step;
00612 
00613     assert( iVar < nVars );
00614     switch ( iVar )
00615     {
00616     case 0:
00617         for ( i = 0; i < nWords; i++ )
00618             pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
00619         return;
00620     case 1:
00621         for ( i = 0; i < nWords; i++ )
00622             pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
00623         return;
00624     case 2:
00625         for ( i = 0; i < nWords; i++ )
00626             pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
00627         return;
00628     case 3:
00629         for ( i = 0; i < nWords; i++ )
00630             pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
00631         return;
00632     case 4:
00633         for ( i = 0; i < nWords; i++ )
00634             pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
00635         return;
00636     default:
00637         Step = (1 << (iVar - 5));
00638         for ( k = 0; k < nWords; k += 2*Step )
00639         {
00640             for ( i = 0; i < Step; i++ )
00641             {
00642                 pOut[i]      = pCof0[i];
00643                 pOut[Step+i] = pCof1[Step+i];
00644             }
00645             pOut += 2*Step;
00646         }
00647         return;
00648     }
00649 }

unsigned Extra_TruthSemiCanonicize ( unsigned *  pInOut,
unsigned *  pAux,
int  nVars,
char *  pCanonPerm,
short *  pStore 
)

Function*************************************************************

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 996 of file extraUtilTruth.c.

00997 {
00998     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
00999     int nWords = Extra_TruthWordNum( nVars );
01000     int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
01001     unsigned uCanonPhase;
01002 
01003     // canonicize output
01004     uCanonPhase = 0;
01005     nOnes = Extra_TruthCountOnes(pIn, nVars);
01006     if ( (nOnes > nWords * 16) || ((nOnes == nWords * 16) && (pIn[0] & 1)) )
01007     {
01008         uCanonPhase |= (1 << nVars);
01009         Extra_TruthNot( pIn, pIn, nVars );
01010     }
01011 
01012     // collect the minterm counts
01013     Extra_TruthCountOnesInCofs( pIn, nVars, pStore );
01014 
01015     // canonicize phase
01016     for ( i = 0; i < nVars; i++ )
01017     {
01018         if ( pStore[2*i+0] <= pStore[2*i+1] )
01019             continue;
01020         uCanonPhase |= (1 << i);
01021         Temp = pStore[2*i+0];
01022         pStore[2*i+0] = pStore[2*i+1];
01023         pStore[2*i+1] = Temp;
01024         Extra_TruthChangePhase( pIn, nVars, i );
01025     }
01026 
01027 //    Extra_PrintHexadecimal( stdout, pIn, nVars );
01028 //    printf( "\n" );
01029 
01030     // permute
01031     Counter = 0;
01032     do {
01033         fChange = 0;
01034         for ( i = 0; i < nVars-1; i++ )
01035         {
01036             if ( pStore[2*i] <= pStore[2*(i+1)] )
01037                 continue;
01038             Counter++;
01039             fChange = 1;
01040 
01041             Temp = pCanonPerm[i];
01042             pCanonPerm[i] = pCanonPerm[i+1];
01043             pCanonPerm[i+1] = Temp;
01044 
01045             Temp = pStore[2*i];
01046             pStore[2*i] = pStore[2*(i+1)];
01047             pStore[2*(i+1)] = Temp;
01048 
01049             Temp = pStore[2*i+1];
01050             pStore[2*i+1] = pStore[2*(i+1)+1];
01051             pStore[2*(i+1)+1] = Temp;
01052 
01053             Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
01054             pTemp = pIn; pIn = pOut; pOut = pTemp;
01055         }
01056     } while ( fChange );
01057 
01058 /*
01059     Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
01060     for ( i = 0; i < nVars; i++ )
01061         printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
01062     printf( "  C = %d\n", Counter );
01063     Extra_PrintHexadecimal( stdout, pIn, nVars );
01064     printf( "\n" );
01065 */
01066 
01067 /*
01068     // process symmetric variable groups
01069     uSymms = 0;
01070     for ( i = 0; i < nVars-1; i++ )
01071     {
01072         if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
01073             continue;
01074         if ( pStore[2*i] != pStore[2*i+1] )
01075             continue;
01076         if ( Extra_TruthVarsSymm( pIn, nVars, i, i+1 ) )
01077             continue;
01078         if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
01079             Extra_TruthChangePhase( pIn, nVars, i+1 );
01080     }
01081 */
01082 
01083 /*
01084     // process symmetric variable groups
01085     uSymms = 0;
01086     for ( i = 0; i < nVars-1; i++ )
01087     {
01088         if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
01089             continue;
01090         // i and i+1 can be symmetric
01091         // find the end of this group
01092         for ( k = i+1; k < nVars; k++ )
01093             if ( pStore[2*i] != pStore[2*k] ) 
01094                 break;
01095         Limit = k;
01096         assert( i < Limit-1 );
01097         // go through the variables in this group
01098         for ( j = i + 1; j < Limit; j++ )
01099         {
01100             // check symmetry
01101             if ( Extra_TruthVarsSymm( pIn, nVars, i, j ) )
01102             {
01103                 uSymms |= (1 << j);
01104                 continue;
01105             }
01106             // they are phase-unknown
01107             if ( pStore[2*i] == pStore[2*i+1] ) 
01108             {
01109                 if ( Extra_TruthVarsAntiSymm( pIn, nVars, i, j ) )
01110                 {
01111                     Extra_TruthChangePhase( pIn, nVars, j );
01112                     uCanonPhase ^= (1 << j);
01113                     uSymms |= (1 << j);
01114                     continue;
01115                 }
01116             }
01117 
01118             // they are not symmetric - move j as far as it goes in the group
01119             for ( k = j; k < Limit-1; k++ )
01120             {
01121                 Counter++;
01122 
01123                 Temp = pCanonPerm[k];
01124                 pCanonPerm[k] = pCanonPerm[k+1];
01125                 pCanonPerm[k+1] = Temp;
01126 
01127                 assert( pStore[2*k] == pStore[2*(k+1)] );
01128                 Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
01129                 pTemp = pIn; pIn = pOut; pOut = pTemp;
01130             }
01131             Limit--;
01132             j--;
01133         }
01134         i = Limit - 1;
01135     }
01136 */
01137 
01138     // swap if it was moved an even number of times
01139     if ( Counter & 1 )
01140         Extra_TruthCopy( pOut, pIn, nVars );
01141     return uCanonPhase;
01142 }

void Extra_TruthShrink ( unsigned *  pOut,
unsigned *  pIn,
int  nVars,
int  nVarsAll,
unsigned  Phase 
)

Function*************************************************************

Synopsis [Shrinks the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows what variables should remain.]

SideEffects []

SeeAlso []

Definition at line 265 of file extraUtilTruth.c.

00266 {
00267     unsigned * pTemp;
00268     int i, k, Var = 0, Counter = 0;
00269     for ( i = 0; i < nVarsAll; i++ )
00270         if ( Phase & (1 << i) )
00271         {
00272             for ( k = i-1; k >= Var; k-- )
00273             {
00274                 Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
00275                 pTemp = pIn; pIn = pOut; pOut = pTemp;
00276                 Counter++;
00277             }
00278             Var++;
00279         }
00280     assert( Var == nVars );
00281     // swap if it was moved an even number of times
00282     if ( !(Counter & 1) )
00283         Extra_TruthCopy( pOut, pIn, nVarsAll );
00284 }

void Extra_TruthStretch ( unsigned *  pOut,
unsigned *  pIn,
int  nVars,
int  nVarsAll,
unsigned  Phase 
)

Function*************************************************************

Synopsis [Expands the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows where the variables should go.]

SideEffects []

SeeAlso []

Definition at line 231 of file extraUtilTruth.c.

00232 {
00233     unsigned * pTemp;
00234     int i, k, Var = nVars - 1, Counter = 0;
00235     for ( i = nVarsAll - 1; i >= 0; i-- )
00236         if ( Phase & (1 << i) )
00237         {
00238             for ( k = Var; k < i; k++ )
00239             {
00240                 Extra_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
00241                 pTemp = pIn; pIn = pOut; pOut = pTemp;
00242                 Counter++;
00243             }
00244             Var--;
00245         }
00246     assert( Var == -1 );
00247     // swap if it was moved an even number of times
00248     if ( !(Counter & 1) )
00249         Extra_TruthCopy( pOut, pIn, nVarsAll );
00250 }

int Extra_TruthSupport ( unsigned *  pTruth,
int  nVars 
)

Function*************************************************************

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 374 of file extraUtilTruth.c.

00375 {
00376     int i, Support = 0;
00377     for ( i = 0; i < nVars; i++ )
00378         if ( Extra_TruthVarInSupport( pTruth, nVars, i ) )
00379             Support |= (1 << i);
00380     return Support;
00381 }

int Extra_TruthSupportSize ( unsigned *  pTruth,
int  nVars 
)

Function*************************************************************

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 355 of file extraUtilTruth.c.

00356 {
00357     int i, Counter = 0;
00358     for ( i = 0; i < nVars; i++ )
00359         Counter += Extra_TruthVarInSupport( pTruth, nVars, i );
00360     return Counter;
00361 }

void Extra_TruthSwapAdjacentVars ( unsigned *  pOut,
unsigned *  pIn,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Swaps two adjacent variables in the truth table.]

Description [Swaps var number Start and var number Start+1 (0-based numbers). The input truth table is pIn. The output truth table is pOut.]

SideEffects []

SeeAlso []

Definition at line 111 of file extraUtilTruth.c.

00112 {
00113     static unsigned PMasks[4][3] = {
00114         { 0x99999999, 0x22222222, 0x44444444 },
00115         { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
00116         { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
00117         { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
00118     };
00119     int nWords = Extra_TruthWordNum( nVars );
00120     int i, k, Step, Shift;
00121 
00122     assert( iVar < nVars - 1 );
00123     if ( iVar < 4 )
00124     {
00125         Shift = (1 << iVar);
00126         for ( i = 0; i < nWords; i++ )
00127             pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
00128     }
00129     else if ( iVar > 4 )
00130     {
00131         Step = (1 << (iVar - 5));
00132         for ( k = 0; k < nWords; k += 4*Step )
00133         {
00134             for ( i = 0; i < Step; i++ )
00135                 pOut[i] = pIn[i];
00136             for ( i = 0; i < Step; i++ )
00137                 pOut[Step+i] = pIn[2*Step+i];
00138             for ( i = 0; i < Step; i++ )
00139                 pOut[2*Step+i] = pIn[Step+i];
00140             for ( i = 0; i < Step; i++ )
00141                 pOut[3*Step+i] = pIn[3*Step+i];
00142             pIn  += 4*Step;
00143             pOut += 4*Step;
00144         }
00145     }
00146     else // if ( iVar == 4 )
00147     {
00148         for ( i = 0; i < nWords; i += 2 )
00149         {
00150             pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
00151             pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
00152         }
00153     }
00154 }

void Extra_TruthSwapAdjacentVars2 ( unsigned *  pIn,
unsigned *  pOut,
int  nVars,
int  Start 
)

Function*************************************************************

Synopsis [Swaps two adjacent variables in the truth table.]

Description [Swaps var number Start and var number Start+1 (0-based numbers). The input truth table is pIn. The output truth table is pOut.]

SideEffects []

SeeAlso []

Definition at line 168 of file extraUtilTruth.c.

00169 {
00170     int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
00171     int i, k, Step;
00172 
00173     assert( Start < nVars - 1 );
00174     switch ( Start )
00175     {
00176     case 0:
00177         for ( i = 0; i < nWords; i++ )
00178             pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
00179         return;
00180     case 1:
00181         for ( i = 0; i < nWords; i++ )
00182             pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
00183         return;
00184     case 2:
00185         for ( i = 0; i < nWords; i++ )
00186             pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
00187         return;
00188     case 3:
00189         for ( i = 0; i < nWords; i++ )
00190             pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
00191         return;
00192     case 4:
00193         for ( i = 0; i < nWords; i += 2 )
00194         {
00195             pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
00196             pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
00197         }
00198         return;
00199     default:
00200         Step = (1 << (Start - 5));
00201         for ( k = 0; k < nWords; k += 4*Step )
00202         {
00203             for ( i = 0; i < Step; i++ )
00204                 pOut[i] = pIn[i];
00205             for ( i = 0; i < Step; i++ )
00206                 pOut[Step+i] = pIn[2*Step+i];
00207             for ( i = 0; i < Step; i++ )
00208                 pOut[2*Step+i] = pIn[Step+i];
00209             for ( i = 0; i < Step; i++ )
00210                 pOut[3*Step+i] = pIn[3*Step+i];
00211             pIn  += 4*Step;
00212             pOut += 4*Step;
00213         }
00214         return;
00215     }
00216 }

int Extra_TruthVarInSupport ( unsigned *  pTruth,
int  nVars,
int  iVar 
)

Function*************************************************************

Synopsis [Returns 1 if TT depends on the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 298 of file extraUtilTruth.c.

00299 {
00300     int nWords = Extra_TruthWordNum( nVars );
00301     int i, k, Step;
00302 
00303     assert( iVar < nVars );
00304     switch ( iVar )
00305     {
00306     case 0:
00307         for ( i = 0; i < nWords; i++ )
00308             if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
00309                 return 1;
00310         return 0;
00311     case 1:
00312         for ( i = 0; i < nWords; i++ )
00313             if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
00314                 return 1;
00315         return 0;
00316     case 2:
00317         for ( i = 0; i < nWords; i++ )
00318             if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
00319                 return 1;
00320         return 0;
00321     case 3:
00322         for ( i = 0; i < nWords; i++ )
00323             if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
00324                 return 1;
00325         return 0;
00326     case 4:
00327         for ( i = 0; i < nWords; i++ )
00328             if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
00329                 return 1;
00330         return 0;
00331     default:
00332         Step = (1 << (iVar - 5));
00333         for ( k = 0; k < nWords; k += 2*Step )
00334         {
00335             for ( i = 0; i < Step; i++ )
00336                 if ( pTruth[i] != pTruth[Step+i] )
00337                     return 1;
00338             pTruth += 2*Step;
00339         }
00340         return 0;
00341     }
00342 }

int Extra_TruthVarsAntiSymm ( unsigned *  pTruth,
int  nVars,
int  iVar0,
int  iVar1 
)

Function*************************************************************

Synopsis [Checks antisymmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 689 of file extraUtilTruth.c.

00690 {
00691     static unsigned uTemp0[16], uTemp1[16];
00692     assert( nVars <= 9 );
00693     // compute Cof00
00694     Extra_TruthCopy( uTemp0, pTruth, nVars );
00695     Extra_TruthCofactor0( uTemp0, nVars, iVar0 );
00696     Extra_TruthCofactor0( uTemp0, nVars, iVar1 );
00697     // compute Cof11
00698     Extra_TruthCopy( uTemp1, pTruth, nVars );
00699     Extra_TruthCofactor1( uTemp1, nVars, iVar0 );
00700     Extra_TruthCofactor1( uTemp1, nVars, iVar1 );
00701     // compare
00702     return Extra_TruthIsEqual( uTemp0, uTemp1, nVars );
00703 }

int Extra_TruthVarsSymm ( unsigned *  pTruth,
int  nVars,
int  iVar0,
int  iVar1 
)

Function*************************************************************

Synopsis [Checks symmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 662 of file extraUtilTruth.c.

00663 {
00664     static unsigned uTemp0[16], uTemp1[16];
00665     assert( nVars <= 9 );
00666     // compute Cof01
00667     Extra_TruthCopy( uTemp0, pTruth, nVars );
00668     Extra_TruthCofactor0( uTemp0, nVars, iVar0 );
00669     Extra_TruthCofactor1( uTemp0, nVars, iVar1 );
00670     // compute Cof10
00671     Extra_TruthCopy( uTemp1, pTruth, nVars );
00672     Extra_TruthCofactor1( uTemp1, nVars, iVar0 );
00673     Extra_TruthCofactor0( uTemp1, nVars, iVar1 );
00674     // compare
00675     return Extra_TruthIsEqual( uTemp0, uTemp1, nVars );
00676 }

Variable Documentation

unsigned s_VarMasks[5][2] [static]
Initial value:
 {
    { 0x33333333, 0xAAAAAAAA },
    { 0x55555555, 0xCCCCCCCC },
    { 0x0F0F0F0F, 0xF0F0F0F0 },
    { 0x00FF00FF, 0xFF00FF00 },
    { 0x0000FFFF, 0xFFFF0000 }
}

CFile****************************************************************

FileName [extraUtilMisc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [Various procedures for truth table manipulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp

]

Definition at line 39 of file extraUtilTruth.c.

Generated on Tue Jan 5 12:19:15 2010 for abc70930 by  doxygen 1.6.1