Version abc80420_2

14 files changed, 519 insertions, 126 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index fc9d21bc..0ba62bea 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -235,7 +235,7 @@ extern void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2,
 extern Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 /*=== ntlExtract.c ==========================================================*/
 extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p );
+extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
 extern Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
 extern Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
 /*=== ntlInsert.c ==========================================================*/
@@ -247,12 +247,13 @@ extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
 extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
 /*=== ntlMan.c ============================================================*/
-extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
+extern Ntl_Man_t *     Ntl_ManAlloc();
 extern void            Ntl_ManCleanup( Ntl_Man_t * p );
 extern Ntl_Man_t *     Ntl_ManStartFrom( Ntl_Man_t * p );
 extern Ntl_Man_t *     Ntl_ManDup( Ntl_Man_t * p );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
 extern int             Ntl_ManIsComb( Ntl_Man_t * p );
+extern int             Ntl_ManLatchNum( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
@@ -292,6 +293,7 @@ extern Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 extern Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 /*=== ntlWriteBlif.c ==========================================================*/
 extern void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
+extern void            Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
 /*=== ntlUtil.c ==========================================================*/
 extern int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
 extern int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 7cb6d6f5..0cd75cbc 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -238,7 +238,7 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
     // derive AIGs
     *ppMan1 = Ntl_ManCollapseForCec( pMan1 );
     *ppMan2 = Ntl_ManCollapseForCec( pMan2 );
-    // cleanup
+    // cleanup 
     Ntl_ManFree( pMan1 );
     Ntl_ManFree( pMan2 );
 }
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 5a681a7e..f278cba8 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -404,7 +404,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
 {
     Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
@@ -443,6 +443,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+        if ( fSeq && (pObj->LatchId & 3) == 1 )
+            pNet->pCopy = Aig_Not(pNet->pCopy);
         if ( pNet->nVisits )
         {
             printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
@@ -470,7 +472,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
             printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
             return 0;
         }
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
+        if ( fSeq && (pObj->LatchId & 3) == 1 )
+            Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
+        else
+            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     // cleanup the AIG
     Aig_ManCleanup( p->pAig );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 86d92b3c..767ea6e4 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -181,6 +181,35 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
 
 /**Function*************************************************************
 
+  Synopsis    [Resets complemented attributes of the collapsed AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    Aig_Obj_t * pObjCol;
+    int i;
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        if ( (pObj->LatchId & 3) == 1 )
+        {
+            pObjCol = Ntl_ObjFanout0(pObj)->pCopy;
+            assert( pObjCol->fPhase == 0 );
+            pObjCol->fPhase = 1;
+        }
+    }
+}
+ 
+/**Function*************************************************************
+
   Synopsis    [Finalizes the transformation.]
 
   Description []
@@ -242,14 +271,14 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew );
+    pAigCol = Ntl_ManCollapse( pNew, 0 );
 
     // perform fraiging for the given design
     nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
     pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
     Aig_ManStop( pTemp );
 
-    // finalize the transformatoin
+    // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
     Ntl_ManFree( pAux );
     Aig_ManStop( pAig );
@@ -273,20 +302,17 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
 
-    // transform the design
-    Ntl_ManTransformInitValues( p );
-
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew );
+    pAigCol = Ntl_ManCollapse( pNew, 1 );
 
     // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
 
-    // finalize the transformatoin
+    // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
     Ntl_ManFree( pAux );
     Aig_ManStop( pAig );
@@ -310,20 +336,17 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
 
-    // transform the design
-    Ntl_ManTransformInitValues( p );
-
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew );
+    pAigCol = Ntl_ManCollapse( pNew, 1 );
 
     // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
-    // finalize the transformatoin
+    // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
     Ntl_ManFree( pAux );
     Aig_ManStop( pAig );
@@ -347,20 +370,17 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
 
-    // transform the design
-    Ntl_ManTransformInitValues( p );
-
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew );
+    pAigCol = Ntl_ManCollapse( pNew, 1 );
 
     // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Fra_FraigInduction( pAigCol, pPars );
     Aig_ManStop( pTemp );
 
-    // finalize the transformatoin
+    // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
     Ntl_ManFree( pAux );
     Aig_ManStop( pAig );
@@ -459,6 +479,63 @@ void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pA
 
 /**Function*************************************************************
 
+  Synopsis    [Flip complemented edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    Aig_Obj_t * pObjCol, * pFanin;
+    int i, iLatch;
+    pRoot = Ntl_ManRootModel(p);
+    iLatch = 0;
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        if ( (pObj->LatchId & 3) == 1 )
+        {
+            pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
+            assert( pObjCol->fMarkA == 0 );
+            pObjCol->fMarkA = 1;
+        }
+        iLatch++;
+    }
+    // flip pointers to the complemented edges
+    Aig_ManForEachObj( pAigCol, pObjCol, i )
+    {
+        pFanin = Aig_ObjFanin0(pObjCol);
+        if ( pFanin && pFanin->fMarkA )
+            pObjCol->pFanin0 = Aig_Not(pObjCol->pFanin0);
+        pFanin = Aig_ObjFanin1(pObjCol);
+        if ( pFanin && pFanin->fMarkA )
+            pObjCol->pFanin1 = Aig_Not(pObjCol->pFanin1);
+    }
+    // flip complemented latch derivers and undo the marks
+    iLatch = 0;
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        if ( (pObj->LatchId & 3) == 1 )
+        {
+            // flip the latch input
+            pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch );
+            pObjCol->pFanin0 = Aig_Not(pObjCol->pFanin0);
+            // unmark the latch output
+            pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
+            assert( pObjCol->fMarkA == 1 );
+            pObjCol->fMarkA = 0;
+        }
+        iLatch++;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns AIG with WB after sequential SAT sweeping.]
 
   Description []
@@ -473,13 +550,14 @@ 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 = Ntl_ManCollapse( p, 1 );
     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_ManFlipEdges( p, pAigRed );
     Ntl_ManTransferCopy( p );
     pNew = Ntl_ManInsertAig( p, pAigRed );
     // attach the white-boxes
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index b4b63905..e80e02c6 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
+Ntl_Man_t * Ntl_ManAlloc()
 {
     Ntl_Man_t * p;
     // start the manager
@@ -53,9 +53,6 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
-    // same the names
-    p->pName = Ntl_ManStoreFileName( p, pFileName );
-    p->pSpec = Ntl_ManStoreName( p, pFileName );
     return p;
 }
 
@@ -106,7 +103,9 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
     Ntl_Obj_t * pBox;
     Ntl_Net_t * pNet;
     int i, k;
-    pNew = Ntl_ManAlloc( pOld->pSpec );
+    pNew = Ntl_ManAlloc();
+    pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName );
+    pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName );
     Vec_PtrForEachEntry( pOld->vModels, pModel, i )
         if ( i == 0 )
         {
@@ -146,7 +145,9 @@ Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * pOld )
     Ntl_Obj_t * pBox;
     Ntl_Net_t * pNet;
     int i, k;
-    pNew = Ntl_ManAlloc( pOld->pSpec );
+    pNew = Ntl_ManAlloc();
+    pNew->pName = Ntl_ManStoreFileName( pNew, pOld->pName );
+    pNew->pSpec = Ntl_ManStoreName( pNew, pOld->pName );
     Vec_PtrForEachEntry( pOld->vModels, pModel, i )
         pModel->pCopy = Ntl_ModelDup( pNew, pModel );
     Vec_PtrForEachEntry( pOld->vModels, pModel, i )
@@ -213,6 +214,22 @@ int Ntl_ManIsComb( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManLatchNum( Ntl_Man_t * p )          
+{ 
+    return Ntl_ModelLatchNum(Ntl_ManRootModel(p)); 
+} 
+
+/**Function*************************************************************
+
   Synopsis    [Find the model with the given name.]
 
   Description []
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 23bb6d76..13050047 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -131,6 +131,8 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
     }
     // set the design name
     p->pDesign = Ntl_ManAlloc( pFileName );
+    p->pDesign->pName = Ntl_ManStoreFileName( p->pDesign, pFileName );
+    p->pDesign->pSpec = Ntl_ManStoreName( p->pDesign, pFileName );
     // prepare the file for parsing
     Ioa_ReadReadPreparse( p );
     // parse interfaces of each network
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 24fa1370..ed45fcaf 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -141,7 +141,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the network into the BLIF file.]
+  Synopsis    [Writes the netlist into the BLIF file.]
 
   Description []
                
@@ -170,6 +170,25 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
     fclose( pFile );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the logic network into the BLIF file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName )
+{
+    Ntl_Man_t * pNew;
+    pNew = Ntl_ManInsertNtk( p, pNtk );
+    Ioa_WriteBlif( pNew, pFileName );
+    Ntl_ManFree( pNew );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index d0a871cf..c36f3498 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -250,7 +250,7 @@ extern Vec_Ptr_t *     Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches,
 /*=== nwkMan.c ============================================================*/
 extern Nwk_Man_t *     Nwk_ManAlloc();
 extern void            Nwk_ManFree( Nwk_Man_t * p );
-extern void            Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib );
+extern void            Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
 /*=== nwkMap.c ============================================================*/
 extern Nwk_Man_t *     Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
 /*=== nwkObj.c ============================================================*/
diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c
index 1b701e9e..89bf60ee 100644
--- a/src/aig/nwk/nwkFanio.c
+++ b/src/aig/nwk/nwkFanio.c
@@ -125,58 +125,6 @@ static inline int Nwk_ObjReallocIsNeeded( Nwk_Obj_t * pObj )
 {  
     return pObj->nFanins + pObj->nFanouts == pObj->nFanioAlloc;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Reallocates the object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Nwk_Obj_t * Nwk_ManReallocNode_old( Nwk_Obj_t * pObj )
-{  
-    Nwk_Obj_t * pObjNew, * pTemp;
-    int i, iNum;
-    assert( Nwk_ObjReallocIsNeeded(pObj) );
-    pObjNew = (Nwk_Obj_t *)Aig_MmFlexEntryFetch( pObj->pMan->pMemObjs, sizeof(Nwk_Obj_t) + 2 * pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) );
-    memmove( pObjNew, pObj, sizeof(Nwk_Obj_t) + pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) );
-    pObjNew->nFanioAlloc = 2 * pObj->nFanioAlloc;
-    // update the fanouts' fanins
-    Nwk_ObjForEachFanout( pObj, pTemp, i )
-    {
-        iNum = Nwk_ObjFindFanin( pTemp, pObj );
-        if ( iNum == -1 )
-            printf( "Nwk_ManReallocNode(): Error! Fanin cannot be found.\n" );
-        pTemp->pFanio[iNum] = pObjNew;
-    }
-    // update the fanins' fanouts
-    Nwk_ObjForEachFanin( pObj, pTemp, i )
-    {
-        iNum = Nwk_ObjFindFanout( pTemp, pObj );
-        if ( iNum == -1 )
-            printf( "Nwk_ManReallocNode(): Error! Fanout cannot be found.\n" );
-        pTemp->pFanio[pTemp->nFanins+iNum] = pObjNew;
-    }
-    memset( pObj, 0, sizeof(Nwk_Obj_t) + pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) );
-    assert( Nwk_ManObj(pObjNew->pMan, pObjNew->Id) == pObj );
-    Vec_PtrWriteEntry( pObjNew->pMan->vObjs, pObjNew->Id, pObjNew );
-    if ( Nwk_ObjIsCi(pObjNew) )
-    {
-        assert( Nwk_ManCi(pObjNew->pMan, pObjNew->PioId) == pObj );
-        Vec_PtrWriteEntry( pObjNew->pMan->vCis, pObjNew->PioId, pObjNew );
-    }
-    if ( Nwk_ObjIsCo(pObjNew) )
-    {
-        assert( Nwk_ManCo(pObjNew->pMan, pObjNew->PioId) == pObj );
-        Vec_PtrWriteEntry( pObjNew->pMan->vCos, pObjNew->PioId, pObjNew );
-    }
-    pObjNew->pMan->nRealloced++;
-    return pObjNew;
-}
  
 /**Function*************************************************************
 
@@ -200,7 +148,6 @@ static Nwk_Obj_t * Nwk_ManReallocNode( Nwk_Obj_t * pObj )
     return NULL;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Creates fanout/fanin relationship between the nodes.]
diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c
index b245628a..3a7e6df6 100644
--- a/src/aig/nwk/nwkFlow.c
+++ b/src/aig/nwk/nwkFlow.c
@@ -524,7 +524,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
         pObj->MarkA = 1;
     Nwk_ManForEachPoSeq( pMan, pObj, i )
         Nwk_ManMarkTfiCone_rec( pObj );
-    Nwk_ManForEachObj( pMan, pObj, i )
+    Nwk_ManForEachNode( pMan, pObj, i )
         if ( Nwk_ObjFaninNum(pObj) == 0 )
             pObj->MarkA = 1;
     // start flow computation from each LI driver
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index a1f20a8e..aeebac3f 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -104,6 +104,92 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
 
 /**Function*************************************************************
 
+  Synopsis    [If the network is best, saves it in "best.blif" and returns 1.]
+
+  Description [If the networks are incomparable, saves the new network, 
+  returns its parameters in the internal parameter structure, and returns 1.
+  If the new network is not a logic network, quits without saving and returns 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
+{
+    extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName );
+    static struct ParStruct {
+        char * pName;  // name of the best saved network
+        int    Depth;  // depth of the best saved network
+        int    Flops;  // flops in the best saved network 
+        int    Nodes;  // nodes in the best saved network
+        int    nPis;   // the number of primary inputs
+        int    nPos;   // the number of primary outputs
+    } ParsNew, ParsBest = { 0 };
+    // free storage for the name
+    if ( pNtk == NULL )
+    {
+        FREE( ParsBest.pName );
+        return 0;
+    }
+    // get the parameters
+    ParsNew.Depth = Nwk_ManLevel( pNtk );
+    ParsNew.Flops = Nwk_ManLatchNum( pNtk );
+    ParsNew.Nodes = Nwk_ManNodeNum( pNtk );
+    ParsNew.nPis  = Nwk_ManPiNum( pNtk );
+    ParsNew.nPos  = Nwk_ManPoNum( pNtk );
+    // reset the parameters if the network has the same name
+    if ( ParsBest.pName == NULL || 
+         strcmp(ParsBest.pName, pNtk->pName) ||
+         ParsBest.Depth >  ParsNew.Depth || 
+         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops || 
+         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes )
+    {
+        FREE( ParsBest.pName );
+        ParsBest.pName = Aig_UtilStrsav( pNtk->pName );
+        ParsBest.Depth = ParsNew.Depth; 
+        ParsBest.Flops = ParsNew.Flops; 
+        ParsBest.Nodes = ParsNew.Nodes; 
+        ParsBest.nPis  = ParsNew.nPis; 
+        ParsBest.nPos  = ParsNew.nPos;
+        // writ the network
+        Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" );
+        return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Nwk_FileNameGeneric( char * FileName )
+{
+    char * pDot;
+    char * pUnd;
+    char * pRes;
+    // find the generic name of the file
+    pRes = Aig_UtilStrsav( FileName );
+    // find the pointer to the "." symbol in the file name
+//  pUnd = strstr( FileName, "_" );
+    pUnd = NULL;
+    pDot = strstr( FileName, "." );
+    if ( pUnd )
+        pRes[pUnd - FileName] = 0;
+    else if ( pDot )
+        pRes[pDot - FileName] = 0;
+    return pRes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints stats of the manager.]
 
   Description []
@@ -113,24 +199,37 @@ void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
   SeeAlso     []
 
 ***********************************************************************/
