Version abc80411

7 files changed, 166 insertions, 12 deletions

diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 4c99c3a9..6fc84893 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -195,6 +195,8 @@ static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { r
 /*=== 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 );
+/*=== nwkCheck.c ==========================================================*/
+extern int             Nwk_ManCheck( Nwk_Man_t * p );
 /*=== nwkDfs.c ==========================================================*/
 extern int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
 extern int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
@@ -253,6 +255,7 @@ extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_
 extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
 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 );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkCheck.c b/src/aig/nwk/nwkCheck.c
index 5c547dbe..6922e439 100644
--- a/src/aig/nwk/nwkCheck.c
+++ b/src/aig/nwk/nwkCheck.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Checking the logic network for consistency.]
 
   Description []
                
@@ -39,6 +39,32 @@
   SeeAlso     []
 
 ***********************************************************************/
+int Nwk_ManCheck( Nwk_Man_t * p )
+{
+    Nwk_Obj_t * pObj;
+    int i, k, m;
+    // check if the nodes have duplicated fanins
+    Nwk_ManForEachNode( p, pObj, i )
+    {
+        for ( k = 0; k < pObj->nFanins; k++ )
+            for ( m = k + 1; m < pObj->nFanins; m++ )
+                if ( pObj->pFanio[k] == pObj->pFanio[m] )
+                    printf( "Node %d has duplicated fanin %d.\n", pObj->Id, pObj->pFanio[k]->Id );
+    }
+/*
+    // check if all nodes are in the correct fanin/fanout relationship
+    Nwk_ManForEachObj( p, pObj, i )
+    {
+        Nwk_ObjForEachFanin( pObj, pNext, k )
+            if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 )
+                printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id );
+        Nwk_ObjForEachFanout( pObj, pNext, k )
+            if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 )
+                printf( "Nwk_ManCheck(): Object %d has fanout %d which does not have a corresponding fanin.\n", pObj->Id, pNext->Id );
+    }
+*/
+    return 1;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/nwk/nwkFanio.c b/src/aig/nwk/nwkFanio.c
index f338d07d..1b701e9e 100644
--- a/src/aig/nwk/nwkFanio.c
+++ b/src/aig/nwk/nwkFanio.c
@@ -221,7 +221,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
         Nwk_ManReallocNode( pObj );
     if ( Nwk_ObjReallocIsNeeded(pFanin) )
         Nwk_ManReallocNode( pFanin );
-    for ( i = pObj->nFanins + pObj->nFanouts; i > (int)pObj->nFanins; i-- )
+    for ( i = pObj->nFanins + pObj->nFanouts; i > pObj->nFanins; i-- )
         pObj->pFanio[i] = pObj->pFanio[i-1];
     pObj->pFanio[pObj->nFanins++] = pFanin;
     pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
@@ -247,15 +247,15 @@ void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
     for ( k = i = 0; i < Limit; i++ )
         if ( pObj->pFanio[i] != pFanin )
             pObj->pFanio[k++] = pObj->pFanio[i];
-    assert( i == k + 1 );
+    assert( i == k + 1 ); // if it fails, likely because of duplicated fanin
     pObj->nFanins--;
     // remove pObj from the fanout list of pFanin
     Limit = pFanin->nFanins + pFanin->nFanouts;
     for ( k = i = pFanin->nFanins; i < Limit; i++ )
         if ( pFanin->pFanio[i] != pObj )
             pFanin->pFanio[k++] = pFanin->pFanio[i];
-    assert( i == k + 1 );
-    pFanin->nFanouts--;
+    assert( i == k + 1 ); // if it fails, likely because of duplicated fanout
+    pFanin->nFanouts--; 
 }
 
 /**Function*************************************************************
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index 6c1e1330..f5b2b7f8 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -56,7 +56,7 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fExpRed     =  0;
+    pPars->fExpRed     =  1; ////
     pPars->fLatchPaths =  0;
     pPars->fEdge       =  1;
     pPars->fCutMin     =  0;
@@ -244,16 +244,25 @@ Hop_Obj_t * Nwk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
 ***********************************************************************/
 Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToIf )
 {
+    Vec_Ptr_t * vIfToAig;
     Nwk_Man_t * pNtk;
     Nwk_Obj_t * pObjNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjRepr;
     If_Obj_t * pIfObj;
     If_Cut_t * pCutBest;
     int i, k, nLeaves, * ppLeaves;
     assert( Aig_ManPiNum(p) == If_ManCiNum(pIfMan) );
     assert( Aig_ManPoNum(p) == If_ManCoNum(pIfMan) );
     assert( Aig_ManNodeNum(p) == If_ManAndNum(pIfMan) );
+    Aig_ManCleanData( p );
     If_ManCleanCutData( pIfMan );
+    // create mapping of IF to AIG
+    vIfToAig = Vec_PtrStart( If_ManObjNum(pIfMan) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pIfObj = Vec_PtrEntry( vAigToIf, i );
+        Vec_PtrWriteEntry( vIfToAig, pIfObj->Id, pObj );
+    }
     // construct the network
     pNtk = Nwk_ManAlloc();
     pNtk->pName = Aig_UtilStrsav( p->pName );
@@ -271,7 +280,10 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
             // create node
             pObjNew = Nwk_ManCreateNode( pNtk, nLeaves, pIfObj->nRefs );
             for ( k = 0; k < nLeaves; k++ )
-                Nwk_ObjAddFanin( pObjNew, Aig_ManObj(p, ppLeaves[k])->pData );
+            {
+                pObjRepr = Vec_PtrEntry( vIfToAig, ppLeaves[k] );
+                Nwk_ObjAddFanin( pObjNew, pObjRepr->pData );
+            }
             // get the functionality
             pObjNew->pFunc = Nwk_NodeIfToHop( pNtk->pManHop, pIfMan, pIfObj );
         }
