Removing the memory saving mode, it is no longer necessary.

5 files changed, 17 insertions, 178 deletions

diff --git a/src/opt/fxch/Fxch.c b/src/opt/fxch/Fxch.c
index a9228dc6..6c3983ef 100644
--- a/src/opt/fxch/Fxch.c
+++ b/src/opt/fxch/Fxch.c
@@ -39,12 +39,11 @@ ABC_NAMESPACE_IMPL_START
 int Fxch_FastExtract( Vec_Wec_t* vCubes,
                       int ObjIdMax,
                       int nMaxDivExt,
-                      int SMode, 
                       int fVerbose,
                       int fVeryVerbose )
 {
     abctime TempTime;
-    Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes, (char)SMode );
+    Fxch_Man_t* pFxchMan = Fxch_ManAlloc( vCubes );
     int i;
 
     TempTime = Abc_Clock();
@@ -102,7 +101,6 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
 ***********************************************************************/
 int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk,
                         int nMaxDivExt,
-                        int SMode,
                         int fVerbose,
                         int fVeryVerbose )
 {
@@ -117,7 +115,7 @@ int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk,
     }
 
     vCubes = Abc_NtkFxRetrieve( pNtk );
-    if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, SMode, fVerbose, fVeryVerbose ) > 0 )
+    if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, fVerbose, fVeryVerbose ) > 0 )
     {
         Abc_NtkFxInsert( pNtk, vCubes );
         Vec_WecFree( vCubes );
diff --git a/src/opt/fxch/Fxch.h b/src/opt/fxch/Fxch.h
index be229b98..d9f9dc7e 100644
--- a/src/opt/fxch/Fxch.h
+++ b/src/opt/fxch/Fxch.h
@@ -113,9 +113,6 @@ struct Fxch_Man_t_
     Vec_Int_t*     vCubeFree;  // cube-free divisor
     Vec_Int_t*     vDiv;       // selected divisor
 
-    /* Config */
-    char    SMode;        /* Saving Memory mode */
-
     /* Statistics */
     abctime timeInit;   /* Initialization time */
     abctime timeExt;    /* Extraction time */
@@ -138,8 +135,8 @@ extern void       Abc_NtkFxInsert( Abc_Ntk_t* pNtk, Vec_Wec_t* vCubes );
 extern int        Abc_NtkFxCheck( Abc_Ntk_t* pNtk );
 
 /*===== Fxch.c =======================================================*/
-int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose );
-int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose );
+int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int fVerbose, int fVeryVerbose );
+int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int fVerbose, int fVeryVerbose );
 
 /*===== FxchDiv.c ====================================================================================================*/
 int  Fxch_DivCreate( Fxch_Man_t* pFxchMan,  Fxch_SubCube_t* pSubCube0, Fxch_SubCube_t* pSubCube1 );
@@ -149,13 +146,8 @@ void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube
 int  Fxch_DivRemoveLits( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vDiv, int *fCompl );
 void Fxch_DivPrint( Fxch_Man_t* pFxchMan, int iDiv );
 
-/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ 
-void Fxch_DivFindPivots( Vec_Int_t* vDiv, int* pLit0, int* pLit1 );
-int  Fxch_DivFind( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vCubeFree );
-void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubes_Lit0, Vec_Int_t* vCubes_Lit1 );
-
 /*===== FxchMan.c ====================================================================================================*/
-Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes, char SMode );
+Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes );
 void  Fxch_ManFree( Fxch_Man_t* pFxchMan );
 void  Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, int nVars );
 void  Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan );
diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c
index 9541d8e8..68fd569d 100644
--- a/src/opt/fxch/FxchDiv.c
+++ b/src/opt/fxch/FxchDiv.c
@@ -225,8 +225,7 @@ int Fxch_DivAdd( Fxch_Man_t* pFxchMan,
     /* Verify if the divisor already exist */ 
     if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
     {
-        if ( pFxchMan->SMode == 0 )
-            Vec_WecPushLevel( pFxchMan->vDivCubePairs );
+        Vec_WecPushLevel( pFxchMan->vDivCubePairs );
 
         /* Assign initial weight */
         if ( fSingleCube )
@@ -458,128 +457,6 @@ void Fxch_DivPrint( Fxch_Man_t* pFxchMan,
     printf( "Divs =%8d  \n", Hsh_VecSize( pFxchMan->pDivHash ) );
 }
 
-/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ 
-void Fxch_DivFindPivots( Vec_Int_t* vDiv, 
-                         int* pLit0, 
-                         int* pLit1 )
-{
-    int  i, 
-         Lit;
-       * pLit0 = -1;
-       * pLit1 = -1;
- 
-    Vec_IntForEachEntry( vDiv, Lit, i )
-    {
-        if ( Abc_LitIsCompl( Lit ) )
-        {
-            if ( *pLit1 == -1 )
-                *pLit1 = Abc_Lit2Var( Lit );
-        }
-        else
-        {
-            if ( *pLit0 == -1 )
-                *pLit0 = Abc_Lit2Var( Lit );
-        }
-        if ( *pLit0 >= 0 && *pLit1 >= 0 )
-            return;
-    }
-}
-
-int Fxch_DivFind( Vec_Int_t* vCube0,
-                  Vec_Int_t* vCube1,
-                  Vec_Int_t* vCubeFree )
-{
-    int Counter = 0, 
-        fAttr0 = 0,
-        fAttr1 = 1;
-    int* pBeg1 = vCube0->pArray + 1,
-       * pBeg2 = vCube1->pArray + 1,
-       * pEnd1 = vCube0->pArray + vCube0->nSize,
-       * pEnd2 = vCube1->pArray + vCube1->nSize;
- 
-    Vec_IntClear( vCubeFree );
-
-    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
-    {
-        if ( *pBeg1 == *pBeg2 )
-        {
-            pBeg1++;
-            pBeg2++;
-            Counter++;
-        }
-        else if ( *pBeg1 < *pBeg2 )
-            Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) );
-        else  
-        {
-            if ( Vec_IntSize( vCubeFree ) == 0 )
-                fAttr0 = 1, fAttr1 = 0;
-            Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1) );
-        }
-    }
-    while ( pBeg1 < pEnd1 )
-        Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) );
-    while ( pBeg2 < pEnd2 )
-        Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1 ) );
-
-    assert( !Abc_LitIsCompl( Vec_IntEntry(vCubeFree, 0) ) );
-    return Counter;
-}
-
-void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan,
-                            Vec_Int_t* vCubes_Lit0, 
-                            Vec_Int_t* vCubes_Lit1 )
-{
-    int* pBeg1 = vCubes_Lit0->pArray + 1,
-       * pBeg2 = vCubes_Lit1->pArray + 1,
-       * pEnd1 = vCubes_Lit0->pArray + vCubes_Lit0->nSize,
-       * pEnd2 = vCubes_Lit1->pArray + vCubes_Lit1->nSize;
- 
-    Vec_IntClear( pFxchMan->vPairs );
-
-    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
-    {
-        int CubeId1 = Fxch_ManGetLit( pFxchMan, *pBeg1, 0 ),
-            CubeId2 = Fxch_ManGetLit( pFxchMan, *pBeg2, 0 ),
-            i, k, i_, k_;
-
-        if ( CubeId1 == CubeId2 )
-        {
-            for ( i = 1; pBeg1+i < pEnd1; i++ )
-                if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg1[i], 0) )
-                    break;
-
-            for ( k = 1; pBeg2+k < pEnd2; k++ )
-                if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg2[k], 0) )
-                    break;
-
-            for ( i_ = 0; i_ < i; i_++ )
-            for ( k_ = 0; k_ < k; k_++ )
-            {
-                if ( pBeg1[i_] == pBeg2[k_] )
-                    continue;
-                Fxch_DivFind( Vec_WecEntry( pFxchMan->vCubes, pBeg1[i_] ),
-                              Vec_WecEntry( pFxchMan->vCubes, pBeg2[k_] ), 
-                              pFxchMan->vCubeFree );
-
-                if ( Vec_IntSize( pFxchMan->vCubeFree ) == 4 )
-                    Fxch_DivNormalize( pFxchMan->vCubeFree );
-
-                if ( !Vec_IntEqual( pFxchMan->vDiv, pFxchMan->vCubeFree ) )
-                    continue;
-
-                Vec_IntPush( pFxchMan->vPairs, pBeg1[i_] );
-                Vec_IntPush( pFxchMan->vPairs, pBeg2[k_] );
-            }
-            pBeg1 += i;
-            pBeg2 += k;
-        }
-        else if ( CubeId1 < CubeId2 )
-            pBeg1++;
-        else 
-            pBeg2++;
-    }
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c
index a54e6c9a..83794ea9 100644
--- a/src/opt/fxch/FxchMan.c
+++ b/src/opt/fxch/FxchMan.c
@@ -160,23 +160,18 @@ static inline void Fxch_ManCompressCubes( Vec_Wec_t* vCubes,
 ////////////////////////////////////////////////////////////////////////
 ///                     PUBLIC INTERFACE                             ///
 ////////////////////////////////////////////////////////////////////////
-Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes,
-                           char SMode )
+Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes )
 {
     Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 );
 
     pFxchMan->vCubes = vCubes;
