summaryrefslogtreecommitdiffstats
path: root/src/bool/lucky
diff options
context:
space:
mode:
Diffstat (limited to 'src/bool/lucky')
-rw-r--r--src/bool/lucky/lucky.h19
-rw-r--r--src/bool/lucky/luckyFast16.c219
-rw-r--r--src/bool/lucky/luckyFast6.c156
-rw-r--r--src/bool/lucky/luckyInt.h7
-rw-r--r--src/bool/lucky/luckySimple.c183
-rw-r--r--src/bool/lucky/luckySwap.c14
-rw-r--r--src/bool/lucky/module.make1
7 files changed, 521 insertions, 78 deletions
diff --git a/src/bool/lucky/lucky.h b/src/bool/lucky/lucky.h
index 0a055b40..fac24aeb 100644
--- a/src/bool/lucky/lucky.h
+++ b/src/bool/lucky/lucky.h
@@ -20,9 +20,24 @@
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 int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
-extern void resetPCanonPermArray(char* x, int nVars);
+extern unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm );
+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
diff --git a/src/bool/lucky/luckyFast16.c b/src/bool/lucky/luckyFast16.c
index ebeeab1b..83a64b11 100644
--- a/src/bool/lucky/luckyFast16.c
+++ b/src/bool/lucky/luckyFast16.c
@@ -15,7 +15,7 @@
***********************************************************************/
#include "luckyInt.h"
-
+//#define LUCKY_VERIFY
ABC_NAMESPACE_IMPL_START
@@ -27,6 +27,48 @@ static word SFmask[5][4] = {
{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/////////////////////////////////////////////////////////////////////////////////////////////
// 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/////////////////////////////////////////////////////////////////////////////////////////////
// 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/////////////////////////////////////////////////////////////////////////////////////////////
// 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 /////////////////////////////////////////////////////////////////////////////////////////////
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;
}
-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)
+{
+ 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_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)
{
- minimalInitialFlip_fast_16Vars(pInOut, nVars, pCanonPhase);
- while( minimalSwapAndFlipIVar_superFast_all(pInOut, nVars, nWords, pStore, pCanonPerm, pCanonPhase) != 0)
- continue;
+ 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 luckyCanonicizer_final_fast_16Vars(word* pInOut, int nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase)
+inline void luckyCanonicizerS_F_first_16Vars11(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));
+ 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)
+{
assert( nVars > 6 && nVars <= 16 );
(* 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 );
+}
+
+void bitReverceOrder(word* x, int nVars)
+{
+ int i;
+ for(i= nVars-1;i>=0;i--)
+ Kit_TruthChangePhase_64bit( x, nVars, i );
+}
+
-// memcpy(pDuplicate,pInOut,nWords*sizeof(word));
-// assert(!luckyCheck(pDuplicate, pDuplicateLocal, nVars, pCanonPerm, * pCanonPhase));
+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)
-int luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
+unsigned luckyCanonicizer_final_fast( word * pInOut, int nVars, char * pCanonPerm )
{
+ int nWords;
int pStore[16];
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 )
- 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 )
+ {
+ nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
luckyCanonicizer_final_fast_16Vars( 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;
+}
+
+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;
}
@@ -627,4 +815,3 @@ ABC_NAMESPACE_IMPL_END
-
diff --git a/src/bool/lucky/luckyFast6.c b/src/bool/lucky/luckyFast6.c
index 086a9bc6..bfc555aa 100644
--- a/src/bool/lucky/luckyFast6.c
+++ b/src/bool/lucky/luckyFast6.c
@@ -34,47 +34,7 @@ inline void resetPCanonPermArray(char* x, int nVars)
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)
{
@@ -194,13 +154,29 @@ inline word Extra_Truth6MinimumRoundOne( word t, int iVar, char* pCanonPerm, uns
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
//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);
+ word tMin0, tMin=t;
do
{
bitInfoTemp = pStore[0];
@@ -211,23 +187,99 @@ inline word Extra_Truth6MinimumRoundMany( word t, int* pStore, char* pCanonPerm,
tMin = Extra_Truth6MinimumRoundOne( tMin, i, pCanonPerm, pCanonPhase );
else
bitInfoTemp = pStore[i+1];
+ }
+ }while ( tMin0 != tMin );
+ return tMin;
+}
+
+inline word Extra_Truth6MinimumRoundMany_noEBFC( word t, int* pStore, char* pCanonPerm, unsigned* pCanonPhase )
+{
+ int i, bitInfoTemp;
+ word tMin0, tMin=t;
+ do
+ {
+ bitInfoTemp = pStore[0];
+ tMin0 = tMin;
+ 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 )
+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 );
-
+ 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
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 2e476f86..4801b961 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -41,6 +41,7 @@ typedef unsigned __int64 word;
#define true 1
#define inline __inline // compatible with MS VS 6.0
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
+// #define LUCKY_VERIFY
#endif
@@ -118,9 +119,9 @@ extern permInfo* setPermInfoPtr(int var);
extern void freePermInfoPtr(permInfo* x);
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 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_6Vars1(word InOut, 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);
diff --git a/src/bool/lucky/luckySimple.c b/src/bool/lucky/luckySimple.c
new file mode 100644
index 00000000..52e5e13d
--- /dev/null
+++ b/src/bool/lucky/luckySimple.c
@@ -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
diff --git a/src/bool/lucky/luckySwap.c b/src/bool/lucky/luckySwap.c
index 13bb489e..e4065db6 100644
--- a/src/bool/lucky/luckySwap.c
+++ b/src/bool/lucky/luckySwap.c
@@ -241,6 +241,7 @@ 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 );
@@ -250,8 +251,8 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
assert( nVars <= 16 );
nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
- // if ( (nOnes == nWords * 32) )
- // return 999999;
+ if ( nOnes == nWords * 32 )
+ uCanonPhase |= (1 << (nVars+2));
if ( (nOnes > nWords * 32) )
{
@@ -266,9 +267,12 @@ inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char *
// canonicize phase
for ( i = 0; i < nVars; i++ )
{
- // if ( pStore[i] == nOnes-pStore[i])
- // return 999999;
- if ( pStore[i] >= nOnes-pStore[i])
+ if ( 2*pStore[i] == nOnes)
+ {
+ uCanonPhase |= (1 << (nVars+1));
+ continue;
+ }
+ if ( pStore[i] > nOnes-pStore[i])
continue;
uCanonPhase |= (1 << i);
pStore[i] = nOnes-pStore[i];
diff --git a/src/bool/lucky/module.make b/src/bool/lucky/module.make
index dad5ee61..a65f61df 100644
--- a/src/bool/lucky/module.make
+++ b/src/bool/lucky/module.make
@@ -2,5 +2,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/luckySimple.c \
src/bool/lucky/luckySwapIJ.c \
src/bool/lucky/luckySwap.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 16:37:49 +0000