Merged alanmi/abc into default

src/opt/fxch/Fxch.c

@@ -15,7 +15,6 @@
   Revision    []
 
 ***********************************************************************/
-
 #include "Fxch.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -26,6 +25,128 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxch_CubesGruping(Fxch_Man_t* pFxchMan)
+{
+    Vec_Int_t* vCube;
+    int iCube, nOutputs, SizeOutputID;
+    Hsh_VecMan_t* pCubeHash;
+
+    /* Identify the number of Outputs and create the translation table */
+    pFxchMan->vTranslation = Vec_IntAlloc( 32 );
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
+    {
+        int Id = Vec_IntEntry( vCube, 0 );
+        int iTranslation = Vec_IntFind( pFxchMan->vTranslation, Id );
+
+        if ( iTranslation == -1 )
+            Vec_IntPush( pFxchMan->vTranslation, Id );
+    }
+    nOutputs = Vec_IntSize( pFxchMan->vTranslation );
+
+    /* Size of the OutputID in number o ints */
+    SizeOutputID = ( nOutputs >> 5 ) + ( ( nOutputs & 31 ) > 0 );
+
+    /* Initialize needed structures */
+    pFxchMan->vOutputID = Vec_IntAlloc( 4096 );
+    pFxchMan->pTempOutputID = ABC_CALLOC( int, SizeOutputID );
+    pFxchMan->nSizeOutputID = SizeOutputID;
+
+    pCubeHash =  Hsh_VecManStart( 1024 );
+
+    /* Identify equal cubes */
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
+    {
+        int Id = Vec_IntEntry( vCube, 0 );
+        int iTranslation = Vec_IntFind( pFxchMan->vTranslation, Id );
+        int i, iCubeNoID, Temp, * pEntry;
+        Vec_IntWriteEntry( vCube, 0, 0 ); // Clear ID, Outputs will be identified by it later
+
+        iCubeNoID = Hsh_VecManAdd( pCubeHash, vCube );
+        Temp = ( 1 << ( iTranslation & 31 ) );
+        if ( iCubeNoID == Vec_IntSize( pFxchMan->vOutputID ) / SizeOutputID )
+        {
+            for ( i = 0; i < SizeOutputID; i++ )
+                pFxchMan->pTempOutputID[i] = 0;
+
+            pFxchMan->pTempOutputID[ iTranslation >> 5 ] = Temp;
+            Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, SizeOutputID ); 
+        }
+        else
+        {
+            Vec_IntClear( vCube );
+            pEntry = Vec_IntEntryP( pFxchMan->vOutputID, ( iCubeNoID * SizeOutputID ) + ( iTranslation >> 5 ) );
+            *pEntry |= Temp;
+        }
+    }
+
+    Hsh_VecManStop( pCubeHash );
+    Vec_WecRemoveEmpty( pFxchMan->vCubes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxch_CubesUnGruping(Fxch_Man_t* pFxchMan)
+{
+    int iCube;
+    int i, j;
+    Vec_Int_t* vCube;
+    Vec_Int_t* vNewCube;
+
+    assert( Vec_WecSize( pFxchMan->vCubes ) == ( Vec_IntSize( pFxchMan->vOutputID ) / pFxchMan->nSizeOutputID ) );
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
+    {
+        int * pOutputID, nOnes;
+        if ( Vec_IntSize( vCube ) == 0 || Vec_IntEntry( vCube, 0 ) != 0 )
+            continue;
+
+        pOutputID = Vec_IntEntryP( pFxchMan->vOutputID, iCube * pFxchMan->nSizeOutputID );
+        nOnes = 0;
+
+        for ( i = 0; i < pFxchMan->nSizeOutputID; i++ )
+            nOnes += Fxch_CountOnes( (unsigned int) pOutputID[i] );
+
+        for ( i = 0; i < pFxchMan->nSizeOutputID && nOnes; i++ )
+            for ( j = 0; j < 32 && nOnes; j++ )
+                if ( pOutputID[i] & ( 1 << j ) )
+                {
+                    if ( nOnes == 1 )
+                        Vec_IntWriteEntry( vCube, 0, Vec_IntEntry( pFxchMan->vTranslation, ( i << 5 ) | j ) );
+                    else
+                    {
+                        vNewCube = Vec_WecPushLevel( pFxchMan->vCubes );
+                        Vec_IntAppend( vNewCube, vCube );
+                        Vec_IntWriteEntry( vNewCube, 0, Vec_IntEntry( pFxchMan->vTranslation, (i << 5 ) | j ) );
+                    }
+                    nOnes -= 1;
+                }
+    }
+
+    Vec_IntFree( pFxchMan->vTranslation );
+    Vec_IntFree( pFxchMan->vOutputID );
+    ABC_FREE( pFxchMan->pTempOutputID );
+    return;
+}
+
+/**Function*************************************************************
+
   Synopsis    [ Performs fast extract with cube hashing on a set
                 of covers. ]
 
@@ -47,6 +168,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
     int i;
 
     TempTime = Abc_Clock();
+    Fxch_CubesGruping( pFxchMan );
     Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax );
     Fxch_ManGenerateLitHashKeys( pFxchMan );
     Fxch_ManComputeLevel( pFxchMan );
@@ -61,6 +183,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
         Fxch_ManPrintStats( pFxchMan );
 
     TempTime = Abc_Clock();
+    
     for ( i = 0; (!nMaxDivExt || i < nMaxDivExt) && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ )
     {
         int iDiv = Vec_QuePop( pFxchMan->vDivPrio );
@@ -70,6 +193,7 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
 
         Fxch_ManUpdate( pFxchMan, iDiv );
     }
+   
     pFxchMan->timeExt = Abc_Clock() - TempTime;
 
     if ( fVerbose )
@@ -80,9 +204,12 @@ int Fxch_FastExtract( Vec_Wec_t* vCubes,
         Abc_PrintTime( 1, "[FXCH]    +-> Extr", pFxchMan->timeExt );
     }
 
+    Fxch_CubesUnGruping( pFxchMan );
     Fxch_ManSCHashTablesFree( pFxchMan );
     Fxch_ManFree( pFxchMan );
+
     Vec_WecRemoveEmpty( vCubes );
+    Vec_WecSortByFirstInt( vCubes, 0 );
 
     return 1;
 }

src/opt/fxch/Fxch.h

@@ -28,6 +28,9 @@
 
 ABC_NAMESPACE_HEADER_START
 
+typedef unsigned char uint8_t;
+typedef unsigned int  uint32_t;
+
 ////////////////////////////////////////////////////////////////////////
 ///                    TYPEDEF DECLARATIONS                          ///
 ////////////////////////////////////////////////////////////////////////
@@ -52,25 +55,22 @@ typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t;
  *   its literals.
  *
  */
+
 struct Fxch_SubCube_t_
 {
-    unsigned int Id,
+    uint32_t Id,
              iCube;
-    unsigned int iLit0 : 16,
+    uint32_t iLit0 : 16,
              iLit1 : 16;
 };
 
 /* Sub-cube Hash Table
- *
  */
 struct Fxch_SCHashTable_Entry_t_
 {
-    Fxch_SubCube_t SCData;
-
-    unsigned int iTable : 31,
-                 Used   :  1;
-    unsigned int iPrev,
-                 iNext;
+    Fxch_SubCube_t* vSCData;
+    uint32_t Size : 16,
+             Cap : 16;
 };
 
 struct Fxch_SCHashTable_t_
@@ -80,7 +80,6 @@ struct Fxch_SCHashTable_t_
     Fxch_SCHashTable_Entry_t* pBins;
     unsigned int nEntries,
                  SizeMask;
-    Vec_Int_t*   vCubeLinks;
 
     /* Temporary data */
     Vec_Int_t    vSubCube0;
@@ -91,6 +90,7 @@ struct Fxch_Man_t_
 {
     /* user's data */
     Vec_Wec_t* vCubes;
+    int nCubesInit;
     int LitCountMax;
 
     /* internal data */
@@ -107,11 +107,20 @@ struct Fxch_Man_t_
 
     Vec_Int_t*    vLevels;       /* variable levels */
 
+    // Cube Grouping
+    Vec_Int_t* vTranslation;
+    Vec_Int_t* vOutputID;
+    int* pTempOutputID;
+    int  nSizeOutputID;
+
     // temporary data to update the data-structure when a divisor is extracted
     Vec_Int_t* vCubesS;    /* cubes for the given single cube divisor */
     Vec_Int_t* vPairs;     /* cube pairs for the given double cube divisor */
     Vec_Int_t* vCubeFree;  // cube-free divisor
     Vec_Int_t* vDiv;       // selected divisor
+
+    Vec_Int_t* vCubesToRemove;
+    Vec_Int_t* vCubesToUpdate;
     Vec_Int_t* vSCC;
 
     /* Statistics */
@@ -135,6 +144,15 @@ extern Vec_Wec_t* Abc_NtkFxRetrieve( Abc_Ntk_t* pNtk );
 extern void       Abc_NtkFxInsert( Abc_Ntk_t* pNtk, Vec_Wec_t* vCubes );
 extern int        Abc_NtkFxCheck( Abc_Ntk_t* pNtk );
 
+static inline int Fxch_CountOnes( unsigned num )
+{
+    num = ( num & 0x55555555 ) + ( ( num >> 1) & 0x55555555 );
+    num = ( num & 0x33333333 ) + ( ( num >> 2) & 0x33333333 );
+    num = ( num & 0x0F0F0F0F ) + ( ( num >> 4) & 0x0F0F0F0F );
+    num = ( num & 0x00FF00FF ) + ( ( num >> 8) & 0x00FF00FF );
+    return  ( num & 0x0000FFFF ) + ( num >> 16 );
+}
+
 /*===== Fxch.c =======================================================*/
 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 );
@@ -177,26 +195,25 @@ static inline int Fxch_ManGetLit( Fxch_Man_t* pFxchMan,
 }
 
 /*===== FxchSCHashTable.c ============================================*/
-Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeLinks, int nEntries );
+Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, int nEntries );
 
 void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* );
 
 int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
                             Vec_Wec_t* vCubes,