-void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
+void Nwk_ManPrintStats( Nwk_Man_t * pNtk, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl )
 {
-    p->pLutLib = pLutLib;
-    printf( "%-15s : ",      p->pName );
-    printf( "pi = %5d  ",    Nwk_ManPiNum(p) );
-    printf( "po = %5d  ",    Nwk_ManPoNum(p) );
-    printf( "ci = %5d  ",    Nwk_ManCiNum(p) );
-    printf( "co = %5d  ",    Nwk_ManCoNum(p) );
-    printf( "lat = %5d  ",   Nwk_ManLatchNum(p) );
-    printf( "node = %5d  ",  Nwk_ManNodeNum(p) );
-    printf( "edge = %5d  ",  Nwk_ManGetTotalFanins(p) );
-    printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(p) );
-    printf( "lev = %3d  ",   Nwk_ManLevel(p) );
-//    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(p) );
-    printf( "delay = %5.2f   ", Nwk_ManDelayTraceLut(p) );
-    Nwk_ManPrintLutSizes( p, pLutLib );
+    extern int Ntl_ManLatchNum( void * p );
+    extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName );
+    if ( fSaveBest )
+        Nwk_ManCompareAndSaveBest( pNtk, pNtl );
+    if ( fDumpResult )
+    {
+        char Buffer[1000] = {0};
+        char * pNameGen = pNtk->pSpec? Nwk_FileNameGeneric( pNtk->pSpec ) : "nameless_";
+        sprintf( Buffer, "%s_dump.blif", pNameGen );
+        Ioa_WriteBlifLogic( pNtk, pNtl, Buffer );
+        if ( pNtk->pSpec ) free( pNameGen );
+    }
+
+    pNtk->pLutLib = pLutLib;
+    printf( "%-15s : ",      pNtk->pName );
+    printf( "pi = %5d  ",    Nwk_ManPiNum(pNtk) );
+    printf( "po = %5d  ",    Nwk_ManPoNum(pNtk) );
+    printf( "ci = %5d  ",    Nwk_ManCiNum(pNtk) );
+    printf( "co = %5d  ",    Nwk_ManCoNum(pNtk) );
+    printf( "lat = %5d  ",   Ntl_ManLatchNum(pNtl) );
+    printf( "node = %5d  ",  Nwk_ManNodeNum(pNtk) );
+    printf( "edge = %5d  ",  Nwk_ManGetTotalFanins(pNtk) );
+    printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(pNtk) );
+    printf( "lev = %3d  ",   Nwk_ManLevel(pNtk) );
+//    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(pNtk) );
+    printf( "delay = %5.2f   ", Nwk_ManDelayTraceLut(pNtk) );
+    Nwk_ManPrintLutSizes( pNtk, pLutLib );
     printf( "\n" );
