Skip to content

A
abc
Commit ce3f8cb1 by Alan Mishchenko
Options

Improvements to the truth table computations.

parent 42e767c2
Showing with 451 additions and 126 deletions
lib/pthreadVC2.dll 0 → 100644
This diff was suppressed by a .gitattributes entry.
src/base/abci/abcNpn.c
...@@ -202,10 +202,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose ) ...@@ -202,10 +202,10 @@ 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_TtConfactorTest( word * pTruth, int nVars, int i ); extern void Abc_TtCofactorTest( word * pTruth, int nVars, int i );
if ( fVerbose ) if ( fVerbose )
printf( "%7d : ", i ); printf( "%7d : ", i );
Abc_TtConfactorTest( p->pFuncs[i], p->nVars, 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" );
} }
......
src/misc/util/utilTruth.h
...@@ -943,43 +943,43 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar ...@@ -943,43 +943,43 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
word * pMasks = PPMasks[iVar][jVar]; word * pMasks = PPMasks[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] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift);
return;
} }
else if ( jVar <= 5 )
{ {
if ( jVar <= 5 ) word * pMasks = PPMasks[iVar][jVar];
{ int nWords = Abc_TtWordNum(nVars);
word * pMasks = PPMasks[iVar][jVar]; int w, shift = (1 << jVar) - (1 << iVar);
int nWords = Abc_TtWordNum(nVars); for ( w = 0; w < nWords; w++ )
int w, shift = (1 << jVar) - (1 << iVar); pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
for ( w = 0; w < nWords; w++ ) return;
pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift); }
} if ( iVar <= 5 && jVar > 5 )
else if ( iVar <= 5 && jVar > 5 ) {
{ word low2High, high2Low;
word low2High, high2Low; word * pLimit = pTruth + Abc_TtWordNum(nVars);
word * pLimit = pTruth + Abc_TtWordNum(nVars); int j, jStep = Abc_TtWordNum(jVar);
int j, jStep = Abc_TtWordNum(jVar); int shift = 1 << iVar;
int shift = 1 << iVar; for ( ; pTruth < pLimit; pTruth += 2*jStep )
for ( ; pTruth < pLimit; pTruth += 2*jStep ) for ( j = 0; j < jStep; j++ )
for ( j = 0; j < jStep; j++ ) {
{ low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
low2High = (pTruth[j] & s_Truths6[iVar]) >> shift; high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar]; pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low; pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High; }
} return;
}
else
{
word * pLimit = pTruth + Abc_TtWordNum(nVars);
int i, iStep = Abc_TtWordNum(iVar);
int j, jStep = Abc_TtWordNum(jVar);
for ( ; pTruth < pLimit; pTruth += 2*jStep )
for ( i = 0; i < jStep; i += 2*iStep )
for ( j = 0; j < iStep; j++ )
ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
}
} }
{
word * pLimit = pTruth + Abc_TtWordNum(nVars);
int i, iStep = Abc_TtWordNum(iVar);
int j, jStep = Abc_TtWordNum(jVar);
for ( ; pTruth < pLimit; pTruth += 2*jStep )
for ( i = 0; i < jStep; i += 2*iStep )
for ( j = 0; j < iStep; j++ )
ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
return;
}
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1037,16 +1037,18 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore ...@@ -1037,16 +1037,18 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore
{ {
word Temp; word Temp;
int i, k, Counter, nWords; int i, k, Counter, nWords;
memset( pStore, 0, sizeof(int) * nVars );
if ( nVars <= 6 ) if ( nVars <= 6 )
{ {
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
if ( pTruth[0] & s_Truths6Neg[i] ) if ( pTruth[0] & s_Truths6Neg[i] )
pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] ); pStore[i] = Abc_TtCountOnes( pTruth[0] & s_Truths6Neg[i] );
else
pStore[i] = 0;
return; return;
} }
assert( nVars > 6 ); assert( nVars > 6 );
nWords = Abc_TtWordNum( nVars ); nWords = Abc_TtWordNum( nVars );
memset( pStore, 0, sizeof(int) * nVars );
for ( k = 0; k < nWords; k++ ) for ( k = 0; k < nWords; k++ )
{ {
// count 1's for the first six variables // count 1's for the first six variables
...@@ -1110,16 +1112,21 @@ static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pS ...@@ -1110,16 +1112,21 @@ static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pS
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm ) static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pCanonPerm, int * pStoreOut )
{ {
extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore ); extern int Abc_TtCountOnesInCofsFast( word * pTruth, int nVars, int * pStore );
int pStore[16]; int fOldSwap = 0;
// int pStore2[16]; int pStoreIn[17];
int * pStore = pStoreOut ? pStoreOut : pStoreIn;
// int pStore2[17];
int nWords = Abc_TtWordNum( nVars ); int nWords = Abc_TtWordNum( nVars );
int i, k, BestK, Temp, nOnes;//, nSwaps = 0;//, fChange; int i, Temp, nOnes;//, fChange;//, nSwaps = 0;//;
int k, BestK;
unsigned uCanonPhase = 0; unsigned uCanonPhase = 0;
assert( nVars <= 16 ); assert( nVars <= 16 );
for ( i = 0; i < nVars; i++ )
pCanonPerm[i] = i;
// normalize polarity // normalize polarity
nOnes = Abc_TtCountOnesInTruth( pTruth, nVars ); nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
if ( nOnes > nWords * 32 ) if ( nOnes > nWords * 32 )
...@@ -1130,6 +1137,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC ...@@ -1130,6 +1137,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
} }
// normalize phase // normalize phase
Abc_TtCountOnesInCofs( pTruth, nVars, pStore ); Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
pStore[nVars] = nOnes;
// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore ); // Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore );
// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 ); // Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 );
...@@ -1144,62 +1152,71 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC ...@@ -1144,62 +1152,71 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
uCanonPhase |= (1 << i); uCanonPhase |= (1 << i);
pStore[i] = nOnes - pStore[i]; pStore[i] = nOnes - pStore[i];
} }
/*
do { if ( fOldSwap )
fChange = 0; {
for ( i = 0; i < nVars-1; i++ ) int fChange;
{ do {
if ( pStore[i] <= pStore[i+1] ) fChange = 0;
continue; for ( i = 0; i < nVars-1; i++ )
{
// if ( pStore[i] <= pStore[i+1] )
if ( pStore[i] >= pStore[i+1] )
continue;
Temp = pCanonPerm[i]; Temp = pCanonPerm[i];
pCanonPerm[i] = pCanonPerm[i+1]; pCanonPerm[i] = pCanonPerm[i+1];
pCanonPerm[i+1] = Temp; pCanonPerm[i+1] = Temp;
Temp = pStore[i]; Temp = pStore[i];
pStore[i] = pStore[i+1]; pStore[i] = pStore[i+1];
pStore[i+1] = Temp; pStore[i+1] = Temp;
if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) ) if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
{ {
uCanonPhase ^= (1 << i); uCanonPhase ^= (1 << i);
uCanonPhase ^= (1 << (i+1)); uCanonPhase ^= (1 << (i+1));
}
Abc_TtSwapAdjacent( pTruth, nWords, i );
fChange = 1;
// nSwaps++;
} }
Abc_TtSwapAdjacent( pTruth, nWords, i ); } while ( fChange );
fChange = 1; }
// nSwaps++; else
}
} while ( fChange );
*/
for ( i = 0; i < nVars - 1; i++ )
{ {
BestK = i + 1; for ( i = 0; i < nVars - 1; i++ )
for ( k = i + 2; k < nVars; k++ ) {
if ( pStore[BestK] > pStore[k] ) BestK = i + 1;
BestK = k; for ( k = i + 2; k < nVars; k++ )
if ( pStore[BestK] >= pStore[i] ) // if ( pStore[BestK] > pStore[k] )
continue; if ( pStore[BestK] < pStore[k] )
BestK = k;
// if ( pStore[i] <= pStore[BestK] )
if ( pStore[i] >= pStore[BestK] )
continue;
Temp = pCanonPerm[i]; Temp = pCanonPerm[i];
pCanonPerm[i] = pCanonPerm[BestK]; pCanonPerm[i] = pCanonPerm[BestK];
pCanonPerm[BestK] = Temp; pCanonPerm[BestK] = Temp;
Temp = pStore[i]; Temp = pStore[i];
pStore[i] = pStore[BestK]; pStore[i] = pStore[BestK];
pStore[BestK] = Temp; pStore[BestK] = Temp;
if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) ) if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
{ {
uCanonPhase ^= (1 << i); uCanonPhase ^= (1 << i);
uCanonPhase ^= (1 << BestK); uCanonPhase ^= (1 << BestK);
}
Abc_TtSwapVars( pTruth, nVars, i, BestK );
// nSwaps++;
} }
Abc_TtSwapVars( pTruth, nVars, i, BestK );
// nSwaps++;
} }
/*
printf( "%d ", nSwaps );
// printf( "%d ", nSwaps );
/*
printf( "Minterms: " ); printf( "Minterms: " );
for ( i = 0; i < nVars; i++ ) for ( i = 0; i < nVars; i++ )
printf( "%d ", pStore[i] ); printf( "%d ", pStore[i] );
......
src/opt/dau/dauCanon.c
...@@ -70,7 +70,7 @@ void Abc_TtReverseBypes() ...@@ -70,7 +70,7 @@ void Abc_TtReverseBypes()
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_TtConfactorTest7( word * pTruth, int nVars, int N ) void Abc_TtCofactorTest7( word * pTruth, int nVars, int N )
{ {
word Cof[4][1024]; word Cof[4][1024];
int i, nWords = Abc_TtWordNum( nVars ); int i, nWords = Abc_TtWordNum( nVars );
...@@ -125,7 +125,7 @@ void Abc_TtConfactorTest7( word * pTruth, int nVars, int N ) ...@@ -125,7 +125,7 @@ void Abc_TtConfactorTest7( word * pTruth, int nVars, int N )
*/ */
} }
} }
void Abc_TtConfactorTest2( word * pTruth, int nVars, int N ) void Abc_TtCofactorTest2( word * pTruth, int nVars, int N )
{ {
// word Cof[4][1024]; // word Cof[4][1024];
int i, j, nWords = Abc_TtWordNum( nVars ); int i, j, nWords = Abc_TtWordNum( nVars );
...@@ -185,7 +185,7 @@ void Abc_TtConfactorTest2( word * pTruth, int nVars, int N ) ...@@ -185,7 +185,7 @@ void Abc_TtConfactorTest2( word * pTruth, int nVars, int N )
*/ */
} }
} }
void Abc_TtConfactorTest3( word * pTruth, int nVars, int N ) void Abc_TtCofactorTest3( word * pTruth, int nVars, int N )
{ {
word Cof[4][1024]; word Cof[4][1024];
int i, j, nWords = Abc_TtWordNum( nVars ); int i, j, nWords = Abc_TtWordNum( nVars );
...@@ -217,7 +217,7 @@ void Abc_TtConfactorTest3( word * pTruth, int nVars, int N ) ...@@ -217,7 +217,7 @@ void Abc_TtConfactorTest3( word * pTruth, int nVars, int N )
} }
} }
void Abc_TtConfactorTest4( word * pTruth, int nVars, int N ) void Abc_TtCofactorTest4( word * pTruth, int nVars, int N )
{ {
word Cof[4][1024]; word Cof[4][1024];
int i, j, nWords = Abc_TtWordNum( nVars ); int i, j, nWords = Abc_TtWordNum( nVars );
...@@ -259,7 +259,7 @@ void Abc_TtConfactorTest4( word * pTruth, int nVars, int N ) ...@@ -259,7 +259,7 @@ void Abc_TtConfactorTest4( word * pTruth, int nVars, int N )
} }
} }
void Abc_TtConfactorTest6( word * pTruth, int nVars, int N ) void Abc_TtCofactorTest6( word * pTruth, int nVars, int N )
{ {
// word Cof[4][1024]; // word Cof[4][1024];
int i, nWords = Abc_TtWordNum( nVars ); int i, nWords = Abc_TtWordNum( nVars );
...@@ -304,12 +304,22 @@ void Abc_TtConfactorTest6( word * pTruth, int nVars, int N ) ...@@ -304,12 +304,22 @@ void Abc_TtConfactorTest6( word * pTruth, int nVars, int N )
i = 0; i = 0;
} }
int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) int Abc_TtCofactorPermNaive( word * pTruth, int i, int nWords, int fSwapOnly )
{ {
static word pCopy[1024]; static word pCopy[1024];
static word pBest[1024]; static word pBest[1024];
int nWords = Abc_TtWordNum( nVars ); if ( fSwapOnly )
{
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;
}
return 0;
}
// save two copies // save two copies
Abc_TtCopy( pCopy, pTruth, nWords, 0 ); Abc_TtCopy( pCopy, pTruth, nWords, 0 );
...@@ -335,7 +345,7 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) ...@@ -335,7 +345,7 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars )
// PXY // PXY
// 110 // 110
Abc_TtSwapVars( pCopy, nVars, i, i+1 ); Abc_TtSwapAdjacent( pCopy, nWords, i );
if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
Abc_TtCopy( pBest, pCopy, nWords, 0 ); Abc_TtCopy( pBest, pCopy, nWords, 0 );
...@@ -359,76 +369,261 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars ) ...@@ -359,76 +369,261 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars )
// PXY // PXY
// 000 // 000
Abc_TtSwapVars( pCopy, nVars, i, i+1 ); Abc_TtSwapAdjacent( pCopy, nWords, i );
if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 ) if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
Abc_TtCopy( pBest, pCopy, nWords, 0 ); Abc_TtCopy( pBest, pCopy, nWords, 0 );
assert( Abc_TtEqual( pTruth, pCopy, nWords ) ); assert( Abc_TtEqual( pTruth, pCopy, nWords ) );
if ( Abc_TtEqual( pTruth, pBest, nWords ) ) if ( Abc_TtEqual( pTruth, pBest, nWords ) )
return 0; return 0;
assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
Abc_TtCopy( pTruth, pBest, nWords, 0 ); Abc_TtCopy( pTruth, pBest, nWords, 0 );
return 1; return 1;
} }
int Abc_TtConfactorPerm( word * pTruth, int i, int nVars ) int Abc_TtCofactorPerm( word * pTruth, int i, int nWords, char * pCanonPerm, unsigned * puCanonPhase, int fSwapOnly )
{ {
int nWords = Abc_TtWordNum( nVars ); static word pCopy1[1024];
int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23; int fComp01, fComp02, fComp03, fComp12, fComp13, fComp23;
unsigned uPhaseInit = *puCanonPhase;
int RetValue = 0; int RetValue = 0;
fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
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) )
{
*puCanonPhase ^= (1 << i);
*puCanonPhase ^= (1 << (i+1));
}
ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
}
return RetValue;
}
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 ); fComp01 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 1 );
if ( fComp23 >= 1 ) // Cof2 >= Cof3 fComp23 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 2, 3 );
if ( fComp23 >= 0 ) // Cof2 >= Cof3
{ {
if ( fComp01 >= 1 ) // Cof0 >= Cof1 if ( fComp01 >= 0 ) // Cof0 >= Cof1
{ {
fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 ); fComp13 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 3 );
if ( fComp13 < 1 ) // Cof1 < Cof3 ) if ( fComp13 < 0 ) // Cof1 < Cof3
Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; {
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 else // Cof0 < Cof1
{ {
fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 ); fComp03 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 3 );
if ( fComp03 < 1 ) // Cof0 < Cof3 ) if ( fComp03 < 0 ) // Cof0 < Cof3
{ {
Abc_TtFlip( pTruth, nWords, i ); Abc_TtFlip( pTruth, nWords, i );
Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; Abc_TtFlip( pTruth, nWords, i + 1 );
*puCanonPhase ^= (1 << i);
*puCanonPhase ^= (1 << (i+1));
RetValue = 1;
} }
else // Cof0 >= Cof3 else // Cof0 >= Cof3
{ {
if ( fComp23 == 0 ) if ( fComp23 == 0 ) // can flip Cof0 and Cof1
Abc_TtFlip( pTruth, nWords, i ), RetValue = 1; {
Abc_TtFlip( pTruth, nWords, i );
*puCanonPhase ^= (1 << i);
RetValue = 1;
}
} }
} }
} }
else // Cof2 < Cof3 else // Cof2 < Cof3
{ {
if ( fComp01 >= 1 ) // Cof0 >= Cof1 if ( fComp01 >= 0 ) // Cof0 >= Cof1
{ {
fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
if ( fComp12 < 1 ) // Cof1 < Cof2 ) if ( fComp12 > 0 ) // Cof1 > Cof2
Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1; {
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);
}
}
} }
else // Cof0 < Cof1 else // Cof0 < Cof1
{ {
fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 ); fComp02 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 0, 2 );
if ( fComp02 == -1 ) // Cof0 < Cof2 ) if ( fComp02 == -1 ) // Cof0 < Cof2
{
Abc_TtFlip( pTruth, nWords, i );
Abc_TtFlip( pTruth, nWords, i + 1 ); Abc_TtFlip( pTruth, nWords, i + 1 );
Abc_TtFlip( pTruth, nWords, i ), RetValue = 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 // perform final swap if needed
fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 ); fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
if ( fComp12 == 1 ) // Cof1 > Cof2 if ( fComp12 < 0 ) // Cof1 < Cof2
Abc_TtSwapVars( pTruth, nVars, i, i+1 ), RetValue = 1; {
Abc_TtSwapAdjacent( pTruth, nWords, i );
RetValue = 1;
if ( ((*puCanonPhase >> i) & 1) != ((*puCanonPhase >> (i+1)) & 1) )
{
*puCanonPhase ^= (1 << i);
*puCanonPhase ^= (1 << (i+1));
}
ABC_SWAP( int, pCanonPerm[i], pCanonPerm[i+1] );
}
if ( RetValue == 1 )
{
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;
}
}
return RetValue; return RetValue;
} }
void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
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;
// pTruth[0] = (s_Truths6[0] & s_Truths6[1]) | s_Truths6[2];
// nVars = 3;
/*
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++ )
{
/*
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 s = 0;
continue;
}
*/
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 );
}
void Abc_TtCofactorTest8( word * pTruth, int nVars, int N )
{ {
int fVerbose = 0; int fVerbose = 0;
int i; int i;
int nWords = Abc_TtWordNum( nVars );
if ( fVerbose ) if ( fVerbose )
printf( "\n " ), Abc_TtPrintHex( pTruth, nVars ); printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
...@@ -437,7 +632,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) ...@@ -437,7 +632,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 1\n" ); printf( "Round 1\n" );
for ( i = nVars - 2; i >= 0; i-- ) for ( i = nVars - 2; i >= 0; i-- )
{ {
if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
...@@ -448,7 +643,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) ...@@ -448,7 +643,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 2\n" ); printf( "Round 2\n" );
for ( i = 0; i < nVars - 1; i++ ) for ( i = 0; i < nVars - 1; i++ )
{ {
if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
...@@ -461,7 +656,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) ...@@ -461,7 +656,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 3\n" ); printf( "Round 3\n" );
for ( i = nVars - 2; i >= 0; i-- ) for ( i = nVars - 2; i >= 0; i-- )
{ {
if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
...@@ -472,7 +667,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) ...@@ -472,7 +667,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 4\n" ); printf( "Round 4\n" );
for ( i = 0; i < nVars - 1; i++ ) for ( i = 0; i < nVars - 1; i++ )
{ {
if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) ) if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars ); printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
...@@ -481,7 +676,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N ) ...@@ -481,7 +676,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
i = 0; i = 0;
} }
void Abc_TtConfactorTest10( 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];
...@@ -505,24 +700,137 @@ void Abc_TtConfactorTest10( word * pTruth, int nVars, int N ) ...@@ -505,24 +700,137 @@ void Abc_TtConfactorTest10( word * pTruth, int nVars, int N )
} }
void Abc_TtConfactorTest( word * pTruth, int nVars, int N ) void Abc_TtCofactorTest111( word * pTruth, int nVars, int N )
{ {
char pCanonPerm[32]; char pCanonPerm[32];
// 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 );
// Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" ); // Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
// Abc_TtCopy( pCopy1, pTruth, nWords, 0 ); Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
// Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm ); // Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm );
// 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_TtSemiCanonicize( pCopy2, nVars, pCanonPerm ); Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL );
// Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" ); // Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
// assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) ); assert( Abc_TtEqual( pCopy1, pCopy2, nWords ) );
}
void Abc_TtCofactorMinimize( word * pTruth, int nVars, int N )
{
char pCanonPerm[16];
unsigned uCanonPhase;
int i, fVerbose = 0;
int nWords = Abc_TtWordNum( nVars );
if ( fVerbose )
printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
if ( fVerbose )
printf( "Round 1\n" );
for ( i = nVars - 2; i >= 0; i-- )
{
if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
{
if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
}
}
if ( fVerbose )
printf( "Round 2\n" );
for ( i = 0; i < nVars - 1; i++ )
{
if ( Abc_TtCofactorPerm( pTruth, i, nWords, pCanonPerm, &uCanonPhase, 0 ) )
{
if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
}
}
}
void Abc_TtCofactorVerify( 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] );
}
}
//#define CANON_VERIFY
void Abc_TtCofactorTest( word * pTruth, int nVars, int N )
{
int pStoreIn[17];
char pCanonPerm[16];
unsigned uCanonPhase;
int i, nWords = Abc_TtWordNum( nVars );
#ifdef CANON_VERIFY
char pCanonPermCopy[16];
static word pCopy1[1024];
static word pCopy2[1024];
Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
#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 );
#ifdef CANON_VERIFY
Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
memcpy( pCanonPermCopy, pCanonPerm, sizeof(char) * nVars );
Abc_TtCofactorVerify( pCopy2, nVars, pCanonPermCopy, uCanonPhase );
if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
printf( "Canonical form verification failed!\n" );
#endif
/*
if ( !Abc_TtEqual( pCopy1, pCopy2, nWords ) )
{
Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
Kit_DsdPrintFromTruth( pCopy2, nVars ); printf( "\n" );
i = 0;
}
*/
} }
......
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