-                            unsigned int SubCubeID,
-                            unsigned int iSubCube,
-                            unsigned int iCube,
-                            unsigned int iLit0,
-                            unsigned int iLit1,
+                            uint32_t SubCubeID,
+                            uint32_t iCube,
+                            uint32_t iLit0,
+                            uint32_t iLit1,
                             char fUpdate );
 
+
 int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
                             Vec_Wec_t* vCubes,
-                            unsigned int SubCubeID,
-                            unsigned int iSubCube,
-                            unsigned int iCube,
-                            unsigned int iLit0,
-                            unsigned int iLit1,
+                            uint32_t SubCubeID,
+                            uint32_t iCube,
+                            uint32_t iLit0,
+                            uint32_t iLit1,
                             char fUpdate );
 
 unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* );

src/opt/fxch/FxchDiv.c

@@ -142,10 +142,20 @@ int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
         SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
         SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
 
+        if ( SC0_Lit0 < SC1_Lit0 )
+        {
             Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
             Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
             Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
             Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
+        }
+        else
+        {
+            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) );
+            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) );
+            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) );
+            Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) );
+        }
 
         RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
         if ( RetValue == -1 )

src/opt/fxch/FxchMan.c

@@ -15,7 +15,6 @@
   Revision    []
 
 ***********************************************************************/
-
 #include "Fxch.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -25,7 +24,6 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan,
                                        unsigned int SubCubeID,
-                                       unsigned int iSubCube,
                                        unsigned int iCube,
                                        unsigned int iLit0,
                                        unsigned int iLit1,
