Integrated new fast semi-canonical form for Boolean functions up to 16 inputs.

1 files changed, 233 insertions, 0 deletions

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