Version abc70703

3 files changed, 481 insertions, 12 deletions

diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 4535244b..a0552b19 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -120,6 +120,7 @@ struct Kit_DsdNtk_t_
     unsigned char  nNodes;          // the number of nodes
     unsigned char  Root;            // the root of the tree
     unsigned *     pMem;            // memory for the truth tables (memory manager?)
+    unsigned *     pSupps;          // supports of the nodes
     Kit_DsdObj_t * pNodes[0];       // the nodes
 };
 
@@ -142,8 +143,10 @@ static inline int             Kit_DsdLitRegular( int Lit )           { return Li
  
 static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
 static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
-static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )  { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
-static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )  { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );   }
+static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )      { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
+static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )             { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );                      }
+static inline int             Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit )   { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
+static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )  { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return pNtk->pSupps? (Id < pNtk->nVars? (1 << Id) : pNtk->pSupps[Id - pNtk->nVars]) : 0; }
 
 #define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
     for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
@@ -398,6 +401,12 @@ static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned
             pOut[w] = pIn0[w] & pIn1[w];
     }
 }
+static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars )
+{
+    int w;
+    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                           ITERATORS                              ///
@@ -428,6 +437,11 @@ extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
 extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
 extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
+extern void            Kit_DsdGetSupports( Kit_DsdNtk_t * p );
+extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
+extern Kit_DsdNtk_t *  Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
+extern void            Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] );
+extern int             Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose );
 /*=== kitFactor.c ==========================================================*/
 extern Kit_Graph_t *   Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
 /*=== kitGraph.c ==========================================================*/
@@ -478,7 +492,7 @@ extern void            Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
 extern void            Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
 extern void            Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
 extern void            Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
-extern void            Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
+extern void            Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern void            Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 4bf8d7ef..8dd1b06f 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -153,6 +153,7 @@ void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
     unsigned i;
     Kit_DsdNtkForEachObj( pNtk, pObj, i )
         free( pObj );
+    FREE( pNtk->pSupps );
     free( pNtk->pMem );
     free( pNtk );
 }
