Version abc80411

3 files changed, 17 insertions, 7 deletions

diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 9c3666ab..b3d099c9 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -364,7 +364,7 @@ Aig_Obj_t * Ntl_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
 Aig_Obj_t * Ntl_ManBuildNodeAig( Ntl_Obj_t * pNode )
 {
     Aig_Man_t * pMan = pNode->pModel->pMan->pAig;
-    int fUseFactor = 0;
+    int fUseFactor = 1;
     // consider the constant node
     if ( Ntl_SopGetVarNum(pNode->pSop) == 0 )
         return Aig_NotCond( Aig_ManConst1(pMan), Ntl_SopIsConst0(pNode->pSop) );
@@ -957,8 +957,8 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
 ***********************************************************************/
 static inline void Ntl_NetIncrementRefs( Ntl_Net_t * pNet )
 {
-    int nRefs = (int)pNet->pCopy;
-    pNet->pCopy = (void *)(nRefs + 1);
+    int nRefs = (int)(long)pNet->pCopy;
+    pNet->pCopy = (void *)(long)(nRefs + 1);
 }
 
 /**Function*************************************************************
@@ -981,7 +981,7 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
     if ( pNet->fMark )
         return pNet->pCopy;
     pNet->fMark = 1;
-    pNode = Nwk_ManCreateNode( pNtk, Ntl_ObjFaninNum(pNet->pDriver), (int)pNet->pCopy );
+    pNode = Nwk_ManCreateNode( pNtk, Ntl_ObjFaninNum(pNet->pDriver), (int)(long)pNet->pCopy );
     Ntl_ObjForEachFanin( pNet->pDriver, pFaninNet, i )
     {
         Ntl_ManExtractNwk_rec( p, pFaninNet, pNtk, vCover, vMemory );
@@ -1046,7 +1046,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
             pObj = Ntl_ModelPi( pRoot, Aig_ObjPioNum(pAnd) );
             pNet = Ntl_ObjFanout0(pObj);
             pNet->fMark = 1;
-            pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)pNet->pCopy ); 
+            pNet->pCopy = Nwk_ManCreateCi( pNtk, (int)(long)pNet->pCopy ); 
         }
         else if ( Aig_ObjIsPo(pAnd) )
         {
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 8a172e6c..98f14d3d 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -192,6 +192,8 @@ Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fL
 
     // derive the new AIG
     pTemp = Aig_ManDupRepresDfs( pAig );
+printf( "Intermediate:\n" );
+Aig_ManPrintStats( pTemp );
     // duplicate the timing manager
     if ( pAig->pManTime )
         pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
@@ -230,17 +232,21 @@ Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVe
     // perform fraiging for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAigCol) );
     Aig_ManStop( pTemp );
 
     // transfer equivalence classes to the original AIG
     pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
     pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAig) );
     // cleanup
     Aig_ManStop( pAigCol );
     Ntl_ManFree( pNew );
 
     // derive the new AIG
     pTemp = Aig_ManDupRepresDfs( pAig );
+//printf( "Intermediate LCORR:\n" );
+//Aig_ManPrintStats( pTemp );
     // duplicate the timing manager
     if ( pAig->pManTime )
         pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index fddd4167..cefa38d3 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -45,7 +45,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     float Delay;
-    int i, k;
+    int i, k, fClockAdded = 0;
     fprintf( pFile, ".model %s\n", pModel->pName );
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
@@ -117,8 +117,10 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
             if ( pObj->LatchId >> 2 )
                 fprintf( pFile, " %d", pObj->LatchId >> 2 );
-            if ( pObj->pFanio[1] != NULL )
+            if ( Ntl_ObjFanin(pObj, 1) != NULL )
                 fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
+            else if ( pObj->LatchId >> 2 )
+                fprintf( pFile, " clock" ), fClockAdded = 1;
             fprintf( pFile, " %d", pObj->LatchId & 3 );
             fprintf( pFile, "\n" );
         }
@@ -132,6 +134,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, "\n" );
         }
     }
+    if ( fClockAdded )
+        fprintf( pFile, ".names clock\n 0\n" );
     fprintf( pFile, ".end\n\n" );
 }