Improved DSD.

2 files changed, 253 insertions, 41 deletions

diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 486cbf48..f6476724 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -172,6 +172,17 @@ static inline int Abc_TtIsConst1( word * pIn1, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
+static inline word Abc_Tt6Cofactor0( word t, int iVar )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
+}
+static inline word Abc_Tt6Cofactor1( word t, int iVar )
+{
+    assert( iVar >= 0 && iVar < 6 );
+    return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
+}
+
 static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
 {
     if ( nWords == 1 )
@@ -289,18 +300,10 @@ static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths
 static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar];                         }
 static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0;                                             }
 static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar];                               }
-static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return ((t >> (1 << iVar)) & s_Truths6Neg[iVar]) == (~t & s_Truths6Neg[iVar]); } 
-
-static inline word Abc_Tt6Cofactor0( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
-}
-static inline word Abc_Tt6Cofactor1( word t, int iVar )
-{
-    assert( iVar >= 0 && iVar < 6 );
-    return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
-}
+static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return (~t & s_Truths6Neg[iVar]) == ((t >> (1 << iVar)) & s_Truths6Neg[iVar]); } 
+static inline int Abc_Tt6Cof0EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == ((t2 >> (1 << iVar)) & s_Truths6Neg[iVar]); } 
+static inline int Abc_Tt6Cof0EqualCof0( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == (t2 & s_Truths6Neg[iVar]); } 
+static inline int Abc_Tt6Cof1EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6[iVar])    == (t2 & s_Truths6[iVar]); } 
 
 /**Function*************************************************************
 
@@ -433,13 +436,12 @@ static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Abc_TtPrintDigit( int Digit )
+static inline char Abc_TtPrintDigit( int Digit )
 {
     assert( Digit >= 0 && Digit < 16 );
     if ( Digit < 10 )
-        printf( "%d", Digit );
-    else
-        printf( "%c", 'A' + Digit-10 );
+        return '0' + Digit;;
+    return 'A' + Digit-10;
 }
 static inline void Abc_TtPrintHex( word * pTruth, int nVars )
 {
@@ -448,7 +450,7 @@ static inline void Abc_TtPrintHex( word * pTruth, int nVars )
     assert( nVars >= 2 );
     for ( pThis = pTruth; pThis < pLimit; pThis++ )
         for ( k = 0; k < 16; k++ )
-            Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+            printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
     printf( "\n" );
 }
 static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
@@ -458,7 +460,7 @@ static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
     assert( nVars >= 2 );
     for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
         for ( k = 15; k >= 0; k-- )
-            Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+            printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
     printf( "\n" );
 }
 static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
@@ -468,9 +470,20 @@ static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
     assert( nVars >= 2 );
     for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
         for ( k = 0; k < 16; k++ )
-            Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+            printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
     printf( "\n" );
 }
+static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
+{
+    word * pThis;
+    char * pStrInit = pStr;
+    int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
+    assert( nVars >= 2 );
+    for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
+        for ( k = StartK - 1; k >= 0; k-- )
+            *pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
+    return pStr - pStrInit;
+}
 
 
 /**Function*************************************************************
@@ -531,11 +544,13 @@ static inline int Abc_Tt6HasVar( word t, int iVar )
 }
 static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
 {
-    int nWords = Abc_TtWordNum( nVars );
     assert( iVar < nVars );
+    if ( nVars <= 6 )
+        return Abc_Tt6HasVar( t[0], iVar );
     if ( iVar < 6 )
     {
         int i, Shift = (1 << iVar);
+        int nWords = Abc_TtWordNum( nVars );
         for ( i = 0; i < nWords; i++ )
             if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
                 return 1;
@@ -544,7 +559,7 @@ static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
     else
     {
         int i, Step = (1 << (iVar - 6));
-        word * tLimit = t + nWords;
+        word * tLimit = t + Abc_TtWordNum( nVars );
         for ( ; t < tLimit; t += 2*Step )
             for ( i = 0; i < Step; i++ )
                 if ( t[i] != t[Step+i] )
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index e6981c91..9c764de8 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -711,6 +711,8 @@ struct Dau_Dsd_t_
     char     pVarDefs[32][8];      // variable definitions
     char     pOutput[DAU_MAX_STR]; // output stream
     int      nPos;                 // writing position
+    int      nConsts;              // the number of constant decompositions
+    int      uConstMask;           // constant decomposition mask
 };
 
 /**Function*************************************************************
@@ -742,19 +744,31 @@ void Dua_DsdWriteInv( Dau_Dsd_t * p, int Cond )
     if ( Cond )
         p->pOutput[ p->nPos++ ] = '!';
 }
-void Dua_DsdWriteVar( Dau_Dsd_t * p, int iVar )
+void Dua_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv )
 {
     char * pStr;
+    if ( fInv )
+        p->pOutput[ p->nPos++ ] = '!';
     for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
         if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
-            Dua_DsdWriteVar( p, *pStr - 'a' );
+            Dua_DsdWriteVar( p, *pStr - 'a', 0 );
         else
             p->pOutput[ p->nPos++ ] = *pStr;
 }
 void Dua_DsdWriteStop( Dau_Dsd_t * p )
 {
+    int i;
+    for ( i = 0; i < p->nConsts; i++ )
+        p->pOutput[ p->nPos++ ] = ((p->uConstMask >> i) & 1) ? ']' : ')';
     p->pOutput[ p->nPos++ ] = 0;
 }
+int Dua_DsdAddVarDef( Dau_Dsd_t * p, char * pStr )
+{
+    assert( strlen(pStr) < 8 );
+    assert( p->nVarsUsed < 32 );
+    sprintf( p->pVarDefs[p->nVarsUsed++], "%s", pStr );
+    return p->nVarsUsed - 1;
+}
 
 /**Function*************************************************************
 
@@ -767,18 +781,24 @@ void Dua_DsdWriteStop( Dau_Dsd_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Dua_DsdMinBase( word t, int nVars, int * pVarsNew )
+int Dua_DsdMinBase( word * pTruth, int nVars, int * pVarsNew )
 {
-    int v, nVarsNew = 0;
+    int v;
     for ( v = 0; v < nVars; v++ )
-        if ( Abc_Tt6HasVar( t, v ) )
-            pVarsNew[nVarsNew++] = v;
-    return nVarsNew;
+        pVarsNew[v] = v;
+    for ( v = nVars - 1; v >= 0; v-- )
+    {
+        if ( Abc_TtHasVar( pTruth, nVars, v ) )
+            continue;
+        Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
+        pVarsNew[v] = pVarsNew[--nVars];
+    }
+    return nVars;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns 1 if constant cofactor is found.]
 
   Description []
                
@@ -787,29 +807,206 @@ int Dua_DsdMinBase( word t, int nVars, int * pVarsNew )
   SeeAlso     []
 
 ***********************************************************************/