@@ -37,13 +35,13 @@ static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan,
     if ( fAdd )
     {
         ret = Fxch_SCHashTableInsert( pFxchMan->pSCHashTable, pFxchMan->vCubes,
-                                      SubCubeID, iSubCube,
+                                      SubCubeID,
                                       iCube, iLit0, iLit1, fUpdate );
     }
     else
     {
         ret = Fxch_SCHashTableRemove( pFxchMan->pSCHashTable, pFxchMan->vCubes,
-                                      SubCubeID, iSubCube,
+                                      SubCubeID,
                                       iCube, iLit0, iLit1, fUpdate );
     }
 
@@ -63,25 +61,37 @@ static inline int Fxch_ManDivSingleCube( Fxch_Man_t* pFxchMan,
         fSingleCube = 1,
         fBase = 0;
 
-    if ( Vec_IntSize(vCube) < 2 )
+    if ( Vec_IntSize( vCube ) < 2 )
         return 0;
 
     Vec_IntForEachEntryStart( vCube, Lit0, i, 1)
     Vec_IntForEachEntryStart( vCube, Lit1, k, (i + 1) )
     {
+        int * pOutputID, nOnes, j, z;
         assert( Lit0 < Lit1 );
 
         Vec_IntClear( pFxchMan->vCubeFree );
         Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit0 ), 0 ) );
         Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( Abc_LitNot( Lit1 ), 1 ) );
 
+        pOutputID = Vec_IntEntryP( pFxchMan->vOutputID, iCube * pFxchMan->nSizeOutputID );
+        nOnes = 0;
+
+        for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
+            nOnes += Fxch_CountOnes( pOutputID[j] );
+
+        if ( nOnes == 0 )
+            nOnes = 1;
+
         if (fAdd)
         {
+            for ( z = 0; z < nOnes; z++ )
                 Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase );
             pFxchMan->nPairsS++;
         }
         else
         {
+            for ( z = 0; z < nOnes; z++ )
                 Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase );
             pFxchMan->nPairsS--;
         }
@@ -98,15 +108,13 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
     Vec_Int_t* vLitHashKeys = pFxchMan->vLitHashKeys,
              * vCube = Vec_WecEntry( pFxchMan->vCubes, iCube );
     int SubCubeID = 0,
-        nHashedSC = 0,
         iLit0,
         Lit0;
 
     Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
         SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 );
 
-    Fxch_ManSCAddRemove( pFxchMan,
-                         SubCubeID, nHashedSC++,
+    Fxch_ManSCAddRemove( pFxchMan, SubCubeID,
                          iCube, 0, 0,
                          (char)fAdd, (char)fUpdate );
 
@@ -115,8 +123,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
         /* 1 Lit remove */
         SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit0 );
 
-        pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
-                                                  SubCubeID, nHashedSC++,
+        pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, SubCubeID,
                                                   iCube, iLit0, 0,
                                                   (char)fAdd, (char)fUpdate );
 
@@ -130,8 +137,7 @@ static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
                 /* 2 Lit remove */
                 SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit1 );
 
-                pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
-                                                          SubCubeID, nHashedSC++,
+                pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan, SubCubeID,
                                                           iCube, iLit0, iLit1,
                                                           (char)fAdd, (char)fUpdate );
 
@@ -165,14 +171,20 @@ 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->vDivWeights = Vec_FltAlloc( 1000 );
-    pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 );
-    pFxchMan->vCubeFree = Vec_IntAlloc( 100 );
-    pFxchMan->vDiv = Vec_IntAlloc( 100 );
+    pFxchMan->nCubesInit = Vec_WecSize( vCubes );
+
+    pFxchMan->pDivHash = Hsh_VecManStart( 1024 );
+    pFxchMan->vDivWeights = Vec_FltAlloc( 1024 );
+    pFxchMan->vDivCubePairs = Vec_WecAlloc( 1024 );
+
+    pFxchMan->vCubeFree = Vec_IntAlloc( 4 );
+    pFxchMan->vDiv = Vec_IntAlloc( 4 );
+
+    pFxchMan->vCubesS = Vec_IntAlloc( 128 );
+    pFxchMan->vPairs = Vec_IntAlloc( 128 );
+    pFxchMan->vCubesToUpdate = Vec_IntAlloc( 64 );
+    pFxchMan->vCubesToRemove = Vec_IntAlloc( 64 );
     pFxchMan->vSCC = Vec_IntAlloc( 64 );
-    pFxchMan->vCubesS = Vec_IntAlloc( 100 );
-    pFxchMan->vPairs = Vec_IntAlloc( 100 );
 
     return pFxchMan;
 }
@@ -187,11 +199,16 @@ void Fxch_ManFree( Fxch_Man_t* pFxchMan )
     Vec_QueFree( pFxchMan->vDivPrio );
     Vec_WecFree( pFxchMan->vDivCubePairs );
     Vec_IntFree( pFxchMan->vLevels );
+
     Vec_IntFree( pFxchMan->vCubeFree );
     Vec_IntFree( pFxchMan->vDiv );
-    Vec_IntFree( pFxchMan->vSCC );
+
     Vec_IntFree( pFxchMan->vCubesS );
     Vec_IntFree( pFxchMan->vPairs );
+    Vec_IntFree( pFxchMan->vCubesToUpdate );
+    Vec_IntFree( pFxchMan->vCubesToRemove );
+    Vec_IntFree( pFxchMan->vSCC );
+
     ABC_FREE( pFxchMan );
 }
 
@@ -248,22 +265,19 @@ void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan )
 void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan )
 {
     Vec_Wec_t* vCubes = pFxchMan->vCubes;
-    Vec_Int_t* vCube,
-             * vCubeLinks;
+    Vec_Int_t* vCube;
     int iCube,
         nTotalHashed = 0;
 
-    vCubeLinks = Vec_IntAlloc( Vec_WecSize( vCubes ) + 1 );
     Vec_WecForEachLevel( vCubes, vCube, iCube )
     {
         int nLits = Vec_IntSize( vCube ) - 1,
             nSubCubes = nLits <= 2? nLits + 1: ( nLits * nLits + nLits ) / 2;
 
-        Vec_IntPush( vCubeLinks, ( nTotalHashed + 1 ) );
         nTotalHashed += nSubCubes + 1;
     }
 
-    pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, vCubeLinks, nTotalHashed );
+    pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, nTotalHashed );
 }
 
 void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan )
@@ -364,56 +378,135 @@ static inline void Fxch_ManExtractDivFromCube( Fxch_Man_t* pFxchMan,
 
         Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
         Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+        Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 );
 
         pFxchMan->nLits--;
     }
 }
 
 /* Extract divisor from cube pairs */
-static inline int Fxch_ManExtractDivFromCubePairs( Fxch_Man_t* pFxchMan,
+static inline void Fxch_ManExtractDivFromCubePairs( Fxch_Man_t* pFxchMan,
                                                    const int iVarNew )
 {
     /* For each pair (Ci, Cj) */
-    int k = 0,
-        iCube0, iCube1, i;
+    int iCube0, iCube1, i;
 
-    Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ),
-             * vLitN = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 1 );
 
     Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
     {
-        int RetValue,  
+        int j, Lit,
+            RetValue,  
             fCompl = 0;
+        int * pOutputID0, * pOutputID1;
 
-        Vec_Int_t* vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ),
-                 * vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 );
+        Vec_Int_t* vCube = NULL,
+                 * vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ),
+                 * vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ),
+                 * vCube0Copy = Vec_IntDup( vCube0 ),
+                 * vCube1Copy = Vec_IntDup( vCube1 );
 
-        RetValue  = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl );
+        RetValue  = Fxch_DivRemoveLits( vCube0Copy, vCube1Copy, pFxchMan->vDiv, &fCompl );
 
         assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) );
 
         pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2;
 
-        /* Remove second cube */
+        /* Identify type of Extraction */
+        pOutputID0 = Vec_IntEntryP( pFxchMan->vOutputID, iCube0 * pFxchMan->nSizeOutputID );
+        pOutputID1 = Vec_IntEntryP( pFxchMan->vOutputID, iCube1 * pFxchMan->nSizeOutputID );
+        RetValue = 1;
+        for ( j = 0; j < pFxchMan->nSizeOutputID && RetValue; j++ )
+            RetValue = ( pOutputID0[j] == pOutputID1[j] );
+
+        /* Exact Extractraion */
+        if ( RetValue )
+        {
+            Vec_IntClear( vCube0 );
+            Vec_IntAppend( vCube0, vCube0Copy );
+            vCube = vCube0;
+
+            Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 );
             Vec_IntClear( vCube1 );
-        Vec_IntWriteEntry( pFxchMan->vPairs, k++, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+
+            /* Update Lit -> Cube mapping */
+            Vec_IntForEachEntry( pFxchMan->vDiv, Lit, j )
+            {
+                Vec_IntRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit ) ), 
+                               Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+                Vec_IntRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit ) ) ), 
+                               Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+            }
+
+        }
+        /* Unexact Extraction */
+        else
+        {
+            for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
+                pFxchMan->pTempOutputID[j] = ( pOutputID0[j] & pOutputID1[j] );
+
+            /* Create new cube */
+            vCube = Vec_WecPushLevel( pFxchMan->vCubes );
+            Vec_IntAppend( vCube, vCube0Copy );
+            Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID ); 
+            Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
+
+            /* Update Lit -> Cube mapping */
+            Vec_IntForEachEntryStart( vCube, Lit, j, 1 )
+                Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
+
+            /*********************************************************/
+            RetValue = 0;
+            for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
+            {
+                pFxchMan->pTempOutputID[j] = pOutputID0[j];
+                RetValue |= ( pOutputID0[j] & ~( pOutputID1[j] ) );
+                pOutputID0[j] &= ~( pOutputID1[j] );
+            }
+
+            if ( RetValue != 0 )
+                Vec_IntPush( pFxchMan->vCubesToUpdate, iCube0 );
+            else
+                Vec_IntClear( vCube0 );
+
+            /*********************************************************/
+            RetValue = 0;
+            for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
+            {
+                RetValue |= ( pOutputID1[j] & ~( pFxchMan->pTempOutputID[j] ) );
+                pOutputID1[j] &= ~( pFxchMan->pTempOutputID[j] );
+            }
+
+            if ( RetValue != 0 )
+                Vec_IntPush( pFxchMan->vCubesToUpdate, iCube1 );
+            else
+                Vec_IntClear( vCube1 );
+
+        }
+        Vec_IntFree( vCube0Copy );
+        Vec_IntFree( vCube1Copy );
 
         if ( iVarNew )
         {
+            Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ),
+                     * vLitN = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 1 );
+ 
+            assert( vCube );
             if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl )
             {
-                Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) );
-                Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+                Vec_IntPush( vCube, Abc_Var2Lit( iVarNew, 1 ) );
+                Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
+                Vec_IntSort( vLitN, 0 );
             }
             else
             {
-                Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
-                Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+                Vec_IntPush( vCube, Abc_Var2Lit( iVarNew, 0 ) );
+                Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube ) );
+                Vec_IntSort( vLitP, 0 );
             }
         }
     }
 
-    return k;
+    return;
 }
 
 static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
@@ -421,7 +514,8 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
                                       int Lit1 )
 {
     int Level,
-        iVarNew;
+        iVarNew, 
+        j;
     Vec_Int_t* vCube0,
              * vCube1;
  
@@ -429,6 +523,10 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
     iVarNew = pFxchMan->nVars;
     pFxchMan->nVars++;
 
+    /* Clear temporary outputID vector */
+    for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
+        pFxchMan->pTempOutputID[j] = 0;
+    
     /* Create new Lit hash keys */
     Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
     Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
@@ -436,6 +534,7 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
     /* Create new Cube */
     vCube0 = Vec_WecPushLevel( pFxchMan->vCubes );
     Vec_IntPush( vCube0, iVarNew );
+    Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID );
 
     if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
     {
@@ -448,12 +547,27 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
     }
     else
     {
+        int i;
+        int Lit;
+
         vCube1 = Vec_WecPushLevel( pFxchMan->vCubes );
-        vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 );
         Vec_IntPush( vCube1, iVarNew );