-//    Nwk_ManDelayTracePrint( p, pLutLib );
+//    Nwk_ManDelayTracePrint( pNtk, pLutLib );
     fflush( stdout );
 }
 
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index effffcf7..45d56eb5 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -267,6 +267,9 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
     pNtk = Nwk_ManAlloc();
     pNtk->pName = Aig_UtilStrsav( p->pName );
     pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
+//    pNtk->nLatches = Aig_ManRegNum(p);
+//    pNtk->nTruePis = Nwk_ManCiNum(pNtk) - pNtk->nLatches;
+//    pNtk->nTruePos = Nwk_ManCoNum(pNtk) - pNtk->nLatches;
     Aig_ManForEachObj( p, pObj, i )
     {
         pIfObj = Vec_PtrEntry( vAigToIf, i );
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 9ab24467..e8123dae 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -427,7 +427,7 @@ int Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk )
     int i;
     Nwk_ManForEachObj( pNtk, pObj, i )
     {
-        if ( Nwk_ObjIsPi(pObj) && Nwk_ObjFanoutNum(pObj) == 0 )
+        if ( Nwk_ObjIsCi(pObj) && Nwk_ObjFanoutNum(pObj) == 0 )
             continue;
         tArrival = Nwk_NodeComputeArrival( pObj, 1 );
         tRequired = Nwk_NodeComputeRequired( pObj, 1 );
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 92d39ab6..3adb76c6 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "saig.h"
+#include "satSolver.h"
+#include "cnf.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -54,7 +56,7 @@ void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Marks the TFI cones with the current traversal ID.]
+  Synopsis    [Counts the number of nodes to get registers after retiming.]
 
   Description []
                
@@ -63,18 +65,44 @@ void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManMarkCones( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
 {
-    Aig_Obj_t * pObj;
-    int i;
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj, * pFanin;
+    int i, RetValue;
+    // mark the cones
     Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( vCut, pObj, i )
         Saig_ManMarkCone_rec( p, pObj );
+    // collect the new cut
+    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;
+        }
+    }
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->fMarkA = 0;
+    RetValue = Vec_PtrSize( vNodes );
+    Vec_PtrFree( vNodes );
+    return RetValue;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of nodes to get registers after retiming.]
+  Synopsis    [Computes the new cut after excluding the nodes in the set.]
 
   Description []
                