-    pFxchMan->pDivHash    = Hsh_VecManStart( 1000 );
+    pFxchMan->pDivHash = Hsh_VecManStart( 1000 );
     pFxchMan->vDivWeights = Vec_FltAlloc( 1000 );
-
-    pFxchMan->SMode = SMode;
-    if ( pFxchMan->SMode == 0 )
-        pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 );
-
+    pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 );
     pFxchMan->vCubeFree = Vec_IntAlloc( 100 );
-    pFxchMan->vDiv      = Vec_IntAlloc( 100 );
-    pFxchMan->vCubesS   = Vec_IntAlloc( 100 );
-    pFxchMan->vPairs    = Vec_IntAlloc( 100 );
+    pFxchMan->vDiv = Vec_IntAlloc( 100 );
+    pFxchMan->vCubesS = Vec_IntAlloc( 100 );
+    pFxchMan->vPairs = Vec_IntAlloc( 100 );
 
     return pFxchMan;
 }
@@ -186,21 +181,15 @@ void Fxch_ManFree( Fxch_Man_t* pFxchMan )
     Vec_WecFree( pFxchMan->vLits );
     Vec_IntFree( pFxchMan->vLitCount );
     Vec_IntFree( pFxchMan->vLitHashKeys );
-
     Hsh_VecManStop( pFxchMan->pDivHash );
     Vec_FltFree( pFxchMan->vDivWeights );
     Vec_QueFree( pFxchMan->vDivPrio );
-
-    if ( pFxchMan->SMode == 0 )
-        Vec_WecFree( pFxchMan->vDivCubePairs );
-
+    Vec_WecFree( pFxchMan->vDivCubePairs );
     Vec_IntFree( pFxchMan->vLevels );
-
     Vec_IntFree( pFxchMan->vCubeFree );
     Vec_IntFree( pFxchMan->vDiv );
     Vec_IntFree( pFxchMan->vCubesS );
     Vec_IntFree( pFxchMan->vPairs );
-
     ABC_FREE( pFxchMan );
 }
 
@@ -381,6 +370,7 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
     {
         Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) );
         Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) );
+        assert( Lit0 >= 0 && Lit1 >= 0 );
 
         Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) );
         Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) );
@@ -388,25 +378,13 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
                                 Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ),
                                 pFxchMan->vCubesS );
     }
-    else
-        Fxch_DivFindPivots( pFxchMan->vDiv, &Lit0, &Lit1 );
 
-    assert( Lit0 >= 0 && Lit1 >= 0 );
 
     /* Find pairs associated with the divisor */
     Vec_IntClear( pFxchMan->vPairs );
-    if ( pFxchMan->SMode == 1 )
-    {
-        Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit0) );
-        Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry(pFxchMan->vLits, Lit1) );
-        Fxch_DivFindCubePairs( pFxchMan, Vec_WecEntry( pFxchMan->vLits, Lit0 ), Vec_WecEntry( pFxchMan->vLits, Lit1 ) );
-    }
-    else
-    {
-        vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv );
-        Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs );
-        Vec_IntErase( vDivCubePairs );
-    }
+    vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv );
+    Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs );
+    Vec_IntErase( vDivCubePairs );
 
     Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
     {
diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c
index 149169ad..669d92c2 100644
--- a/src/opt/fxch/FxchSCHashTable.c
+++ b/src/opt/fxch/FxchSCHashTable.c
@@ -291,11 +291,8 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
 
         iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
-        if ( pSCHashTable->pFxchMan->SMode == 0 )
-        {
         Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->SCData.iCube );
         Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->SCData.iCube );
-        }
 
         Pairs++;
     }
@@ -365,8 +362,6 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
 
         iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
-        if ( pSCHashTable->pFxchMan->SMode == 0 )
-        {
         int i,
             iCube0,
             iCube1;
@@ -381,7 +376,6 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
             }
         if ( Vec_IntSize( vDivCubePairs ) == 0 )
             Vec_IntErase( vDivCubePairs );
-        }
 
         Pairs++;
     }