+        Vec_IntPushArray( pFxchMan->vOutputID, pFxchMan->pTempOutputID, pFxchMan->nSizeOutputID );
+
+        vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 );
         Fxch_DivSepareteCubes( pFxchMan->vDiv, vCube0, vCube1 );
         Level = 2 + Abc_MaxInt( Fxch_ManComputeLevelCube( pFxchMan, vCube0 ),
                                 Fxch_ManComputeLevelCube( pFxchMan, vCube1 ) );
+
+        Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+        Vec_IntPush( pFxchMan->vCubesToUpdate, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) );
+
+        /* Update Lit -> Cube mapping */
+        Vec_IntForEachEntryStart( vCube0, Lit, i, 1 )
+            Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+
+        Vec_IntForEachEntryStart( vCube1, Lit, i, 1 )
+            Vec_WecPush( pFxchMan->vLits, Lit, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) );
     }
     assert( Vec_IntSize( pFxchMan->vLevels ) == iVarNew );
     Vec_IntPush( pFxchMan->vLevels, Level );
@@ -470,7 +584,7 @@ static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan,
 void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
                      int iDiv )
 {
-    int i, k, iCube0, iCube1,
+    int i, iCube0, iCube1,
         Lit0 = -1,
         Lit1 = -1,
         iVarNew;
@@ -519,89 +633,128 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
 
     /* subtract cost of single-cube divisors */
     Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
-        Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */
-
-    Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
-        Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1), /* remove (fAdd = 0) - fUpdate = 1 */
-        Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */
+    {
+        Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1);
 
-    /* subtract cost of double-cube divisors */
-    Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
-        if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
-            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */
+        if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 )
+            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 );
+    }
 
     Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
-        if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
-            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */
+    {
+        Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1);
+
+        if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 )
+            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 );
+    }
 
-    k = 0;
+    Vec_IntClear( pFxchMan->vCubesToUpdate );
     if ( Fxch_DivIsNotConstant1( pFxchMan->vDiv ) )
     {
         iVarNew = Fxch_ManCreateCube( pFxchMan, Lit0, Lit1 );
         Fxch_ManExtractDivFromCube( pFxchMan, Lit0, Lit1, iVarNew );
-        k = Fxch_ManExtractDivFromCubePairs( pFxchMan, iVarNew );
+        Fxch_ManExtractDivFromCubePairs( pFxchMan, iVarNew );
     }
     else
-        k = Fxch_ManExtractDivFromCubePairs( pFxchMan, 0 );
+        Fxch_ManExtractDivFromCubePairs( pFxchMan, 0 );
  
-    assert( k == Vec_IntSize( pFxchMan->vPairs ) / 2 );
-    Vec_IntShrink( pFxchMan->vPairs, k );
+    assert( Vec_IntSize( pFxchMan->vCubesToUpdate ) );
 
-    /* Add cost of single-cube divisors */
-    Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
-        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+    /* Add cost */
+    Vec_IntForEachEntry( pFxchMan->vCubesToUpdate, iCube0, i )
+    {
+        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 );
 
-    Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
-        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+        if ( Vec_WecEntryEntry( pFxchMan->vCubes, iCube0, 0 ) == 0 )
+            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 );
+    }
 
-    /* Add cost of double-cube divisors */
-    Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
-        if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
-            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+    /* Deal with SCC */
+    if ( Vec_IntSize( pFxchMan->vSCC ) && pFxchMan->nExtDivs < 17 )
+    {
+        Vec_IntUniqifyPairs( pFxchMan->vSCC );
+        assert( Vec_IntSize( pFxchMan->vSCC ) % 2 == 0 );
 
-    Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
-        if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
-            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+        Vec_IntForEachEntryDouble( pFxchMan->vSCC, iCube0, iCube1, i )
+        {
+            int j, RetValue = 1;
+            int* pOutputID0 = Vec_IntEntryP( pFxchMan->vOutputID, iCube0 * pFxchMan->nSizeOutputID );
+            int* pOutputID1 = Vec_IntEntryP( pFxchMan->vOutputID, iCube1 * pFxchMan->nSizeOutputID );
+            vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 );
+            vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 );
 
-    /* Deal with SCC */
-    if ( Vec_IntSize( pFxchMan->vSCC ) )
+            if ( !Vec_WecIntHasMark( vCube0 ) )
             {
-        Vec_IntUniqify( pFxchMan->vSCC );
-        Vec_IntForEachEntry( pFxchMan->vSCC, iCube0, i )
-            if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+                Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1 );
+                Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 );
+                Vec_WecIntSetMark( vCube0 );
+            }
+
+            if ( !Vec_WecIntHasMark( vCube1 ) )
             {
-                Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */
-                vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ),
-                Vec_IntClear( vCube0 );
+                Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1 );
+                Fxch_ManDivDoubleCube( pFxchMan, iCube1, 0, 1 );
+                Vec_WecIntSetMark( vCube1 );
             }
 
-        Vec_IntClear( pFxchMan->vSCC );
+            if ( Vec_IntSize( vCube0 ) == Vec_IntSize( vCube1 ) )
+            {
+                for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
+                {
+                    pOutputID1[j] |= pOutputID0[j];
+                    pOutputID0[j] = 0;
+                }
+                Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) );
+                Vec_WecIntXorMark( vCube0 );
+                continue;
             }
 
+            for ( j = 0; j < pFxchMan->nSizeOutputID && RetValue; j++ )
+                RetValue = ( pOutputID0[j] == pOutputID1[j] );
 
