Version abc80420

6 files changed, 1364 insertions, 2 deletions

diff --git a/src/aig/nwk/module.make b/src/aig/nwk/module.make
index 3cf2acc6..c0447823 100644
--- a/src/aig/nwk/module.make
+++ b/src/aig/nwk/module.make
@@ -1,7 +1,9 @@
-SRC +=    src/aig/nwk/nwkCheck.c \
+SRC +=    src/aig/nwk/nwkAig.c \
+    src/aig/nwk/nwkCheck.c \
     src/aig/nwk/nwkBidec.c \
     src/aig/nwk/nwkDfs.c \
     src/aig/nwk/nwkFanio.c \
+    src/aig/nwk/nwkFlow.c \
     src/aig/nwk/nwkMan.c \
     src/aig/nwk/nwkMap.c \
     src/aig/nwk/nwkObj.c \
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index c087cde8..d0a871cf 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -75,6 +75,10 @@ struct Nwk_Man_t_
     Vec_Ptr_t *        vTemp;          // array used for incremental updates
     int                nTravIds;       // the counter of traversal IDs
     int                nRealloced;     // the number of realloced nodes
+    // sequential information
+    int                nLatches;       // the total number of latches 
+    int                nTruePis;       // the number of true primary inputs
+    int                nTruePos;       // the number of true primary outputs
 };
 
 struct Nwk_Obj_t_
@@ -88,7 +92,8 @@ struct Nwk_Obj_t_
     unsigned           fInvert  :  1;  // complemented attribute
     unsigned           MarkA    :  1;  // temporary mark  
     unsigned           MarkB    :  1;  // temporary mark
-    unsigned           PioId    : 26;  // number of this node in the PI/PO list
+    unsigned           MarkC    :  1;  // temporary mark
+    unsigned           PioId    : 25;  // number of this node in the PI/PO list
     int                Id;             // unique ID
     int                TravId;         // traversal ID
     // timing information
