src/aig/kit/kitTruth.c File Reference

#include "kit.h"
Include dependency graph for kitTruth.c:

Go to the source code of this file.

Functions

void Kit_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
void Kit_TruthSwapAdjacentVars2 (unsigned *pIn, unsigned *pOut, int nVars, int Start)
void Kit_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
void Kit_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
int Kit_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
int Kit_TruthSupportSize (unsigned *pTruth, int nVars)
unsigned Kit_TruthSupport (unsigned *pTruth, int nVars)
void Kit_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
void Kit_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
void Kit_TruthCofactor0New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
void Kit_TruthCofactor1New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
void Kit_TruthExist (unsigned *pTruth, int nVars, int iVar)
void Kit_TruthExistNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void Kit_TruthExistSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
void Kit_TruthForall (unsigned *pTruth, int nVars, int iVar)
void Kit_TruthForallNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void Kit_TruthUniqueNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void Kit_TruthForallSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
void Kit_TruthMuxVar (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
void Kit_TruthMuxVarPhase (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
int Kit_TruthVarsSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1)
int Kit_TruthVarsAntiSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1)
void Kit_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
int Kit_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
int Kit_TruthBestCofVar (unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
void Kit_TruthCountOnesInCofs (unsigned *pTruth, int nVars, short *pStore)
void Kit_TruthCountOnesInCofsSlow (unsigned *pTruth, int nVars, short *pStore, unsigned *pAux)
unsigned Kit_TruthHash (unsigned *pIn, int nWords)
unsigned Kit_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm, short *pStore)
int Kit_TruthCountMinterms (unsigned *pTruth, int nVars, int *pRes, int *pBytes)
void Kit_PrintHexadecimal (FILE *pFile, unsigned Sign[], int nVars)
void Kit_TruthCountMintermsPrecomp ()
char * Kit_TruthDumpToFile (unsigned *pTruth, int nVars, int nFile)

Function Documentation

void Kit_PrintHexadecimal ( FILE *  pFile,
unsigned  Sign[],
int  nVars 
)

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

Synopsis [Prints the hex unsigned into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1638 of file kitTruth.c.

01639 {
01640     int nDigits, Digit, k;
01641     // write the number into the file
01642     nDigits = (1 << nVars) / 4;
01643     for ( k = nDigits - 1; k >= 0; k-- )
01644     {
01645         Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15);
01646         if ( Digit < 10 )
01647             fprintf( pFile, "%d", Digit );
01648         else
01649             fprintf( pFile, "%c", 'a' + Digit-10 );
01650     }
01651 //    fprintf( pFile, "\n" );
01652 }

int Kit_TruthBestCofVar ( unsigned *  pTruth,
int  nVars,
unsigned *  pCof0,
unsigned *  pCof1 
)

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

