Improvements to the truth table computation in 'if' package.

2 files changed, 442 insertions, 4 deletions

diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 8ec4a513..6bfb5699 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -115,7 +115,7 @@ static inline int Abc_TtSuppIsMinBase( int Supp )
 }
 static inline int Abc_Tt6HasVar( word t, int iVar )
 {
-    return (t & ~s_Truths6[iVar]) != ((t & s_Truths6[iVar]) >> (1<<iVar));
+    return ((t << (1<<iVar)) & s_Truths6[iVar]) != (t & s_Truths6[iVar]);
 }
 static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
 {
@@ -125,14 +125,15 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
     {
         int i, Shift = (1 << iVar);
         for ( i = 0; i < nWords; i++ )
-            if ( (t[i] & ~s_Truths6[iVar]) != ((t[i] & s_Truths6[iVar]) >> Shift) )
+            if ( ((t[i] << Shift) & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
                 return 1;
         return 0;
     }
     else
     {
-        int i, k, Step = (1 << (iVar - 6));
-        for ( k = 0; k < nWords; k += 2*Step, t += 2*Step )
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
             for ( i = 0; i < Step; i++ )
                 if ( t[i] != t[Step+i] )
                     return 1;
@@ -189,6 +190,103 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
 ***********************************************************************/
 static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
 {
+    static word PPMasks[5][6][3] = {
+        { 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 0 0  
+            { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, // 0 1  
+            { 0xA5A5A5A5A5A5A5A5, 0x0A0A0A0A0A0A0A0A, 0x5050505050505050 }, // 0 2 
+            { 0xAA55AA55AA55AA55, 0x00AA00AA00AA00AA, 0x5500550055005500 }, // 0 3 
+            { 0xAAAA5555AAAA5555, 0x0000AAAA0000AAAA, 0x5555000055550000 }, // 0 4 
+            { 0xAAAAAAAA55555555, 0x00000000AAAAAAAA, 0x5555555500000000 }  // 0 5 
+        },
+        { 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 0  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 1 1  
+            { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, // 1 2 
+            { 0xCC33CC33CC33CC33, 0x00CC00CC00CC00CC, 0x3300330033003300 }, // 1 3 
+            { 0xCCCC3333CCCC3333, 0x0000CCCC0000CCCC, 0x3333000033330000 }, // 1 4 
+            { 0xCCCCCCCC33333333, 0x00000000CCCCCCCC, 0x3333333300000000 }  // 1 5 
+        },
+        { 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 0  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 1  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 2 2 
+            { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, // 2 3 
+            { 0xF0F00F0FF0F00F0F, 0x0000F0F00000F0F0, 0x0F0F00000F0F0000 }, // 2 4 
+            { 0xF0F0F0F00F0F0F0F, 0x00000000F0F0F0F0, 0x0F0F0F0F00000000 }  // 2 5 
+        },
+        { 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 0  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 1  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 2 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 3 3 
+            { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, // 3 4 
+            { 0xFF00FF0000FF00FF, 0x00000000FF00FF00, 0x00FF00FF00000000 }  // 3 5 
+        },
+        { 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 0  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 1  
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 2 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 3 
+            { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000 }, // 4 4 
+            { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 }  // 4 5 
+        }
+    };
+    if ( iVar == jVar )
+        return;
+    if ( jVar < iVar )
+        ABC_SWAP( int, iVar, jVar );
+    assert( iVar < jVar && jVar < nVars );
+    if ( nVars <= 6 )
+    {
+        word * pMasks = PPMasks[iVar][jVar];
+        int shift = (1 << jVar) - (1 << iVar);
+        pTruth[0] = (pTruth[0] & pMasks[0]) | ((pTruth[0] & pMasks[1]) << shift) | ((pTruth[0] & pMasks[2]) >> shift);
+    }
+    else
+    {
+        if ( jVar <= 5 )
+        {
+            word * pMasks = PPMasks[iVar][jVar];
+            int nWords = Abc_TtWordNum(nVars);
+            int w, shift = (1 << jVar) - (1 << iVar);
+            for ( w = 0; w < nWords; w++ )
+                pTruth[w] = (pTruth[w] & pMasks[0]) | ((pTruth[w] & pMasks[1]) << shift) | ((pTruth[w] & pMasks[2]) >> shift);
+        }
+        else if ( iVar <= 5 && jVar > 5 )
+        {
+            word low2High, high2Low;
+            word * pLimit = pTruth + Abc_TtWordNum(nVars);
+            int j, jStep = Abc_TtWordNum(jVar);
+            int shift = 1 << iVar;
+            for ( ; pTruth < pLimit; pTruth += 2*jStep )
+                for ( j = 0; j < jStep; j++ )
+                {
+                    low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
+                    high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
+                    pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
+                    pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
+                }
+        }
+        else
+        {
+            word temp, * pLimit = pTruth + Abc_TtWordNum(nVars);
+            int i, iStep = Abc_TtWordNum(iVar);
+            int j, jStep = Abc_TtWordNum(jVar);
+            for ( ; pTruth < pLimit; pTruth += 2*jStep )
+                for ( i = 0; i < jStep; i += 2*iStep )
+                    for ( j = 0; j < iStep; j++ )
+                    {
+                        temp = pTruth[iStep + i + j];
+                        pTruth[iStep + i + j] = pTruth[jStep + i + j];
+                        pTruth[jStep + i + j] = temp;
+                    }
+        }    
+    }
+}
+
+static inline void Abc_TtSwapVars_( word * pTruth, int nVars, int iVar, int jVar )
+{
     static word PPMasks[6][6] = {
         { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA },
         { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC },
@@ -269,6 +367,7 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
 }
 
 
+
 /**Function*************************************************************
 
   Synopsis    [Stretch truthtable to have more input variables.]
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index 262314d8..f6367304 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "dauInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -463,6 +464,344 @@ void Dau_DsdTestOne( word t, int i )
     Dau_DsdTestOne( *p->pFuncs[i], i );
 */
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0        ) return 0; return 1; }
+static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
+
+static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( t[i] & ~s_Truths6[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( (t[i] & ~s_Truths6[iVar]) != ~s_Truths6[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != ~(word)0 )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( t[i] & s_Truths6[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i+Step] )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i;
+        for ( i = 0; i < nWords; i++ )
+            if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i+Step] != ~(word)0 )
+                    return 0;
+        return 1;
+    }
+}
+static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar ) 
+{ 
+    if ( iVar < 6 )
+    {
+        int i, Shift = (1 << iVar);
+        for ( i = 0; i < nWords; i++ )
+            if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
+                return 0;
+        return 1;
+    }
+    else
+    {
+        int i, Step = (1 << (iVar - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != ~t[i+Step] )
+                    return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_TtCof0HasVar( word * t, int nWords, int iVarI, int iVarJ ) 
+{
+    assert( iVarI > iVarJ );
+    if ( iVarI < 6 )
+    {
+        int i, Shift = (1 << iVarJ);
+        for ( i = 0; i < nWords; i++ )
+            if ( (((t[i] & ~s_Truths6[iVarI]) << Shift) & s_Truths6[iVarJ]) != ((t[i] & ~s_Truths6[iVarI]) & s_Truths6[iVarJ]) )
+                return 0;
+        return 1;
+    }
+    else if ( iVarI == 6 )
+    {
+    }
+    else
+    {
+        int i, Step = (1 << (iVarJ - 6));
+        word * tLimit = t + nWords;
+        for ( ; t < tLimit; t += 2*Step )
+            for ( i = 0; i < Step; i++ )
+                if ( t[i] != t[i+Step] )
+                    return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DsdMinimize( word * p, int * pVars, int nVars )
+{
+    int i, k;
+    assert( nVars > 6 );
+    for ( i = k = nVars - 1; i >= 0; i-- )
+    {
+        if ( Abc_TtHasVar( p, nVars, i ) )
+            continue;
+        if ( i < k )
+        {
+            pVars[i] = pVars[k];
+            Abc_TtSwapVars( p, nVars, i, k );
+        }
+        k--;
+        nVars--;
+    }
+    return nVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DsdRun6_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dau_DsdRun_rec( word * p, int * pVars, int nVars, char * pBuffer, int Pos, char pStore[16][16], int Func )
+{
+    int v, nWords = Abc_TtWordNum( nVars );
+    nVars = Dau_DsdMinimize( p, pVars, nVars );
+    if ( nVars <= 6 )
+        return Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
+    if ( p[0] & 1 )
+    {
+        // check for !(ax)
+        for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtCof0IsConst0( p, nWords, v ) )
+        {
+            pBuffer[Pos++] = '(';
+            pBuffer[Pos++] = 'a' + pVars[v];
+            Abc_TtSwapVars( p, nVars, v, nVars - 1 );
+            pVars[v] = pVars[nVars-1];
+            Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func );
+            pBuffer[Pos++] = ')';
+            return Pos;
+        }
+    }
+    else
+    {
+        // check for ax
+        for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtCof0IsConst1( p, nWords, v ) )
+        {
+            pBuffer[Pos++] = '!';
+            pBuffer[Pos++] = '(';
+            pBuffer[Pos++] = 'a' + pVars[v];
+            Abc_TtSwapVars( p, nVars, v, nVars - 1 );
+            pVars[v] = pVars[nVars-1];
+            Pos = Dau_DsdRun_rec( p + nWords/2, pVars, nVars-1, pBuffer, Pos, pStore, Func );
+            pBuffer[Pos++] = ')';
+            return Pos;
+        }
+    }
+    if ( (p[nWords-1] >> 63) & 1 )
+    {
+        // check for !(!ax)
+        for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtCof0IsConst1( p, nWords, v ) )
+        {
+            pBuffer[Pos++] = '!';
+            pBuffer[Pos++] = '(';
+            pBuffer[Pos++] = '!';
+            pBuffer[Pos++] = 'a' + pVars[v];
+            Abc_TtSwapVars( p, nVars, v, nVars - 1 );
+            pVars[v] = pVars[nVars-1];
+            Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
+            pBuffer[Pos++] = ')';
+            return Pos;
+        }
+    }
+    else
+    {
+        // check for !ax
+        for ( v = 0; v < nVars; v++ )
+        if ( Abc_TtCof1IsConst0( p, nWords, v ) )
+        {
+            pBuffer[Pos++] = '(';
+            pBuffer[Pos++] = '!';
+            pBuffer[Pos++] = 'a' + pVars[v];
+            Abc_TtSwapVars( p, nVars, v, nVars - 1 );
+            pVars[v] = pVars[nVars-1];
+            Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
+            pBuffer[Pos++] = ')';
+            return Pos;
+        }
+    }
+    // check for a^x
+    for ( v = 0; v < nVars; v++ )
+    if ( Abc_TtCofsOpposite( p, nWords, v ) )
+    {
+        pBuffer[Pos++] = '[';
+        pBuffer[Pos++] = 'a' + pVars[v];
+        Abc_TtSwapVars( p, nVars, v, nVars - 1 );
+        pVars[v] = pVars[nVars-1];
+        Pos = Dau_DsdRun_rec( p, pVars, nVars-1, pBuffer, Pos, pStore, Func );
+        pBuffer[Pos++] = ']';
+        return Pos;
+    }
+
+    return 0;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Dau_DsdRun( word * p, int nVars )
+{
+    static char pBuffer[DAU_MAX_STR+20];
+    static char pStore[16][16];
+    int nWords = Abc_TtWordNum( nVars );
+    int i, Pos = 0, Func = 0, pVars[16];
+    assert( nVars <= 16 );
+    for ( i = 0; i < nVars; i++ )
+        pVars[i] = i;
+    if ( Abc_TtTruthIsConst0( p, nWords ) )
+        pBuffer[Pos++] = '0';
+    else if ( Abc_TtTruthIsConst1( p, nWords ) )
+        pBuffer[Pos++] = '1';
+    else if ( nVars <= 6 )
+        Pos = Dau_DsdRun6_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
+    else
+        Pos = Dau_DsdRun_rec( p, pVars, nVars, pBuffer, Pos, pStore, Func );
+    pBuffer[Pos++] = 0;
+    Dau_DsdCleanBraces( pBuffer );
+    return pBuffer;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////