-    /* If it's a double-cube devisor add its cost */
-    if ( Vec_IntSize( pFxchMan->vDiv ) > 2 )
+            if ( RetValue )
+            {
+                Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) );
+                Vec_WecIntXorMark( vCube0 );
+            }
+            else
+            {
+                RetValue = 0;
+                for ( j = 0; j < pFxchMan->nSizeOutputID; j++ )
                 {
-        iCube0 = Vec_WecSize( pFxchMan->vCubes ) - 2;
-        iCube1 = Vec_WecSize( pFxchMan->vCubes ) - 1;
+                    RetValue |= ( pOutputID0[j] & ~( pOutputID1[j] ) );
+                    pOutputID0[j] &= ~( pOutputID1[j] );
+                }
 
-        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 );  /* fAdd = 1 - fUpdate = 1 */
-        Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 );  /* fAdd = 1 - fUpdate = 1 */
+                if ( RetValue == 0 )
+                {
+                    Vec_IntClear( Vec_WecEntry( pFxchMan->vCubes, iCube0 ) );
+                    Vec_WecIntXorMark( vCube0 );
+                }
+            }
+        }
 
+        Vec_IntForEachEntryDouble( pFxchMan->vSCC, iCube0, iCube1, i )
+        {
             vCube0 = Vec_WecEntry( pFxchMan->vCubes, iCube0 );
-        Vec_IntForEachEntryStart( vCube0, Lit0, i, 1 )
-            Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
-
             vCube1 = Vec_WecEntry( pFxchMan->vCubes, iCube1 );
-        Vec_IntForEachEntryStart( vCube1, Lit0, i, 1 )
-            Vec_WecPush( pFxchMan->vLits, Lit0, Vec_WecLevelId( pFxchMan->vCubes, vCube1 ) );
+
+            if ( Vec_WecIntHasMark( vCube0 ) )
+            {
+                Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 );
+                Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 );
+                Vec_WecIntXorMark( vCube0 );
             }
 
-    /* remove these cubes from the lit array of the divisor */
-    Vec_IntForEachEntry( pFxchMan->vDiv, Lit0, i )
+            if ( Vec_WecIntHasMark( vCube1 ) )
             {
-        Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit0 ) ), pFxchMan->vPairs );
-        Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit0 ) ) ), pFxchMan->vPairs );
+                Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 );
+                Fxch_ManDivDoubleCube( pFxchMan, iCube1, 1, 1 );
+                Vec_WecIntXorMark( vCube1 );
+            }
+        }
+
+        Vec_IntClear( pFxchMan->vSCC );
     }
 
     pFxchMan->nExtDivs++;

src/opt/fxch/FxchSCHashTable.c

@@ -19,11 +19,6 @@
 
 ABC_NAMESPACE_IMPL_START
 
-//#ifdef _WIN32
-typedef unsigned int uint32_t;
-typedef unsigned char uint8_t;
-//#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -92,7 +87,6 @@ static inline void MurmurHash3_x86_32 ( const void* key,
 }
 
 Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan,
-                                            Vec_Int_t* vCubeLinks,
                                             int nEntries )
 {
     Fxch_SCHashTable_t* pSCHashTable = ABC_CALLOC( Fxch_SCHashTable_t, 1 );
@@ -101,7 +95,6 @@ Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan,
 
     pSCHashTable->pFxchMan = pFxchMan;
     pSCHashTable->SizeMask = (1 << nBits) - 1;
-    pSCHashTable->vCubeLinks = vCubeLinks;
     pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 );
 
     return pSCHashTable;
@@ -109,7 +102,6 @@ Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan,
 
 void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* pSCHashTable )
 {
-    Vec_IntFree( pSCHashTable->vCubeLinks );
     Vec_IntErase( &pSCHashTable->vSubCube0 );
     Vec_IntErase( &pSCHashTable->vSubCube1 );
     ABC_FREE( pSCHashTable->pBins );
@@ -122,49 +114,6 @@ static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableBin( Fxch_SCHashTable_t*
     return pSCHashTable->pBins + (SubCubeID & pSCHashTable->SizeMask);
 }
 
-static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableEntry( Fxch_SCHashTable_t* pSCHashTable,
-                                                               unsigned int iEntry )
-{
-    if ( ( iEntry > 0 ) && ( iEntry < ( pSCHashTable->SizeMask + 1 ) ) )
-        return pSCHashTable->pBins + iEntry;
-
-    return NULL;
-}
-
-static inline void Fxch_SCHashTableInsertLink( Fxch_SCHashTable_t* pSCHashTable,
-                                               unsigned int iEntry0,
-                                               unsigned int iEntry1 )
-{
-    Fxch_SCHashTable_Entry_t* pEntry0 = Fxch_SCHashTableEntry( pSCHashTable, iEntry0 ),
-                            * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ),
-                            * pEntry0Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry0->iNext );
-
-    assert( pEntry0Next->iPrev == iEntry0 );
-
-    pEntry1->iNext = pEntry0->iNext;
-    pEntry0->iNext = iEntry1;
-    pEntry1->iPrev = iEntry0;
-    pEntry0Next->iPrev = iEntry1;
-}
-
-static inline void Fxch_SCHashTableRemoveLink( Fxch_SCHashTable_t* pSCHashTable,
-                                               int iEntry0,
-                                               int iEntry1 )
-{
-    Fxch_SCHashTable_Entry_t* pEntry0 = Fxch_SCHashTableEntry( pSCHashTable, iEntry0 ),
-                            * pEntry1 = Fxch_SCHashTableEntry( pSCHashTable, iEntry1 ),
-                            * pEntry1Next = Fxch_SCHashTableEntry( pSCHashTable, pEntry1->iNext );
-
-    assert( (int)pEntry0->iNext == iEntry1 );
-    assert( (int)pEntry1->iPrev == iEntry0 );
-    assert( (int)pEntry1Next->iPrev == iEntry1 );
-
-    pEntry0->iNext = pEntry1->iNext;
-    pEntry1->iNext = 0;
-    pEntry1Next->iPrev = pEntry1->iPrev;
-    pEntry1->iPrev = 0;
-}
-
 static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable,
                                                 Vec_Wec_t* vCubes,
                                                 Fxch_SubCube_t* pSCData0,
@@ -173,12 +122,22 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable
     Vec_Int_t* vCube0 = Vec_WecEntry( vCubes, pSCData0->iCube ),
              * vCube1 = Vec_WecEntry( vCubes, pSCData1->iCube );
 