@@ -292,7 +304,9 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
             assert( 0 );
         pObj->pData = pObjNew;
     }
+    Vec_PtrFree( vIfToAig );
     pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    assert( Nwk_ManCheck( pNtk ) );
     return pNtk;
 }
 
@@ -328,6 +342,8 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
     }
     // transform the result of mapping into the new network
     pNtk = Nwk_ManFromIf( pIfMan, p, vAigToIf );
+    if ( pPars->fBidec && pPars->nLutSize <= 8 )
+        Nwk_ManBidecResyn( pNtk, 0 );
     If_ManStop( pIfMan );
     Vec_PtrFree( vAigToIf );
     return pNtk;
diff --git a/src/aig/nwk/nwkObj.c b/src/aig/nwk/nwkObj.c
index 6d1f0428..58587f07 100644
--- a/src/aig/nwk/nwkObj.c
+++ b/src/aig/nwk/nwkObj.c
@@ -154,10 +154,8 @@ void Nwk_ManDeleteNode( Nwk_Obj_t * pObj )
     Vec_Ptr_t * vNodes = pObj->pMan->vTemp;
     Nwk_Obj_t * pTemp;
     int i;
-    // delete fanins and fanouts
-    Nwk_ObjCollectFanouts( pObj, vNodes );
-    Vec_PtrForEachEntry( vNodes, pTemp, i )
-        Nwk_ObjDeleteFanin( pTemp, pObj );
+    assert( Nwk_ObjFanoutNum(pObj) == 0 );
+    // delete fanins
     Nwk_ObjCollectFanins( pObj, vNodes );
     Vec_PtrForEachEntry( vNodes, pTemp, i )
         Nwk_ObjDeleteFanin( pObj, pTemp );
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index c27f9d61..9ab24467 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -427,6 +427,8 @@ int Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk )
     int i;
     Nwk_ManForEachObj( pNtk, pObj, i )
     {
+        if ( Nwk_ObjIsPi(pObj) && Nwk_ObjFanoutNum(pObj) == 0 )
+            continue;
         tArrival = Nwk_NodeComputeArrival( pObj, 1 );
         tRequired = Nwk_NodeComputeRequired( pObj, 1 );
         if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) )
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 5fb594ec..97c95d27 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "nwk.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -254,6 +255,114 @@ void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames,
     printf( "Dumping logic network is currently not supported.\n" );
 }
 
+/**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)  );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////