Cosmetic changes after incorporating new code of 'fxch'.

6 files changed, 89 insertions, 55 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cc687689..302b8553 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4139,13 +4139,13 @@ static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
 
     int c,
-        nMaxDivExt,
+        nMaxDivExt = 0,
         SMode = 0,
         fVerbose = 0,
         fVeryVerbose = 0;
 
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "NSvwh")) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "Nsvwh")) != EOF )
     {
         switch (c)
         {
@@ -4162,7 +4162,7 @@ static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv )
                     goto usage;
                 break;
 
-            case 'S':
+            case 's':
                 SMode ^= 1;
                 break;
 
@@ -4209,13 +4209,16 @@ static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: fxch [-N <num>] [-vwh]\n");
+    Abc_Print( -2, "usage: fxch [-N <num>] [-svwh]\n");
     Abc_Print( -2, "\t           performs fast extract with cube hashing on the current network\n");
-    Abc_Print( -2, "\t-N <num> : max number of divisors to extract during this run [default = %d]\n", nMaxDivExt );
-    Abc_Print( -2, "\t-S       : memory saving mode (slower) [default = %d]\n", SMode );
+    Abc_Print( -2, "\t-N <num> : max number of divisors to extract during this run [default = unused]\n" );
+    Abc_Print( -2, "\t-s       : memory saving mode (slower) [default = %d]\n", SMode? "yes": "no" );
     Abc_Print( -2, "\t-v       : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : print additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Bruno Schmitt from UFRGS in May 2016.\n" );
+    Abc_Print( -2, "\t           The author can be contacted as boschmitt at inf.ufrgs.br\n" );
     return 1;
 }
 
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index de7125bc..8208f68b 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -664,8 +664,8 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu
         printf( "The SOP has duplicated cubes.\n" );
     else if ( Vec_IntSize(vCubeFree) == 1 )
         printf( "The SOP has contained cubes.\n" );
-    else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) && !*fWarning )
-        printf( "The SOP has distance-1 cubes or it is not a prime cover.  Please make sure the result verifies.\n" ), *fWarning = 1;
+//    else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) && !*fWarning )
+//        printf( "The SOP has distance-1 cubes or it is not a prime cover.  Please make sure the result verifies.\n" ), *fWarning = 1;
     assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
     return Counter;
 }
diff --git a/src/opt/fxch/Fxch.c b/src/opt/fxch/Fxch.c
index 9d674720..a9228dc6 100644
--- a/src/opt/fxch/Fxch.c
+++ b/src/opt/fxch/Fxch.c
@@ -44,7 +44,8 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
                       int fVeryVerbose )
 {
     abctime TempTime;
-    Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes, SMode );
+    Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes, (char)SMode );
+    int i;
 
     TempTime = Abc_Clock();
     Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax );
@@ -61,7 +62,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
         Fxch_ManPrintStats( pFxchMan );
 
     TempTime = Abc_Clock();
-    for ( int i = 0; i < nMaxDivExt && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ )
+    for ( i = 0; (!nMaxDivExt || i < nMaxDivExt) && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ )
     {
         int iDiv = Vec_QuePop( pFxchMan->vDivPrio );
 
diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c
index 072198ef..9541d8e8 100644
--- a/src/opt/fxch/FxchDiv.c
+++ b/src/opt/fxch/FxchDiv.c
@@ -115,13 +115,16 @@ int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
 {
     int Base = 0;
 
-    Vec_IntClear( pFxchMan->vCubeFree );
-
     int SC0_Lit0,
         SC0_Lit1,
         SC1_Lit0,
         SC1_Lit1;
 
+    int Cube0Size,
+        Cube1Size;
+
+    Vec_IntClear( pFxchMan->vCubeFree );
+
     SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
     SC0_Lit1 = 0;
     SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
@@ -134,6 +137,8 @@ int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
     }
     else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
     {
+        int RetValue;
+
         SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
         SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
 
@@ -142,7 +147,7 @@ int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
         Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
         Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
 
-        int RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
+        RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
         if ( RetValue == -1 )
             return -1;
     } 
@@ -181,8 +186,8 @@ int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
         Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
     }
 