@@ -645,6 +646,296 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Sorts the literals by their support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], int piLitsNew[], int nVars )
+{
+    int nSuppSizes[16], Priority[16], pOrder[16], Temp[16];
+    int i, k, iVarBest, SuppMax, PrioMin;
+    // compute support sizes and priorities of the components
+    for ( i = 0; i < nVars; i++ )
+    {
+        Temp[i] = piLitsNew[i];
+        pOrder[i] = i;
+        Priority[i] = 16;
+        nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
+        for ( k = 0; k < 16; k++ )
+            if ( uSupps[i] & (1 << k) )
+                Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
+        assert( Priority[i] != 16 );
+    }
+    // find the component by with largest size and smallest priority
+    iVarBest = -1;
+    SuppMax = 0;
+    PrioMin = 16;
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMin > Priority[i]) )
+        {
+            SuppMax = nSuppSizes[i];
+            PrioMin = Priority[i];
+            iVarBest = i;
+        }
+    }
+    // sort the components by pririty
+    Extra_BubbleSort( pOrder, Priority, nVars, 1 );
+    // copy the resulting literals
+    k = 0;
+    piLitsNew[k++] = piLitsNew[iVarBest];
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( pOrder[i] == iVarBest )
+            continue;
+        piLitsNew[k++] = piLitsNew[pOrder[i]];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Shrinks multi-input nodes.]
+
+  Description [Takes the array of variable priorities pPrios.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPrios[] )
+{
+    Kit_DsdObj_t * pObj, * pObjNew;
+    unsigned * pTruth, * pTruthNew;
+    unsigned i, piLitsNew[16], uSupps[16];
+    int fCompl, iLitFanin, iLitNew;
+
+    // remember the complement
+    fCompl = Kit_DsdLitIsCompl(iLit); 
+    iLit = Kit_DsdLitRegular(iLit); 
+    assert( !Kit_DsdLitIsCompl(iLit) );
+
+    // consider the case of simple gate
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+        return Kit_DsdLitNotCond( iLit, fCompl );
+    if ( pObj->Type == KIT_DSD_AND )
+    {
+        if ( pObj->nFans == 2 )
+        {
+            pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
+            pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
+            pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
+        }
+        else
+        {
+            // get the supports
+            Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+            {
+                piLitsNew[i] = iLitFanin;
+                uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
+            }
+            // put the largest component first
+            // sort other components in the increasing order of the highest variable
+            Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
+            iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
+            for ( i = 1; i < pObj->nFans; i++ )
+            {
+                pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
+                pObjNew->pFans[0] = iLitNew;
+                pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
+                iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
+            }
+        }
+        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+    }
+    if ( pObj->Type == KIT_DSD_XOR )
+    {
+        if ( pObj->nFans == 2 )
+        {
+            pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
+            pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
+            pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
+        }
+        else
+        {
+            // get the supports
+            Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+            {
+                piLitsNew[i] = iLitFanin;
+                uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
+            }
+            // put the largest component first
+            // sort other components in the increasing order of the highest variable
+            Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
+            iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
+            for ( i = 1; i < pObj->nFans; i++ )
+            {
+                pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
+                pObjNew->pFans[0] = iLitNew;
+                pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
+                iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
+            }
+        }
+        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+
+    // create new PRIME node
+    pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
+    // copy the truth table
+    pTruth = Kit_DsdObjTruth( pObj );
+    pTruthNew = Kit_DsdObjTruth( pObjNew );
+    Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
+    // create fanins
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
+    {
+        pObjNew->pFans[i] = Kit_DsdShrink_rec( pNew, p, iLitFanin, pPrios );
+        // complement the corresponding inputs of the truth table
+        if ( Kit_DsdLitIsCompl(pObjNew->pFans[i]) )
+        {
+            pObjNew->pFans[i] = Kit_DsdLitRegular(pObjNew->pFans[i]);
+            Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
+        }
+    }
+    // if the incoming phase is complemented, absorb it into the prime node
+    if ( fCompl )
+        Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
+    return Kit_DsdVar2Lit( pObjNew->Id, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Shrinks the network.]
+
+  Description [Transforms the network to have two-input nodes so that the
+  higher-ordered nodes were decomposed out first.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] )
+{
+    Kit_DsdNtk_t * pNew;
+    Kit_DsdObj_t * pObjNew;
+    assert( p->nVars <= 16 );
+    // create a new network
+    pNew = Kit_DsdNtkAlloc( p->nVars );
+    // consider simple special cases
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
+    {
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
+        pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
+        return pNew;
+    }
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
+    {
+        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
+        pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
+        pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
+        return pNew;
+    }
+    // convert the root node
+    pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Rotates the network.]
+
+  Description [Transforms prime nodes to have the fanin with the
+  highest frequency of supports go first.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned * pIn, * pOut, * pTemp, k;
+    int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps;
+    int Weights[16];
+    // go through the prime nodes
+    Kit_DsdNtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type != KIT_DSD_PRIME )
+            continue;
+        // count the fanin frequencies
+        Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
+        {
+            uSuppFanin = Kit_DsdLitSupport( p, iFaninLit );
+            Weights[k] = 0;
+            for ( v = 0; v < 16; v++ )
+                if ( uSuppFanin & (1 << v) )
+                    Weights[k] += pFreqs[v];
+        }
+        // find the most frequent fanin
+        WeightMax = FaninMax = 0;
+        for ( k = 0; k < pObj->nFans; k++ )
+            if ( WeightMax < Weights[k] )
+            {
+                WeightMax = Weights[k];
+                FaninMax = k;
+            }
+        assert( k < pObj->nFans );
+        // move the fanins number k to the first place
+        nSwaps = 0;
+        pIn = Kit_DsdObjTruth(pObj);
+        pOut = p->pSupps;
+        for ( v = k-1; v >= 0; v-- )
+        {
+            // swap the fanins
+            Temp = pObj->pFans[v];
+            pObj->pFans[v] = pObj->pFans[v+1];
+            pObj->pFans[v+1] = Temp;
+            // swap the truth table variables
+            Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v );
+            pTemp = pIn; pIn = pOut; pOut = pTemp;
+            nSwaps++;
+        }
+        if ( nSwaps & 1)
+            Kit_TruthCopy( pIn, pOut, pObj->nFans );
+    }    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned uSupport, k;
+    int iFaninLit, i;
+    p->pSupps = ALLOC( unsigned, p->nNodes );
+    Kit_DsdNtkForEachObj( p, pObj, i )
+    {
+        uSupport = 0;
+        Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
+            uSupport |= Kit_DsdLitSupport( p, iFaninLit );
+        p->pSupps[pObj->Id - p->nVars] = uSupport;
+    }    
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if there is a component with more than 3 inputs.]
 
   Description []
@@ -926,10 +1217,10 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
                 pRes->pFans[2] = pObj->pFans[i];     pObj->pFans[i] = 2 * pRes->Id; // remains in support
                 // update the node
 //                if ( fEquals[0][0] && fEquals[0][1] )
-//                    Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
+//                    Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
 //                else
-//                    Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
-                Kit_TruthMux( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
+//                    Kit_TruthMuxVar( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
+                Kit_TruthMuxVar( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i );
                 if ( fEquals[1][0] && fEquals[1][1] )
                     pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
                 // decompose the remainder
@@ -967,17 +1258,17 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
             {
                 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);  
                 pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);
-                Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
+                Kit_TruthMuxVar( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
             }
             else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
             {
                 pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]);  
-                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
+                Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
             }
             else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
             {
                 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);  
-                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
+                Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
             }
             else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
             {
@@ -986,7 +1277,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
 //                unsigned uSupp;
 //                Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" );
 //                Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" );
-                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
+                Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
 //                uSupp = Kit_TruthSupport(pTruth, pObj->nFans);
 //                Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" );
             }