+    int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pSCData0->iCube * pSCHashTable->pFxchMan->nSizeOutputID ),
+       * pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pSCData1->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
+    int i, Result = 0;
+
     if ( !Vec_IntSize( vCube0 ) ||
          !Vec_IntSize( vCube1 ) ||
          Vec_IntEntry( vCube0, 0 ) != Vec_IntEntry( vCube1, 0 ) ||
          pSCData0->Id != pSCData1->Id )
         return 0;
 
+    for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID && Result == 0; i++ )
+        Result = ( pOutputID0[i] & pOutputID1[i] );
+
+    if ( Result == 0 )
+        return 0;
+
     Vec_IntClear( &pSCHashTable->vSubCube0 );
     Vec_IntClear( &pSCHashTable->vSubCube1 );
 
@@ -189,7 +148,6 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable
            Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ) )
         return 0;
 
-
     if ( pSCData0->iLit0 > 0 )
         Vec_IntAppendSkip( &pSCHashTable->vSubCube0, vCube0, pSCData0->iLit0 );
     else
@@ -200,7 +158,6 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable
     else
         Vec_IntAppend( &pSCHashTable->vSubCube1, vCube1 );
 
-
     if ( pSCData0->iLit1 > 0)
         Vec_IntDrop( &pSCHashTable->vSubCube0,
                        pSCData0->iLit0 < pSCData0->iLit1 ? pSCData0->iLit1 - 1 : pSCData0->iLit1 );
@@ -209,167 +166,169 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable
         Vec_IntDrop( &pSCHashTable->vSubCube1,
                        pSCData1->iLit0 < pSCData1->iLit1 ? pSCData1->iLit1 - 1 : pSCData1->iLit1 );
 
-    Vec_IntDrop( &pSCHashTable->vSubCube0, 0 );
-    Vec_IntDrop( &pSCHashTable->vSubCube1, 0 );
-
     return Vec_IntEqual( &pSCHashTable->vSubCube0, &pSCHashTable->vSubCube1 );
 }
 
 int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
                             Vec_Wec_t* vCubes,
-                            unsigned int SubCubeID,
-                            unsigned int iSubCube,
-                            unsigned int iCube,
-                            unsigned int iLit0,
-                            unsigned int iLit1,
+                            uint32_t SubCubeID,
+                            uint32_t iCube,
+                            uint32_t iLit0,
+                            uint32_t iLit1,
                             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;
+    int iNewEntry;
+    int Pairs = 0;
+    uint32_t BinID;
+    Fxch_SCHashTable_Entry_t* pBin;
+    Fxch_SubCube_t* pNewEntry;
+    int iEntry;
 
     MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
-
-    iNewEntry = ( unsigned int )( Vec_IntEntry( pSCHashTable->vCubeLinks, iCube ) ) + iSubCube;
     pBin = Fxch_SCHashTableBin( pSCHashTable, BinID );
-    pNewEntry = Fxch_SCHashTableEntry( pSCHashTable, iNewEntry );
     
-    assert( pNewEntry->Used == 0 );
-
-    pNewEntry->SCData.Id = SubCubeID;
-    pNewEntry->SCData.iCube = iCube;
-    pNewEntry->SCData.iLit0 = iLit0;
-    pNewEntry->SCData.iLit1 = iLit1;
+    if ( pBin->vSCData == NULL )
+    {
+        pBin->vSCData = ABC_CALLOC( Fxch_SubCube_t, 16 );
+        pBin->Size = 0;
+        pBin->Cap = 16;
+    }
+    else if ( pBin->Size == pBin->Cap )
+    {
+        pBin->Cap = 2 * pBin->Size;
+        pBin->vSCData = ABC_REALLOC( Fxch_SubCube_t, pBin->vSCData, pBin->Cap );
+    }
 
-    pNewEntry->Used = 1;
+    iNewEntry = pBin->Size++;
+    pBin->vSCData[iNewEntry].Id = SubCubeID;
+    pBin->vSCData[iNewEntry].iCube = iCube;
+    pBin->vSCData[iNewEntry].iLit0 = iLit0;
+    pBin->vSCData[iNewEntry].iLit1 = iLit1;
     pSCHashTable->nEntries++;
-    if ( pBin->iTable == 0 )
-    {
-        pBin->iTable = iNewEntry;
-        pNewEntry->iNext = iNewEntry;
-        pNewEntry->iPrev = iNewEntry;
+
+    if ( pBin->Size == 1 )
         return 0;
-    }
 
-    for ( iEntry = pBin->iTable; iEntry != pBin->iTable || fStart; iEntry = pEntry->iNext, fStart = 0 )
+    pNewEntry = &( pBin->vSCData[iNewEntry] );
+    for ( iEntry = 0; iEntry < (int)pBin->Size - 1; iEntry++ )
     {
+        Fxch_SubCube_t* pEntry = &( pBin->vSCData[iEntry] );
+        int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
+        int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNewEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
+        int Result = 0;
         int Base;
-        int iNewDiv;
-
-        pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry );
+        int iNewDiv, i, z;
 
-        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) )
+        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNewEntry ) )
             continue;
 
-        if ( ( pEntry->SCData.iLit0 == 0 ) || ( pNewEntry->SCData.iLit0 == 0 ) )
+        if ( ( pEntry->iLit0 == 0 ) || ( pNewEntry->iLit0 == 0 ) )
         {
-            Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->SCData.iCube ),
-                     * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->SCData.iCube );
+            Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->iCube ),
+                     * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pNewEntry->iCube );
  
             if ( Vec_IntSize( vCube0 ) > Vec_IntSize( vCube1 ) )
-                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->SCData.iCube );
+            {
+                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube );
+                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube );
+            }
             else
-                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->SCData.iCube );
+            {
+                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->iCube );
+                Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->iCube );
+            }
 
             continue;
         }
 
-        if ( pEntry->SCData.iCube < pNewEntry->SCData.iCube )
-            Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNewEntry->SCData ) );
-        else
-            Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNewEntry->SCData ), &( pEntry->SCData ) );
+        Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pEntry, pNewEntry );
 
         if ( Base < 0 )
             continue;
 