-    int Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) ),
-        Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
+    Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) );
+    Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
     if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
     {
         Base = Abc_MinInt( Cube0Size, Cube1Size )
@@ -535,7 +540,7 @@ void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan,
     {
         int CubeId1 = Fxch_ManGetLit( pFxchMan, *pBeg1, 0 ),
             CubeId2 = Fxch_ManGetLit( pFxchMan, *pBeg2, 0 ),
-            i, k;
+            i, k, i_, k_;
 
         if ( CubeId1 == CubeId2 )
         {
@@ -547,8 +552,8 @@ void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan,
                 if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg2[k], 0) )
                     break;
 
-            for ( int i_ = 0; i_ < i; i_++ )
-            for ( int k_ = 0; k_ < k; k_++ )
+            for ( i_ = 0; i_ < i; i_++ )
+            for ( k_ = 0; k_ < k; k_++ )
             {
                 if ( pBeg1[i_] == pBeg2[k_] )
                     continue;
diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c
index 6437950d..4fcd8e51 100644
--- a/src/opt/fxch/FxchMan.c
+++ b/src/opt/fxch/FxchMan.c
@@ -108,7 +108,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
     Fxch_ManSCAddRemove( pFxchMan,
                          SubCubeID, nHashedSC++,
                          iCube, 0, 0,
-                         fAdd, fUpdate );
+                         (char)fAdd, (char)fUpdate );
 
     Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
     {
@@ -118,7 +118,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
         pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
                                                   SubCubeID, nHashedSC++,
                                                   iCube, iLit0, 0,
-                                                  fAdd, fUpdate );
+                                                  (char)fAdd, (char)fUpdate );
 
         if ( Vec_IntSize( vCube ) > 3 )
         {
@@ -133,7 +133,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
                 pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
                                                           SubCubeID, nHashedSC++,
                                                           iCube, iLit0, iLit1,
-                                                          fAdd, fUpdate );
+                                                          (char)fAdd, (char)fUpdate );
 
                 SubCubeID += Vec_IntEntry( vLitHashKeys, Lit1 );
             }
@@ -246,10 +246,11 @@ void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan,
 
 void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan )
 {
+    int i;
     /* Generates the random number which will be used for hashing cubes */
     Gia_ManRandom( 1 );
     pFxchMan->vLitHashKeys = Vec_IntAlloc( ( 2 * pFxchMan->nVars ) );
-    for ( int i = 0; i < (2 * pFxchMan->nVars); i++ )
+    for ( i = 0; i < (2 * pFxchMan->nVars); i++ )
         Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
 }
 
@@ -355,10 +356,14 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
                      int iDiv )
 {
     int i,
+        k,
         iCube0, 
         iCube1,
         Lit0 = -1, 
-        Lit1 = -1;
+        Lit1 = -1,
+        iVarNew, 
+        Level,
+        nCompls;
 
     Vec_Int_t* vCube0,
              * vCube1,
@@ -439,7 +444,7 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
     }
 
     /* Create a new variable */
-    int iVarNew = pFxchMan->nVars;
+    iVarNew = pFxchMan->nVars;
     pFxchMan->nVars++;
 
     /* Create new Lit hash keys */
@@ -450,7 +455,6 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
     vCube0 = Vec_WecPushLevel( pFxchMan->vCubes );
     Vec_IntPush( vCube0, iVarNew );
 
-    int Level;
     if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
     {
         if ( Lit0 > Lit1 )
@@ -497,8 +501,8 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
 
     /* For each pair (Ci, Cj) */
     /* Extract divisor from cube pairs */
-    int k = 0,
-        nCompls = 0;
+    k = 0;
+    nCompls = 0;
     Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
     {
         int RetValue, fCompl = 0;
diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c
index f9c3e7a2..b2708337 100644
--- a/src/opt/fxch/FxchSCHashTable.c
+++ b/src/opt/fxch/FxchSCHashTable.c
@@ -19,6 +19,11 @@
 
 ABC_NAMESPACE_IMPL_START
 
+#ifdef _WIN32
+typedef unsigned int uint32_t;
+typedef unsigned char uint8_t;
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,12 +40,16 @@ static inline void MurmurHash3_x86_32 ( const void* key,
     const uint32_t c1 = 0xcc9e2d51;
     const uint32_t c2 = 0x1b873593;
 
+    const uint8_t * tail;
+    uint32_t k1;
+
     //----------
     // body
 
     const uint32_t * blocks = (const uint32_t *)(data + nblocks*4);
+    int i;
 
-    for(int i = -nblocks; i; i++)
+    for(i = -nblocks; i; i++)
     {
         uint32_t k1 = blocks[i];
 
@@ -56,9 +65,9 @@ static inline void MurmurHash3_x86_32 ( const void* key,
     //----------
     // tail
 
-    const uint8_t * tail = (const uint8_t*)(data + nblocks*4);
+    tail = (const uint8_t*)(data + nblocks*4);
 
-    uint32_t k1 = 0;
+    k1 = 0;
 
     switch(len & 3)
     {
@@ -146,9 +155,9 @@ static inline void Fxch_SCHashTableRemoveLink( Fxch_SCHashTable_t* pSCHashTable,
                             * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ),
                             * pEntry1Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry1->iNext );
 
-    assert( pEntry0->iNext == iEntry1 );
-    assert( pEntry1->iPrev == iEntry0 );
-    assert( pEntry1Next->iPrev == iEntry1 );
+    assert( (int)pEntry0->iNext == iEntry1 );
+    assert( (int)pEntry1->iPrev == iEntry0 );
+    assert( (int)pEntry1Next->iPrev == iEntry1 );
 
     pEntry0->iNext = pEntry1->iNext;
     pEntry1->iNext = 0;
@@ -220,11 +229,19 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
                             char fUpdate )
 {
     unsigned int BinID;
+    unsigned int iNewEntry;
+    Fxch_SCHashTable_Entry_t* pBin,* pNewEntry;
+
+    Fxch_SCHashTable_Entry_t* pEntry;
+    unsigned int iEntry;
+    char Pairs = 0,
+         fStart = 1;
+
     MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
     
-    unsigned int iNewEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
-    Fxch_SCHashTable_Entry_t* pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ),
-                            * pNewEntry = Fxch_SCHashTableEntry( pSCHashTable, iNewEntry );
+    iNewEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
+    pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
+    pNewEntry = Fxch_SCHashTableEntry( pSCHashTable, iNewEntry );
 
     assert( pNewEntry->Used == 0 );
 
@@ -243,12 +260,11 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
         return 0;
     }
 
-    Fxch_SCHashTable_Entry_t* pEntry;
-    unsigned int iEntry;
-    char Pairs = 0,
-         fStart = 1;
     for ( iEntry = pBin->iTable; iEntry != pBin->iTable || fStart; iEntry = pEntry->iNext, fStart = 0 )
     {
+        int Base;
+        int iNewDiv;
+
         pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry );
 
         if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) )
@@ -265,7 +281,6 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
             continue;
         }
 
