Version abc80330

12 files changed, 2595 insertions, 0 deletions

diff --git a/src/aig/mfx/mfx.h b/src/aig/mfx/mfx.h
new file mode 100644
index 00000000..783de56c
--- /dev/null
+++ b/src/aig/mfx/mfx.h
@@ -0,0 +1,80 @@
+/**CFile****************************************************************
+
+  FileName    [mfx.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfx.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __MFX_H__
+#define __MFX_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Mfx_Par_t_ Mfx_Par_t;
+struct Mfx_Par_t_
+{
+    // general parameters
+    int           nWinTfoLevs;   // the maximum fanout levels
+    int           nFanoutsMax;   // the maximum number of fanouts
+    int           nDepthMax;     // the maximum number of logic levels
+    int           nDivMax;       // the maximum number of divisors
+    int           nWinSizeMax;   // the maximum size of the window
+    int           nGrowthLevel;  // the maximum allowed growth in level
+    int           nBTLimit;      // the maximum number of conflicts in one SAT run
+    int           fResub;        // performs resubstitution
+    int           fArea;         // performs optimization for area
+    int           fMoreEffort;   // performs high-affort minimization
+    int           fSwapEdge;     // performs edge swapping
+    int           fDelay;        // performs optimization for delay
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== mfxCore.c ==========================================================*/
+extern void        Mfx_ParsDefault( Mfx_Par_t * pPars );
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
new file mode 100644
index 00000000..4c8988cc
--- /dev/null
+++ b/src/aig/mfx/mfxCore.c
@@ -0,0 +1,330 @@
+/**CFile****************************************************************
+
+  FileName    [mfxCore.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: mfxCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Mfx_ParsDefault( Mfx_Par_t * pPars )
+{
+    pPars->nWinTfoLevs  =    2;
+    pPars->nFanoutsMax  =   10;
+    pPars->nDepthMax    =   20;
+    pPars->nDivMax      =  250;
+    pPars->nWinSizeMax  =  300;
+    pPars->nGrowthLevel =    0;
+    pPars->nBTLimit     = 5000;
+    pPars->fResub       =    1;
+    pPars->fArea        =    0;
+    pPars->fMoreEffort  =    0;
+    pPars->fSwapEdge    =    0;
+    pPars->fVerbose     =    0;
+    pPars->fVeryVerbose =    0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_Resub( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    int clk;
+    p->nNodesTried++;
+    // prepare data structure for this node
+    Mfx_ManClean( p ); 
+    // compute window roots, window support, and window nodes
+clk = clock();
+    p->vRoots = Mfx_ComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
+    p->vSupp  = Nwk_ManSupportNodes( p->pNtk, (Nwk_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+    p->vNodes = Nwk_ManDfsNodes( p->pNtk, (Nwk_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  = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
+    p->vDivs  = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
+    p->nTotalDivs += Vec_PtrSize(p->vDivs);
+p->timeDiv += clock() - clk;
+    // construct AIG for the window
+clk = clock();
+    p->pAigWin = Mfx_ConstructAig( 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 = Mfx_CreateSolverResub( p, NULL, 0, 0 );
+    if ( p->pSat == NULL )
+    {
+        p->nNodesBad++;
+        return 1;
+    }
+    // solve the SAT problem
+    if ( p->pPars->fSwapEdge )
+        Mfx_EdgeSwapEval( p, pNode );
+    else
+    {
+        Mfx_ResubNode( p, pNode );
+        if ( p->pPars->fMoreEffort )
+            Mfx_ResubNode2( p, pNode );
+    }
+p->timeSat += clock() - clk;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_Node( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Hop_Obj_t * pObj;
+    int RetValue;
+
+    int nGain, clk;
+    p->nNodesTried++;
+    // prepare data structure for this node
+    Mfx_ManClean( p );
+    // compute window roots, window support, and window nodes
+clk = clock();
+    p->vRoots = Mfx_ComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
+    p->vSupp  = Nwk_ManSupportNodes( p->pNtk, (Nwk_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+    p->vNodes = Nwk_ManDfsNodes( p->pNtk, (Nwk_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+p->timeWin += clock() - clk;
+    // count the number of patterns
+//    p->dTotalRatios += Mfx_ConstraintRatio( p, pNode );
+    // construct AIG for the window
+clk = clock();
+    p->pAigWin = Mfx_ConstructAig( p, pNode );
+p->timeAig += clock() - clk;
+    // translate it into CNF
+clk = clock();
+    p->pCnf = Cnf_DeriveSimple( p->pAigWin, Nwk_ObjFaninNum(pNode) );
+p->timeCnf += clock() - clk;
+    // create the SAT problem
+clk = clock();
+    p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+    if ( p->pSat == NULL )
+        return 0;
+    // solve the SAT problem
+    RetValue = Mfx_SolveSat( 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 == Nwk_ObjFaninNum(pNode) );
+    pObj = Nwk_NodeIfNodeResyn( p->pManDec, pNode->pMan->pManHop, pNode->pFunc, p->nFanins, p->vTruth, p->uCare );
+    nGain = Hop_DagSize(pNode->pFunc) - Hop_DagSize(pObj);
+    if ( nGain >= 0 )
+    {
+        p->nNodesDec++;
+        p->nNodesGained += nGain;
+        p->nNodesGainedLevel += nGain;
+        pNode->pFunc = pObj;    
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
+{
+    Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
+//    ProgressBar * pProgress;
+    Mfx_Man_t * p;
+    Tim_Man_t * pManTimeOld = NULL;
+    Nwk_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    Vec_Ptr_t * vNodes;
+    int i, k, nNodes, nFaninMax, clk = clock(), clk2;
+    int nTotalNodesBeg = Nwk_ManNodeNum(pNtk);
+    int nTotalEdgesBeg = Nwk_ManGetTotalFanins(pNtk);
+
+    // check limits on the number of fanins
+    nFaninMax = Nwk_ManGetFaninMax(pNtk);
+    if ( pPars->fResub )
+    {
+        if ( nFaninMax > 8 )
+        {
+            printf( "Nodes with more than %d fanins will node be processed.\n", 8 );
+            nFaninMax = 8;
+        }
+    }
+    else
+    {
+        if ( nFaninMax > MFX_FANIN_MAX )
+        {
+            printf( "Nodes with more than %d fanins will node be processed.\n", MFX_FANIN_MAX );
+            nFaninMax = MFX_FANIN_MAX;
+        }
+    }
+
+/*
+    // prepare timing information
+    if ( pNtk->pManTime )
+    {
+        // compute levels
+        Nwk_ManLevel( pNtk );
+        // compute delay trace with white-boxes
+        Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
+        // save the general timing manager
+        pManTimeOld = pNtk->pManTime;
+        // derive an approximate timing manager without white-boxes
+        pNtk->pManTime = Tim_ManDupApprox( pNtk->pManTime );
+    }
+    // compute delay trace with the given timing manager
+    Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
+*/
+
+    // start the manager
+    p = Mfx_ManAlloc( pPars );
+    p->pNtk = pNtk;
+    p->nFaninMax = nFaninMax;
+    if ( !pPars->fResub )
+    {
+        pDecPars->nVarsMax = nFaninMax;
+        pDecPars->fVerbose = pPars->fVerbose;
+        p->vTruth = Vec_IntAlloc( 0 );
+        p->pManDec = Bdc_ManAlloc( pDecPars );
+    }
+
+    // compute don't-cares for each node
+    nNodes = 0;
+    p->nTotalNodesBeg = nTotalNodesBeg;
+    p->nTotalEdgesBeg = nTotalEdgesBeg;
+    if ( pPars->fResub )
+    {
+//        pProgress = Extra_ProgressBarStart( stdout, Nwk_ObjNumMax(pNtk) );
+        Nwk_ManForEachNode( pNtk, pObj, i )
+        {
+            if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax )
+                continue;
+            if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax )
+                continue;
+//            if ( !p->pPars->fVeryVerbose )
+//                Extra_ProgressBarUpdate( pProgress, i, NULL );
+            Mfx_Resub( p, pObj );
+        }
+//        Extra_ProgressBarStop( pProgress );
+    }
+    else
+    {
+//        pProgress = Extra_ProgressBarStart( stdout, Nwk_NodeNum(pNtk) );
+        vLevels = Nwk_ManLevelize( 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 && pObj->Level > p->pPars->nDepthMax )
+                    break;
+                if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax )
+                    continue;
+                Mfx_Node( 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 );
+    }
+    p->nTotalNodesEnd = Nwk_ManNodeNum(pNtk);
+    p->nTotalEdgesEnd = Nwk_ManGetTotalFanins(pNtk);
+/*
+    // reset the timing manager
+    if ( pNtk->pManTime )
+    {
+        Tim_ManStop( pNtk->pManTime );
+        pNtk->pManTime = pManTimeOld;
+    }
+    Nwk_ManVerifyLevel( pNtk );
+*/
+    // free the manager
+    p->timeTotal = clock() - clk;
+    Mfx_ManStop( p );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxDiv.c b/src/aig/mfx/mfxDiv.c
new file mode 100644
index 00000000..b7b76031
--- /dev/null
+++ b/src/aig/mfx/mfxDiv.c
@@ -0,0 +1,303 @@
+/**CFile****************************************************************
+
+  FileName    [mfxDiv.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to compute candidate divisors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks and collects the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfxWinMarkTfi_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vCone )
+{
+    Nwk_Obj_t * pFanin;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent(pObj) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjIsCi(pObj) )
+    {
+        Vec_PtrPush( vCone, pObj );
+        return;
+    }
+    assert( Nwk_ObjIsNode(pObj) );
+    // visit the fanins of the node
+    Nwk_ObjForEachFanin( pObj, pFanin, i )
+        Abc_MfxWinMarkTfi_rec( pFanin, vCone );
+    Vec_PtrPush( vCone, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks and collects the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfxWinMarkTfi( Nwk_Obj_t * pNode )
+{
+    Vec_Ptr_t * vCone;
+    vCone = Vec_PtrAlloc( 100 );
+    Abc_MfxWinMarkTfi_rec( pNode, vCone );
+    return vCone;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, int nLevelLimit )
+{
+    Nwk_Obj_t * pFanout;
+    int i;
+    if ( Nwk_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+        return;
+    if ( Nwk_ObjIsTravIdCurrent(pObj) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    Nwk_ObjForEachFanout( pObj, pFanout, i )
+        Abc_MfxWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfxNodeDeref_rec( Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Nwk_ObjIsCi(pNode) )
+        return 0;
+    Nwk_ObjSetTravIdCurrent( pNode );
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        assert( pFanin->nFanouts > 0 );
+        if ( --pFanin->nFanouts == 0 )
+            Counter += Abc_MfxNodeDeref_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfxNodeRef_rec( Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Nwk_ObjIsCi(pNode) )
+        return 0;
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( pFanin->nFanouts++ == 0 )
+            Counter += Abc_MfxNodeRef_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels MFFC of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_MfxWinVisitMffc( Nwk_Obj_t * pNode )
+{
+    int Count1, Count2;
+    assert( Nwk_ObjIsNode(pNode) );
+    // dereference the node (mark with the current trav ID)
+    Count1 = Abc_MfxNodeDeref_rec( pNode );
+    // reference it back
+    Count2 = Abc_MfxNodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes divisors and add them to nodes in the window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax )
+{
+    Vec_Ptr_t * vCone, * vDivs;
+    Nwk_Obj_t * pObj, * pFanout, * pFanin;
+    int k, f, m;
+    int nDivsPlus = 0, nTrueSupp;
+    assert( p->vDivs == NULL );
+
+    // mark the TFI with the current trav ID
+    Nwk_ManIncrementTravId( pNode->pMan );
+    vCone = Abc_MfxWinMarkTfi( pNode );
+
+    // count the number of PIs
+    nTrueSupp = 0;
+    Vec_PtrForEachEntry( vCone, pObj, k )
+        nTrueSupp += Nwk_ObjIsCi(pObj);
+//    printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );
+
+    // mark with the current trav ID those nodes that should not be divisors:
+    // (1) the node and its TFO
+    // (2) the MFFC of the node
+    // (3) the node's fanins (these are treated as a special case)
+    Nwk_ManIncrementTravId( pNode->pMan );
+    Abc_MfxWinSweepLeafTfo_rec( pNode, nLevDivMax );
+    Abc_MfxWinVisitMffc( pNode );
+    Nwk_ObjForEachFanin( pNode, pObj, k )
+        Nwk_ObjSetTravIdCurrent( pObj );
+
+    // at this point the nodes are marked with two trav IDs:
+    // nodes to be collected as divisors are marked with previous trav ID
+    // nodes to be avoided as divisors are marked with current trav ID
+
+    // start collecting the divisors
+    vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
+    Vec_PtrForEachEntry( vCone, pObj, k )
+    {
+        if ( !Nwk_ObjIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > nLevDivMax )
+            continue;
+        Vec_PtrPush( vDivs, pObj );
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            break;
+    }
+    Vec_PtrFree( vCone );
+
+    // explore the fanouts of already collected divisors
+    if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
+    Vec_PtrForEachEntry( vDivs, pObj, k )
+    {
+        // consider fanouts of this node
+        Nwk_ObjForEachFanout( pObj, pFanout, f )
+        {
+            // stop if there are too many fanouts
+            if ( f > 20 )
+                break;
+            // skip nodes that are already added
+            if ( Nwk_ObjIsTravIdPrevious(pFanout) )
+                continue;
+            // skip nodes in the TFO or in the MFFC of node
+            if ( Nwk_ObjIsTravIdCurrent(pFanout) )
+                continue;
+            // skip COs
+            if ( !Nwk_ObjIsNode(pFanout) ) 
+                continue;
+            // skip nodes with large level
+            if ( (int)pFanout->Level > nLevDivMax )
+                continue;
+            // skip nodes whose fanins are not divisors
+            Nwk_ObjForEachFanin( pFanout, pFanin, m )
+                if ( !Nwk_ObjIsTravIdPrevious(pFanin) )
+                    break;
+            if ( m < Nwk_ObjFaninNum(pFanout) )
+                continue;
+            // make sure this divisor in not among the nodes
+//            Vec_PtrForEachEntry( p->vNodes, pFanin, m )
+//                assert( pFanout != pFanin );
+            // add the node to the divisors
+            Vec_PtrPush( vDivs, pFanout );
+//            Vec_PtrPush( p->vNodes, pFanout );
+            Vec_PtrPushUnique( p->vNodes, pFanout );
+            Nwk_ObjSetTravIdPrevious( pFanout );
+            nDivsPlus++;
+            if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+                break;
+        }
+        if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+            break;
+    }
+
+    // sort the divisors by level in the increasing order
+    Vec_PtrSort( vDivs, Nwk_NodeCompareLevelsIncrease );
+
+    // add the fanins of the node
+    Nwk_ObjForEachFanin( pNode, pFanin, k )
+        Vec_PtrPush( vDivs, pFanin );
+
+/*
+    printf( "Node level = %d.  ", Nwk_ObjLevel(p->pNode) );
+    Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
+        printf( "%d ", Nwk_ObjLevel(pObj) );
+    printf( "\n" );
+*/
+//printf( "%d ", p->nDivsPlus );
+//    printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), 
+//        nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus );
+    return vDivs;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h
new file mode 100644
index 00000000..88792bf2
--- /dev/null
+++ b/src/aig/mfx/mfxInt.h
@@ -0,0 +1,160 @@
+/**CFile****************************************************************
+
+  FileName    [mfxInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __MFX_INT_H__
+#define __MFX_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "nwk.h"
+#include "mfx.h"
+#include "aig.h"
+#include "cnf.h"
+#include "satSolver.h"
+#include "satStore.h"
+#include "bdc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define MFX_FANIN_MAX   12
+
+typedef struct Mfx_Man_t_ Mfx_Man_t;
+struct Mfx_Man_t_
+{
+    // input data
+    Mfx_Par_t *         pPars;
+    Nwk_Man_t *         pNtk;
+    Aig_Man_t *         pCare;
+    Vec_Ptr_t *         vSuppsInv;
+    int                 nFaninMax;
+    // intermeditate data for the node
+    Vec_Ptr_t *         vRoots;    // the roots of the window
+    Vec_Ptr_t *         vSupp;     // the support of the window
+    Vec_Ptr_t *         vNodes;    // the internal nodes of the window
+    Vec_Ptr_t *         vDivs;     // the divisors of the node
+    Vec_Int_t *         vDivLits;  // the SAT literals of divisor nodes
+    Vec_Int_t *         vProjVars; // the projection variables
+    // intermediate simulation data
+    Vec_Ptr_t *         vDivCexes; // the counter-example for dividors
+    int                 nDivWords; // the number of words
+    int                 nCexes;    // the numbe rof current counter-examples
+    int                 nSatCalls; 
+    int                 nSatCexes;
+    // used for bidecomposition
+    Vec_Int_t *         vTruth;
+    Bdc_Man_t *         pManDec;
+    int                 nNodesDec;
+    int                 nNodesGained;
+    int                 nNodesGainedLevel;
+    // solving data
+    Aig_Man_t *         pAigWin;   // window AIG with constraints
+    Cnf_Dat_t *         pCnf;      // the CNF for the window
+    sat_solver *        pSat;      // the SAT solver used 
+    Int_Man_t *         pMan;      // interpolation manager;
+    Vec_Int_t *         vMem;      // memory for intermediate SOPs
+    Vec_Vec_t *         vLevels;   // levelized structure for updating
+    Vec_Ptr_t *         vFanins;   // the new set of fanins
+    int                 nTotConfLim; // total conflict limit
+    int                 nTotConfLevel; // total conflicts on this level
+    // the result of solving
+    int                 nFanins;   // the number of fanins
+    int                 nWords;    // the number of words
+    int                 nCares;    // the number of care minterms
+    unsigned            uCare[(MFX_FANIN_MAX<=5)?1:1<<(MFX_FANIN_MAX-5)];  // the computed care-set
+    // performance statistics
+    int                 nNodesTried;
+    int                 nNodesResub;
+    int                 nMintsCare;
+    int                 nMintsTotal;
+    int                 nNodesBad;
+    int                 nTotalDivs;
+    int                 nTimeOuts;
+    int                 nTimeOutsLevel;
+    int                 nDcMints;
+    double              dTotalRatios;
+    // node/edge stats
+    int                 nTotalNodesBeg;
+    int                 nTotalNodesEnd;
+    int                 nTotalEdgesBeg;
+    int                 nTotalEdgesEnd;
+    // statistics
+    int                 timeWin;
+    int                 timeDiv;
+    int                 timeAig;
+    int                 timeCnf;
+    int                 timeSat;
+    int                 timeInt;
+    int                 timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== mfxDiv.c ==========================================================*/
+extern Vec_Ptr_t *      Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax );
+/*=== mfxInter.c ==========================================================*/
+extern sat_solver *     Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert );
+extern Hop_Obj_t *      Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands );
+extern int              Mfx_InterplateEval( Mfx_Man_t * p, int * pCands, int nCands );
+/*=== mfxMan.c ==========================================================*/
+extern Mfx_Man_t *      Mfx_ManAlloc( Mfx_Par_t * pPars );
+extern void             Mfx_ManStop( Mfx_Man_t * p );
+extern void             Mfx_ManClean( Mfx_Man_t * p );
+/*=== mfxResub.c ==========================================================*/
+extern void             Mfx_PrintResubStats( Mfx_Man_t * p );
+extern int              Mfx_EdgeSwapEval( Mfx_Man_t * p, Nwk_Obj_t * pNode );
+extern int              Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode );
+extern int              Mfx_ResubNode2( Mfx_Man_t * p, Nwk_Obj_t * pNode );
+/*=== mfxSat.c ==========================================================*/
+extern int              Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode );
+/*=== mfxStrash.c ==========================================================*/
+extern Aig_Man_t *      Mfx_ConstructAig( Mfx_Man_t * p, Nwk_Obj_t * pNode );
+extern double           Mfx_ConstraintRatio( Mfx_Man_t * p, Nwk_Obj_t * pNode );
+/*=== mfxWin.c ==========================================================*/
+extern Vec_Ptr_t *      Mfx_ComputeRoots( Nwk_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c
new file mode 100644
index 00000000..a42e02fe
--- /dev/null
+++ b/src/aig/mfx/mfxInter.c
@@ -0,0 +1,361 @@
+/**CFile****************************************************************
+
+  FileName    [mfxInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures for computing resub function by interpolation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constraints for the two-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_SatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
+{
+    lit Lits[3];
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+        return 0;
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates miter for checking resubsitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert )
+{
+    sat_solver * pSat;
+    Aig_Obj_t * pObjPo;
+    int Lits[2], status, iVar, i, c;
+
+    // get the literal for the output of F
+    pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
+    Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
+
+    // collect the outputs of the divisors
+    Vec_IntClear( p->vProjVars );
+    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
+    {
+        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
+        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+    }
+    assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
+    if ( pCands )
+        sat_solver_store_alloc( pSat );
+
+    // load the first copy of the clauses
+    for ( i = 0; i < p->pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    // add the clause for the first output of F
+    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+    {
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+
+    // bookmark the clauses of A
+    if ( pCands )
+        sat_solver_store_mark_clauses_a( pSat );
+
+    // transform the literals
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+        p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
+    // load the second copy of the clauses
+    for ( i = 0; i < p->pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    // transform the literals
+    for ( i = 0; i < p->pCnf->nLiterals; i++ )
+        p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
+    // add the clause for the second output of F
+    Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
+    if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+    {
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+
+    if ( pCands )
+    {
+        // add relevant clauses for EXOR gates
+        for ( c = 0; c < nCands; c++ )
+        {
+            // get the variable number of this divisor
+            i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+            // get the corresponding SAT variable
+            iVar = Vec_IntEntry( p->vProjVars, i );
+            // add the corresponding EXOR gate
+            if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+            // add the corresponding clause
+            if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+        }
+        // bookmark the roots
+        sat_solver_store_mark_roots( pSat );
+    }
+    else
+    {
+        // add the clauses for the EXOR gates - and remember their outputs
+        Vec_IntForEachEntry( p->vProjVars, iVar, i )
+        {
+            if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+            {
+                sat_solver_delete( pSat );
+                return NULL;
+            }
+            Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
+        }
+        // simplify the solver
+        status = sat_solver_simplify(pSat);
+        if ( status == 0 )
+        {
+//            printf( "Mfx_CreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fInvert )
+{
+    sat_solver * pSat;
+    Sto_Man_t * pCnf = NULL;
+    unsigned * puTruth;
+    int nFanins, status;
+    int c, i, * pGloVars;
+
+    // derive the SAT solver for interpolation
+    pSat = Mfx_CreateSolverResub( p, pCands, nCands, fInvert );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    if ( status != l_False )
+    {
+        p->nTimeOuts++;
+        return NULL;
+    }
+    // get the learned clauses
+    pCnf = sat_solver_store_release( pSat );
+    sat_solver_delete( pSat );
+
+    // set the global variables
+    pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
+    for ( c = 0; c < nCands; c++ )
+    {
+        // get the variable number of this divisor
+        i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+        // get the corresponding SAT variable
+        pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+    }
+
+    // derive the interpolant
+    nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+    Sto_ManFree( pCnf );
+    assert( nFanins == nCands );
+    return puTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_InterplateEval( Mfx_Man_t * p, int * pCands, int nCands )
+{
+    unsigned * pTruth, uTruth0[2], uTruth1[2];
+    int nCounter;
+    pTruth = Mfx_InterplateTruth( p, pCands, nCands, 0 );
+    if ( nCands == 6 )
+    {
+        uTruth1[0] = pTruth[0];
+        uTruth1[1] = pTruth[1];
+    }
+    else
+    {
+        uTruth1[0] = pTruth[0];
+        uTruth1[1] = pTruth[0];
+    }
+    pTruth = Mfx_InterplateTruth( p, pCands, nCands, 1 );
+    if ( nCands == 6 )
+    {
+        uTruth0[0] = ~pTruth[0];
+        uTruth0[1] = ~pTruth[1];
+    }
+    else
+    {
+        uTruth0[0] = ~pTruth[0];
+        uTruth0[1] = ~pTruth[0];
+    }
+    nCounter  = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] );
+    nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] );
+//    printf( "%d ", nCounter );
+    return nCounter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands )
+{
+    extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
+    sat_solver * pSat;
+    Sto_Man_t * pCnf = NULL;
+    unsigned * puTruth;
+    Kit_Graph_t * pGraph;
+    Hop_Obj_t * pFunc;
+    int nFanins, status;
+    int c, i, * pGloVars;
+
+//    p->nDcMints += Mfx_InterplateEval( p, pCands, nCands );
+
+    // derive the SAT solver for interpolation
+    pSat = Mfx_CreateSolverResub( p, pCands, nCands, 0 );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    if ( status != l_False )
+    {
+        p->nTimeOuts++;
+        return NULL;
+    }
+    // get the learned clauses
+    pCnf = sat_solver_store_release( pSat );
+    sat_solver_delete( pSat );
+
+    // set the global variables
+    pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
+    for ( c = 0; c < nCands; c++ )
+    {
+        // get the variable number of this divisor
+        i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+        // get the corresponding SAT variable
+        pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+    }
+
+    // derive the interpolant
+    nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+    Sto_ManFree( pCnf );
+    assert( nFanins == nCands );
+
+    // transform interpolant into AIG
+    pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+    pFunc = Kit_GraphToHop( p->pNtk->pManHop, pGraph );
+    Kit_GraphFree( pGraph );
+    return pFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c
new file mode 100644
index 00000000..1b536f8c
--- /dev/null
+++ b/src/aig/mfx/mfxMan.c
@@ -0,0 +1,186 @@
+/**CFile****************************************************************
+
+  FileName    [mfxMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures working with the manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars )
+{
+    Mfx_Man_t * p;
+    // start the manager
+    p = ALLOC( Mfx_Man_t, 1 );
+    memset( p, 0, sizeof(Mfx_Man_t) );
+    p->pPars     = pPars;
+    p->vProjVars = Vec_IntAlloc( 100 );
+    p->vDivLits  = Vec_IntAlloc( 100 );
+    p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX);
+    p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords );
+    p->pMan      = Int_ManAlloc();
+    p->vMem      = Vec_IntAlloc( 0 );
+    p->vLevels   = Vec_VecStart( 32 );
+    p->vFanins   = Vec_PtrAlloc( 32 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfx_ManClean( Mfx_Man_t * p )
+{
+    if ( p->pAigWin )
+        Aig_ManStop( p->pAigWin );
+    if ( p->pCnf )
+        Cnf_DataFree( p->pCnf );
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    if ( p->vRoots )
+        Vec_PtrFree( p->vRoots );
+    if ( p->vSupp )
+        Vec_PtrFree( p->vSupp );
+    if ( p->vNodes )
+        Vec_PtrFree( p->vNodes );
+    if ( p->vDivs )
+        Vec_PtrFree( p->vDivs );
+    p->pAigWin = NULL;
+    p->pCnf    = NULL;
+    p->pSat    = NULL;
+    p->vRoots  = NULL;
+    p->vSupp   = NULL;
+    p->vNodes  = NULL;
+    p->vDivs   = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfx_ManPrint( Mfx_Man_t * p )
+{
+    if ( p->pPars->fResub )
+    {
+        printf( "Reduction in nodes = %5d. (%.2f %%) ", 
+            p->nTotalNodesBeg-p->nTotalNodesEnd, 
+            100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
+        printf( "Reduction in edges = %5d. (%.2f %%) ", 
+            p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
+            100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+        printf( "\n" );
+        printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", 
+            Nwk_ManNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
+        if ( p->pPars->fSwapEdge )
+            printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
+                p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) );
+        else
+            Mfx_PrintResubStats( p );
+//        printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
+    }
+    else
+    {
+        printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", 
+            Nwk_ManNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 
+            1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
+//        printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", 
+//            1.0-(p->dTotalRatios/p->nNodesTried) );
+        printf( "Nodes resyn = %d. Ratio = %5.2f.  Total AIG node gain = %d. Timeouts = %d.\n", 
+            p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
+    }
+/*
+    PRTP( "Win", p->timeWin            ,  p->timeTotal );
+    PRTP( "Div", p->timeDiv            ,  p->timeTotal );
+    PRTP( "Aig", p->timeAig            ,  p->timeTotal );
+    PRTP( "Cnf", p->timeCnf            ,  p->timeTotal );
+    PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
+    PRTP( "Int", p->timeInt            ,  p->timeTotal );
+    PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfx_ManStop( Mfx_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+        Mfx_ManPrint( p );
+    if ( p->vTruth )
+        Vec_IntFree( p->vTruth );
+    if ( p->pManDec )
+        Bdc_ManFree( p->pManDec );
+    if ( p->pCare )
+        Aig_ManStop( p->pCare );
+    if ( p->vSuppsInv )
+        Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv );
+    Mfx_ManClean( p );
+    Int_ManFree( p->pMan );
+    Vec_IntFree( p->vMem );
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vFanins );
+    Vec_IntFree( p->vProjVars );
+    Vec_IntFree( p->vDivLits );
+    Vec_PtrFree( p->vDivCexes );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
new file mode 100644
index 00000000..2eafc559
--- /dev/null
+++ b/src/aig/mfx/mfxResub.c
@@ -0,0 +1,529 @@
+/**CFile****************************************************************
+
+  FileName    [mfxResub.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: mfxResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the network after resubstitution.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfx_UpdateNetwork( Mfx_Man_t * p, Nwk_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+{
+    Nwk_Obj_t * pObjNew, * pFanin;
+    int k;
+    // create the new node
+    pObjNew = Nwk_ManCreateNode( pObj->pMan, Vec_PtrSize(vFanins), Nwk_ObjFanoutNum(pObj) );
+if ( pObjNew->Id == 19969 )
+{
+    int x = 0;
+}
+    pObjNew->pFunc = pFunc;
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
+        Nwk_ObjAddFanin( pObjNew, pFanin );
+    // replace the old node by the new node
+//printf( "Replacing node " ); Nwk_ObjPrint( stdout, pObj );
+//printf( "Inserting node " ); Nwk_ObjPrint( stdout, pObjNew );
+    // update the level of the node
+    Nwk_ManUpdate( pObj, pObjNew, p->vLevels );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints resub candidate stats.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfx_PrintResubStats( Mfx_Man_t * p )
+{
+    Nwk_Obj_t * pFanin, * pNode;
+    int i, k, nAreaCrits = 0, nAreaExpanse = 0;
+    int nFaninMax = Nwk_ManGetFaninMax(p->pNtk);
+    Nwk_ManForEachNode( p->pNtk, pNode, i )
+        Nwk_ObjForEachFanin( pNode, pFanin, k )
+        {
+            if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
+            {
+                nAreaCrits++;
+                nAreaExpanse += (int)(Nwk_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 Mfx_TryResubOnce( Mfx_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 Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
+{
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+    unsigned * pData;
+    int pCands[MFX_FANIN_MAX];
+    int RetValue, iVar, i, nCands, nWords, w, clk;
+    Nwk_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)-Nwk_ObjFaninNum(pNode), 
+            iFanin, Nwk_ObjFaninNum(pNode), 
+            Nwk_ObjFanoutNum(Nwk_ObjFanin(pNode, iFanin)) == 1 ? Nwk_ObjMffcLabel(Nwk_ObjFanin(pNode, iFanin)) : 0 );
+    }
+
+    // try fanins without the critical fanin
+    nCands = 0;
+    Vec_PtrClear( p->vFanins );
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( i == iFanin )
+            continue;
+        Vec_PtrPush( p->vFanins, pFanin );
+        iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+    }
+    RetValue = Mfx_TryResubOnce( 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 = Mfx_Interplate( p, pCands, nCands );
+        if ( pFunc == NULL )
+            return 0;
+        // update the network
+        Mfx_UpdateNetwork( 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)-Nwk_ObjFaninNum(pNode); i++ )
+            printf( "%d", i % 10 );
+        for ( i = 0; i < Nwk_ObjFaninNum(pNode); i++ )
+            if ( i == iFanin )
+                printf( "*" );
+            else
+                printf( "%c", 'a' + i );
+        printf( "\n" );
+    }
+    iVar = -1;
+    while ( 1 )
+    {
+        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)-Nwk_ObjFaninNum(pNode); iVar++ )
+        {
+            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)-Nwk_ObjFaninNum(pNode) )
+            return 0;
+
+        pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        RetValue = Mfx_TryResubOnce( 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 = Mfx_Interplate( p, pCands, nCands+1 );
+            if ( pFunc == NULL )
+                return 0;
+            // update the network
+            Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+            Mfx_UpdateNetwork( 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 Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin2 )
+{
+    int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+    unsigned * pData, * pData2;
+    int pCands[MFX_FANIN_MAX];
+    int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
+    Nwk_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)-Nwk_ObjFaninNum(pNode), 
+            iFanin, iFanin2, Nwk_ObjFaninNum(pNode), 
+            Nwk_ObjFanoutNum(Nwk_ObjFanin(pNode, iFanin)) == 1 ? Nwk_ObjMffcLabel(Nwk_ObjFanin(pNode, iFanin)) : 0 );
+    }
+
+    // try fanins without the critical fanin
+    nCands = 0;
+    Vec_PtrClear( p->vFanins );
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( i == iFanin || i == iFanin2 )
+            continue;
+        Vec_PtrPush( p->vFanins, pFanin );
+        iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i;
+        pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+    }
+    RetValue = Mfx_TryResubOnce( 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 = Mfx_Interplate( p, pCands, nCands );
+        if ( pFunc == NULL )
+            return 0;
+        // update the network
+        Mfx_UpdateNetwork( 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)-Nwk_ObjFaninNum(pNode); i++ )
+            printf( "%d", i % 10 );
+        for ( i = 0; i < Nwk_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)-Nwk_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)-Nwk_ObjFaninNum(pNode) )
+            return 0;
+
+        pCands[nCands]   = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 );
+        pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+        RetValue = Mfx_TryResubOnce( 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 = Mfx_Interplate( 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 );
+            Mfx_UpdateNetwork( 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 Mfx_EdgeSwapEval( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    int i;
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        Mfx_SolveSatResub( p, pNode, i, 0, 1 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    int i;
+    // try replacing area critical fanins
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Mfx_SolveSatResub( p, pNode, i, 0, 0 ) )
+                return 1;
+        }
+    // try removing redundant edges
+    if ( !p->pPars->fArea )
+    {
+        Nwk_ObjForEachFanin( pNode, pFanin, i )
+            if ( Nwk_ObjIsCi(pFanin) || Nwk_ObjFanoutNum(pFanin) != 1 )
+            {
+                if ( Mfx_SolveSatResub( p, pNode, i, 1, 0 ) )
+                    return 1;
+            }
+    }
+    if ( Nwk_ObjFaninNum(pNode) == p->nFaninMax )
+        return 0;
+    // try replacing area critical fanins while adding two new fanins
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Mfx_SolveSatResub2( p, pNode, i, -1 ) )
+                return 1;
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resubstitution for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_ResubNode2( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin, * pFanin2;
+    int i, k;
+/*
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
+        {
+            if ( Mfx_SolveSatResub( p, pNode, i, 0, 0 ) )
+                return 1;
+        }
+*/
+    if ( Nwk_ObjFaninNum(pNode) < 2 )
+        return 0;
+    // try replacing one area critical fanin and one other fanin while adding two new fanins
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
+        {
+            // consider second fanin to remove at the same time
+            Nwk_ObjForEachFanin( pNode, pFanin2, k )
+            {
+                if ( i != k && Mfx_SolveSatResub2( p, pNode, i, k ) )
+                    return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c
new file mode 100644
index 00000000..9dd42e8c
--- /dev/null
+++ b/src/aig/mfx/mfxSat.c
@@ -0,0 +1,140 @@
+/**CFile****************************************************************
+
+  FileName    [mfxSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to compute don't-cares using SAT.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Enumerates through the SAT assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mfx_SolveSat_iter( Mfx_Man_t * p )
+{
+    int Lits[MFX_FANIN_MAX];
+    int RetValue, nBTLimit, iVar, b, Mint;
+    if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts )
+        return -1;
+    nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0;
+    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False );
+    if ( RetValue == l_Undef )
+        return -1;
+    if ( RetValue == l_False )
+        return 0;
+    p->nCares++;
+    // add SAT assignment to the solver
+    Mint = 0;
+    Vec_IntForEachEntry( p->vProjVars, iVar, b )
+    {
+        Lits[b] = toLit( iVar );
+        if ( sat_solver_var_value( p->pSat, iVar ) )
+        {
+            Mint |= (1 << b);
+            Lits[b] = lit_neg( Lits[b] );
+        }
+    }
+    assert( !Aig_InfoHasBit(p->uCare, Mint) );
+    Aig_InfoSetBit( p->uCare, Mint );
+    // add the blocking clause
+    RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) );
+    if ( RetValue == 0 )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Enumerates through the SAT assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Aig_Obj_t * pObjPo;
+    int RetValue, i;
+    // collect projection variables
+    Vec_IntClear( p->vProjVars );
+    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) )
+    {
+        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
+        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+    }
+
+    // prepare the truth table of care set
+    p->nFanins = Vec_IntSize( p->vProjVars );
+    p->nWords = Aig_TruthWordNum( p->nFanins );
+    memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
+
+    // iterate through the SAT assignments
+    p->nCares = 0;
+    p->nTotConfLim = p->pPars->nBTLimit;
+    while ( (RetValue = Mfx_SolveSat_iter(p)) == 1 );
+    if ( RetValue == -1 )
+        return 0;
+
+    // write statistics
+    p->nMintsCare  += p->nCares;
+    p->nMintsTotal += (1<<p->nFanins);
+
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf( "Node %4d : Care = %2d. Total = %2d.  ", pNode->Id, p->nCares, (1<<p->nFanins) );
+//        Kit_TruthPrintBinary( stdout, p->uCare, (1<<p->nFanins) );
+        printf( "\n" );
+    }
+
+    // map the care 
+    if ( p->nFanins > 4 )
+        return 1;
+    if ( p->nFanins == 4 )
+        p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
+    if ( p->nFanins == 3 )
+        p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24);
+    if ( p->nFanins == 2 )
+        p->uCare[0] = p->uCare[0] | (p->uCare[0] <<  4) | (p->uCare[0] <<  8) | (p->uCare[0] << 12) |
+              (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
+    assert( p->nFanins != 1 );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxStrash.c b/src/aig/mfx/mfxStrash.c
new file mode 100644
index 00000000..5cb6452f
--- /dev/null
+++ b/src/aig/mfx/mfxStrash.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+  FileName    [mfxStrash.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Structural hashing of the window with ODCs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Construct BDDs and mark AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ConvertHopToAig_rec( Hop_Obj_t * pObj, Aig_Man_t * pMan )
+{
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return;
+    Nwk_ConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan ); 
+    Nwk_ConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan );
+    pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) ); 
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from AIG to BDD representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ConvertHopToAig( Nwk_Obj_t * pObjOld, Aig_Man_t * pMan )
+{
+    Hop_Man_t * pHopMan;
+    Hop_Obj_t * pRoot;
+    Nwk_Obj_t * pFanin;
+    int i;
+    // get the local AIG
+    pHopMan = pObjOld->pMan->pManHop;
+    pRoot = pObjOld->pFunc;
+    // check the case of a constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+    {
+        pObjOld->pCopy = (Nwk_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) );
+        pObjOld->pNext = pObjOld->pCopy;
+        return;
+    }
+
+    // assign the fanin nodes
+    Nwk_ObjForEachFanin( pObjOld, pFanin, i )
+        Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
+    // construct the AIG
+    Nwk_ConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
+    pObjOld->pCopy = (Nwk_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+
+    // assign the fanin nodes
+    Nwk_ObjForEachFanin( pObjOld, pFanin, i )
+        Hop_ManPi(pHopMan, i)->pData = pFanin->pNext;
+    // construct the AIG
+    Nwk_ConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
+    pObjOld->pNext = (Nwk_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the care set of the node under ODCs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Mfx_ConstructAig_rec( Mfx_Man_t * p, Nwk_Obj_t * pNode, Aig_Man_t * pMan )
+{
+    Aig_Obj_t * pRoot, * pExor;
+    Nwk_Obj_t * pObj;
+    int i;
+    // assign AIG nodes to the leaves
+    Vec_PtrForEachEntry( p->vSupp, pObj, i )
+        pObj->pCopy = pObj->pNext = (Nwk_Obj_t *)Aig_ObjCreatePi( pMan );
+    // strash intermediate nodes
+    Nwk_ManIncrementTravId( pNode->pMan );
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    {
+        Nwk_ConvertHopToAig( pObj, pMan );
+        if ( pObj == pNode )
+            pObj->pNext = Aig_Not(pObj->pNext);
+    }
+    // create the observability condition
+    pRoot = Aig_ManConst0(pMan);
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+    {
+        pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext );
+        pRoot = Aig_Or( pMan, pRoot, pExor );
+    }
+    return pRoot;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds relevant constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Mfx_ConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan )
+{
+    Aig_Obj_t * pObj0, * pObj1;
+    if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
+        return pObj->pData;
+    Aig_ObjSetTravIdCurrent( pCare, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+        return pObj->pData = NULL;
+    pObj0 = Mfx_ConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
+    if ( pObj0 == NULL )
+        return pObj->pData = NULL;
+    pObj1 = Mfx_ConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
+    if ( pObj1 == NULL )
+        return pObj->pData = NULL;
+    pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
+    pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
+    return pObj->pData = Aig_And( pMan, pObj0, pObj1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManVerifyManager( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        assert( pObj->pMan == pNtk );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG for the window with constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Mfx_ConstructAig( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Aig_Man_t * pMan;
+    Nwk_Obj_t * pFanin;
+    Aig_Obj_t * pObjAig, * pPi, * pPo;
+    Vec_Int_t * vOuts;
+    int i, k, iOut;
+//    Nwk_ManVerifyManager( p->pNtk );
+    // start the new manager
+    pMan = Aig_ManStart( 1000 );
+    // construct the root node's AIG cone
+    pObjAig = Mfx_ConstructAig_rec( p, pNode, pMan );
+//    assert( Aig_ManConst1(pMan) == pObjAig );
+    Aig_ObjCreatePo( pMan, pObjAig );
+    if ( p->pCare )
+    {
+        // mark the care set
+        Aig_ManIncrementTravId( p->pCare );
+        Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+        {
+            pPi = Aig_ManPi( p->pCare, pFanin->PioId );
+            Aig_ObjSetTravIdCurrent( p->pCare, pPi );
+            pPi->pData = pFanin->pCopy;
+        }
+        // construct the constraints
+        Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+        {
+            vOuts = Vec_PtrEntry( p->vSuppsInv, pFanin->PioId );
+            Vec_IntForEachEntry( vOuts, iOut, k )
+            {
+                pPo = Aig_ManPo( p->pCare, iOut );
+                if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
+                    continue;
+                Aig_ObjSetTravIdCurrent( p->pCare, pPo );
+                if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                    continue;
+                pObjAig = Mfx_ConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
+                if ( pObjAig == NULL )
+                    continue;
+                pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+                Aig_ObjCreatePo( pMan, pObjAig );
+            }
+        }
+/*
+        Aig_ManForEachPo( p->pCare, pPo, i )
+        {
+//            assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
+            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                continue;
+            pObjAig = Mfx_ConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
+            if ( pObjAig == NULL )
+                continue;
+            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
+*/
+    }
+    if ( p->pPars->fResub )
+    {
+        // construct the node
+        pObjAig = (Aig_Obj_t *)pNode->pCopy;
+        Aig_ObjCreatePo( pMan, pObjAig );
+        // construct the divisors
+        Vec_PtrForEachEntry( p->vDivs, pFanin, i )
+        {
+            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
+    }
+    else
+    {
+        // construct the fanins
+        Nwk_ObjForEachFanin( pNode, pFanin, i )
+        {
+            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
+    }
+    Aig_ManCleanup( pMan );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG for the window with constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Nwk_AigForConstraints( Mfx_Man_t * p, Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    Aig_Man_t * pMan;
+    Aig_Obj_t * pPi, * pPo, * pObjAig, * pObjRoot;
+    Vec_Int_t * vOuts;
+    int i, k, iOut;
+    if ( p->pCare == NULL )
+        return NULL;
+    pMan = Aig_ManStart( 1000 );
+    // mark the care set
+    Aig_ManIncrementTravId( p->pCare );
+    Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+    {
+        pPi = Aig_ManPi( p->pCare, pFanin->PioId );
+        Aig_ObjSetTravIdCurrent( p->pCare, pPi );
+        pPi->pData = Aig_ObjCreatePi(pMan);
+    }
+    // construct the constraints
+    pObjRoot = Aig_ManConst1(pMan);
+    Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+    {
+        vOuts = Vec_PtrEntry( p->vSuppsInv, pFanin->PioId );
+        Vec_IntForEachEntry( vOuts, iOut, k )
+        {
+            pPo = Aig_ManPo( p->pCare, iOut );
+            if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
+                continue;
+            Aig_ObjSetTravIdCurrent( p->pCare, pPo );
+            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                continue;
+            pObjAig = Mfx_ConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
+            if ( pObjAig == NULL )
+                continue;
+            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+            pObjRoot = Aig_And( pMan, pObjRoot, pObjAig );
+        }
+    }
+    Aig_ObjCreatePo( pMan, pObjRoot );
+    Aig_ManCleanup( pMan );
+    return pMan;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfxWin.c b/src/aig/mfx/mfxWin.c
new file mode 100644
index 00000000..e84a9b90
--- /dev/null
+++ b/src/aig/mfx/mfxWin.c
@@ -0,0 +1,112 @@
+/**CFile****************************************************************
+
+  FileName    [mfxWin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedures to compute windows stretching to the PIs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfxWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfxInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node should be a root.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Mfx_ComputeRootsCheck( Nwk_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
+{
+    Nwk_Obj_t * pFanout;
+    int i;
+    // the node is the root if one of the following is true:
+    // (1) the node has more than fanouts than the limit
+    if ( Nwk_ObjFanoutNum(pNode) > nFanoutLimit )
+        return 1;
+    // (2) the node has CO fanouts
+    // (3) the node has fanouts above the cutoff level
+    Nwk_ObjForEachFanout( pNode, pFanout, i )
+        if ( Nwk_ObjIsCo(pFanout) || pFanout->Level > nLevelMax )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfx_ComputeRoots_rec( Nwk_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
+{
+    Nwk_Obj_t * pFanout;
+    int i;
+    assert( Nwk_ObjIsNode(pNode) );
+    if ( Nwk_ObjIsTravIdCurrent(pNode) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pNode );
+    // check if the node should be the root
+    if ( Mfx_ComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
+        Vec_PtrPush( vRoots, pNode );
+    else // if not, explore its fanouts
+        Nwk_ObjForEachFanout( pNode, pFanout, i )
+            Mfx_ComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description [Returns 1 if the only root is this node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Mfx_ComputeRoots( Nwk_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit )
+{
+    Vec_Ptr_t * vRoots;
+    vRoots = Vec_PtrAlloc( 10 );
+    Nwk_ManIncrementTravId( pNode->pMan );
+    Mfx_ComputeRoots_rec( pNode, pNode->Level + nWinTfoMax, nFanoutLimit, vRoots );
+    assert( Vec_PtrSize(vRoots) > 0 );
+//    if ( Vec_PtrSize(vRoots) == 1 && Vec_PtrEntry(vRoots, 0) == pNode )
+//        return 0;
+    return vRoots;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/mfx_.c b/src/aig/mfx/mfx_.c
new file mode 100644
index 00000000..32caf7ff
--- /dev/null
+++ b/src/aig/mfx/mfx_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [mfs_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfs_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/mfx/module.make b/src/aig/mfx/module.make
new file mode 100644
index 00000000..22b9b72a
--- /dev/null
+++ b/src/aig/mfx/module.make
@@ -0,0 +1,8 @@
+SRC +=  src/aig/mfx/mfxCore.c \
+    src/aig/mfx/mfxDiv.c \
+    src/aig/mfx/mfxInter.c \
+    src/aig/mfx/mfxMan.c \
+    src/aig/mfx/mfxResub.c \
+    src/aig/mfx/mfxSat.c \
+    src/aig/mfx/mfxStrash.c \
+    src/aig/mfx/mfxWin.c