diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c
deleted file mode 100644
index 38e407bc38..0000000000
--- a/src/opt/mfs/mfsCore_.c
+++ /dev/null
@@ -1,394 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [mfsCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [The good old minimization with complete don't-cares.]
-
-  Synopsis    [Core procedures of this package.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: mfsCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "mfsInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
-{
-    memset( pPars, 0, sizeof(Mfs_Par_t) );
-    pPars->nWinTfoLevs  =    2;
-    pPars->nFanoutsMax  =   10;
-    pPars->nDepthMax    =   20;
-    pPars->nWinSizeMax  =  300;
-    pPars->nGrowthLevel =    0;
-    pPars->nBTLimit     = 5000;
-    pPars->fResub       =    1;
-    pPars->fArea        =    0;
-    pPars->fMoreEffort  =    0;
-    pPars->fSwapEdge    =    0;
-    pPars->fOneHotness  =    0;
-    pPars->fVerbose     =    0;
-    pPars->fVeryVerbose =    0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
-{
-    clock_t clk;
-    p->nNodesTried++;
-    // prepare data structure for this node
-    Mfs_ManClean( p ); 
-    // compute window roots, window support, and window nodes
-clk = clock();
-    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
-    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-p->timeWin += clock() - clk;
-    if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
-        return 1;
-    // compute the divisors of the window
-clk = clock();
-    p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
-    p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
-p->timeDiv += clock() - clk;
-    // construct AIG for the window
-clk = clock();
-    p->pAigWin = Abc_NtkConstructAig( p, pNode );
-p->timeAig += clock() - clk;
-    // translate it into CNF
-clk = clock();
-    p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
-p->timeCnf += clock() - clk;
-    // create the SAT problem
-clk = clock();
-    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
-    if ( p->pSat == NULL )
-    {
-        p->nNodesBad++;
-        return 1;
-    }
-    // solve the SAT problem
-    if ( p->pPars->fPower )
-        Abc_NtkMfsEdgePower( p, pNode );
-    else if ( p->pPars->fSwapEdge )
-        Abc_NtkMfsEdgeSwapEval( p, pNode );
-    else
-    {
-        Abc_NtkMfsResubNode( p, pNode );
-        if ( p->pPars->fMoreEffort )
-            Abc_NtkMfsResubNode2( p, pNode );
-    }
-p->timeSat += clock() - clk;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
-{
-    Hop_Obj_t * pObj;
-    int RetValue;
-    float dProb;
-    extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb );
-
-    int nGain;
-    clock_t clk;
-    p->nNodesTried++;
-    // prepare data structure for this node
-    Mfs_ManClean( p );
-    // compute window roots, window support, and window nodes
-clk = clock();
-    p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
-    p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-    p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-p->timeWin += clock() - clk;
-    // count the number of patterns
-//    p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode );
-    // construct AIG for the window
-clk = clock();
-    p->pAigWin = Abc_NtkConstructAig( p, pNode );
-p->timeAig += clock() - clk;
-    // translate it into CNF
-clk = clock();
-    p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) );
-p->timeCnf += clock() - clk;
-    // create the SAT problem
-clk = clock();
-    p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
-    if ( p->pSat && p->pPars->fOneHotness )
-        Abc_NtkAddOneHotness( p );
-    if ( p->pSat == NULL )
-        return 0;
-    // solve the SAT problem
-    RetValue = Abc_NtkMfsSolveSat( p, pNode );
-    p->nTotConfLevel += p->pSat->stats.conflicts;
-p->timeSat += clock() - clk;
-    if ( RetValue == 0 )
-    {
-        p->nTimeOutsLevel++;
-        p->nTimeOuts++;
-        return 0;
-    }
-    // minimize the local function of the node using bi-decomposition
-    assert( p->nFanins == Abc_ObjFaninNum(pNode) );
-    dProb = p->pPars->fPower? ((float *)p->vProbs->pArray)[pNode->Id] : -1.0;
-    pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare, dProb );
-    nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj);
-    if ( nGain >= 0 )
-    {
-        p->nNodesDec++;
-        p->nNodesGained += nGain;
-        p->nNodesGainedLevel += nGain;
-        pNode->pData = pObj;    
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
-{
-    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-
-    Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
-    ProgressBar * pProgress;
-    Mfs_Man_t * p;
-    Abc_Obj_t * pObj;
-    Vec_Vec_t * vLevels;
-    Vec_Ptr_t * vNodes;
-    int i, k, nNodes, nFaninMax;
-    clock_t clk = clock(), clk2;
-    int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
-    int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
-
-    assert( Abc_NtkIsLogic(pNtk) );
-    nFaninMax = Abc_NtkGetFaninMax(pNtk);
-    if ( pPars->fResub )
-    {
-        if ( nFaninMax > 8 )
-        {
-            printf( "Nodes with more than %d fanins will not be processed.\n", 8 );
-            nFaninMax = 8;
-        }
-    }
-    else
-    {
-        if ( nFaninMax > MFS_FANIN_MAX )
-        {
-            printf( "Nodes with more than %d fanins will not be processed.\n", MFS_FANIN_MAX );
-            nFaninMax = MFS_FANIN_MAX;
-        }
-    }
-    // perform the network sweep
-    Abc_NtkSweep( pNtk, 0 );
-    // convert into the AIG
-    if ( !Abc_NtkToAig(pNtk) )
-    {
-        fprintf( stdout, "Converting to AIGs has failed.\n" );
-        return 0;
-    }
-    assert( Abc_NtkHasAig(pNtk) );
-
-    // start the manager
-    p = Mfs_ManAlloc( pPars );
-    p->pNtk = pNtk;
-    p->nFaninMax = nFaninMax;
-
-    // precomputer power-aware metrics
-    if ( pPars->fPower )
-    {
-        extern Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne );
-        if ( pPars->fResub )
-            p->vProbs = Abc_NtkPowerEstimate( pNtk, 0 );
-        else
-            p->vProbs = Abc_NtkPowerEstimate( pNtk, 1 );
-        printf( "Total switching before = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
-    }
-
-    if ( pNtk->pExcare )
-    {
-        Abc_Ntk_t * pTemp;
-        if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
-            printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n", 
-                Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) );
-        else
-        {
-            pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
-            p->pCare = Abc_NtkToDar( pTemp, 0, 0 );
-            Abc_NtkDelete( pTemp );
-            p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
-        }
-    }
-    if ( p->pCare != NULL )
-        printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
-    // prepare the BDC manager
-    if ( !pPars->fResub )
-    {
-        pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
-        pDecPars->fVerbose = pPars->fVerbose;
-        p->vTruth = Vec_IntAlloc( 0 );
-        p->pManDec = Bdc_ManAlloc( pDecPars );
-    }
-
-    // label the register outputs
-    if ( p->pCare )
-    {
-        Abc_NtkForEachCi( pNtk, pObj, i )
-            pObj->pData = (void *)(PORT_PTRUINT_T)i;
-    }
- 
-    // compute levels
-    Abc_NtkLevel( pNtk );
-    Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
-
-    // compute don't-cares for each node
-    nNodes = 0;
-    p->nTotalNodesBeg = nTotalNodesBeg;
-    p->nTotalEdgesBeg = nTotalEdgesBeg;
-    if ( pPars->fResub )
-    {
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
-        Abc_NtkForEachNode( pNtk, pObj, i )
-        {
-            if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
-                continue;
-            if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
-                continue;
-            if ( !p->pPars->fVeryVerbose )
-                Extra_ProgressBarUpdate( pProgress, i, NULL );
-            if ( pPars->fResub )
-                Abc_NtkMfsResub( p, pObj );
-            else
-                Abc_NtkMfsNode( p, pObj );
-        }
-        Extra_ProgressBarStop( pProgress );
-    }
-    else
-    {
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
-        vLevels = Abc_NtkLevelize( pNtk );
-        Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
-        {
-            if ( !p->pPars->fVeryVerbose )
-                Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
-            p->nNodesGainedLevel = 0;
-            p->nTotConfLevel = 0;
-            p->nTimeOutsLevel = 0;
-            clk2 = clock();
-            Vec_PtrForEachEntry( vNodes, pObj, i )
-            {
-                if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
-                    break;
-                if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
-                    continue;
-                if ( pPars->fResub )
-                    Abc_NtkMfsResub( p, pObj );
-                else 
-                    Abc_NtkMfsNode( p, pObj );
-            }
-            nNodes += Vec_PtrSize(vNodes);
-            if ( pPars->fVerbose )
-            {
-            printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %%  ", 
-                k, Vec_PtrSize(vNodes),
-                1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
-                1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
-                100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
-            PRT( "Time", clock() - clk2 );
-            }
-        }
-        Extra_ProgressBarStop( pProgress );
-        Vec_VecFree( vLevels );
-    }
-    Abc_NtkStopReverseLevels( pNtk );
-
-    // perform the sweeping
-    if ( !pPars->fResub )
-    {
-        extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
-//        Abc_NtkSweep( pNtk, 0 );
-//        Abc_NtkBidecResyn( pNtk, 0 );
-    }
-
-    p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
-    p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
-
-    // undo labesl
-    if ( p->pCare )
-    {
-        Abc_NtkForEachCi( pNtk, pObj, i )
-            pObj->pData = NULL;
-    }
-    if ( pPars->fPower )
-        printf( "Total switching after  = %7.2f.\n", Abc_NtkMfsTotalSwitching(pNtk) );
-
-    // free the manager
-    p->timeTotal = clock() - clk;
-    Mfs_ManStop( p );
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/opt/mfs/mfsResub_.c b/src/opt/mfs/mfsResub_.c
deleted file mode 100644
index b79ccd9e5b..0000000000
--- a/src/opt/mfs/mfsResub_.c
+++ /dev/null
@@ -1,567 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [mfsResub.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [The good old minimization with complete don't-cares.]
-
-  Synopsis    [Procedures to perform resubstitution.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "mfsInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the network after resubstitution.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
-{
-    Abc_Obj_t * pObjNew, * pFanin;
-    int k;
-    // create the new node
-    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
-    pObjNew->pData = pFunc;
-    Vec_PtrForEachEntry( vFanins, pFanin, k )
-        Abc_ObjAddFanin( pObjNew, pFanin );
-    // replace the old node by the new node
-//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
-//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
-    // update the level of the node
-    Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints resub candidate stats.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p )
-{
-    Abc_Obj_t * pFanin, * pNode;
-    int i, k, nAreaCrits = 0, nAreaExpanse = 0;
-    int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
-    Abc_NtkForEachNode( p->pNtk, pNode, i )
-        Abc_ObjForEachFanin( pNode, pFanin, k )
-        {
-            if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
-            {
-                nAreaCrits++;
-                nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
-            }
-        }
-    printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n", 
-        nAreaCrits, nAreaExpanse );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Tries resubstitution.]
-
-  Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
-{
-    unsigned * pData;
-    int RetValue, iVar, i;
-    p->nSatCalls++;
-    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-//    assert( RetValue == l_False || RetValue == l_True );
-    if ( RetValue == l_False )
-        return 1;
-    if ( RetValue != l_True )
-    {
-        p->nTimeOuts++;
-        return -1;
-    }
-    p->nSatCexes++;
-    // store the counter-example
-    Vec_IntForEachEntry( p->vProjVars, iVar, i )
-    {
-        pData = Vec_PtrEntry( p->vDivCexes, i );
-        if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
-        {
-            assert( Aig_InfoHasBit(pData, p->nCexes) );
-            Aig_InfoXorBit( pData, p->nCexes );
-        }
-    }
-    p->nCexes++;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resubstitution for the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
-{
-    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
-    unsigned * pData;
-    int pCands[MFS_FANIN_MAX];
-    int RetValue, iVar, i, nCands, nWords, w;
-    clock_t clk;
-    Abc_Obj_t * pFanin;
-    Hop_Obj_t * pFunc;
-    assert( iFanin >= 0 );
-
-    // clean simulation info
-    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
-    p->nCexes = 0;
-    if ( fVeryVerbose )
-    {
-        printf( "\n" );
-        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanin = %d (out of %d). MFFC = %d\n", 
-            pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
-            iFanin, Abc_ObjFaninNum(pNode), 
-            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
-    }
-
-    // try fanins without the critical fanin
-    nCands = 0;
-    Vec_PtrClear( p->vFanins );
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-    {
-        if ( i == iFanin )
-            continue;
-        Vec_PtrPush( p->vFanins, pFanin );
-        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
-        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
-    }
-    RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
-    if ( RetValue == -1 )
-        return 0;
-    if ( RetValue == 1 )
-    {
-        if ( fVeryVerbose )
-        printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
-        p->nNodesResub++;
-        p->nNodesGainedLevel++;
-        if ( fSkipUpdate )
-            return 1;
-clk = clock();
-        // derive the function
-        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
-        if ( pFunc == NULL )
-            return 0;
-        // update the network
-        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
-p->timeInt += clock() - clk;
-        return 1;
-    }
-
-    if ( fOnlyRemove )
-        return 0;
-
-    if ( fVeryVerbose )
-    {
-        for ( i = 0; i < 8; i++ )
-            printf( " " );
-        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
-            printf( "%d", i % 10 );
-        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
-            if ( i == iFanin )
-                printf( "*" );
-            else
-                printf( "%c", 'a' + i );
-        printf( "\n" );
-    }
-    iVar = -1;
-    while ( 1 )
-    {
-        float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL);
-        assert( (pProbab != NULL) == p->pPars->fPower );
-        if ( fVeryVerbose )
-        {
-            printf( "%3d: %2d ", p->nCexes, iVar );
-            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
-            {
-                pData = Vec_PtrEntry( p->vDivCexes, i );
-                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
-            }
-            printf( "\n" );
-        }
-
-        // find the next divisor to try
-        nWords = Aig_BitWordNum(p->nCexes);
-        assert( nWords <= p->nDivWords );
-        for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
-        {
-            if ( p->pPars->fPower )
-            {
-                Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar);
-                // only accept the divisor if it is "cool"
-                if ( pProbab[Abc_ObjId(pDiv)] >= 0.2 )
-                    continue;
-            }
-            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
-            for ( w = 0; w < nWords; w++ )
-                if ( pData[w] != ~0 )
-                    break;
-            if ( w == nWords )
-                break;
-        }
-        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
-            return 0;
-
-        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
-        RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
-        if ( RetValue == -1 )
-            return 0;
-        if ( RetValue == 1 )
-        {
-            if ( fVeryVerbose )
-            printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
-            p->nNodesResub++;
-            p->nNodesGainedLevel++;
-            if ( fSkipUpdate )
-                return 1;
-clk = clock();
-            // derive the function
-            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
-            if ( pFunc == NULL )
-                return 0;
-            // update the network
-            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
-            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
-p->timeInt += clock() - clk;
-            return 1;
-        }
-        if ( p->nCexes >= p->pPars->nDivMax )
-            break;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resubstitution for the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iFanin2 )
-{
-    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
-    unsigned * pData, * pData2;
-    int pCands[MFS_FANIN_MAX];
-    int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
-    clock_t clk;
-    Abc_Obj_t * pFanin;
-    Hop_Obj_t * pFunc;
-    assert( iFanin >= 0 );
-    assert( iFanin2 >= 0 || iFanin2 == -1 );
-
-    // clean simulation info
-    Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords ); 
-    p->nCexes = 0;
-    if ( fVeryVerbose )
-    {
-        printf( "\n" );
-        printf( "Node %5d : Level = %2d. Divs = %3d.  Fanins = %d/%d (out of %d). MFFC = %d\n", 
-            pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode), 
-            iFanin, iFanin2, Abc_ObjFaninNum(pNode), 
-            Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
-    }
-
-    // try fanins without the critical fanin
-    nCands = 0;
-    Vec_PtrClear( p->vFanins );
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-    {
-        if ( i == iFanin || i == iFanin2 )
-            continue;
-        Vec_PtrPush( p->vFanins, pFanin );
-        iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
-        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
-    }
-    RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
-    if ( RetValue == -1 )
-        return 0;
-    if ( RetValue == 1 )
-    {
-        if ( fVeryVerbose )
-        printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
-        p->nNodesResub++;
-        p->nNodesGainedLevel++;
-clk = clock();
-        // derive the function
-        pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
-        if ( pFunc == NULL )
-            return 0;
-        // update the network
-        Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
-p->timeInt += clock() - clk;
-        return 1;
-    }
-
-    if ( fVeryVerbose )
-    {
-        for ( i = 0; i < 11; i++ )
-            printf( " " );
-        for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
-            printf( "%d", i % 10 );
-        for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
-            if ( i == iFanin || i == iFanin2 )
-                printf( "*" );
-            else
-                printf( "%c", 'a' + i );
-        printf( "\n" );
-    }
-    iVar = iVar2 = -1;
-    while ( 1 )
-    {
-        if ( fVeryVerbose )
-        {
-            printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
-            for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
-            {
-                pData = Vec_PtrEntry( p->vDivCexes, i );
-                printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
-            }
-            printf( "\n" );
-        }
-
-        // find the next divisor to try
-        nWords = Aig_BitWordNum(p->nCexes);
-        assert( nWords <= p->nDivWords );
-        fBreak = 0;
-        for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
-        {
-            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
-            for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
-            {
-                pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 );
-                for ( w = 0; w < nWords; w++ )
-                    if ( (pData[w] | pData2[w]) != ~0 )
-                        break;
-                if ( w == nWords )
-                {
-                    fBreak = 1;
-                    break;
-                }
-            }
-            if ( fBreak )
-                break;
-        }
-        if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
-            return 0;
-
-        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
-        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
-        RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
-        if ( RetValue == -1 )
-            return 0;
-        if ( RetValue == 1 )
-        {
-            if ( fVeryVerbose )
-            printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
-            p->nNodesResub++;
-            p->nNodesGainedLevel++;
-clk = clock();
-            // derive the function
-            pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
-            if ( pFunc == NULL )
-                return 0;
-            // update the network
-            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) );
-            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
-            assert( Vec_PtrSize(p->vFanins) == nCands + 2 );
-            Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
-p->timeInt += clock() - clk;
-            return 1;
-        }
-        if ( p->nCexes >= p->pPars->nDivMax )
-            break;
-    }
-    return 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Evaluates the possibility of replacing given edge by another edge.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanin;
-    int i;
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Evaluates the possibility of replacing given edge by another edge.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanin;
-    float * pProbab = (float *)p->vProbs->pArray;
-    int i;
-    // try replacing area critical fanins
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( pProbab[pFanin->Id] >= 0.4 )
-        {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
-                return 1;
-        }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resubstitution for the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanin;
-    int i;
-    // try replacing area critical fanins
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
-        {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
-                return 1;
-        }
-    // try removing redundant edges
-    if ( !p->pPars->fArea )
-    {
-        Abc_ObjForEachFanin( pNode, pFanin, i )
-            if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
-            {
-                if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
-                    return 1;
-            }
-    }
-    if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
-        return 0;
-    // try replacing area critical fanins while adding two new fanins
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
-        {
-            if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
-                return 1;
-        }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resubstitution for the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanin, * pFanin2;
-    int i, k;
-/*
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
-        {
-            if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
-                return 1;
-        }
-*/
-    if ( Abc_ObjFaninNum(pNode) < 2 )
-        return 0;
-    // try replacing one area critical fanin and one other fanin while adding two new fanins
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-    {
-        if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
-        {
-            // consider second fanin to remove at the same time
-            Abc_ObjForEachFanin( pNode, pFanin2, k )
-            {
-                if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
-                    return 1;
-            }
-        }
-    }
-    return 0;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-