Synopsis [Find the best cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1127 of file kitTruth.c.

01128 {
01129     int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
01130     if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
01131         return -1;
01132     // iterate through variables
01133     iBestVar = -1;
01134     nSuppSizeMin = KIT_INFINITY;
01135     for ( i = 0; i < nVars; i++ )
01136     {
01137         // cofactor the functiona and get support sizes
01138         Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
01139         Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
01140         nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
01141         nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
01142         nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
01143         // compare this variable with other variables
01144         if ( nSuppSizeMin > nSuppSizeCur ) 
01145         {
01146             nSuppSizeMin = nSuppSizeCur;
01147             iBestVar = i;
01148         }
01149     }
01150     assert( iBestVar != -1 );
01151     // cofactor w.r.t. this variable
01152     Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
01153     Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
01154     return iBestVar;
01155 }

void Kit_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 1021 of file kitTruth.c.

01022 {
01023     int nWords = Kit_TruthWordNum( nVars );
01024     int i, k, Step;
01025     unsigned Temp;
01026 
01027     assert( iVar < nVars );
01028     switch ( iVar )
01029     {
01030     case 0:
01031         for ( i = 0; i < nWords; i++ )
01032             pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
01033         return;
01034     case 1:
01035         for ( i = 0; i < nWords; i++ )
01036             pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
01037         return;
01038     case 2:
01039         for ( i = 0; i < nWords; i++ )
01040             pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
01041         return;
01042     case 3:
01043         for ( i = 0; i < nWords; i++ )
01044             pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
01045         return;
01046     case 4:
01047         for ( i = 0; i < nWords; i++ )
01048             pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
01049         return;
01050     default:
01051         Step = (1 << (iVar - 5));
01052         for ( k = 0; k < nWords; k += 2*Step )
01053         {
01054             for ( i = 0; i < Step; i++ )
01055             {
01056                 Temp = pTruth[i];
01057                 pTruth[i] = pTruth[Step+i];
01058                 pTruth[Step+i] = Temp;
01059             }
01060             pTruth += 2*Step;
01061         }
01062         return;
01063     }
01064 }

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

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file kitTruth.c.

00329 {
00330     int nWords = Kit_TruthWordNum( nVars );
00331     int i, k, Step;
00332 
00333     assert( iVar < nVars );
00334     switch ( iVar )
00335     {
00336     case 0:
00337         for ( i = 0; i < nWords; i++ )
00338             pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
00339         return;
00340     case 1:
00341         for ( i = 0; i < nWords; i++ )
00342             pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
00343         return;
00344     case 2:
00345         for ( i = 0; i < nWords; i++ )
00346             pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00347         return;
00348     case 3:
00349         for ( i = 0; i < nWords; i++ )
00350             pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
00351         return;
00352     case 4:
00353         for ( i = 0; i < nWords; i++ )
00354             pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
00355         return;
00356     default:
00357         Step = (1 << (iVar - 5));
00358         for ( k = 0; k < nWords; k += 2*Step )
00359         {
00360             for ( i = 0; i < Step; i++ )
00361                 pTruth[Step+i] = pTruth[i];
00362             pTruth += 2*Step;
00363         }
00364         return;
00365     }
00366 }

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

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 430 of file kitTruth.c.

00431 {
00432     int nWords = Kit_TruthWordNum( nVars );
00433     int i, k, Step;
00434 
00435     assert( iVar < nVars );
00436     switch ( iVar )
00437     {
00438     case 0:
00439         for ( i = 0; i < nWords; i++ )
00440             pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
00441         return;
00442     case 1:
00443         for ( i = 0; i < nWords; i++ )
00444             pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
00445         return;
00446     case 2:
00447         for ( i = 0; i < nWords; i++ )
00448             pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
00449         return;
00450     case 3:
00451         for ( i = 0; i < nWords; i++ )
00452             pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
00453         return;
00454     case 4:
00455         for ( i = 0; i < nWords; i++ )
00456             pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
00457         return;
00458     default:
00459         Step = (1 << (iVar - 5));
00460         for ( k = 0; k < nWords; k += 2*Step )
00461         {
00462             for ( i = 0; i < Step; i++ )
00463                 pOut[i] = pOut[Step+i] = pIn[i];
00464             pIn += 2*Step;
00465             pOut += 2*Step;
00466         }
00467         return;
00468     }
00469 }

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

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file kitTruth.c.

00380 {
00381     int nWords = Kit_TruthWordNum( nVars );
00382     int i, k, Step;
00383 
00384     assert( iVar < nVars );
00385     switch ( iVar )
00386     {
00387     case 0:
00388         for ( i = 0; i < nWords; i++ )
00389             pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
00390         return;
00391     case 1:
00392         for ( i = 0; i < nWords; i++ )
00393             pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
00394         return;
00395     case 2:
00396         for ( i = 0; i < nWords; i++ )
00397             pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
00398         return;
00399     case 3:
00400         for ( i = 0; i < nWords; i++ )
00401             pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
00402         return;
00403     case 4:
00404         for ( i = 0; i < nWords; i++ )
00405             pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
00406         return;
00407     default:
00408         Step = (1 << (iVar - 5));
00409         for ( k = 0; k < nWords; k += 2*Step )
00410         {
00411             for ( i = 0; i < Step; i++ )
00412                 pTruth[i] = pTruth[Step+i];
00413             pTruth += 2*Step;
00414         }
00415         return;
00416     }
00417 }

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

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 482 of file kitTruth.c.

00483 {
00484     int nWords = Kit_TruthWordNum( nVars );
00485     int i, k, Step;
00486 
00487     assert( iVar < nVars );
00488     switch ( iVar )
00489     {
00490     case 0:
00491         for ( i = 0; i < nWords; i++ )
00492             pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
00493         return;
00494     case 1:
00495         for ( i = 0; i < nWords; i++ )
00496             pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
00497         return;
00498     case 2:
00499         for ( i = 0; i < nWords; i++ )
00500             pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
00501         return;
00502     case 3:
00503         for ( i = 0; i < nWords; i++ )
00504             pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
00505         return;
00506     case 4:
00507         for ( i = 0; i < nWords; i++ )
00508             pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
00509         return;
00510     default:
00511         Step = (1 << (iVar - 5));
00512         for ( k = 0; k < nWords; k += 2*Step )
00513         {
00514             for ( i = 0; i < Step; i++ )
00515                 pOut[i] = pOut[Step+i] = pIn[Step+i];
00516             pIn += 2*Step;
00517             pOut += 2*Step;
00518         }
00519         return;
00520     }
00521 }

int Kit_TruthCountMinterms ( unsigned *  pTruth,
int  nVars,
int *  pRes,
int *  pBytes 
)

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

Synopsis [Fast counting minterms in the cofactors of a function.]

Description [Returns the total number of minterms in the function. The resulting array (pRes) contains the number of minterms in 0-cofactor w.r.t. each variables. The additional array (pBytes) is used for internal storage. It should have the size equal to the number of truth table bytes.]

SideEffects []

SeeAlso []

Definition at line 1542 of file kitTruth.c.

01543 {
01544     // the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
01545     static unsigned Table[256] = {
01546         0x00000000, 0x01010101, 0x01010001, 0x02020102, 0x01000101, 0x02010202, 0x02010102, 0x03020203,
01547         0x01000001, 0x02010102, 0x02010002, 0x03020103, 0x02000102, 0x03010203, 0x03010103, 0x04020204,
01548         0x00010101, 0x01020202, 0x01020102, 0x02030203, 0x01010202, 0x02020303, 0x02020203, 0x03030304,
01549         0x01010102, 0x02020203, 0x02020103, 0x03030204, 0x02010203, 0x03020304, 0x03020204, 0x04030305,
01550         0x00010001, 0x01020102, 0x01020002, 0x02030103, 0x01010102, 0x02020203, 0x02020103, 0x03030204,
01551         0x01010002, 0x02020103, 0x02020003, 0x03030104, 0x02010103, 0x03020204, 0x03020104, 0x04030205,
01552         0x00020102, 0x01030203, 0x01030103, 0x02040204, 0x01020203, 0x02030304, 0x02030204, 0x03040305,
01553         0x01020103, 0x02030204, 0x02030104, 0x03040205, 0x02020204, 0x03030305, 0x03030205, 0x04040306,
01554         0x00000101, 0x01010202, 0x01010102, 0x02020203, 0x01000202, 0x02010303, 0x02010203, 0x03020304,
01555         0x01000102, 0x02010203, 0x02010103, 0x03020204, 0x02000203, 0x03010304, 0x03010204, 0x04020305,
01556         0x00010202, 0x01020303, 0x01020203, 0x02030304, 0x01010303, 0x02020404, 0x02020304, 0x03030405,
01557         0x01010203, 0x02020304, 0x02020204, 0x03030305, 0x02010304, 0x03020405, 0x03020305, 0x04030406,
01558         0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
01559         0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
01560         0x00020203, 0x01030304, 0x01030204, 0x02040305, 0x01020304, 0x02030405, 0x02030305, 0x03040406,
01561         0x01020204, 0x02030305, 0x02030205, 0x03040306, 0x02020305, 0x03030406, 0x03030306, 0x04040407,
01562         0x00000001, 0x01010102, 0x01010002, 0x02020103, 0x01000102, 0x02010203, 0x02010103, 0x03020204,
01563         0x01000002, 0x02010103, 0x02010003, 0x03020104, 0x02000103, 0x03010204, 0x03010104, 0x04020205,
01564         0x00010102, 0x01020203, 0x01020103, 0x02030204, 0x01010203, 0x02020304, 0x02020204, 0x03030305,
01565         0x01010103, 0x02020204, 0x02020104, 0x03030205, 0x02010204, 0x03020305, 0x03020205, 0x04030306,
01566         0x00010002, 0x01020103, 0x01020003, 0x02030104, 0x01010103, 0x02020204, 0x02020104, 0x03030205,
01567         0x01010003, 0x02020104, 0x02020004, 0x03030105, 0x02010104, 0x03020205, 0x03020105, 0x04030206,
01568         0x00020103, 0x01030204, 0x01030104, 0x02040205, 0x01020204, 0x02030305, 0x02030205, 0x03040306,
01569         0x01020104, 0x02030205, 0x02030105, 0x03040206, 0x02020205, 0x03030306, 0x03030206, 0x04040307,
01570         0x00000102, 0x01010203, 0x01010103, 0x02020204, 0x01000203, 0x02010304, 0x02010204, 0x03020305,
01571         0x01000103, 0x02010204, 0x02010104, 0x03020205, 0x02000204, 0x03010305, 0x03010205, 0x04020306,
01572         0x00010203, 0x01020304, 0x01020204, 0x02030305, 0x01010304, 0x02020405, 0x02020305, 0x03030406,
01573         0x01010204, 0x02020305, 0x02020205, 0x03030306, 0x02010305, 0x03020406, 0x03020306, 0x04030407,
01574         0x00010103, 0x01020204, 0x01020104, 0x02030205, 0x01010204, 0x02020305, 0x02020205, 0x03030306,
01575         0x01010104, 0x02020205, 0x02020105, 0x03030206, 0x02010205, 0x03020306, 0x03020206, 0x04030307,
01576         0x00020204, 0x01030305, 0x01030205, 0x02040306, 0x01020305, 0x02030406, 0x02030306, 0x03040407,
01577         0x01020205, 0x02030306, 0x02030206, 0x03040307, 0x02020306, 0x03030407, 0x03030307, 0x04040408
01578     };
01579     unsigned uSum;
01580     unsigned char * pTruthC, * pLimit;
01581     int i, iVar, Step, nWords, nBytes, nTotal;
01582 
01583     assert( nVars <= 20 );
01584 
01585     // clear storage
01586     memset( pRes, 0, sizeof(int) * nVars );
01587 
01588     // count the number of one's in 0-cofactors of the first three variables
01589     nTotal = uSum = 0;
01590     nWords = Kit_TruthWordNum( nVars );
01591     nBytes = nWords * 4;
01592     pTruthC = (unsigned char *)pTruth;
01593     pLimit = pTruthC + nBytes;
01594     for ( ; pTruthC < pLimit; pTruthC++ )
01595     {
01596         uSum += Table[*pTruthC];
01597         *pBytes++ = (Table[*pTruthC] & 0xff);
01598         if ( (uSum & 0xff) > 246 )
01599         {
01600             nTotal += (uSum & 0xff);
01601             pRes[0] += ((uSum >>  8) & 0xff);
01602             pRes[2] += ((uSum >> 16) & 0xff);
01603             pRes[3] += ((uSum >> 24) & 0xff);
01604             uSum = 0;
01605         }
01606     }
01607     if ( uSum )
01608     {
01609         nTotal += (uSum & 0xff);
01610         pRes[0] += ((uSum >>  8) & 0xff);
01611         pRes[1] += ((uSum >> 16) & 0xff);
01612         pRes[2] += ((uSum >> 24) & 0xff);
01613     }
01614 
01615     // count all other variables
01616     for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
01617         for ( i = 0; i < nBytes; i += Step + Step )
01618         {
01619             pRes[iVar] += pBytes[i];
01620             pBytes[i] += pBytes[i+Step];
01621         }
01622     assert( pBytes[0] == nTotal );
01623     assert( iVar == nVars );
01624     return nTotal;
01625 }

void Kit_TruthCountMintermsPrecomp (  ) 

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

Synopsis [Fast counting minterms for the functions.]

Description [Returns 0 if the function is a constant.]

SideEffects []

SeeAlso []

Definition at line 1665 of file kitTruth.c.

01666 {
01667     int bit_count[256] = {
01668       0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
01669       1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
01670       1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
01671       2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
01672       1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
01673       2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
01674       2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
01675       3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
01676     };
01677     unsigned i, uWord;
01678     for ( i = 0; i < 256; i++ )
01679     {
01680         if ( i % 8 == 0 )
01681             printf( "\n" );
01682         uWord  =  bit_count[i];
01683         uWord |= (bit_count[i & 0x55] <<  8);
01684         uWord |= (bit_count[i & 0x33] << 16);
01685         uWord |= (bit_count[i & 0x0f] << 24);
01686         printf( "0x" );
01687         Kit_PrintHexadecimal( stdout, &uWord, 5 );
01688         printf( ", " );
01689     }
01690 }

void Kit_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 1172 of file kitTruth.c.

01173 {
01174     int nWords = Kit_TruthWordNum( nVars );
01175     int i, k, Counter;
01176     memset( pStore, 0, sizeof(short) * 2 * nVars );
01177     if ( nVars <= 5 )
01178     {
01179         if ( nVars > 0 )
01180         {
01181             pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
01182             pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
01183         }
01184         if ( nVars > 1 )
01185         {
01186             pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
01187             pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
01188         }
01189         if ( nVars > 2 )
01190         {
01191             pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
01192             pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
01193         }
01194         if ( nVars > 3 )
01195         {
01196             pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
01197             pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
01198         }
01199         if ( nVars > 4 )
01200         {
01201             pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
01202             pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
01203         }
01204         return;
01205     }
01206     // nVars >= 6
01207     // count 1's for all other variables
01208     for ( k = 0; k < nWords; k++ )
01209     {
01210         Counter = Kit_WordCountOnes( pTruth[k] );
01211         for ( i = 5; i < nVars; i++ )
01212             if ( k & (1 << (i-5)) )
01213                 pStore[2*i+1] += Counter;
01214             else
01215                 pStore[2*i+0] += Counter;
01216     }
01217     // count 1's for the first five variables
01218     for ( k = 0; k < nWords/2; k++ )
01219     {
01220         pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
01221         pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >>  1) );
01222         pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
01223         pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >>  2) );
01224         pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
01225         pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >>  4) );
01226         pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
01227         pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >>  8) );
01228         pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
01229         pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
01230         pTruth += 2;
01231     }
01232 }

