Version abc70831

8 files changed, 1169 insertions, 51 deletions

diff --git a/src/opt/lpk/lpkAbcCore.c b/src/opt/lpk/lpkAbcCore.c
new file mode 100644
index 00000000..53b2668d
--- /dev/null
+++ b/src/opt/lpk/lpkAbcCore.c
@@ -0,0 +1,158 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [The new core procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the function.]
+
+  Description [Returns the node implementing this function.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_FunImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
+{
+    Abc_Obj_t * pObjNew;
+    int i;
+    pObjNew = Abc_NtkCreateNode( pNtk );
+    for ( i = 0; i < (int)p->nVars; i++ )
+        Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) );
+    Abc_ObjLevelNew( pObjNew );
+    // create the logic function
+    {
+        extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+        // allocate memory for the ISOP
+        Vec_Int_t * vCover = Vec_IntAlloc( 0 );
+        // transform truth table into the decomposition tree
+        Kit_Graph_t * pGraph = Kit_TruthToGraph( Lpk_FunTruth(p, 0), p->nVars, vCover );
+        // derive the AIG for the decomposition tree
+        pObjNew->pData = Kit_GraphToHop( pNtk->pManFunc, pGraph );
+        Kit_GraphFree( pGraph );
+        Vec_IntFree( vCover );
+    }
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the function.]
+
+  Description [Returns the node implementing this function.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_LptImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
+{
+    Lpk_Fun_t * pFun;
+    Abc_Obj_t * pRes;
+    int i;
+    for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- )
+    {
+        pFun = Vec_PtrEntry( vLeaves, i );
+        pRes = Lpk_FunImplement( pNtk, vLeaves, pFun );
+        Vec_PtrWriteEntry( vLeaves, i, pRes );
+        Lpk_FunFree( pFun );
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the function using recursive MUX decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_LpkDecompose_rec( Lpk_Fun_t * p )
+{
+    Lpk_Fun_t * p2;
+    int VarPol;
+    assert( p->nAreaLim > 0 );
+    if ( p->nVars <= p->nLutK )
+        return 1;
+    // check if decomposition exists
+    VarPol = Lpk_FunAnalizeMux( p );
+    if ( VarPol == -1 )
+        return 0;
+    // split and call recursively
+    p2 = Lpk_FunSplitMux( p, VarPol );
+    if ( !Lpk_LpkDecompose_rec( p2 ) )
+        return 0;
+    return Lpk_LpkDecompose_rec( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the function using recursive MUX decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
+{
+    Lpk_Fun_t * p;
+    Abc_Obj_t * pObjNew = NULL;
+    int i, nLeaves;
+    // create the starting function
+    nLeaves = Vec_PtrSize( vLeaves );
+    p = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
+    Lpk_FunSuppMinimize( p );
+    // decompose the function 
+    if ( Lpk_LpkDecompose_rec(p) )
+        pObjNew = Lpk_LptImplement( pNtk, vLeaves, nLeaves );
+    else
+    {
+        for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeaves; i-- )
+            Lpk_FunFree( Vec_PtrEntry(vLeaves, i) );
+    }
+    Vec_PtrShrink( vLeaves, nLeaves );
+    return pObjNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
new file mode 100644
index 00000000..893844e0
--- /dev/null
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -0,0 +1,395 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the variable whose cofs have min sum of supp sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
+{
+    int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
+    VarBest = -1;
+    Lpk_SuppForEachVar( p->uSupp, Var )
+    {
+        nSuppMaxCur = 0;
+        nSuppTotalCur = 0;
+        for ( i = 0; i < nTruths; i++ )
+        {
+            Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
+            Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
+            nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
+            nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
+            nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 );
+            nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 );
+            nSuppTotalCur += nSuppSize0 + nSuppSize1;
+        }
+        if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur ||
+             (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) )
+        {
+            VarBest = Var;
+            nSuppMaxMin = nSuppMaxCur;
+            nSuppTotalMin = nSuppTotalCur;
+        }
+    }
+    // recompute cofactors for the best var
+    for ( i = 0; i < nTruths; i++ )
+    {
+        Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest );
+        Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest );
+    }
+    return VarBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes decomposable subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
+{
+    unsigned i, iLitFanin, uSupport, uSuppCur;
+    Kit_DsdObj_t * pObj;
+    // consider the case of simple gate
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+        return (1 << Kit_DsdLit2Var(iLit));
+    if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
+    {
+        unsigned uSupps[16], Limit, s;
+        uSupport = 0;
+        Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+        {
+            uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
+            uSupport |= uSupps[i];
+        }
+        // create all subsets, except empty and full
+        Limit = (1 << pObj->nFans) - 1;
+        for ( s = 1; s < Limit; s++ )
+        {
+            uSuppCur = 0;
+            for ( i = 0; i < pObj->nFans; i++ )
+                if ( s & (1 << i) )
+                    uSuppCur |= uSupps[i];
+            Vec_IntPush( vSets, uSuppCur );
+        }
+        return uSupport;
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+    // get the cumulative support of all fanins
+    uSupport = 0;
+    Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+    {
+        uSuppCur  = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
+        uSupport |= uSuppCur;
+        Vec_IntPush( vSets, uSuppCur );
+    }
+    return uSupport;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of subsets of decomposable variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
+{
+    Vec_Int_t * vSets;
+    unsigned uSupport, Entry;
+    int Number, i;
+    assert( p->nVars <= 16 );
+    vSets = Vec_IntAlloc( 100 );
+    Vec_IntPush( vSets, 0 );
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
+        return vSets;
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
+    {
+        uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
+        Vec_IntPush( vSets, uSupport );
+        return vSets;
+    }
+    uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets );
+    assert( (uSupport & 0xFFFF0000) == 0 );
+    Vec_IntPush( vSets, uSupport );
+    // set the remaining variables
+    Vec_IntForEachEntry( vSets, Number, i )
+    {
+        Entry = Number;
+        Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+    }
+    return vSets;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two bound sets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
+{
+    Vec_Int_t * vSets;
+    int Entry0, Entry1, Entry;
+    int i, k;
+    vSets = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vSets0, Entry0, i )
+    Vec_IntForEachEntry( vSets1, Entry1, k )
+    {
+        Entry = Entry0 | Entry1;
+        if ( (Entry & (Entry >> 16)) )
+            continue;
+        Vec_IntPush( vSets, Entry );
+    }
+    return vSets;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates truth tables for cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+{
+    int i;
+    assert( nCofDepth <= 4 );
+    ppTruths[0][0] = Lpk_FunTruth( p, 0 );
+    if ( nCofDepth >= 1 )
+    {
+        ppTruths[1][0] = Lpk_FunTruth( p, 1 );
+        ppTruths[1][1] = Lpk_FunTruth( p, 2 );
+    }
+    if ( nCofDepth >= 2 )
+    {
+        ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 );
+        for ( i = 1; i < 4; i++ )
+            ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i;
+    }
+    if ( nCofDepth >= 3 )
+    {
+        ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 );
+        for ( i = 1; i < 8; i++ )
+            ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i;
+    }
+    if ( nCofDepth >= 4 )
+    {
+        ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 );
+        for ( i = 1; i < 16; i++ )
+            ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates truth tables for cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+{
+    if ( nCofDepth >= 2 )
+        free( ppTruths[2][0] );
+    if ( nCofDepth >= 3 )
+        free( ppTruths[3][0] );
+    if ( nCofDepth >= 4 )
+        free( ppTruths[4][0] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD-based decomposition of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth )
+{
+    static Lpk_Res_t Res, * pRes = &Res;
+    unsigned * ppTruths[5][16];
+    Vec_Int_t * pvBSets[4][8];
+    Kit_DsdNtk_t * pNtkDec, * pTemp;
+    unsigned uBoundSet;
+    int i, k, nVarsBS, nVarsRem, Delay, Area;
+    Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
+    // find the best cofactors
+    memset( pRes, 0, sizeof(Lpk_Res_t) );
+    pRes->nCofVars = nCofDepth;
+    for ( i = 0; i < nCofDepth; i++ )
+        pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<<i, ppTruths[i+1] );
+    // derive decomposed networks
+    for ( i = 0; i < (1<<nCofDepth); i++ )
+    {
+        pNtkDec = Kit_DsdDecompose( ppTruths[nCofDepth][i], p->nVars );
+        pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
+        pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth );
+        Kit_DsdNtkFree( pNtkDec );
+    }
+    // derive the set of feasible boundsets
+    for ( i = nCofDepth - 1; i >= 0; i-- )
+        for ( k = 0; k < (1<<i); k++ )
+            pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] );
+    // compare the resulting boundsets
+    Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
+    {
+        if ( uBoundSet == 0 )
+            continue;
+        assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
+        nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
+        nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
+        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
+        Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
+        if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim )
+            continue;
+        if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
+        {
+            pRes->nBSVars = nVarsBS;
+            pRes->BSVars = uBoundSet;
+            pRes->nSuppSizeS = nVarsBS;
+            pRes->nSuppSizeL = nVarsRem;
+            pRes->DelayEst = Delay;
+            pRes->AreaEst = Area;
+        }
+    }
+    // free cofactor storage
+    Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits the function into two subfunctions using DSD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
+{
+    Kit_DsdMan_t * pDsdMan;
+    Kit_DsdNtk_t * pNtkDec, * pTemp;
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    Lpk_Fun_t * pNew;
+    unsigned * ppTruths[5][16];
+    char pBSVars[5];
+    int i, k, nVars, nCofs;
+    // get the bound set variables
+    nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
+    // compute the cofactors
+    Lpk_FunAllocTruthTables( p, nCofVars, ppTruths );
+    for ( i = 0; i < nCofVars; i++ )
+        for ( k = 0; k < (1<<i); k++ )
+        {
+            Kit_TruthCofactor0New( ppTruths[i+1][2*k+0], ppTruths[i][k], p->nVars, pCofVars[i] );
+            Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] );
+        }
+    // decompose each cofactor w.r.t. the bound set
+    nCofs = (1<<nCofVars);
+    pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 );
+    for ( k = 0; k < nCofs; k++ )
+    {
+        pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars );
+        pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
+        Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
+        Kit_DsdNtkFree( pNtkDec );
+    }
+    Kit_DsdManFree( pDsdMan );
+    // compute the composition function
+    for ( i = nCofVars - 1; i >= 1; i-- )
+        for ( k = 0; k < (1<<i); k++ )
+            Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] );
+    // now the composition/decomposition functions are in pTruth0/pTruth1
+
+    // derive the new component
+    pNew = Lpk_FunDup( p, pTruth1 );
+    // update the old component
+    Kit_TruthCopy( pTruth, pTruth0, p->nVars );
+    p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
+    p->pFanins[pBSVars[0]] = pNew->Id;
+    p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
+    // support minimize both
+    Lpk_FunSuppMinimize( p );
+    Lpk_FunSuppMinimize( pNew );
+    // update delay and area requirements
+    pNew->nDelayLim = p->nDelayLim - 1;
+    pNew->nAreaLim = 1;
+    p->nAreaLim = p->nAreaLim - 1;
+
+    // free cofactor storage
+    Lpk_FunFreeTruthTables( p, nCofVars, ppTruths );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcFun.c b/src/opt/lpk/lpkAbcFun.c
new file mode 100644
index 00000000..f7d2f402
--- /dev/null
+++ b/src/opt/lpk/lpkAbcFun.c
@@ -0,0 +1,204 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcFun.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [Procedures working on decomposed functions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcFun.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunAlloc( int nVars )
+{
+    Lpk_Fun_t * p;
+    p = (Lpk_Fun_t *)malloc( sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
+    memset( p, 0, sizeof(Lpk_Fun_t) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the function]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunFree( Lpk_Fun_t * p )
+{
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the starting function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
+{
+    Lpk_Fun_t * p;
+    Abc_Obj_t * pNode;
+    int i;
+    p = Lpk_FunAlloc( Vec_PtrSize(vLeaves) );
+    p->Id = Vec_PtrSize(vLeaves);
+    p->vNodes = vLeaves;
+    p->nVars = Vec_PtrSize(vLeaves);
+    p->nLutK = nLutK;
+    p->nAreaLim = AreaLim;
+    p->nDelayLim = DelayLim;
+    p->uSupp = Kit_TruthSupport( pTruth, p->nVars );
+    Kit_TruthCopy( Lpk_FunTruth(p,0), pTruth, p->nVars );
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        p->pFanins[i] = i;
+        p->pDelays[i] = pNode->Level;
+    }
+    Vec_PtrPush( p->vNodes, p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new function with the given truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
+{
+    Lpk_Fun_t * pNew;
+    pNew = Lpk_FunAlloc( p->nVars );
+    pNew->Id = Vec_PtrSize(p->vNodes);
+    pNew->vNodes = p->vNodes;
+    pNew->nVars = p->nVars;
+    pNew->nLutK = p->nLutK;
+    pNew->nAreaLim = p->nAreaLim;
+    pNew->nDelayLim = p->nDelayLim;
+    pNew->uSupp = Kit_TruthSupport( pTruth, p->nVars );
+    Kit_TruthCopy( Lpk_FunTruth(pNew,0), pTruth, p->nVars );
+    memcpy( pNew->pFanins, p->pFanins, 16 );
+    memcpy( pNew->pDelays, p->pDelays, 16 );
+    Vec_PtrPush( p->vNodes, pNew );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes support of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
+{
+    int j, k, nVarsNew;
+    // compress the truth table
+    if ( p->uSupp == Kit_BitMask(p->nVars) )
+        return;
+    // minimize support
+    nVarsNew = Kit_WordCountOnes(p->uSupp);
+    Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
+    for ( j = k = 0; j < (int)p->nVars; j++ )
+        if ( p->uSupp & (1 << j) )
+        {
+            p->pFanins[k] = p->pFanins[j];
+            p->pDelays[k] = p->pDelays[j];
+            k++;
+        }
+    assert( k == nVarsNew );
+    p->nVars = k;
+    p->uSupp = Kit_BitMask(p->nVars);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Get the delay of the bound set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_SuppDelay( unsigned uSupp, char * pDelays )
+{
+    int Delay, Var;
+    Delay = 0;
+    Lpk_SuppForEachVar( uSupp, Var )
+        Delay = ABC_MAX( Delay, pDelays[Var] );
+    return Delay + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts support into variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_SuppToVars( unsigned uBoundSet, char * pVars )
+{
+    int i, nVars = 0;
+    Lpk_SuppForEachVar( uBoundSet, i )
+        pVars[nVars++] = i;
+    return nVars;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c
new file mode 100644
index 00000000..1525a7e0
--- /dev/null
+++ b/src/opt/lpk/lpkAbcMux.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcMux.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [Iterative MUX decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cofactors w.r.t. the given var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar )
+{
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, iVar );
+    Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cofactors w.r.t. each variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps )
+{
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    int Var;
+    Lpk_SuppForEachVar( p->uSupp, Var )
+    {
+        Lpk_FunComputeCofs( p, Var );
+        puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
+        puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the possibility of MUX decomposition.]
+
+  Description [Returns the best variable to use for MUX decomposition.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_FunAnalizeMux( Lpk_Fun_t * p )
+{
+    unsigned puSupps[32] = {0};
+    int nSuppSize0, nSuppSize1, Delay, Delay0, Delay1, DelayA, DelayB;
+    int Var, Area, Polarity, VarBest, AreaBest, PolarityBest, nSuppSizeBest;
+
+    if ( p->nVars > p->nAreaLim * (p->nLutK - 1) + 1 )
+        return -1;
+    // get cofactor supports for each variable
+    Lpk_FunComputeCofSupps( p, puSupps );
+    // derive the delay and area of each MUX-decomposition
+    VarBest = -1;
+    Lpk_SuppForEachVar( p->uSupp, Var )
+    {
+        nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]);
+        nSuppSize1 = Kit_WordCountOnes(puSupps[2*Var+1]);
+        if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
+        {
+            // include cof var into 0-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay0 = ABC_MAX( DelayA, DelayB + 1 );
+            // include cof var into 1-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay1 = ABC_MAX( DelayA, DelayB + 1 );
+            // get the best delay
+            Delay = ABC_MIN( Delay0, Delay1 );
+            Area = 2;
+            Polarity = (int)(Delay1 == Delay);
+        }
+        else if ( nSuppSize0 <= (int)p->nLutK - 2 )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
+            Polarity = 0;
+        }
+        else if ( nSuppSize0 <= (int)p->nLutK )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
+            Polarity = 1;
+        }
+        else if ( nSuppSize1 <= (int)p->nLutK - 2 )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
+            Polarity = 1;
+        }
+        else if ( nSuppSize1 <= (int)p->nLutK )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK );
+            Polarity = 0;
+        }
+        else
+        {
+            // include cof var into 0-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay0 = ABC_MAX( DelayA, DelayB + 1 );
+            // include cof var into 1-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay1 = ABC_MAX( DelayA, DelayB + 1 );
+            // get the best delay
+            Delay = ABC_MIN( Delay0, Delay1 );
+            if ( Delay == Delay0 )
+                Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
+            else
+                Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
+            Polarity = (int)(Delay1 == Delay);
+        }
+        // find the best variable
+        if ( Delay > (int)p->nDelayLim )
+            continue;
+        if ( Area > (int)p->nAreaLim )
+            continue;
+        if ( VarBest == -1 || AreaBest > Area || (AreaBest == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) )
+        {
+            VarBest = Var;
+            AreaBest = Area;
+            PolarityBest = Polarity;
+            nSuppSizeBest = nSuppSize0+nSuppSize1;
+        }
+    }
+    return (VarBest == -1)? -1 : (2*VarBest + Polarity);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the function decomposed by the MUX decomposition.]
+
+  Description [Returns the best variable to use for MUX decomposition.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol )
+{
+    Lpk_Fun_t * pNew;
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    int Var = VarPol / 2;
+    int Pol = VarPol % 2;
+    int iVarVac;
+    assert( VarPol >= 0 && VarPol < 2 * (int)p->nVars );
+    assert( p->nAreaLim >= 2 );
+    Lpk_FunComputeCofs( p, Var );
+    if ( Pol == 0 )
+    {
+        // derive the new component
+        pNew = Lpk_FunDup( p, pTruth1 );
+        // update the old component
+        p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
+        iVarVac = Kit_WordFindFirstBit( ~(p->uSupp | (1 << Var)) );
+        assert( iVarVac < (int)p->nVars );
+        Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
+        // update the truth table
+        Kit_TruthMux( pTruth, pTruth0, pTruth1, pTruth, p->nVars );
+        p->pFanins[iVarVac] = pNew->Id;
+        p->pDelays[iVarVac] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
+        // support minimize both
+        Lpk_FunSuppMinimize( p );
+        Lpk_FunSuppMinimize( pNew );
+        // update delay and area requirements
+        pNew->nDelayLim = p->nDelayLim - 1;
+        if ( p->nVars <= p->nLutK )
+        {
+            pNew->nAreaLim = p->nAreaLim - 1;
+            p->nAreaLim = 1;
+        }
+        else if ( pNew->nVars <= pNew->nLutK )
+        {
+            pNew->nAreaLim = 1;
+            p->nAreaLim = p->nAreaLim - 1;
+        }
+        else if ( p->nVars < pNew->nVars )
+        {
+            pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
+            p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
+        }
+        else // if ( pNew->nVars < p->nVars )
+        {
+            pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
+            p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
+        }
+    }
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index a1da45b5..2158f8f7 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -258,11 +258,6 @@ p->timeCuts += clock() - clk;
         if ( p->pPars->fFirst && i == 1 )
             break;
 
-        if ( p->pObj->Id == 8835 )
-        {
-            int x = 0;
-        }
-
         // compute the truth table
 clk = clock();
         pTruth = Lpk_CutTruth( p, pCut );
@@ -312,6 +307,91 @@ p->timeEval += clock() - clk;
 
 /**Function*************************************************************
 
+  Synopsis    [Performs resynthesis for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
+{
+    static int Count = 0;
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObjNew;
+    Lpk_Cut_t * pCut;
+    unsigned * pTruth;
+    void * pDsd = NULL;
+    int i, k, clk;
+
+    // compute the cuts
+clk = clock();
+    if ( !Lpk_NodeCuts( p ) )
+    {
+p->timeCuts += clock() - clk;
+        return 0;
+    }
+p->timeCuts += clock() - clk;
+
+    if ( p->pPars->fVeryVerbose )
+    printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
+    vLeaves = Vec_PtrAlloc( 32 );
+    // try the good cuts
+    p->nCutsTotal  += p->nCuts;
+    p->nCutsUseful += p->nEvals;
+    for ( i = 0; i < p->nEvals; i++ )
+    {
+        // get the cut
+        pCut = p->pCuts + p->pEvals[i];
+        if ( p->pPars->fFirst && i == 1 )
+            break;
+
+        // collect nodes into the array
+        Vec_PtrClear( vLeaves );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) );
+
+        // compute the truth table
+clk = clock();
+        pTruth = Lpk_CutTruth( p, pCut );
+p->timeTruth += clock() - clk;
+
+        if ( p->pPars->fVeryVerbose )
+        {
+//            char * pFileName;
+            int nSuppSize;
+            Kit_DsdNtk_t * pDsdNtk;
+            nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
+            printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
+                i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+
+            pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); 
+//        Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); 
+            Kit_DsdPrint( stdout, pDsdNtk );
+            Kit_DsdNtkFree( pDsdNtk );
+//            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+//            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
+//            printf( "Saved truth table in file \"%s\".\n", pFileName );
+        }
+
+        // update the network
+clk = clock();
+        pObjNew = Lpk_LpkDecompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize,
+            (int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) );
+p->timeEval += clock() - clk;
+
+        // perform replacement
+        if ( pObjNew )
+            Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+    }
+    Vec_PtrFree( vLeaves );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs resynthesis for one network.]
 
   Description []
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 27a0317c..d0908a6a 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -410,14 +410,6 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
     // initialize the set of leaves to the nodes in the cut
     assert( p->nCuts < LPK_CUTS_MAX );
     pCutNew = p->pCuts + p->nCuts;
-/*
-if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
-{
-    int x = 0;
-    printf( "Start:\n" );
-    Lpk_NodePrintCut( p, pCut );
-}
-*/
     pCutNew->nLeaves = 0;
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
         if ( pCut->pLeaves[i] != Node )
@@ -443,47 +435,30 @@ if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1]
         assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
 
     }
-/*
-    printf( "   Trying cut: " );
-    Lpk_NodePrintCut( p, pCutNew, 1 );
-    printf( "\n" );
-*/
     // skip the contained cuts
     Lpk_NodeCutSignature( pCutNew );
     if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
         return;
 
-
     // update the set of internal nodes
     assert( pCut->nNodes < LPK_SIZE_MAX );
     memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
     pCutNew->nNodes = pCut->nNodes;
-    pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
-
-    // add the marked node
-    pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
-/*
-if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
-{
-    int x = 0;
-    printf( "Finish:\n" );
-    Lpk_NodePrintCut( p, pCutNew );
-}
-*/
+    pCutNew->nNodesDup = pCut->nNodesDup;
+    // check if the node is already there
+    for ( i = 0; i < (int)pCutNew->nNodes; i++ )
+        if ( pCutNew->pNodes[i] == Node )
+            break;
+    if ( i == (int)pCutNew->nNodes ) // new node
+    {
+        pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
+        pCutNew->nNodesDup += !Abc_NodeIsTravIdCurrent(pObj);
+    }
+    // the number of nodes does not exceed MFFC plus duplications
+    assert( pCutNew->nNodes <= p->nMffc + pCutNew->nNodesDup );
     // add the cut to storage
     assert( p->nCuts < LPK_CUTS_MAX );
     p->nCuts++;
-
-//    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
-
-/*
-    printf( "      Creating cut: " );
-    Lpk_NodePrintCut( p, pCutNew, 1 );
-    printf( "\n" );
-*/
-
-//    if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) )
-//        printf( "Assertion in line 477 failed.\n" );
 }
 
 /**Function*************************************************************
@@ -527,13 +502,6 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
         // try to expand the fanins of this cut
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
         {
-
-            if ( p->pObj->Id == 28 && i == 273 && k == 13 )
-            {
-                Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]);
-                int s = 0;
-            }
-
             // create a new cut
             Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
             // quit if the number of cuts has exceeded the limit
@@ -559,7 +527,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
             continue;
         // compute the minimum number of LUTs needed to implement this cut
         // V = N * (K-1) + 1  ~~~~~  N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
-        pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); 
+        pCut->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); 
         pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
         if ( pCut->Weight <= 1.001 )
             continue;
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 683e7b92..d04032ef 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -117,6 +117,47 @@ struct Lpk_Man_t_
     int          timeTotal;
 };
 
+
+// preliminary decomposition result
+typedef struct Lpk_Res_t_ Lpk_Res_t;
+struct Lpk_Res_t_
+{
+    int           nBSVars;
+    unsigned      BSVars;
+    int           nCofVars;
+    char          pCofVars[4];
+    int           nSuppSizeS;
+    int           nSuppSizeL;
+    int           DelayEst;
+    int           AreaEst;
+};
+
+// function to be decomposed
+typedef struct Lpk_Fun_t_ Lpk_Fun_t;
+struct Lpk_Fun_t_
+{
+    Vec_Ptr_t *   vNodes;           // the array of all functions
+    unsigned int  Id         :  5;  // the ID of this node
+    unsigned int  nVars      :  5;  // the number of variables
+    unsigned int  nLutK      :  4;  // the number of LUT inputs
+    unsigned int  nAreaLim   :  8;  // the area limit (the largest allowed)
+    unsigned int  nDelayLim  : 10;  // the delay limit (the largest allowed)
+    char          pFanins[16];      // the fanins of this function
+    char          pDelays[16];      // the delays of the inputs
+    unsigned      uSupp;            // the support of this component
+    unsigned      pTruth[0];        // the truth table (contains room for three truth tables)    
+};
+
+#define Lpk_SuppForEachVar( Supp, Var )\
+    for ( Var = 0; Var < 16; Var++ )\
+        if ( !(Supp & (1<<Var)) ) {} else
+
+static inline int Lpk_LutNumVars( int nLutsLim, int nLutK )  { return  nLutsLim * (nLutK - 1) + 1;                                            }
+static inline int Lpk_LutNumLuts( int nVarsMax, int nLutK )  { return (nVarsMax - 1) / (nLutK - 1) + (int)((nVarsMax - 1) % (nLutK - 1) > 0); }
+    
+static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num )  { assert( Num < 3 ); return p->pTruth + Kit_TruthWordNum(p->nVars) * Num; }
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -136,6 +177,24 @@ struct Lpk_Man_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== lpkAbcCore.c ============================================================*/
+extern Abc_Obj_t *    Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
+/*=== lpkAbcFun.c ============================================================*/
+extern Lpk_Fun_t *    Lpk_FunAlloc( int nVars );
+extern void           Lpk_FunFree( Lpk_Fun_t * p );
+extern Lpk_Fun_t *    Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
+extern Lpk_Fun_t *    Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth );
+extern void           Lpk_FunSuppMinimize( Lpk_Fun_t * p );
+extern int            Lpk_SuppDelay( unsigned uSupp, char * pDelays );
+extern int            Lpk_SuppToVars( unsigned uBoundSet, char * pVars );
+/*=== lpkAbcDsd.c ============================================================*/
+extern Lpk_Res_t *    Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth );
+extern Lpk_Fun_t *    Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
+/*=== lpkAbcMux.c ============================================================*/
+extern int            Lpk_FunAnalizeMux( Lpk_Fun_t * p );
+extern Lpk_Fun_t *    Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol );
+
+
 /*=== lpkCut.c =========================================================*/
 extern unsigned *     Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
 extern int            Lpk_NodeCuts( Lpk_Man_t * p );
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index c11a0a33..5be198d7 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -54,7 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     p->vCover = Vec_IntAlloc( 1 << 12 );
     for ( i = 0; i < 8; i++ )
         p->vSets[i] = Vec_IntAlloc(100);
-    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
+    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
     return p;
 }