@@ -140,6 +145,8 @@ static inline int         Nwk_ObjIsNode( Nwk_Obj_t * p )          { return p->Ty
 static inline int         Nwk_ObjIsLatch( Nwk_Obj_t * p )         { return p->Type == NWK_OBJ_LATCH;            } 
 static inline int         Nwk_ObjIsPi( Nwk_Obj_t * p )            { return Nwk_ObjIsCi(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1); } 
 static inline int         Nwk_ObjIsPo( Nwk_Obj_t * p )            { return Nwk_ObjIsCo(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1);  }
+static inline int         Nwk_ObjIsLi( Nwk_Obj_t * p )            { return p->pMan->nTruePos && Nwk_ObjIsCo(p) && (int)p->PioId >= p->pMan->nTruePos;       } 
+static inline int         Nwk_ObjIsLo( Nwk_Obj_t * p )            { return p->pMan->nTruePis && Nwk_ObjIsCi(p) && (int)p->PioId >= p->pMan->nTruePis;       } 
 
 static inline float       Nwk_ObjArrival( Nwk_Obj_t * pObj )                 { return pObj->tArrival;           }
 static inline float       Nwk_ObjRequired( Nwk_Obj_t * pObj )                { return pObj->tRequired;          }
@@ -190,10 +197,26 @@ static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { r
 #define Nwk_ObjForEachFanout( pObj, pFanout, i )                                \
     for ( i = 0; (i < (int)(pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
 
+// sequential iterators
+#define Nwk_ManForEachPiSeq( p, pObj, i )                                           \
+    Vec_PtrForEachEntryStop( p->vCis, pObj, i, (p)->nTruePis )
+#define Nwk_ManForEachPoSeq( p, pObj, i )                                           \
+    Vec_PtrForEachEntryStop( p->vCos, pObj, i, (p)->nTruePos )
+#define Nwk_ManForEachLoSeq( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCis, i+(p)->nTruePis)), 1); i++ )
+#define Nwk_ManForEachLiSeq( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCos, i+(p)->nTruePos)), 1); i++ )
+#define Nwk_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )                               \
+    for ( i = 0; (i < (p)->nLatches) && (((pObjLi) = Nwk_ManCo(p, i+(p)->nTruePos)), 1)        \
+        && (((pObjLo) = Nwk_ManCi(p, i+(p)->nTruePis)), 1); i++ )
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== nwkAig.c ==========================================================*/
+extern Vec_Ptr_t *     Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
 /*=== nwkBidec.c ==========================================================*/
 extern void            Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
 extern Hop_Obj_t *     Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
@@ -221,6 +244,9 @@ extern void            Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin
 extern void            Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
 extern void            Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
 extern void            Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
+/*=== nwkFlow.c ============================================================*/
+extern Vec_Ptr_t *     Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
+extern Vec_Ptr_t *     Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
 /*=== nwkMan.c ============================================================*/
 extern Nwk_Man_t *     Nwk_ManAlloc();
 extern void            Nwk_ManFree( Nwk_Man_t * p );
@@ -258,6 +284,7 @@ extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_
 extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
 extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
 extern void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
+extern void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkAig.c b/src/aig/nwk/nwkAig.c
new file mode 100644
index 00000000..7421348a
--- /dev/null
+++ b/src/aig/nwk/nwkAig.c
@@ -0,0 +1,107 @@
+/**CFile****************************************************************
+
+  FileName    [nwkAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Translating of AIG into the network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Man_t * Nwk_ManDeriveFromAig( Aig_Man_t * p )
+{
+    Nwk_Man_t * pNtk;
+    Aig_Obj_t * pObj;
+    int i;
+    pNtk = Nwk_ManAlloc();
+    pNtk->nFanioPlus = 0;
+    Hop_ManStop( pNtk->pManHop );
+    pNtk->pManHop = NULL;
+    pNtk->pName = Aig_UtilStrsav( p->pName );
+    pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
+    pObj = Aig_ManConst1(p);
+    pObj->pData = Nwk_ManCreateNode( pNtk, 0, pObj->nRefs );
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Nwk_ManCreateCi( pNtk, pObj->nRefs );
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        pObj->pData = Nwk_ManCreateNode( pNtk, 2, pObj->nRefs );
+        Nwk_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData );
+        Nwk_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData );
+    }
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObj->pData = Nwk_ManCreateCo( pNtk );
+        Nwk_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData );
+    }
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Man_t * pNtk;
+    Nwk_Obj_t * pNode;
+    Aig_Obj_t * pObj;
+    int i;
+    pNtk = Nwk_ManDeriveFromAig( p );
+    if ( fForward )
+        vNodes = Nwk_ManRetimeCutForward( pNtk, Aig_ManRegNum(p), fVerbose );
+    else
+        vNodes = Nwk_ManRetimeCutBackward( pNtk, Aig_ManRegNum(p), fVerbose );
+    Aig_ManForEachObj( p, pObj, i )
+        ((Nwk_Obj_t *)pObj->pData)->pCopy = pObj;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        Vec_PtrWriteEntry( vNodes, i, pNode->pCopy );
+    Nwk_ManFree( pNtk );
+    assert( Vec_PtrSize(vNodes) <= Aig_ManRegNum(p) );
+    return vNodes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c
new file mode 100644
index 00000000..b245628a
--- /dev/null
+++ b/src/aig/nwk/nwkFlow.c
@@ -0,0 +1,593 @@
+/**CFile****************************************************************
+
+  FileName    [nwkFlow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Max-flow/min-cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// predecessors
+static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj )                   { return pObj->pCopy;        }
+static inline int         Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; }
+// sink
+static inline int         Nwk_ObjIsSink( Nwk_Obj_t * pObj )                 { return pObj->MarkA;        }
+static inline void        Nwk_ObjSetSink( Nwk_Obj_t * pObj )                { pObj->MarkA = 1;           }
+// flow
+static inline int         Nwk_ObjHasFlow( Nwk_Obj_t * pObj )                { return pObj->MarkB;        }
+static inline void        Nwk_ObjSetFlow( Nwk_Obj_t * pObj )                { pObj->MarkB = 1;           }
+static inline void        Nwk_ObjClearFlow( Nwk_Obj_t * pObj )              { pObj->MarkB = 0;           }
+ 
+// representation of visited nodes
+// pObj->TravId  < pNtk->nTravIds-2   --- not visited
+// pObj->TravId == pNtk->nTravIds-2   --- visited bot only
+// pObj->TravId == pNtk->nTravIds-1   --- visited top only
+// pObj->TravId == pNtk->nTravIds     --- visited bot and top
+static inline int  Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj )   
+{
+    return pObj->TravId == pObj->pMan->nTravIds - 2;
+}
+static inline int  Nwk_ObjVisitedBot( Nwk_Obj_t * pObj )     
+{ 
+    return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds; 
+}
+static inline int  Nwk_ObjVisitedTop( Nwk_Obj_t * pObj )     
+{ 
+    return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds; 
+}
+static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj )  
+{
+    if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+        pObj->TravId = pObj->pMan->nTravIds - 2;
+    else if ( pObj->TravId == pObj->pMan->nTravIds - 1 )
+        pObj->TravId = pObj->pMan->nTravIds;
+    else
+        assert( 0 );
+}
+static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj )  
+{
+    if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+        pObj->TravId = pObj->pMan->nTravIds - 1;
+    else if ( pObj->TravId == pObj->pMan->nTravIds - 2 )
+        pObj->TravId = pObj->pMan->nTravIds;
+    else
+        assert( 0 );
+}
+static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan )
+{
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManIncrementTravId( pMan );
+}
+
+static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks TFI of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkTfiCone_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return;
+    pObj->MarkA = 1;
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        Nwk_ManMarkTfiCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks TFO of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkTfoCone_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return;
+    pObj->MarkA = 1;
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        Nwk_ManMarkTfoCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast forward flow pushing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushForwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 0;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjHasFlow(pObj) )
+        return 0;
+    if ( Nwk_ObjIsSink(pObj) )
+    {
+        Nwk_ObjSetFlow(pObj);
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) )
+        {
+            Nwk_ObjSetFlow(pObj);
+            return Nwk_ObjSetPred( pObj, pPred );
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast backward flow pushing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushBackwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 0;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjHasFlow(pObj) )
+        return 0;
+    if ( Nwk_ObjIsSink(pObj) )
+    {
+        Nwk_ObjSetFlow(pObj);
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) )
+        {
+            Nwk_ObjSetFlow(pObj);
+            return Nwk_ObjSetPred( pObj, pPred );
+        }
+    return 0;
+}
+  
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the bottom part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjVisitedBot(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedBot(pObj);
+    // propagate through the internal edge
+    if ( Nwk_ObjHasFlow(pObj) )
+    {
+        if ( Nwk_ObjPred(pObj) )
+            if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+                return Nwk_ObjSetPred( pObj, pPred ); 
+    }
+    else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) )
+    {
+        Nwk_ObjSetFlow( pObj );
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    // try to push through the fanins
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the top part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjVisitedTop(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedTop(pObj);
+    // check if this is the sink
+    if ( Nwk_ObjIsSink(pObj) )
+        return 1;
+    // try to push through the fanouts
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+            return 1;
+    // redirect the flow
+    if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) )
+        if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+        {
+            Nwk_ObjClearFlow( pObj );
+            return Nwk_ObjSetPred( pObj, NULL );
+        }
+    return 0;
+}
+  
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the bottom part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    if ( Nwk_ObjVisitedBot(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedBot(pObj);
+    // propagate through the internal edge
+    if ( Nwk_ObjHasFlow(pObj) )
+    {
+        if ( Nwk_ObjPred(pObj) )
+            if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+                return Nwk_ObjSetPred( pObj, pPred ); 
+    }
+    else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) )
+    {
+        Nwk_ObjSetFlow( pObj );
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the top part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjVisitedTop(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedTop(pObj);
+    // check if this is the sink
+    if ( Nwk_ObjIsSink(pObj) )
+        return 1;
+    // try to push through the fanins
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) )
+            return 1;
+    // try to push through the fanouts
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) )
+            return 1;
+    // redirect the flow
+    if ( Nwk_ObjHasFlow(pObj) )
+        if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+        {
+            Nwk_ObjClearFlow( pObj );
+            return Nwk_ObjSetPred( pObj, NULL );
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if there is an unmarked path to a CI.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return 1;
+    if ( Nwk_ObjIsLo(pObj) )
+        return 0;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 1;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( !Nwk_ManVerifyCut_rec( pNext ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the forward cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutForward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    // mark the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        assert( pObj->MarkA == 0 );
+        pObj->MarkA = 1;
+    }
+    // traverse from the COs
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManForEachCo( pMan, pObj, i )
+        if ( !Nwk_ManVerifyCut_rec( pObj ) )
+            printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" );
+    // unmark the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->MarkA = 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the forward cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutBackward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes minimum cut for forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj;
+    int i, RetValue, Counter = 0, Counter2 = 0;
+    int clk = clock();
+    // set the sequential parameters
+    pMan->nLatches = nLatches;
+    pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+    pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+    // mark the COs and the TFO of PIs
+    Nwk_ManForEachCo( pMan, pObj, i )
+        pObj->MarkA = 1;
+    Nwk_ManForEachPiSeq( pMan, pObj, i )
+        Nwk_ManMarkTfoCone_rec( pObj );
+    // start flow computation from each LO
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLoSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter++;
+    }
+    if ( fVerbose )
+    printf( "Forward: Max-flow1 = %5d.  ", Counter );
+    // continue flow computation from each LO
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLoSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter2++;
+    }
+    if ( fVerbose )
+    printf( "Max-flow2 = %5d.  ", Counter+Counter2 );
+    // repeat flow computation from each LO
+    if ( Counter2 > 0 )
+    {
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Nwk_ManForEachLoSeq( pMan, pObj, i )
+        {
+            RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL );
+            assert( !RetValue );
+        }
+    }
+    // cut is a set of nodes whose bottom is visited but top is not visited
+    vNodes = Vec_PtrAlloc( Counter+Counter2 );
+    Counter = 0;
+    Nwk_ManForEachObj( pMan, pObj, i )
+    {
+        if ( Nwk_ObjVisitedBotOnly(pObj) )
+        {
+            assert( Nwk_ObjHasFlow(pObj) );
+            assert( !Nwk_ObjIsCo(pObj) );
+            Vec_PtrPush( vNodes, pObj );
+            Counter += Nwk_ObjIsCi(pObj);
+        }
+    }
+    Nwk_ManCleanMarks( pMan );
+    assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
+    if ( fVerbose )
+    {
+    printf( "Min-cut = %5d.  Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+    PRT( "Time", clock() - clk );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes minimum cut for backward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj;
+    int i, RetValue, Counter = 0, Counter2 = 0;
+    int clk = clock();
+    // set the sequential parameters
+    pMan->nLatches = nLatches;
+    pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+    pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+    // mark the CIs, the TFI of POs, and the constant nodes
+    Nwk_ManForEachCi( pMan, pObj, i )
+        pObj->MarkA = 1;
+    Nwk_ManForEachPoSeq( pMan, pObj, i )
+        Nwk_ManMarkTfiCone_rec( pObj );
+    Nwk_ManForEachObj( pMan, pObj, i )
+        if ( Nwk_ObjFaninNum(pObj) == 0 )
+            pObj->MarkA = 1;
+    // start flow computation from each LI driver
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter++; 
+    }
+    if ( fVerbose )
+    printf( "Backward: Max-flow1 = %5d.  ", Counter );
+    // continue flow computation from each LI driver
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter2++;
+    }
+    if ( fVerbose )
+    printf( "Max-flow2 = %5d.  ", Counter+Counter2 );
+    // repeat flow computation from each LI driver
+    if ( Counter2 > 0 )
+    {
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Nwk_ManForEachLiSeq( pMan, pObj, i )
+        {
+            RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL );
+            assert( !RetValue );
+        }
+    }
+    // cut is a set of nodes whose bottom is visited but top is not visited
+    vNodes = Vec_PtrAlloc( Counter+Counter2 );
+    Nwk_ManForEachObj( pMan, pObj, i )
+    {
+        if ( Nwk_ObjVisitedBotOnly(pObj) )
+        {
+            assert( Nwk_ObjHasFlow(pObj) );
+            assert( !Nwk_ObjIsCo(pObj) );
+            Vec_PtrPush( vNodes, pObj );
+        }
+    }
+    // count CO drivers
+    Counter = 0;
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+        if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
+            Counter++;
+    Nwk_ManCleanMarks( pMan );
+    assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
+    if ( fVerbose )
+    {
+    printf( "Min-cut = %5d.  Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+    PRT( "Time", clock() - clk );
+    }
+    return vNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index f30f7251..1ef0af67 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -447,6 +447,24 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
         nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk)  );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    Nwk_ManForEachObj( pMan, pObj, i )
+        pObj->MarkA = pObj->MarkB = 0;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/nwk/nwkUtil_old.c b/src/aig/nwk/nwkUtil_old.c
new file mode 100644
index 00000000..c6f5c136
--- /dev/null
+++ b/src/aig/nwk/nwkUtil_old.c
@@ -0,0 +1,615 @@
+/**CFile****************************************************************
+
+  FileName    [nwkUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+#include "kit.h"
+#include <math.h>
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the current traversal ID of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    if ( pNtk->nTravIds >= (1<<26)-1 )
+    {
+        pNtk->nTravIds = 0;
+        Nwk_ManForEachObj( pNtk, pObj, i )
+            pObj->TravId = 0;
+    }
+    pNtk->nTravIds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the maximum number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, nFaninsMax = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( nFaninsMax < Nwk_ObjFaninNum(pNode) )
+            nFaninsMax = Nwk_ObjFaninNum(pNode);
+    }
+    return nFaninsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the total number of all fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, nFanins = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+        nFanins += Nwk_ObjFaninNum(pNode);
+    return nFanins;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPiNum( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, Counter = 0;
+    Nwk_ManForEachCi( pNtk, pNode, i )
+        Counter += Nwk_ObjIsPi( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPoNum( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, Counter = 0;
+    Nwk_ManForEachCo( pNtk, pNode, i )
+        Counter += Nwk_ObjIsPo( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of BDD nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, nNodes = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( pNode->pFunc == NULL )
+        {
+            printf( "Nwk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
+            continue;
+        }
+        if ( Nwk_ObjFaninNum(pNode) < 2 )
+            continue;
+        nNodes += Hop_DagSize( pNode->pFunc );
+    }
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
+{
+    int Diff = (*pp1)->Level - (*pp2)->Level;
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
+{
+    int Diff = (*pp1)->Level - (*pp2)->Level;
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjPrint( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    printf( "ObjId = %5d.  ", pObj->Id );
+    if ( Nwk_ObjIsPi(pObj) )
+        printf( "PI" );
+    if ( Nwk_ObjIsPo(pObj) )
+        printf( "PO" );
+    if ( Nwk_ObjIsNode(pObj) )
+        printf( "Node" );
+    printf( "   Fanins = " );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "   Fanouts = " );
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Nwk_Obj_t * pObj, * pFanin;
+    Aig_MmFlex_t * pMem;
+    char * pSop = NULL;
+    unsigned * pTruth;
+    int i, k, nDigits, Counter = 0;
+    if ( Nwk_ManPoNum(pNtk) == 0 )
+    {
+        printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" );
+        return;
+    }
+    // collect nodes in the DFS order
+    nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) );
+    // write the file 
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" );
+//    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
+    fprintf( pFile, ".model %s\n", pNtk->pName );
+    // write PIs
+    fprintf( pFile, ".inputs" );
+    Nwk_ManForEachCi( pNtk, pObj, i )
+        if ( vPiNames )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+    fprintf( pFile, "\n" );
+    // write POs
+    fprintf( pFile, ".outputs" );
+    Nwk_ManForEachCo( pNtk, pObj, i )
+        if ( vPoNames )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+    fprintf( pFile, "\n" );
+    // write nodes
+    pMem = Aig_MmFlexStart();
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    vNodes = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( !Nwk_ObjIsNode(pObj) )
+            continue;
+        // derive SOP for the AIG
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        if ( Hop_IsComplement(pObj->pFunc) )
+            Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+        pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+        // write the node
+        fprintf( pFile, ".names" );
+        if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            Nwk_ObjForEachFanin( pObj, pFanin, k )
+                if ( vPiNames && Nwk_ObjIsPi(pFanin) )
+                    fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) );
+                else
+                    fprintf( pFile, " n%0*d", nDigits, pFanin->Id );
+        }
+        fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+        // write the function
+        fprintf( pFile, "%s", pSop );
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    Vec_PtrFree( vNodes );
+    Aig_MmFlexStop( pMem, 0 );
+    // write POs
+    Nwk_ManForEachCo( pNtk, pObj, i )
+    {
+        fprintf( pFile, ".names" );
+        if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) )
+            fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id );
+        if ( vPoNames )
+            fprintf( pFile, " %s\n", Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) );
+        else
+            fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+        fprintf( pFile, "%d 1\n", !pObj->fInvert );
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the distribution of fanins/fanouts in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
+{
+    char Buffer[100];
+    Nwk_Obj_t * pNode;
+    Vec_Int_t * vFanins, * vFanouts;
+    int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll;
+    int i, k, nSizeMax;
+
+    // determine the largest fanin and fanout
+    nFaninsMax = nFanoutsMax = 0;
+    nFaninsAll = nFanoutsAll = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Nwk_ObjFaninNum(pNode);
+        nFanouts = Nwk_ObjFanoutNum(pNode);
+        nFaninsAll  += nFanins;
+        nFanoutsAll += nFanouts;
+        nFaninsMax   = AIG_MAX( nFaninsMax, nFanins );
+        nFanoutsMax  = AIG_MAX( nFanoutsMax, nFanouts );
+    }
+
+    // allocate storage for fanin/fanout numbers
+    nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+    vFanins  = Vec_IntStart( nSizeMax );
+    vFanouts = Vec_IntStart( nSizeMax );
+
+    // count the number of fanins and fanouts
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Nwk_ObjFaninNum(pNode);
+        nFanouts = Nwk_ObjFanoutNum(pNode);
+//        nFanouts = Nwk_NodeMffcSize(pNode);
+
+        if ( nFanins < 10 )
+            Vec_IntAddToEntry( vFanins, nFanins, 1 );
+        else if ( nFanins < 100 )
+            Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 );
+        else if ( nFanins < 1000 )
+            Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 );
+        else if ( nFanins < 10000 )
+            Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 );
+        else if ( nFanins < 100000 )
+            Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 );
+        else if ( nFanins < 1000000 )
+            Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 );
+        else if ( nFanins < 10000000 )
+            Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 );
+
+        if ( nFanouts < 10 )
+            Vec_IntAddToEntry( vFanouts, nFanouts, 1 );
+        else if ( nFanouts < 100 )
+            Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 );
+        else if ( nFanouts < 1000 )
+            Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 );
+        else if ( nFanouts < 10000 )
+            Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 );
+        else if ( nFanouts < 100000 )
+            Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 );
+        else if ( nFanouts < 1000000 )
+            Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 );
+        else if ( nFanouts < 10000000 )
+            Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 );
+    }
+
+    printf( "The distribution of fanins and fanouts in the network:\n" );
+    printf( "         Number   Nodes with fanin  Nodes with fanout\n" );
+    for ( k = 0; k < nSizeMax; k++ )
+    {
+        if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
+            continue;
+        if ( k < 10 )
+            printf( "%15d : ", k );
+        else
+        {
+            sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); 
+            printf( "%15s : ", Buffer );
+        }
+        if ( vFanins->pArray[k] == 0 )
+            printf( "              " );
+        else
+            printf( "%12d  ", vFanins->pArray[k] );
+        printf( "    " );
+        if ( vFanouts->pArray[k] == 0 )
+            printf( "              " );
+        else
+            printf( "%12d  ", vFanouts->pArray[k] );
+        printf( "\n" );
+    }
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vFanouts );
+
+    printf( "Fanins: Max = %d. Ave = %.2f.  Fanouts: Max = %d. Ave =  %.2f.\n", 
+        nFaninsMax,  1.0*nFaninsAll/Nwk_ManNodeNum(pNtk), 
+        nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk)  );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    Nwk_ManForEachObj( pMan, pObj, i )
+        pObj->MarkA = pObj->MarkB = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkCone_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return;
+    pObj->MarkA = 1;
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        Nwk_ManMarkCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the flow can be pushed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushFlow_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 0;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    // check the case when there is no flow
+    if ( !pObj->MarkB )
+    {
+        if ( pObj->MarkA )
+            return pObj->MarkB = 1;
+        Nwk_ObjForEachFanin( pObj, pNext, i )
+            if ( Nwk_ManPushFlow_rec( pNext ) )
+                return pObj->MarkB = 1;
+    }
+    // check the case when there is no flow or we could not push the flow
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( Nwk_ManPushFlow_rec( pNext ) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes min-cut using max-flow.]
+
+  Description [MarkA means the sink. MarkB means the flow is present.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManComputeCut( Nwk_Man_t * pMan, int nLatches )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj, * pNext;
+    int i, k, RetValue, Counter = 0;
+    // set the sequential parameters
+    pMan->nLatches = nLatches;
+    pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+    pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+    // mark the CIs
+    Nwk_ManForEachCi( pMan, pObj, i )
+        pObj->MarkA = 1;
+    // mark the TFI of the POs
+    Nwk_ManForEachPoSeq( pMan, pObj, i )
+        Nwk_ManMarkCone_rec( pObj );
+    // start flow computation from each LI
+//    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+    {
+        Nwk_ManIncrementTravId( pMan );
+        if ( !Nwk_ManPushFlow_rec( pObj ) )
+            continue;
+//        Nwk_ManIncrementTravId( pMan );
+        Counter++;
+    }
+    // mark the nodes reachable from the LIs
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+    {
+        RetValue = Nwk_ManPushFlow_rec( pObj );
+        assert( RetValue == 0 );
+    }
+    // collect labeled nodes whose all fanins are labeled
+    vNodes = Vec_PtrAlloc( Counter );
+    Nwk_ManForEachObj( pMan, pObj, i )
+    {
+        // skip unlabeled
+        if ( !Nwk_ObjIsTravIdCurrent(pObj) )
+            continue;
+        // visit the fanins
+        Nwk_ObjForEachFanin( pObj, pNext, k )
+            if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                break;
+        if ( k == Nwk_ObjFaninNum(pObj) )
+            Vec_PtrPush( vNodes, pObj );
+    }
+    // unlabel these nodes
+    Nwk_ManIncrementTravId( pMan );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Nwk_ObjSetTravIdCurrent( pObj );
+    // collect labeled nodes having unlabeled fanouts
+    Vec_PtrClear( vNodes );
+    Nwk_ManForEachObj( pMan, pObj, i )
+    {
+        // skip unreachable nodes
+        if ( !Nwk_ObjIsTravIdPrevious(pObj) )
+            continue;
+        if ( Nwk_ObjIsCo(pObj) )
+        {
+            Vec_PtrPush( vNodes, pObj );
+            continue;
+        }
+        Nwk_ObjForEachFanout( pObj, pNext, k )
+            if ( Nwk_ObjIsTravIdCurrent(pNext) )
+                break;
+        if ( k < Nwk_ObjFanoutNum(pObj) )
+            Vec_PtrPush( vNodes, pObj );
+    }
+
+    // clean the marks
+    Nwk_ManCleanMarks( pMan );
+    printf( "Flow = %5d.  Cut = %5d. \n", Counter, Vec_PtrSize(vNodes) );
+    Vec_PtrFree( vNodes );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+