summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c1
-rw-r--r--src/base/abci/abcNpn.c18
-rw-r--r--src/misc/util/utilTruth.h531
-rw-r--r--src/opt/dau/dau.h69
-rw-r--r--src/opt/dau/dauCanon.c1370
5 files changed, 889 insertions, 1100 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b973aba7..3b6746ed 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4937,6 +4937,7 @@ usage:
Abc_Print( -2, "\t 2: semi-canonical form by counting 1s in cofactors\n" );
Abc_Print( -2, "\t 3: Jake's hybrid semi-canonical form (fast)\n" );
Abc_Print( -2, "\t 4: Jake's hybrid semi-canonical form (high-effort)\n" );
+ Abc_Print( -2, "\t 5: new fast hybrid semi-canonical form\n" );
Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
Abc_Print( -2, "\t-d : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" );
Abc_Print( -2, "\t-b : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 759d91b3..ffcf00f7 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -23,6 +23,7 @@
#include "bool/kit/kit.h"
#include "bool/lucky/lucky.h"
+#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START
@@ -190,6 +191,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
pAlgoName = "Jake's hybrid fast ";
else if ( NpnType == 4 )
pAlgoName = "Jake's hybrid good ";
+ else if ( NpnType == 5 )
+ pAlgoName = "new hybrid fast ";
assert( p->nVars <= 16 );
if ( pAlgoName )
@@ -202,10 +205,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
for ( i = 0; i < p->nFuncs; i++ )
{
- extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i );
if ( fVerbose )
printf( "%7d : ", i );
- Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
}
@@ -261,6 +262,17 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
}
}
+ else if ( NpnType == 5 )
+ {
+ for ( i = 0; i < p->nFuncs; i++ )
+ {
+ if ( fVerbose )
+ printf( "%7d : ", i );
+ uCanonPhase = Abc_TtCanonicize( p->pFuncs[i], p->nVars, pCanonPerm );
+ if ( fVerbose )
+ Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
+ }
+ }
else assert( 0 );
clk = clock() - clk;
printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
@@ -324,7 +336,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
{
if ( fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
- if ( NpnType >= 0 && NpnType <= 4 )
+ if ( NpnType >= 0 && NpnType <= 5 )
Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
else
printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 236c0d62..c742aac9 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -61,6 +61,14 @@ static word s_CMasks6[5] = {
0x000000000000FFFF
};
+static word s_PMasks[5][3] = {
+ { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+ { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+ { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+ { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+ { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -161,10 +169,9 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
return 1;
}
-
/**Function*************************************************************
- Synopsis [Compares Cof0 and Cof1.]
+ Synopsis []
Description []
@@ -173,217 +180,42 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
SeeAlso []
***********************************************************************/
-static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
+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 )
{
- 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;
+ pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
}
- // if ( iVar > 5 )
+ else // 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;
+ pTruth[i + iStep] = pTruth[i];
}
}
-static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
+static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
{
- assert( Num1 < Num2 && Num2 < 4 );
if ( nWords == 1 )
+ pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
+ else if ( iVar <= 5 )
{
- 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;
+ pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
}
- // if ( iVar > 5 )
+ else // 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 ( ; pTruth < pLimit; pTruth += 2*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;
+ pTruth[i] = pTruth[i + iStep];
}
}
@@ -449,56 +281,6 @@ static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int
}
}
-/**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*************************************************************
@@ -826,6 +608,10 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
SeeAlso []
***********************************************************************/
+static inline word Abc_Tt6Flip( word Truth, int iVar )
+{
+ return Truth = ((Truth << (1 << iVar)) & s_Truths6[iVar]) | ((Truth & s_Truths6[iVar]) >> (1 << iVar));
+}
static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
{
if ( nWords == 1 )
@@ -857,9 +643,13 @@ static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
SeeAlso []
***********************************************************************/
+static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar )
+{
+ return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar));
+}
static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
{
- static word PMasks[5][3] = {
+ static word s_PMasks[5][3] = {
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
@@ -870,7 +660,7 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
{
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);
+ pTruth[i] = (pTruth[i] & s_PMasks[iVar][0]) | ((pTruth[i] & s_PMasks[iVar][1]) << Shift) | ((pTruth[i] & s_PMasks[iVar][2]) >> Shift);
}
else if ( iVar == 5 )
{
@@ -888,10 +678,9 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
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] = {
+ static word Ps_PMasks[5][6][3] = {
{
{ 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1
@@ -940,18 +729,18 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
assert( iVar < jVar && jVar < nVars );
if ( nVars <= 6 )
{
- word * pMasks = PPMasks[iVar][jVar];
+ word * s_PMasks = Ps_PMasks[iVar][jVar];
int shift = (1 << jVar) - (1 << iVar);
- pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift);
+ pTruth[0] = (pTruth[0] & s_PMasks[0]) | ((pTruth[0] & s_PMasks[1]) << shift) | ((pTruth[0] & s_PMasks[2]) >> shift);
return;
}
if ( jVar <= 5 )
{
- word * pMasks = PPMasks[iVar][jVar];
+ word * s_PMasks = Ps_PMasks[iVar][jVar];
int nWords = Abc_TtWordNum(nVars);
int w, shift = (1 << jVar) - (1 << iVar);
for ( w = 0; w < nWords; w++ )
- pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
+ pTruth[w] = (pTruth[w] & s_PMasks[0]) | ((pTruth[w] & s_PMasks[1]) << shift) | ((pTruth[w] & s_PMasks[2]) >> shift);
return;
}
if ( iVar <= 5 && jVar > 5 )
@@ -984,6 +773,38 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
/**Function*************************************************************
+ Synopsis [Implemeting given NPN config.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
+{
+ int i, k, nWords = Abc_TtWordNum( nVars );
+ if ( (uCanonPhase >> nVars) & 1 )
+ Abc_TtNot( pTruth, nWords );
+ for ( i = 0; i < nVars; i++ )
+ if ( (uCanonPhase >> i) & 1 )
+ Abc_TtFlip( pTruth, nWords, i );
+ for ( i = 0; i < nVars; i++ )
+ {
+ for ( k = i; k < nVars; k++ )
+ if ( pCanonPerm[k] == i )
+ break;
+ assert( k < nVars );
+ if ( i == k )
+ continue;
+ Abc_TtSwapVars( pTruth, nVars, i, k );
+ ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -1024,220 +845,6 @@ static inline int Abc_TtCountOnes( word x )
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++ )
- if ( pTruth[k] )
- Counter += Abc_TtCountOnes( pTruth[k] );
- return Counter;
-}
-static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
-{
- word Temp;
- int i, k, Counter, nWords;
- if ( nVars <= 6 )
- {
- for ( i = 0; i < nVars; i++ )
- if ( pTruth[0] & s_Truths6Neg[i] )
- pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
- else
- pStore[i] = 0;
- return;
- }
- assert( nVars > 6 );
- nWords = Abc_TtWordNum( nVars );
- memset( pStore, 0, sizeof(int) * nVars );
- for ( k = 0; k < nWords; k++ )
- {
- // count 1's for the first six variables
- for ( i = 0; i < 6; i++ )
- if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) )
- pStore[i] += Abc_TtCountOnes( Temp );
- // count 1's for all other variables
- if ( pTruth[k] )
- {
- Counter = Abc_TtCountOnes( pTruth[k] );
- for ( i = 6; i < nVars; i++ )
- if ( (k & (1 << (i-6))) == 0 )
- pStore[i] += Counter;
- }
- k++;
- // count 1's for all other variables
- if ( pTruth[k] )
- {
- 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 * pStoreOut )
-{
- extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore );
-
- int fOldSwap = 0;
- int pStoreIn[17];
- int * pStore = pStoreOut ? pStoreOut : pStoreIn;
-// int pStore2[17];
- int nWords = Abc_TtWordNum( nVars );
- int i, Temp, nOnes;//, fChange;//, nSwaps = 0;//;
- int k, BestK;
- unsigned uCanonPhase = 0;
- assert( nVars <= 16 );
- for ( i = 0; i < nVars; i++ )
- pCanonPerm[i] = i;
- // 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 );
- pStore[nVars] = nOnes;
-// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore );
-
-// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 );
-// for ( i = 0; i < nVars; i++ )
-// assert( pStore[i] == pStore2[i] );
-
- 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];
- }
-
- if ( fOldSwap )
- {
- int fChange;
- do {
- fChange = 0;
- for ( i = 0; i < nVars-1; i++ )
- {
- // if ( pStore[i] <= pStore[i+1] )
- 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) )
- {
- uCanonPhase ^= (1 << i);
- uCanonPhase ^= (1 << (i+1));
- }
- Abc_TtSwapAdjacent( pTruth, nWords, i );
- fChange = 1;
- // nSwaps++;
- }
- } while ( fChange );
- }
- else
- {
- for ( i = 0; i < nVars - 1; i++ )
- {
- BestK = i + 1;
- for ( k = i + 2; k < nVars; k++ )
- // if ( pStore[BestK] > pStore[k] )
- if ( pStore[BestK] < pStore[k] )
- BestK = k;
- // if ( pStore[i] <= pStore[BestK] )
- if ( pStore[i] >= pStore[BestK] )
- continue;
-
- Temp = pCanonPerm[i];
- pCanonPerm[i] = pCanonPerm[BestK];
- pCanonPerm[BestK] = Temp;
-
- Temp = pStore[i];
- pStore[i] = pStore[BestK];
- pStore[BestK] = Temp;
-
- if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
- {
- uCanonPhase ^= (1 << i);
- uCanonPhase ^= (1 << BestK);
- }
- Abc_TtSwapVars( pTruth, nVars, i, BestK );
- // nSwaps++;
- }
- }
-
-
-// printf( "%d ", nSwaps );
-/*
- printf( "Minterms: " );
- for ( i = 0; i < nVars; i++ )
- printf( "%d ", pStore[i] );
- printf( "\n" );
-*/
- return uCanonPhase;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
static inline void Abc_TtReverseVars( word * pTruth, int nVars )
{
int k;
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
new file mode 100644
index 00000000..b65a1b2c
--- /dev/null
+++ b/src/opt/dau/dau.h
@@ -0,0 +1,69 @@
+/**CFile****************************************************************
+
+ FileName [dau.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware unmapping.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: dau.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__DAU___h
+#define ABC__DAU___h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "misc/vec/vec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dauCanon.c ==========================================================*/
+extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index b66b276b..2853f238 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -30,10 +30,10 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-
+
/**Function*************************************************************
- Synopsis [Generate reverse bytes.]
+ Synopsis [Compares Cof0 and Cof1.]
Description []
@@ -42,26 +42,80 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-void Abc_TtReverseBypes()
+static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
{
- int i, k;
- for ( i = 0; i < 256; i++ )
+ if ( nWords == 1 )
{
- int Mask = 0;
- for ( k = 0; k < 8; k++ )
- if ( (i >> k) & 1 )
- Mask |= (1 << (7-k));
-// printf( "%3d %3d\n", i, Mask );
-
- if ( i % 16 == 0 )
- printf( "\n" );
- printf( "%-3d, ", Mask );
+ 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 []
+ Synopsis [Checks equality of pairs of cofactors w.r.t. adjacent variables.]
Description []
@@ -70,722 +124,772 @@ void Abc_TtReverseBypes()
SeeAlso []
***********************************************************************/
-void Abc_TtCofactorTest7( word * pTruth, int nVars, int N )
+static inline int Abc_TtCheckEqual2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
{
- word Cof[4][1024];
- int i, nWords = Abc_TtWordNum( nVars );
-// int Counter = 0;
- for ( i = 0; i < nVars-1; i++ )
+ 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 )
{
- Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[0], nWords, i );
- Abc_TtCofactor0( Cof[0], nWords, i + 1 );
+ 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;
+ }
+}
- Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[1], nWords, i );
- Abc_TtCofactor0( Cof[1], nWords, i + 1 );
+/**Function*************************************************************
- Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[2], nWords, i );
- Abc_TtCofactor1( Cof[2], nWords, i + 1 );
+ Synopsis [Compares pairs of cofactors w.r.t. adjacent variables.]
- Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[3], nWords, i );
- Abc_TtCofactor1( Cof[3], nWords, i + 1 );
+ Description []
+
+ SideEffects []
- if ( i == 5 && N == 4 )
- {
- printf( "\n" );
- Abc_TtPrintHex( Cof[0], nVars );
- Abc_TtPrintHex( Cof[1], nVars );
- Abc_TtPrintHex( Cof[2], nVars );
- Abc_TtPrintHex( Cof[3], nVars );
- }
+ SeeAlso []
- assert( Abc_TtCompareRev(Cof[0], Cof[1], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) );
- assert( Abc_TtCompareRev(Cof[0], Cof[2], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) );
- assert( Abc_TtCompareRev(Cof[0], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) );
- assert( Abc_TtCompareRev(Cof[1], Cof[2], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) );
- assert( Abc_TtCompareRev(Cof[1], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) );
- assert( Abc_TtCompareRev(Cof[2], Cof[3], nWords) == Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) );
-/*
- Counter += Abc_TtCompare(Cof[0], Cof[1], nWords);
- Counter += Abc_TtCompare(Cof[0], Cof[2], nWords);
- Counter += Abc_TtCompare(Cof[0], Cof[3], nWords);
- Counter += Abc_TtCompare(Cof[1], Cof[2], nWords);
- Counter += Abc_TtCompare(Cof[1], Cof[3], nWords);
- Counter += Abc_TtCompare(Cof[2], Cof[3], nWords);
-
- Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 1);
- Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 2);
- Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 0, 3);
- Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 1, 2);
- Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 1, 3);
- Counter += Abc_TtCompare2VarCofs(pTruth, nWords, i, 2, 3);
-*/
- }
-}
-void Abc_TtCofactorTest2( word * pTruth, int nVars, int N )
+***********************************************************************/
+static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
{
-// word Cof[4][1024];
- int i, j, nWords = Abc_TtWordNum( nVars );
- int Counter = 0;
- for ( i = 0; i < nVars-1; i++ )
- for ( j = i+1; j < nVars; j++ )
+ assert( Num1 < Num2 && Num2 < 4 );
+ if ( nWords == 1 )
{
-/*
- Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[0], nWords, i );
- Abc_TtCofactor0( Cof[0], nWords, j );
-
- Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[1], nWords, i );
- Abc_TtCofactor0( Cof[1], nWords, j );
-
- Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[2], nWords, i );
- Abc_TtCofactor1( Cof[2], nWords, j );
-
- Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[3], nWords, i );
- Abc_TtCofactor1( Cof[3], nWords, j );
-*/
-/*
- if ( i == 0 && j == 1 && N == 0 )
+ 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++ )
{
- printf( "\n" );
- Abc_TtPrintHexSpecial( Cof[0], nVars ); printf( "\n" );
- Abc_TtPrintHexSpecial( Cof[1], nVars ); printf( "\n" );
- Abc_TtPrintHexSpecial( Cof[2], nVars ); printf( "\n" );
- Abc_TtPrintHexSpecial( Cof[3], nVars ); printf( "\n" );
+ Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+ Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+ if ( Cof1 != Cof2 )
+ return Cof1 < Cof2 ? -1 : 1;
}
-*/
-/*
- assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) );
- assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) );
- assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) );
- assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) );
- assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) );
- assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) );
-*/
-
- Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1);
- Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2);
- Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3);
- Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2);
- Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3);
- Counter += Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3);
-/*
- Counter += Abc_TtEqual(Cof[0], Cof[1], nWords);
- Counter += Abc_TtEqual(Cof[0], Cof[2], nWords);
- Counter += Abc_TtEqual(Cof[0], Cof[3], nWords);
- Counter += Abc_TtEqual(Cof[1], Cof[2], nWords);
- Counter += Abc_TtEqual(Cof[1], Cof[3], nWords);
- Counter += Abc_TtEqual(Cof[2], Cof[3], nWords);
-*/
+ return 0;
}
-}
-void Abc_TtCofactorTest3( word * pTruth, int nVars, int N )
-{
- word Cof[4][1024];
- int i, j, nWords = Abc_TtWordNum( nVars );
- for ( i = 0; i < nVars-1; i++ )
- for ( j = i+1; j < nVars; j++ )
- {
- Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[0], nWords, i );
- Abc_TtCofactor0( Cof[0], nWords, j );
-
- Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[1], nWords, i );
- Abc_TtCofactor0( Cof[1], nWords, j );
-
- Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[2], nWords, i );
- Abc_TtCofactor1( Cof[2], nWords, j );
-
- Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[3], nWords, i );
- Abc_TtCofactor1( Cof[3], nWords, j );
-
- assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) );
- assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) );
- assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) );
- assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) );
- assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) );
- assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) );
+ 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;
+ }
}
-
-void Abc_TtCofactorTest4( word * pTruth, int nVars, int N )
+static inline int Abc_TtCompare2VarCofsRev( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
{
- word Cof[4][1024];
- int i, j, nWords = Abc_TtWordNum( nVars );
- int Sum = 0;
- for ( i = 0; i < nVars-1; i++ )
- for ( j = i+1; j < nVars; j++ )
- {
- Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[0], nWords, i );
- Abc_TtCofactor0( Cof[0], nWords, j );
-
- Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[1], nWords, i );
- Abc_TtCofactor0( Cof[1], nWords, j );
-
- Abc_TtCopy( Cof[2], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[2], nWords, i );
- Abc_TtCofactor1( Cof[2], nWords, j );
-
- Abc_TtCopy( Cof[3], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[3], nWords, i );
- Abc_TtCofactor1( Cof[3], nWords, j );
-
-
- Sum = 0;
- Sum += Abc_TtEqual(Cof[0], Cof[1], nWords);
- Sum += Abc_TtEqual(Cof[0], Cof[2], nWords);
- Sum += Abc_TtEqual(Cof[0], Cof[3], nWords);
- Sum += Abc_TtEqual(Cof[1], Cof[2], nWords);
- Sum += Abc_TtEqual(Cof[1], Cof[3], nWords);
- Sum += Abc_TtEqual(Cof[2], Cof[3], nWords);
-
- assert( Abc_TtEqual(Cof[0], Cof[1], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 1) );
- assert( Abc_TtEqual(Cof[0], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 2) );
- assert( Abc_TtEqual(Cof[0], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 0, 3) );
- assert( Abc_TtEqual(Cof[1], Cof[2], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 2) );
- assert( Abc_TtEqual(Cof[1], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 1, 3) );
- assert( Abc_TtEqual(Cof[2], Cof[3], nWords) == Abc_TtCheckEqualCofs(pTruth, nWords, i, j, 2, 3) );
+ 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;
}
-}
-
-void Abc_TtCofactorTest6( word * pTruth, int nVars, int N )
-{
-// word Cof[4][1024];
- int i, nWords = Abc_TtWordNum( nVars );
-// if ( N != 30 )
-// return;
- printf( "\n " );
- Abc_TtPrintHex( pTruth, nVars );
-// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
-
- for ( i = nVars - 1; i >= 0; i-- )
+ if ( iVar <= 4 )
{
-/*
- Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[0], nWords, i );
- printf( "- " );
- Abc_TtPrintHex( Cof[0], nVars );
-
- Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[1], nWords, i );
- printf( "+ " );
- Abc_TtPrintHex( Cof[1], nVars );
-*/
- if ( Abc_TtCompare1VarCofsRev( pTruth, nWords, i ) == -1 )
+ word Cof1, Cof2;
+ int w, shift = (1 << iVar);
+ for ( w = nWords - 1; w >= 0; w-- )
{
- printf( "%d ", i );
- Abc_TtFlip( pTruth, nWords, i );
- Abc_TtPrintHex( pTruth, nVars );
-// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
+ Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
+ Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
+ if ( Cof1 != Cof2 )
+ return Cof1 < Cof2 ? -1 : 1;
}
-
-
-/*
- Abc_TtCopy( Cof[0], pTruth, nWords, 0 );
- Abc_TtCofactor0( Cof[0], nWords, i );
-
- Abc_TtCopy( Cof[1], pTruth, nWords, 0 );
- Abc_TtCofactor1( Cof[1], nWords, i );
-
- assert( Abc_TtCompareRev(Cof[0], Cof[1], nWords) == Abc_TtCompare1VarCofsRev(pTruth, nWords, i) );
-*/
+ return 0;
}
- i = 0;
-}
-
-int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
-{
- static word pCopy[1024];
- static word pBest[1024];
-
- if ( fSwapOnly )
+ if ( iVar == 5 )
{
- Abc_TtCopy( pCopy, pTruth, nWords, 0 );
- Abc_TtSwapAdjacent( pCopy, nWords, i );
- if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
- {
- Abc_TtCopy( pTruth, pCopy, nWords, 0 );
- return 1;
- }
+ 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;
}
-
- // save two copies
- Abc_TtCopy( pCopy, pTruth, nWords, 0 );
- Abc_TtCopy( pBest, pTruth, nWords, 0 );
-
- // PXY
- // 001
- Abc_TtFlip( pCopy, nWords, i );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 011
- Abc_TtFlip( pCopy, nWords, i+1 );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 010
- Abc_TtFlip( pCopy, nWords, i );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 110
- Abc_TtSwapAdjacent( pCopy, nWords, i );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 111
- Abc_TtFlip( pCopy, nWords, i+1 );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 101
- Abc_TtFlip( pCopy, nWords, i );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 100
- Abc_TtFlip( pCopy, nWords, i+1 );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- // PXY
- // 000
- Abc_TtSwapAdjacent( pCopy, nWords, i );
- if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
- Abc_TtCopy( pBest, pCopy, nWords, 0 );
-
- assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
- if ( Abc_TtEqual( pTruth, pBest, nWords ) )
+ // 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;
- assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
- Abc_TtCopy( pTruth, pBest, nWords, 0 );
- return 1;
+ }
}
+/**Function*************************************************************
-int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, char * pCanonPerm, unsigned * puCanonPhase, int fSwapOnly )
-{
- static word pCopy1[1024];
- int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23;
- unsigned uPhaseInit = *puCanonPhase;
- int RetValue = 0;
-
- if ( fSwapOnly )
- {
- fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
- if ( fComp12 < 0 ) // Cof1 < Cof2
- {
- Abc_TtSwapAdjacent( pTruth, nWords, i );
- RetValue = 1;
+ Synopsis [Minterm counting in all cofactors.]
- if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
- {
- *puCanonPhase ^= (1 << i);
- *puCanonPhase ^= (1 << (i+1));
- }
+ Description []
+
+ SideEffects []
- ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
- }
- return RetValue;
- }
+ SeeAlso []
- Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
-
- fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
- fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
- if ( fComp23 >= 0 ) // Cof2 >= Cof3
+***********************************************************************/
+static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
+{
+ int nWords = Abc_TtWordNum( nVars );
+ int k, Counter = 0;
+ for ( k = 0; k < nWords; k++ )
+ if ( pTruth[k] )
+ Counter += Abc_TtCountOnes( pTruth[k] );
+ return Counter;
+}
+static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore )
+{
+ word Temp;
+ int i, k, Counter, nWords;
+ if ( nVars <= 6 )
{
- if ( fComp01 >= 0 ) // Cof0 >= Cof1
- {
- fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
- if ( fComp13 < 0 ) // Cof1 < Cof3
- {
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << (i+1));
- RetValue = 1;
- }
- else if ( fComp13 == 0 ) // Cof1 == Cof3
- {
- fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
- if ( fComp02 < 0 )
- {
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << (i+1));
- RetValue = 1;
- }
- }
- // else Cof1 > Cof3 -- do nothing
- }
- else // Cof0 < Cof1
- {
- fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
- if ( fComp03 < 0 ) // Cof0 < Cof3
- {
- Abc_TtFlip( pTruth, nWords, i );
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << i);
- *puCanonPhase ^= (1 << (i+1));
- RetValue = 1;
- }
- else // Cof0 >= Cof3
- {
- if ( fComp23 == 0 ) // can flip Cof0 and Cof1
- {
- Abc_TtFlip( pTruth, nWords, i );
- *puCanonPhase ^= (1 << i);
- RetValue = 1;
- }
- }
- }
+ for ( i = 0; i < nVars; i++ )
+ pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
+ return;
}
- else // Cof2 < Cof3
+ assert( nVars > 6 );
+ nWords = Abc_TtWordNum( nVars );
+ memset( pStore, 0, sizeof(int) * nVars );
+ for ( k = 0; k < nWords; k++ )
{
- if ( fComp01 >= 0 ) // Cof0 >= Cof1
+ // count 1's for the first six variables
+ for ( i = 0; i < 6; i++ )
+ if ( (Temp = (pTruth[k] & s_Truths6Neg[i]) | ((pTruth[k+1] & s_Truths6Neg[i]) << (1 << i))) )
+ pStore[i] += Abc_TtCountOnes( Temp );
+ // count 1's for all other variables
+ if ( pTruth[k] )
{
- fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
- if ( fComp12 > 0 ) // Cof1 > Cof2
- {
- Abc_TtFlip( pTruth, nWords, i );
- *puCanonPhase ^= (1 << i);
- }
- else if ( fComp12 == 0 ) // Cof1 == Cof2
- {
- Abc_TtFlip( pTruth, nWords, i );
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << i);
- *puCanonPhase ^= (1 << (i+1));
- }
- else // Cof1 < Cof2
- {
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << (i+1));
- if ( fComp01 == 0 )
- {
- Abc_TtFlip( pTruth, nWords, i );
- *puCanonPhase ^= (1 << i);
- }
- }
+ Counter = Abc_TtCountOnes( pTruth[k] );
+ for ( i = 6; i < nVars; i++ )
+ if ( (k & (1 << (i-6))) == 0 )
+ pStore[i] += Counter;
}
- else // Cof0 < Cof1
+ k++;
+ // count 1's for all other variables
+ if ( pTruth[k] )
{
- fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
- if ( fComp02 == -1 ) // Cof0 < Cof2
- {
- Abc_TtFlip( pTruth, nWords, i );
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << i);
- *puCanonPhase ^= (1 << (i+1));
- }
- else if ( fComp02 == 0 ) // Cof0 == Cof2
- {
- fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
- if ( fComp13 >= 0 ) // Cof1 >= Cof3
- {
- Abc_TtFlip( pTruth, nWords, i );
- *puCanonPhase ^= (1 << i);
- }
- else // Cof1 < Cof3
- {
- Abc_TtFlip( pTruth, nWords, i );
- Abc_TtFlip( pTruth, nWords, i + 1 );
- *puCanonPhase ^= (1 << i);
- *puCanonPhase ^= (1 << (i+1));
- }
- }
- else // Cof0 > Cof2
- {
- Abc_TtFlip( pTruth, nWords, i );
- *puCanonPhase ^= (1 << i);
- }
+ Counter = Abc_TtCountOnes( pTruth[k] );
+ for ( i = 6; i < nVars; i++ )
+ if ( (k & (1 << (i-6))) == 0 )
+ pStore[i] += Counter;
}
- RetValue = 1;
- }
- // perform final swap if needed
- fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
- if ( fComp12 < 0 ) // Cof1 < Cof2
- {
- Abc_TtSwapAdjacent( pTruth, nWords, i );
- RetValue = 1;
+ }
+}
- if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
- {
- *puCanonPhase ^= (1 << i);
- *puCanonPhase ^= (1 << (i+1));
- }
+/**Function*************************************************************
- ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
- }
+ Synopsis [Minterm counting in all cofactors.]
- if ( RetValue == 1 )
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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++ )
{
- if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
- {
- Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
- // undo the flips
- *puCanonPhase = uPhaseInit;
- // undo the swap
- if ( fComp12 < 0 ) // Cof1 < Cof2
- ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
- RetValue = 0;
- }
+ 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]];
}
- return RetValue;
}
+/**Function*************************************************************
-void Abc_TtCofactorTest__( word * pTruth, int nVars, int N )
-{
- char pCanonPerm[16];
- unsigned uCanonPhase;
- static word pCopy1[1024];
- static word pCopy2[1024];
- int i, nWords = Abc_TtWordNum( nVars );
- static int Counter = 0;
+ Synopsis [Minterm counting in all cofactors.]
-// pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2];
-// nVars = 3;
+ Description []
+
+ SideEffects []
-/*
- printf( "\n" );
- Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
- Abc_TtPrintBinary( pTruth, nVars );
- printf( "\n" );
-*/
+ SeeAlso []
-// for ( i = nVars - 2; i >= 0; i-- )
- for ( i = 3; i < nVars - 1; i++ )
+***********************************************************************/
+int Abc_TtCountOnesInCofsFast6_rec( word Truth, int iVar, int nBytes, 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 nMints0, nMints1;
+ if ( Truth == 0 )
+ return 0;
+ if ( ~Truth == 0 )
{
-/*
- word Cof0s = Abc_Tt6Cof0( pTruth[0], i+1 );
- word Cof1s = Abc_Tt6Cof1( pTruth[0], i+1 );
-
- word Cof0 = Abc_Tt6Cof0( Cof0s, i );
- word Cof1 = Abc_Tt6Cof1( Cof0s, i );
- word Cof2 = Abc_Tt6Cof0( Cof1s, i );
- word Cof3 = Abc_Tt6Cof1( Cof1s, i );
-
- Abc_TtPrintBinary( &Cof0, 6 );
- Abc_TtPrintBinary( &Cof1, 6 );
- Abc_TtPrintBinary( &Cof2, 6 );
- Abc_TtPrintBinary( &Cof3, 6 );
-
- printf( "01 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) );
- printf( "02 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) );
- printf( "03 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) );
- printf( "12 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 2) );
- printf( "13 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 1, 3) );
- printf( "23 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 2, 3) );
-
- if ( i == 0 && N == 74 )
+ int i;
+ for ( i = 0; i <= iVar; i++ )
+ pStore[i] += nBytes * 4;
+ return nBytes * 8;
+ }
+ if ( nBytes == 1 )
+ {
+ assert( iVar == 2 );
+ pStore[0] += bit_count[ Truth & 0x55 ];
+ pStore[1] += bit_count[ Truth & 0x33 ];
+ pStore[2] += bit_count[ Truth & 0x0F ];
+ return bit_count[ Truth & 0xFF ];
+ }
+ nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof0(Truth, iVar), iVar - 1, nBytes/2, pStore );
+ nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof1(Truth, iVar), iVar - 1, nBytes/2, pStore );
+ pStore[iVar] += nMints0;
+ return nMints0 + nMints1;
+}
+
+int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore )
+{
+ int nMints0, nMints1;
+ if ( nWords == 1 )
+ {
+ assert( iVar == 5 );
+ return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], iVar, 8, pStore );
+ }
+ assert( nWords > 1 );
+ assert( iVar > 5 );
+ if ( pTruth[0] & 1 )
+ {
+ if ( Abc_TtIsConst1( pTruth, nWords ) )
{
- int s = 0;
- continue;
+ int i;
+ for ( i = 0; i <= iVar; i++ )
+ pStore[i] += nWords * 32;
+ return nWords * 64;
}
-*/
- Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
- Abc_TtCofactorPermNaive( pCopy1, i, nWords, 0 );
-
- Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
- Abc_TtCofactorPerm( pCopy2, i, nWords, pCanonPerm, &uCanonPhase, 0 );
-
-// assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
- if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
- Counter++;
-
}
- if ( Counter % 1000 == 0 )
- printf( "%d ", Counter );
-
+ else
+ {
+ if ( Abc_TtIsConst0( pTruth, nWords ) )
+ return 0;
+ }
+ nMints0 = Abc_TtCountOnesInCofsFast_rec( pTruth, iVar - 1, nWords/2, pStore );
+ nMints1 = Abc_TtCountOnesInCofsFast_rec( pTruth + nWords/2, iVar - 1, nWords/2, pStore );
+ pStore[iVar] += nMints0;
+ return nMints0 + nMints1;
+}
+int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore )
+{
+ memset( pStore, 0, sizeof(int) * nVars );
+ assert( nVars >= 3 );
+ if ( nVars <= 6 )
+ return Abc_TtCountOnesInCofsFast6_rec( pTruth[0], nVars - 1, Abc_TtByteNum( nVars ), pStore );
+ else
+ return Abc_TtCountOnesInCofsFast_rec( pTruth, nVars - 1, Abc_TtWordNum( nVars ), pStore );
}
+/**Function*************************************************************
-void Abc_TtCofactorTest8( word * pTruth, int nVars, int N )
-{
- int fVerbose = 0;
- int i;
- int nWords = Abc_TtWordNum( nVars );
+ Synopsis []
- if ( fVerbose )
- printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
+ Description []
+
+ SideEffects []
- if ( fVerbose )
- printf( "Round 1\n" );
- for ( i = nVars - 2; i >= 0; i-- )
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut )
+{
+ int fOldSwap = 0;
+ int pStoreIn[17];
+ int * pStore = pStoreOut ? pStoreOut : pStoreIn;
+ int i, nOnes, nWords = Abc_TtWordNum( nVars );
+ unsigned uCanonPhase = 0;
+ assert( nVars <= 16 );
+ for ( i = 0; i < nVars; i++ )
+ pCanonPerm[i] = i;
+ // normalize polarity
+ nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
+ if ( nOnes > nWords * 32 )
{
- if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
- {
- if ( fVerbose )
- printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
- }
+ Abc_TtNot( pTruth, nWords );
+ nOnes = nWords*64 - nOnes;
+ uCanonPhase |= (1 << nVars);
}
-
- if ( fVerbose )
- printf( "Round 2\n" );
- for ( i = 0; i < nVars - 1; i++ )
+ // normalize phase
+ Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+ pStore[nVars] = nOnes;
+ for ( i = 0; i < nVars; i++ )
{
- if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
- {
- if ( fVerbose )
- printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
- }
+ if ( pStore[i] >= nOnes - pStore[i] )
+ continue;
+ Abc_TtFlip( pTruth, nWords, i );
+ uCanonPhase |= (1 << i);
+ pStore[i] = nOnes - pStore[i];
}
-
- return;
-
- if ( fVerbose )
- printf( "Round 3\n" );
- for ( i = nVars - 2; i >= 0; i-- )
+ // normalize permutation
+ if ( fOldSwap )
{
- if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
- {
- if ( fVerbose )
- printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
- }
+ int fChange;
+ do {
+ fChange = 0;
+ for ( i = 0; i < nVars-1; i++ )
+ {
+ if ( pStore[i] <= pStore[i+1] )
+ // if ( pStore[i] >= pStore[i+1] )
+ continue;
+ ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
+ ABC_SWAP( int, pStore[i], pStore[i+1] );
+ if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
+ {
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << (i+1));
+ }
+ Abc_TtSwapAdjacent( pTruth, nWords, i );
+ fChange = 1;
+ // nSwaps++;
+ }
+ }
+ while ( fChange );
}
-
- if ( fVerbose )
- printf( "Round 4\n" );
- for ( i = 0; i < nVars - 1; i++ )
+ else
{
- if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
+ int k, BestK;
+ for ( i = 0; i < nVars - 1; i++ )
{
- if ( fVerbose )
- printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
+ BestK = i + 1;
+ for ( k = i + 2; k < nVars; k++ )
+ if ( pStore[BestK] > pStore[k] )
+ // if ( pStore[BestK] < pStore[k] )
+ BestK = k;
+ if ( pStore[i] <= pStore[BestK] )
+ // if ( pStore[i] >= pStore[BestK] )
+ continue;
+ ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
+ ABC_SWAP( int, pStore[i], pStore[BestK] );
+ if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
+ {
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << BestK);
+ }
+ Abc_TtSwapVars( pTruth, nVars, i, BestK );
+ // nSwaps++;
}
}
- i = 0;
+ return uCanonPhase;
}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Abc_TtCofactorTest10( word * pTruth, int nVars, int N )
{
static word pCopy1[1024];
static word pCopy2[1024];
int nWords = Abc_TtWordNum( nVars );
int i;
-
for ( i = 0; i < nVars - 1; i++ )
{
// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
-
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
Abc_TtSwapAdjacent( pCopy1, nWords, i );
// Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
-
Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
Abc_TtSwapVars( pCopy2, nVars, i, i+1 );
// Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
-
assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
}
}
+/**Function*************************************************************
-void Abc_TtCofactorTest111( word * pTruth, int nVars, int N )
-{
- char pCanonPerm[32];
- static word pCopy1[1024];
- static word pCopy2[1024];
- int nWords = Abc_TtWordNum( nVars );
-
-// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
+ Synopsis [Naive evaluation.]
- Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
-// Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm );
-// Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
+ Description []
+
+ SideEffects []
- Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
- Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL );
-// Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
+ SeeAlso []
- assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
+***********************************************************************/
+int Abc_Tt6CofactorPermNaive( word * pTruth, int i, int fSwapOnly )
+{
+ if ( fSwapOnly )
+ {
+ word Copy = Abc_Tt6SwapAdjacent( pTruth[0], i );
+ if ( pTruth[0] > Copy )
+ {
+ pTruth[0] = Copy;
+ return 4;
+ }
+ return 0;
+ }
+ {
+ word Copy = pTruth[0];
+ word Best = pTruth[0];
+ int Config = 0;
+ // PXY
+ // 001
+ Copy = Abc_Tt6Flip( Copy, i );
+ if ( Best > Copy )
+ Best = Copy, Config = 1;
+ // PXY
+ // 011
+ Copy = Abc_Tt6Flip( Copy, i+1 );
+ if ( Best > Copy )
+ Best = Copy, Config = 3;
+ // PXY
+ // 010
+ Copy = Abc_Tt6Flip( Copy, i );
+ if ( Best > Copy )
+ Best = Copy, Config = 2;
+ // PXY
+ // 110
+ Copy = Abc_Tt6SwapAdjacent( Copy, i );
+ if ( Best > Copy )
+ Best = Copy, Config = 6;
+ // PXY
+ // 111
+ Copy = Abc_Tt6Flip( Copy, i+1 );
+ if ( Best > Copy )
+ Best = Copy, Config = 7;
+ // PXY
+ // 101
+ Copy = Abc_Tt6Flip( Copy, i );
+ if ( Best > Copy )
+ Best = Copy, Config = 5;
+ // PXY
+ // 100
+ Copy = Abc_Tt6Flip( Copy, i+1 );
+ if ( Best > Copy )
+ Best = Copy, Config = 4;
+ // PXY
+ // 000
+ Copy = Abc_Tt6SwapAdjacent( Copy, i );
+ assert( Copy == pTruth[0] );
+ assert( Best <= pTruth[0] );
+ pTruth[0] = Best;
+ return Config;
+ }
+}
+int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
+{
+ if ( fSwapOnly )
+ {
+ static word pCopy[1024];
+ Abc_TtCopy( pCopy, pTruth, nWords, 0 );
+ Abc_TtSwapAdjacent( pCopy, nWords, i );
+ if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 )
+ {
+ Abc_TtCopy( pTruth, pCopy, nWords, 0 );
+ return 4;
+ }
+ return 0;
+ }
+ {
+ static word pCopy[1024];
+ static word pBest[1024];
+ int Config = 0;
+ // save two copies
+ Abc_TtCopy( pCopy, pTruth, nWords, 0 );
+ Abc_TtCopy( pBest, pTruth, nWords, 0 );
+ // PXY
+ // 001
+ Abc_TtFlip( pCopy, nWords, i );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 1;
+ // PXY
+ // 011
+ Abc_TtFlip( pCopy, nWords, i+1 );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 3;
+ // PXY
+ // 010
+ Abc_TtFlip( pCopy, nWords, i );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 2;
+ // PXY
+ // 110
+ Abc_TtSwapAdjacent( pCopy, nWords, i );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 6;
+ // PXY
+ // 111
+ Abc_TtFlip( pCopy, nWords, i+1 );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 7;
+ // PXY
+ // 101
+ Abc_TtFlip( pCopy, nWords, i );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 5;
+ // PXY
+ // 100
+ Abc_TtFlip( pCopy, nWords, i+1 );
+ if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
+ Abc_TtCopy( pBest, pCopy, nWords, 0 ), Config = 4;
+ // PXY
+ // 000
+ Abc_TtSwapAdjacent( pCopy, nWords, i );
+ assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
+ if ( Config == 0 )
+ return 0;
+ assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
+ Abc_TtCopy( pTruth, pBest, nWords, 0 );
+ return Config;
+ }
}
+/**Function*************************************************************
+ Synopsis [Smart evaluation.]
-void Abc_TtCofactorMinimize( word * pTruth, int nVars, int N )
-{
- char pCanonPerm[16];
- unsigned uCanonPhase;
- int i, fVerbose = 0;
- int nWords = Abc_TtWordNum( nVars );
+ Description []
+
+ SideEffects []
- if ( fVerbose )
- printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
+ SeeAlso []
- if ( fVerbose )
- printf( "Round 1\n" );
- for ( i = nVars - 2; i >= 0; i-- )
+***********************************************************************/
+int Abc_TtCofactorPermConfig( word * pTruth, int i, int nWords, int fSwapOnly, int fNaive )
+{
+ if ( nWords == 1 )
+ return Abc_Tt6CofactorPermNaive( pTruth, i, fSwapOnly );
+ if ( fNaive )
+ return Abc_TtCofactorPermNaive( pTruth, i, nWords, fSwapOnly );
+ if ( fSwapOnly )
{
- if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
+ if ( Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ) < 0 ) // Cof1 < Cof2
{
- if ( fVerbose )
- printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
+ Abc_TtSwapAdjacent( pTruth, nWords, i );
+ return 4;
}
+ return 0;
}
-
- if ( fVerbose )
- printf( "Round 2\n" );
- for ( i = 0; i < nVars - 1; i++ )
- {
- if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
+ {
+ int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0;
+ fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
+ fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
+ if ( fComp23 >= 0 ) // Cof2 >= Cof3
{
- if ( fVerbose )
- printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
+ if ( fComp01 >= 0 ) // Cof0 >= Cof1
+ {
+ fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
+ if ( fComp13 < 0 ) // Cof1 < Cof3
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
+ else if ( fComp13 == 0 ) // Cof1 == Cof3
+ {
+ fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
+ if ( fComp02 < 0 )
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
+ }
+ // else Cof1 > Cof3 -- do nothing
+ }
+ else // Cof0 < Cof1
+ {
+ fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
+ if ( fComp03 < 0 ) // Cof0 < Cof3
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+ }
+ else // Cof0 >= Cof3
+ {
+ if ( fComp23 == 0 ) // can flip Cof0 and Cof1
+ Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+ }
+ }
+ }
+ else // Cof2 < Cof3
+ {
+ if ( fComp01 >= 0 ) // Cof0 >= Cof1
+ {
+ fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
+ if ( fComp12 > 0 ) // Cof1 > Cof2
+ Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+ else if ( fComp12 == 0 ) // Cof1 == Cof2
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+ }
+ else // Cof1 < Cof2
+ {
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 2;
+ if ( fComp01 == 0 )
+ Abc_TtFlip( pTruth, nWords, i ), Config ^= 1;
+ }
+ }
+ else // Cof0 < Cof1
+ {
+ fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
+ if ( fComp02 == -1 ) // Cof0 < Cof2
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+ }
+ else if ( fComp02 == 0 ) // Cof0 == Cof2
+ {
+ fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
+ if ( fComp13 >= 0 ) // Cof1 >= Cof3
+ Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+ else // Cof1 < Cof3
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ Abc_TtFlip( pTruth, nWords, i + 1 ), Config = 3;
+ }
+ }
+ else // Cof0 > Cof2
+ Abc_TtFlip( pTruth, nWords, i ), Config = 1;
+ }
}
+ // perform final swap if needed
+ fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
+ if ( fComp12 < 0 ) // Cof1 < Cof2
+ Abc_TtSwapAdjacent( pTruth, nWords, i ), Config ^= 4;
+ return Config;
}
}
-
-
-void Abc_TtCofactorVerify( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
+int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char * pCanonPerm, unsigned * puCanonPhase, int fNaive )
{
- int i, k, nWords = Abc_TtWordNum( nVars );
- if ( (uCanonPhase >> nVars) & 1 )
- Abc_TtNot( pTruth, nWords );
- for ( i = 0; i < nVars; i++ )
- if ( (uCanonPhase >> i) & 1 )
- Abc_TtFlip( pTruth, nWords, i );
- for ( i = 0; i < nVars; i++ )
+ if ( fSwapOnly )
{
- for ( k = i; k < nVars; k++ )
- if ( pCanonPerm[k] == i )
- break;
- assert( k < nVars );
- if ( i == k )
- continue;
- Abc_TtSwapVars( pTruth, nVars, i, k );
- ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
+ int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 );
+ if ( Config )
+ {
+ if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
+ {
+ *puCanonPhase ^= (1 << i);
+ *puCanonPhase ^= (1 << (i+1));
+ }
+ ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
+ }
+ return Config;
+ }
+ {
+ static word pCopy1[1024];
+ int Config;
+ Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
+ Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 0, fNaive );
+ if ( Config == 0 )
+ return 0;
+ if ( Abc_TtCompareRev(pTruth, pCopy1, nWords) == 1 ) // made it worse
+ {
+ Abc_TtCopy( pTruth, pCopy1, nWords, 0 );
+ return 0;
+ }
+ // improved
+ if ( Config & 1 )
+ *puCanonPhase ^= (1 << i);
+ if ( Config & 2 )
+ *puCanonPhase ^= (1 << (i+1));
+ if ( Config & 4 )
+ {
+ if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
+ {
+ *puCanonPhase ^= (1 << i);
+ *puCanonPhase ^= (1 << (i+1));
+ }
+ ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
+ }
+ return Config;
}
}
-//#define CANON_VERIFY
+/**Function*************************************************************
+
+ Synopsis [Semi-canonical form computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
-void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
+***********************************************************************/
+//#define CANON_VERIFY
+unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm )
{
int pStoreIn[17];
- char pCanonPerm[16];
unsigned uCanonPhase;
- int i, nWords = Abc_TtWordNum( nVars );
+ int i, k, nWords = Abc_TtWordNum( nVars );
+ int fNaive = 1;
#ifdef CANON_VERIFY
char pCanonPermCopy[16];
@@ -795,31 +899,26 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
#endif
uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
-
- for ( i = nVars - 2; i >= 0; i-- )
- if ( pStoreIn[i] == pStoreIn[i+1] )
- Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
-
- for ( i = 1; i < nVars - 1; i++ )
- if ( pStoreIn[i] == pStoreIn[i+1] )
- Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
-
- for ( i = nVars - 3; i >= 0; i-- )
- if ( pStoreIn[i] == pStoreIn[i+1] )
- Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
-
- for ( i = 1; i < nVars - 1; i++ )
- if ( pStoreIn[i] == pStoreIn[i+1] )
- Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 );
-// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 );
+ for ( k = 0; k < 3; k++ )
+ {
+ int fChanges = 0;
+ for ( i = nVars - 2; i >= 0; i-- )
+ if ( pStoreIn[i] == pStoreIn[i+1] )
+ fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
+ if ( !fChanges )
+ break;
+ fChanges = 0;
+ for ( i = 1; i < nVars - 1; i++ )
+ if ( pStoreIn[i] == pStoreIn[i+1] )
+ fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
+ if ( !fChanges )
+ break;
+ }
#ifdef CANON_VERIFY
Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
- Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
+ Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
printf( "Canonical form verification failed!\n" );
#endif
@@ -831,6 +930,7 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
i = 0;
}
*/
+ return uCanonPhase;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 10:28:08 +0000