-        int Base;
         if ( pEntry->SCData.iCube < pNewEntry->SCData.iCube )
             Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNewEntry->SCData ) );
         else
@@ -274,7 +289,7 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
         if ( Base < 0 ) 
             continue;
 
-        int iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
+        iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
         if ( pSCHashTable->pFxchMan->SMode == 0 )
         {
@@ -302,11 +317,18 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
                             char fUpdate )
 {
     unsigned int BinID;
+    unsigned int iEntry;
+    Fxch_SCHashTable_Entry_t* pBin,* pEntry;
+    Fxch_SCHashTable_Entry_t* pNextEntry;
+    int iNextEntry,
+        Pairs = 0,
+        fStart = 1;
+
     MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
     
-    unsigned int iEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
-    Fxch_SCHashTable_Entry_t* pBin = Fxch_SCHashTableBin( pSCHashTable, BinID ),
-                            * pEntry = Fxch_SCHashTableEntry( pSCHashTable, iEntry );
+    iEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
+    pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
+    pEntry = Fxch_SCHashTableEntry( pSCHashTable, iEntry );
     
     assert( pEntry->Used == 1 );
     assert( pEntry->SCData.iCube == iCube );
@@ -321,12 +343,11 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
         return 0;
     }
 
-    Fxch_SCHashTable_Entry_t* pNextEntry;
-    int iNextEntry,
-        Pairs = 0,
-        fStart = 1;
-    for ( iNextEntry = pEntry->iNext; iNextEntry != iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 )
+    for ( (int)iNextEntry = pEntry->iNext; iNextEntry != (int)iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 )
     {
+        int Base, 
+            iDiv;
+
         pNextEntry = Fxch_SCHashTableBin( pSCHashTable, iNextEntry );
 
         if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNextEntry->SCData ) ) 
@@ -334,7 +355,6 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
              || pNextEntry->SCData.iLit0 == 0 )
             continue;
 
-        int Base;
         if ( pNextEntry->SCData.iCube < pEntry->SCData.iCube )
             Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNextEntry->SCData ), &( pEntry->SCData ) );
         else
@@ -343,7 +363,7 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
         if ( Base < 0 ) 
             continue;
 
-        int iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
+        iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
         if ( pSCHashTable->pFxchMan->SMode == 0 )
         {
@@ -353,8 +373,8 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
 
             Vec_Int_t* vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv );
             Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i )
-                if ( ( iCube0 == pNextEntry->SCData.iCube &&  iCube1 == pEntry->SCData.iCube )  ||
-                     ( iCube0 == pEntry->SCData.iCube &&  iCube1 == pNextEntry->SCData.iCube ) )
+                if ( ( iCube0 == (int)pNextEntry->SCData.iCube &&  iCube1 == (int)pEntry->SCData.iCube )  ||
+                     ( iCube0 == (int)pEntry->SCData.iCube &&  iCube1 == (int)pNextEntry->SCData.iCube ) )
                 {
                     Vec_IntDrop( vDivCubePairs, i+1 );
                     Vec_IntDrop( vDivCubePairs, i );
@@ -386,11 +406,12 @@ unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* pHashTable )
 
 void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* pHashTable )
 {
+    int Memory;
     printf( "SubCube Hash Table at %p\n", ( void* )pHashTable );
     printf("%20s %20s\n", "nEntries",
                           "Memory Usage (MB)" );
 
-    int Memory = Fxch_SCHashTableMemory( pHashTable );
+    Memory = Fxch_SCHashTableMemory( pHashTable );
     printf("%20d %18.2f\n", pHashTable->nEntries,
                             ( ( double ) Memory / 1048576 ) );
 }