Version abc80420

16 files changed, 1874 insertions, 5 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8593fd76..74e3de31 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -66,7 +66,10 @@ typedef enum {
 // the AIG node
 struct Aig_Obj_t_  // 8 words
 {
-    Aig_Obj_t *      pNext;          // strashing table
+    union {                         
+        Aig_Obj_t *  pNext;          // strashing table
+        int          PioNum;         // the number of PI/PO
+    };
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
     Aig_Obj_t *      pHaig;          // pointer to the HAIG node
@@ -551,6 +554,7 @@ extern void            Aig_ManReprStop( Aig_Man_t * p );
 extern void            Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
+extern Aig_Man_t *     Aig_ManDupReprBasic( Aig_Man_t * p );
 extern int             Aig_ManCountReprs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern int             Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
@@ -563,6 +567,7 @@ extern Aig_Man_t *     Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax );
 /*=== aigScl.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
 extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
+extern int             Aig_ManSeqCleanupBasic( Aig_Man_t * p );
 extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
 extern void            Aig_ManComputeSccs( Aig_Man_t * p ); 
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 3829ee22..e7623739 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -50,6 +50,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nRegs = p->nRegs;
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = p->nTruePos;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 88cdbf17..54ab0a33 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -302,6 +302,34 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates AIG with representatives without removing registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupReprBasic( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( p->pReprs != NULL );
+    // reconstruct AIG with representatives
+    pNew = Aig_ManDupRepr( p, 0 );
+    // perfrom sequential cleanup but do not remove registers
+    Aig_ManSeqCleanupBasic( pNew );
+    // remove pointers to the dead nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
+            pObj->pData = NULL;
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfer representatives and return the number of critical fanouts.]
 
   Description []
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 34b3482d..00a8159e 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -240,6 +240,60 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
 
   Synopsis    [Returns the number of dangling nodes removed.]
 
+  Description [This cleanup procedure is different in that 
+  it removes logic but does not remove the dangling latches.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSeqCleanupBasic( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+//    assert( Aig_ManBufNum(p) == 0 );
+
+    // mark the PIs
+    Aig_ManIncrementTravId( p );
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+
+    // prepare to collect nodes reachable from POs
+    vNodes = Vec_PtrAlloc( 100 );
+    Aig_ManForEachPoSeq( p, pObj, i )
+        Vec_PtrPush( vNodes, pObj );
+
+    // remember latch inputs in latch outputs
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = pObjLi;
+    // mark the nodes reachable from these nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Aig_ManSeqCleanup_rec( p, pObj, vNodes );
+    assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
+    // clean latch output pointers
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = NULL;
+
+    // if some latches are removed, update PIs/POs
+    if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
+    {
+        // add constant drivers to the dangling latches
+        Aig_ManForEachPo( p, pObj, i )
+            if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
+                Aig_ObjPatchFanin0( p, pObj, Aig_ManConst0(p) );
+    }
+    Vec_PtrFree( vNodes );
+    // remove dangling nodes
+    return Aig_ManCleanup( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
   Description []
                
   SideEffects []
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 2dde907c..b29fa946 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -580,6 +580,10 @@ clk2 = clock();
 //        Fra_ImpRecordInManager( p, pManAigNew );
     // cleanup the new manager
     Aig_ManSeqCleanup( pManAigNew );
+    // remove pointers to the dead nodes
+//    Aig_ManForEachObj( pManAig, pObj, i )
+//        if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
+//            pObj->pData = NULL;
 //    Aig_ManCountMergeRegs( pManAigNew );
 p->timeTrav += clock() - clk2;
 p->timeTotal = clock() - clk;
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 4f00cbda..fc9d21bc 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -120,6 +120,7 @@ struct Ntl_Net_t_
 {
     Ntl_Net_t *        pNext;          // next net in the hash table
     void *             pCopy;          // the copy of this object
+    void *             pCopy2;         // the copy of this object
     Ntl_Obj_t *        pDriver;        // driver of the net
     char               nVisits;        // the number of times the net is visited
     char               fMark;          // temporary mark
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 18ca1a53..5a681a7e 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -233,7 +233,10 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel( p );
     // clear net visited flags
     Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
         pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // collect primary inputs
     Ntl_ModelForEachPi( pRoot, pObj, i )
     {
@@ -417,7 +420,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel( p );
     // clear net visited flags
     Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
         pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // collect primary inputs
     Ntl_ModelForEachPi( pRoot, pObj, i )
     {
@@ -486,9 +492,17 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
 Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
 {
     Aig_Man_t * pAig;
+    Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i;
+    // clear net visited flags
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // create the manager
     p->pAig = Aig_ManStart( 10000 );
     p->pAig->pName = Aig_UtilStrsav( p->pName );
@@ -557,6 +571,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
     Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
 
     /////////////////////////////////////////////////////
+    // clear net visited flags
+    pRoot1 = Ntl_ManRootModel(p1);
+    Ntl_ModelForEachNet( pRoot1, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // primary inputs
     Ntl_ManForEachCiNet( p1, pObj, i )
     {
@@ -571,7 +592,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
         pNet->nVisits = 2;
     }
     // latch outputs
-    pRoot1 = Ntl_ManRootModel(p1);
     Ntl_ModelForEachLatch( pRoot1, pObj, i )
     {
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
@@ -614,6 +634,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
     }
 
     /////////////////////////////////////////////////////
+    // clear net visited flags
+    pRoot2 = Ntl_ManRootModel(p2);
+    Ntl_ModelForEachNet( pRoot2, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
     // primary inputs
     Ntl_ManForEachCiNet( p2, pObj, i )
     {
@@ -628,7 +655,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
         pNet->nVisits = 2;
     }
     // latch outputs
-    pRoot2 = Ntl_ManRootModel(p2);
     Ntl_ModelForEachLatch( pRoot2, pObj, i )
     {
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 63725558..86d92b3c 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -369,6 +369,128 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the copy field into the second copy field.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManTransferCopy( Ntl_Man_t * p )
+{
+    Ntl_Net_t * pNet;
+    Ntl_Mod_t * pRoot;
+    int i;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        pNet->pCopy2 = pNet->pCopy;
+        pNet->pCopy = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reattaches one white-box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManAttachWhiteBox( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, Ntl_Obj_t * pBox )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reattaches white-boxes after reducing the netlist.]
+
+  Description [The following parameters are given:
+  Original netlist (p) whose nets point to the nodes of collapsed AIG.
+  Collapsed AIG (pAigCol) whose objects point to those of reduced AIG.
+  Reduced AIG (pAigRed) whose objects point to the nets of the new netlist.
+  The new netlist is changed by this procedure to have those white-boxes
+  from the original AIG (p) those outputs are preserved after reduction.
+  Note that if outputs are preserved, the inputs are also preserved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, int fVerbose )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pBox;
+    Ntl_Net_t * pNet;
+    int i, k, Counter = 0;
+    // go through the white-boxes and check if they are preserved
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachBox( pRoot, pBox, i )
+    {
+        Ntl_ObjForEachFanout( pBox, pNet, k )
+        {
+            // skip dangling outputs of the box
+            if ( pNet->pCopy == NULL )
+                continue;
+            // skip the outputs that are not preserved after merging equivalence
+            if ( Aig_Regular(pNet->pCopy2)->pData == NULL )
+                continue;
+            break;
+        }
+        if ( k == Ntl_ObjFanoutNum(pBox) )
+            continue;
+        // the box is preserved
+        Ntl_ManAttachWhiteBox( p, pAigCol, pAigRed, pNew, pBox );
+        Counter++;
+    }
+    if ( fVerbose )
+        printf( "Attached %d boxed (out of %d).\n", Counter, Ntl_ModelBoxNum(pRoot) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after sequential SAT sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
+{
+    Ntl_Man_t * pNew;
+    Aig_Man_t * pAigRed, * pAigCol;
+    // collapse the AIG
+    pAigCol = Ntl_ManCollapse( p );
+    pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+    // transform the collapsed AIG
+    pAigRed = Fra_FraigInduction( pAigCol, pPars );
+    Aig_ManStop( pAigRed );
+    pAigRed = Aig_ManDupReprBasic( pAigCol );
+    // insert the result back
+    Ntl_ManTransferCopy( p );
+    pNew = Ntl_ManInsertAig( p, pAigRed );
+    // attach the white-boxes
+    Ntl_ManAttachWhiteBoxes( p, pAigCol, pAigRed, pNew, pPars->fVerbose );
+    Ntl_ManSweep( pNew, pPars->fVerbose );
+    // cleanup
+    Aig_ManStop( pAigRed );
+    Aig_ManStop( pAigCol );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
new file mode 100644
index 00000000..3902ce70
--- /dev/null
+++ b/src/aig/saig/module.make
@@ -0,0 +1,3 @@
+SRC +=    src/aig/saig/saig_.c \
+    src/aig/saig/saigPhase.c \
+    src/aig/saig/saigRetMin.c
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
new file mode 100644
index 00000000..92d39ab6
--- /dev/null
+++ b/src/aig/saig/saigRetMin.c
@@ -0,0 +1,262 @@
+/**CFile****************************************************************
+
+  FileName    [saigRetMin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Min-area retiming for the AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigRetMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone with the current traversal ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj == NULL )
+        return;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) );
+    Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cones with the current traversal ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManMarkCones( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Saig_ManMarkCone_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of nodes to get registers after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj, * pFanin;
+    int i, RetValue;
+    Saig_ManMarkCones( p, vCut );
+    vNodes = Vec_PtrAlloc( 1000 );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+            continue;
+        pFanin = Aig_ObjFanin0( pObj );
+        if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
+        {
+            Vec_PtrPush( vNodes, pFanin );
+            pFanin->fMarkA = 1;
+        }
+        pFanin = Aig_ObjFanin1( pObj );
+        if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
+        {
+            Vec_PtrPush( vNodes, pFanin );
+            pFanin->fMarkA = 1;
+        }
+    }
+    RetValue = Vec_PtrSize( vNodes );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->fMarkA = 0;
+    Vec_PtrFree( vNodes );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManRetimeDupForward_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) );
+    Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+    // mark the cones under the cut
+//    assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = Vec_PtrSize(vCut);
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = p->nTruePos;
+    // create the true PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Saig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // create the registers
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), pObj->fPhase );
+    // duplicate the logic above the cut
+    Aig_ManForEachPo( p, pObj, i )
+        Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) );
+    // create the true POs
+    Saig_ManForEachPo( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // remember value in LI
+    Saig_ManForEachLi( p, pObj, i )
+        pObj->pData = Aig_ObjChild0Copy(pObj);
+    // transfer values from the LIs to the LOs
+    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+        pObjLo->pData = pObjLi->pData;
+    // erase the data values on the internal nodes of the cut
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        if ( !Aig_ObjIsPi(pObj) )
+            pObj->pData = NULL;
+    // duplicate the logic below the cut
+    Vec_PtrForEachEntry( vCut, pObj, i )
+    {
+        Saig_ManRetimeDupForward_rec( pNew, pObj );
+        Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut )
+{
+    Aig_Man_t * pNew;
+    pNew = Aig_ManDup( p );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs min-area retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fVerbose )
+{
+    Vec_Ptr_t * vCut;
+    Aig_Man_t * pNew, * pTemp;
+    pNew = Aig_ManDup( p );
+    // perform several iterations of forward retiming
+    if ( !fBackwardOnly )
+    while ( 1 )
+    {
+        vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
+        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
+        {
+            Vec_PtrFree( vCut );
+            break;
+        }
+        pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
+        Aig_ManStop( pTemp );
+        Vec_PtrFree( vCut );
+    }
+    // perform one iteration of backward retiming
+    if ( !fForwardOnly )
+    {
+        vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
+        if ( Vec_PtrSize(vCut) < Aig_ManRegNum(pNew) )
+        {
+            pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut );
+            Aig_ManStop( pTemp );
+        }
+        Vec_PtrFree( vCut );
+    }
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+