void Kit_TruthCountOnesInCofsSlow ( unsigned *  pTruth,
int  nVars,
short *  pStore,
unsigned *  pAux 
)

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

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

Description [Verifies the above procedure.]

SideEffects []

SeeAlso []

Definition at line 1245 of file kitTruth.c.

01246 {
01247     int i;
01248     for ( i = 0; i < nVars; i++ )
01249     {
01250         Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
01251         pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
01252         Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
01253         pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
01254     }
01255 }

char* Kit_TruthDumpToFile ( unsigned *  pTruth,
int  nVars,
int  nFile 
)

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 1703 of file kitTruth.c.

01704 {
01705     static char pFileName[100];
01706     FILE * pFile;
01707     sprintf( pFileName, "tt\\s%04d", nFile );
01708     pFile = fopen( pFileName, "w" );
01709     fprintf( pFile, "rt " );
01710     Kit_PrintHexadecimal( pFile, pTruth, nVars );
01711     fprintf( pFile, "; bdd; sop; ps\n" );
01712     fclose( pFile );
01713     return pFileName;
01714 }

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

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 535 of file kitTruth.c.

00536 {
00537     int nWords = Kit_TruthWordNum( nVars );
00538     int i, k, Step;
00539 
00540     assert( iVar < nVars );
00541     switch ( iVar )
00542     {
00543     case 0:
00544         for ( i = 0; i < nWords; i++ )
00545             pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00546         return;
00547     case 1:
00548         for ( i = 0; i < nWords; i++ )
00549             pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00550         return;
00551     case 2:
00552         for ( i = 0; i < nWords; i++ )
00553             pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00554         return;
00555     case 3:
00556         for ( i = 0; i < nWords; i++ )
00557             pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00558         return;
00559     case 4:
00560         for ( i = 0; i < nWords; i++ )
00561             pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00562         return;
00563     default:
00564         Step = (1 << (iVar - 5));
00565         for ( k = 0; k < nWords; k += 2*Step )
00566         {
00567             for ( i = 0; i < Step; i++ )
00568             {
00569                 pTruth[i]     |= pTruth[Step+i];
00570                 pTruth[Step+i] = pTruth[i];
00571             }
00572             pTruth += 2*Step;
00573         }
00574         return;
00575     }
00576 }