-void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word t, int * pVars, int nVars )
+int Dau_Dsd6DecomposeConstCofOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
+{
+    int nConstOld = p->nConsts;
+    // consider negative cofactors
+    if ( pTruth[0] & 1 )
+    {        
+        if ( Abc_Tt6Cof0IsConst1( pTruth[0], v ) ) // !(ax)
+        {
+            Dua_DsdWrite( p, "!(" );
+            pTruth[0] = ~Abc_Tt6Cofactor1( pTruth[0], v );
+            p->nConsts++;
+        }
+    }
+    else
+    {
+        if ( Abc_Tt6Cof0IsConst0( pTruth[0], v ) ) // ax
+        {
+            Dua_DsdWrite( p, "(" );
+            pTruth[0] = Abc_Tt6Cofactor1( pTruth[0], v );
+            p->nConsts++;
+        }
+    }
+    // consider positive cofactors
+    if ( pTruth[0] >> 63 )
+    {        
+        if ( Abc_Tt6Cof1IsConst1( pTruth[0], v ) ) // !(!ax)
+        {
+            Dua_DsdWrite( p, "!(!" );
+            pTruth[0] = ~Abc_Tt6Cofactor0( pTruth[0], v );
+            p->nConsts++;
+        }
+    }
+    else
+    {
+        if ( Abc_Tt6Cof1IsConst0( pTruth[0], v ) ) // !ax
+        {
+            Dua_DsdWrite( p, "(!" );
+            pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
+            p->nConsts++;
+        }
+    }
+    // consider equal cofactors
+    if ( Abc_Tt6CofsOpposite( pTruth[0], v ) ) // [ax]
+    {
+        Dua_DsdWrite( p, "[" );
+        pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
+        p->uConstMask |= (1 << p->nConsts++);
+    }
+    if ( nConstOld == p->nConsts )
+        return 0;
+    Dua_DsdWriteVar( p, pVars[v], 0 );
+    pVars[v] = pVars[nVars-1];
+    Abc_TtSwapVars( pTruth, 6, v, nVars-1 );
+    return 1;
+}
+int Dau_Dsd6DecomposeConstCof( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
+{
+    int v;
+    assert( nVars > 1 );
+    for ( v = nVars - 1; v >= 0 && nVars > 1; v++ )
+        if ( Dau_Dsd6DecomposeConstCofOne( p, pTruth, pVars, nVars, v ) )
+            nVars--;
+    if ( nVars == 1 )
+        Dua_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
+    return nVars;
+}
+void Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word t, int * pVars, int nVars )
+{
+    char pBuffer[10];
+    int v, u;
+    nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, nVars );
+    if ( nVars == 0 )
+        return;
+    // consider two-variable cofactors
+    for ( v = nVars - 1; v > 0; v-- )
+    {
+        word tCof0 = Abc_Tt6Cofactor0( t, v );
+        word tCof1 = Abc_Tt6Cofactor1( t, v );
+        unsigned uSupp0 = 0, uSupp1 = 0;
+        for ( u = v - 1; u >= 0; u-- )
+        {
+            if ( Abc_Tt6HasVar(tCof0, u) )
+            {
+                uSupp0 |= (1 << u);
+                if ( Abc_Tt6HasVar(tCof1, u) )
+                {
+                    uSupp1 |= (1 << u);
+                    // both F(v=0) and F(v=1) depend on u
+                    if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) )
+                    {
+                        // perform XOR (u, v)
+                        t = (s_Truths6[u] & tCof1) | (~s_Truths6[u] & tCof0);
+                        sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
+                        break;
+                    }
+                }
+                else
+                {
+                    // F(v=0) does not depend on u; F(v=1) depends on u
+                    if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) )
+                    {
+                        // perform AND (u, v)
+                        break;
+                    }
+                    if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) )
+                    {
+                        // perform AND (u, v)
+                        break;
+                    }
+                }
+            }
+            else if ( Abc_Tt6HasVar(tCof1, u) )
+            {
+                uSupp1 |= (1 << u);
+                // F(v=0) depends on u; F(v=1) does not depend on u
+                if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) )
+                {
+                    // perform AND (u, v)
+                    break;
+                }
+                if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) )
+                {
+                    // perform AND (u, v)
+                    break;
+                }
+            }
+            else assert( 0 ); // should depend on u
+        }
+
+        // check if decomposition happened
+        if ( u >= 0 )
+        {
+            // finalize decomposition
+            pVars[u] = Dua_DsdAddVarDef( p, pBuffer );
+            pVars[v] = pVars[nVars-1];
+            Abc_TtSwapVars( &t, 6, v, nVars-1 );
+            nVars = Dau_Dsd6DecomposeConstCof( p, &t, pVars, --nVars );
+            if ( nVars == 0 )
+                return;
+            continue;
+        }
+
+        // check MUX decomposition w.r.t. u
+        if ( Abc_TtSuppOnlyOne( uSupp0 & ~uSupp1 ) && Abc_TtSuppOnlyOne( ~uSupp0 & uSupp1 ) )
+        {
+            // check MUX 
+            int iVar0 = Abc_TtSuppFindFirst( uSupp0 );
+            int iVar1 = Abc_TtSuppFindFirst( uSupp1 );
+            int fEqual0, fEqual1;
+
+            if ( iVar0 > iVar1 )
+                ABC_SWAP( int, iVar0, iVar1 );
+
+            // check existence conditions
+            assert( iVar0 < iVar1 );
+            fEqual0 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 2 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 3 );
+            fEqual1 = Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 0, 3 ) && Abc_TtCheckEqualCofs( &t, 1, iVar0, iVar1, 1, 2 );
+            if ( fEqual0 || fEqual1 )
+            {
+                // perform MUX( v, F(v=1), F(v=0) )
+                break;
+            }
+        }
+         // check MUX decomposition w.r.t. u
+        if ( (uSupp0 & uSupp1) == 0 )
+        {
+            // perform MUX( v, F(v=1), F(v=0) )
+        }
+    }
+    // this non-DSD-decomposable function
+    assert( nVars > 2 );
+    // write truth table
+    p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, &t, nVars );
+    Dua_DsdWrite( p, "{" );
+    for ( v = 0; v < nVars; v++ )
+        Dua_DsdWriteVar( p, pVars[v], 0 );
+    Dua_DsdWrite( p, "}" );
+}
+void Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
 }