@@ -83,12 +111,18 @@ void Saig_ManMarkCones( Aig_Man_t * p, Vec_Ptr_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
+Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t * vToExclude )
 {
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj, * pFanin;
-    int i, RetValue;
-    Saig_ManMarkCones( p, vCut );
+    int i;
+    // mark the cones
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        Saig_ManMarkCone_rec( p, pObj );
+    Vec_PtrForEachEntry( vToExclude, pObj, i )
+        Saig_ManMarkCone_rec( p, pObj );
+    // collect the new cut
     vNodes = Vec_PtrAlloc( 1000 );
     Aig_ManForEachObj( p, pObj, i )
     {
@@ -107,16 +141,14 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
             pFanin->fMarkA = 1;
         }
     }
-    RetValue = Vec_PtrSize( vNodes );
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->fMarkA = 0;
-    Vec_PtrFree( vNodes );
-    return RetValue;
+    return vNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+  Synopsis    [Duplicates the AIG recursively.]
 
   Description []
                
@@ -125,13 +157,13 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManRetimeDupForward_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+void Saig_ManRetimeDup_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) );
+    Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
+    Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin1(pObj) );
     pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
 }
 
@@ -168,9 +200,9 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
     // create the registers
     Vec_PtrForEachEntry( vCut, pObj, i )
         pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), pObj->fPhase );