+        for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ )
+            Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] );
+
+        for ( z = 0; z < Result; z++ )
             iNewDiv = Fxch_DivAdd( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
-        Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->SCData.iCube );
-        Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->SCData.iCube );
+        Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pEntry->iCube );
+        Vec_WecPush( pSCHashTable->pFxchMan->vDivCubePairs, iNewDiv, pNewEntry->iCube );
 
         Pairs++;
     }
-    assert( iEntry == (unsigned int)( pBin->iTable ) );
-
-    pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry );
-    Fxch_SCHashTableInsertLink( pSCHashTable, pEntry->iPrev, iNewEntry );
 
     return Pairs;
 }
 
 int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
                             Vec_Wec_t* vCubes,
-                            unsigned int SubCubeID,
-                            unsigned int iSubCube,
-                            unsigned int iCube,
-                            unsigned int iLit0,
-                            unsigned int iLit1,
+                            uint32_t SubCubeID,
+                            uint32_t iCube,
+                            uint32_t iLit0,
+                            uint32_t iLit1,
                             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;
+    int iEntry;
+    int Pairs = 0;
+    uint32_t BinID;
+    Fxch_SCHashTable_Entry_t* pBin;
+    Fxch_SubCube_t* pEntry;
+    int idx;
 
     MurmurHash3_x86_32( ( void* ) &SubCubeID, sizeof( int ), 0x9747b28c, &BinID);
 
-    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 );
 
-    if ( pEntry->iNext == iEntry )
+    if ( pBin->Size == 1 )
     {
-        assert( pEntry->iPrev == iEntry );
-        pBin->iTable = 0;
-        pEntry->iNext = 0;
-        pEntry->iPrev = 0;
-        pEntry->Used = 0;
+        pBin->Size = 0;
         return 0;
     }
 
-    for ( iNextEntry = (int)pEntry->iNext; iNextEntry != (int)iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 )
+    for ( iEntry = 0; iEntry < (int)pBin->Size; iEntry++ )
+        if ( pBin->vSCData[iEntry].iCube == iCube )
+            break;
+
+    assert( ( iEntry != pBin->Size ) && ( pBin->Size != 0 ) );
+
+    pEntry = &( pBin->vSCData[iEntry] );
+    for ( idx = 0; idx < (int)pBin->Size; idx++ )
+    if ( idx != iEntry )
     {
         int Base,
             iDiv;
 
-        int i,
+        int i, z,
             iCube0,
             iCube1;
 
+        Fxch_SubCube_t* pNextEntry = &( pBin->vSCData[idx] );
         Vec_Int_t* vDivCubePairs;
+        int* pOutputID0 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
+        int* pOutputID1 = Vec_IntEntryP( pSCHashTable->pFxchMan->vOutputID, pNextEntry->iCube * pSCHashTable->pFxchMan->nSizeOutputID );
+        int Result = 0;
 
-        pNextEntry = Fxch_SCHashTableBin( pSCHashTable, iNextEntry );
-
-        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNextEntry->SCData ) )
-             || pEntry->SCData.iLit0 == 0
-             || pNextEntry->SCData.iLit0 == 0 )
+        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, pEntry, pNextEntry )
+             || pEntry->iLit0 == 0
+             || pNextEntry->iLit0 == 0 )
             continue;
 
-        if ( pNextEntry->SCData.iCube < pEntry->SCData.iCube )
-            Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pNextEntry->SCData ), &( pEntry->SCData ) );
-        else
-            Base = Fxch_DivCreate( pSCHashTable->pFxchMan, &( pEntry->SCData ), &( pNextEntry->SCData ) );
+        Base = Fxch_DivCreate( pSCHashTable->pFxchMan, pNextEntry, pEntry );
 
         if ( Base < 0 )
             continue;
 
+        for ( i = 0; i < pSCHashTable->pFxchMan->nSizeOutputID; i++ )
+            Result += Fxch_CountOnes( pOutputID0[i] & pOutputID1[i] );
+
+        for ( z = 0; z < Result; z++ )
             iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
 
         vDivCubePairs = Vec_WecEntry( pSCHashTable->pFxchMan->vDivCubePairs, iDiv );
         Vec_IntForEachEntryDouble( vDivCubePairs, iCube0, iCube1, i )
-            if ( ( iCube0 == (int)pNextEntry->SCData.iCube &&  iCube1 == (int)pEntry->SCData.iCube )  ||
-                 ( iCube0 == (int)pEntry->SCData.iCube &&  iCube1 == (int)pNextEntry->SCData.iCube ) )
+            if ( ( iCube0 == (int)pNextEntry->iCube && iCube1 == (int)pEntry->iCube )  ||
+                 ( iCube0 == (int)pEntry->iCube && iCube1 == (int)pNextEntry->iCube ) )
             {
                 Vec_IntDrop( vDivCubePairs, i+1 );
                 Vec_IntDrop( vDivCubePairs, i );
@@ -380,11 +339,9 @@ int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
         Pairs++;
     }
     
-    if ( pBin->iTable == iEntry )
-        pBin->iTable = ( pEntry->iNext != iEntry ) ? pEntry->iNext : 0;
+    memmove(pBin->vSCData + iEntry, pBin->vSCData + iEntry + 1, (pBin->Size - iEntry - 1) * sizeof(*pBin->vSCData));
+    pBin->Size -= 1;
 
-    pEntry->Used = 0;
-    Fxch_SCHashTableRemoveLink( pSCHashTable, pEntry->iPrev, iEntry );
     return Pairs;
 }
 
@@ -392,7 +349,6 @@ unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* pHashTable )
 {
     unsigned int Memory = sizeof ( Fxch_SCHashTable_t );
 
-    Memory += Vec_IntMemory( pHashTable->vCubeLinks );
     Memory += sizeof( Fxch_SubCube_t ) * ( pHashTable->SizeMask + 1 );
 
     return Memory;