Skip to content

A
abc
Commit d56570f2 by Alan Mishchenko
Options

Improvements to the truth table computations.

parent ce3f8cb1
Showing with 889 additions and 1100 deletions
src/base/abci/abc.c
...@@ -4937,6 +4937,7 @@ usage: ...@@ -4937,6 +4937,7 @@ usage:
Abc_Print( -2, "\t 2: semi-canonical form by counting 1s in cofactors\n" ); 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 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 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-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-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" ); Abc_Print( -2, "\t-b : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );
......
src/base/abci/abcNpn.c
...@@ -23,6 +23,7 @@ ...@@ -23,6 +23,7 @@
#include "bool/kit/kit.h" #include "bool/kit/kit.h"
#include "bool/lucky/lucky.h" #include "bool/lucky/lucky.h"
#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -190,6 +191,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) ...@@ -190,6 +191,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
pAlgoName = "Jake's hybrid fast "; pAlgoName = "Jake's hybrid fast ";
else if ( NpnType == 4 ) else if ( NpnType == 4 )
pAlgoName = "Jake's hybrid good "; pAlgoName = "Jake's hybrid good ";
else if ( NpnType == 5 )
pAlgoName = "new hybrid fast ";
assert( p->nVars <= 16 ); assert( p->nVars <= 16 );
if ( pAlgoName ) if ( pAlgoName )
...@@ -202,10 +205,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) ...@@ -202,10 +205,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{ {
for ( i = 0; i < p->nFuncs; i++ ) for ( i = 0; i < p->nFuncs; i++ )
{ {
extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i );
if ( fVerbose ) if ( fVerbose )
printf( "%7d : ", i ); printf( "%7d : ", i );
Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i );
if ( fVerbose ) if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" ); 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 ) ...@@ -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" ); 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 ); else assert( 0 );
clk = clock() - clk; clk = clock() - clk;
printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) ); printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
...@@ -324,7 +336,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f ...@@ -324,7 +336,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
{ {
if ( fVerbose ) if ( fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName ); 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 ); Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
else else
printf( "Unknown canonical form value (%d).\n", NpnType ); printf( "Unknown canonical form value (%d).\n", NpnType );
......
src/misc/util/utilTruth.h
...@@ -61,6 +61,14 @@ static word s_CMasks6[5] = { ...@@ -61,6 +61,14 @@ static word s_CMasks6[5] = {
0x000000000000FFFF 0x000000000000FFFF
}; };
static word s_PMasks[5][3] = {
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
{ 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
{ 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
};
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -161,10 +169,9 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords ) ...@@ -161,10 +169,9 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
return 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Compares Cof0 and Cof1.] Synopsis []
Description [] Description []
...@@ -173,217 +180,42 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords ) ...@@ -173,217 +180,42 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
SeeAlso [] 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 ) 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); int w, shift = (1 << iVar);
for ( w = 0; w < nWords; w++ ) for ( w = 0; w < nWords; w++ )
{ pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
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 ) else // if ( iVar > 5 )
{ {
word * pLimit = pTruth + nWords; word * pLimit = pTruth + nWords;
int i, iStep = Abc_TtWordNum(iVar); int i, iStep = Abc_TtWordNum(iVar);
assert( nWords >= 2 );
for ( ; pTruth < pLimit; pTruth += 2*iStep ) for ( ; pTruth < pLimit; pTruth += 2*iStep )
for ( i = 0; i < iStep; i++ ) for ( i = 0; i < iStep; i++ )
if ( pTruth[i] != pTruth[i + iStep] ) pTruth[i + iStep] = pTruth[i];
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 ) static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
{ {
assert( Num1 < Num2 && Num2 < 4 );
if ( nWords == 1 ) 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); int w, shift = (1 << iVar);
for ( w = 0; w < nWords; w++ ) for ( w = 0; w < nWords; w++ )
{ pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
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 ) else // if ( iVar > 5 )
{ {
word * pLimit = pTruth + nWords; word * pLimit = pTruth + nWords;
int i, iStep = Abc_TtWordNum(iVar); int i, iStep = Abc_TtWordNum(iVar);
int Offset1 = Num1*iStep; for ( ; pTruth < pLimit; pTruth += 2*iStep )
int Offset2 = Num2*iStep;
assert( nWords >= 4 );
for ( ; pTruth < pLimit; pTruth += 4*iStep )
for ( i = 0; i < iStep; i++ ) for ( i = 0; i < iStep; i++ )
if ( pTruth[i + Offset1] != pTruth[i + Offset2] ) pTruth[i] = pTruth[i + iStep];
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;
} }
} }
...@@ -449,56 +281,6 @@ static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int ...@@ -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************************************************************* /**Function*************************************************************
...@@ -826,6 +608,10 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize ) ...@@ -826,6 +608,10 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
SeeAlso [] 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 ) static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
{ {
if ( nWords == 1 ) if ( nWords == 1 )
...@@ -857,9 +643,13 @@ static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar ) ...@@ -857,9 +643,13 @@ static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
SeeAlso [] 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 inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
{ {
static word PMasks[5][3] = { static word s_PMasks[5][3] = {
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
{ 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
{ 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
...@@ -870,7 +660,7 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar ) ...@@ -870,7 +660,7 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
{ {
int i, Shift = (1 << iVar); int i, Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ ) 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 ) else if ( iVar == 5 )
{ {
...@@ -888,10 +678,9 @@ static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar ) ...@@ -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] ); ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] );
} }
} }
static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ) 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 { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0
{ 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1 { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1
...@@ -940,18 +729,18 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ...@@ -940,18 +729,18 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
assert( iVar < jVar && jVar < nVars ); assert( iVar < jVar && jVar < nVars );
if ( nVars <= 6 ) if ( nVars <= 6 )
{ {
word * pMasks = PPMasks[iVar][jVar]; word * s_PMasks = Ps_PMasks[iVar][jVar];
int shift = (1 << jVar) - (1 << iVar); 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; return;
} }
if ( jVar <= 5 ) if ( jVar <= 5 )
{ {
word * pMasks = PPMasks[iVar][jVar]; word * s_PMasks = Ps_PMasks[iVar][jVar];
int nWords = Abc_TtWordNum(nVars); int nWords = Abc_TtWordNum(nVars);
int w, shift = (1 << jVar) - (1 << iVar); int w, shift = (1 << jVar) - (1 << iVar);
for ( w = 0; w < nWords; w++ ) 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; return;
} }
if ( iVar <= 5 && jVar > 5 ) if ( iVar <= 5 && jVar > 5 )
...@@ -984,6 +773,38 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ...@@ -984,6 +773,38 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
/**Function************************************************************* /**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 [] Synopsis []
Description [] Description []
...@@ -1024,220 +845,6 @@ static inline int Abc_TtCountOnes( word x ) ...@@ -1024,220 +845,6 @@ static inline int Abc_TtCountOnes( word x )
SeeAlso [] 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 ) static inline void Abc_TtReverseVars( word * pTruth, int nVars )
{ {
int k; int k;
......
src/opt/dau/dau.h 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/opt/dau/dauCanon.c
...@@ -30,10 +30,10 @@ ABC_NAMESPACE_IMPL_START ...@@ -30,10 +30,10 @@ ABC_NAMESPACE_IMPL_START
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [Generate reverse bytes.] Synopsis [Compares Cof0 and Cof1.]
Description [] Description []
...@@ -42,26 +42,80 @@ ABC_NAMESPACE_IMPL_START ...@@ -42,26 +42,80 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_TtReverseBypes() static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
{ {
int i, k; if ( nWords == 1 )
for ( i = 0; i < 256; i++ )
{ {
int Mask = 0; word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
for ( k = 0; k < 8; k++ ) word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
if ( (i >> k) & 1 ) if ( Cof0 != Cof1 )
Mask |= (1 << (7-k)); return Cof0 < Cof1 ? -1 : 1;
// printf( "%3d %3d\n", i, Mask ); return 0;
}
if ( i % 16 == 0 ) if ( iVar <= 5 )
printf( "\n" ); {
printf( "%-3d, ", Mask ); 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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Checks equality of pairs of cofactors w.r.t. adjacent variables.]
Description [] Description []
...@@ -70,722 +124,772 @@ void Abc_TtReverseBypes() ...@@ -70,722 +124,772 @@ void Abc_TtReverseBypes()
SeeAlso [] 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]; assert( Num1 < Num2 && Num2 < 4 );
int i, nWords = Abc_TtWordNum( nVars ); if ( nWords == 1 )
// int Counter = 0; return ((pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar]) == ((pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar]);
for ( i = 0; i < nVars-1; i++ ) 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 ); word * pLimit = pTruth + nWords;
Abc_TtCofactor0( Cof[0], nWords, i ); int i, iStep = Abc_TtWordNum(iVar);
Abc_TtCofactor0( Cof[0], nWords, i + 1 ); 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 ); /**Function*************************************************************
Abc_TtCofactor1( Cof[1], nWords, i );
Abc_TtCofactor0( Cof[1], nWords, i + 1 );
Abc_TtCopy( Cof[2], pTruth, nWords, 0 ); Synopsis [Compares pairs of cofactors w.r.t. adjacent variables.]
Abc_TtCofactor0( Cof[2], nWords, i );
Abc_TtCofactor1( Cof[2], nWords, i + 1 );
Abc_TtCopy( Cof[3], pTruth, nWords, 0 ); Description []
Abc_TtCofactor1( Cof[3], nWords, i );
Abc_TtCofactor1( Cof[3], nWords, i + 1 ); SideEffects []
if ( i == 5 && N == 4 ) SeeAlso []
{
printf( "\n" );
Abc_TtPrintHex( Cof[0], nVars );
Abc_TtPrintHex( Cof[1], nVars );
Abc_TtPrintHex( Cof[2], nVars );
Abc_TtPrintHex( Cof[3], nVars );
}
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) ); static inline int Abc_TtCompare2VarCofs( word * pTruth, int nWords, int iVar, int Num1, int Num2 )
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 )
{ {
// word Cof[4][1024]; assert( Num1 < Num2 && Num2 < 4 );
int i, j, nWords = Abc_TtWordNum( nVars ); if ( nWords == 1 )
int Counter = 0;
for ( i = 0; i < nVars-1; i++ )
for ( j = i+1; j < nVars; j++ )
{ {
/* word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
Abc_TtCofactor0( Cof[0], nWords, i ); if ( Cof1 != Cof2 )
Abc_TtCofactor0( Cof[0], nWords, j ); return Cof1 < Cof2 ? -1 : 1;
return 0;
Abc_TtCopy( Cof[1], pTruth, nWords, 0 ); }
Abc_TtCofactor1( Cof[1], nWords, i ); if ( iVar <= 4 )
Abc_TtCofactor0( Cof[1], nWords, j ); {
word Cof1, Cof2;
Abc_TtCopy( Cof[2], pTruth, nWords, 0 ); int w, shift = (1 << iVar);
Abc_TtCofactor0( Cof[2], nWords, i ); for ( w = 0; w < nWords; w++ )
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 )
{ {
printf( "\n" ); Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
Abc_TtPrintHexSpecial( Cof[0], nVars ); printf( "\n" ); Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
Abc_TtPrintHexSpecial( Cof[1], nVars ); printf( "\n" ); if ( Cof1 != Cof2 )
Abc_TtPrintHexSpecial( Cof[2], nVars ); printf( "\n" ); return Cof1 < Cof2 ? -1 : 1;
Abc_TtPrintHexSpecial( Cof[3], nVars ); printf( "\n" );
} }
*/ return 0;
/*
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);
*/
} }
} if ( iVar == 5 )
void Abc_TtCofactorTest3( word * pTruth, int nVars, int N ) {
{ unsigned * pTruthU = (unsigned *)pTruth;
word Cof[4][1024]; unsigned * pLimitU = (unsigned *)(pTruth + nWords);
int i, j, nWords = Abc_TtWordNum( nVars ); assert( nWords >= 2 );
for ( i = 0; i < nVars-1; i++ ) for ( ; pTruthU < pLimitU; pTruthU += 4 )
for ( j = i+1; j < nVars; j++ ) if ( pTruthU[Num1] != pTruthU[Num2] )
{ return pTruthU[Num1] < pTruthU[Num2] ? -1 : 1;
Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); return 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 )
{
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 )
void Abc_TtCofactorTest4( word * pTruth, int nVars, int N )
{ {
word Cof[4][1024]; assert( Num1 < Num2 && Num2 < 4 );
int i, j, nWords = Abc_TtWordNum( nVars ); if ( nWords == 1 )
int Sum = 0; {
for ( i = 0; i < nVars-1; i++ ) word Cof1 = (pTruth[0] >> (Num1 * (1 << iVar))) & s_CMasks6[iVar];
for ( j = i+1; j < nVars; j++ ) word Cof2 = (pTruth[0] >> (Num2 * (1 << iVar))) & s_CMasks6[iVar];
{ if ( Cof1 != Cof2 )
Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); return Cof1 < Cof2 ? -1 : 1;
Abc_TtCofactor0( Cof[0], nWords, i ); return 0;
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) );
} }
} if ( iVar <= 4 )
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-- )
{ {
/* word Cof1, Cof2;
Abc_TtCopy( Cof[0], pTruth, nWords, 0 ); int w, shift = (1 << iVar);
Abc_TtCofactor0( Cof[0], nWords, i ); for ( w = nWords - 1; w >= 0; w-- )
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 )
{ {
printf( "%d ", i ); Cof1 = (pTruth[w] >> Num1 * shift) & s_CMasks6[iVar];
Abc_TtFlip( pTruth, nWords, i ); Cof2 = (pTruth[w] >> Num2 * shift) & s_CMasks6[iVar];
Abc_TtPrintHex( pTruth, nVars ); if ( Cof1 != Cof2 )
// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); return Cof1 < Cof2 ? -1 : 1;
} }
return 0;
/*
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) );
*/
} }
i = 0; if ( iVar == 5 )
}
int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
{
static word pCopy[1024];
static word pBest[1024];
if ( fSwapOnly )
{ {
Abc_TtCopy( pCopy, pTruth, nWords, 0 ); unsigned * pTruthU = (unsigned *)pTruth;
Abc_TtSwapAdjacent( pCopy, nWords, i ); unsigned * pLimitU = (unsigned *)(pTruth + nWords);
if ( Abc_TtCompareRev(pTruth, pCopy, nWords) == 1 ) assert( nWords >= 2 );
{ for ( pLimitU -= 4; pLimitU >= pTruthU; pLimitU -= 4 )
Abc_TtCopy( pTruth, pCopy, nWords, 0 ); if ( pLimitU[Num1] != pLimitU[Num2] )
return 1; return pLimitU[Num1] < pLimitU[Num2] ? -1 : 1;
}
return 0; return 0;
} }
// if ( iVar > 5 )
// save two copies {
Abc_TtCopy( pCopy, pTruth, nWords, 0 ); word * pLimit = pTruth + nWords;
Abc_TtCopy( pBest, pTruth, nWords, 0 ); int i, iStep = Abc_TtWordNum(iVar);
int Offset1 = Num1*iStep;
// PXY int Offset2 = Num2*iStep;
// 001 assert( nWords >= 4 );
Abc_TtFlip( pCopy, nWords, i ); for ( pLimit -= 4*iStep; pLimit >= pTruth; pLimit -= 4*iStep )
if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) for ( i = iStep - 1; i >= 0; i-- )
Abc_TtCopy( pBest, pCopy, nWords, 0 ); if ( pLimit[i + Offset1] != pLimit[i + Offset2] )
return pLimit[i + Offset1] < pLimit[i + Offset2] ? -1 : 1;
// 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 ) )
return 0; 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 ) Synopsis [Minterm counting in all cofactors.]
{
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;
if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) ) Description []
{
*puCanonPhase ^= (1 << i); SideEffects []
*puCanonPhase ^= (1 << (i+1));
}
ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] ); SeeAlso []
}
return RetValue;
}
Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); ***********************************************************************/
static inline int Abc_TtCountOnesInTruth( word * pTruth, int nVars )
fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); {
fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 ); int nWords = Abc_TtWordNum( nVars );
if ( fComp23 >= 0 ) // Cof2 >= Cof3 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 for ( i = 0; i < nVars; i++ )
{ pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); return;
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;
}
}
}
} }
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 ); Counter = Abc_TtCountOnes( pTruth[k] );
if ( fComp12 > 0 ) // Cof1 > Cof2 for ( i = 6; i < nVars; i++ )
{ if ( (k & (1 << (i-6))) == 0 )
Abc_TtFlip( pTruth, nWords, i ); pStore[i] += Counter;
*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);
}
}
} }
else // Cof0 < Cof1 k++;
// count 1's for all other variables
if ( pTruth[k] )
{ {
fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); Counter = Abc_TtCountOnes( pTruth[k] );
if ( fComp02 == -1 ) // Cof0 < Cof2 for ( i = 6; i < nVars; i++ )
{ if ( (k & (1 << (i-6))) == 0 )
Abc_TtFlip( pTruth, nWords, i ); pStore[i] += Counter;
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);
}
} }
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) ) /**Function*************************************************************
{
*puCanonPhase ^= (1 << i);
*puCanonPhase ^= (1 << (i+1));
}
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 pStore[0] += bit_count[ pTruthC[k] & 0x55 ];
{ pStore[1] += bit_count[ pTruthC[k] & 0x33 ];
Abc_TtCopy( pTruth, pCopy1, nWords, 0 ); pStore[2] += bit_count[ pTruthC[k] & 0x0F ];
// undo the flips for ( i = 3; i < nVars; i++ )
*puCanonPhase = uPhaseInit; if ( (k & (1 << (i-3))) == 0 )
// undo the swap pStore[i] += bit_count[pTruthC[k]];
if ( fComp12 < 0 ) // Cof1 < Cof2
ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
RetValue = 0;
}
} }
return RetValue;
} }
/**Function*************************************************************
void Abc_TtCofactorTest__( word * pTruth, int nVars, int N ) Synopsis [Minterm counting in all cofactors.]
{
char pCanonPerm[16];
unsigned uCanonPhase;
static word pCopy1[1024];
static word pCopy2[1024];
int i, nWords = Abc_TtWordNum( nVars );
static int Counter = 0;
// pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2]; Description []
// nVars = 3;
SideEffects []
/* SeeAlso []
printf( "\n" );
Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
Abc_TtPrintBinary( pTruth, nVars );
printf( "\n" );
*/
// 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 )
{ {
/* int i;
word Cof0s = Abc_Tt6Cof0( pTruth[0], i+1 ); for ( i = 0; i <= iVar; i++ )
word Cof1s = Abc_Tt6Cof1( pTruth[0], i+1 ); pStore[i] += nBytes * 4;
return nBytes * 8;
word Cof0 = Abc_Tt6Cof0( Cof0s, i ); }
word Cof1 = Abc_Tt6Cof1( Cof0s, i ); if ( nBytes == 1 )
word Cof2 = Abc_Tt6Cof0( Cof1s, i ); {
word Cof3 = Abc_Tt6Cof1( Cof1s, i ); assert( iVar == 2 );
pStore[0] += bit_count[ Truth & 0x55 ];
Abc_TtPrintBinary( &Cof0, 6 ); pStore[1] += bit_count[ Truth & 0x33 ];
Abc_TtPrintBinary( &Cof1, 6 ); pStore[2] += bit_count[ Truth & 0x0F ];
Abc_TtPrintBinary( &Cof2, 6 ); return bit_count[ Truth & 0xFF ];
Abc_TtPrintBinary( &Cof3, 6 ); }
nMints0 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof0(Truth, iVar), iVar - 1, nBytes/2, pStore );
printf( "01 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 1) ); nMints1 = Abc_TtCountOnesInCofsFast6_rec( Abc_Tt6Cof1(Truth, iVar), iVar - 1, nBytes/2, pStore );
printf( "02 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 2) ); pStore[iVar] += nMints0;
printf( "03 = %d\n", Abc_TtCompare2VarCofsRev(pTruth, nWords, i, 0, 3) ); return nMints0 + nMints1;
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) ); int Abc_TtCountOnesInCofsFast_rec( word * pTruth, int iVar, int nWords, int * pStore )
{
if ( i == 0 && N == 74 ) 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; int i;
continue; 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 ) else
printf( "%d ", Counter ); {
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 ) Synopsis []
{
int fVerbose = 0;
int i;
int nWords = Abc_TtWordNum( nVars );
if ( fVerbose ) Description []
printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
SideEffects []
if ( fVerbose ) SeeAlso []
printf( "Round 1\n" );
for ( i = nVars - 2; i >= 0; i-- ) ***********************************************************************/
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 ) ) Abc_TtNot( pTruth, nWords );
{ nOnes = nWords*64 - nOnes;
if ( fVerbose ) uCanonPhase |= (1 << nVars);
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
}
} }
// normalize phase
if ( fVerbose ) Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
printf( "Round 2\n" ); pStore[nVars] = nOnes;
for ( i = 0; i < nVars - 1; i++ ) for ( i = 0; i < nVars; i++ )
{ {
if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) if ( pStore[i] >= nOnes - pStore[i] )
{ continue;
if ( fVerbose ) Abc_TtFlip( pTruth, nWords, i );
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); uCanonPhase |= (1 << i);
} pStore[i] = nOnes - pStore[i];
} }
// normalize permutation
return; if ( fOldSwap )
if ( fVerbose )
printf( "Round 3\n" );
for ( i = nVars - 2; i >= 0; i-- )
{ {
if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) int fChange;
{ do {
if ( fVerbose ) fChange = 0;
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); 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 );
} }
else
if ( fVerbose )
printf( "Round 4\n" );
for ( i = 0; i < nVars - 1; i++ )
{ {
if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) ) int k, BestK;
for ( i = 0; i < nVars - 1; i++ )
{ {
if ( fVerbose ) BestK = i + 1;
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); 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 ) void Abc_TtCofactorTest10( word * pTruth, int nVars, int N )
{ {
static word pCopy1[1024]; static word pCopy1[1024];
static word pCopy2[1024]; static word pCopy2[1024];
int nWords = Abc_TtWordNum( nVars ); int nWords = Abc_TtWordNum( nVars );
int i; int i;
for ( i = 0; i < nVars - 1; i++ ) for ( i = 0; i < nVars - 1; i++ )
{ {
// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
Abc_TtSwapAdjacent( pCopy1, nWords, i ); Abc_TtSwapAdjacent( pCopy1, nWords, i );
// Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); // Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
Abc_TtSwapVars( pCopy2, nVars, i, i+1 ); Abc_TtSwapVars( pCopy2, nVars, i, i+1 );
// Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
} }
} }
/**Function*************************************************************
void Abc_TtCofactorTest111( word * pTruth, int nVars, int N ) Synopsis [Naive evaluation.]
{
char pCanonPerm[32];
static word pCopy1[1024];
static word pCopy2[1024];
int nWords = Abc_TtWordNum( nVars );
// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); Description []
// Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm );
// Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" ); SideEffects []
Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); SeeAlso []
Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL );
// Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
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 ) Description []
{
char pCanonPerm[16]; SideEffects []
unsigned uCanonPhase;
int i, fVerbose = 0;
int nWords = Abc_TtWordNum( nVars );
if ( fVerbose ) SeeAlso []
printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
if ( fVerbose ) ***********************************************************************/
printf( "Round 1\n" ); int Abc_TtCofactorPermConfig( word * pTruth, int i, int nWords, int fSwapOnly, int fNaive )
for ( i = nVars - 2; i >= 0; i-- ) {
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 ) Abc_TtSwapAdjacent( pTruth, nWords, i );
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); return 4;
} }
return 0;
} }
{
if ( fVerbose ) int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23, Config = 0;
printf( "Round 2\n" ); fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
for ( i = 0; i < nVars - 1; i++ ) fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
{ if ( fComp23 >= 0 ) // Cof2 >= Cof3
if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
{ {
if ( fVerbose ) if ( fComp01 >= 0 ) // Cof0 >= Cof1
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); {
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;
} }
} }
int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, int fSwapOnly, char * pCanonPerm, unsigned * puCanonPhase, int fNaive )
void Abc_TtCofactorVerify( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
{ {
int i, k, nWords = Abc_TtWordNum( nVars ); if ( fSwapOnly )
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++ ) int Config = Abc_TtCofactorPermConfig( pTruth, i, nWords, 1, 0 );
if ( pCanonPerm[k] == i ) if ( Config )
break; {
assert( k < nVars ); if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
if ( i == k ) {
continue; *puCanonPhase ^= (1 << i);
Abc_TtSwapVars( pTruth, nVars, i, k ); *puCanonPhase ^= (1 << (i+1));
ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] ); }
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]; int pStoreIn[17];
char pCanonPerm[16];
unsigned uCanonPhase; unsigned uCanonPhase;
int i, nWords = Abc_TtWordNum( nVars ); int i, k, nWords = Abc_TtWordNum( nVars );
int fNaive = 1;
#ifdef CANON_VERIFY #ifdef CANON_VERIFY
char pCanonPermCopy[16]; char pCanonPermCopy[16];
...@@ -795,31 +899,26 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) ...@@ -795,31 +899,26 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
#endif #endif
uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn ); uCanonPhase = Abc_TtSemiCanonicize( pTruth, nVars, pCanonPerm, pStoreIn );
for ( k = 0; k < 3; k++ )
for ( i = nVars - 2; i >= 0; i-- ) {
if ( pStoreIn[i] == pStoreIn[i+1] ) int fChanges = 0;
Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); for ( i = nVars - 2; i >= 0; i-- )
// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); if ( pStoreIn[i] == pStoreIn[i+1] )
fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
for ( i = 1; i < nVars - 1; i++ ) if ( !fChanges )
if ( pStoreIn[i] == pStoreIn[i+1] ) break;
Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); fChanges = 0;
// Abc_TtCofactorPermNaive( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2 ); for ( i = 1; i < nVars - 1; i++ )
if ( pStoreIn[i] == pStoreIn[i+1] )
for ( i = nVars - 3; i >= 0; i-- ) fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStoreIn[i] != pStoreIn[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
if ( pStoreIn[i] == pStoreIn[i+1] ) if ( !fChanges )
Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, pStoreIn[i] != pStoreIn[nVars]/2 ); break;
// 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 );
#ifdef CANON_VERIFY #ifdef CANON_VERIFY
Abc_TtCopy( pCopy2, pTruth, nWords, 0 ); Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars ); memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase ); Abc_TtImplementNpnConfig( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) ) if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
printf( "Canonical form verification failed!\n" ); printf( "Canonical form verification failed!\n" );
#endif #endif
...@@ -831,6 +930,7 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N ) ...@@ -831,6 +930,7 @@ void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
i = 0; i = 0;
} }
*/ */
return uCanonPhase;
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment