Version abc80411_2

5 files changed, 50 insertions, 21 deletions

diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index b435aade..aaaa287f 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -366,6 +366,45 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew, * pEquivNew = NULL;
+    if ( pObj->pData )
+        return pObj->pData;
+    if ( Aig_ObjIsPi(pObj) )
+        return NULL;
+    if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
+        pEquivNew = Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
+    if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) ) )
+        return NULL;
+    if ( Aig_ObjIsBuf(pObj) )
+        return pObj->pData = Aig_ObjChild0Copy(pObj);
+    if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
+        return NULL;
+    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+    if ( pObj->pHaig )
+        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    if ( pEquivNew )
+    {
+        if ( pNew->pEquivs )
+            pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pEquivNew);        
+        if ( pNew->pReprs )
+            pNew->pReprs[Aig_Regular(pEquivNew)->Id] = Aig_Regular(pObjNew);
+    }
+    return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG manager.]
 
   Description [This duplicator works for AIGs with choices.]
@@ -417,7 +456,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
         }
         else if ( Aig_ObjIsPo(pObj) )
         {
-            Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+            Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
             pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
             Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 52633da7..cec92c11 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1312,19 +1312,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     Vec_PtrForEachEntry( vAigs, pAig, i )
         Aig_ManForEachPi( pAig, pObj, k )
             pObj->pNext = NULL;
-/*
-    // collect the missing outputs (outputs whose driver is not a node)
-    pAig = Vec_PtrEntry( vAigs, 0 );
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pAigTotal);
-    Aig_ManForEachPi( pAig, pObj, i )
-        pAig->pData = Aig_ManPi( pAigTotal, i );
-    Aig_ManForEachPo( pAig, pObj, i )
-        if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
-        {
-            assert( Vec_PtrEntry( vOutsTotal, i ) == NULL );
-            Vec_PtrWriteEntry( vOutsTotal, i, Aig_ObjChild0Copy(pObj) );
-        }
-*/
+
     // add the outputs in the same order
     Vec_PtrForEachEntry( vOutsTotal, pObj, i )
         Aig_ObjCreatePo( pAigTotal, pObj );
@@ -1335,7 +1323,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pAig );
     // reconstruct the network
-    pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry( vAigs, 0 ) );
+    pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
     Aig_ManStop( pTemp );
     // duplicate the timing manager
     pTemp = Vec_PtrEntry( vAigs, 0 );
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 6d6b761c..bc86de20 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -171,7 +171,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
 
     pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
-
+/*
     // balance
     if ( fBalance )
     {
@@ -179,7 +179,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     }
-    
+*/    
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
@@ -243,7 +243,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
 
     pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
-
+/*
     // balance
     if ( fBalance )
     {
@@ -251,8 +251,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     }
-    
-
+*/
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
@@ -388,6 +387,7 @@ clk = clock();
 
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
+    // (it is also important when constructing choices)
     if ( !fConstruct )
     {
         pMan = Vec_PtrPop( vAigs );
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 6b7b1a41..7cb6d6f5 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -276,7 +276,7 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
     {
         if ( pMan1 )  Ntl_ManFree( pMan1 );
         if ( pMan2 )  Ntl_ManFree( pMan2 );
-        printf( "Ntl_ManPrepareSec(): The designs have no latches. Used combinational command \"*cec\".\n" );
+        printf( "Ntl_ManPrepareSec(): The designs have no latches. Use combinational command \"*cec\".\n" );
         return NULL;
     }
     if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 53b25b63..9ae7f0da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16932,6 +16932,8 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
+    if ( pAig == NULL )
+        return 0;
     Fra_FraigSec( pAig, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
     Aig_ManStop( pAig );
     return 0;