Version abc80403

6 files changed, 39 insertions, 11 deletions

diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index aead8c9e..779337bf 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -166,7 +166,7 @@ PRT( "Time", clock() - clk );
 
     // duplicate the AIG
 clk = clock();
-//    pAig = Aig_ManDup( pTemp = pAig );
+//    pAig = Aig_ManDupDfs( pTemp = pAig );
     pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose )
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 444157f0..80799e3e 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -369,7 +369,7 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     Aig_Man_t * pManAigNew;
     int clk;
     if ( Aig_ManNodeNum(pManAig) == 0 )
-        return Aig_ManDup(pManAig, 1);
+        return Aig_ManDupOrdered(pManAig);
 clk = clock();
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 8b9e863e..03d03ea1 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -343,7 +343,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
         pParams->nIters = 0;
-        return Aig_ManDup(pManAig, 1);
+        return Aig_ManDupOrdered(pManAig);
     }
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( pParams->nFramesK > 0 );
@@ -563,7 +563,7 @@ clk2 = clock();
         Aig_Man_t * pNew;
         char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
         printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
-        pManAigNew = Aig_ManDup( pManAig, 1 );
+        pManAigNew = Aig_ManDupOrdered( pManAig );
         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
         Ioa_WriteAiger( pNew, pFileName, 0, 1 );
         Aig_ManStop( pNew );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 9149aca4..145bafae 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -251,6 +251,31 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew;
+    if ( pObj->pData )
+        return pObj->pData;
+    Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    if ( Aig_ObjIsBuf(pObj) )
+        return pObj->pData = Aig_ObjChild0Copy(pObj);
+    Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Give the AIG and classes, reduces AIG for partitioning.]
 
   Description [Ignores registers that are not in the classes. 
@@ -290,7 +315,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         {
             assert( Aig_ObjIsPi(ppClass[c]) );
             pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
-            pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+            pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
             pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
         }
         Aig_ObjCreatePo( pNew, pMiter );
@@ -300,7 +325,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
     {
         assert( Aig_ObjIsPi(pObj) );
         pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
-        pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+        pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
         Aig_ObjCreatePo( pNew, pMiter );
     }
     return pNew;
@@ -514,7 +539,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
-        return Aig_ManDup(pAig, 1);
+        return Aig_ManDupOrdered(pAig);
     }
     assert( Aig_ManRegNum(pAig) > 0 );
 
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 720260a5..da7c37a3 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -298,6 +298,7 @@ void Fra_ManPrint( Fra_Man_t * p )
     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
     if ( p->nSpeculs )
     printf( "Speculations = %d.\n", p->nSpeculs );
+    fflush( stdout );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index bbad2a6e..83a551b8 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -52,7 +52,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
     pPars->fLatchCorr  = fLatchCorr;
     pPars->fVerbose = fVeryVerbose;
 
-    pNew = Aig_ManDup( p, 1 );
+    pNew = Aig_ManDupOrdered( p );
+//    pNew = Aig_ManDupDfs( p );
     if ( fVerbose )
     {
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
@@ -91,7 +92,8 @@ PRT( "Time", clock() - clk );
 clk = clock();
     if ( pNew->nRegs )
     {
-    pNew = Aig_ManDup( pTemp = pNew, 1 );
+    pNew = Aig_ManDupOrdered( pTemp = pNew );
+//    pNew = Aig_ManDupDfs( pTemp = pNew );
     Aig_ManStop( pTemp );
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
     p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
@@ -147,7 +149,7 @@ PRT( "Time", clock() - clk );
 
         // perform rewriting
 clk = clock();
-        pNew = Aig_ManDup( pTemp = pNew, 1 );
+        pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
         pNew = Dar_ManRewriteDefault( pTemp = pNew );
         Aig_ManStop( pTemp );
@@ -165,7 +167,7 @@ PRT( "Time", clock() - clk );
 clk = clock();
         pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
         Aig_ManStop( pTemp );
-        pNew = Aig_ManDup( pTemp = pNew, 1 );
+        pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
         if ( fVerbose )
         {