void Kit_TruthExistNew ( unsigned *  pRes,
unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 589 of file kitTruth.c.

00590 {
00591     int nWords = Kit_TruthWordNum( nVars );
00592     int i, k, Step;
00593 
00594     assert( iVar < nVars );
00595     switch ( iVar )
00596     {
00597     case 0:
00598         for ( i = 0; i < nWords; i++ )
00599             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00600         return;
00601     case 1:
00602         for ( i = 0; i < nWords; i++ )
00603             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00604         return;
00605     case 2:
00606         for ( i = 0; i < nWords; i++ )
00607             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00608         return;
00609     case 3:
00610         for ( i = 0; i < nWords; i++ )
00611             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00612         return;
00613     case 4:
00614         for ( i = 0; i < nWords; i++ )
00615             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00616         return;
00617     default:
00618         Step = (1 << (iVar - 5));
00619         for ( k = 0; k < nWords; k += 2*Step )
00620         {
00621             for ( i = 0; i < Step; i++ )
00622             {
00623                 pRes[i]      = pTruth[i] | pTruth[Step+i];
00624                 pRes[Step+i] = pRes[i];
00625             }
00626             pRes += 2*Step;
00627             pTruth += 2*Step;
00628         }
00629         return;
00630     }
00631 }

void Kit_TruthExistSet ( unsigned *  pRes,
unsigned *  pTruth,
int  nVars,
unsigned  uMask 
)

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

Synopsis [Existantially quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 644 of file kitTruth.c.

00645 {
00646     int v;
00647     Kit_TruthCopy( pRes, pTruth, nVars );
00648     for ( v = 0; v < nVars; v++ )
00649         if ( uMask & (1 << v) )
00650             Kit_TruthExist( pRes, nVars, v );
00651 }

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

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

Synopsis [Unversally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 664 of file kitTruth.c.

00665 {
00666     int nWords = Kit_TruthWordNum( nVars );
00667     int i, k, Step;
00668 
00669     assert( iVar < nVars );
00670     switch ( iVar )
00671     {
00672     case 0:
00673         for ( i = 0; i < nWords; i++ )
00674             pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00675         return;
00676     case 1:
00677         for ( i = 0; i < nWords; i++ )
00678             pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00679         return;
00680     case 2:
00681         for ( i = 0; i < nWords; i++ )
00682             pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00683         return;
00684     case 3:
00685         for ( i = 0; i < nWords; i++ )
00686             pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00687         return;
00688     case 4:
00689         for ( i = 0; i < nWords; i++ )
00690             pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00691         return;
00692     default:
00693         Step = (1 << (iVar - 5));
00694         for ( k = 0; k < nWords; k += 2*Step )
00695         {
00696             for ( i = 0; i < Step; i++ )
00697             {
00698                 pTruth[i]     &= pTruth[Step+i];
00699                 pTruth[Step+i] = pTruth[i];
00700             }
00701             pTruth += 2*Step;
00702         }
00703         return;
00704     }
00705 }

void Kit_TruthForallNew ( unsigned *  pRes,
unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 718 of file kitTruth.c.

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

void Kit_TruthForallSet ( unsigned *  pRes,
unsigned *  pTruth,
int  nVars,
unsigned  uMask 
)

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

Synopsis [Universally quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 828 of file kitTruth.c.

00829 {
00830     int v;
00831     Kit_TruthCopy( pRes, pTruth, nVars );
00832     for ( v = 0; v < nVars; v++ )
00833         if ( uMask & (1 << v) )
00834             Kit_TruthForall( pRes, nVars, v );
00835 }

unsigned Kit_TruthHash ( unsigned *  pIn,
int  nWords 
)

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

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1268 of file kitTruth.c.

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

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

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 1077 of file kitTruth.c.

01078 {
01079     static unsigned uCofactor[16];
01080     int i, ValueCur, ValueMin, VarMin;
01081     unsigned uSupp0, uSupp1;
01082     int nVars0, nVars1;
01083     assert( nVars <= 9 );
01084     ValueMin = 32;
01085     VarMin   = -1;
01086     for ( i = 0; i < nVars; i++ )
01087     {
01088         // get negative cofactor
01089         Kit_TruthCopy( uCofactor, pTruth, nVars );
01090         Kit_TruthCofactor0( uCofactor, nVars, i );
01091         uSupp0 = Kit_TruthSupport( uCofactor, nVars );
01092         nVars0 = Kit_WordCountOnes( uSupp0 );
01093 //Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
01094         // get positive cofactor
01095         Kit_TruthCopy( uCofactor, pTruth, nVars );
01096         Kit_TruthCofactor1( uCofactor, nVars, i );
01097         uSupp1 = Kit_TruthSupport( uCofactor, nVars );
01098         nVars1 = Kit_WordCountOnes( uSupp1 );
01099 //Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
01100         // get the number of common vars
01101         ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
01102         if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
01103         {
01104             ValueMin = ValueCur;
01105             VarMin = i;
01106         }
01107         if ( ValueMin == 0 )
01108             break;
01109     }
01110     if ( pVarMin )
01111         *pVarMin = VarMin;
01112     return ValueMin;
01113 }

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

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 849 of file kitTruth.c.

00850 {
00851     int nWords = Kit_TruthWordNum( nVars );
00852     int i, k, Step;
00853 
00854     assert( iVar < nVars );
00855     switch ( iVar )
00856     {
00857     case 0:
00858         for ( i = 0; i < nWords; i++ )
00859             pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
00860         return;
00861     case 1:
00862         for ( i = 0; i < nWords; i++ )
00863             pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
00864         return;
00865     case 2:
00866         for ( i = 0; i < nWords; i++ )
00867             pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
00868         return;
00869     case 3:
00870         for ( i = 0; i < nWords; i++ )
00871             pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
00872         return;
00873     case 4:
00874         for ( i = 0; i < nWords; i++ )
00875             pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
00876         return;
00877     default:
00878         Step = (1 << (iVar - 5));
00879         for ( k = 0; k < nWords; k += 2*Step )
00880         {
00881             for ( i = 0; i < Step; i++ )
00882             {
00883                 pOut[i]      = pCof0[i];
00884                 pOut[Step+i] = pCof1[Step+i];
00885             }
00886             pOut += 2*Step;
00887             pCof0 += 2*Step;
00888             pCof1 += 2*Step;
00889         }
00890         return;
00891     }
00892 }

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

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 905 of file kitTruth.c.

00906 {
00907     int nWords = Kit_TruthWordNum( nVars );
00908     int i, k, Step;
00909 
00910     if ( fCompl0 == 0 )
00911     {
00912         Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
00913         return;
00914     }
00915 
00916     assert( iVar < nVars );
00917     switch ( iVar )
00918     {
00919     case 0:
00920         for ( i = 0; i < nWords; i++ )
00921             pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
00922         return;
00923     case 1:
00924         for ( i = 0; i < nWords; i++ )
00925             pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
00926         return;
00927     case 2:
00928         for ( i = 0; i < nWords; i++ )
00929             pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
00930         return;
00931     case 3:
00932         for ( i = 0; i < nWords; i++ )
00933             pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
00934         return;
00935     case 4:
00936         for ( i = 0; i < nWords; i++ )
00937             pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
00938         return;
00939     default:
00940         Step = (1 << (iVar - 5));
00941         for ( k = 0; k < nWords; k += 2*Step )
00942         {
00943             for ( i = 0; i < Step; i++ )
00944             {
00945                 pOut[i]      = ~pCof0[i];
00946                 pOut[Step+i] = pCof1[Step+i];
00947             }
00948             pOut += 2*Step;
00949             pCof0 += 2*Step;
00950             pCof1 += 2*Step;
00951         }
00952         return;
00953     }
00954 }

unsigned Kit_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 1365 of file kitTruth.c.

01366 {
01367 //    short pStore2[32];
01368     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
01369 //    int nWords = Kit_TruthWordNum( nVars );
01370     int i, Temp, fChange, Counter;//, nOnes;//, k, j, w, Limit;
01371     unsigned uCanonPhase;
01372 
01373     // canonicize output
01374     uCanonPhase = 0;
01375 /*
01376     nOnes = Kit_TruthCountOnes(pIn, nVars);
01377     if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
01378     {
01379         uCanonPhase |= (1 << nVars);
01380         Kit_TruthNot( pIn, pIn, nVars );
01381     }
01382 */
01383     // collect the minterm counts
01384     Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
01385 //    Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
01386 //    for ( i = 0; i < 2*nVars; i++ )
01387 //    {
01388 //        assert( pStore[i] == pStore2[i] );
01389 //    }
01390 
01391     // canonicize phase
01392     for ( i = 0; i < nVars; i++ )
01393     {
01394         if ( pStore[2*i+0] >= pStore[2*i+1] )
01395             continue;
01396         uCanonPhase |= (1 << i);
01397         Temp = pStore[2*i+0];
01398         pStore[2*i+0] = pStore[2*i+1];
01399         pStore[2*i+1] = Temp;
01400         Kit_TruthChangePhase( pIn, nVars, i );
01401     }
01402 
01403 //    Kit_PrintHexadecimal( stdout, pIn, nVars );
01404 //    printf( "\n" );
01405 
01406     // permute
01407     Counter = 0;
01408     do {
01409         fChange = 0;
01410         for ( i = 0; i < nVars-1; i++ )
01411         {
01412             if ( pStore[2*i] >= pStore[2*(i+1)] )
01413                 continue;
01414             Counter++;
01415             fChange = 1;
01416 
01417             Temp = pCanonPerm[i];
01418             pCanonPerm[i] = pCanonPerm[i+1];
01419             pCanonPerm[i+1] = Temp;
01420 
01421             Temp = pStore[2*i];
01422             pStore[2*i] = pStore[2*(i+1)];
01423             pStore[2*(i+1)] = Temp;
01424 
01425             Temp = pStore[2*i+1];
01426             pStore[2*i+1] = pStore[2*(i+1)+1];
01427             pStore[2*(i+1)+1] = Temp;
01428 
01429             // if the polarity of variables is different, swap them
01430             if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
01431             {
01432                 uCanonPhase ^= (1 << i);
01433                 uCanonPhase ^= (1 << (i+1));
01434             }
01435 
01436             Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
01437             pTemp = pIn; pIn = pOut; pOut = pTemp;
01438         }
01439     } while ( fChange );
01440 
01441 /*
01442     Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
01443     for ( i = 0; i < nVars; i++ )
01444         printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
01445     printf( "  C = %d\n", Counter );
01446     Extra_PrintHexadecimal( stdout, pIn, nVars );
01447     printf( "\n" );
01448 */
01449 
01450 /*
01451     // process symmetric variable groups
01452     uSymms = 0;
01453     for ( i = 0; i < nVars-1; i++ )
01454     {
01455         if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
01456             continue;
01457         if ( pStore[2*i] != pStore[2*i+1] )
01458             continue;
01459         if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
01460             continue;
01461         if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
01462             Kit_TruthChangePhase( pIn, nVars, i+1 );
01463     }
01464 */
01465 
01466 /*
01467     // process symmetric variable groups
01468     uSymms = 0;
01469     for ( i = 0; i < nVars-1; i++ )
01470     {
01471         if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
01472             continue;
01473         // i and i+1 can be symmetric
01474         // find the end of this group
01475         for ( k = i+1; k < nVars; k++ )
01476             if ( pStore[2*i] != pStore[2*k] ) 
01477                 break;
01478         Limit = k;
01479         assert( i < Limit-1 );
01480         // go through the variables in this group
01481         for ( j = i + 1; j < Limit; j++ )
01482         {
01483             // check symmetry
01484             if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
01485             {
01486                 uSymms |= (1 << j);
01487                 continue;
01488             }
01489             // they are phase-unknown
01490             if ( pStore[2*i] == pStore[2*i+1] ) 
01491             {
01492                 if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
01493                 {
01494                     Kit_TruthChangePhase( pIn, nVars, j );
01495                     uCanonPhase ^= (1 << j);
01496                     uSymms |= (1 << j);
01497                     continue;
01498                 }
01499             }
01500 
01501             // they are not symmetric - move j as far as it goes in the group
01502             for ( k = j; k < Limit-1; k++ )
01503             {
01504                 Counter++;
01505 
01506                 Temp = pCanonPerm[k];
01507                 pCanonPerm[k] = pCanonPerm[k+1];
01508                 pCanonPerm[k+1] = Temp;
01509 
01510                 assert( pStore[2*k] == pStore[2*(k+1)] );
01511                 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
01512                 pTemp = pIn; pIn = pOut; pOut = pTemp;
01513             }
01514             Limit--;
01515             j--;
01516         }
01517         i = Limit - 1;
01518     }
01519 */
01520 
01521     // swap if it was moved an even number of times
01522     if ( Counter & 1 )
01523         Kit_TruthCopy( pOut, pIn, nVars );
01524     return uCanonPhase;
01525 }

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

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 197 of file kitTruth.c.

00198 {
00199     unsigned * pTemp;
00200     int i, k, Var = 0, Counter = 0;
00201     for ( i = 0; i < nVarsAll; i++ )
00202         if ( Phase & (1 << i) )
00203         {
00204             for ( k = i-1; k >= Var; k-- )
00205             {
00206                 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
00207                 pTemp = pIn; pIn = pOut; pOut = pTemp;
00208                 Counter++;
00209             }
00210             Var++;
00211         }
00212     assert( Var == nVars );
00213     // swap if it was moved an even number of times
00214     if ( fReturnIn ^ !(Counter & 1) )
00215         Kit_TruthCopy( pOut, pIn, nVarsAll );
00216 }

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

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 163 of file kitTruth.c.

00164 {
00165     unsigned * pTemp;
00166     int i, k, Var = nVars - 1, Counter = 0;
00167     for ( i = nVarsAll - 1; i >= 0; i-- )
00168         if ( Phase & (1 << i) )
00169         {
00170             for ( k = Var; k < i; k++ )
00171             {
00172                 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
00173                 pTemp = pIn; pIn = pOut; pOut = pTemp;
00174                 Counter++;
00175             }
00176             Var--;
00177         }
00178     assert( Var == -1 );
00179     // swap if it was moved an even number of times
00180     if ( fReturnIn ^ !(Counter & 1) )
00181         Kit_TruthCopy( pOut, pIn, nVarsAll );
00182 }

unsigned Kit_TruthSupport ( unsigned *  pTruth,
int  nVars 
)

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 306 of file kitTruth.c.

00307 {
00308     int i, Support = 0;
00309     for ( i = 0; i < nVars; i++ )
00310         if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
00311             Support |= (1 << i);
00312     return Support;
00313 }

int Kit_TruthSupportSize ( unsigned *  pTruth,
int  nVars 
)

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file kitTruth.c.

00288 {
00289     int i, Counter = 0;
00290     for ( i = 0; i < nVars; i++ )
00291         Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
00292     return Counter;
00293 }

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

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

FileName [kitTruth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving truth tables.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id
kitTruth.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///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 43 of file kitTruth.c.

00044 {
00045     static unsigned PMasks[4][3] = {
00046         { 0x99999999, 0x22222222, 0x44444444 },
00047         { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
00048         { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
00049         { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
00050     };
00051     int nWords = Kit_TruthWordNum( nVars );
00052     int i, k, Step, Shift;
00053 
00054     assert( iVar < nVars - 1 );
00055     if ( iVar < 4 )
00056     {
00057         Shift = (1 << iVar);
00058         for ( i = 0; i < nWords; i++ )
00059             pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
00060     }
00061     else if ( iVar > 4 )
00062     {
00063         Step = (1 << (iVar - 5));
00064         for ( k = 0; k < nWords; k += 4*Step )
00065         {
00066             for ( i = 0; i < Step; i++ )
00067                 pOut[i] = pIn[i];
00068             for ( i = 0; i < Step; i++ )
00069                 pOut[Step+i] = pIn[2*Step+i];
00070             for ( i = 0; i < Step; i++ )
00071                 pOut[2*Step+i] = pIn[Step+i];
00072             for ( i = 0; i < Step; i++ )
00073                 pOut[3*Step+i] = pIn[3*Step+i];
00074             pIn  += 4*Step;
00075             pOut += 4*Step;
00076         }
00077     }
00078     else // if ( iVar == 4 )
00079     {
00080         for ( i = 0; i < nWords; i += 2 )
00081         {
00082             pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
00083             pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
00084         }
00085     }
00086 }

void Kit_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 100 of file kitTruth.c.

00101 {
00102     int nWords = (nVars <= 5)? 1 : (1 << (nVars-5));
00103     int i, k, Step;
00104 
00105     assert( Start < nVars - 1 );
00106     switch ( Start )
00107     {
00108     case 0:
00109         for ( i = 0; i < nWords; i++ )
00110             pOut[i] = (pIn[i] & 0x99999999) | ((pIn[i] & 0x22222222) << 1) | ((pIn[i] & 0x44444444) >> 1);
00111         return;
00112     case 1:
00113         for ( i = 0; i < nWords; i++ )
00114             pOut[i] = (pIn[i] & 0xC3C3C3C3) | ((pIn[i] & 0x0C0C0C0C) << 2) | ((pIn[i] & 0x30303030) >> 2);
00115         return;
00116     case 2:
00117         for ( i = 0; i < nWords; i++ )
00118             pOut[i] = (pIn[i] & 0xF00FF00F) | ((pIn[i] & 0x00F000F0) << 4) | ((pIn[i] & 0x0F000F00) >> 4);
00119         return;
00120     case 3:
00121         for ( i = 0; i < nWords; i++ )
00122             pOut[i] = (pIn[i] & 0xFF0000FF) | ((pIn[i] & 0x0000FF00) << 8) | ((pIn[i] & 0x00FF0000) >> 8);
00123         return;
00124     case 4:
00125         for ( i = 0; i < nWords; i += 2 )
00126         {
00127             pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
00128             pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
00129         }
00130         return;
00131     default:
00132         Step = (1 << (Start - 5));
00133         for ( k = 0; k < nWords; k += 4*Step )
00134         {
00135             for ( i = 0; i < Step; i++ )
00136                 pOut[i] = pIn[i];
00137             for ( i = 0; i < Step; i++ )
00138                 pOut[Step+i] = pIn[2*Step+i];
00139             for ( i = 0; i < Step; i++ )
00140                 pOut[2*Step+i] = pIn[Step+i];
00141             for ( i = 0; i < Step; i++ )
00142                 pOut[3*Step+i] = pIn[3*Step+i];
00143             pIn  += 4*Step;
00144             pOut += 4*Step;
00145         }
00146         return;
00147     }
00148 }

void Kit_TruthUniqueNew ( unsigned *  pRes,
unsigned *  pTruth,
int  nVars,
int  iVar 
)

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 773 of file kitTruth.c.

00774 {
00775     int nWords = Kit_TruthWordNum( nVars );
00776     int i, k, Step;
00777 
00778     assert( iVar < nVars );
00779     switch ( iVar )
00780     {
00781     case 0:
00782         for ( i = 0; i < nWords; i++ )
00783             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
00784         return;
00785     case 1:
00786         for ( i = 0; i < nWords; i++ )
00787             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
00788         return;
00789     case 2:
00790         for ( i = 0; i < nWords; i++ )
00791             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
00792         return;
00793     case 3:
00794         for ( i = 0; i < nWords; i++ )
00795             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
00796         return;
00797     case 4:
00798         for ( i = 0; i < nWords; i++ )
00799             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
00800         return;
00801     default:
00802         Step = (1 << (iVar - 5));
00803         for ( k = 0; k < nWords; k += 2*Step )
00804         {
00805             for ( i = 0; i < Step; i++ )
00806             {
00807                 pRes[i]      = pTruth[i] ^ pTruth[Step+i];
00808                 pRes[Step+i] = pRes[i];
00809             }
00810             pRes += 2*Step;
00811             pTruth += 2*Step;
00812         }
00813         return;
00814     }
00815 }

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file kitTruth.c.

00231 {
00232     int nWords = Kit_TruthWordNum( nVars );
00233     int i, k, Step;
00234 
00235     assert( iVar < nVars );
00236     switch ( iVar )
00237     {
00238     case 0:
00239         for ( i = 0; i < nWords; i++ )
00240             if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
00241                 return 1;
00242         return 0;
00243     case 1:
00244         for ( i = 0; i < nWords; i++ )
00245             if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
00246                 return 1;
00247         return 0;
00248     case 2:
00249         for ( i = 0; i < nWords; i++ )
00250             if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
00251                 return 1;
00252         return 0;
00253     case 3:
00254         for ( i = 0; i < nWords; i++ )
00255             if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
00256                 return 1;
00257         return 0;
00258     case 4:
00259         for ( i = 0; i < nWords; i++ )
00260             if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
00261                 return 1;
00262         return 0;
00263     default:
00264         Step = (1 << (iVar - 5));
00265         for ( k = 0; k < nWords; k += 2*Step )
00266         {
00267             for ( i = 0; i < Step; i++ )
00268                 if ( pTruth[i] != pTruth[Step+i] )
00269                     return 1;
00270             pTruth += 2*Step;
00271         }
00272         return 0;
00273     }
00274 }

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

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

Synopsis [Checks antisymmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 994 of file kitTruth.c.

00995 {
00996     static unsigned uTemp0[16], uTemp1[16];
00997     assert( nVars <= 9 );
00998     // compute Cof00
00999     Kit_TruthCopy( uTemp0, pTruth, nVars );
01000     Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
01001     Kit_TruthCofactor0( uTemp0, nVars, iVar1 );
01002     // compute Cof11
01003     Kit_TruthCopy( uTemp1, pTruth, nVars );
01004     Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
01005     Kit_TruthCofactor1( uTemp1, nVars, iVar1 );
01006     // compare
01007     return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
01008 }

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

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

Synopsis [Checks symmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 967 of file kitTruth.c.

00968 {
00969     static unsigned uTemp0[16], uTemp1[16];
00970     assert( nVars <= 9 );
00971     // compute Cof01
00972     Kit_TruthCopy( uTemp0, pTruth, nVars );
00973     Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
00974     Kit_TruthCofactor1( uTemp0, nVars, iVar1 );
00975     // compute Cof10
00976     Kit_TruthCopy( uTemp1, pTruth, nVars );
00977     Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
00978     Kit_TruthCofactor0( uTemp1, nVars, iVar1 );
00979     // compare
00980     return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
00981 }

Generated on Tue Jan 5 12:18:28 2010 for abc70930 by  doxygen 1.6.1