mirror of https://github.com/YosysHQ/abc.git
Improvements to the NPN semi-canonical form computation package.
This commit is contained in:
parent
aed3b3a13a
commit
0a9236add5
|
|
@ -4866,17 +4866,18 @@ int Abc_CommandTestNpn( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
usage:
|
usage:
|
||||||
Abc_Print( -2, "usage: testnpn [-A <num>] [-vh] <file_name>\n" );
|
Abc_Print( -2, "usage: testnpn [-A <num>] [-vh] <file>\n" );
|
||||||
Abc_Print( -2, "\t testbench for computing semi-canonical forms of Boolean functions\n" );
|
Abc_Print( -2, "\t testbench for computing (semi-)canonical forms\n" );
|
||||||
|
Abc_Print( -2, "\t of completely-specified Boolean functions up to 16 varibles\n" );
|
||||||
Abc_Print( -2, "\t-A <num> : semi-caninical form computation algorithm [default = %d]\n", NpnType );
|
Abc_Print( -2, "\t-A <num> : semi-caninical form computation algorithm [default = %d]\n", NpnType );
|
||||||
Abc_Print( -2, "\t 0: none (reading and writing the file)\n" );
|
Abc_Print( -2, "\t 0: uniqifying truth tables\n" );
|
||||||
Abc_Print( -2, "\t 1: exact canonical form (works only for 6 variables)\n" );
|
Abc_Print( -2, "\t 1: exact NPN canonical form by brute-force enumeration\n" );
|
||||||
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: semi-canonical form by minimizing truth table value\n" );
|
Abc_Print( -2, "\t 3: Jake's hybrid semi-canonical form (fast)\n" );
|
||||||
Abc_Print( -2, "\t 4: hybrid semi-canonical form (works only for 6 variables)\n" );
|
Abc_Print( -2, "\t 4: Jake's hybrid semi-canonical form (high-effort)\n" );
|
||||||
Abc_Print( -2, "\t 5: Jake's hybrid semi-canonical form (works up to 16 variables)\n" );
|
|
||||||
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
|
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
|
||||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||||
|
Abc_Print( -2, "\t<file> : the text file with truth tables in hexadecimal, listed one per line\n");
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -55,6 +55,63 @@ extern void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p );
|
||||||
/// FUNCTION DEFINITIONS ///
|
/// FUNCTION DEFINITIONS ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Counts the number of unique truth tables.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
// returns hash key of the truth table
|
||||||
|
static inline int Abc_TruthHashKey( word * pFunc, int nWords, int nTableSize )
|
||||||
|
{
|
||||||
|
static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
|
||||||
|
int w;
|
||||||
|
word Key = 0;
|
||||||
|
for ( w = 0; w < nWords; w++ )
|
||||||
|
Key += pFunc[w] * s_BigPrimes[w % 7];
|
||||||
|
return (int)(Key % nTableSize);
|
||||||
|
}
|
||||||
|
// returns 1 if the entry with this truth table exits
|
||||||
|
static inline int Abc_TruthHashLookup( word ** pFuncs, int iThis, int nWords, int * pTable, int * pNexts, int Key )
|
||||||
|
{
|
||||||
|
int iThat;
|
||||||
|
for ( iThat = pTable[Key]; iThat != -1; iThat = pNexts[iThat] )
|
||||||
|
if ( !memcmp( pFuncs[iThat], pFuncs[iThis], sizeof(word) * nWords ) )
|
||||||
|
return 1;
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
// hashes truth tables and collects unique ones
|
||||||
|
int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
|
||||||
|
{
|
||||||
|
// allocate hash table
|
||||||
|
int nTableSize = Abc_PrimeCudd(p->nFuncs);
|
||||||
|
int * pTable = ABC_FALLOC( int, nTableSize );
|
||||||
|
int * pNexts = ABC_FALLOC( int, nTableSize );
|
||||||
|
// hash functions
|
||||||
|
int i, k, Key;
|
||||||
|
for ( i = 0; i < p->nFuncs; i++ )
|
||||||
|
{
|
||||||
|
Key = Abc_TruthHashKey( p->pFuncs[i], p->nWords, nTableSize );
|
||||||
|
if ( Abc_TruthHashLookup( p->pFuncs, i, p->nWords, pTable, pNexts, Key ) ) // found equal
|
||||||
|
p->pFuncs[i] = NULL;
|
||||||
|
else // there is no equal (the first time this one occurs so far)
|
||||||
|
pNexts[i] = pTable[Key], pTable[Key] = i;
|
||||||
|
}
|
||||||
|
ABC_FREE( pTable );
|
||||||
|
ABC_FREE( pNexts );
|
||||||
|
// count the number of unqiue functions
|
||||||
|
assert( p->pFuncs[0] != NULL );
|
||||||
|
for ( i = k = 1; i < p->nFuncs; i++ )
|
||||||
|
if ( p->pFuncs[i] != NULL )
|
||||||
|
p->pFuncs[k++] = p->pFuncs[i];
|
||||||
|
return (p->nFuncs = k);
|
||||||
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Counts the number of unique truth tables.]
|
Synopsis [Counts the number of unique truth tables.]
|
||||||
|
|
@ -68,7 +125,7 @@ extern void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p );
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
int nWords = 0; // unfortunate global variable
|
int nWords = 0; // unfortunate global variable
|
||||||
int Abc_TruthCompare( word ** p1, word ** p2 ) { return memcmp(*p1, *p2, sizeof(word) * nWords); }
|
int Abc_TruthCompare( word ** p1, word ** p2 ) { return memcmp(*p1, *p2, sizeof(word) * nWords); }
|
||||||
int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
|
int Abc_TruthNpnCountUniqueSort( Abc_TtStore_t * p )
|
||||||
{
|
{
|
||||||
int i, k;
|
int i, k;
|
||||||
// sort them by value
|
// sort them by value
|
||||||
|
|
@ -116,28 +173,27 @@ void Abc_TruthNpnPrint( char * pCanonPerm, unsigned uCanonPhase, int nVars )
|
||||||
void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
|
void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
|
||||||
{
|
{
|
||||||
unsigned pAux[2048];
|
unsigned pAux[2048];
|
||||||
char pCanonPerm[32];
|
word pAuxWord[1024], pAuxWord1[1024];
|
||||||
|
char pCanonPerm[16];
|
||||||
unsigned uCanonPhase=0;
|
unsigned uCanonPhase=0;
|
||||||
clock_t clk = clock();
|
clock_t clk = clock();
|
||||||
int i;
|
int i, maxCtr=0;
|
||||||
|
|
||||||
char * pAlgoName = NULL;
|
char * pAlgoName = NULL;
|
||||||
if ( NpnType == 0 )
|
if ( NpnType == 0 )
|
||||||
pAlgoName = "uniqifying ";
|
pAlgoName = "uniqifying ";
|
||||||
else if ( NpnType == 1 )
|
else if ( NpnType == 1 )
|
||||||
pAlgoName = "exact NPN ";
|
pAlgoName = "exact NPN ";
|
||||||
else if ( NpnType == 2 )
|
else if ( NpnType == 2 )
|
||||||
pAlgoName = "counting 1s ";
|
pAlgoName = "counting 1s ";
|
||||||
else if ( NpnType == 3 )
|
else if ( NpnType == 3 )
|
||||||
pAlgoName = "minimizing TT ";
|
pAlgoName = "Jake's hybrid fast ";
|
||||||
else if ( NpnType == 4 )
|
else if ( NpnType == 4 )
|
||||||
pAlgoName = "hybrid NPN ";
|
pAlgoName = "Jake's hybrid good ";
|
||||||
else if ( NpnType == 5 )
|
|
||||||
pAlgoName = "Jake's hybrid NPN";
|
|
||||||
|
|
||||||
assert( p->nVars <= 16 );
|
assert( p->nVars <= 16 );
|
||||||
if ( pAlgoName )
|
if ( pAlgoName )
|
||||||
printf( "Applying %-10s to %8d func%s of %2d vars... ",
|
printf( "Applying %-20s to %8d func%s of %2d vars... ",
|
||||||
pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars );
|
pAlgoName, p->nFuncs, (p->nFuncs == 1 ? "":"s"), p->nVars );
|
||||||
if ( fVerbose )
|
if ( fVerbose )
|
||||||
printf( "\n" );
|
printf( "\n" );
|
||||||
|
|
@ -154,23 +210,18 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
|
||||||
}
|
}
|
||||||
else if ( NpnType == 1 )
|
else if ( NpnType == 1 )
|
||||||
{
|
{
|
||||||
int * pComp = Extra_GreyCodeSchedule( p->nVars );
|
permInfo* pi;
|
||||||
int * pPerm = Extra_PermSchedule( p->nVars );
|
Abc_TruthNpnCountUnique(p);
|
||||||
if ( p->nVars == 6 )
|
pi = setPermInfoPtr(p->nVars);
|
||||||
|
for ( i = 0; i < p->nFuncs; i++ )
|
||||||
{
|
{
|
||||||
for ( i = 0; i < p->nFuncs; i++ )
|
if ( fVerbose )
|
||||||
{
|
printf( "%7d : ", i );
|
||||||
if ( fVerbose )
|
simpleMinimal(p->pFuncs[i], pAuxWord, pAuxWord1, pi, p->nVars);
|
||||||
printf( "%7d : ", i );
|
if ( fVerbose )
|
||||||
*((word *)p->pFuncs[i]) = Extra_Truth6MinimumExact( *((word *)p->pFuncs[i]), pComp, pPerm );
|
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
|
||||||
if ( fVerbose )
|
|
||||||
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
else
|
freePermInfoPtr(pi);
|
||||||
printf( "This feature only works for 6-variable functions.\n" );
|
|
||||||
ABC_FREE( pComp );
|
|
||||||
ABC_FREE( pPerm );
|
|
||||||
}
|
}
|
||||||
else if ( NpnType == 2 )
|
else if ( NpnType == 2 )
|
||||||
{
|
{
|
||||||
|
|
@ -191,43 +242,24 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
|
||||||
if ( fVerbose )
|
if ( fVerbose )
|
||||||
printf( "%7d : ", i );
|
printf( "%7d : ", i );
|
||||||
resetPCanonPermArray(pCanonPerm, p->nVars);
|
resetPCanonPermArray(pCanonPerm, p->nVars);
|
||||||
uCanonPhase = Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
|
uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
|
||||||
if ( fVerbose )
|
if ( 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 == 4 )
|
else if ( NpnType == 4 )
|
||||||
{
|
|
||||||
if ( p->nVars == 6 )
|
|
||||||
{
|
|
||||||
for ( i = 0; i < p->nFuncs; i++ )
|
|
||||||
{
|
|
||||||
if ( fVerbose )
|
|
||||||
printf( "%7d : ", i );
|
|
||||||
resetPCanonPermArray(pCanonPerm, p->nVars);
|
|
||||||
Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
|
|
||||||
*((word *)p->pFuncs[i]) = Extra_Truth6MinimumHeuristic( *((word *)p->pFuncs[i]) );
|
|
||||||
if ( fVerbose )
|
|
||||||
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
printf( "This feature only works for 6-variable functions.\n" );
|
|
||||||
}
|
|
||||||
else if ( NpnType == 5 )
|
|
||||||
{
|
{
|
||||||
for ( i = 0; i < p->nFuncs; i++ )
|
for ( i = 0; i < p->nFuncs; i++ )
|
||||||
{
|
{
|
||||||
if ( fVerbose )
|
if ( fVerbose )
|
||||||
printf( "%7d : ", i );
|
printf( "%7d : ", i );
|
||||||
resetPCanonPermArray(pCanonPerm, p->nVars);
|
resetPCanonPermArray(pCanonPerm, p->nVars);
|
||||||
uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
|
uCanonPhase = luckyCanonicizer_final_fast1( p->pFuncs[i], p->nVars, pCanonPerm );
|
||||||
if ( fVerbose )
|
if ( 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 assert( 0 );
|
else assert( 0 );
|
||||||
|
|
||||||
clk = clock() - clk;
|
clk = clock() - clk;
|
||||||
printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
|
printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
|
||||||
Abc_PrintTime( 1, "Time", clk );
|
Abc_PrintTime( 1, "Time", clk );
|
||||||
|
|
@ -284,7 +316,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int fVerbose )
|
||||||
{
|
{
|
||||||
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 <= 5 )
|
if ( NpnType >= 0 && NpnType <= 4 )
|
||||||
Abc_TruthNpnTest( pFileName, NpnType, fVerbose );
|
Abc_TruthNpnTest( pFileName, NpnType, fVerbose );
|
||||||
else
|
else
|
||||||
printf( "Unknown canonical form value (%d).\n", NpnType );
|
printf( "Unknown canonical form value (%d).\n", NpnType );
|
||||||
|
|
|
||||||
|
|
@ -20,9 +20,24 @@
|
||||||
|
|
||||||
ABC_NAMESPACE_HEADER_START
|
ABC_NAMESPACE_HEADER_START
|
||||||
|
|
||||||
|
typedef struct
|
||||||
|
{
|
||||||
|
int varN;
|
||||||
|
int* swapArray;
|
||||||
|
int swapCtr;
|
||||||
|
int totalSwaps;
|
||||||
|
int* flipArray;
|
||||||
|
int flipCtr;
|
||||||
|
int totalFlips;
|
||||||
|
}permInfo;
|
||||||
|
|
||||||
extern unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
|
extern unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
|
||||||
extern int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
|
extern unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
|
||||||
extern void resetPCanonPermArray(char* x, int nVars);
|
extern unsigned luckyCanonicizer_final_fast1( word * pInOut, int nVars, char * pCanonPerm );
|
||||||
|
extern void resetPCanonPermArray(char* x, int nVars);
|
||||||
|
extern permInfo* setPermInfoPtr(int var);
|
||||||
|
extern void freePermInfoPtr(permInfo* x);
|
||||||
|
extern void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars);
|
||||||
|
|
||||||
ABC_NAMESPACE_HEADER_END
|
ABC_NAMESPACE_HEADER_END
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -15,7 +15,7 @@
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
|
|
||||||
#include "luckyInt.h"
|
#include "luckyInt.h"
|
||||||
|
//#define LUCKY_VERIFY
|
||||||
|
|
||||||
ABC_NAMESPACE_IMPL_START
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
|
@ -27,6 +27,48 @@ static word SFmask[5][4] = {
|
||||||
{0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
|
{0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// we need next two functions only for verification of lucky method in debugging mode
|
||||||
|
void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
|
||||||
|
{
|
||||||
|
int Temp;
|
||||||
|
swap_ij(pAfter, nVars, iVarInPosition, jVar);
|
||||||
|
|
||||||
|
Temp = pCanonPerm[iVarInPosition];
|
||||||
|
pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
|
||||||
|
pCanonPerm[jVar] = Temp;
|
||||||
|
|
||||||
|
if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
|
||||||
|
{
|
||||||
|
*pUCanonPhase ^= (1 << iVarInPosition);
|
||||||
|
*pUCanonPhase ^= (1 << jVar);
|
||||||
|
}
|
||||||
|
if((*pUCanonPhase>>iVarInPosition) & 1)
|
||||||
|
Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
|
||||||
|
|
||||||
|
}
|
||||||
|
int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
|
||||||
|
{
|
||||||
|
int i,j;
|
||||||
|
char tempChar;
|
||||||
|
for(j=0;j<nVars;j++)
|
||||||
|
{
|
||||||
|
tempChar = 'a'+ j;
|
||||||
|
for(i=j;i<nVars;i++)
|
||||||
|
{
|
||||||
|
if(tempChar != pCanonPerm[i])
|
||||||
|
continue;
|
||||||
|
swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if((uCanonPhase>>nVars) & 1)
|
||||||
|
Kit_TruthNot_64bit(pAfter, nVars );
|
||||||
|
if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
|
||||||
|
return 0;
|
||||||
|
else
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
|
// there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
|
||||||
|
|
@ -203,6 +245,13 @@ inline void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, i
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inline void minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
int DifStart1;
|
||||||
|
if(minTemp1_fast(pInOut, iVar, nWords, &DifStart1) == 2)
|
||||||
|
arrangeQuoters_superFast_lessThen5(pInOut, DifStart1/100, 0, 2, 1, 3, iVar, nWords, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// It rearranges InOut (swaps and flips through rearrangement of quoters)
|
// It rearranges InOut (swaps and flips through rearrangement of quoters)
|
||||||
|
|
@ -362,6 +411,14 @@ inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inline void minimalSwapAndFlipIVar_superFast_iVar5_noEBFC(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
int DifStart1;
|
||||||
|
unsigned temp[2048];
|
||||||
|
if(minTemp1_fast_iVar5(pInOut, nWords, &DifStart1) == 2)
|
||||||
|
arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart1, 0, 2, 1, 3, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
|
|
||||||
////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// It rearranges InOut (swaps and flips through rearrangement of quoters)
|
// It rearranges InOut (swaps and flips through rearrangement of quoters)
|
||||||
|
|
@ -536,6 +593,14 @@ inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, i
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inline void minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
int DifStart1;
|
||||||
|
word temp[1024];
|
||||||
|
if(minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1) == 2)
|
||||||
|
arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart1, 0, 2, 1, 3, iVar, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
|
|
||||||
/////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
|
/////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
inline void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* pCanonPhase)
|
inline void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* pCanonPhase)
|
||||||
{
|
{
|
||||||
|
|
@ -587,38 +652,161 @@ inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWo
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
inline int minimalSwapAndFlipIVar_superFast_all_noEBFC(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
{
|
{
|
||||||
minimalInitialFlip_fast_16Vars(pInOut, nVars, pCanonPhase);
|
int i;
|
||||||
while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
|
word pDuplicate[1024];
|
||||||
continue;
|
int bitInfoTemp = pStore[0];
|
||||||
|
memcpy(pDuplicate,pInOut,nWords*sizeof(word));
|
||||||
|
for(i=0;i<5;i++)
|
||||||
|
{
|
||||||
|
if(bitInfoTemp == pStore[i+1])
|
||||||
|
minimalSwapAndFlipIVar_superFast_lessThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase);
|
||||||
|
else
|
||||||
|
{
|
||||||
|
bitInfoTemp = pStore[i+1];
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if(bitInfoTemp == pStore[i+1])
|
||||||
|
minimalSwapAndFlipIVar_superFast_iVar5_noEBFC((unsigned*) pInOut, nWords, pCanonPerm, pCanonPhase);
|
||||||
|
else
|
||||||
|
bitInfoTemp = pStore[i+1];
|
||||||
|
|
||||||
|
for(i=6;i<nVars-1;i++)
|
||||||
|
{
|
||||||
|
if(bitInfoTemp == pStore[i+1])
|
||||||
|
minimalSwapAndFlipIVar_superFast_moreThen5_noEBFC(pInOut, i, nWords, pCanonPerm, pCanonPhase);
|
||||||
|
else
|
||||||
|
{
|
||||||
|
bitInfoTemp = pStore[i+1];
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
|
||||||
|
return 0;
|
||||||
|
else
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// old version with out noEBFC
|
||||||
|
// inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
// {
|
||||||
|
// while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
|
||||||
|
// continue;
|
||||||
|
// }
|
||||||
|
|
||||||
|
inline void luckyCanonicizerS_F_first_16Vars1(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
if(((* pCanonPhase) >> (nVars+1)) & 1)
|
||||||
|
while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
|
||||||
|
continue;
|
||||||
|
else
|
||||||
|
while( minimalSwapAndFlipIVar_superFast_all_noEBFC(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
inline void luckyCanonicizerS_F_first_16Vars11(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
word duplicate[1024];
|
||||||
|
char pCanonPerm1[16];
|
||||||
|
unsigned uCanonPhase1;
|
||||||
|
|
||||||
|
if((* pCanonPhase) >> (nVars+2) )
|
||||||
|
{
|
||||||
|
memcpy(duplicate, pInOut, sizeof(word)*nWords);
|
||||||
|
Kit_TruthNot_64bit(duplicate, nVars);
|
||||||
|
uCanonPhase1 = *pCanonPhase;
|
||||||
|
uCanonPhase1 ^= (1 << nVars);
|
||||||
|
memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
|
||||||
|
luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
luckyCanonicizerS_F_first_16Vars1(duplicate, nVars, nWords, pStore, pCanonPerm1, &uCanonPhase1);
|
||||||
|
if(memCompare(pInOut, duplicate,nVars) == 1)
|
||||||
|
{
|
||||||
|
*pCanonPhase = uCanonPhase1;
|
||||||
|
memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
|
||||||
|
memcpy(pInOut, duplicate, sizeof(word)*nWords);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else
|
||||||
|
luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase);
|
||||||
}
|
}
|
||||||
|
|
||||||
inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
{
|
{
|
||||||
// word pDuplicate[1024]={0};
|
|
||||||
// word pDuplicateLocal[1024]={0};
|
|
||||||
// memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
|
|
||||||
|
|
||||||
assert( nVars > 6 && nVars <= 16 );
|
assert( nVars > 6 && nVars <= 16 );
|
||||||
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
|
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
|
||||||
luckyCanonicizerS_F_first_16Vars(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
|
luckyCanonicizerS_F_first_16Vars1(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
|
||||||
|
|
||||||
// memcpy(pDuplicate,pInOut,nWords*sizeof(word));
|
|
||||||
// assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
// top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
|
void bitReverceOrder(word* x, int nVars)
|
||||||
int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
|
|
||||||
{
|
{
|
||||||
|
int i;
|
||||||
|
for(i= nVars-1;i>=0;i--)
|
||||||
|
Kit_TruthChangePhase_64bit( x, nVars, i );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
inline void luckyCanonicizer_final_fast_16Vars1(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
assert( nVars > 6 && nVars <= 16 );
|
||||||
|
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
|
||||||
|
luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
|
||||||
|
bitReverceOrder(pInOut, nVars);
|
||||||
|
(*pCanonPhase) ^= (1<<nVars) -1;
|
||||||
|
luckyCanonicizerS_F_first_16Vars11(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// top-level procedure calling two special cases (nVars <= 6 and nVars <= 16)
|
||||||
|
unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
|
||||||
|
{
|
||||||
|
int nWords;
|
||||||
int pStore[16];
|
int pStore[16];
|
||||||
unsigned uCanonPhase = 0;
|
unsigned uCanonPhase = 0;
|
||||||
int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
|
#ifdef LUCKY_VERIFY
|
||||||
|
word temp[1024] = {0};
|
||||||
|
word duplicate[1024] = {0};
|
||||||
|
Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
|
||||||
|
#endif
|
||||||
if ( nVars <= 6 )
|
if ( nVars <= 6 )
|
||||||
pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );
|
pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
|
||||||
else if ( nVars <= 16 )
|
else if ( nVars <= 16 )
|
||||||
|
{
|
||||||
|
nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
|
||||||
luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
|
luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
|
||||||
|
}
|
||||||
else assert( 0 );
|
else assert( 0 );
|
||||||
|
#ifdef LUCKY_VERIFY
|
||||||
|
Kit_TruthCopy_64bit( temp, pInOut, nVars );
|
||||||
|
assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
|
||||||
|
#endif
|
||||||
|
return uCanonPhase;
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned luckyCanonicizer_final_fast1( word * pInOut, int nVars, char * pCanonPerm)
|
||||||
|
{
|
||||||
|
int nWords;
|
||||||
|
int pStore[16];
|
||||||
|
unsigned uCanonPhase = 0;
|
||||||
|
#ifdef LUCKY_VERIFY
|
||||||
|
word temp[1024] = {0};
|
||||||
|
word duplicate[1024] = {0};
|
||||||
|
Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
|
||||||
|
#endif
|
||||||
|
if ( nVars <= 6 )
|
||||||
|
pInOut[0] = luckyCanonicizer_final_fast_6Vars1( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
|
||||||
|
else if ( nVars <= 16 )
|
||||||
|
{
|
||||||
|
nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
|
||||||
|
luckyCanonicizer_final_fast_16Vars1( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
|
||||||
|
}
|
||||||
|
else assert( 0 );
|
||||||
|
#ifdef LUCKY_VERIFY
|
||||||
|
Kit_TruthCopy_64bit( temp, pInOut, nVars );
|
||||||
|
assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
|
||||||
|
#endif
|
||||||
return uCanonPhase;
|
return uCanonPhase;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -627,4 +815,3 @@ ABC_NAMESPACE_IMPL_END
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -34,47 +34,7 @@ inline void resetPCanonPermArray(char* x, int nVars)
|
||||||
x[i] = 'a'+i;
|
x[i] = 'a'+i;
|
||||||
}
|
}
|
||||||
|
|
||||||
// we need next two functions only for verification of lucky method in debugging mode
|
|
||||||
void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
|
|
||||||
{
|
|
||||||
int Temp;
|
|
||||||
swap_ij(pAfter, nVars, iVarInPosition, jVar);
|
|
||||||
|
|
||||||
Temp = pCanonPerm[iVarInPosition];
|
|
||||||
pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
|
|
||||||
pCanonPerm[jVar] = Temp;
|
|
||||||
|
|
||||||
if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
|
|
||||||
{
|
|
||||||
*pUCanonPhase ^= (1 << iVarInPosition);
|
|
||||||
*pUCanonPhase ^= (1 << jVar);
|
|
||||||
}
|
|
||||||
if((*pUCanonPhase>>iVarInPosition) & 1)
|
|
||||||
Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
|
|
||||||
|
|
||||||
}
|
|
||||||
int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
|
|
||||||
{
|
|
||||||
int i,j;
|
|
||||||
char tempChar;
|
|
||||||
for(j=0;j<nVars;j++)
|
|
||||||
{
|
|
||||||
tempChar = 'a'+ j;
|
|
||||||
for(i=j;i<nVars;i++)
|
|
||||||
{
|
|
||||||
if(tempChar != pCanonPerm[i])
|
|
||||||
continue;
|
|
||||||
swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if((uCanonPhase>>nVars) & 1)
|
|
||||||
Kit_TruthNot_64bit(pAfter, nVars );
|
|
||||||
if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
|
|
||||||
return 0;
|
|
||||||
else
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
inline word Abc_allFlip(word x, unsigned* pCanonPhase)
|
inline word Abc_allFlip(word x, unsigned* pCanonPhase)
|
||||||
{
|
{
|
||||||
|
|
@ -194,13 +154,29 @@ inline word Extra_Truth6MinimumRoundOne( word t, int iVar, char* pCanonPerm, uns
|
||||||
return tMin;
|
return tMin;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inline word Extra_Truth6MinimumRoundOne_noEBFC( word t, int iVar, char* pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
word tMin;
|
||||||
|
assert( iVar >= 0 && iVar < 5 );
|
||||||
|
|
||||||
|
tMin = Extra_Truth6SwapAdjacent( t, iVar ); // b a
|
||||||
|
if(t<tMin)
|
||||||
|
return t;
|
||||||
|
else
|
||||||
|
{
|
||||||
|
(* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, 4);
|
||||||
|
return tMin;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
// this function finds minimal for all TIED(and tied only) iVars
|
// this function finds minimal for all TIED(and tied only) iVars
|
||||||
//it finds tied vars based on rearranged Store info - group of tied vars has the same bit count in Store
|
//it finds tied vars based on rearranged Store info - group of tied vars has the same bit count in Store
|
||||||
inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
|
inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
|
||||||
{
|
{
|
||||||
int i, bitInfoTemp;
|
int i, bitInfoTemp;
|
||||||
word tMin0, tMin;
|
word tMin0, tMin=t;
|
||||||
tMin=Abc_allFlip(t, pCanonPhase);
|
|
||||||
do
|
do
|
||||||
{
|
{
|
||||||
bitInfoTemp = pStore[0];
|
bitInfoTemp = pStore[0];
|
||||||
|
|
@ -211,23 +187,99 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
|
||||||
tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
|
tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
|
||||||
else
|
else
|
||||||
bitInfoTemp = pStore[i+1];
|
bitInfoTemp = pStore[i+1];
|
||||||
}
|
}
|
||||||
|
|
||||||
}while ( tMin0 != tMin );
|
}while ( tMin0 != tMin );
|
||||||
return tMin;
|
return tMin;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inline word Extra_Truth6MinimumRoundMany_noEBFC( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
|
||||||
inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
|
|
||||||
{
|
{
|
||||||
// word temp, duplicat = InOut;
|
int i, bitInfoTemp;
|
||||||
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
|
word tMin0, tMin=t;
|
||||||
// InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
|
do
|
||||||
// temp = InOut;
|
{
|
||||||
// assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
|
bitInfoTemp = pStore[0];
|
||||||
// return(InOut);
|
tMin0 = tMin;
|
||||||
return Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPerm, pCanonPhase );
|
for ( i = 0; i < 5; i++ )
|
||||||
|
{
|
||||||
|
if(bitInfoTemp == pStore[i+1])
|
||||||
|
tMin = Extra_Truth6MinimumRoundOne_noEBFC( tMin, i, pCanonPerm, pCanonPhase );
|
||||||
|
else
|
||||||
|
bitInfoTemp = pStore[i+1];
|
||||||
|
}
|
||||||
|
}while ( tMin0 != tMin );
|
||||||
|
return tMin;
|
||||||
|
}
|
||||||
|
inline word Extra_Truth6MinimumRoundMany1( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
|
||||||
|
{
|
||||||
|
word tMin0, tMin=t;
|
||||||
|
char pCanonPerm1[16];
|
||||||
|
unsigned uCanonPhase1;
|
||||||
|
switch ((* pCanonPhase) >> 7)
|
||||||
|
{
|
||||||
|
case 0 :
|
||||||
|
{
|
||||||
|
|
||||||
|
return Extra_Truth6MinimumRoundMany_noEBFC( t, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
|
case 1 :
|
||||||
|
{
|
||||||
|
return Extra_Truth6MinimumRoundMany( t, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
|
case 2 :
|
||||||
|
{
|
||||||
|
uCanonPhase1 = *pCanonPhase;
|
||||||
|
uCanonPhase1 ^= (1 << 6);
|
||||||
|
memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
|
||||||
|
tMin0 = Extra_Truth6MinimumRoundMany_noEBFC( t, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
tMin = Extra_Truth6MinimumRoundMany_noEBFC( ~t, pStore, pCanonPerm1, &uCanonPhase1);
|
||||||
|
if(tMin0 <=tMin)
|
||||||
|
return tMin0;
|
||||||
|
else
|
||||||
|
{
|
||||||
|
*pCanonPhase = uCanonPhase1;
|
||||||
|
memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
|
||||||
|
return tMin;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
case 3 :
|
||||||
|
{
|
||||||
|
uCanonPhase1 = *pCanonPhase;
|
||||||
|
uCanonPhase1 ^= (1 << 6);
|
||||||
|
memcpy(pCanonPerm1,pCanonPerm,sizeof(char)*16);
|
||||||
|
tMin0 = Extra_Truth6MinimumRoundMany( t, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
tMin = Extra_Truth6MinimumRoundMany( ~t, pStore, pCanonPerm1, &uCanonPhase1);
|
||||||
|
if(tMin0 <=tMin)
|
||||||
|
return tMin0;
|
||||||
|
else
|
||||||
|
{
|
||||||
|
*pCanonPhase = uCanonPhase1;
|
||||||
|
memcpy(pCanonPerm,pCanonPerm1,sizeof(char)*16);
|
||||||
|
return tMin;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return Extra_Truth6MinimumRoundMany( t, pStore, pCanonPerm, pCanonPhase);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase)
|
||||||
|
{
|
||||||
|
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
|
||||||
|
return Extra_Truth6MinimumRoundMany1(InOut, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
|
inline word luckyCanonicizer_final_fast_6Vars1(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
|
||||||
|
{
|
||||||
|
(* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
|
||||||
|
InOut = Extra_Truth6MinimumRoundMany1(InOut, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
Kit_TruthChangePhase_64bit( &InOut, 6, 5 );
|
||||||
|
Kit_TruthChangePhase_64bit( &InOut, 6, 4 );
|
||||||
|
Kit_TruthChangePhase_64bit( &InOut, 6, 3 );
|
||||||
|
Kit_TruthChangePhase_64bit( &InOut, 6, 2 );
|
||||||
|
Kit_TruthChangePhase_64bit( &InOut, 6, 1 );
|
||||||
|
Kit_TruthChangePhase_64bit( &InOut, 6, 0 );
|
||||||
|
(*pCanonPhase) ^= 0x3F;
|
||||||
|
return Extra_Truth6MinimumRoundMany1(InOut, pStore, pCanonPerm, pCanonPhase);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
ABC_NAMESPACE_IMPL_END
|
ABC_NAMESPACE_IMPL_END
|
||||||
|
|
|
||||||
|
|
@ -41,6 +41,7 @@ typedef unsigned __int64 word;
|
||||||
#define true 1
|
#define true 1
|
||||||
#define inline __inline // compatible with MS VS 6.0
|
#define inline __inline // compatible with MS VS 6.0
|
||||||
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
|
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
|
||||||
|
// #define LUCKY_VERIFY
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -118,9 +119,9 @@ extern permInfo* setPermInfoPtr(int var);
|
||||||
extern void freePermInfoPtr(permInfo* x);
|
extern void freePermInfoPtr(permInfo* x);
|
||||||
extern inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
|
extern inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
|
||||||
extern inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
|
extern inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
|
||||||
extern inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore );
|
extern inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore);
|
||||||
extern inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase );
|
extern inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
|
||||||
extern inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase);
|
extern inline word luckyCanonicizer_final_fast_6Vars1(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
|
||||||
extern inline void resetPCanonPermArray_6Vars(char* x);
|
extern inline void resetPCanonPermArray_6Vars(char* x);
|
||||||
extern void swap_ij( word* f,int totalVars, int varI, int varJ);
|
extern void swap_ij( word* f,int totalVars, int varI, int varJ);
|
||||||
extern inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
|
extern inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,183 @@
|
||||||
|
/**CFile****************************************************************
|
||||||
|
|
||||||
|
FileName [luckySimple.c]
|
||||||
|
|
||||||
|
SystemName [ABC: Logic synthesis and verification system.]
|
||||||
|
|
||||||
|
PackageName [Semi-canonical form computation package.]
|
||||||
|
|
||||||
|
Synopsis [Truth table minimization procedures.]
|
||||||
|
|
||||||
|
Author [Jake]
|
||||||
|
|
||||||
|
Date [Started - August 2012]
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include "luckyInt.h"
|
||||||
|
|
||||||
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
static swapInfo* setSwapInfoPtr(int varsN)
|
||||||
|
{
|
||||||
|
int i;
|
||||||
|
swapInfo* x = (swapInfo*) malloc(sizeof(swapInfo));
|
||||||
|
x->posArray = (varInfo*) malloc (sizeof(varInfo)*(varsN+2));
|
||||||
|
x->realArray = (int*) malloc (sizeof(int)*(varsN+2));
|
||||||
|
x->varN = varsN;
|
||||||
|
x->realArray[0]=varsN+100;
|
||||||
|
for(i=1;i<=varsN;i++)
|
||||||
|
{
|
||||||
|
x->posArray[i].position=i;
|
||||||
|
x->posArray[i].direction=-1;
|
||||||
|
x->realArray[i]=i;
|
||||||
|
}
|
||||||
|
x->realArray[varsN+1]=varsN+10;
|
||||||
|
return x;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
static void freeSwapInfoPtr(swapInfo* x)
|
||||||
|
{
|
||||||
|
free(x->posArray);
|
||||||
|
free(x->realArray);
|
||||||
|
free(x);
|
||||||
|
}
|
||||||
|
|
||||||
|
int nextSwap(swapInfo* x)
|
||||||
|
{
|
||||||
|
int i,j,temp;
|
||||||
|
for(i=x->varN;i>1;i--)
|
||||||
|
{
|
||||||
|
if( i > x->realArray[x->posArray[i].position + x->posArray[i].direction] )
|
||||||
|
{
|
||||||
|
x->posArray[i].position = x->posArray[i].position + x->posArray[i].direction;
|
||||||
|
temp = x->realArray[x->posArray[i].position];
|
||||||
|
x->realArray[x->posArray[i].position] = i;
|
||||||
|
x->realArray[x->posArray[i].position - x->posArray[i].direction] = temp;
|
||||||
|
x->posArray[temp].position = x->posArray[i].position - x->posArray[i].direction;
|
||||||
|
for(j=x->varN;j>i;j--)
|
||||||
|
{
|
||||||
|
x->posArray[j].direction = x->posArray[j].direction * -1;
|
||||||
|
}
|
||||||
|
x->positionToSwap1 = x->posArray[temp].position - 1;
|
||||||
|
x->positionToSwap2 = x->posArray[i].position - 1;
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
void fillInSwapArray(permInfo* pi)
|
||||||
|
{
|
||||||
|
int counter=pi->totalSwaps-1;
|
||||||
|
swapInfo* x= setSwapInfoPtr(pi->varN);
|
||||||
|
while(nextSwap(x)==1)
|
||||||
|
{
|
||||||
|
if(x->positionToSwap1<x->positionToSwap2)
|
||||||
|
pi->swapArray[counter--]=x->positionToSwap1;
|
||||||
|
else
|
||||||
|
pi->swapArray[counter--]=x->positionToSwap2;
|
||||||
|
}
|
||||||
|
|
||||||
|
freeSwapInfoPtr(x);
|
||||||
|
}
|
||||||
|
int oneBitPosition(int x, int size)
|
||||||
|
{
|
||||||
|
int i;
|
||||||
|
for(i=0;i<size;i++)
|
||||||
|
if((x>>i)&1 == 1)
|
||||||
|
return i;
|
||||||
|
return -1;
|
||||||
|
}
|
||||||
|
void fillInFlipArray(permInfo* pi)
|
||||||
|
{
|
||||||
|
int i, temp=0, grayNumber;
|
||||||
|
for(i=1;i<=pi->totalFlips;i++)
|
||||||
|
{
|
||||||
|
grayNumber = i^(i>>1);
|
||||||
|
pi->flipArray[pi->totalFlips-i]=oneBitPosition(temp^grayNumber, pi->varN);
|
||||||
|
temp = grayNumber;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
inline int factorial(int n)
|
||||||
|
{
|
||||||
|
return (n == 1 || n == 0) ? 1 : factorial(n - 1) * n;
|
||||||
|
}
|
||||||
|
permInfo* setPermInfoPtr(int var)
|
||||||
|
{
|
||||||
|
permInfo* x;
|
||||||
|
x = (permInfo*) malloc(sizeof(permInfo));
|
||||||
|
x->flipCtr=0;
|
||||||
|
x->varN = var;
|
||||||
|
x->totalFlips=(1<<var)-1;
|
||||||
|
x->swapCtr=0;
|
||||||
|
x->totalSwaps=factorial(var)-1;
|
||||||
|
x->flipArray = (int*) malloc(sizeof(int)*x->totalFlips);
|
||||||
|
x->swapArray = (int*) malloc(sizeof(int)*x->totalSwaps);
|
||||||
|
fillInSwapArray(x);
|
||||||
|
fillInFlipArray(x);
|
||||||
|
return x;
|
||||||
|
}
|
||||||
|
|
||||||
|
void freePermInfoPtr(permInfo* x)
|
||||||
|
{
|
||||||
|
free(x->flipArray);
|
||||||
|
free(x->swapArray);
|
||||||
|
free(x);
|
||||||
|
}
|
||||||
|
inline void minWord(word* a, word* b, word* minimal, int nVars)
|
||||||
|
{
|
||||||
|
if(memCompare(a, b, nVars) == -1)
|
||||||
|
Kit_TruthCopy_64bit( minimal, a, nVars );
|
||||||
|
else
|
||||||
|
Kit_TruthCopy_64bit( minimal, b, nVars );
|
||||||
|
}
|
||||||
|
inline void minWord3(word* a, word* b, word* minimal, int nVars)
|
||||||
|
{
|
||||||
|
if (memCompare(a, b, nVars) <= 0)
|
||||||
|
{
|
||||||
|
if (memCompare(a, minimal, nVars) < 0)
|
||||||
|
Kit_TruthCopy_64bit( minimal, a, nVars );
|
||||||
|
else
|
||||||
|
return ;
|
||||||
|
}
|
||||||
|
if (memCompare(b, minimal, nVars) <= 0)
|
||||||
|
Kit_TruthCopy_64bit( minimal, b, nVars );
|
||||||
|
}
|
||||||
|
void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
|
||||||
|
{
|
||||||
|
int i,j=0;
|
||||||
|
Kit_TruthCopy_64bit( pAux, x, nVars );
|
||||||
|
Kit_TruthNot_64bit( x, nVars );
|
||||||
|
|
||||||
|
minWord(x, pAux, minimal, nVars);
|
||||||
|
|
||||||
|
for(i=pi->totalSwaps-1;i>=0;i--)
|
||||||
|
{
|
||||||
|
Kit_TruthSwapAdjacentVars_64bit(x, nVars, pi->swapArray[i]);
|
||||||
|
Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, pi->swapArray[i]);
|
||||||
|
minWord3(x, pAux, minimal, nVars);
|
||||||
|
}
|
||||||
|
for(j=pi->totalFlips-1;j>=0;j--)
|
||||||
|
{
|
||||||
|
Kit_TruthSwapAdjacentVars_64bit(x, nVars, 0);
|
||||||
|
Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, 0);
|
||||||
|
Kit_TruthChangePhase_64bit(x, nVars, pi->flipArray[j]);
|
||||||
|
Kit_TruthChangePhase_64bit(pAux, nVars, pi->flipArray[j]);
|
||||||
|
minWord3(x, pAux, minimal, nVars);
|
||||||
|
for(i=pi->totalSwaps-1;i>=0;i--)
|
||||||
|
{
|
||||||
|
Kit_TruthSwapAdjacentVars_64bit(x, nVars, pi->swapArray[i]);
|
||||||
|
Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, pi->swapArray[i]);
|
||||||
|
minWord3(x, pAux, minimal, nVars);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Kit_TruthCopy_64bit( x, minimal, nVars );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
ABC_NAMESPACE_IMPL_END
|
||||||
|
|
@ -241,6 +241,7 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
|
||||||
} while ( fChange );
|
} while ( fChange );
|
||||||
return uCanonPhase;
|
return uCanonPhase;
|
||||||
}
|
}
|
||||||
|
|
||||||
inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
|
inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
|
||||||
{
|
{
|
||||||
int nWords = Kit_TruthWordNum_64bit( nVars );
|
int nWords = Kit_TruthWordNum_64bit( nVars );
|
||||||
|
|
@ -250,8 +251,8 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
|
||||||
assert( nVars <= 16 );
|
assert( nVars <= 16 );
|
||||||
|
|
||||||
nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
|
nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
|
||||||
// if ( (nOnes == nWords * 32) )
|
if ( nOnes == nWords * 32 )
|
||||||
// return 999999;
|
uCanonPhase |= (1 << (nVars+2));
|
||||||
|
|
||||||
if ( (nOnes > nWords * 32) )
|
if ( (nOnes > nWords * 32) )
|
||||||
{
|
{
|
||||||
|
|
@ -266,9 +267,12 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
|
||||||
// canonicize phase
|
// canonicize phase
|
||||||
for ( i = 0; i < nVars; i++ )
|
for ( i = 0; i < nVars; i++ )
|
||||||
{
|
{
|
||||||
// if ( pStore[i] == nOnes-pStore[i])
|
if ( 2*pStore[i] == nOnes)
|
||||||
// return 999999;
|
{
|
||||||
if ( pStore[i] >= nOnes-pStore[i])
|
uCanonPhase |= (1 << (nVars+1));
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
if ( pStore[i] > nOnes-pStore[i])
|
||||||
continue;
|
continue;
|
||||||
uCanonPhase |= (1 << i);
|
uCanonPhase |= (1 << i);
|
||||||
pStore[i] = nOnes-pStore[i];
|
pStore[i] = nOnes-pStore[i];
|
||||||
|
|
|
||||||
|
|
@ -2,5 +2,6 @@ SRC += src/bool/lucky/lucky.c \
|
||||||
src/bool/lucky/luckyFast16.c \
|
src/bool/lucky/luckyFast16.c \
|
||||||
src/bool/lucky/luckyFast6.c \
|
src/bool/lucky/luckyFast6.c \
|
||||||
src/bool/lucky/luckyRead.c \
|
src/bool/lucky/luckyRead.c \
|
||||||
|
src/bool/lucky/luckySimple.c \
|
||||||
src/bool/lucky/luckySwapIJ.c \
|
src/bool/lucky/luckySwapIJ.c \
|
||||||
src/bool/lucky/luckySwap.c
|
src/bool/lucky/luckySwap.c
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue