summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abcNpn.c4
-rw-r--r--src/misc/util/utilTruth.h185
-rw-r--r--src/opt/dau/dauCanon.c388
3 files changed, 451 insertions, 126 deletions
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 06732d2b..759d91b3 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -202,10 +202,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
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 )
printf( "%7d : ", i );
- Abc_TtConfactorTest( p->pFuncs[i], p->nVars, i );
+ Abc_TtCofactorTest( p->pFuncs[i], p->nVars, i );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
}
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 443ff061..236c0d62 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -943,43 +943,43 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
word * pMasks = PPMasks[iVar][jVar];
int shift = (1 << jVar) - (1 << iVar);
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);
- int w, shift = (1 << jVar) - (1 << iVar);
- for ( w = 0; w < nWords; w++ )
- pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
- }
- else if ( iVar <= 5 && jVar > 5 )
- {
- word low2High, high2Low;
- word * pLimit = pTruth + Abc_TtWordNum(nVars);
- int j, jStep = Abc_TtWordNum(jVar);
- int shift = 1 << iVar;
- for ( ; pTruth < pLimit; pTruth += 2*jStep )
- for ( j = 0; j < jStep; j++ )
- {
- low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
- high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
- pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
- pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
- }
- }
- 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 * pMasks = PPMasks[iVar][jVar];
+ int nWords = Abc_TtWordNum(nVars);
+ int w, shift = (1 << jVar) - (1 << iVar);
+ for ( w = 0; w < nWords; w++ )
+ pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
+ return;
+ }
+ if ( iVar <= 5 && jVar > 5 )
+ {
+ word low2High, high2Low;
+ word * pLimit = pTruth + Abc_TtWordNum(nVars);
+ int j, jStep = Abc_TtWordNum(jVar);
+ int shift = 1 << iVar;
+ for ( ; pTruth < pLimit; pTruth += 2*jStep )
+ for ( j = 0; j < jStep; j++ )
+ {
+ low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
+ high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
+ pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
+ pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
+ }
+ return;
}
+ {
+ 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*************************************************************
@@ -1037,16 +1037,18 @@ static inline void Abc_TtCountOnesInCofs( word * pTruth, int nVars, int * pStore
{
word Temp;
int i, k, Counter, nWords;
- memset( pStore, 0, sizeof(int) * nVars );
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
@@ -1110,16 +1112,21 @@ static inline void Abc_TtCountOnesInCofsSlow( word * pTruth, int nVars, int * pS
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 );
- int pStore[16];
-// int pStore2[16];
+ int fOldSwap = 0;
+ int pStoreIn[17];
+ int * pStore = pStoreOut ? pStoreOut : pStoreIn;
+// int pStore2[17];
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;
assert( nVars <= 16 );
+ for ( i = 0; i < nVars; i++ )
+ pCanonPerm[i] = i;
// normalize polarity
nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
if ( nOnes > nWords * 32 )
@@ -1130,6 +1137,7 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
}
// normalize phase
Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+ pStore[nVars] = nOnes;
// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore );
// Abc_TtCountOnesInCofsFast( pTruth, nVars, pStore2 );
@@ -1144,62 +1152,71 @@ static inline unsigned Abc_TtSemiCanonicize( word * pTruth, int nVars, char * pC
uCanonPhase |= (1 << i);
pStore[i] = nOnes - pStore[i];
}
-/*
- do {
- fChange = 0;
- for ( i = 0; i < nVars-1; i++ )
- {
- if ( pStore[i] <= pStore[i+1] )
- continue;
+
+ 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 = pCanonPerm[i];
+ pCanonPerm[i] = pCanonPerm[i+1];
+ pCanonPerm[i+1] = Temp;
- Temp = pStore[i];
- pStore[i] = pStore[i+1];
- pStore[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));
+ if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> (i+1)) & 1) )
+ {
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << (i+1));
+ }
+ Abc_TtSwapAdjacent( pTruth, nWords, i );
+ fChange = 1;
+ // nSwaps++;
}
- Abc_TtSwapAdjacent( pTruth, nWords, i );
- fChange = 1;
-// nSwaps++;
- }
- } while ( fChange );
-*/
-
- for ( i = 0; i < nVars - 1; i++ )
+ } while ( fChange );
+ }
+ else
{
- BestK = i + 1;
- for ( k = i + 2; k < nVars; k++ )
- if ( pStore[BestK] > pStore[k] )
- BestK = k;
- if ( pStore[BestK] >= pStore[i] )
- continue;
+ 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 = pCanonPerm[i];
+ pCanonPerm[i] = pCanonPerm[BestK];
+ pCanonPerm[BestK] = Temp;
- Temp = pStore[i];
- pStore[i] = pStore[BestK];
- pStore[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);
+ if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
+ {
+ uCanonPhase ^= (1 << i);
+ 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: " );
for ( i = 0; i < nVars; i++ )
printf( "%d ", pStore[i] );
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 3ad44715..b66b276b 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -70,7 +70,7 @@ void Abc_TtReverseBypes()
SeeAlso []
***********************************************************************/
-void Abc_TtConfactorTest7( word * pTruth, int nVars, int N )
+void Abc_TtCofactorTest7( word * pTruth, int nVars, int N )
{
word Cof[4][1024];
int i, nWords = Abc_TtWordNum( nVars );
@@ -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];
int i, j, nWords = Abc_TtWordNum( nVars );
@@ -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];
int i, j, nWords = Abc_TtWordNum( nVars );
@@ -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];
int i, j, nWords = Abc_TtWordNum( nVars );
@@ -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];
int i, nWords = Abc_TtWordNum( nVars );
@@ -304,12 +304,22 @@ void Abc_TtConfactorTest6( word * pTruth, int nVars, int N )
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 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
Abc_TtCopy( pCopy, pTruth, nWords, 0 );
@@ -335,7 +345,7 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars )
// PXY
// 110
- Abc_TtSwapVars( pCopy, nVars, i, i+1 );
+ Abc_TtSwapAdjacent( pCopy, nWords, i );
if ( Abc_TtCompareRev(pBest, pCopy, nWords) == 1 )
Abc_TtCopy( pBest, pCopy, nWords, 0 );
@@ -359,76 +369,261 @@ int Abc_TtConfactorPermNaive( word * pTruth, int i, int nVars )
// PXY
// 000
- Abc_TtSwapVars( pCopy, nVars, i, i+1 );
+ 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;
+ assert( Abc_TtCompareRev(pTruth, pBest, nWords) == 1 );
Abc_TtCopy( pTruth, pBest, nWords, 0 );
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;
+ unsigned uPhaseInit = *puCanonPhase;
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 );
- 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 );
- if ( fComp13 < 1 ) // Cof1 < Cof3 )
- Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1;
+ 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 < 1 ) // Cof0 < Cof3 )
+ if ( fComp03 < 0 ) // Cof0 < Cof3
{
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 )
- Abc_TtFlip( pTruth, nWords, i ), RetValue = 1;
+ if ( fComp23 == 0 ) // can flip Cof0 and Cof1
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ *puCanonPhase ^= (1 << i);
+ RetValue = 1;
+ }
}
}
}
else // Cof2 < Cof3
{
- if ( fComp01 >= 1 ) // Cof0 >= Cof1
+ if ( fComp01 >= 0 ) // Cof0 >= Cof1
{
fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
- if ( fComp12 < 1 ) // Cof1 < Cof2 )
- Abc_TtFlip( pTruth, nWords, i + 1 ), RetValue = 1;
+ if ( fComp12 > 0 ) // Cof1 > Cof2
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ *puCanonPhase ^= (1 << i);
+ }
+ else if ( fComp12 == 0 ) // Cof1 == Cof2
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ Abc_TtFlip( pTruth, nWords, i + 1 );
+ *puCanonPhase ^= (1 << i);
+ *puCanonPhase ^= (1 << (i+1));
+ }
+ else // Cof1 < Cof2
+ {
+ Abc_TtFlip( pTruth, nWords, i + 1 );
+ *puCanonPhase ^= (1 << (i+1));
+ if ( fComp01 == 0 )
+ {
+ Abc_TtFlip( pTruth, nWords, i );
+ *puCanonPhase ^= (1 << i);
+ }
+ }
}
else // Cof0 < Cof1
{
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 ), 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
fComp12 = Abc_TtCompare2VarCofsRev( pTruth, nWords, i, 1, 2 );
- if ( fComp12 == 1 ) // Cof1 > Cof2
- Abc_TtSwapVars( pTruth, nVars, i, i+1 ), RetValue = 1;
+ 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] );
+ }
+
+ 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;
}
-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 i;
+ int nWords = Abc_TtWordNum( nVars );
if ( fVerbose )
printf( "\n " ), Abc_TtPrintHex( pTruth, nVars );
@@ -437,7 +632,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 1\n" );
for ( i = nVars - 2; i >= 0; i-- )
{
- if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) )
+ if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{
if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
@@ -448,7 +643,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 2\n" );
for ( i = 0; i < nVars - 1; i++ )
{
- if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) )
+ if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{
if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
@@ -461,7 +656,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 3\n" );
for ( i = nVars - 2; i >= 0; i-- )
{
- if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) )
+ if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{
if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
@@ -472,7 +667,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
printf( "Round 4\n" );
for ( i = 0; i < nVars - 1; i++ )
{
- if ( Abc_TtConfactorPermNaive( pTruth, i, nVars ) )
+ if ( Abc_TtCofactorPermNaive( pTruth, i, nWords, 0 ) )
{
if ( fVerbose )
printf( "%d ", i ), Abc_TtPrintHex( pTruth, nVars );
@@ -481,7 +676,7 @@ void Abc_TtConfactorTest8( word * pTruth, int nVars, int N )
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 pCopy2[1024];
@@ -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];
-// static word pCopy1[1024];
+ 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 );
+ Abc_TtCopy( pCopy1, pTruth, nWords, 0 );
// Kit_TruthSemiCanonicize_Yasha( pCopy1, nVars, pCanonPerm );
// Kit_DsdPrintFromTruth( pCopy1, nVars ); printf( "\n" );
Abc_TtCopy( pCopy2, pTruth, nWords, 0 );
- Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm );
+ Abc_TtSemiCanonicize( pCopy2, nVars, pCanonPerm, NULL );
// 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;
+ }
+*/
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-09 19:35:19 +0000