summaryrefslogtreecommitdiffstats
path: root/src/misc/util/utilTruth.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/util/utilTruth.h')
-rw-r--r--src/misc/util/utilTruth.h966
1 files changed, 886 insertions, 80 deletions
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 6bfb5699..30508498 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -44,6 +44,23 @@ static word s_Truths6[6] = {
0xFFFFFFFF00000000
};
+static word s_Truths6Neg[6] = {
+ 0x5555555555555555,
+ 0x3333333333333333,
+ 0x0F0F0F0F0F0F0F0F,
+ 0x00FF00FF00FF00FF,
+ 0x0000FFFF0000FFFF,
+ 0x00000000FFFFFFFF
+};
+
+static word s_CMasks6[5] = {
+ 0x1111111111111111,
+ 0x0303030303030303,
+ 0x000F000F000F000F,
+ 0x000000FF000000FF,
+ 0x000000000000FFFF
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -76,6 +93,12 @@ static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nV
SeeAlso []
***********************************************************************/
+static inline void Abc_TtNot( word * pOut, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ pOut[w] = ~pOut[w];
+}
static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
{
int w;
@@ -96,6 +119,368 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
for ( w = 0; w < nWords; w++ )
pOut[w] = pIn1[w] & pIn2[w];
}
+static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ if ( pIn1[w] != pIn2[w] )
+ return 0;
+ return 1;
+}
+static inline int Abc_TtCompare( word * pIn1, word * pIn2, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ if ( pIn1[w] != pIn2[w] )
+ return (pIn1[w] < pIn2[w]) ? -1 : 1;
+ return 0;
+}
+static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords )
+{
+ int w;
+ for ( w = nWords - 1; w >= 0; w-- )
+ if ( pIn1[w] != pIn2[w] )
+ return (pIn1[w] < pIn2[w]) ? -1 : 1;
+ return 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Compares Cof0 and Cof1.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
+{
+ if ( nWords == 1 )
+ {
+ word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
+ word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
+ if ( Cof0 != Cof1 )
+ return Cof0 < Cof1 ? -1 : 1;
+ return 0;
+ }
+ if ( iVar <= 5 )
+ {
+ word Cof0, Cof1;
+ int w, shift = (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ {
+ Cof0 = pTruth[w] & s_Truths6Neg[iVar];
+ Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
+ if ( Cof0 != Cof1 )
+ return Cof0 < Cof1 ? -1 : 1;
+ }
+ return 0;
+ }
+ // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ assert( nWords >= 2 );
+ for ( ; pTruth < pLimit; pTruth += 2*iStep )
+ for ( i = 0; i < iStep; i++ )
+ if ( pTruth[i] != pTruth[i + iStep] )
+ return pTruth[i] < pTruth[i + iStep] ? -1 : 1;
+ return 0;
+ }
+}
+static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar )
+{
+ if ( nWords == 1 )
+ {
+ word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
+ word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
+ if ( Cof0 != Cof1 )
+ return Cof0 < Cof1 ? -1 : 1;
+ return 0;
+ }
+ if ( iVar <= 5 )
+ {
+ word Cof0, Cof1;
+ int w, shift = (1 << iVar);
+ for ( w = nWords - 1; w >= 0; w-- )
+ {
+ Cof0 = pTruth[w] & s_Truths6Neg[iVar];
+ Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
+ if ( Cof0 != Cof1 )
+ return Cof0 < Cof1 ? -1 : 1;
+ }
+ return 0;
+ }
+ // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ assert( nWords >= 2 );
+ for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep )
+ for ( i = iStep - 1; i >= 0; i-- )
+ if ( pLimit[i] != pLimit[i + iStep] )
+ return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
+ return 0;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks pairs of cofactors w.r.t. adjacent variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+{
+ assert( Num1 < Num2 && Num2 < 4 );
+ if ( nWords == 1 )
+ return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]);
+ if ( iVar <= 4 )
+ {
+ int w, shift = (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ if ( ((pTruth[w] >> Num2 * shift) & s_CMasks6[iVar]) != ((pTruth[w] >> Num1 * shift) & s_CMasks6[iVar]) )
+ return 0;
+ return 1;
+ }
+ if ( iVar == 5 )
+ {
+ unsigned * pTruthU = (unsigned *)pTruth;
+ unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+ assert( nWords >= 2 );
+ for ( ; pTruthU < pLimitU; pTruthU += 4 )
+ if ( pTruthU[Num2] != pTruthU[Num1] )
+ return 0;
+ return 1;
+ }
+ // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ assert( nWords >= 4 );
+ for ( ; pTruth < pLimit; pTruth += 4*iStep )
+ for ( i = 0; i < iStep; i++ )
+ if ( pTruth[i+Num2*iStep] != pTruth[i+Num1*iStep] )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+{
+ assert( Num1 < Num2 && Num2 < 4 );
+ if ( nWords == 1 )
+ {
+ word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
+ word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
+ if ( Cof1 != Cof2 )
+ return Cof1 < Cof2 ? -1 : 1;
+ return 0;
+ }
+ if ( iVar <= 4 )
+ {
+ word Cof1, Cof2;
+ int w, shift = (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ {
+ Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+ Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+ if ( Cof1 != Cof2 )
+ return Cof1 < Cof2 ? -1 : 1;
+ }
+ return 0;
+ }
+ if ( iVar == 5 )
+ {
+ unsigned * pTruthU = (unsigned *)pTruth;
+ unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+ assert( nWords >= 2 );
+ for ( ; pTruthU < pLimitU; pTruthU += 4 )
+ if ( pTruthU[Num1] != pTruthU[Num2] )
+ return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1;
+ return 0;
+ }
+ // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ int Offset1 = Num1*iStep;
+ int Offset2 = Num2*iStep;
+ assert( nWords >= 4 );
+ for ( ; pTruth < pLimit; pTruth += 4*iStep )
+ for ( i = 0; i < iStep; i++ )
+ if ( pTruth[i + Offset1] != pTruth[i + Offset2] )
+ return pTruth[i + Offset1] < pTruth[i + Offset2] ? -1 : 1;
+ return 0;
+ }
+}
+static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+{
+ assert( Num1 < Num2 && Num2 < 4 );
+ if ( nWords == 1 )
+ {
+ word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
+ word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
+ if ( Cof1 != Cof2 )
+ return Cof1 < Cof2 ? -1 : 1;
+ return 0;
+ }
+ if ( iVar <= 4 )
+ {
+ word Cof1, Cof2;
+ int w, shift = (1 << iVar);
+ for ( w = nWords - 1; w >= 0; w-- )
+ {
+ Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+ Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+ if ( Cof1 != Cof2 )
+ return Cof1 < Cof2 ? -1 : 1;
+ }
+ return 0;
+ }
+ if ( iVar == 5 )
+ {
+ unsigned * pTruthU = (unsigned *)pTruth;
+ unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+ assert( nWords >= 2 );
+ for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 )
+ if ( pLimitU[Num1] != pLimitU[Num2] )
+ return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1;
+ return 0;
+ }
+ // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ int Offset1 = Num1*iStep;
+ int Offset2 = Num2*iStep;
+ assert( nWords >= 4 );
+ for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep )
+ for ( i = iStep - 1; i >= 0; i-- )
+ if ( pLimit[i + Offset1] != pLimit[i + Offset2] )
+ return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1;
+ return 0;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks pairs of cofactors w.r.t. two variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int jVar, int Num1, int Num2 )
+{
+ assert( Num1 < Num2 && Num2 < 4 );
+ assert( iVar < jVar );
+ if ( nWords == 1 )
+ {
+ word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
+ int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
+ int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
+ return ((pTruth[0] >> shift1) & Mask) == ((pTruth[0] >> shift2) & Mask);
+ }
+ if ( jVar <= 5 )
+ {
+ word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
+ int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
+ int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ if ( ((pTruth[w] >> shift1) & Mask) != ((pTruth[w] >> shift2) & Mask) )
+ return 0;
+ return 1;
+ }
+ if ( iVar <= 5 && jVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int j, jStep = Abc_TtWordNum(jVar);
+ int shift1 = (Num1 & 1) * (1 << iVar);
+ int shift2 = (Num2 & 1) * (1 << iVar);
+ int Offset1 = (Num1 >> 1) * jStep;
+ int Offset2 = (Num2 >> 1) * jStep;
+ for ( ; pTruth < pLimit; pTruth += 2*jStep )
+ for ( j = 0; j < jStep; j++ )
+ if ( ((pTruth[j + Offset1] >> shift1) & s_Truths6Neg[iVar]) != ((pTruth[j + Offset2] >> shift2) & s_Truths6Neg[iVar]) )
+ return 0;
+ return 1;
+ }
+ {
+ word * pLimit = pTruth + nWords;
+ int j, jStep = Abc_TtWordNum(jVar);
+ int i, iStep = Abc_TtWordNum(iVar);
+ int Offset1 = (Num1 >> 1) * jStep + (Num1 & 1) * iStep;
+ int Offset2 = (Num2 >> 1) * jStep + (Num2 & 1) * iStep;
+ for ( ; pTruth < pLimit; pTruth += 2*jStep )
+ for ( i = 0; i < jStep; i += 2*iStep )
+ for ( j = 0; j < iStep; j++ )
+ if ( pTruth[Offset1 + i + j] != pTruth[Offset2 + i + j] )
+ return 0;
+ return 1;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
+{
+ if ( nWords == 1 )
+ pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]);
+ else if ( iVar <= 5 )
+ {
+ int w, shift = (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
+ }
+ else // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ for ( ; pTruth < pLimit; pTruth += 2*iStep )
+ for ( i = 0; i < iStep; i++ )
+ pTruth[i + iStep] = pTruth[i];
+ }
+}
+static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
+{
+ if ( nWords == 1 )
+ pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
+ else if ( iVar <= 5 )
+ {
+ int w, shift = (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
+ }
+ else // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ for ( ; pTruth < pLimit; pTruth += 2*iStep )
+ for ( i = 0; i < iStep; i++ )
+ pTruth[i] = pTruth[i + iStep];
+ }
+}
/**Function*************************************************************
@@ -109,13 +494,238 @@ static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords,
SeeAlso []
***********************************************************************/
+static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == 0; }
+static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar]; }
+static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0; }
+static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar]; }
+static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); }
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; }
+static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
+
+static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar )
+{
+ if ( iVar < 6 )
+ {
+ int i;
+ for ( i = 0; i < nWords; i++ )
+ if ( t[i] & s_Truths6Neg[iVar] )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + nWords;
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( t[i] )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar )
+{
+ if ( iVar < 6 )
+ {
+ int i;
+ for ( i = 0; i < nWords; i++ )
+ if ( (t[i] & s_Truths6Neg[iVar]) != s_Truths6Neg[iVar] )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + nWords;
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( ~t[i] )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar )
+{
+ if ( iVar < 6 )
+ {
+ int i;
+ for ( i = 0; i < nWords; i++ )
+ if ( t[i] & s_Truths6[iVar] )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + nWords;
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( t[i+Step] )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar )
+{
+ if ( iVar < 6 )
+ {
+ int i;
+ for ( i = 0; i < nWords; i++ )
+ if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + nWords;
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( ~t[i+Step] )
+ return 0;
+ return 1;
+ }
+}
+static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
+{
+ if ( iVar < 6 )
+ {
+ int i, Shift = (1 << iVar);
+ for ( i = 0; i < nWords; i++ )
+ if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
+ return 0;
+ return 1;
+ }
+ else
+ {
+ int i, Step = (1 << (iVar - 6));
+ word * tLimit = t + nWords;
+ for ( ; t < tLimit; t += 2*Step )
+ for ( i = 0; i < Step; i++ )
+ if ( t[i] != ~t[i+Step] )
+ return 0;
+ return 1;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_TtPrintDigit( int Digit )
+{
+ assert( Digit >= 0 && Digit < 16 );
+ if ( Digit < 10 )
+ printf( "%d", Digit );
+ else
+ printf( "%c", 'A' + Digit-10 );
+}
+static inline void Abc_TtPrintHex( word * pTruth, int nVars )
+{
+ word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
+ int k, nDigits = 1 << (nVars-2);
+ assert( nVars >= 2 );
+ for ( pThis = pTruth; pThis < pLimit; pThis++ )
+ for ( k = 0; k < 16; k++ )
+ Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+ printf( "\n" );
+}
+static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
+{
+ word * pThis;
+ int k, nDigits = 1 << (nVars-2);
+ assert( nVars >= 2 );
+ for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
+ for ( k = 15; k >= 0; k-- )
+ Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+ printf( "\n" );
+}
+static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
+{
+ word * pThis;
+ int k, nDigits = 1 << (nVars-2);
+ assert( nVars >= 2 );
+ for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
+ for ( k = 0; k < 16; k++ )
+ Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+ printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
+{
+ word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
+ int k, nDigits = 1 << (nVars-2);
+ assert( nVars >= 2 );
+ for ( pThis = pTruth; pThis < pLimit; pThis++ )
+ for ( k = 0; k < 64; k++ )
+ printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtSuppFindFirst( int Supp )
+{
+ int i;
+ assert( Supp > 0 );
+ for ( i = 0; i < 32; i++ )
+ if ( Supp & (1 << i) )
+ return i;
+ return -1;
+}
+static inline int Abc_TtSuppOnlyOne( int Supp )
+{
+ assert( Supp > 0 );
+ return (Supp & (Supp-1)) == 0;
+}
static inline int Abc_TtSuppIsMinBase( int Supp )
{
+ assert( Supp > 0 );
return (Supp & (Supp+1)) == 0;
}
static inline int Abc_Tt6HasVar( word t, int iVar )
{
- return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]);
+ return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]);
}
static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
{
@@ -125,7 +735,7 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
{
int i, Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
- if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
+ if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
return 1;
return 0;
}
@@ -188,6 +798,69 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
SeeAlso []
***********************************************************************/
+static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
+{
+ if ( nWords == 1 )
+ pTruth[0] = ((pTruth[0] << (1 << iVar)) & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
+ else if ( iVar <= 5 )
+ {
+ int w, shift = (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ pTruth[w] = ((pTruth[w] << shift) & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
+ }
+ else // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ for ( ; pTruth < pLimit; pTruth += 2*iStep )
+ for ( i = 0; i < iStep; i++ )
+ ABC_SWAP( word, pTruth[i], pTruth[i + iStep] );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
+{
+ static word PMasks[5][3] = {
+ { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+ { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+ { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+ { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+ { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+ };
+ if ( iVar < 5 )
+ {
+ int i, Shift = (1 << iVar);
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = (pTruth[i] & PMasks[iVar][0]) | ((pTruth[i] & PMasks[iVar][1]) << Shift) | ((pTruth[i] & PMasks[iVar][2]) >> Shift);
+ }
+ else if ( iVar == 5 )
+ {
+ unsigned * pTruthU = (unsigned *)pTruth;
+ unsigned * pLimitU = (unsigned *)(pTruth + nWords);
+ for ( ; pTruthU < pLimitU; pTruthU += 4 )
+ ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] );
+ }
+ else // if ( iVar > 5 )
+ {
+ word * pLimit = pTruth + nWords;
+ int i, iStep = Abc_TtWordNum(iVar);
+ for ( ; pTruth < pLimit; pTruth += 4*iStep )
+ for ( i = 0; i < iStep; i++ )
+ ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] );
+ }
+}
+
static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
{
static word PPMasks[5][6][3] = {
@@ -270,106 +943,239 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
}
else
{
- word temp, * pLimit = pTruth + Abc_TtWordNum(nVars);
+ word * pLimit = pTruth + Abc_TtWordNum(nVars);
int i, iStep = Abc_TtWordNum(iVar);
int j, jStep = Abc_TtWordNum(jVar);
for ( ; pTruth < pLimit; pTruth += 2*jStep )
for ( i = 0; i < jStep; i += 2*iStep )
for ( j = 0; j < iStep; j++ )
- {
- temp = pTruth[iStep + i + j];
- pTruth[iStep + i + j] = pTruth[jStep + i + j];
- pTruth[jStep + i + j] = temp;
- }
+ ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
}
}
}
-static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar )
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtCountOnesSlow( word t )
{
- static word PPMasks[6][6] = {
- { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
- { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
- { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 },
- { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 },
- { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 },
- { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 }
- };
+ t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555);
+ t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333);
+ t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F);
+ t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF);
+ t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF);
+ return (t & 0x00000000FFFFFFFF) + (t>>32);
+}
+static inline int Abc_TtCountOnes( word x )
+{
+ x = x - ((x >> 1) & 0x5555555555555555);
+ x = (x & 0x3333333333333333) + ((x >> 2) & 0x3333333333333333);
+ x = (x + (x >> 4)) & 0x0F0F0F0F0F0F0F0F;
+ x = x + (x >> 8);
+ x = x + (x >> 16);
+ x = x + (x >> 32);
+ return (int)(x & 0xFF);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
+{
+ int nWords = Abc_TtWordNum( nVars );
+ int k, Counter = 0;
+ for ( k = 0; k < nWords; k++ )
+ Counter += Abc_TtCountOnes( pTruth[k] );
+ return Counter;
+}
+static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
+{
+ int i, k, Counter, nWords;
+ memset( pStore, 0, sizeof(int) * nVars );
if ( nVars <= 6 )
{
- int shift;
- word low2High, high2Low;
- assert( iVar <= 5 && jVar <= 5 && iVar < jVar );
- shift = (1 << jVar) - (1 << iVar);
- low2High = (pTruth[0] & PPMasks[iVar][jVar - 1] ) << shift;
- pTruth[0] &= ~PPMasks[iVar][jVar - 1];
- high2Low = (pTruth[0] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
- pTruth[0] &= ~(PPMasks[iVar][jVar - 1] << shift);
- pTruth[0] |= low2High | high2Low;
+ for ( i = 0; i < nVars; i++ )
+ pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
+ return;
}
- else
+ assert( nVars > 6 );
+ nWords = Abc_TtWordNum( nVars );
+ for ( k = 0; k < nWords; k++ )
{
- word low2High, high2Low, temp;
- int nWords = Abc_TtWordNum(nVars);
- int shift, step, iStep, jStep;
- int w = 0, i = 0, j = 0;
- if ( iVar == jVar )
- return;
- if ( jVar < iVar )
- ABC_SWAP( int, iVar, jVar );
- if ( iVar <= 5 && jVar <= 5 )
- {
- shift = (1 << jVar) - (1 << iVar);
- for ( w = 0; w < nWords; w++ )
- {
- low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift;
- pTruth[w] &= ~PPMasks[iVar][jVar - 1];
- high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift;
- pTruth[w] &= ~(PPMasks[iVar][jVar - 1] << shift);
- pTruth[w] |= low2High | high2Low;
- }
- }
- else if ( iVar <= 5 && jVar > 5 )
+ // count 1's for the first six variables
+ for ( i = 0; i < 6; i++ )
+ pStore[i] += Abc_TtCountOnes( (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i)) );
+ // count 1's for all other variables
+ Counter = Abc_TtCountOnes( pTruth[k] );
+ for ( i = 6; i < nVars; i++ )
+ if ( (k & (1 << (i-6))) == 0 )
+ pStore[i] += Counter;
+ // count 1's for all other variables
+ Counter = Abc_TtCountOnes( pTruth[++k] );
+ for ( i = 6; i < nVars; i++ )
+ if ( (k & (1 << (i-6))) == 0 )
+ pStore[i] += Counter;
+ }
+}
+static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pStore )
+{
+ static int bit_count[256] = {
+ 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,
+ 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,
+ 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,
+ 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,
+ 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,
+ 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,
+ 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,
+ 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
+ };
+ int i, k, nBytes;
+ unsigned char * pTruthC = (unsigned char *)pTruth;
+ nBytes = 8 * Abc_TtWordNum( nVars );
+ memset( pStore, 0, sizeof(int) * nVars );
+ for ( k = 0; k < nBytes; k++ )
+ {
+ pStore[0] += bit_count[ pTruthC[k] & 0x55 ];
+ pStore[1] += bit_count[ pTruthC[k] & 0x33 ];
+ pStore[2] += bit_count[ pTruthC[k] & 0x0F ];
+ for ( i = 3; i < nVars; i++ )
+ if ( (k & (1 << (i-3))) == 0 )
+ pStore[i] += bit_count[pTruthC[k]];
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm )
+{
+ int pStore[16];
+ int nWords = Abc_TtWordNum( nVars );
+ int i, Temp, fChange, nOnes;
+ unsigned uCanonPhase = 0;
+ assert( nVars <= 16 );
+ // normalize polarity
+ nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
+ if ( nOnes > nWords * 32 )
+ {
+ Abc_TtNot( pTruth, nWords );
+ nOnes = nWords*64 - nOnes;
+ uCanonPhase |= (1 << nVars);
+ }
+ // normalize phase
+ Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pStore[i] >= nOnes - pStore[i] )
+ continue;
+ Abc_TtFlip( pTruth, nWords, i );
+ uCanonPhase |= (1 << i);
+ pStore[i] = nOnes - pStore[i];
+ }
+
+ do {
+ fChange = 0;
+ for ( i = 0; i < nVars-1; i++ )
{
- step = Abc_TtWordNum(jVar + 1)/2;
- shift = 1 << iVar;
- for ( w = 0; w < nWords; w += 2*step )
+ if ( pStore[i] <= pStore[i+1] )
+ continue;
+
+ Temp = pCanonPerm[i];
+ pCanonPerm[i] = pCanonPerm[i+1];
+ pCanonPerm[i+1] = Temp;
+
+ Temp = pStore[i];
+ pStore[i] = pStore[i+1];
+ pStore[i+1] = Temp;
+
+ if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
{
- for (j = 0; j < step; j++)
- {
- low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift;
- pTruth[w + j] &= ~PPMasks[iVar][5];
- high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift;
- pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift);
- pTruth[w + j] |= high2Low;
- pTruth[w + step + j] |= low2High;
- }
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << (i+1));
}
+ Abc_TtSwapAdjacent( pTruth, nWords, i );
+ fChange = 1;
}
- else
- {
- iStep = Abc_TtWordNum(iVar + 1)/2;
- jStep = Abc_TtWordNum(jVar + 1)/2;
- for (w = 0; w < nWords; w += 2*jStep)
- {
- for (i = 0; i < jStep; i += 2*iStep)
- {
- for (j = 0; j < iStep; j++)
- {
- temp = pTruth[w + iStep + i + j];
- pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j];
- pTruth[w + jStep + i + j] = temp;
- }
- }
- }
- }
- }
+ } while ( fChange );
+ return uCanonPhase;
}
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_TtReverseVars( word * pTruth, int nVars )
+{
+ int k;
+ for ( k = 0; k < nVars/2 ; k++ )
+ Abc_TtSwapVars( pTruth, nVars, k, nVars - 1 - k );
+}
+static inline void Abc_TtReverseBits( word * pTruth, int nVars )
+{
+ static unsigned char pMirror[256] = {
+ 0, 128, 64, 192, 32, 160, 96, 224, 16, 144, 80, 208, 48, 176, 112, 240,
+ 8, 136, 72, 200, 40, 168, 104, 232, 24, 152, 88, 216, 56, 184, 120, 248,
+ 4, 132, 68, 196, 36, 164, 100, 228, 20, 148, 84, 212, 52, 180, 116, 244,
+ 12, 140, 76, 204, 44, 172, 108, 236, 28, 156, 92, 220, 60, 188, 124, 252,
+ 2, 130, 66, 194, 34, 162, 98, 226, 18, 146, 82, 210, 50, 178, 114, 242,
+ 10, 138, 74, 202, 42, 170, 106, 234, 26, 154, 90, 218, 58, 186, 122, 250,
+ 6, 134, 70, 198, 38, 166, 102, 230, 22, 150, 86, 214, 54, 182, 118, 246,
+ 14, 142, 78, 206, 46, 174, 110, 238, 30, 158, 94, 222, 62, 190, 126, 254,
+ 1, 129, 65, 193, 33, 161, 97, 225, 17, 145, 81, 209, 49, 177, 113, 241,
+ 9, 137, 73, 201, 41, 169, 105, 233, 25, 153, 89, 217, 57, 185, 121, 249,
+ 5, 133, 69, 197, 37, 165, 101, 229, 21, 149, 85, 213, 53, 181, 117, 245,
+ 13, 141, 77, 205, 45, 173, 109, 237, 29, 157, 93, 221, 61, 189, 125, 253,
+ 3, 131, 67, 195, 35, 163, 99, 227, 19, 147, 83, 211, 51, 179, 115, 243,
+ 11, 139, 75, 203, 43, 171, 107, 235, 27, 155, 91, 219, 59, 187, 123, 251,
+ 7, 135, 71, 199, 39, 167, 103, 231, 23, 151, 87, 215, 55, 183, 119, 247,
+ 15, 143, 79, 207, 47, 175, 111, 239, 31, 159, 95, 223, 63, 191, 127, 255
+ };
+ unsigned char Temp, * pTruthC = (unsigned char *)pTruth;
+ int i, nBytes = (nVars > 6) ? (1 << (nVars - 3)) : 8;
+ for ( i = 0; i < nBytes/2; i++ )
+ {
+ Temp = pMirror[pTruthC[i]];
+ pTruthC[i] = pMirror[pTruthC[nBytes-1-i]];
+ pTruthC[nBytes-1-i] = Temp;
+ }
+}
+
+
+/**Function*************************************************************
+
Synopsis [Stretch truthtable to have more input variables.]
Description []
@@ -379,7 +1185,7 @@ static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar
SeeAlso []
***********************************************************************/
-static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
+static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
{
int w, i, step, nWords;
if ( nVarS == nVarB )
@@ -394,7 +1200,7 @@ static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
for ( i = 0; i < step; i++ )
pInOut[w + i] = pInOut[i];
}
-static void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
+static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
{
int w, i, step, nWords;
if ( nVarS == nVarB )
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 09:57:25 +0000