@@ -994,7 +1285,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
             {
                 assert( fPairs[0][3] && fPairs[1][2] );
                 pRes->Type = KIT_DSD_XOR;;
-                Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
+                Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
             }
             // decompose the remainder
             Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
@@ -1317,6 +1608,170 @@ void Kit_DsdPrecompute4Vars()
     printf( "non-DSD = %d   implementable = %d\n", Counter1, Counter2 );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of cofactoring variables.]
+
+  Description [If there is no DSD components returns 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCofactoringGetVars( Kit_DsdNtk_t ** ppNtk, int nSize, int * pVars )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned m;
+    int i, k, v, Var, nVars, iFaninLit;
+    // go through all the networks
+    nVars = 0;
+    for ( i = 0; i < nSize; i++ )
+    {
+        // go through the prime objects of each networks
+        Kit_DsdNtkForEachObj( ppNtk[i], pObj, k )     
+        {
+            if ( pObj->Type != KIT_DSD_PRIME )
+                continue;
+            if ( pObj->nFans == 3 )
+                continue;
+            // collect direct fanin variables
+            Kit_DsdObjForEachFanin( ppNtk[i], pObj, iFaninLit, m )
+            {
+                if ( !Kit_DsdLitIsLeaf(ppNtk[i], iFaninLit) )
+                    continue;
+                // add it to the array
+                Var = Kit_DsdLit2Var( iFaninLit );
+                for ( v = 0; v < nVars; v++ )
+                    if ( pVars[v] == Var )
+                        break;
+                if ( v == nVars )
+                    pVars[nVars++] = Var;
+            }
+        }
+    }
+    return nVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Canonical decomposition into completely DSD-structure.]
+
+  Description [Returns the number of cofactoring steps. Also returns
+  the cofactoring variables in pVars.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose )
+{
+    Kit_DsdNtk_t * ppNtks[5][16] = {0}, * pTemp;
+    unsigned * ppCofs[5][16];
+    int pTryVars[16], nTryVars;
+    int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
+    int nSuppSizeMin, nSuppSizeMax, iVarBest;
+    int i, k, v, nStep, nSize, nMemSize;
+    assert( nLimit < 5 );
+
+    // allocate storage for cofactors
+    nMemSize = Kit_TruthWordNum(nVars);
+    ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize );
+    nSize = 0;
+    for ( i = 0; i <  5; i++ )
+    for ( k = 0; k < 16; k++ )
+        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+    assert( nSize == 80 );
+
+    // copy the function
+    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+    ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );
+
+    if ( fVerbose )
+        printf( "\nProcessing prime function with %d support variables:\n", nVars );
+
+    // perform recursive cofactoring
+    for ( nStep = 0; nStep < nLimit; nStep++ )
+    {
+        nSize = (1 << nStep);
+        // find the variables to use in the cofactoring step
+        nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
+        if ( nTryVars == 0 )
+            break;
+        // cofactor w.r.t. the above variables
+        iVarBest = -1;
+        nPrimeSizeMin = 10000;
+        nSuppSizeMin  = 10000;
+        for ( v = 0; v < nTryVars; v++ )
+        {
+            nPrimeSizeMax = 0;
+            nSuppSizeMax = 0;
+            for ( i = 0; i < nSize; i++ )
+            {
+                // cofactor and decompose cofactors          
+                Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
+                Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
+                ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
+                ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
+                // compute the largest non-decomp block
+                nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
+                nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+                nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
+                nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+                // compute the sum total of supports
+                nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
+                nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
+                // free the networks
+                Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
+                Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
+            }
+            // find the min max support size of the prime component
+            if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
+            {
+                nPrimeSizeMin = nPrimeSizeMax;
+                nSuppSizeMin  = nSuppSizeMax;
+                iVarBest      = pTryVars[v];
+            }
+        }
+        assert( iVarBest != -1 );
+        // save the variable
+        if ( pCofVars )
+            pCofVars[nStep] = iVarBest;
+        // cofactor w.r.t. the best
+        for ( i = 0; i < nSize; i++ )
+        {
+            Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
+            Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
+            ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
+            ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
+            if ( fVerbose )
+            {
+                ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
+                Kit_DsdNtkFree( pTemp );
+                ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
+                Kit_DsdNtkFree( pTemp );
+
+                printf( "Cof%d%d: ", nStep+1, 2*i+0 );
+                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] );
+                printf( "Cof%d%d: ", nStep+1, 2*i+1 );
+                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] );
+            }
+        }
+    }
+
+    // free the networks
+    for ( i = 0; i <  5; i++ )
+    for ( k = 0; k < 16; k++ )
+        if ( ppNtks[i][k] )
+            Kit_DsdNtkFree( ppNtks[i][k] );
+    free( ppCofs[0][0] );
+
+    assert( nStep <= nLimit );
+    return nStep;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 73264661..dbf222c2 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -854,7 +854,7 @@ void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
+void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
 {
     int nWords = Kit_TruthWordNum( nVars );
     int i, k, Step;