summaryrefslogtreecommitdiffstats
path: root/src/aig/kit/kitTruth.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/kit/kitTruth.c')
-rw-r--r--src/aig/kit/kitTruth.c403
1 files changed, 376 insertions, 27 deletions
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index 3f9188c7..56f10ac0 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -187,7 +190,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
Description [The input and output truth tables are in pIn/pOut. The current number
of variables is nVars. The total number of variables in nVarsAll. The last argument
- (Phase) contains shows what variables should remain.]
+ (Phase) shows what variables should remain.]
SideEffects [The input truth table is modified.]
@@ -229,7 +232,7 @@ void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
***********************************************************************/
void Kit_TruthPermute( unsigned * pOut, unsigned * pIn, int nVars, char * pPerm, int fReturnIn )
{
- int * pTemp;
+ unsigned * pTemp;
int i, Temp, fChange, Counter = 0;
do {
fChange = 0;
@@ -404,6 +407,57 @@ void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
/**Function*************************************************************
+ Synopsis [Computes negative cofactor of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthCofactor0Count( unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step, Counter = 0;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x55555555);
+ return Counter;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x33333333);
+ return Counter;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x0F0F0F0F);
+ return Counter;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x00FF00FF);
+ return Counter;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x0000FFFF);
+ return Counter;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i]);
+ pTruth += 2*Step;
+ }
+ return Counter;
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Computes positive cofactor of the function.]
Description []
@@ -598,7 +652,7 @@ int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int
return 1;
case 4:
for ( i = 0; i < nWords; i++ )
- if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
+ if ( ((pOnset[i] & (pOffset[i] >> 16)) | (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
return 0;
return 1;
default:
@@ -911,6 +965,77 @@ void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar
/**Function*************************************************************
+ Synopsis [Returns the number of minterms in the Boolean difference.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthBooleanDiffCount( unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step, Counter = 0;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 1)) & 0x55555555 );
+ return Counter;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 2)) & 0x33333333 );
+ return Counter;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 4)) & 0x0F0F0F0F );
+ return Counter;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 8)) & 0x00FF00FF );
+ return Counter;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >>16)) & 0x0000FFFF );
+ return Counter;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ Counter += Kit_WordCountOnes( pTruth[i] ^ pTruth[Step+i] );
+ pTruth += 2*Step;
+ }
+ return Counter;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of minterms in the Boolean difference.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthXorCount( unsigned * pTruth0, unsigned * pTruth1, int nVars )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, Counter = 0;
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( pTruth0[i] ^ pTruth1[i] );
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Universally quantifies the set of variables.]
Description []
@@ -1059,20 +1184,29 @@ void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1,
SeeAlso []
***********************************************************************/
-int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
+int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
{
- static unsigned uTemp0[16], uTemp1[16];
- assert( nVars <= 9 );
+ static unsigned uTemp0[32], uTemp1[32];
+ if ( pCof0 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof0 = uTemp0;
+ }
+ if ( pCof1 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof1 = uTemp1;
+ }
// compute Cof01
- Kit_TruthCopy( uTemp0, pTruth, nVars );
- Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
- Kit_TruthCofactor1( uTemp0, nVars, iVar1 );
+ Kit_TruthCopy( pCof0, pTruth, nVars );
+ Kit_TruthCofactor0( pCof0, nVars, iVar0 );
+ Kit_TruthCofactor1( pCof0, nVars, iVar1 );
// compute Cof10
- Kit_TruthCopy( uTemp1, pTruth, nVars );
- Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
- Kit_TruthCofactor0( uTemp1, nVars, iVar1 );
+ Kit_TruthCopy( pCof1, pTruth, nVars );
+ Kit_TruthCofactor1( pCof1, nVars, iVar0 );
+ Kit_TruthCofactor0( pCof1, nVars, iVar1 );
// compare
- return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
+ return Kit_TruthIsEqual( pCof0, pCof1, nVars );
}
/**Function*************************************************************
@@ -1086,20 +1220,29 @@ int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
SeeAlso []
***********************************************************************/
-int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
+int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
{
- static unsigned uTemp0[16], uTemp1[16];
- assert( nVars <= 9 );
+ static unsigned uTemp0[32], uTemp1[32];
+ if ( pCof0 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof0 = uTemp0;
+ }
+ if ( pCof1 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof1 = uTemp1;
+ }
// compute Cof00
- Kit_TruthCopy( uTemp0, pTruth, nVars );
- Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
- Kit_TruthCofactor0( uTemp0, nVars, iVar1 );
+ Kit_TruthCopy( pCof0, pTruth, nVars );
+ Kit_TruthCofactor0( pCof0, nVars, iVar0 );
+ Kit_TruthCofactor0( pCof0, nVars, iVar1 );
// compute Cof11
- Kit_TruthCopy( uTemp1, pTruth, nVars );
- Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
- Kit_TruthCofactor1( uTemp1, nVars, iVar1 );
+ Kit_TruthCopy( pCof1, pTruth, nVars );
+ Kit_TruthCofactor1( pCof1, nVars, iVar0 );
+ Kit_TruthCofactor1( pCof1, nVars, iVar1 );
// compare
- return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
+ return Kit_TruthIsEqual( pCof0, pCof1, nVars );
}
/**Function*************************************************************
@@ -1691,7 +1834,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
SeeAlso []
***********************************************************************/
-int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytes )
+int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytesInit )
{
// the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
static unsigned Table[256] = {
@@ -1730,6 +1873,7 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
};
unsigned uSum;
unsigned char * pTruthC, * pLimit;
+ int * pBytes = pBytesInit;
int i, iVar, Step, nWords, nBytes, nTotal;
assert( nVars <= 20 );
@@ -1768,11 +1912,14 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
for ( i = 0; i < nBytes; i += Step + Step )
{
- pRes[iVar] += pBytes[i];
- pBytes[i] += pBytes[i+Step];
+ pRes[iVar] += pBytesInit[i];
+ pBytesInit[i] += pBytesInit[i+Step];
}
- assert( pBytes[0] == nTotal );
+ assert( pBytesInit[0] == nTotal );
assert( iVar == nVars );
+
+ for ( i = 0; i < nVars; i++ )
+ assert( pRes[i] == Kit_TruthCofactor0Count(pTruth, nVars, i) );
return nTotal;
}
@@ -1866,8 +2013,210 @@ char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
}
+/**Function*************************************************************
+
+ Synopsis [Dumps truth table into a file.]
+
+ Description [Generates script file for reading into ABC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthPrintProfile_int( unsigned * pTruth, int nVars )
+{
+ int Mints[20];
+ int Mints0[20];
+ int Mints1[20];
+ int Unique1[20];
+ int Total2[20][20];
+ int Unique2[20][20];
+ int Common2[20][20];
+ int nWords = Kit_TruthWordNum( nVars );
+ int * pBytes = ABC_ALLOC( int, nWords * 4 );
+ unsigned * pIn = ABC_ALLOC( unsigned, nWords );
+ unsigned * pOut = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof00 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof01 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof10 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof11 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pTemp;
+ int nTotalMints, nTotalMints0, nTotalMints1;
+ int v, u, i, iVar, nMints1;
+ int Cof00, Cof01, Cof10, Cof11;
+ int Coz00, Coz01, Coz10, Coz11;
+ assert( nVars <= 20 );
+ assert( nVars >= 6 );
+
+ nTotalMints = Kit_TruthCountMinterms( pTruth, nVars, Mints, pBytes );
+ for ( v = 0; v < nVars; v++ )
+ Unique1[v] = Kit_TruthBooleanDiffCount( pTruth, nVars, v );
+
+ for ( v = 0; v < nVars; v++ )
+ for ( u = 0; u < nVars; u++ )
+ Total2[v][u] = Unique2[v][u] = Common2[v][u] = -1;
+
+ nMints1 = (1<<(nVars-2));
+ for ( v = 0; v < nVars; v++ )
+ {
+ // move this var to be the first
+ Kit_TruthCopy( pIn, pTruth, nVars );
+// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
+ for ( i = v; i < nVars - 1; i++ )
+ {
+ Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
+ pTemp = pIn; pIn = pOut; pOut = pTemp;
+ }
+// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
+// printf( "\n" );
+
+
+ // count minterms in both cofactor
+ nTotalMints0 = Kit_TruthCountMinterms( pIn, nVars-1, Mints0, pBytes );
+ nTotalMints1 = Kit_TruthCountMinterms( pIn+nWords/2, nVars-1, Mints1, pBytes );
+ assert( nTotalMints == nTotalMints0 + nTotalMints1 );
+/*
+ for ( u = 0; u < nVars-1; u++ )
+ printf( "%2d ", Mints0[u] );
+ printf( "\n" );
+
+ for ( u = 0; u < nVars-1; u++ )
+ printf( "%2d ", Mints1[u] );
+ printf( "\n" );
+*/
+ for ( u = 0; u < nVars-1; u++ )
+ {
+ if ( u < v )
+ iVar = u;
+ else
+ iVar = u + 1;
+ assert( v != iVar );
+ // get minter counts in the cofactors
+ Cof00 = Mints0[u]; Coz00 = nMints1 - Cof00;
+ Cof01 = nTotalMints0-Mints0[u]; Coz01 = nMints1 - Cof01;
+ Cof10 = Mints1[u]; Coz10 = nMints1 - Cof10;
+ Cof11 = nTotalMints1-Mints1[u]; Coz11 = nMints1 - Cof11;
+
+ assert( Cof00 >= 0 && Cof00 <= nMints1 );
+ assert( Cof01 >= 0 && Cof01 <= nMints1 );
+ assert( Cof10 >= 0 && Cof10 <= nMints1 );
+ assert( Cof11 >= 0 && Cof11 <= nMints1 );
+
+ assert( Coz00 >= 0 && Coz00 <= nMints1 );
+ assert( Coz01 >= 0 && Coz01 <= nMints1 );
+ assert( Coz10 >= 0 && Coz10 <= nMints1 );
+ assert( Coz11 >= 0 && Coz11 <= nMints1 );
+
+ Common2[v][iVar] = Common2[iVar][v] = Cof00 * Coz11 + Coz00 * Cof11 + Cof01 * Coz10 + Coz01 * Cof10;
+
+ Total2[v][iVar] = Total2[iVar][v] =
+ Cof00 * Coz01 + Coz00 * Cof01 +
+ Cof00 * Coz10 + Coz00 * Cof10 +
+ Cof00 * Coz11 + Coz00 * Cof11 +
+ Cof01 * Coz10 + Coz01 * Cof10 +
+ Cof01 * Coz11 + Coz01 * Cof11 +
+ Cof10 * Coz11 + Coz10 * Cof11 ;
+
+
+ Kit_TruthCofactor0New( pCof00, pIn, nVars-1, u );
+ Kit_TruthCofactor1New( pCof01, pIn, nVars-1, u );
+ Kit_TruthCofactor0New( pCof10, pIn+nWords/2, nVars-1, u );
+ Kit_TruthCofactor1New( pCof11, pIn+nWords/2, nVars-1, u );
+
+ Unique2[v][iVar] = Unique2[iVar][v] =
+ Kit_TruthXorCount( pCof00, pCof01, nVars-1 ) +
+ Kit_TruthXorCount( pCof00, pCof10, nVars-1 ) +
+ Kit_TruthXorCount( pCof00, pCof11, nVars-1 ) +
+ Kit_TruthXorCount( pCof01, pCof10, nVars-1 ) +
+ Kit_TruthXorCount( pCof01, pCof11, nVars-1 ) +
+ Kit_TruthXorCount( pCof10, pCof11, nVars-1 );
+ }
+ }
+
+ printf( "\n" );
+ printf( " V: " );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8c ", v+'a' );
+ printf( "\n" );
+
+ printf( " M: " );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Mints[v] );
+ printf( "\n" );
+
+ printf( " U: " );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Unique1[v] );
+ printf( "\n" );
+ printf( "\n" );
+
+ printf( "Unique:\n" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( " %2d ", i );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Unique2[i][v] );
+ printf( "\n" );
+ }
+
+ printf( "Common:\n" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( " %2d ", i );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Common2[i][v] );
+ printf( "\n" );
+ }
+
+ printf( "Total:\n" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( " %2d ", i );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Total2[i][v] );
+ printf( "\n" );
+ }
+
+ ABC_FREE( pIn );
+ ABC_FREE( pOut );
+ ABC_FREE( pCof00 );
+ ABC_FREE( pCof01 );
+ ABC_FREE( pCof10 );
+ ABC_FREE( pCof11 );
+ ABC_FREE( pBytes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dumps truth table into a file.]
+
+ Description [Generates script file for reading into ABC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthPrintProfile( unsigned * pTruth, int nVars )
+{
+ unsigned uTruth[2];
+ if ( nVars >= 6 )
+ {
+ Kit_TruthPrintProfile_int( pTruth, nVars );
+ return;
+ }
+ assert( nVars >= 2 );
+ uTruth[0] = pTruth[0];
+ uTruth[1] = pTruth[0];
+ Kit_TruthPrintProfile( uTruth, 6 );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 18:00:55 +0000