summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp12
-rw-r--r--src/aig/aig/aigCanon.c8
-rw-r--r--src/base/abci/abc.c5
-rw-r--r--src/base/abci/abcNpn.c74
-rw-r--r--src/base/abci/abcRec.c8
-rw-r--r--src/base/abci/abcRec2.c11
-rw-r--r--src/bool/kit/kit.h8
-rw-r--r--src/bool/kit/kitTruth.c18
-rw-r--r--src/bool/lucky/lucky.c4
-rw-r--r--src/bool/lucky/lucky.h4
-rw-r--r--src/bool/lucky/luckyFast16.c625
-rw-r--r--src/bool/lucky/luckyFast6.c233
-rw-r--r--src/bool/lucky/luckyInt.h34
-rw-r--r--src/bool/lucky/luckySwap.c117
-rw-r--r--src/bool/lucky/luckySwapIJ.c102
-rw-r--r--src/bool/lucky/module.make3
-rw-r--r--src/map/if/ifDec16.c2
17 files changed, 1212 insertions, 56 deletions
diff --git a/abclib.dsp b/abclib.dsp
index 1a0a093d..2180e9a4 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3759,6 +3759,14 @@ SOURCE=.\src\bool\lucky\lucky.h
# End Source File
# Begin Source File
+SOURCE=.\src\bool\lucky\luckyFast16.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\lucky\luckyFast6.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\bool\lucky\luckyInt.h
# End Source File
# Begin Source File
@@ -3769,6 +3777,10 @@ SOURCE=.\src\bool\lucky\luckyRead.c
SOURCE=.\src\bool\lucky\luckySwap.c
# End Source File
+# Begin Source File
+
+SOURCE=.\src\bool\lucky\luckySwapIJ.c
+# End Source File
# End Group
# End Group
# Begin Group "prove"
diff --git a/src/aig/aig/aigCanon.c b/src/aig/aig/aigCanon.c
index e13e88fd..f8a50fab 100644
--- a/src/aig/aig/aigCanon.c
+++ b/src/aig/aig/aigCanon.c
@@ -37,7 +37,7 @@ typedef struct Aig_VSig_t_ Aig_VSig_t;
struct Aig_VSig_t_
{
int nOnes;
- short nCofOnes[RMAN_MAXVARS];
+ int nCofOnes[RMAN_MAXVARS];
};
typedef struct Aig_Tru_t_ Aig_Tru_t;
@@ -307,7 +307,7 @@ void Aig_RManQuit()
***********************************************************************/
void Aig_RManPrintVarProfile( unsigned * pTruth, int nVars, unsigned * pTruthAux )
{
- short pStore2[32];
+ int pStore2[32];
int i;
Kit_TruthCountOnesInCofsSlow( pTruth, nVars, pStore2, pTruthAux );
for ( i = 0; i < nVars; i++ )
@@ -326,7 +326,7 @@ void Aig_RManPrintVarProfile( unsigned * pTruth, int nVars, unsigned * pTruthAu
SeeAlso []
***********************************************************************/
-void Aig_RManSortNums( short * pArray, int nVars )
+void Aig_RManSortNums( int * pArray, int nVars )
{
int i, j, best_i, tmp;
for ( i = 0; i < nVars-1; i++ )
@@ -409,7 +409,7 @@ void Aig_RManComputeVSigs( unsigned * pTruth, int nVars, Aig_VSig_t * pSigs, uns
***********************************************************************/
static inline int Aig_RManCompareSigs( Aig_VSig_t * p0, Aig_VSig_t * p1, int nVars )
{
-// return memcmp( p0, p1, sizeof(int) + sizeof(short) * nVars );
+// return memcmp( p0, p1, sizeof(int) + sizeof(int) * nVars );
return memcmp( p0, p1, sizeof(int) );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 940e2643..25c77048 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4907,10 +4907,11 @@ usage:
Abc_Print( -2, "\t testbench for computing semi-canonical forms of Boolean functions\n" );
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 1: exact canonical form (work only for 6 variables)\n" );
+ Abc_Print( -2, "\t 1: exact canonical form (works only for 6 variables)\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 4: hybrid semi-canonical form (work only for 6 variables)\n" );
+ Abc_Print( -2, "\t 4: hybrid semi-canonical form (works only for 6 variables)\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-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 6e753e3b..e8c9168d 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -41,10 +41,10 @@ ABC_NAMESPACE_IMPL_START
typedef struct Abc_TtStore_t_ Abc_TtStore_t;
struct Abc_TtStore_t_
{
- int nVars;
- int nWords;
- int nFuncs;
- word ** pFuncs;
+ int nVars;
+ int nWords;
+ int nFuncs;
+ word ** pFuncs;
};
extern Abc_TtStore_t * Abc_TtStoreLoad( char * pFileName );
@@ -84,6 +84,26 @@ int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
/**Function*************************************************************
+ Synopsis [Prints out one NPN transform.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_TruthNpnPrint( char * pCanonPerm, unsigned uCanonPhase, int nVars )
+{
+ int i;
+ printf( " %c = ( ", Abc_InfoHasBit(&uCanonPhase, nVars) ? 'Z':'z' );
+ for ( i = 0; i < nVars; i++ )
+ printf( "%c%s", pCanonPerm[i] + ('A'-'a') * Abc_InfoHasBit(&uCanonPhase, pCanonPerm[i]-'a'), i == nVars-1 ? "":"," );
+ printf( " ) " );
+}
+
+/**Function*************************************************************
+
Synopsis [Apply decomposition to the truth table.]
Description [Returns the number of AIG nodes.]
@@ -95,24 +115,25 @@ int Abc_TruthNpnCountUnique( Abc_TtStore_t * p )
***********************************************************************/
void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
- short pStore[16];
- char pCanonPerm[16];
unsigned pAux[2048];
-
+ char pCanonPerm[32];
+ unsigned uCanonPhase=0;
clock_t clk = clock();
- int i;//, nFuncs = 0;
+ int i;
char * pAlgoName = NULL;
if ( NpnType == 0 )
- pAlgoName = "uniqifying ";
+ pAlgoName = "uniqifying ";
else if ( NpnType == 1 )
- pAlgoName = "exact NPN ";
+ pAlgoName = "exact NPN ";
else if ( NpnType == 2 )
- pAlgoName = "counting 1s ";
+ pAlgoName = "counting 1s ";
else if ( NpnType == 3 )
- pAlgoName = "minimizing TT";
+ pAlgoName = "minimizing TT ";
else if ( NpnType == 4 )
- pAlgoName = "hybrid NPN ";
+ pAlgoName = "hybrid NPN ";
+ else if ( NpnType == 5 )
+ pAlgoName = "Jake's hybrid NPN";
assert( p->nVars <= 16 );
if ( pAlgoName )
@@ -157,9 +178,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
- Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm, pStore );
+ resetPCanonPermArray(pCanonPerm, p->nVars);
+ uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
if ( fVerbose )
- Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), printf( "\n" );
+ Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
}
}
else if ( NpnType == 3 )
@@ -168,9 +190,10 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
- Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
+ resetPCanonPermArray(pCanonPerm, p->nVars);
+ uCanonPhase = Kit_TruthSemiCanonicize_new( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm );
if ( fVerbose )
- Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], 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 )
@@ -181,7 +204,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
- Kit_TruthSemiCanonicize( (unsigned *)p->pFuncs[i], pAux, p->nVars, pCanonPerm, pStore );
+ 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" );
@@ -190,6 +214,18 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
else
printf( "This feature only works for 6-variable functions.\n" );
}
+ else if ( NpnType == 5 )
+ {
+ for ( i = 0; i < p->nFuncs; i++ )
+ {
+ if ( fVerbose )
+ printf( "%7d : ", i );
+ resetPCanonPermArray(pCanonPerm, p->nVars);
+ uCanonPhase = luckyCanonicizer_final_fast( p->pFuncs[i], p->nVars, pCanonPerm );
+ if ( fVerbose )
+ Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(pCanonPerm, uCanonPhase, p->nVars), printf( "\n" );
+ }
+ }
else assert( 0 );
clk = clock() - clk;
@@ -248,7 +284,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int fVerbose )
{
if ( fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
- if ( NpnType >= 0 && NpnType <= 4 )
+ if ( NpnType >= 0 && NpnType <= 5 )
Abc_TruthNpnTest( pFileName, NpnType, fVerbose );
else
printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 83780233..cd2cae93 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -881,7 +881,7 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
- uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
+ uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
pCandMin = Abc_NtkRecLookUpBest(pIfMan, pCut, pInOut, pCanonPerm, pCompl,NULL);
Vec_PtrGrow(s_pMan->vLabels, Abc_NtkObjNumMax(pAig));
@@ -2252,7 +2252,7 @@ clk = clock();
// semi-canonicize the truth table
clk = clock();
- uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm, (short *)s_pMan->pMints );
+ uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm );
If_CutTruthStretch(pInOut, nLeaves, s_pMan->nVars);
s_pMan->timeCanon += clock() - clk;
// pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
@@ -2819,7 +2819,7 @@ int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
//canonicize
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
- uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
+ uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
s_pMan->timeIfCanonicize += clock() - timeCanonicize;
timeDelayComput = clock();
@@ -2997,7 +2997,7 @@ int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
pCanonPerm[i] = i;
// canonicize the truth table
- uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nVars, pCanonPerm, (short *)s_pMan->pMints );
+ uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nVars, pCanonPerm );
// get hold of the curresponding class
ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index 460436ef..4edda73a 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -1183,6 +1183,11 @@ for ( i = 0; i < p->nBins; i++ )
for ( entry = p->pBins[i]; entry != REC_EMPTY_ID; entry = Rec_Obj(p, entry)->pCopy )
{
int tmp = 0;
+
+ assert( 0 );
+ // added the next line to silence the warning that 'pEntry' is not initialized
+ pEntry = -1;
+
// pTruth = (unsigned*)Vec_PtrEntry(p->vTtNodes, entry);
pTruth = Rec_MemReadEntry( p, Rec_Obj(p, pEntry)->truthID );
/*if ( (int)Kit_TruthSupport(pTruth, nVars) != (1<<nVars)-1 )
@@ -1525,7 +1530,7 @@ clk = clock();
// semi-canonicize the truth table
clk = clock();
- uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm, (short *)s_pMan->pMints );
+ uCanonPhase = Kit_TruthSemiCanonicize( pInOut, pTemp, nLeaves, pCanonPerm );
If_CutTruthStretch(pInOut, nLeaves, s_pMan->nVars);
s_pMan->timeCanon += clock() - clk;
// pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
@@ -1875,7 +1880,7 @@ int If_CutDelayRecCost2(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
//canonicize
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
- uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
+ uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
s_pMan->timeIfCanonicize += clock() - timeCanonicize;
timeDelayComput = clock();
@@ -1986,7 +1991,7 @@ Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
for (i = 0; i < nLeaves; i++)
pCanonPerm[i] = i;
- uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
+ uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm);
If_CutTruthStretch(pInOut, nLeaves, nVars);
pCandMin = Abc_NtkRecLookUpBest(pIfMan, pCut, pInOut, pCanonPerm, pCompl,NULL);
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index 8151f1d2..5ecb5581 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -623,11 +623,11 @@ extern int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar
extern int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
extern int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
-extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
-extern void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore );
-extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
+extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, int * pStore );
+extern void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, int * pStore );
+extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, int * pStore, unsigned * pAux );
extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
-extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
+extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm );
extern char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
extern void Kit_TruthPrintProfile( unsigned * pTruth, int nVars );
diff --git a/src/bool/kit/kitTruth.c b/src/bool/kit/kitTruth.c
index 258207c2..a6951163 100644
--- a/src/bool/kit/kitTruth.c
+++ b/src/bool/kit/kitTruth.c
@@ -1397,7 +1397,7 @@ int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigne
Synopsis [Counts the number of 1's in each cofactor.]
- Description [The resulting numbers are stored in the array of shorts,
+ Description [The resulting numbers are stored in the array of ints,
whose length is 2*nVars. The number of 1's is counted in a different
space than the original function. For example, if the function depends
on k variables, the cofactors are assumed to depend on k-1 variables.]
@@ -1407,11 +1407,11 @@ int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigne
SeeAlso []
***********************************************************************/
-void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
+void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, int * pStore )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Counter;
- memset( pStore, 0, sizeof(short) * 2 * nVars );
+ memset( pStore, 0, sizeof(int) * 2 * nVars );
if ( nVars <= 5 )
{
if ( nVars > 0 )
@@ -1473,7 +1473,7 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
Synopsis [Counts the number of 1's in each negative cofactor.]
- Description [The resulting numbers are stored in the array of shorts,
+ Description [The resulting numbers are stored in the array of ints,
whose length is nVars. The number of 1's is counted in a different
space than the original function. For example, if the function depends
on k variables, the cofactors are assumed to depend on k-1 variables.]
@@ -1483,11 +1483,11 @@ void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore )
SeeAlso []
***********************************************************************/
-void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore )
+void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, int * pStore )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Counter;
- memset( pStore, 0, sizeof(short) * nVars );
+ memset( pStore, 0, sizeof(int) * nVars );
if ( nVars <= 5 )
{
if ( nVars > 0 )
@@ -1534,7 +1534,7 @@ void Kit_TruthCountOnesInCofs0( unsigned * pTruth, int nVars, short * pStore )
SeeAlso []
***********************************************************************/
-void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux )
+void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, int * pStore, unsigned * pAux )
{
int i;
for ( i = 0; i < nVars; i++ )
@@ -1654,9 +1654,9 @@ unsigned Kit_TruthHash( unsigned * pIn, int nWords )
SeeAlso []
***********************************************************************/
-unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore )
+unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
{
-// short pStore2[32];
+ int pStore[32];
unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
int nWords = Kit_TruthWordNum( nVars );
int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
diff --git a/src/bool/lucky/lucky.c b/src/bool/lucky/lucky.c
index 8fc413be..159c54bc 100644
--- a/src/bool/lucky/lucky.c
+++ b/src/bool/lucky/lucky.c
@@ -655,7 +655,7 @@ int main ()
word** a, ** b;
Abc_TtStore_t* p;
word * pAux, * pAux1;
- short * pStore;
+ int * pStore;
// cycleCtr* cCtr;
charArray = (char**)malloc(sizeof(char*)*3);
@@ -672,7 +672,7 @@ int main ()
pAux = (word*)malloc(sizeof(word)*(p->nWords));
pAux1 = (word*)malloc(sizeof(word)*(p->nWords));
- pStore = (short*)malloc(sizeof(short)*(p->nVars));
+ pStore = (int*)malloc(sizeof(int)*(p->nVars));
printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
tempNF = p->nFuncs;
diff --git a/src/bool/lucky/lucky.h b/src/bool/lucky/lucky.h
index 7b866bc7..0a055b40 100644
--- a/src/bool/lucky/lucky.h
+++ b/src/bool/lucky/lucky.h
@@ -6,7 +6,7 @@
PackageName [Semi-canonical form computation package.]
- Synopsis [Internal declarations.]
+ Synopsis [External declarations.]
Author [Jake]
@@ -21,6 +21,8 @@
ABC_NAMESPACE_HEADER_START
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 void resetPCanonPermArray(char* x, int nVars);
ABC_NAMESPACE_HEADER_END
diff --git a/src/bool/lucky/luckyFast16.c b/src/bool/lucky/luckyFast16.c
new file mode 100644
index 00000000..518f236b
--- /dev/null
+++ b/src/bool/lucky/luckyFast16.c
@@ -0,0 +1,625 @@
+/**CFile****************************************************************
+
+ FileName [luckyFast16.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Semi-canonical form computation package.]
+
+ Synopsis [Truth table minimization procedures for up to 16 vars.]
+
+ Author [Jake]
+
+ Date [Started - September 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////lessThen5/////////////////////////////////////////////////////////////////////////////////////////////
+
+// there are 4 parts in every block to compare and rearrange - quoters(0Q,1Q,2Q,3Q)
+//updataInfo updates CanonPerm and CanonPhase based on what quoter in position iQ and jQ
+inline void updataInfo(int iQ, int jQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ *pCanonPhase = adjustInfoAfterSwap(pCanonPerm, *pCanonPhase, iVar, ((abs(iQ-jQ)-1)<<2) + iQ );
+
+}
+// It rearranges InOut (swaps and flips through rearrangement of quoters)
+// It updates Info at the end
+inline void arrangeQuoters_superFast_lessThen5(word* pInOut, int start, int iQ, int jQ, int kQ, int lQ, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int i;
+ int blockSize = 1<<iVar;
+ for(i=start;i>=0;i--)
+ {
+ pInOut[i] = (pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize) |
+ (((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize))>>blockSize) |
+ (((pInOut[i] & SFmask[iVar][kQ])<<(kQ*blockSize))>>2*blockSize) |
+ (((pInOut[i] & SFmask[iVar][lQ])<<(lQ*blockSize))>>3*blockSize);
+ }
+ updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
+}
+
+//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 0Q and 3Q
+inline int minTemp0_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+ int i, j=1;
+ int blockSize = 1<<iVar;
+ int shiftSize = blockSize*4;
+ word temp;
+ for(i=nWords - 1; i>=0; i--)
+ {
+ temp = ((pInOut[i] & SFmask[iVar][0])) ^ ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize));
+ if( temp == 0)
+ continue;
+ else
+ {
+ *pDifStart = i*100;
+ while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+ j++;
+ *pDifStart += 21 - j;
+
+ if( ((pInOut[i] & SFmask[iVar][0])) < ((pInOut[i] & SFmask[iVar][3])<<(3*blockSize)) )
+ return 0;
+ else
+ return 3;
+ }
+ }
+ *pDifStart=0;
+ return 0;
+
+}
+
+//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 1Q and 2Q
+inline int minTemp1_fast(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+ int i, j=1;
+ int blockSize = 1<<iVar;
+ int shiftSize = blockSize*4;
+ word temp;
+ for(i=nWords - 1; i>=0; i--)
+ {
+ temp = ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) ^ ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize));
+ if( temp == 0)
+ continue;
+ else
+ {
+ *pDifStart = i*100;
+ while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+ j++;
+ *pDifStart += 21 - j;
+ if( ((pInOut[i] & SFmask[iVar][1])<<(blockSize)) < ((pInOut[i] & SFmask[iVar][2])<<(2*blockSize)) )
+ return 1;
+ else
+ return 2;
+ }
+ }
+ *pDifStart=0;
+ return 1;
+}
+
+//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in iQ and jQ
+inline int minTemp2_fast(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
+{
+ int i, j=1;
+ int blockSize = 1<<iVar;
+ int shiftSize = blockSize*4;
+ word temp;
+ for(i=nWords - 1; i>=0; i--)
+ {
+ temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
+ if( temp == 0)
+ continue;
+ else
+ {
+ *pDifStart = i*100;
+ while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+ j++;
+ *pDifStart += 21 - j;
+ if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
+ return 0;
+ else
+ return 1;
+ }
+ }
+ *pDifStart=0;
+ return iQ;
+}
+// same as minTemp2_fast but this one has a start position
+inline int minTemp3_fast(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
+{
+ int i, j=1;
+ int blockSize = 1<<iVar;
+ int shiftSize = blockSize*4;
+ word temp;
+ for(i=start; i>=finish; i--)
+ {
+ temp = ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) ^ ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize));
+ if( temp == 0)
+ continue;
+ else
+ {
+ *pDifStart = i*100;
+ while(temp == (temp<<(shiftSize*j))>>shiftSize*j)
+ j++;
+ *pDifStart += 21 - j;
+
+ if( ((pInOut[i] & SFmask[iVar][iQ])<<(iQ*blockSize)) <= ((pInOut[i] & SFmask[iVar][jQ])<<(jQ*blockSize)) )
+ return 0;
+ else
+ return 1;
+ }
+ }
+ *pDifStart=0;
+ return iQ;
+}
+
+// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
+inline void minimalSwapAndFlipIVar_superFast_lessThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int min1, min2, DifStart0, DifStart1, DifStartMin;
+ int M[2];
+ int blockSize = 1<<iVar;
+ int shiftSize = blockSize*4;
+
+ M[0] = minTemp0_fast(pInOut, iVar, nWords, &DifStart0); // 0, 3
+ M[1] = minTemp1_fast(pInOut, iVar, nWords, &DifStart1); // 1, 2
+ min1 = minTemp2_fast(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
+ if(DifStart0 != DifStart1)
+ {
+ if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
+ arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
+ else if( DifStart0 > DifStart1)
+ arrangeQuoters_superFast_lessThen5(pInOut,max(DifStartMin/100, DifStart0/100), M[0], M[1], 3 - M[1], 3 - M[0], iVar, nWords, pCanonPerm, pCanonPhase);
+ else
+ arrangeQuoters_superFast_lessThen5(pInOut,max(DifStartMin/100, DifStart1/100), M[1], M[0], 3 - M[0], 3 - M[1], iVar, nWords, pCanonPerm, pCanonPhase);
+ }
+ else
+ {
+ if(DifStartMin>=DifStart0)
+ arrangeQuoters_superFast_lessThen5(pInOut, DifStartMin/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
+ else
+ {
+ min2 = minTemp3_fast(pInOut, iVar, DifStart0/100, DifStartMin/100, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
+ if(DifStart1>DifStartMin)
+ arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], iVar, nWords, pCanonPerm, pCanonPhase);
+ else
+ arrangeQuoters_superFast_lessThen5(pInOut, DifStart0/100, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, nWords, pCanonPerm, pCanonPhase);
+ }
+ }
+}
+////////////////////////////////////iVar = 5/////////////////////////////////////////////////////////////////////////////////////////////
+
+// It rearranges InOut (swaps and flips through rearrangement of quoters)
+// It updates Info at the end
+inline void arrangeQuoters_superFast_iVar5(unsigned* pInOut, unsigned* temp, int start, int iQ, int jQ, int kQ, int lQ, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int i,blockSize,shiftSize;
+ unsigned* tempPtr = temp+start;
+ if(iQ == 0 && jQ == 1)
+ return;
+ blockSize = sizeof(unsigned);
+ shiftSize = 4;
+ for(i=start-1;i>0;i-=shiftSize)
+ {
+ tempPtr -= 1;
+ memcpy(tempPtr, pInOut+i-iQ, blockSize);
+ tempPtr -= 1;
+ memcpy(tempPtr, pInOut+i-jQ, blockSize);
+ tempPtr -= 1;
+ memcpy(tempPtr, pInOut+i-kQ, blockSize);
+ tempPtr -= 1;
+ memcpy(tempPtr, pInOut+i-lQ, blockSize);
+
+ }
+ memcpy(pInOut, temp, start*sizeof(unsigned));
+ updataInfo(iQ, jQ, 5, pCanonPerm, pCanonPhase);
+}
+
+//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 0Q and 3Q
+inline int minTemp0_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
+{
+ int i, temp;
+ for(i=(nWords)*2 - 1; i>=0; i-=4)
+ {
+ temp = CompareWords(pInOut[i],pInOut[i-3]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+1;
+ return 0;
+ }
+ else
+ {
+ *pDifStart = i+1;
+ return 3;
+ }
+ }
+ *pDifStart=0;
+ return 0;
+}
+
+//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 1Q and 2Q
+inline int minTemp1_fast_iVar5(unsigned* pInOut, int nWords, int* pDifStart)
+{
+ int i, temp;
+ for(i=(nWords)*2 - 2; i>=0; i-=4)
+ {
+ temp = CompareWords(pInOut[i],pInOut[i-1]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+2;
+ return 1;
+ }
+ else
+ {
+ *pDifStart = i+2;
+ return 2;
+ }
+ }
+ *pDifStart=0;
+ return 1;
+}
+
+//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in iQ and jQ
+inline int minTemp2_fast_iVar5(unsigned* pInOut, int iQ, int jQ, int nWords, int* pDifStart)
+{
+ int i, temp;
+ for(i=(nWords)*2 - 1; i>=0; i-=4)
+ {
+ temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+1;
+ return 0;
+ }
+ else
+ {
+ *pDifStart = i+1;
+ return 1;
+ }
+ }
+ *pDifStart=0;
+ return iQ;
+}
+
+// same as minTemp2_fast but this one has a start position
+inline int minTemp3_fast_iVar5(unsigned* pInOut, int start, int finish, int iQ, int jQ, int* pDifStart)
+{
+ int i, temp;
+ for(i=start-1; i>=finish; i-=4)
+ {
+ temp = CompareWords(pInOut[i-iQ],pInOut[i-jQ]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+1;
+ return 0;
+ }
+ else
+ {
+ *pDifStart = i+1;
+ return 1;
+ }
+ }
+ *pDifStart=0;
+ return iQ;
+}
+
+// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
+inline void minimalSwapAndFlipIVar_superFast_iVar5(unsigned* pInOut, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int min1, min2, DifStart0, DifStart1, DifStartMin;
+ int M[2];
+ unsigned temp[2048];
+
+ M[0] = minTemp0_fast_iVar5(pInOut, nWords, &DifStart0); // 0, 3
+ M[1] = minTemp1_fast_iVar5(pInOut, nWords, &DifStart1); // 1, 2
+ min1 = minTemp2_fast_iVar5(pInOut, M[0], M[1], nWords, &DifStartMin);
+ if(DifStart0 != DifStart1)
+ {
+ if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
+ arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
+ else if( DifStart0 > DifStart1)
+ arrangeQuoters_superFast_iVar5(pInOut, temp, max(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], pCanonPerm, pCanonPhase);
+ else
+ arrangeQuoters_superFast_iVar5(pInOut, temp, max(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], pCanonPerm, pCanonPhase);
+ }
+ else
+ {
+ if(DifStartMin>=DifStart0)
+ arrangeQuoters_superFast_iVar5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
+ else
+ {
+ min2 = minTemp3_fast_iVar5(pInOut, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
+ if(DifStart1>DifStartMin)
+ arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], pCanonPerm, pCanonPhase);
+ else
+ arrangeQuoters_superFast_iVar5(pInOut, temp, DifStart0, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], pCanonPerm, pCanonPhase);
+ }
+ }
+}
+
+////////////////////////////////////moreThen5/////////////////////////////////////////////////////////////////////////////////////////////
+
+// It rearranges InOut (swaps and flips through rearrangement of quoters)
+// It updates Info at the end
+inline void arrangeQuoters_superFast_moreThen5(word* pInOut, word* temp, int start, int iQ, int jQ, int kQ, int lQ, int iVar, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int i,wordBlock,blockSize,shiftSize;
+ word* tempPtr = temp+start;
+ if(iQ == 0 && jQ == 1)
+ return;
+ wordBlock = (1<<(iVar-6));
+ blockSize = wordBlock*sizeof(word);
+ shiftSize = wordBlock*4;
+ for(i=start-wordBlock;i>0;i-=shiftSize)
+ {
+ tempPtr -= wordBlock;
+ memcpy(tempPtr, pInOut+i-iQ*wordBlock, blockSize);
+ tempPtr -= wordBlock;
+ memcpy(tempPtr, pInOut+i-jQ*wordBlock, blockSize);
+ tempPtr -= wordBlock;
+ memcpy(tempPtr, pInOut+i-kQ*wordBlock, blockSize);
+ tempPtr -= wordBlock;
+ memcpy(tempPtr, pInOut+i-lQ*wordBlock, blockSize);
+
+ }
+ memcpy(pInOut, temp, start*sizeof(word));
+ updataInfo(iQ, jQ, iVar, pCanonPerm, pCanonPhase);
+}
+
+//It compares 0Q and 3Q and returns 0 if 0Q is smaller then 3Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 0Q and 3Q
+inline int minTemp0_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+ int i, j, temp;
+ int wordBlock = 1<<(iVar-6);
+ int wordDif = 3*wordBlock;
+ int shiftBlock = wordBlock*4;
+ for(i=nWords - 1; i>=0; i-=shiftBlock)
+ for(j=0;j<wordBlock;j++)
+ {
+ temp = CompareWords(pInOut[i-j],pInOut[i-j-wordDif]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+1;
+ return 0;
+ }
+ else
+ {
+ *pDifStart = i+1;
+ return 3;
+ }
+ }
+ *pDifStart=0;
+ return 0;
+}
+
+//It compares 1Q and 2Q and returns 1 if 1Q is smaller then 2Q ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in 1Q and 2Q
+inline int minTemp1_fast_moreThen5(word* pInOut, int iVar, int nWords, int* pDifStart)
+{
+ int i, j, temp;
+ int wordBlock = 1<<(iVar-6);
+ int shiftBlock = wordBlock*4;
+ for(i=nWords - wordBlock - 1; i>=0; i-=shiftBlock)
+ for(j=0;j<wordBlock;j++)
+ {
+ temp = CompareWords(pInOut[i-j],pInOut[i-j-wordBlock]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+wordBlock+1;
+ return 1;
+ }
+ else
+ {
+ *pDifStart = i+wordBlock+1;
+ return 2;
+ }
+ }
+ *pDifStart=0;
+ return 1;
+}
+
+//It compares iQ and jQ and returns 0 if iQ is smaller then jQ ( comparison starts at highest bit) and visa versa
+// DifStart contains the information about the first different bit in iQ and jQ
+inline int minTemp2_fast_moreThen5(word* pInOut, int iVar, int iQ, int jQ, int nWords, int* pDifStart)
+{
+ int i, j, temp;
+ int wordBlock = 1<<(iVar-6);
+ int shiftBlock = wordBlock*4;
+ for(i=nWords - 1; i>=0; i-=shiftBlock)
+ for(j=0;j<wordBlock;j++)
+ {
+ temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+1;
+ return 0;
+ }
+ else
+ {
+ *pDifStart = i+1;
+ return 1;
+ }
+ }
+ *pDifStart=0;
+ return iQ;
+}
+
+// same as minTemp2_fast but this one has a start position
+inline int minTemp3_fast_moreThen5(word* pInOut, int iVar, int start, int finish, int iQ, int jQ, int* pDifStart)
+{
+ int i, j, temp;
+ int wordBlock = 1<<(iVar-6);
+ int shiftBlock = wordBlock*4;
+ for(i=start-1; i>=finish; i-=shiftBlock)
+ for(j=0;j<wordBlock;j++)
+ {
+ temp = CompareWords(pInOut[i-j-iQ*wordBlock],pInOut[i-j-jQ*wordBlock]);
+ if(temp == 0)
+ continue;
+ else if(temp == -1)
+ {
+ *pDifStart = i+1;
+ return 0;
+ }
+ else
+ {
+ *pDifStart = i+1;
+ return 1;
+ }
+ }
+ *pDifStart=0;
+ return iQ;
+}
+
+// It considers all swap and flip possibilities of iVar and iVar+1 and switches InOut to a minimal of them
+inline void minimalSwapAndFlipIVar_superFast_moreThen5(word* pInOut, int iVar, int nWords, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int min1, min2, DifStart0, DifStart1, DifStartMin;
+ int M[2];
+ word temp[1024];
+ int blockSize = 1<<(iVar-6);
+ int shiftSize = blockSize*4;
+
+ M[0] = minTemp0_fast_moreThen5(pInOut, iVar, nWords, &DifStart0); // 0, 3
+ M[1] = minTemp1_fast_moreThen5(pInOut, iVar, nWords, &DifStart1); // 1, 2
+ min1 = minTemp2_fast_moreThen5(pInOut, iVar, M[0], M[1], nWords, &DifStartMin);
+ if(DifStart0 != DifStart1)
+ {
+ if( DifStartMin>=DifStart1 && DifStartMin>=DifStart0 )
+ arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
+ else if( DifStart0 > DifStart1)
+ arrangeQuoters_superFast_moreThen5(pInOut, temp, max(DifStartMin,DifStart0), M[0], M[1], 3 - M[1], 3 - M[0], iVar, pCanonPerm, pCanonPhase);
+ else
+ arrangeQuoters_superFast_moreThen5(pInOut, temp, max(DifStartMin,DifStart1), M[1], M[0], 3 - M[0], 3 - M[1], iVar, pCanonPerm, pCanonPhase);
+ }
+ else
+ {
+ if(DifStartMin>=DifStart0)
+ arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStartMin, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
+ else
+ {
+ min2 = minTemp3_fast_moreThen5(pInOut, iVar, DifStart0, DifStartMin, 3-M[0], 3-M[1], &DifStart1); // reuse DifStart1 because DifStart1 = DifStart1=0
+ if(DifStart1>DifStartMin)
+ arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[(min2+1)%2], M[min2], 3 - M[min2], 3 - M[(min2+1)%2], iVar, pCanonPerm, pCanonPhase);
+ else
+ arrangeQuoters_superFast_moreThen5(pInOut, temp, DifStart0, M[min1], M[(min1+1)%2], 3 - M[(min1+1)%2], 3 - M[min1], iVar, pCanonPerm, pCanonPhase);
+ }
+ }
+}
+
+/////////////////////////////////// for all /////////////////////////////////////////////////////////////////////////////////////////////
+inline void minimalInitialFlip_fast_16Vars(word* pInOut, int nVars, unsigned* pCanonPhase)
+{
+ word oneWord=1;
+ if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
+ {
+ Kit_TruthNot_64bit( pInOut, nVars );
+ (* pCanonPhase) ^=(1<<nVars);
+ }
+
+}
+
+// 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
+inline int minimalSwapAndFlipIVar_superFast_all(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ int i;
+ word pDuplicate[1024];
+ int bitInfoTemp = pStore[0];
+ memcpy(pDuplicate,pInOut,nWords*sizeof(word));
+ for(i=0;i<5;i++)
+ {
+ if(bitInfoTemp == pStore[i+1])
+ minimalSwapAndFlipIVar_superFast_lessThen5(pInOut, i, nWords, pCanonPerm, pCanonPhase);
+ else
+ {
+ bitInfoTemp = pStore[i+1];
+ continue;
+ }
+ }
+ if(bitInfoTemp == pStore[i+1])
+ minimalSwapAndFlipIVar_superFast_iVar5((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(pInOut, i, nWords, pCanonPerm, pCanonPhase);
+ else
+ {
+ bitInfoTemp = pStore[i+1];
+ continue;
+ }
+ }
+ if(memcmp(pInOut,pDuplicate , nWords*sizeof(word)) == 0)
+ return 0;
+ else
+ return 1;
+}
+
+inline void luckyCanonicizerS_F_first_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
+ minimalInitialFlip_fast_16Vars(pInOut, nVars, pCanonPhase);
+ while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
+ continue;
+}
+
+inline void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+{
+// word pDuplicateLocal[1024]={0};
+// memcpy(pDuplicateLocal,pInOut,nWords*sizeof(word));
+ assert( nVars <= 16 );
+ assert( nVars > 6 );
+ (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( pInOut, nVars, pCanonPerm, pStore );
+ luckyCanonicizerS_F_first_16Vars(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)
+int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
+{
+ int pStore[16];
+ int uCanonPhase = 0;
+ int nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
+ if ( nVars <= 6 )
+ pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase );
+ else if ( nVars <= 16 )
+ luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
+ else assert( 0 );
+ return uCanonPhase;
+}
+
+
+ABC_NAMESPACE_IMPL_END
+
+
+
+
diff --git a/src/bool/lucky/luckyFast6.c b/src/bool/lucky/luckyFast6.c
new file mode 100644
index 00000000..9ba6691c
--- /dev/null
+++ b/src/bool/lucky/luckyFast6.c
@@ -0,0 +1,233 @@
+/**CFile****************************************************************
+
+ FileName [luckyFast6.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Semi-canonical form computation package.]
+
+ Synopsis [Truth table minimization procedures for 6 vars.]
+
+ Author [Jake]
+
+ Date [Started - September 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+inline void resetPCanonPermArray_6Vars(char* x)
+{
+ x[0]='a';
+ x[1]='b';
+ x[2]='c';
+ x[3]='d';
+ x[4]='e';
+ x[5]='f';
+}
+inline void resetPCanonPermArray(char* x, int nVars)
+{
+ int i;
+ for(i=0;i<nVars;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 & (unsigned)1 == 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 & (unsigned)1 == 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)
+{
+ if( (x>>63) )
+ {
+ (* pCanonPhase) ^=(1<<6);
+ return ~x;
+ }
+ else
+ return x;
+
+}
+
+inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info)
+{
+ if(info<4)
+ return (uCanonPhase ^= (info << iVar));
+ else
+ {
+ char temp;
+ uCanonPhase ^= ((info-4) << iVar);
+ temp=pCanonPerm[iVar];
+ pCanonPerm[iVar]=pCanonPerm[iVar+1];
+ pCanonPerm[iVar+1]=temp;
+ if ( ((uCanonPhase & (1 << iVar)) > 0) != ((uCanonPhase & (1 << (iVar+1))) > 0) )
+ {
+ uCanonPhase ^= (1 << iVar);
+ uCanonPhase ^= (1 << (iVar+1));
+ }
+ return uCanonPhase;
+ }
+
+
+}
+
+inline word Extra_Truth6SwapAdjacent( word t, int iVar )
+{
+ // variable swapping code
+ static word PMasks[5][3] = {
+ { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
+ { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 },
+ { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 },
+ { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 },
+ { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }
+ };
+ assert( iVar < 5 );
+ return (t & PMasks[iVar][0]) | ((t & PMasks[iVar][1]) << (1 << iVar)) | ((t & PMasks[iVar][2]) >> (1 << iVar));
+}
+inline word Extra_Truth6ChangePhase( word t, int iVar)
+{
+ // elementary truth tables
+ static word Truth6[6] = {
+ 0xAAAAAAAAAAAAAAAA,
+ 0xCCCCCCCCCCCCCCCC,
+ 0xF0F0F0F0F0F0F0F0,
+ 0xFF00FF00FF00FF00,
+ 0xFFFF0000FFFF0000,
+ 0xFFFFFFFF00000000
+ };
+ assert( iVar < 6 );
+ return ((t & ~Truth6[iVar]) << (1 << iVar)) | ((t & Truth6[iVar]) >> (1 << iVar));
+}
+
+inline word Extra_Truth6MinimumRoundOne( word t, int iVar, char* pCanonPerm, unsigned* pCanonPhase )
+{
+ word tCur, tMin = t; // ab
+ unsigned info =0;
+ assert( iVar >= 0 && iVar < 5 );
+
+ tCur = Extra_Truth6ChangePhase( t, iVar ); // !a b
+ if(tCur<tMin)
+ {
+ info = 1;
+ tMin = tCur;
+ }
+ tCur = Extra_Truth6ChangePhase( t, iVar+1 ); // a !b
+ if(tCur<tMin)
+ {
+ info = 2;
+ tMin = tCur;
+ }
+ tCur = Extra_Truth6ChangePhase( tCur, iVar ); // !a !b
+ if(tCur<tMin)
+ {
+ info = 3;
+ tMin = tCur;
+ }
+
+ t = Extra_Truth6SwapAdjacent( t, iVar ); // b a
+ if(t<tMin)
+ {
+ info = 4;
+ tMin = t;
+ }
+
+ tCur = Extra_Truth6ChangePhase( t, iVar ); // !b a
+ if(tCur<tMin)
+ {
+ info = 6;
+ tMin = tCur;
+ }
+ tCur = Extra_Truth6ChangePhase( t, iVar+1 ); // b !a
+ if(tCur<tMin)
+ {
+ info = 5;
+ tMin = tCur;
+ }
+ tCur = Extra_Truth6ChangePhase( tCur, iVar ); // !b !a
+ if(tCur<tMin)
+ {
+ (* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, 7);
+ return tCur;
+ }
+ else
+ {
+ (* pCanonPhase) = adjustInfoAfterSwap(pCanonPerm, * pCanonPhase, iVar, info);
+ return tMin;
+ }
+}
+// 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
+inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+ int i, bitInfoTemp;
+ word tMin0, tMin;
+ tMin=Abc_allFlip(t, pCanonPhase);
+ do
+ {
+ bitInfoTemp = pStore[0];
+ tMin0 = tMin;
+ for ( i = 0; i < 5; i++ )
+ {
+ if(bitInfoTemp == pStore[i+1])
+ tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
+ else
+ bitInfoTemp = pStore[i+1];
+ }
+
+ }while ( tMin0 != tMin );
+ return tMin;
+}
+
+
+inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+// word temp, duplicat = InOut;
+ (* pCanonPhase) = Kit_TruthSemiCanonicize_Yasha1( &InOut, 6, pCanonPerm, pStore);
+// InOut = Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPhase, pCanonPerm );
+// temp = InOut;
+// assert(!luckyCheck(&temp, &duplicat, 6, pCanonPerm, * pCanonPhase));
+// return(InOut);
+ return Extra_Truth6MinimumRoundMany(InOut, pStore, pCanonPerm, pCanonPhase );
+
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 295d3c30..02dc690d 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -24,6 +24,7 @@
#include <math.h>
#include <time.h>
+
// comment out this line to run Lucky Code outside of ABC
#define _RUNNING_ABC_
@@ -80,6 +81,8 @@ typedef struct
int totalFlips;
}permInfo;
+
+
static inline void TimePrint( char* Message )
{
static int timeBegin;
@@ -89,6 +92,25 @@ static inline void TimePrint( char* Message )
timeBegin = clock();
}
+static word SFmask[5][4] = {
+ {0x8888888888888888,0x4444444444444444,0x2222222222222222,0x1111111111111111},
+ {0xC0C0C0C0C0C0C0C0,0x3030303030303030,0x0C0C0C0C0C0C0C0C,0x0303030303030303},
+ {0xF000F000F000F000,0x0F000F000F000F00,0x00F000F000F000F0,0x000F000F000F000F},
+ {0xFF000000FF000000,0x00FF000000FF0000,0x0000FF000000FF00,0x000000FF000000FF},
+ {0xFFFF000000000000,0x0000FFFF00000000,0x00000000FFFF0000,0x000000000000FFFF}
+};
+
+static inline int CompareWords(word x, word y)
+{
+ if(x>y)
+ return 1;
+ else if(x<y)
+ return -1;
+ else
+ return 0;
+
+}
+
extern inline int memCompare(word* x, word* y, int nVars);
extern inline int Kit_TruthWordNum_64bit( int nVars );
extern Abc_TtStore_t * setTtStore(char * pFileInput);
@@ -101,8 +123,16 @@ extern inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars );
extern void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars);
extern permInfo* setPermInfoPtr(int var);
extern void freePermInfoPtr(permInfo* x);
-extern inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm );
-extern inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm );
+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_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 void luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase);
+extern inline void resetPCanonPermArray_6Vars(char* x);
+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 void resetPCanonPermArray(char* x, int nVars);
+
ABC_NAMESPACE_HEADER_END
diff --git a/src/bool/lucky/luckySwap.c b/src/bool/lucky/luckySwap.c
index 46db2b0f..2a710160 100644
--- a/src/bool/lucky/luckySwap.c
+++ b/src/bool/lucky/luckySwap.c
@@ -16,6 +16,7 @@
#include "luckyInt.h"
+
ABC_NAMESPACE_IMPL_START
@@ -205,7 +206,7 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
- if ( pStore[i] <= nOnes-pStore[i])
+ if ( pStore[i] >= nOnes-pStore[i])
continue;
uCanonPhase |= (1 << i);
pStore[i] = nOnes-pStore[i];
@@ -240,11 +241,118 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char *
} while ( fChange );
return uCanonPhase;
}
+inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore )
+{
+ int nWords = Kit_TruthWordNum_64bit( nVars );
+ int i, fChange, nOnes;
+ int Temp;
+ unsigned uCanonPhase=0;
+ assert( nVars <= 16 );
+
+ nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+ // if ( (nOnes == nWords * 32) )
+ // return 999999;
+
+ if ( (nOnes > nWords * 32) )
+ {
+ uCanonPhase |= (1 << nVars);
+ Kit_TruthNot_64bit( pInOut, nVars );
+ nOnes = nWords*64 - nOnes;
+ }
+
+ // collect the minterm counts
+ Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
+
+ // canonicize phase
+ for ( i = 0; i < nVars; i++ )
+ {
+ // if ( pStore[i] == nOnes-pStore[i])
+ // return 999999;
+ if ( pStore[i] >= nOnes-pStore[i])
+ continue;
+ uCanonPhase |= (1 << i);
+ pStore[i] = nOnes-pStore[i];
+ Kit_TruthChangePhase_64bit( pInOut, nVars, i );
+ }
+
+ do {
+ fChange = 0;
+ for ( i = 0; i < nVars-1; i++ )
+ {
+ if ( pStore[i] <= pStore[i+1] )
+ continue;
+ fChange = 1;
+
+ Temp = pCanonPerm[i];
+ pCanonPerm[i] = pCanonPerm[i+1];
+ pCanonPerm[i+1] = Temp;
+
+ Temp = pStore[i];
+ pStore[i] = pStore[i+1];
+ pStore[i+1] = Temp;
+
+ // if the polarity of variables is different, swap them
+ if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
+ {
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << (i+1));
+ }
+
+ Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+ }
+ } while ( fChange );
+ return uCanonPhase;
+}
+
-inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
+// inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, char * pCanonPerm )
+// {
+// unsigned uCanonPhase = 0;
+// int pStore[16];
+// int nWords = Kit_TruthWordNum_64bit( nVars );
+// int i, Temp, fChange, nOnes;
+// assert( nVars <= 16 );
+//
+// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
+//
+// if ( (nOnes > nWords * 32) )
+// {
+// Kit_TruthNot_64bit( pInOut, nVars );
+// nOnes = nWords*64 - nOnes;
+// }
+//
+// // collect the minterm counts
+// Kit_TruthCountOnesInCofs_64bit( pInOut, nVars, pStore );
+//
+// // canonicize phase
+// for ( i = 0; i < nVars; i++ )
+// {
+// if ( pStore[i] >= nOnes-pStore[i])
+// continue;
+// pStore[i] = nOnes-pStore[i];
+// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
+// }
+//
+// do {
+// fChange = 0;
+// for ( i = 0; i < nVars-1; i++ )
+// {
+// if ( pStore[i] <= pStore[i+1] )
+// continue;
+// fChange = 1;
+//
+// Temp = pStore[i];
+// pStore[i] = pStore[i+1];
+// pStore[i+1] = Temp;
+//
+// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
+// }
+// } while ( fChange );
+// return uCanonPhase;
+// }
+
+inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore )
{
- unsigned uCanonPhase = 0;
- int pStore[16];
int nWords = Kit_TruthWordNum_64bit( nVars );
int i, Temp, fChange, nOnes;
assert( nVars <= 16 );
@@ -284,7 +392,6 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars,
Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
}
} while ( fChange );
- return uCanonPhase;
}
diff --git a/src/bool/lucky/luckySwapIJ.c b/src/bool/lucky/luckySwapIJ.c
new file mode 100644
index 00000000..1d598c2a
--- /dev/null
+++ b/src/bool/lucky/luckySwapIJ.c
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+ FileName [luckySwapIJ.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Semi-canonical form computation package.]
+
+ Synopsis [just for support of swap_ij() function]
+
+ Author [Jake]
+
+ Date [Started - September 2012]
+
+***********************************************************************/
+
+#include "luckyInt.h"
+
+
+ABC_NAMESPACE_IMPL_START
+
+
+void swap_ij_case1( word* f,int totalVars, int i, int j)
+{
+ int e,wordsNumber,n,shift;
+ word maskArray[45]=
+ { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 ,0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050,
+ 0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 ,0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 ,
+ 0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 ,0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 ,
+ 0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 ,0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 ,
+ 0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 ,0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 ,
+ 0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 ,0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 ,
+ 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 ,0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 ,
+ 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000
+ };
+ e = 3*((9*i - i*i -2)/2 + j); // Exact formula for index in maskArray
+ wordsNumber = Kit_TruthWordNum_64bit(totalVars);
+ shift = (1<<j)-(1<<i);
+ for(n = 0; n < wordsNumber; n++)
+ f[n] = (f[n]&maskArray[e])+((f[n]&(maskArray[e+1]))<< shift)+((f[n]&(maskArray[e+2]))>> shift);
+}
+// "width" - how many "Words" in a row have "1s" (or "0s")in position "i"
+// wi - width of i
+// wj - width of j
+// wwi = 2*wi; wwj = 2*wj;
+
+void swap_ij_case2( word* f,int totalVars, int i, int j)
+{
+ word mask[] = { 0xAAAAAAAAAAAAAAAA,0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0,
+ 0xFF00FF00FF00FF00,0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 };
+ word temp;
+ int x,y,wj;
+ int WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
+ // int forShift = ((Word)1)<<i;
+ int forShift = (1<<i);
+ wj = 1 << (j - 6);
+ x = 0;
+ y = wj;
+ for(y=wj; y<WORDS_IN_TT;y+=2*wj)
+ for(x=y-wj; x < y; x++)
+ {
+ temp = f[x+wj];
+ f[x+wj] = ((f[x+wj])&(mask[i])) + (((f[x]) & (mask[i])) >> forShift);
+ f[x] = ((f[x])&(~mask[i])) + ((temp&(~mask[i])) << forShift);
+ }
+}
+
+void swap_ij_case3( word* f,int totalVars, int i, int j)
+{
+ int x,y,wwi,wwj,shift;
+ int WORDS_IN_TT;
+ int SizeOfBlock;
+ word* temp;
+ wwi = 1 << (i - 5);
+ wwj = 1 << (j - 5);
+ shift = (wwj - wwi)/2;
+ WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
+ SizeOfBlock = sizeof(word)*wwi/2;
+ temp = malloc(SizeOfBlock);
+ for(y=wwj/2; y<WORDS_IN_TT; y+=wwj)
+ for(x=y-shift; x<y; x+=wwi)
+ {
+ memcpy(temp,&f[x],SizeOfBlock);
+ memcpy(&f[x],&f[x+shift],SizeOfBlock);
+ memcpy(&f[x+shift],temp,SizeOfBlock);
+ }
+}
+void swap_ij( word* f,int totalVars, int varI, int varJ)
+{
+ if (varI == varJ)
+ return;
+ else if(varI>varJ)
+ swap_ij( f,totalVars,varJ,varI);
+ else if((varI <= 4) && (varJ <= 5))
+ swap_ij_case1(f,totalVars, varI, varJ);
+ else if((varI <= 5) && (varJ > 5))
+ swap_ij_case2(f,totalVars, varI, varJ);
+ else if((varI > 5) && (varJ > 5))
+ swap_ij_case3(f,totalVars,varI,varJ);
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/bool/lucky/module.make b/src/bool/lucky/module.make
index 70fa67f3..dad5ee61 100644
--- a/src/bool/lucky/module.make
+++ b/src/bool/lucky/module.make
@@ -1,3 +1,6 @@
SRC += src/bool/lucky/lucky.c \
+ src/bool/lucky/luckyFast16.c \
+ src/bool/lucky/luckyFast6.c \
src/bool/lucky/luckyRead.c \
+ src/bool/lucky/luckySwapIJ.c \
src/bool/lucky/luckySwap.c
diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c
index cc1a06f3..1abf5fca 100644
--- a/src/map/if/ifDec16.c
+++ b/src/map/if/ifDec16.c
@@ -1585,7 +1585,7 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int iVarStart, in
short pStore[32];
unsigned uCanonPhase;
If_CluCopy( pF, pTruth, nVars );
- uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm, pStore );
+ uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm );
G1.nVars = 1;
return G1;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 01:08:08 +0000