Version abc80130

15 files changed, 0 insertions, 4612 deletions

diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
deleted file mode 100644
index 2a642db2..00000000
--- a/src/opt/lpk/lpk.h
+++ /dev/null
@@ -1,84 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpk.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Fast Boolean matching for LUT structures.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - April 28, 2007.]
-
-  Revision    [$Id: lpk.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __LPK_H__
-#define __LPK_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Lpk_Par_t_ Lpk_Par_t;
-struct Lpk_Par_t_
-{
-    // user-controlled parameters
-    int               nLutsMax;      // (N) the maximum number of LUTs in the structure
-    int               nLutsOver;     // (Q) the maximum number of LUTs not in the MFFC
-    int               nVarsShared;   // (S) the maximum number of shared variables (crossbars)
-    int               nGrowthLevel;  // (L) the maximum increase in the node level after resynthesis
-    int               fSatur;        // iterate till saturation
-    int               fZeroCost;     // accept zero-cost replacements
-    int               fFirst;        // use root node and first cut only
-    int               fOldAlgo;      // use old algorithm
-    int               fVerbose;      // the verbosiness flag
-    int               fVeryVerbose;  // additional verbose info printout
-    // internal parameters
-    int               nLutSize;      // (K) the LUT size (determined by the input network)
-    int               nVarsMax;      // (V) the largest number of variables: V = N * (K-1) + 1
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                           ITERATORS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== lpkCore.c ========================================================*/
-extern int     Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars );
-
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c
deleted file mode 100644
index aa2d4bc0..00000000
--- a/src/opt/lpk/lpkAbcDec.c
+++ /dev/null
@@ -1,290 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkAbcDec.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: lpkAbcDec.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_ImplementFun( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
-{
-    extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
-    unsigned * pTruth;
-    Abc_Obj_t * pObjNew;
-    int i;
-    if ( p->fMark )
-        pMan->nMuxes++;
-    else
-        pMan->nDsds++;
-    // create the new node
-    pObjNew = Abc_NtkCreateNode( pNtk );
-    for ( i = 0; i < (int)p->nVars; i++ )
-        Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(Vec_PtrEntry(vLeaves, p->pFanins[i])) );
-    Abc_ObjSetLevel( pObjNew, Abc_ObjLevelNew(pObjNew) );
-    // assign the node's function
-    pTruth = Lpk_FunTruth(p, 0);
-    if ( p->nVars == 0 )
-    {
-        pObjNew->pData = Hop_NotCond( Hop_ManConst1(pNtk->pManFunc), !(pTruth[0] & 1) );
-        return pObjNew;
-    }
-    if ( p->nVars == 1 )
-    {
-        pObjNew->pData = Hop_NotCond( Hop_ManPi(pNtk->pManFunc, 0), (pTruth[0] & 1) );
-        return pObjNew;
-    }
-    // create the logic function
-    pObjNew->pData = Kit_TruthToHop( pNtk->pManFunc, pTruth, p->nVars, NULL );
-    return pObjNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements the function.]
-
-  Description [Returns the node implementing this function.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Lpk_Implement_rec( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * pFun )
-{
-    Abc_Obj_t * pFanin, * pRes;
-    int i;
-    // prepare the leaves of the function
-    for ( i = 0; i < (int)pFun->nVars; i++ )
-    {
-        pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] );
-        if ( !Abc_ObjIsComplement(pFanin) )
-            Lpk_Implement_rec( pMan, pNtk, vLeaves, (Lpk_Fun_t *)pFanin );
-        pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] );
-        assert( Abc_ObjIsComplement(pFanin) );
-    }
-    // construct the function
-    pRes = Lpk_ImplementFun( pMan, pNtk, vLeaves, pFun );
-    // replace the function
-    Vec_PtrWriteEntry( vLeaves, pFun->Id, Abc_ObjNot(pRes) );
-    Lpk_FunFree( pFun );
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements the function.]
-
-  Description [Returns the node implementing this function.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Lpk_Implement( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
-{
-    Abc_Obj_t * pFanin, * pRes;
-    int i;
-    assert( nLeavesOld < Vec_PtrSize(vLeaves) );
-    // mark implemented nodes
-    Vec_PtrForEachEntryStop( vLeaves, pFanin, i, nLeavesOld )
-        Vec_PtrWriteEntry( vLeaves, i, Abc_ObjNot(pFanin) );
-    // recursively construct starting from the first entry
-    pRes = Lpk_Implement_rec( pMan, pNtk, vLeaves, Vec_PtrEntry( vLeaves, nLeavesOld ) );
-    Vec_PtrShrink( vLeaves, nLeavesOld );
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Decomposes the function using recursive MUX decomposition.]
-
-  Description [Returns the ID of the top-most decomposition node 
-  implementing this function, or 0 if there is no decomposition satisfying
-  the constraints on area and delay.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p )
-{
-    static Lpk_Res_t Res0, * pRes0 = &Res0;
-    Lpk_Res_t * pResMux, * pResDsd;
-    Lpk_Fun_t * p2;
-    int clk;
-
-    // is only called for non-trivial blocks
-    assert( p->nLutK >= 3 && p->nLutK <= 6 );
-    assert( p->nVars > p->nLutK );
-    // skip if area bound is exceeded
-    if ( Lpk_LutNumLuts(p->nVars, p->nLutK) > (int)p->nAreaLim )
-        return 0;
-    // skip if delay bound is exceeded
-    if ( Lpk_SuppDelay(p->uSupp, p->pDelays) > (int)p->nDelayLim )
-        return 0;
-
-    // compute supports if needed
-    if ( !p->fSupports )
-        Lpk_FunComputeCofSupps( p );
-
-    // check DSD decomposition
-clk = clock();
-    pResDsd = Lpk_DsdAnalize( pMan, p, pMan->pPars->nVarsShared );
-pMan->timeEvalDsdAn += clock() - clk;
-    if ( pResDsd && (pResDsd->nBSVars == (int)p->nLutK || pResDsd->nBSVars == (int)p->nLutK - 1) && 
-          pResDsd->AreaEst <= (int)p->nAreaLim && pResDsd->DelayEst <= (int)p->nDelayLim )
-    {
-clk = clock();
-        p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
-pMan->timeEvalDsdSp += clock() - clk;
-        assert( p2->nVars <= (int)p->nLutK );
-        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
-            return 0;
-        return 1;
-    }
-
-    // check MUX decomposition
-clk = clock();
-    pResMux = Lpk_MuxAnalize( pMan, p );
-pMan->timeEvalMuxAn += clock() - clk;
-//    pResMux = NULL;
-    assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) );
-    // accept MUX decomposition if it is "good"
-    if ( pResMux && pResMux->nSuppSizeS <= (int)p->nLutK && pResMux->nSuppSizeL <= (int)p->nLutK )
-        pResDsd = NULL;
-    else if ( pResMux && pResDsd )
-    {
-        // compare two decompositions
-        if ( pResMux->AreaEst < pResDsd->AreaEst || 
-            (pResMux->AreaEst == pResDsd->AreaEst && pResMux->nSuppSizeL < pResDsd->nSuppSizeL) || 
-            (pResMux->AreaEst == pResDsd->AreaEst && pResMux->nSuppSizeL == pResDsd->nSuppSizeL && pResMux->DelayEst < pResDsd->DelayEst) )
-            pResDsd = NULL;
-        else
-            pResMux = NULL;
-    }
-    assert( pResMux == NULL || pResDsd == NULL );
-    if ( pResMux )
-    {
-clk = clock();
-        p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
-pMan->timeEvalMuxSp += clock() - clk;
-        if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p2 ) )
-            return 0;
-        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
-            return 0;
-        return 1;
-    }
-    if ( pResDsd )
-    {
-clk = clock();
-        p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
-pMan->timeEvalDsdSp += clock() - clk;
-        assert( p2->nVars <= (int)p->nLutK );
-        if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
-            return 0;
-        return 1;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes decomposed nodes from the array of fanins.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_DecomposeClean( Vec_Ptr_t * vLeaves, int nLeavesOld )
-{
-    Lpk_Fun_t * pFunc;
-    int i;
-    Vec_PtrForEachEntryStart( vLeaves, pFunc, i, nLeavesOld )
-        Lpk_FunFree( pFunc );
-    Vec_PtrShrink( vLeaves, nLeavesOld );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Decomposes the function using recursive MUX decomposition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Lpk_Decompose( Lpk_Man_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim )
-{
-    Lpk_Fun_t * pFun;
-    Abc_Obj_t * pObjNew = NULL;
-    int nLeaves = Vec_PtrSize( vLeaves );
-    pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
-    if ( puSupps[0] || puSupps[1] )
-    {
-/*
-        int i;
-        Lpk_FunComputeCofSupps( pFun );
-        for ( i = 0; i < nLeaves; i++ )
-        {
-            assert( pFun->puSupps[2*i+0] == puSupps[2*i+0] );
-            assert( pFun->puSupps[2*i+1] == puSupps[2*i+1] );
-        }
-*/
-        memcpy( pFun->puSupps, puSupps, sizeof(unsigned) * 2 * nLeaves );
-        pFun->fSupports = 1;
-    }
-    Lpk_FunSuppMinimize( pFun );
-    if ( pFun->nVars <= pFun->nLutK )
-        pObjNew = Lpk_ImplementFun( p, pNtk, vLeaves, pFun );
-    else if ( Lpk_Decompose_rec(p, pFun) )
-        pObjNew = Lpk_Implement( p, pNtk, vLeaves, nLeaves );
-    Lpk_DecomposeClean( vLeaves, nLeaves );
-    return pObjNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
deleted file mode 100644
index f4095914..00000000
--- a/src/opt/lpk/lpkAbcDsd.c
+++ /dev/null
@@ -1,603 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkAbcDsd.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Fast Boolean matching for LUT structures.]
-
-  Synopsis    [LUT-decomposition based on recursive DSD.]
-
-  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    [Cofactors TTs w.r.t. all vars and finds the best var.]
-
-  Description [The best variable is the variable with the minimum 
-  sum total of the support sizes of all truth tables. This procedure 
-  computes and returns cofactors w.r.t. the best variable.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs, unsigned uNonDecSupp )
-{
-    int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
-    assert( nTruths > 0 );
-    VarBest = -1;
-    Lpk_SuppForEachVar( p->uSupp, Var )
-    {
-        if ( (uNonDecSupp & (1 << Var)) == 0 )
-            continue;
-        nSuppMaxCur = 0;
-        nSuppTotalCur = 0;
-        for ( i = 0; i < nTruths; i++ )
-        {
-            if ( nTruths == 1 )
-            {
-                nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] );
-                nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] );
-            }
-            else
-            {
-                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 || nSuppMaxMin > nSuppMaxCur ||
-             (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) )
-        {
-            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, int nSizeMax )
-{
-    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, nSizeMax );
-            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];
-            if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
-                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, nSizeMax );
-        uSupport |= uSuppCur;
-        if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
-            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]) );
-        if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
-            Vec_IntPush( vSets, uSupport );
-        return vSets;
-    }
-    uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax );
-    assert( (uSupport & 0xFFFF0000) == 0 );
-    // add the total support of the network
-    if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
-        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    [Prints the sets of subsets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Lpk_PrintSetOne( int uSupport )
-{
-    unsigned k;
-    for ( k = 0; k < 16; k++ )
-        if ( uSupport & (1<<k) )
-            printf( "%c", 'a'+k );
-    printf( " " );
-}
-/**Function*************************************************************
-
-  Synopsis    [Prints the sets of subsets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Lpk_PrintSets( Vec_Int_t * vSets )
-{
-    unsigned uSupport;
-    int Number, i;
-    printf( "Subsets(%d): ", Vec_IntSize(vSets) );
-    Vec_IntForEachEntry( vSets, Number, i )
-    {
-        uSupport = Number;
-        Lpk_PrintSetOne( uSupport );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Merges two bound sets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSizeMax )
-{
-    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;
-        if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax )
-            Vec_IntPush( vSets, Entry );
-    }
-    return vSets;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs DSD-based decomposition of the function.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes )
-{
-    int fVerbose = 0;
-    unsigned uBoundSet;
-    int i, nVarsBS, nVarsRem, Delay, Area;
-
-    // compare the resulting boundsets
-    memset( pRes, 0, sizeof(Lpk_Res_t) );
-    Vec_IntForEachEntry( vBSets, uBoundSet, i )
-    {
-        if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset
-            continue;
-        if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest
-            continue;
-        if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving
-            continue;
-if ( fVerbose )
-Lpk_PrintSetOne( uBoundSet );
-        assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
-        nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
-        if ( nVarsBS == 1 )
-            continue;
-        assert( nVarsBS <= (int)p->nLutK - nCofDepth );
-        nVarsRem = p->nVars - nVarsBS + 1;
-        Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
-        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
-if ( fVerbose )
-printf( "area = %d limit = %d  delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim );
-        if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
-            continue;
-        if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) )
-        {
-            pRes->nBSVars = nVarsBS;
-            pRes->BSVars = (uBoundSet & 0xFFFF);
-            pRes->nSuppSizeS = nVarsBS + nCofDepth;
-            pRes->nSuppSizeL = nVarsRem;
-            pRes->DelayEst = Delay;
-            pRes->AreaEst = Area;
-        }
-    }
-if ( fVerbose )
-{
-if ( pRes->BSVars )
-{
-printf( "Found bound set " );
-Lpk_PrintSetOne( pRes->BSVars );
-printf( "\n" );
-}
-else
-printf( "Did not find boundsets.\n" );
-printf( "\n" );
-}
-    if ( pRes->BSVars )
-    {
-        assert( pRes->DelayEst <= (int)p->nDelayLim );
-        assert( pRes->AreaEst <= (int)p->nAreaLim );
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Finds late arriving inputs, which cannot be in the bound set.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p )
-{
-    unsigned i, uLateArrSupp = 0;
-    Lpk_SuppForEachVar( p->uSupp, i )
-        if ( p->pDelays[i] > (int)p->nDelayLim - 2 )
-            uLateArrSupp |= (1 << i);  
-    return uLateArrSupp;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs DSD-based decomposition of the function.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes )
-{
-    int fVerbose = 0;
-    Vec_Int_t * pvBSets[4][8];
-    unsigned uNonDecSupp, uLateArrSupp;
-    int i, k, nNonDecSize, nNonDecSizeMax;
-    assert( nCofDepth >= 1 && nCofDepth <= 3 );
-    assert( nCofDepth < (int)p->nLutK - 1 );
-    assert( p->fSupports );
-
-    // find the support of the largest non-DSD block
-    nNonDecSizeMax = 0;
-    uNonDecSupp = p->uSupp;
-    for ( i = 0; i < (1<<(nCofDepth-1)); i++ )
-    {
-        nNonDecSize = Kit_DsdNonDsdSizeMax( pNtks[i] );
-        if ( nNonDecSizeMax < nNonDecSize )
-        {
-            nNonDecSizeMax = nNonDecSize;
-            uNonDecSupp = Kit_DsdNonDsdSupports( pNtks[i] );
-        }
-        else if ( nNonDecSizeMax == nNonDecSize )
-            uNonDecSupp |= Kit_DsdNonDsdSupports( pNtks[i] );
-    }
-
-    // remove those variables that cannot be used because of delay constraints
-    // if variables arrival time is more than p->DelayLim - 2, it cannot be used
-    uLateArrSupp = Lpk_DsdLateArriving( p );
-    if ( (uNonDecSupp & ~uLateArrSupp) == 0 )
-    {
-        memset( pRes, 0, sizeof(Lpk_Res_t) );
-        return 0;
-    }
-
-    // find the next cofactoring variable
-    pCofVars[nCofDepth-1] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[nCofDepth-1], 1<<(nCofDepth-1), ppTruths[nCofDepth], uNonDecSupp & ~uLateArrSupp );
-
-    // derive decomposed networks
-    for ( i = 0; i < (1<<nCofDepth); i++ )
-    {
-        if ( pNtks[i] )
-            Kit_DsdNtkFree( pNtks[i] );
-        pNtks[i] = Kit_DsdDecomposeExpand( ppTruths[nCofDepth][i], p->nVars );
-if ( fVerbose )
-Kit_DsdPrint( stdout, pNtks[i] );
-        pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtks[i], p->nLutK - nCofDepth ); // try restricting to those in uNonDecSupp!!!
-    }
-
-    // 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], p->nLutK - nCofDepth );
-    // compare bound-sets
-    Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
-    // free the bound sets
-    for ( i = nCofDepth; i >= 0; i-- )
-        for ( k = 0; k < (1<<i); k++ )
-            Vec_IntFree( pvBSets[i][k] );
- 
-    // copy the cofactoring variables
-    if ( pRes->BSVars )
-    {
-        pRes->nCofVars = nCofDepth;
-        for ( i = 0; i < nCofDepth; i++ )
-            pRes->pCofVars[i] = pCofVars[i];
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs DSD-based decomposition of the function.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared )
-{ 
-    static Lpk_Res_t Res0, * pRes0 = &Res0;
-    static Lpk_Res_t Res1, * pRes1 = &Res1;
-    static Lpk_Res_t Res2, * pRes2 = &Res2;
-    static Lpk_Res_t Res3, * pRes3 = &Res3;
-    int fUseBackLooking = 1;
-    Lpk_Res_t * pRes = NULL;
-    Vec_Int_t * vBSets;
-    Kit_DsdNtk_t * pNtks[8] = {NULL};
-    char pCofVars[5];
-    int i;
-
-    assert( p->nLutK >= 3 );
-    assert( nShared >= 0 && nShared <= 3 );
-    assert( p->uSupp == Kit_BitMask(p->nVars) );
-
-    // try decomposition without cofactoring
-    pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
-    if ( pMan->pPars->fVerbose )
-        pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
-    vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
-    Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
-    Vec_IntFree( vBSets );
-
-    // check the result
-    if ( pRes0->nBSVars == (int)p->nLutK )
-        { pRes = pRes0; goto finish; }
-    if ( pRes0->nBSVars == (int)p->nLutK - 1 )
-        { pRes = pRes0; goto finish; }
-    if ( nShared == 0 )
-        goto finish;
-
-    // prepare storage
-    Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );
-
-    // cofactor 1 time
-    if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
-        goto finish;
-    assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
-    if ( pRes1->nBSVars == (int)p->nLutK - 1 )
-        { pRes = pRes1; goto finish; }
-    if ( pRes0->nBSVars == (int)p->nLutK - 2 )
-        { pRes = pRes0; goto finish; }
-    if ( pRes1->nBSVars == (int)p->nLutK - 2 )
-        { pRes = pRes1; goto finish; }
-    if ( nShared == 1 )
-        goto finish;
-
-    // cofactor 2 times
-    if ( p->nLutK >= 4 ) 
-    {
-        if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
-            goto finish;
-        assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
-        if ( pRes2->nBSVars == (int)p->nLutK - 2 )
-            { pRes = pRes2; goto finish; }
-        if ( fUseBackLooking )
-        {
-            if ( pRes0->nBSVars == (int)p->nLutK - 3 )
-                { pRes = pRes0; goto finish; }
-            if ( pRes1->nBSVars == (int)p->nLutK - 3 )
-                { pRes = pRes1; goto finish; }
-        }
-        if ( pRes2->nBSVars == (int)p->nLutK - 3 )
-            { pRes = pRes2; goto finish; }
-        if ( nShared == 2 )
-            goto finish;
-        assert( nShared == 3 );
-    }
-
-    // cofactor 3 times
-    if ( p->nLutK >= 5 ) 
-    {
-        if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
-            goto finish;
-        assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
-        if ( pRes3->nBSVars == (int)p->nLutK - 3 )
-            { pRes = pRes3; goto finish; }
-        if ( fUseBackLooking )
-        {
-            if ( pRes0->nBSVars == (int)p->nLutK - 4 )
-                { pRes = pRes0; goto finish; }
-            if ( pRes1->nBSVars == (int)p->nLutK - 4 )
-                { pRes = pRes1; goto finish; }
-            if ( pRes2->nBSVars == (int)p->nLutK - 4 )
-                { pRes = pRes2; goto finish; }
-        }
-        if ( pRes3->nBSVars == (int)p->nLutK - 4 )
-            { pRes = pRes3; goto finish; }
-    }
-
-finish:
-    // free the networks
-    for ( i = 0; i < (1<<nShared); i++ )
-        if ( pNtks[i] )
-            Kit_DsdNtkFree( pNtks[i] );
-    // choose the best under these conditions
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Splits the function into two subfunctions using DSD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
-{
-    Lpk_Fun_t * pNew;
-    Kit_DsdNtk_t * pNtkDec;
-    int i, k, iVacVar, nCofs;
-    // prepare storage
-    Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars );
-    // get the vacuous variable
-    iVacVar = Kit_WordFindFirstBit( uBoundSet );
-    // compute the cofactors
-    for ( i = 0; i < nCofVars; i++ )
-        for ( k = 0; k < (1<<i); k++ )
-        {
-            Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
-            Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
-        }
-    // decompose each cofactor w.r.t. the bound set
-    nCofs = (1<<nCofVars);
-    for ( k = 0; k < nCofs; k++ )
-    {
-        pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars );
-        Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] );
-        Kit_DsdNtkFree( pNtkDec );
-    }
-    // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1])
-    for ( i = nCofVars; i >= 1; i-- )
-        for ( k = 0; k < (1<<i); k++ )
-            Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] );
-
-    // derive the new component (decomposition function)
-    pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] );
-    // update the old component (composition function)
-    Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars );
-    p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars );
-    p->pFanins[iVacVar] = pNew->Id;
-    p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
-    // support minimize both
-    p->fSupports = 0;
-    Lpk_FunSuppMinimize( p );
-    Lpk_FunSuppMinimize( pNew );
-    // update delay and area requirements
-    pNew->nDelayLim = p->pDelays[iVacVar];
-    pNew->nAreaLim = 1;
-    p->nAreaLim = p->nAreaLim - 1;
-    return pNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c
deleted file mode 100644
index d6f579ee..00000000
--- a/src/opt/lpk/lpkAbcMux.c
+++ /dev/null
@@ -1,235 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkAbcMux.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Fast Boolean matching for LUT structures.]
-
-  Synopsis    [LUT-decomposition based on recursive 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    [Checks the possibility of MUX decomposition.]
-
-  Description [Returns the best variable to use for MUX decomposition.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lpk_Res_t * Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p )
-{
-    static Lpk_Res_t Res, * pRes = &Res;
-    int nSuppSize0, nSuppSize1, nSuppSizeS, nSuppSizeL;
-    int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB;
-    memset( pRes, 0, sizeof(Lpk_Res_t) );
-    assert( p->uSupp == Kit_BitMask(p->nVars) );
-    assert( p->fSupports );
-    // derive the delay and area after MUX-decomp with each var - and find the best var
-    pRes->Variable = -1;
-    Lpk_SuppForEachVar( p->uSupp, Var )
-    {
-        nSuppSize0 = Kit_WordCountOnes(p->puSupps[2*Var+0]);
-        nSuppSize1 = Kit_WordCountOnes(p->puSupps[2*Var+1]);
-        assert( nSuppSize0 < (int)p->nVars );
-        assert( nSuppSize1 < (int)p->nVars );
-        if ( nSuppSize0 < 1 || nSuppSize1 < 1 )
-            continue;
-//printf( "%d %d    ", nSuppSize0, nSuppSize1 );
-        if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
-        {
-            // include cof var into 0-block
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
-            Delay0 = ABC_MAX( DelayA, DelayB + 1 );
-            // include cof var into 1-block
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->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)(Delay == Delay1);
-        }
-        else if ( nSuppSize0 <= (int)p->nLutK - 2 )
-        {
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
-            Delay = ABC_MAX( DelayA, DelayB + 1 );
-            Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
-            Polarity = 0;
-        }
-        else if ( nSuppSize1 <= (int)p->nLutK - 2 )
-        {
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
-            Delay = ABC_MAX( DelayA, DelayB + 1 );
-            Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
-            Polarity = 1;
-        }
-        else if ( nSuppSize0 <= (int)p->nLutK )
-        {
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->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 )
-        {
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->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( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
-            Delay0 = ABC_MAX( DelayA, DelayB + 1 );
-            // include cof var into 1-block
-            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
-            DelayB = Lpk_SuppDelay( p->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)(Delay == Delay1);
-        }
-        // find the best variable
-        if ( Delay > (int)p->nDelayLim )
-            continue;
-        if ( Area > (int)p->nAreaLim )
-            continue;
-        nSuppSizeS = ABC_MIN( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
-        nSuppSizeL = ABC_MAX( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
-        if ( nSuppSizeL > (int)p->nVars )
-            continue;
-        if ( pRes->Variable == -1 || pRes->AreaEst > Area || 
-            (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL > nSuppSizeS + nSuppSizeL) || 
-            (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL == nSuppSizeS + nSuppSizeL && pRes->DelayEst > Delay) )
-        {
-            pRes->Variable = Var;
-            pRes->Polarity = Polarity;
-            pRes->AreaEst  = Area;
-            pRes->DelayEst = Delay;
-            pRes->nSuppSizeS = nSuppSizeS;
-            pRes->nSuppSizeL = nSuppSizeL;
-        }
-    }
-    return pRes->Variable == -1 ? NULL : pRes;
-}
-
-/**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_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol )
-{
-    Lpk_Fun_t * pNew;
-    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
-    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
-    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-//    unsigned uSupp;
-    int iVarVac; 
-    assert( Var >= 0 && Var < (int)p->nVars );
-    assert( p->nAreaLim >= 2 );
-    assert( p->uSupp == Kit_BitMask(p->nVars) );
-    Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
-    Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
-/*
-uSupp = Kit_TruthSupport( pTruth, p->nVars );
-Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
-uSupp = Kit_TruthSupport( pTruth0, p->nVars );
-Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
-uSupp = Kit_TruthSupport( pTruth1, p->nVars );
-Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n\n" );
-*/
-    // derive the new component
-    pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 );
-    // update the support of the old component
-    p->uSupp  = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
-    p->uSupp |= (1 << Var);
-    // update the truth table of the old component
-    iVarVac = Kit_WordFindFirstBit( ~p->uSupp );
-    assert( iVarVac < (int)p->nVars );
-    p->uSupp |= (1 << iVarVac);
-    Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
-    if ( Pol )
-        Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, Var );
-    else
-        Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, Var );
-    assert( p->uSupp == Kit_TruthSupport(pTruth, p->nVars) );
-    // set the decomposed variable
-    p->pFanins[iVarVac] = pNew->Id;
-    p->pDelays[iVarVac] = p->nDelayLim - 1;
-    // support minimize both
-    p->fSupports = 0;
-    Lpk_FunSuppMinimize( p );
-    Lpk_FunSuppMinimize( pNew );
-    // update delay and area requirements
-    pNew->nDelayLim = p->nDelayLim - 1;
-    if ( pNew->nVars <= pNew->nLutK )
-    {
-        pNew->nAreaLim = 1;
-        p->nAreaLim = p->nAreaLim - 1;
-    }
-    else if ( p->nVars <= p->nLutK )
-    {
-        pNew->nAreaLim = p->nAreaLim - 1;
-        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;
-    }
-    pNew->fMark = 1;
-    return pNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkAbcUtil.c b/src/opt/lpk/lpkAbcUtil.c
deleted file mode 100644
index 3f917ce2..00000000
--- a/src/opt/lpk/lpkAbcUtil.c
+++ /dev/null
@@ -1,244 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkAbcUtil.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: lpkAbcUtil.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 pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Minimizes support of the function.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_FunSuppMinimize( Lpk_Fun_t * p )
-{
-    int i, k, nVarsNew;
-    // compress the truth table
-    if ( p->uSupp == Kit_BitMask(p->nVars) )
-        return 0;
-    // invalidate support info
-    p->fSupports = 0;
-//Extra_PrintBinary( stdout, &p->uSupp, p->nVars ); printf( "\n" );
-    // minimize support
-    nVarsNew = Kit_WordCountOnes(p->uSupp);
-    Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
-    k = 0;
-    Lpk_SuppForEachVar( p->uSupp, i )
-    {
-        p->pFanins[k] = p->pFanins[i];
-        p->pDelays[k] = p->pDelays[i];
-/*
-        if ( p->fSupports )
-        {
-            p->puSupps[2*k+0] = p->puSupps[2*i+0];
-            p->puSupps[2*k+1] = p->puSupps[2*i+1];
-        }
-*/
-        k++;
-    }
-    assert( k == nVarsNew );
-    p->nVars = k;
-    p->uSupp = Kit_BitMask(p->nVars);
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes cofactors w.r.t. each variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_FunComputeCofSupps( Lpk_Fun_t * p )
-{
-    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
-    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
-    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
-    int Var;
-    assert( p->fSupports == 0 );
-//    Lpk_SuppForEachVar( p->uSupp, Var )
-    for ( Var = 0; Var < (int)p->nVars; Var++ )
-    {
-        Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
-        Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
-        p->puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
-        p->puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
-    }
-    p->fSupports = 1;
-}
-
-/**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/lpkCore.c b/src/opt/lpk/lpkCore.c
deleted file mode 100644
index e819a7fb..00000000
--- a/src/opt/lpk/lpkCore.c
+++ /dev/null
@@ -1,659 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkCore.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: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#include "lpkInt.h"
-#include "cloud.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_IfManStart( Lpk_Man_t * p )
-{
-    If_Par_t * pPars;
-    assert( p->pIfMan == NULL );
-    // set defaults
-    pPars = ALLOC( If_Par_t, 1 );
-    memset( pPars, 0, sizeof(If_Par_t) );
-    // user-controlable paramters
-    pPars->nLutSize    =  p->pPars->nLutSize;
-    pPars->nCutsMax    = 16;
-    pPars->nFlowIters  =  0; // 1
-    pPars->nAreaIters  =  0; // 1 
-    pPars->DelayTarget = -1;
-    pPars->fPreprocess =  0;
-    pPars->fArea       =  1;
-    pPars->fFancy      =  0;
-    pPars->fExpRed     =  0; //
-    pPars->fLatchPaths =  0;
-    pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;
-    // internal parameters
-    pPars->fTruth      =  1;
-    pPars->fUsePerm    =  0; 
-    pPars->nLatches    =  0;
-    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
-    pPars->pTimesArr   =  NULL; 
-    pPars->pTimesArr   =  NULL;   
-    pPars->fUseBdds    =  0;
-    pPars->fUseSops    =  0;
-    pPars->fUseCnfs    =  0;
-    pPars->fUseMv      =  0;
-    // start the mapping manager and set its parameters
-    p->pIfMan = If_ManStart( pPars );
-    If_ManSetupSetAll( p->pIfMan, 1000 );
-    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if at least one entry has changed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pTemp;
-    int i;
-    vNodes = Vec_VecEntry( p->vVisited, iNode );
-    if ( Vec_PtrSize(vNodes) == 0 )
-        return 1;
-    Vec_PtrForEachEntry( vNodes, pTemp, i )
-    {
-        // check if the node has changed
-        pTemp = Abc_NtkObj( p->pNtk, (int)pTemp );
-        if ( pTemp == NULL )
-            return 1;
-        // check if the number of fanouts has changed
-//        if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
-//            return 1;
-        i++;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
-{
-    extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
-    Kit_DsdObj_t * pRoot;
-    If_Obj_t * pDriver, * ppLeaves[16];
-    Abc_Obj_t * pLeaf, * pObjNew;
-    int nGain, i, clk;
-    int nNodesBef;
-//    int nOldShared;
-
-    // check special cases
-    pRoot = Kit_DsdNtkRoot( pNtk );
-    if ( pRoot->Type == KIT_DSD_CONST1 )
-    {
-        if ( Kit_DsdLitIsCompl(pNtk->Root) )
-            pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
-        else
-            pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
-        Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
-        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
-        return 1;
-    }
-    if ( pRoot->Type == KIT_DSD_VAR )
-    {
-        pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
-        if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
-            pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
-        Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
-        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
-        return 1;
-    }
-    assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
-
-    // start the mapping manager
-    if ( p->pIfMan == NULL )
-        Lpk_IfManStart( p );
-
-    // prepare the mapping manager
-    If_ManRestart( p->pIfMan );
-    // create the PI variables
-    for ( i = 0; i < p->pPars->nVarsMax; i++ )
-        ppLeaves[i] = If_ManCreateCi( p->pIfMan );
-    // set the arrival times
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
-        p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
-    // prepare the PI cuts
-    If_ManSetupCiCutSets( p->pIfMan );
-    // create the internal nodes
-    p->fCalledOnce = 0;
-    p->nCalledSRed = 0;
-    pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
-    if ( pDriver == NULL )
-        return 0;
-    // create the PO node
-    If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
-
-    // perform mapping
-    p->pIfMan->pPars->fAreaOnly = 1;
-clk = clock();
-    If_ManPerformMappingComb( p->pIfMan );
-p->timeMap += clock() - clk;
-
-    // compute the gain in area
-    nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
-    if ( p->pPars->fVeryVerbose )
-        printf( "       Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d. SReds = %d.\n", 
-            pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level, p->nCalledSRed );
-
-    // quit if there is no gain
-    if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
-        return 0;
-
-    // quit if depth increases too much
-    if ( (int)p->pIfMan->RequiredGlo > Abc_ObjRequiredLevel(p->pObj) )
-        return 0;
-
-    // perform replacement
-    p->nGainTotal += nGain;
-    p->nChanges++;
-    if ( p->nCalledSRed )
-        p->nBenefited++;
-
-    nNodesBef = Abc_NtkNodeNum(p->pNtk);
-    // prepare the mapping manager
-    If_ManCleanNodeCopy( p->pIfMan );
-    If_ManCleanCutData( p->pIfMan );
-    // set the PIs of the cut
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
-        If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
-    // get the area of mapping
-    pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
-    pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
-    // perform replacement
-    Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
-//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resynthesis for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_ResynthesizeNode( Lpk_Man_t * p )
-{
-    static int Count = 0;
-    Kit_DsdNtk_t * pDsdNtk;
-    Lpk_Cut_t * pCut;
-    unsigned * pTruth;
-    int i, k, nSuppSize, nCutNodes, RetValue, clk;
-
-    // compute the cuts
-clk = clock();
-    if ( !Lpk_NodeCuts( p ) )
-    {
-p->timeCuts += clock() - clk;
-        return 0;
-    }
-p->timeCuts += clock() - clk;
-
-//return 0;
-
-    if ( p->pPars->fVeryVerbose )
-    printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
-    // 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;
-
-        // skip bad cuts        
-//        printf( "Mffc size = %d.  ", Abc_NodeMffcLabel(p->pObj) );
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++;
-        nCutNodes = Abc_NodeMffcLabel(p->pObj);
-//        printf( "Mffc with cut = %d.  ", nCutNodes );
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--;
-//        printf( "Mffc cut = %d.  ", (int)pCut->nNodes - (int)pCut->nNodesDup );
-//        printf( "\n" );
-        if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup )
-            continue;
-
-        // compute the truth table
-clk = clock();
-        pTruth = Lpk_CutTruth( p, pCut, 0 );
-        nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
-p->timeTruth += clock() - clk;
-
-        pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); 
-//        Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); 
-        // skip 16-input non-DSD because ISOP will not work
-        if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) 
-        {
-            Kit_DsdNtkFree( pDsdNtk );
-            continue;
-        }
-
-        // if DSD has nodes that require splitting to fit them into LUTs
-        // we can skip those cuts that cannot lead to improvement
-        // (a full DSD network requires  V = Nmin * (K-1) + 1 for improvement)
-        if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > p->pPars->nLutSize && 
-             nSuppSize >= ((int)pCut->nNodes - (int)pCut->nNodesDup - 1) * (p->pPars->nLutSize - 1) + 1 )
-        {
-            Kit_DsdNtkFree( pDsdNtk );
-            continue;
-        }
-
-        if ( p->pPars->fVeryVerbose )
-        {
-//            char * pFileName;
-            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 );
-            Kit_DsdPrint( stdout, 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();
-        RetValue = Lpk_ExploreCut( p, pCut, pDsdNtk );
-p->timeEval += clock() - clk;
-        Kit_DsdNtkFree( pDsdNtk );
-        if ( RetValue )
-            break;
-    }
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes supports of the cofactors of the function.]
-
-  Description [This procedure should be called after Lpk_CutTruth(p,pCut,0)]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_ComputeSupports( Lpk_Man_t * p, Lpk_Cut_t * pCut, unsigned * pTruth )
-{
-    unsigned * pTruthInv;
-    int RetValue1, RetValue2;
-    pTruthInv = Lpk_CutTruth( p, pCut, 1 );
-    RetValue1 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruth, pCut->nLeaves, p->vBddDir );
-    RetValue2 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruthInv, pCut->nLeaves, p->vBddInv );
-    if ( RetValue1 && RetValue2 )
-        Kit_TruthCofSupports( p->vBddDir, p->vBddInv, pCut->nLeaves, p->vMemory, p->puSupps ); 
-    else
-        p->puSupps[0] = p->puSupps[1] = 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resynthesis for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
-{
-    static int Count = 0;
-    Abc_Obj_t * pObjNew, * pLeaf;
-    Lpk_Cut_t * pCut;
-    unsigned * pTruth;
-    int nNodesBef, nNodesAft, nCutNodes;
-    int i, k, clk;
-    int Required = Abc_ObjRequiredLevel(p->pObj);
-//    CloudNode * pFun2;//, * pFun1;
-
-    // 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.  Level = %2d. Req = %2d.\n", 
-            p->pObj->Id, p->nMffc, p->nEvals, p->pObj->Level, Required );
-    // 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;
-//        if ( pCut->Weight < 1.05 )
-//            continue;
-
-        // skip bad cuts        
-//        printf( "Mffc size = %d.  ", Abc_NodeMffcLabel(p->pObj) );
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++;
-        nCutNodes = Abc_NodeMffcLabel(p->pObj);
-//        printf( "Mffc with cut = %d.  ", nCutNodes );
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--;
-//        printf( "Mffc cut = %d.  ", (int)pCut->nNodes - (int)pCut->nNodesDup );
-//        printf( "\n" );
-        if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup )
-            continue;
-
-        // collect nodes into the array
-        Vec_PtrClear( p->vLeaves );
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            Vec_PtrPush( p->vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[k]) );
-
-        // compute the truth table
-clk = clock();
-        pTruth = Lpk_CutTruth( p, pCut, 0 );
-p->timeTruth += clock() - clk;
-clk = clock();
-        Lpk_ComputeSupports( p, pCut, pTruth );        
-p->timeSupps += clock() - clk;
-//clk = clock();
-//        pFun1 = Lpk_CutTruthBdd( p, pCut );
-//p->timeTruth2 += clock() - clk;
-/*
-clk = clock();
-        Cloud_Restart( p->pDsdMan->dd );
-        pFun2 = Kit_TruthToCloud( p->pDsdMan->dd, pTruth, pCut->nLeaves );
-        RetValue = Kit_CreateCloud( p->pDsdMan->dd, pFun2, p->vBddNodes );
-p->timeTruth3 += clock() - clk;
-*/
-//        if ( pFun1 != pFun2 )
-//            printf( "Truth tables do not agree!\n" );
-//        else
-//            printf( "Fine!\n" );
-
-        if ( p->pPars->fVeryVerbose )
-        {
-//            char * pFileName;
-            int 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 );
-            Vec_PtrForEachEntry( p->vLeaves, pLeaf, k )
-                printf( "%c=%d ", 'a'+k, Abc_ObjLevel(pLeaf) );
-            printf( "\n" );
-            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
-//            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
-//            printf( "Saved truth table in file \"%s\".\n", pFileName );
-        }
-
-        // update the network
-        nNodesBef = Abc_NtkNodeNum(p->pNtk);
-clk = clock();
-        pObjNew = Lpk_Decompose( p, p->pNtk, p->vLeaves, pTruth, p->puSupps, p->pPars->nLutSize,
-            (int)pCut->nNodes - (int)pCut->nNodesDup - 1 + (int)(p->pPars->fZeroCost > 0), Required );
-p->timeEval += clock() - clk;
-        nNodesAft = Abc_NtkNodeNum(p->pNtk);
-
-        // perform replacement
-        if ( pObjNew )
-        {
-            int nGain = (int)pCut->nNodes - (int)pCut->nNodesDup - (nNodesAft - nNodesBef);
-            assert( nGain >= 1 - p->pPars->fZeroCost );
-            assert( Abc_ObjLevel(pObjNew) <= Required );
-/*
-            if ( nGain <= 0 )
-            {
-                int x = 0;
-            }
-            if ( Abc_ObjLevel(pObjNew) > Required )
-            {
-                int x = 0;
-            }
-*/
-            p->nGainTotal += nGain;
-            p->nChanges++;
-            if ( p->pPars->fVeryVerbose )
-                printf( "Performed resynthesis: Gain = %2d. Level = %2d. Req = %2d.\n", nGain, Abc_ObjLevel(pObjNew), Required );
-            Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
-//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain );
-            break;
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resynthesis for one network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
-{
-    ProgressBar * pProgress;
-    Lpk_Man_t * p;
-    Abc_Obj_t * pObj;
-    double Delta;
-    int i, Iter, nNodes, nNodesPrev, clk = clock();
-    assert( Abc_NtkIsLogic(pNtk) );
- 
-    // sweep dangling nodes as a preprocessing step
-    Abc_NtkSweep( pNtk, 0 );
-
-    // get the number of inputs
-    pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
-    if ( pPars->nLutSize > 6 )
-        pPars->nLutSize = 6;
-    if ( pPars->nLutSize < 3 )
-        pPars->nLutSize = 3;
-    // adjust the number of crossbars based on LUT size
-    if ( pPars->nVarsShared > pPars->nLutSize - 2 )
-        pPars->nVarsShared = pPars->nLutSize - 2;
-    // get the max number of LUTs tried
-    pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
-    while ( pPars->nVarsMax > 16 )
-    {
-        pPars->nLutsMax--;
-        pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1;
-
-    }
-    if ( pPars->fVerbose )
-    {
-        printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
-            pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
-    }
- 
-
-    // convert into the AIG
-    if ( !Abc_NtkToAig(pNtk) )
-    {
-        fprintf( stdout, "Converting to BDD has failed.\n" );
-        return 0;
-    }
-    assert( Abc_NtkHasAig(pNtk) );
-
-    // set the number of levels
-    Abc_NtkLevel( pNtk );
-    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
-
-    // start the manager
-    p = Lpk_ManStart( pPars );
-    p->pNtk = pNtk;
-    p->nNodesTotal = Abc_NtkNodeNum(pNtk);
-    p->vLevels = Vec_VecStart( pNtk->LevelMax ); 
-    if ( p->pPars->fSatur )
-        p->vVisited = Vec_VecStart( 0 );
-    if ( pPars->fVerbose )
-    {
-        p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
-        p->nTotalNodes = Abc_NtkNodeNum(pNtk);
-    }
-
-    // iterate over the network
-    nNodesPrev = p->nNodesTotal;
-    for ( Iter = 1; ; Iter++ )
-    {
-        // expand storage for changed nodes
-        if ( p->pPars->fSatur )
-            Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 );
-
-        // consider all nodes
-        nNodes = Abc_NtkObjNumMax(pNtk);
-        if ( !pPars->fVeryVerbose )
-            pProgress = Extra_ProgressBarStart( stdout, nNodes );
-        Abc_NtkForEachNode( pNtk, pObj, i )
-        {
-            // skip all except the final node
-            if ( pPars->fFirst )
-            {
-                if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
-                    continue;
-            }
-            if ( i >= nNodes )
-                break;
-            if ( !pPars->fVeryVerbose )
-                Extra_ProgressBarUpdate( pProgress, i, NULL );
-            // skip the nodes that did not change
-            if ( p->pPars->fSatur && !Lpk_NodeHasChanged(p, pObj->Id) )
-                continue;
-            // resynthesize
-            p->pObj = pObj;
-            if ( p->pPars->fOldAlgo )
-                Lpk_ResynthesizeNode( p );
-            else
-                Lpk_ResynthesizeNodeNew( p );
-        }
-        if ( !pPars->fVeryVerbose )
-            Extra_ProgressBarStop( pProgress );
-
-        // check the increase
-        Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal;
-        if ( Delta < 0.05 )
-            break;
-        nNodesPrev = Abc_NtkNodeNum(pNtk);
-        if ( !p->pPars->fSatur )
-            break;
-
-        if ( pPars->fFirst )
-            break;
-    }
-    Abc_NtkStopReverseLevels( pNtk );
-
-    if ( pPars->fVerbose )
-    {
-//        Cloud_PrintInfo( p->pDsdMan->dd );
-        p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
-        p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
-        printf( "Node gain = %5d. (%.2f %%)  ", 
-            p->nTotalNodes-p->nTotalNodes2, 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
-        printf( "Edge gain = %5d. (%.2f %%)  ", 
-            p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
-        printf( "Muxes = %4d. Dsds = %4d.", p->nMuxes, p->nDsds );
-        printf( "\n" );
-        printf( "Nodes = %5d (%3d)  Cuts = %5d (%4d)  Changes = %5d  Iter = %2d  Benefit = %d.\n", 
-            p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, Iter, p->nBenefited );
-
-        printf( "Non-DSD:" );
-        for ( i = 3; i <= pPars->nVarsMax; i++ )
-            if ( p->nBlocks[i] )
-                printf( " %d=%d", i, p->nBlocks[i] );
-        printf( "\n" );
-
-        p->timeTotal = clock() - clk;
-        p->timeEval  = p->timeEval  - p->timeMap;
-        p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
-        PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
-        PRTP( "Truth ", p->timeTruth, p->timeTotal );
-        PRTP( "CSupps", p->timeSupps, p->timeTotal );
-        PRTP( "Eval  ", p->timeEval,  p->timeTotal );
-        PRTP( " MuxAn", p->timeEvalMuxAn, p->timeEval );
-        PRTP( " MuxSp", p->timeEvalMuxSp, p->timeEval );
-        PRTP( " DsdAn", p->timeEvalDsdAn, p->timeEval );
-        PRTP( " DsdSp", p->timeEvalDsdSp, p->timeEval );
-        PRTP( " Other", p->timeEval-p->timeEvalMuxAn-p->timeEvalMuxSp-p->timeEvalDsdAn-p->timeEvalDsdSp, p->timeEval );
-        PRTP( "Map   ", p->timeMap,   p->timeTotal );
-        PRTP( "Other ", p->timeOther, p->timeTotal );
-        PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
-    }
-
-    Lpk_ManStop( p );
-    // check the resulting network
-    if ( !Abc_NtkCheck( pNtk ) )
-    {
-        printf( "Lpk_Resynthesize: The network check has failed.\n" );
-        return 0;
-    }
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
deleted file mode 100644
index facd330b..00000000
--- a/src/opt/lpk/lpkCut.c
+++ /dev/null
@@ -1,683 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkCut.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: lpkCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-#include "cloud.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth table of one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-CloudNode * Lpk_CutTruthBdd_rec( CloudManager * dd, Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars )
-{
-    CloudNode * pTruth, * pTruth0, * pTruth1;
-    assert( !Hop_IsComplement(pObj) );
-    if ( pObj->pData )
-    {
-        assert( ((unsigned)pObj->pData) & 0xffff0000 );
-        return pObj->pData;
-    }
-    // get the plan for a new truth table
-    if ( Hop_ObjIsConst1(pObj) )
-        pTruth = dd->one;
-    else
-    {
-        assert( Hop_ObjIsAnd(pObj) );
-        // compute the truth tables of the fanins
-        pTruth0 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin0(pObj), nVars );
-        pTruth1 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin1(pObj), nVars );
-        pTruth0 = Cloud_NotCond( pTruth0, Hop_ObjFaninC0(pObj) );
-        pTruth1 = Cloud_NotCond( pTruth1, Hop_ObjFaninC1(pObj) );
-        // creat the truth table of the node
-        pTruth = Cloud_bddAnd( dd, pTruth0, pTruth1 );
-    }
-    pObj->pData = pTruth;
-    return pTruth;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies that the factoring is correct.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-CloudNode * Lpk_CutTruthBdd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
-{
-    CloudManager * dd = p->pDsdMan->dd;
-    Hop_Man_t * pManHop = p->pNtk->pManFunc;
-    Hop_Obj_t * pObjHop;
-    Abc_Obj_t * pObj, * pFanin;
-    CloudNode * pTruth;
-    int i, k, iCount = 0;
-
-//    return NULL;
-//    Lpk_NodePrintCut( p, pCut );
-    // initialize the leaves
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)dd->vars[pCut->nLeaves-1-i];
-
-    // construct truth table in the topological order
-    Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
-    {
-        // get the local AIG
-        pObjHop = Hop_Regular(pObj->pData);
-        // clean the data field of the nodes in the AIG subgraph
-        Hop_ObjCleanData_rec( pObjHop );
-        // set the initial truth tables at the fanins
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
-            Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
-        }
-        // compute the truth table of internal nodes
-        pTruth = Lpk_CutTruthBdd_rec( dd, pManHop, pObjHop, pCut->nLeaves );
-        if ( Hop_IsComplement(pObj->pData) )
-            pTruth = Cloud_Not(pTruth);
-        // set the truth table at the node
-        pObj->pCopy = (Abc_Obj_t *)pTruth;
-        
-    }
-
-//    Cloud_bddPrint( dd, pTruth );
-//    printf( "Bdd size = %d. Total nodes = %d.\n", Cloud_DagSize( dd, pTruth ), dd->nNodesCur-dd->nVars-1 );
-    return pTruth;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth table of one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * piCount )
-{
-    unsigned * pTruth, * pTruth0, * pTruth1;
-    assert( !Hop_IsComplement(pObj) );
-    if ( pObj->pData )
-    {
-        assert( ((unsigned)pObj->pData) & 0xffff0000 );
-        return pObj->pData;
-    }
-    // get the plan for a new truth table
-    pTruth = Vec_PtrEntry( vTtNodes, (*piCount)++ );
-    if ( Hop_ObjIsConst1(pObj) )
-        Kit_TruthFill( pTruth, nVars );
-    else
-    {
-        assert( Hop_ObjIsAnd(pObj) );
-        // compute the truth tables of the fanins
-        pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, piCount );
-        pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, piCount );
-        // creat the truth table of the node
-        Kit_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
-    }
-    pObj->pData = pTruth;
-    return pTruth;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth able of one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
-{
-    Hop_Man_t * pManHop = p->pNtk->pManFunc;
-    Hop_Obj_t * pObjHop;
-    Abc_Obj_t * pObj, * pFanin;
-    unsigned * pTruth;
-    int i, k, iCount = 0;
-//    Lpk_NodePrintCut( p, pCut );
-    assert( pCut->nNodes > 0 );
-
-    // initialize the leaves
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
-        pObj->pCopy = Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i );
-
-    // construct truth table in the topological order
-    Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
-    {
-        // get the local AIG
-        pObjHop = Hop_Regular(pObj->pData);
-        // clean the data field of the nodes in the AIG subgraph
-        Hop_ObjCleanData_rec( pObjHop );
-        // set the initial truth tables at the fanins
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
-            Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
-        }
-        // compute the truth table of internal nodes
-        pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
-        if ( Hop_IsComplement(pObj->pData) )
-            Kit_TruthNot( pTruth, pTruth, pCut->nLeaves );
-        // set the truth table at the node
-        pObj->pCopy = (Abc_Obj_t *)pTruth;
-    }
-
-    // make sure direct truth table is stored elsewhere (assuming the first call for direct truth!!!)
-    if ( fInv == 0 )
-    {
-        pTruth = Vec_PtrEntry( p->vTtNodes, iCount++ );
-        Kit_TruthCopy( pTruth, (unsigned *)pObj->pCopy, pCut->nLeaves );
-    }
-    assert( iCount <= Vec_PtrSize(p->vTtNodes) );
-    return pTruth;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if at least one entry has changed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_NodeRecordImpact( Lpk_Man_t * p )
-{
-    Lpk_Cut_t * pCut;
-    Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
-    Abc_Obj_t * pNode;
-    int i, k;
-    // collect the nodes that impact the given node
-    Vec_PtrClear( vNodes );
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pCut = p->pCuts + i;
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-        {
-            pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
-            if ( pNode->fMarkC )
-                continue;
-            pNode->fMarkC = 1;
-            Vec_PtrPush( vNodes, (void *)pNode->Id );
-            Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
-        }
-    }
-    // clear the marks
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        pNode = Abc_NtkObj( p->pNtk, (int)pNode );
-        pNode->fMarkC = 0;
-        i++;
-    }
-//printf( "%d ", Vec_PtrSize(vNodes) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the cut has structural DSD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
-{
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k, nCands, fLeavesOnly, RetValue;
-    assert( pCut->nLeaves > 0 );
-    // clear ref counters
-    memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
-    // mark cut leaves
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
-    {
-        assert( pObj->fMarkA == 0 );
-        pObj->fMarkA = 1;
-        pObj->pCopy = (void *)i;
-    }
-    // ref leaves pointed from the internal nodes
-    nCands = 0;
-    Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
-    {
-        fLeavesOnly = 1;
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            if ( pFanin->fMarkA )
-                p->pRefs[(int)pFanin->pCopy]++;
-            else
-                fLeavesOnly = 0;
-        if ( fLeavesOnly )
-            p->pCands[nCands++] = pObj->Id;
-    }
-    // look at the nodes that only point to the leaves
-    RetValue = 0;
-    for ( i = 0; i < nCands; i++ )
-    {
-        pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            assert( pFanin->fMarkA == 1 );
-            if ( p->pRefs[(int)pFanin->pCopy] > 1 )
-                break;
-        }
-        if ( k == Abc_ObjFaninNum(pObj) )
-        {
-            RetValue = 1;
-            break;
-        }
-    }
-    // unmark cut leaves
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
-        pObj->fMarkA = 0;
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pDom is contained in pCut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut )
-{
-    int i, k;
-    for ( i = 0; i < (int)pDom->nLeaves; i++ )
-    {
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                break;
-        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-            return 0;
-    }
-    // every node in pDom is contained in pCut
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check if the cut exists.]
-
-  Description [Returns 1 if the cut exists.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew )
-{
-    Lpk_Cut_t * pCut;
-    int i, k;
-    assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
-    // try to find the cut
-    for ( i = 0; i < nCuts; i++ )
-    {
-        pCut = pCuts + i;
-        if ( pCut->nLeaves == 0 )
-            continue;
-        if ( pCut->nLeaves == pCutNew->nLeaves )
-        {
-            if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
-            {
-                for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
-                    if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
-                        break;
-                if ( k == (int)pCutNew->nLeaves )
-                    return 1;
-            }
-            continue;
-        }
-        if ( pCut->nLeaves < pCutNew->nLeaves )
-        {
-            // skip the non-contained cuts
-            if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
-                continue;
-            if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
-                continue;
-            // check containment seriously
-            if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) )
-                return 1;
-            continue;
-        }
-        // check potential containment of other cut
-
-        // skip the non-contained cuts
-        if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
-            continue;
-        if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
-            continue;
-        // check containment seriously
-        if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) )
-            pCut->nLeaves = 0; // removed
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the given cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly )
-{
-    Abc_Obj_t * pObj;
-    int i;
-    if ( !fLeavesOnly )
-        printf( "LEAVES:\n" );
-    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
-        printf( "%d,", pObj->Id );
-    if ( !fLeavesOnly )
-    {
-        printf( "\nNODES:\n" );
-        Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
-        {
-            printf( "%d,", pObj->Id );
-            assert( Abc_ObjIsNode(pObj) );
-        }
-        printf( "\n" );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Set the cut signature.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_NodeCutSignature( Lpk_Cut_t * pCut )
-{
-    unsigned i;
-    pCut->uSign[0] = pCut->uSign[1] = 0;
-    for ( i = 0; i < pCut->nLeaves; i++ )
-    {
-        pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
-        if ( i != pCut->nLeaves - 1 )
-            assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the set of all cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
-{
-    Lpk_Cut_t * pCutNew;
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k, j, nLeavesNew;
-/*
-    printf( "Exploring cut " );
-    Lpk_NodePrintCut( p, pCut, 1 );
-    printf( "with node %d\n", Node );
-*/
-    // check if the cut can stand adding one more internal node
-    if ( pCut->nNodes == LPK_SIZE_MAX )
-        return;
-
-    // if the node is a PI, quit
-    pObj = Abc_NtkObj( p->pNtk, Node );
-    if ( Abc_ObjIsCi(pObj) )
-        return;
-    assert( Abc_ObjIsNode(pObj) );
-//    assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
-
-    // if the node is not in the MFFC, check the limit
-    if ( !Abc_NodeIsTravIdCurrent(pObj) )
-    {
-        if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
-            return;
-        assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
-    }
-
-    // check the possibility of adding this node using the signature
-    nLeavesNew = pCut->nLeaves - 1;
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-    {
-        if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
-            continue;
-        if ( ++nLeavesNew > p->pPars->nVarsMax )
-            return;
-    }
-
-    // initialize the set of leaves to the nodes in the cut
-    assert( p->nCuts < LPK_CUTS_MAX );
-    pCutNew = p->pCuts + p->nCuts;
-    pCutNew->nLeaves = 0;
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        if ( pCut->pLeaves[i] != Node )
-            pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
-
-    // add new nodes
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-    {
-        // find the place where this node belongs
-        for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
-            if ( pCutNew->pLeaves[k] >= pFanin->Id )
-                break;
-        if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
-            continue;
-        // check if there is room
-        if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
-            return;
-        // move all the nodes
-        for ( j = pCutNew->nLeaves; j > k; j-- )
-            pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
-        pCutNew->pLeaves[k] = pFanin->Id;
-        pCutNew->nLeaves++;
-        assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
-
-    }
-    // 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->nNodesDup = pCut->nNodesDup;
-
-    // check if the node is already there
-    // if so, move the node to be the last
-    for ( i = 0; i < (int)pCutNew->nNodes; i++ )
-        if ( pCutNew->pNodes[i] == Node )
-        {
-            for ( k = i; k < (int)pCutNew->nNodes - 1; k++ )
-                pCutNew->pNodes[k] = pCutNew->pNodes[k+1];
-            pCutNew->pNodes[k] = 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++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the set of all cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_NodeCuts( Lpk_Man_t * p )
-{
-    Lpk_Cut_t * pCut, * pCut2;
-    int i, k, Temp, nMffc, fChanges;
-
-    // mark the MFFC of the node with the current trav ID
-    nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
-    assert( nMffc > 0 );
-    if ( nMffc == 1 )
-        return 0;
-
-    // initialize the first cut
-    pCut = p->pCuts; p->nCuts = 1;
-    pCut->nNodes = 0; 
-    pCut->nNodesDup = 0;
-    pCut->nLeaves = 1;
-    pCut->pLeaves[0] = p->pObj->Id;
-    // assign the signature
-    Lpk_NodeCutSignature( pCut );
-
-    // perform the cut computation
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pCut = p->pCuts + i;
-        if ( pCut->nLeaves == 0 )
-            continue;
-
-        // try to expand the fanins of this cut
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-        {
-            // create a new cut
-            Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
-            // quit if the number of cuts has exceeded the limit
-            if ( p->nCuts == LPK_CUTS_MAX )
-                break;
-        }
-        if ( p->nCuts == LPK_CUTS_MAX )
-            break;
-    }
-    if ( p->nCuts == LPK_CUTS_MAX ) 
-        p->nNodesOver++;
-
-    // record the impact of this node
-    if ( p->pPars->fSatur )
-        Lpk_NodeRecordImpact( p );
-
-    // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
-    p->nEvals = 0;
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pCut = p->pCuts + i;
-        if ( pCut->nLeaves < 2 )
-            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 = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); 
-//        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup - 1) / pCut->nLuts; //p->pPars->nLutsMax;
-        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
-        if ( pCut->Weight <= 1.001 )
-//        if ( pCut->Weight <= 0.999 )
-            continue;
-        pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
-        if ( pCut->fHasDsd )
-            continue;
-        p->pEvals[p->nEvals++] = i;
-    }
-    if ( p->nEvals == 0 )
-        return 0;
-
-    // sort the cuts by Weight
-    do {
-        fChanges = 0;
-        for ( i = 0; i < p->nEvals - 1; i++ )
-        {
-            pCut = p->pCuts + p->pEvals[i];
-            pCut2 = p->pCuts + p->pEvals[i+1];
-            if ( pCut->Weight >= pCut2->Weight - 0.001 )
-                continue;
-            Temp = p->pEvals[i];
-            p->pEvals[i] = p->pEvals[i+1];
-            p->pEvals[i+1] = Temp;
-            fChanges = 1;
-        }
-    } while ( fChanges );
-/*
-    for ( i = 0; i < p->nEvals; i++ )
-    {
-        pCut = p->pCuts + p->pEvals[i];
-        printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
-    }
-    printf( "\n" );
-*/
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
deleted file mode 100644
index 960599e4..00000000
--- a/src/opt/lpk/lpkInt.h
+++ /dev/null
@@ -1,246 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkInt.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Fast Boolean matching for LUT structures.]
-
-  Synopsis    [Internal declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - April 28, 2007.]
-
-  Revision    [$Id: lpkInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __LPK_INT_H__
-#define __LPK_INT_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include "abc.h"
-#include "kit.h"
-#include "if.h"
-#include "lpk.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define LPK_SIZE_MAX             24     // the largest size of the function
-#define LPK_CUTS_MAX            512     // the largest number of cuts considered
-
-typedef struct Lpk_Man_t_ Lpk_Man_t;
-typedef struct Lpk_Cut_t_ Lpk_Cut_t;
-
-struct Lpk_Cut_t_
-{
-    unsigned     nLeaves       : 6;     // (L) the number of leaves
-    unsigned     nNodes        : 6;     // (M) the number of nodes
-    unsigned     nNodesDup     : 6;     // (Q) nodes outside of MFFC
-    unsigned     nLuts         : 6;     // (N) the number of LUTs to try
-    unsigned     unused        : 6;     // unused
-    unsigned     fHasDsd       : 1;     // set to 1 if the cut has structural DSD (and so cannot be used)
-    unsigned     fMark         : 1;     // multipurpose mark
-    unsigned     uSign[2];              // the signature
-    float        Weight;                // the weight of the cut: (M - Q)/N(V)   (the larger the better)
-    int          Gain;                  // the gain achieved using this cut
-    int          pLeaves[LPK_SIZE_MAX]; // the leaves of the cut
-    int          pNodes[LPK_SIZE_MAX];  // the nodes of the cut
-};
-
-struct Lpk_Man_t_
-{
-    // parameters
-    Lpk_Par_t *  pPars;                 // the set of parameters
-    // current representation
-    Abc_Ntk_t *  pNtk;                  // the network
-    Abc_Obj_t *  pObj;                  // the node to resynthesize 
-    // cut representation
-    int          nMffc;                 // the size of MFFC of the node
-    int          nCuts;                 // the total number of cuts    
-    int          nCutsMax;              // the largest possible number of cuts
-    int          nEvals;                // the number of good cuts
-    Lpk_Cut_t    pCuts[LPK_CUTS_MAX];   // the storage for cuts
-    int          pEvals[LPK_CUTS_MAX];  // the good cuts
-    // visited nodes 
-    Vec_Vec_t *  vVisited;
-    // mapping manager
-    If_Man_t *   pIfMan;
-    Vec_Int_t *  vCover; 
-    Vec_Vec_t *  vLevels;
-    // temporary variables
-    int          fCofactoring;          // working in the cofactoring mode
-    int          fCalledOnce;           // limits the depth of MUX cofactoring
-    int          nCalledSRed;           // the number of called to SRed
-    int          pRefs[LPK_SIZE_MAX];   // fanin reference counters 
-    int          pCands[LPK_SIZE_MAX];  // internal nodes pointing only to the leaves
-    Vec_Ptr_t *  vLeaves;
-    // truth table representation
-    Vec_Ptr_t *  vTtElems;              // elementary truth tables
-    Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
-    Vec_Int_t *  vMemory;
-    Vec_Int_t *  vBddDir;
-    Vec_Int_t *  vBddInv;
-    unsigned     puSupps[32];           // the supports of the cofactors
-    unsigned *   ppTruths[5][16];
-    // variable sets
-    Vec_Int_t *  vSets[8];
-    Kit_DsdMan_t* pDsdMan;
-    // statistics
-    int          nNodesTotal;           // total number of nodes
-    int          nNodesOver;            // nodes with cuts over the limit 
-    int          nCutsTotal;            // total number of cuts
-    int          nCutsUseful;           // useful cuts 
-    int          nGainTotal;            // the gain in LUTs
-    int          nChanges;              // the number of changed nodes
-    int          nBenefited;            // the number of gainful that benefited from decomposition
-    int          nMuxes;
-    int          nDsds;
-    int          nTotalNets;
-    int          nTotalNets2;
-    int          nTotalNodes;
-    int          nTotalNodes2;
-    // counter of non-DSD blocks
-    int          nBlocks[17];
-    // runtime
-    int          timeCuts;
-    int          timeTruth;
-    int          timeSupps;
-    int          timeTruth2;
-    int          timeTruth3;
-    int          timeEval;
-    int          timeMap;
-    int          timeOther;
-    int          timeTotal;
-    // runtime of eval
-    int          timeEvalMuxAn;
-    int          timeEvalMuxSp;
-    int          timeEvalDsdAn;
-    int          timeEvalDsdSp;
- 
-};
-
-
-// internal representation of the function to be decomposed
-typedef struct Lpk_Fun_t_ Lpk_Fun_t;
-struct Lpk_Fun_t_
-{
-    Vec_Ptr_t *  vNodes;           // the array of leaves and decomposition nodes
-    unsigned     Id         :  7;  // the ID of this node
-    unsigned     nVars      :  5;  // the number of variables
-    unsigned     nLutK      :  4;  // the number of LUT inputs
-    unsigned     nAreaLim   :  5;  // the area limit (the largest allowed)
-    unsigned     nDelayLim  :  9;  // the delay limit (the largest allowed)
-    unsigned     fSupports  :  1;  // supports of cofactors were precomputed
-    unsigned     fMark      :  1;  // marks the MUX-based dec
-    unsigned     uSupp;            // the support of this component
-    unsigned     puSupps[32];      // the supports of the cofactors
-    char         pDelays[16];      // the delays of the inputs
-    char         pFanins[16];      // the fanins of this function
-    unsigned     pTruth[0];        // the truth table (contains room for three truth tables)    
-};
-
-// preliminary decomposition result
-typedef struct Lpk_Res_t_ Lpk_Res_t;
-struct Lpk_Res_t_
-{
-    int          nBSVars;          // the number of bound set variables
-    unsigned     BSVars;           // the bound set
-    int          nCofVars;         // the number of cofactoring variables
-    char         pCofVars[4];      // the cofactoring variables
-    int          nSuppSizeS;       // support size of the smaller (decomposed) function 
-    int          nSuppSizeL;       // support size of the larger (composition) function
-    int          DelayEst;         // estimated delay of the decomposition
-    int          AreaEst;          // estimated area of the decomposition
-    int          Variable;         // variable in MUX decomposition
-    int          Polarity;         // polarity in MUX decomposition
-};
-
-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                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                           ITERATORS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i )                                        \
-    for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
-#define Lpk_CutForEachNode( pNtk, pCut, pObj, i )                                        \
-    for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
-#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i )                                 \
-    for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
-#define Lpk_SuppForEachVar( Supp, Var )\
-    for ( Var = 0; Var < 16; Var++ )\
-        if ( !(Supp & (1<<Var)) ) {} else
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== lpkAbcDec.c ============================================================*/
-extern Abc_Obj_t *    Lpk_Decompose( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim );
-/*=== lpkAbcDsd.c ============================================================*/
-extern Lpk_Res_t *    Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared );
-extern Lpk_Fun_t *    Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
-/*=== lpkAbcMux.c ============================================================*/
-extern Lpk_Res_t *    Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p );
-extern Lpk_Fun_t *    Lpk_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol );
-/*=== lpkAbcUtil.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 int            Lpk_FunSuppMinimize( Lpk_Fun_t * p );
-extern void           Lpk_FunComputeCofSupps( Lpk_Fun_t * p );
-extern int            Lpk_SuppDelay( unsigned uSupp, char * pDelays );
-extern int            Lpk_SuppToVars( unsigned uBoundSet, char * pVars );
-
-
-/*=== lpkCut.c =========================================================*/
-extern unsigned *     Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv );
-extern int            Lpk_NodeCuts( Lpk_Man_t * p );
-/*=== lpkMap.c =========================================================*/
-extern Lpk_Man_t *    Lpk_ManStart( Lpk_Par_t * pPars );
-extern void           Lpk_ManStop( Lpk_Man_t * p );
-/*=== lpkMap.c =========================================================*/
-extern If_Obj_t *     Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
-extern If_Obj_t *     Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
-/*=== lpkMulti.c =======================================================*/
-extern If_Obj_t *     Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
-/*=== lpkMux.c =========================================================*/
-extern If_Obj_t *     Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
-extern If_Obj_t *     Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
-/*=== lpkSets.c =========================================================*/
-extern unsigned       Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
deleted file mode 100644
index af6a5307..00000000
--- a/src/opt/lpk/lpkMan.c
+++ /dev/null
@@ -1,122 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkMan.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: lpkMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
-{
-    Lpk_Man_t * p;
-    int i, nWords;
-    assert( pPars->nLutsMax <= 16 );
-    assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 );
-    p = ALLOC( Lpk_Man_t, 1 );
-    memset( p, 0, sizeof(Lpk_Man_t) );
-    p->pPars = pPars;
-    p->nCutsMax = LPK_CUTS_MAX;
-    p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
-    p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
-    p->vCover = Vec_IntAlloc( 1 << 12 );
-    p->vLeaves = Vec_PtrAlloc( 32 );
-    for ( i = 0; i < 8; i++ )
-        p->vSets[i] = Vec_IntAlloc(100);
-    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
-    p->vMemory = Vec_IntAlloc( 1024 * 32 );
-    p->vBddDir = Vec_IntAlloc( 256 );
-    p->vBddInv = Vec_IntAlloc( 256 );
-    // allocate temporary storage for truth tables
-    nWords = Kit_TruthWordNum(pPars->nVarsMax);
-    p->ppTruths[0][0] = ALLOC( unsigned, 32 * nWords );
-    p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords;
-    for ( i = 1; i < 2; i++ )
-        p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords;
-    p->ppTruths[2][0] = p->ppTruths[1][0] + 2 * nWords;
-    for ( i = 1; i < 4; i++ )
-        p->ppTruths[2][i] = p->ppTruths[2][0] + i * nWords;
-    p->ppTruths[3][0] = p->ppTruths[2][0] + 4 * nWords; 
-    for ( i = 1; i < 8; i++ )
-        p->ppTruths[3][i] = p->ppTruths[3][0] + i * nWords;
-    p->ppTruths[4][0] = p->ppTruths[3][0] + 8 * nWords; 
-    for ( i = 1; i < 16; i++ )
-        p->ppTruths[4][i] = p->ppTruths[4][0] + i * nWords;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_ManStop( Lpk_Man_t * p )
-{
-    int i;
-    free( p->ppTruths[0][0] );
-    Vec_IntFree( p->vBddDir );
-    Vec_IntFree( p->vBddInv );
-    Vec_IntFree( p->vMemory );
-    Kit_DsdManFree( p->pDsdMan );
-    for ( i = 0; i < 8; i++ )
-        Vec_IntFree(p->vSets[i]);
-    if ( p->pIfMan )
-    {
-        void * pPars = p->pIfMan->pPars;
-        If_ManStop( p->pIfMan );
-        free( pPars );
-    }
-    if ( p->vLevels )
-        Vec_VecFree( p->vLevels );
-    if ( p->vVisited )
-        Vec_VecFree( p->vVisited );
-    Vec_PtrFree( p->vLeaves );
-    Vec_IntFree( p->vCover );
-    Vec_PtrFree( p->vTtElems );
-    Vec_PtrFree( p->vTtNodes );
-    free( p );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c
deleted file mode 100644
index 698aeea1..00000000
--- a/src/opt/lpk/lpkMap.c
+++ /dev/null
@@ -1,205 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkMap.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: lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Transforms the decomposition graph into the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph )
-{
-    Kit_Node_t * pNode;
-    If_Obj_t * pAnd0, * pAnd1;
-    int i;
-    // check for constant function
-    if ( Kit_GraphIsConst(pGraph) )
-        return If_ManConst1(pIfMan);
-    // check for a literal
-    if ( Kit_GraphIsVar(pGraph) )
-        return Kit_GraphVar(pGraph)->pFunc;
-    // build the AIG nodes corresponding to the AND gates of the graph
-    Kit_GraphForEachNode( pGraph, pNode, i )
-    {
-        pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; 
-        pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; 
-        pNode->pFunc = If_ManCreateAnd( pIfMan, 
-            If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ), 
-            If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) );
-    }
-    return pNode->pFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Strashes one logic node using its SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
-{
-    Kit_Graph_t * pGraph;
-    Kit_Node_t * pNode;
-    If_Obj_t * pRes;
-    int i;
-    // derive the factored form
-    pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
-    if ( pGraph == NULL )
-        return NULL;
-    // collect the fanins
-    Kit_GraphForEachLeaf( pGraph, pNode, i )
-        pNode->pFunc = ppLeaves[i];
-    // perform strashing
-    pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
-    pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
-    Kit_GraphFree( pGraph );
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
-{
-    Kit_DsdObj_t * pObj;
-    If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
-    unsigned i, iLitFanin;
-
-    assert( iLit >= 0 );
-
-    // consider the case of a gate
-    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
-    if ( pObj == NULL )
-    {
-        pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)];
-        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
-    }
-    if ( pObj->Type == KIT_DSD_CONST1 )
-    {
-        return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) );
-    }
-    if ( pObj->Type == KIT_DSD_VAR )
-    {
-        pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])];
-        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) );
-    }
-    if ( pObj->Type == KIT_DSD_AND )
-    {
-        assert( pObj->nFans == 2 );
-        pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
-        pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
-        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
-            return NULL;
-        pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] ); 
-        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
-    }
-    if ( pObj->Type == KIT_DSD_XOR )
-    {
-        int fCompl = Kit_DsdLitIsCompl(iLit);
-        assert( pObj->nFans == 2 );
-        pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
-        pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
-        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
-            return NULL;
-        fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
-        pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
-        return If_NotCond( pObjNew, fCompl );
-    }
-    assert( pObj->Type == KIT_DSD_PRIME );
-    p->nBlocks[pObj->nFans]++;
-
-    // solve for the inputs
-    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
-    {
-        if ( i == 0 )
-            pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
-        else
-            pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
-        if ( pFansNew[i] == NULL )
-            return NULL;
-    }
-/* 
-    if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
-    {
-        pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
-    }
-*/
-/*
-    if ( (int)pObj->nFans > p->pPars->nLutSize )
-    {
-        pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-//        if ( pObjNew2 )
-//            return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
-    }
-*/
-
-    // find best cofactoring variable
-    if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
-    {
-        pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-        if ( pObjNew2 )
-            return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
-    }
-
-    pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-
-    // add choice
-    if ( pObjNew && pObjNew2 )
-    {
-        If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
-        If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
-    }
-    return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c
deleted file mode 100644
index 82cf3578..00000000
--- a/src/opt/lpk/lpkMulti.c
+++ /dev/null
@@ -1,495 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkMulti.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: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Records variable order.]
-
-  Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
-{
-    Kit_DsdObj_t * pObj;
-    unsigned uSuppFanins, k;
-    int Above[16], Below[16];
-    int nAbove, nBelow, iFaninLit, i, x, y;
-    // iterate through the nodes
-    Kit_DsdNtkForEachObj( pNtk, pObj, i )
-    {
-        // collect fanin support of this node
-        nAbove = 0;
-        uSuppFanins = 0;
-        Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
-        {
-            if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
-                Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
-            else
-                uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
-        }
-        // find the below variables
-        nBelow = 0;
-        for ( y = 0; y < 16; y++ )
-            if ( uSuppFanins & (1 << y) )
-                Below[nBelow++] = y;
-        // create all pairs
-        for ( x = 0; x < nAbove; x++ )
-            for ( y = 0; y < nBelow; y++ )
-                pTable[Above[x]][Below[y]]++;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates commmon variable order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose )
-{
-    int Score[16] = {0}, pPres[16];
-    int i, y, x, iVarBest, ScoreMax, PrioCount;
-
-    // mark the present variables
-    for ( i = 0; i < nVars; i++ )
-        pPres[i] = 1;
-    // remove cofactored variables
-    for ( i = 0; i < nCBars; i++ )
-        pPres[piCofVar[i]] = 0;
-
-    // compute scores for each leaf
-    for ( i = 0; i < nVars; i++ )
-    {
-        if ( pPres[i] == 0 )
-            continue;
-        for ( y = 0; y < nVars; y++ )
-            Score[i] += pTable[i][y];
-        for ( x = 0; x < nVars; x++ )
-            Score[i] -= pTable[x][i];
-    }
-
-    // print the scores
-    if ( fVerbose )
-    {
-        printf( "Scores: " );
-        for ( i = 0; i < nVars; i++ )
-            printf( "%c=%d ", 'a'+i, Score[i] );
-        printf( "   " );
-        printf( "Prios: " );
-    }
-
-    // derive variable priority
-    // variables with equal score receive the same priority
-    for ( i = 0; i < nVars; i++ )
-        pPrios[i] = 16;
-
-    // iterate until variables remain
-    for ( PrioCount = 1; ; PrioCount++ )
-    {
-        // find the present variable with the highest score
-        iVarBest = -1;
-        ScoreMax = -100000;
-        for ( i = 0; i < nVars; i++ )
-        {
-            if ( pPres[i] == 0 )
-                continue;
-            if ( ScoreMax < Score[i] )
-            {
-                ScoreMax = Score[i];
-                iVarBest = i;
-            }
-        }
-        if ( iVarBest == -1 )
-            break;
-        // give the next priority to all vars having this score
-        if ( fVerbose )
-            printf( "%d=", PrioCount );
-        for ( i = 0; i < nVars; i++ )
-        {
-            if ( pPres[i] == 0 )
-                continue;
-            if ( Score[i] == ScoreMax )
-            {
-                pPrios[i] = PrioCount;
-                pPres[i] = 0;
-                if ( fVerbose )
-                    printf( "%c", 'a'+i );
-            }
-        }
-        if ( fVerbose )
-            printf( " " );
-    }
-    if ( fVerbose )
-        printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finds components with the highest priority.]
-
-  Description [Returns the number of components selected.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision )
-{
-    Kit_DsdObj_t * pObj;
-    unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
-    int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
-
-    // find individual support and total support 
-    uSuppTotal = 0;
-    for ( i = 0; i < nSize; i++ )
-    {
-        pTriv[i] = 1;
-        if ( piLits[i] < 0 ) 
-            uSupps[i] = 0;
-        else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
-            uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
-        else
-        {
-            pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
-            if ( pObj->Type == KIT_DSD_PRIME )
-            {
-                pTriv[i] = 0;
-                uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
-            }
-            else
-            {
-                assert( pObj->nFans == 2 );
-                if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
-                    pTriv[i] = 0;
-                uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
-            }
-            uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
-        }
-        assert( uSupps[i] <= 0xFFFF );
-        uSuppTotal |= uSupps[i];
-    }
-    if ( uSuppTotal == 0 )
-        return 0;
-
-    // find one support variable with the highest priority
-    PrioMin = ABC_INFINITY;
-    iVarMax = -1;
-    for ( i = 0; i < 16; i++ )
-        if ( uSuppTotal & (1 << i) )
-            if ( PrioMin > pPrio[i] )
-            {
-                PrioMin = pPrio[i];
-                iVarMax = i;
-            }
-    assert( iVarMax != -1 );
-
-    // select components, which have this variable
-    nComps = 0;
-    fOneNonTriv = 0;
-    uSuppLarge = 0;
-    for ( i = 0; i < nSize; i++ )
-        if ( uSupps[i] & (1<<iVarMax) )
-        {
-            if ( pTriv[i] || !fOneNonTriv )
-            {
-                if ( !pTriv[i] )
-                {
-                    uSuppLarge = uSupps[i];
-                    fOneNonTriv = 1;
-                }
-                pDecision[i] = 1;
-                nComps++;
-            }
-            else
-                pDecision[i] = 0;
-        }
-        else
-            pDecision[i] = 0;
-
-    // add other non-trivial not-taken components whose support is contained in the current large component support
-    if ( fOneNonTriv )
-        for ( i = 0; i < nSize; i++ )
-            if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
-            {
-                pDecision[i] = 1;
-                nComps++;
-            }
-
-    return nComps;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapTreeMulti_rec( Lpk_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pPrio )
-{
-    Kit_DsdObj_t * pObj;
-    If_Obj_t * pObjsNew[4][8], * pResPrev;
-    int piLitsNew[8], pDecision[8];
-    int i, k, nComps, nSize;
-
-    // find which of the variables is highest in the order
-    nSize = (1 << nCBars);
-    nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
-    if ( nComps == 0 )
-        return If_Not( If_ManConst1(p->pIfMan) );
-
-    // iterate over the nodes
-    if ( p->pPars->fVeryVerbose )
-        printf( "Decision: " );
-    for ( i = 0; i < nSize; i++ )
-    {
-        if ( pDecision[i] )
-        {
-            if ( p->pPars->fVeryVerbose )
-                printf( "%d ", i );
-            assert( piLits[i] >= 0 );
-            pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
-            if ( pObj == NULL )
-                piLitsNew[i] = -2;
-            else if ( pObj->Type == KIT_DSD_PRIME )
-                piLitsNew[i] = pObj->pFans[0];
-            else
-                piLitsNew[i] = pObj->pFans[1];
-        }
-        else
-            piLitsNew[i] = piLits[i];
-    }
-    if ( p->pPars->fVeryVerbose )
-        printf( "\n" );
-
-    // call again
-    pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
-
-    // create new set of nodes
-    for ( i = 0; i < nSize; i++ )
-    {
-        if ( pDecision[i] )
-            pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
-        else if ( piLits[i] == -1 )
-            pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
-        else if ( piLits[i] == -2 )
-            pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
-        else
-            pObjsNew[nCBars][i] = pResPrev;
-    }
-
-    // create MUX using these outputs
-    for ( k = nCBars; k > 0; k-- )
-    {
-        nSize /= 2;
-        for ( i = 0; i < nSize; i++ )
-            pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
-    }
-    assert( nSize == 1 );
-    return pObjsNew[0][0];  
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
-{
-    static Counter = 0;
-    If_Obj_t * pResult;
-    Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
-    Kit_DsdObj_t * pRoot;
-    int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
-    int i, k, nCBars, nSize, nMemSize;
-    unsigned * ppCofs[4][8], uSupport;
-    char pTable[16][16] = {0};
-    int fVerbose = p->pPars->fVeryVerbose;
-
-    Counter++;
-//    printf( "Run %d.\n", Counter );
-
-    // allocate storage for cofactors
-    nMemSize = Kit_TruthWordNum(nVars);
-    ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
-    nSize = 0;
-    for ( i = 0; i < 4; i++ )
-    for ( k = 0; k < 8; k++ )
-        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
-    assert( nSize == 32 );
-
-    // find the best cofactoring variables
-    nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
-//    nCBars = 2;
-//    piCofVar[0] = 0;
-//    piCofVar[1] = 1;
-
-
-    // copy the function
-    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
-
-    // decompose w.r.t. these variables
-    for ( k = 0; k < nCBars; k++ )
-    {
-        nSize = (1 << k);
-        for ( i = 0; i < nSize; i++ )
-        {
-            Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
-            Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
-        }
-    }
-    nSize = (1 << nCBars);
-    // compute DSD networks
-    for ( i = 0; i < nSize; i++ )
-    {
-        ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
-        ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
-        Kit_DsdNtkFree( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Cof%d%d: ", nCBars, i );
-            Kit_DsdPrint( stdout, ppNtks[i] );
-        }
-    }
-
-    // compute variable frequences
-    for ( i = 0; i < nSize; i++ )
-    {
-        uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
-        for ( k = 0; k < nVars; k++ )
-            if ( uSupport & (1<<k) )
-                pFreqs[k]++;
-    }
-
-    // find common variable order
-    for ( i = 0; i < nSize; i++ )
-    {
-        Kit_DsdGetSupports( ppNtks[i] );
-        Lpk_CreateVarOrder( ppNtks[i], pTable );
-    }
-    Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
-    // update priorities with frequences
-    for ( i = 0; i < nVars; i++ )
-        pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
-
-    if ( fVerbose )
-        printf( "After restructuring with priority:\n" );
-
-    if ( Counter == 1 )
-    {
-        int x = 0;
-    }
-    // transform all networks according to the variable order
-    for ( i = 0; i < nSize; i++ )
-    {
-        ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
-        Kit_DsdNtkFree( pTemp );
-        Kit_DsdGetSupports( ppNtks[i] );
-        assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
-        // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
-        Kit_DsdRotate( ppNtks[i], pFreqs );
-        // print the resulting networks
-        if ( fVerbose )
-        {
-            printf( "Cof%d%d: ", nCBars, i );
-            Kit_DsdPrint( stdout, ppNtks[i] );
-        }
-    }
- 
-    for ( i = 0; i < nSize; i++ )
-    {
-        // collect the roots
-        pRoot = Kit_DsdNtkRoot(ppNtks[i]);
-        if ( pRoot->Type == KIT_DSD_CONST1 )
-            piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1;
-        else if ( pRoot->Type == KIT_DSD_VAR )
-            piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) );
-        else
-            piLits[i] = ppNtks[i]->Root;
-    }
-
-
-    // recursively construct AIG for mapping
-    p->fCofactoring = 1;
-    pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
-    p->fCofactoring = 0;
-
-    if ( fVerbose )
-        printf( "\n" );
-
-    // verify the transformations
-    nSize = (1 << nCBars);
-    for ( i = 0; i < nSize; i++ )
-        Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
-    // mux the truth tables
-    for ( k = nCBars-1; k >= 0; k-- )
-    {
-        nSize = (1 << k);
-        for ( i = 0; i < nSize; i++ )
-            Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
-    }
-    if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
-        printf( "Verification failed.\n" );
-
-
-    // free the networks
-    for ( i = 0; i < 8; i++ )
-        if ( ppNtks[i] )
-            Kit_DsdNtkFree( ppNtks[i] );
-    free( ppCofs[0][0] );
-
-    return pResult;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c
deleted file mode 100644
index ed046ad7..00000000
--- a/src/opt/lpk/lpkMux.c
+++ /dev/null
@@ -1,247 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkMux.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: lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Find the best cofactoring variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Lpk_MapTreeBestCofVar( Lpk_Man_t * p, unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
-{
-    int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
-    // iterate through variables
-    iBestVar = -1;
-    nSuppSizeMin = KIT_INFINITY;
-    for ( i = 0; i < nVars; i++ )
-    {
-        // cofactor the functiona and get support sizes
-        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
-        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
-        nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
-        nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
-        nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
-        // skip cofactoring that goes above the limit
-        if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize )
-            continue;
-        // compare this variable with other variables
-        if ( nSuppSizeMin > nSuppSizeCur ) 
-        {
-            nSuppSizeMin = nSuppSizeCur;
-            iBestVar = i;
-        }
-    }
-    // cofactor w.r.t. this variable
-    if ( iBestVar != -1 )
-    {
-        Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
-        Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
-    }
-    return iBestVar;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Maps the function by the best cofactoring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
-{
-    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
-    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
-    If_Obj_t * pObj0, * pObj1;
-    Kit_DsdNtk_t * ppNtks[2];
-    int iBestVar;
-    assert( nVars > 3 );
-    p->fCalledOnce = 1;
-    // cofactor w.r.t. the best variable
-    iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
-    if ( iBestVar == -1 )
-        return NULL;
-    // decompose the functions
-    ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
-    ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
-    if ( p->pPars->fVeryVerbose )
-    {
-        printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n", 
-            'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
-        Kit_DsdPrintExpanded( ppNtks[0] );
-        Kit_DsdPrintExpanded( ppNtks[1] );
-    }
-    // map the DSD structures
-    pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
-    pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
-    Kit_DsdNtkFree( ppNtks[0] );
-    Kit_DsdNtkFree( ppNtks[1] );
-    return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Implements support-reducing decomposition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
-{
-    Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
-    If_Obj_t * pObjNew;
-    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes,  0 );
-    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes,  1 );
-    unsigned * pDec0 = Vec_PtrEntry( p->vTtNodes,  2 );
-    unsigned * pDec1 = Vec_PtrEntry( p->vTtNodes,  3 );
-    unsigned * pDec  = Vec_PtrEntry( p->vTtNodes,  4 );
-    unsigned * pCo00 = Vec_PtrEntry( p->vTtNodes,  5 );
-    unsigned * pCo01 = Vec_PtrEntry( p->vTtNodes,  6 );
-    unsigned * pCo10 = Vec_PtrEntry( p->vTtNodes,  7 );
-    unsigned * pCo11 = Vec_PtrEntry( p->vTtNodes,  8 );
-    unsigned * pCo0  = Vec_PtrEntry( p->vTtNodes,  9 );
-    unsigned * pCo1  = Vec_PtrEntry( p->vTtNodes, 10 );
-    unsigned * pCo   = Vec_PtrEntry( p->vTtNodes, 11 );
-    int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
-    int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
-
-    // determine if supp-red decomposition exists
-    uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
-    if ( uSubsets == 0 )
-        return NULL;
-    p->nCalledSRed++;
-
-    // get the cofactors
-    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
-    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
-
-    // get the bound sets
-    uSubset0 = uSubsets & 0xFFFF;
-    uSubset1 = uSubsets >> 16;
-
-    // compute the decomposed functions
-    ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
-    ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
-    ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
-    ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
-    Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
-    Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
-//    Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 );
-//    Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 );
-    Kit_DsdNtkFree( ppNtks[0] );
-    Kit_DsdNtkFree( ppNtks[1] );
-//Kit_DsdPrintFromTruth( pDec0, nVars );
-//Kit_DsdPrintFromTruth( pDec1, nVars );
-    // get the decomposed function
-    Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
-
-    // find any true assignments of the decomposed functions
-    TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
-    TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
-    assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
-    // find any false assignments of the decomposed functions
-    FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
-    FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
-    assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
-
-    // cofactor the cofactors according to these minterms
-    Kit_TruthCopy( pCo00, pCof0, nVars );
-    Kit_TruthCopy( pCo01, pCof0, nVars );
-    for ( i = 0; i < nVars; i++ )
-        if ( uSubset0 & (1 << i) )
-        {
-            if ( FalseMint0 & (1 << i) )
-                Kit_TruthCofactor1( pCo00, nVars, i );
-            else
-                Kit_TruthCofactor0( pCo00, nVars, i );
-            if ( TrueMint0 & (1 << i) )
-                Kit_TruthCofactor1( pCo01, nVars, i );
-            else
-                Kit_TruthCofactor0( pCo01, nVars, i );
-        }
-    Kit_TruthCopy( pCo10, pCof1, nVars );
-    Kit_TruthCopy( pCo11, pCof1, nVars );
-    for ( i = 0; i < nVars; i++ )
-        if ( uSubset1 & (1 << i) )
-        {
-            if ( FalseMint1 & (1 << i) )
-                Kit_TruthCofactor1( pCo10, nVars, i );
-            else
-                Kit_TruthCofactor0( pCo10, nVars, i );
-            if ( TrueMint1 & (1 << i) )
-                Kit_TruthCofactor1( pCo11, nVars, i );
-            else
-                Kit_TruthCofactor0( pCo11, nVars, i );
-        }
-
-    // derive the functions by composing them with the new variable (iVarReused)
-    Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
-    Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
-//Kit_DsdPrintFromTruth( pCo0, nVars );
-//Kit_DsdPrintFromTruth( pCo1, nVars );
-
-    // derive the composition function
-    Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
-
-    // process the decomposed function
-    pNtkDec = Kit_DsdDecompose( pDec, nVars );
-    pNtkComp = Kit_DsdDecompose( pCo, nVars );
-//Kit_DsdPrint( stdout, pNtkDec );
-//Kit_DsdPrint( stdout, pNtkComp );
-//printf( "cofactored variable %c\n", 'a' + iVar );
-//printf( "reused variable %c\n", 'a' + iVarReused );
-
-    ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
-    pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
-
-    Kit_DsdNtkFree( pNtkDec );
-    Kit_DsdNtkFree( pNtkComp );
-    return pObjNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
deleted file mode 100644
index 90e46863..00000000
--- a/src/opt/lpk/lpkSets.c
+++ /dev/null
@@ -1,440 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpkSets.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: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Lpk_Set_t_ Lpk_Set_t;
-struct Lpk_Set_t_
-{
-    char         iVar;        // the cofactoring variable
-    char         Over;        // the overlap in supports
-    char         SRed;        // the support reduction
-    char         Size;        // the size of the boundset
-    unsigned     uSubset0;    // the first subset (with removed)
-    unsigned     uSubset1;    // the second subset (with removed)
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes decomposable subsets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Lpk_ComputeSets_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_ComputeSets_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_ComputeSets_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     []
-
-***********************************************************************/
-unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
-{
-    unsigned uSupport, Entry;
-    int Number, i;
-    assert( p->nVars <= 16 );
-    Vec_IntClear( vSets );
-    Vec_IntPush( vSets, 0 );
-    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
-        return 0;
-    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
-    {
-        uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
-        Vec_IntPush( vSets, uSupport );
-        return uSupport;
-    }
-    uSupport = Lpk_ComputeSets_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 uSupport;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the sets of subsets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Lpk_PrintSetOne( int uSupport )
-{
-    unsigned k;
-    for ( k = 0; k < 16; k++ )
-        if ( uSupport & (1<<k) )
-            printf( "%c", 'a'+k );
-    printf( " " );
-}
-/**Function*************************************************************
-
-  Synopsis    [Prints the sets of subsets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Lpk_PrintSets( Vec_Int_t * vSets )
-{
-    unsigned uSupport;
-    int Number, i;
-    printf( "Subsets(%d): ", Vec_IntSize(vSets) );
-    Vec_IntForEachEntry( vSets, Number, i )
-    {
-        uSupport = Number;
-        Lpk_PrintSetOne( uSupport );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes maximal support reducing bound-sets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar,
-    Lpk_Set_t * pStore, int * pSize, int nSizeLimit )
-{
-    static int nTravId = 0;            // the number of the times this is visited
-    static int TravId[1<<16] = {0};    // last visited
-    static char SRed[1<<16];           // best support reduction
-    static char Over[1<<16];           // best overlaps
-    static unsigned Parents[1<<16];    // best set of parents
-    static unsigned short Used[1<<16]; // storage for used subsets
-    int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
-    unsigned Entry, Entry0, Entry1;
-    unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
-    Lpk_Set_t * pEntry;
-
-    if ( nTravId == (1 << 30) )
-        memset( TravId, 0, sizeof(int) * (1 << 16) );
-
-    // collect support reducing subsets
-    nUsed = 0;
-    nTravId++;
-    uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
-    Vec_IntForEachEntry( vSets0, Entry0, i )
-    Vec_IntForEachEntry( vSets1, Entry1, k )
-    {
-        uSupp0 = (Entry0 & 0xFFFF);
-        uSupp1 = (Entry1 & 0xFFFF);
-        // skip trivial
-        if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
-            continue;
-        if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
-            continue;
-        // get the entry
-        Entry = Entry0 | Entry1;
-        uSupp = Entry & 0xFFFF;
-        // set the bound set size
-        nSuppSize = Kit_WordCountOnes( uSupp );
-        // get the number of overlapping vars
-        nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
-        // get the support reduction
-        nSuppRed  = nSuppSize - 1 - nSuppOver;
-        // only consider support-reducing subsets
-        if ( nSuppRed <= 0 )
-            continue;
-        // check if this support is already used
-        if ( TravId[uSupp] < nTravId )
-        {
-            Used[nUsed++] = uSupp;
-
-            TravId[uSupp] = nTravId;
-            SRed[uSupp] = nSuppRed;
-            Over[uSupp] = nSuppOver;
-            Parents[uSupp] = (k << 16) | i;
-        }
-        else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
-        {
-            TravId[uSupp] = nTravId;
-            SRed[uSupp] = nSuppRed;
-            Over[uSupp] = nSuppOver;
-            Parents[uSupp] = (k << 16) | i;
-        }
-    }
-
-    // find the minimum overlap
-    nMinOver = 1000;
-    for ( s = 0; s < nUsed; s++ )
-        if ( nMinOver > Over[Used[s]] )
-            nMinOver = Over[Used[s]];
-
-
-    // collect the accumulated ones
-    for ( s = 0; s < nUsed; s++ )
-        if ( Over[Used[s]] == nMinOver )
-        {
-            // save the entry
-            if ( *pSize == nSizeLimit )
-                return;
-            pEntry = pStore + (*pSize)++;
-
-            i = Parents[Used[s]] & 0xFFFF;
-            k = Parents[Used[s]] >> 16;
-
-            pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
-            pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
-            Entry  = pEntry->uSubset0 | pEntry->uSubset1;
-
-            // record the cofactoring variable
-            pEntry->iVar = iCofVar;
-            // set the bound set size
-            pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
-            // get the number of overlapping vars
-            pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
-            // get the support reduction
-            pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
-            assert( pEntry->SRed > 0 );
-        }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints one set.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i )
-{
-    unsigned Entry;
-    Entry = pSet->uSubset0 | pSet->uSubset1;
-    printf( "%2d : ", i );
-    printf( "Var = %c  ",  'a' + pSet->iVar );
-    printf( "Size = %2d  ", pSet->Size );
-    printf( "Over = %2d  ", pSet->Over );
-    printf( "SRed = %2d  ", pSet->SRed );
-    Lpk_PrintSetOne( Entry );
-    printf( "              " );
-    Lpk_PrintSetOne( Entry >> 16 );
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Evaluates the cofactors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused )
-{
-    static int nStoreSize = 256;
-    static Lpk_Set_t pStore[256], * pSet, * pSetBest;
-    Kit_DsdNtk_t * ppNtks[2], * pTemp;
-    Vec_Int_t * vSets0 = p->vSets[0];
-    Vec_Int_t * vSets1 = p->vSets[1];
-    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
-    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
-    int nSets, i, SizeMax;//, SRedMax;
-    unsigned Entry;
-    int fVerbose = p->pPars->fVeryVerbose;
-//    int fVerbose = 0;
-
-    // collect decomposable subsets for each pair of cofactors
-    if ( fVerbose )
-    {
-        printf( "\nExploring support-reducing bound-sets of function:\n" );
-        Kit_DsdPrintFromTruth( pTruth, nVars );
-    }
-    nSets = 0;
-    for ( i = 0; i < nVars; i++ )
-    {
-        if ( fVerbose )
-        printf( "Evaluating variable %c:\n", 'a'+i );
-        // evaluate the cofactor pair
-        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
-        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
-        // decompose and expand
-        ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
-        ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
-        ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
-        ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
-        if ( fVerbose )
-        Kit_DsdPrint( stdout, ppNtks[0] );
-        if ( fVerbose )
-        Kit_DsdPrint( stdout, ppNtks[1] );
-        // compute subsets
-        Lpk_ComputeSets( ppNtks[0], vSets0 );
-        Lpk_ComputeSets( ppNtks[1], vSets1 );
-        // print subsets
-        if ( fVerbose )
-        Lpk_PrintSets( vSets0 );
-        if ( fVerbose )
-        Lpk_PrintSets( vSets1 );
-        // free the networks
-        Kit_DsdNtkFree( ppNtks[0] );
-        Kit_DsdNtkFree( ppNtks[1] );
-        // evaluate the pair
-        Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
-    }
-
-    // print the results
-    if ( fVerbose )
-    printf( "\n" );
-    if ( fVerbose )
-    for ( i = 0; i < nSets; i++ )
-        Lpk_MapSuppPrintSet( pStore + i, i );
-
-    // choose the best subset
-    SizeMax = 0;
-    pSetBest = NULL;
-    for ( i = 0; i < nSets; i++ )
-    {
-        pSet = pStore + i;
-        if ( pSet->Size > p->pPars->nLutSize - 1 )
-            continue;
-        if ( SizeMax < pSet->Size )
-        {
-            pSetBest = pSet;
-            SizeMax = pSet->Size;
-        }
-    }
-/*
-    // if the best is not choosen, select the one with largest reduction
-    SRedMax = 0;
-    if ( pSetBest == NULL )
-    {
-        for ( i = 0; i < nSets; i++ )
-        {
-            pSet = pStore + i;
-            if ( SRedMax < pSet->SRed )
-            {
-                pSetBest = pSet;
-                SRedMax = pSet->SRed;
-            }
-        }
-    }
-*/
-    if ( pSetBest == NULL )
-    {
-        if ( fVerbose )
-        printf( "Could not select a subset.\n" );
-        return 0;
-    }
-    else
-    {
-        if ( fVerbose )
-        printf( "Selected the following subset:\n" );
-        if ( fVerbose )
-        Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
-    }
-
-    // prepare the return result
-    // get the remaining variables
-    Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
-    // get the variables to be removed
-    Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
-    // make sure there are some - otherwise it is not supp-red
-    assert( Entry );
-    // remember the first such variable
-    *piVarReused = Kit_WordFindFirstBit( Entry );
-    *piVar = pSetBest->iVar;
-    return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/lpk_.c b/src/opt/lpk/lpk_.c
deleted file mode 100644
index d8555e08..00000000
--- a/src/opt/lpk/lpk_.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [lpk_.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: lpk_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "lpkInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make
deleted file mode 100644
index 26a54894..00000000
--- a/src/opt/lpk/module.make
+++ /dev/null
@@ -1,11 +0,0 @@
-SRC +=    src/opt/lpk/lpkCore.c \
-    src/opt/lpk/lpkAbcDec.c \
-    src/opt/lpk/lpkAbcMux.c \
-    src/opt/lpk/lpkAbcDsd.c \
-    src/opt/lpk/lpkAbcUtil.c \
-    src/opt/lpk/lpkCut.c \
-    src/opt/lpk/lpkMan.c \
-    src/opt/lpk/lpkMap.c \
-    src/opt/lpk/lpkMulti.c \
-    src/opt/lpk/lpkMux.c \
-    src/opt/lpk/lpkSets.c