-    // duplicate the logic above the cut
+    // duplicate logic above the cut
     Aig_ManForEachPo( p, pObj, i )
-        Saig_ManRetimeDupForward_rec( pNew, Aig_ObjFanin0(pObj) );
+        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
     // create the true POs
     Saig_ManForEachPo( p, pObj, i )
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
@@ -182,12 +214,12 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
         pObjLo->pData = pObjLi->pData;
     // erase the data values on the internal nodes of the cut
     Vec_PtrForEachEntry( vCut, pObj, i )
-        if ( !Aig_ObjIsPi(pObj) )
+        if ( Aig_ObjIsNode(pObj) )
             pObj->pData = NULL;
-    // duplicate the logic below the cut
+    // duplicate logic below the cut
     Vec_PtrForEachEntry( vCut, pObj, i )
     {
-        Saig_ManRetimeDupForward_rec( pNew, pObj );
+        Saig_ManRetimeDup_rec( pNew, pObj );
         Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) );
     }
     return pNew;
@@ -195,7 +227,7 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+  Synopsis    [Derives AIG for the initial state computation.]
 
   Description []
                
@@ -204,10 +236,199 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut )
+Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )
 {
     Aig_Man_t * pNew;
-    pNew = Aig_ManDup( p );
+    Aig_Obj_t * pObj;
+    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) );
+    // create the true PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    // create the registers
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // duplicate logic above the cut and create POs
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the initial state after backward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p )
+{
+    int nConfLimit = 1000000;
+    Vec_Int_t * vCiIds, * vInit = NULL;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int i, RetValue, * pAssumps, * pModel;
+    // solve the SAT problem
+    pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    pAssumps = ALLOC( int, Aig_ManPoNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+        pAssumps[i] = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
+    RetValue = sat_solver_solve( pSat, pAssumps, pAssumps+Aig_ManPoNum(p), (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    free( pAssumps );
+    if ( RetValue == l_True )
+    {
+        // accumulate SAT variables of the CIs
+        vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+        Aig_ManForEachPi( p, pObj, i )
+            Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
+        // create the model
+        pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+        vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) );
+        Vec_IntFree( vCiIds );
+    }
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    return vInit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of bad registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes = NULL;
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Diffs;
+    assert( Saig_ManRegNum(p) > 0 );
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( !Aig_ObjFaninC0(pObj) )
+            pFanin->fMarkA = 1;
+        else
+            pFanin->fMarkB = 1;
+    }
+    Diffs = 0;
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        Diffs += pFanin->fMarkA && pFanin->fMarkB;
+    }
+    if ( Diffs > 0 )
+        vNodes = Vec_PtrAlloc( Diffs );
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( vNodes && pFanin->fMarkA && pFanin->fMarkB )
+            Vec_PtrPush( vNodes, pFanin );
+        pFanin->fMarkA = pFanin->fMarkB = 0;
+    }
+    return vNodes;
+}
+
+/**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 * vCutInit )
+{
+    Vec_Ptr_t * vToExclude, * vCut;
+    Vec_Int_t * vInit = NULL;
+    Aig_Man_t * pNew, * pInit;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+    // check if there are bad registers
+    vToExclude = Saig_ManGetRegistersToExclude( p );
+    if ( vToExclude )
+    {
+        vCut = Saig_ManRetimeExtendCut( p, vCutInit, vToExclude );
+        printf( "Bad registers = %d. Extended cut from %d to %d nodes.\n", 
+            Vec_PtrSize(vToExclude), Vec_PtrSize(vCutInit), Vec_PtrSize(vCut) );
+        Vec_PtrFree( vToExclude );
+    }
+    else
+        vCut = Vec_PtrDup( vCutInit );
+    // mark the cones under the cut
+//    assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
+    // count if there are registers to disable
+    // derive the initial state
+    pInit = Saig_ManRetimeDupInitState( p, vCut );
+    vInit = Saig_ManRetimeFindInitState( pInit );
+    if ( vInit == NULL )
+        printf( "Initial state computation has failed.\n" );
+    Aig_ManStop( pInit );
+    // 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), vInit?Vec_IntEntry(vInit,i):0 );
+    // duplicate logic above the cut and remember values
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
+        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_ObjIsNode(pObj) )
+            pObj->pData = NULL;
+    // replicate the data on the primary inputs
+    Saig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ManPi( pNew, i );
+    // duplicate logic below the cut
+    Saig_ManForEachPo( p, pObj, i )
+    {
+        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Vec_PtrForEachEntry( vCut, pObj, i )
+    {
+        Saig_ManRetimeDup_rec( pNew, pObj );
+        Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );
+    }
+    if ( vInit )
+        Vec_IntFree( vInit );
+    Vec_PtrFree( vCut );
     return pNew;
 }