-char * Dau_DsdDecompose( word t, int nVarsInit )
+char * Dau_DsdDecompose( word * pTruth, int nVarsInit )
 {
     Dau_Dsd_t P, * p = &P;
-    int nVars, pVars[6];
+    int nVars, pVars[16];
     Dua_DsdInit( p, nVarsInit );
-    if ( t == 0 )
+    if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
         Dua_DsdWrite( p, "0" );
-    else if ( ~t == 0 )
+    else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
         Dua_DsdWrite( p, "1" );
-    else
+    else 
     {
-        nVars = Dua_DsdMinBase( t, nVarsInit, pVars );
+        nVars = Dua_DsdMinBase( pTruth, nVarsInit, pVars );
         assert( nVars > 0 && nVars < 6 );
         if ( nVars == 1 )
-        {
-            Dua_DsdWriteInv( p, (int)(t & 1) );
-            Dua_DsdWriteVar( p, pVars[0] );
-        }
+            Dua_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) );
+        else if ( nVars <= 6 )
+            Dau_Dsd6DecomposeInternal( p, pTruth[0], pVars, nVars );
         else
-            Dau_DsdDecomposeInternal( p, t, pVars, nVars );
+            Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars );
     }
     Dua_DsdWriteStop( p );
     return p->pOutput;