Merged in boschmitt/abc/fxch_implementation (pull request #24)

Fast eXtract with Cube Hashing (FXCH) Implementation

Makefile

@@ -20,7 +20,7 @@ MODULES := \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
 	src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
 	src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \
-	src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
+	src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
 	src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
 	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \

src/base/abci/abc.c

@@ -23,6 +23,7 @@
 #include "base/main/mainInt.h"
 #include "proof/fraig/fraig.h"
 #include "opt/fxu/fxu.h"
+#include "opt/fxch/Fxch.h"
 #include "opt/cut/cut.h"
 #include "map/fpga/fpga.h"
 #include "map/if/if.h"
@@ -106,6 +107,7 @@ static int Abc_CommandRenode                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandCleanup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSweep                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFastExtract            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFxch                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEliminate              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSparsify               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -740,6 +742,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "fxch",          Abc_CommandFxch,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "eliminate",     Abc_CommandEliminate,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sparsify",      Abc_CommandSparsify,         1 );
@@ -4130,6 +4133,103 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+static int Abc_CommandFxch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_NtkFxchPerform( Abc_Ntk_t * pNtk, int nMaxDivExt, int SMode, int fVerbose, int fVeryVerbose );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+
+    int c,
+        nMaxDivExt,
+        SMode = 0,
+        fVerbose = 0,
+        fVeryVerbose = 0;
+
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "NSvwh")) != EOF )
+    {
+        switch (c)
+        {
+            case 'N':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                nMaxDivExt = atoi( argv[globalUtilOptind] );
+                globalUtilOptind++;
+
+                if ( nMaxDivExt < 0 )
+                    goto usage;
+                break;
+
+            case 'S':
+                SMode ^= 1;
+                break;
+
+            case 'v':
+                fVerbose ^= 1;
+                break;
+
+            case 'w':
+                fVeryVerbose ^= 1;
+                break;
+
+            case 'h':
+                goto usage;
+                break;
+
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkNodeNum( pNtk ) == 0 )
+    {
+        Abc_Print( -1, "The network does not have internal nodes.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic( pNtk ) )
+    {
+        Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\" or \"if\").\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsSopLogic( pNtk ) )
+    {
+        Abc_Print( -1, "Fast extract can only be applied to a logic network with SOP local functions (run \"bdd; sop\").\n" );
+        return 1;
+    }
+
+    Abc_NtkFxchPerform( pNtk, nMaxDivExt, SMode, fVerbose, fVeryVerbose );
+
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: fxch [-N <num>] [-vwh]\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-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");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);

src/base/pla/module.make

 SRC +=    src/base/pla/plaCom.c \
     src/base/pla/plaHash.c \
-    src/base/pla/plaFxch.c \
     src/base/pla/plaMan.c \
     src/base/pla/plaMerge.c \
     src/base/pla/plaSimple.c \

src/base/pla/pla.h

@@ -268,8 +268,7 @@ static inline void Pla_ManPrintStats( Pla_Man_t * p, int fVerbose )
 }
 
 
-/*=== plaFxch.c ========================================================*/
-extern int                 Pla_ManPerformFxch( Pla_Man_t * p );
+
 /*=== plaHash.c ========================================================*/
 extern int                 Pla_ManHashDist1NumTest( Pla_Man_t * p );
 extern void                Pla_ManComputeDist1Test( Pla_Man_t * p );
@@ -296,4 +295,3 @@ ABC_NAMESPACE_HEADER_END
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-

src/base/pla/plaCom.c

@@ -488,7 +488,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Pla_ManFxPerformSimple( nVars );
     //Pla_ManConvertFromBits( p );
     //Pla_ManConvertToBits( p );
-    Pla_ManPerformFxch( p );
+    //Pla_ManPerformFxch( p );
     return 0;
 usage:
     Abc_Print( -2, "usage: |test [-N num] [-vh]\n" );
@@ -505,4 +505,3 @@ usage:
 
 
 ABC_NAMESPACE_IMPL_END
-

src/opt/fxch/Fxch.c

+/**CFile****************************************************************
+
+  FileName    [ Fxch.c ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ The entrance into the fast extract module. ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************/
+
+#include "Fxch.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [ Performs fast extract with cube hashing on a set
+                of covers. ]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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, SMode );
+
+    TempTime = Abc_Clock();
+    Fxch_ManMapLiteralsIntoCubes( pFxchMan, ObjIdMax );
+    Fxch_ManGenerateLitHashKeys( pFxchMan );
+    Fxch_ManComputeLevel( pFxchMan );
+    Fxch_ManSCHashTablesInit( pFxchMan );
+    Fxch_ManDivCreate( pFxchMan );
+    pFxchMan->timeInit = Abc_Clock() - TempTime;
+
+    if ( fVeryVerbose )
+        Fxch_ManPrintDivs( pFxchMan );
+
+    if ( fVerbose )
+        Fxch_ManPrintStats( pFxchMan );
+
+    TempTime = Abc_Clock();
+    for ( int i = 0; i < nMaxDivExt && Vec_QueTopPriority( pFxchMan->vDivPrio ) > 0.0; i++ )
+    {
+        int iDiv = Vec_QuePop( pFxchMan->vDivPrio );
+
+        if ( fVeryVerbose )
+            Fxch_DivPrint( pFxchMan, iDiv );
+
+        Fxch_ManUpdate( pFxchMan, iDiv );
+    }
+    pFxchMan->timeExt = Abc_Clock() - TempTime;
+
+    if ( fVerbose )
+    {
+        Fxch_ManPrintStats( pFxchMan );
+        Abc_PrintTime( 1, "\n[FXCH] Elapsed Time", pFxchMan->timeInit + pFxchMan->timeExt );
+        Abc_PrintTime( 1, "[FXCH]    +-> Init", pFxchMan->timeInit );
+        Abc_PrintTime( 1, "[FXCH]    +-> Extr", pFxchMan->timeExt );
+    }
+
+    Fxch_ManSCHashTablesFree( pFxchMan );
+    Fxch_ManFree( pFxchMan );
+    Vec_WecRemoveEmpty( vCubes );
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Retrives the necessary information for the fast extract
+                with cube hashing. ]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk,
+                        int nMaxDivExt,
+                        int SMode,
+                        int fVerbose,
+                        int fVeryVerbose )
+{
+    Vec_Wec_t* vCubes;
+
+    assert( Abc_NtkIsSopLogic( pNtk ) );
+
+    if ( !Abc_NtkFxCheck( pNtk ) )
+    {
+        printf( "Abc_NtkFxchPerform(): Nodes have duplicated fanins. FXCH is not performed.\n" );
+        return 0;
+    }
+
+    vCubes = Abc_NtkFxRetrieve( pNtk );
+    if ( Fxch_FastExtract( vCubes, Abc_NtkObjNumMax( pNtk ), nMaxDivExt, SMode, fVerbose, fVeryVerbose ) > 0 )
+    {
+        Abc_NtkFxInsert( pNtk, vCubes );
+        Vec_WecFree( vCubes );
+
+        if ( !Abc_NtkCheck( pNtk ) )
+            printf( "Abc_NtkFxchPerform(): The network check has failed.\n" );
+
+        return 1;
+    }
+    else
+        printf( "Warning: The network has not been changed by \"fxch\".\n" );
+
+    Vec_WecFree( vCubes );
+
+    return 0;
+}
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END

src/opt/fxch/Fxch.h

+/**CFile****************************************************************
+
+  FileName    [ Fxch.h ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ External declarations of fast extract with cube hashing. ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************/
+
+#ifndef ABC__opt__fxch__fxch_h
+#define ABC__opt__fxch__fxch_h
+
+#include "base/abc/abc.h"
+
+#include "misc/vec/vecHsh.h"
+#include "misc/vec/vecQue.h"
+#include "misc/vec/vecVec.h"
+#include "misc/vec/vecWec.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                    TYPEDEF DECLARATIONS                          ///
+////////////////////////////////////////////////////////////////////////
+typedef struct Fxch_Man_t_               Fxch_Man_t;
+typedef struct Fxch_SubCube_t_           Fxch_SubCube_t;
+typedef struct Fxch_SCHashTable_t_       Fxch_SCHashTable_t;
+typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t;
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURES DEFINITIONS                        ///
+////////////////////////////////////////////////////////////////////////
+/* Sub-Cube Structure
+ *
+ *   In the context of this program, a sub-cube is a cube derived from 
+ *   another cube by removing one or two literals. Since a cube is represented
+ *   as a vector of literals, one might think that a sub-cube would also be 
+ *   represented in the same way. However, in order to same memory, we only 
+ *   store a sub-cube identifier and the data necessary to generate the sub-cube:
+ *        - The index number of the orignal cube in the cover. (iCube)
+ *        - Identifiers of which literal(s) was(were) removed. (iLit0, iLit1)
+ *
+ *   The sub-cube identifier is generated by adding the unique identifiers of 
+ *   its literals. 
+ *
+ */
+struct Fxch_SubCube_t_
+{
+    unsigned int Id,          
+                 iCube;      
+    unsigned int 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;
+};
+
+struct Fxch_SCHashTable_t_
+{
+    Fxch_Man_t* pFxchMan;
+    /* Internal data */
+    Fxch_SCHashTable_Entry_t* pBins;
+    unsigned int nEntries,
+                 SizeMask;
+    Vec_Int_t*   vCubeLinks;
+
+    /* Temporary data */
+    Vec_Int_t    vSubCube0;
+    Vec_Int_t    vSubCube1;
+};
+
+struct Fxch_Man_t_
+{
+    /* user's data */
+    Vec_Wec_t* vCubes;
+    int LitCountMax;
+
+    /* internal data */
+    Fxch_SCHashTable_t* pSCHashTable;
+
+    Vec_Wec_t*    vLits;        /* lit -> cube */
+    Vec_Int_t*    vLitCount;    /* literal counts (currently not used) */
+    Vec_Int_t*    vLitHashKeys; /* Literal hash keys used to generate subcube hash */
+
+    Hsh_VecMan_t* pDivHash;
+    Vec_Flt_t*    vDivWeights;   /* divisor weights */
+    Vec_Que_t*    vDivPrio;      /* priority queue for divisors by weight */
+    Vec_Wec_t*    vDivCubePairs; /* cube pairs for each div */
+
+    Vec_Int_t*    vLevels;       /* variable levels */
+
+    // 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
+
+    /* Config */
+    char    SMode;        /* Saving Memory mode */
+
+    /* Statistics */
+    abctime timeInit;   /* Initialization time */
+    abctime timeExt;    /* Extraction time */
+    int     nVars;      // original problem variables
+    int     nLits;      // the number of SOP literals
+    int     nPairsS;    // number of lit pairs
+    int     nPairsD;    // number of cube pairs
+    int     nExtDivs;   /* Number of extracted divisor */
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+/* The following functions are from abcFx.c
+ * They are use in order to retrive SOP information for fast_extract
+ * Since I want an implementation that change only the core part of
+ * the algorithm I'm using this */
+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 );
+
+/*===== 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 );
+
+/*===== FxchDiv.c ====================================================================================================*/
+int  Fxch_DivCreate( Fxch_Man_t* pFxchMan,  Fxch_SubCube_t* pSubCube0, Fxch_SubCube_t* pSubCube1 );
+int  Fxch_DivAdd( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase );
+int  Fxch_DivRemove( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase );
+void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube1 );
+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 );
+void  Fxch_ManFree( Fxch_Man_t* pFxchMan );
+void  Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, int nVars );
+void  Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan );
+void  Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan );
+void  Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan );
+void  Fxch_ManDivCreate( Fxch_Man_t* pFxchMan );
+int   Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeFree );
+int   Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan, Vec_Int_t* vCube );
+void  Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan );
+void  Fxch_ManUpdate( Fxch_Man_t* pFxchMan, int iDiv );
+void  Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan );
+void  Fxch_ManPrintStats( Fxch_Man_t* pFxchMan );
+
+static inline Vec_Int_t* Fxch_ManGetCube( Fxch_Man_t* pFxchMan,
+                                          int iCube )
+{
+    return Vec_WecEntry( pFxchMan->vCubes, iCube );
+}
+
+static inline int Fxch_ManGetLit( Fxch_Man_t* pFxchMan,
+                                  int iCube,
+                                  int iLit )
+{
+    return Vec_IntEntry( Vec_WecEntry(pFxchMan->vCubes, iCube), iLit );
+}
+
+/*===== FxchSCHashTable.c ============================================*/
+Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeLinks, 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,
+                            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,
+                            char fUpdate );
+
+unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* );
+void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/fxch/FxchDiv.c

+/**CFile****************************************************************************************************************
+
+  FileName    [ FxchDiv.c ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ Divisor handling functions ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************************************************************/
+
+#include "Fxch.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+// FUNCTION DEFINITIONS
+////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
+static inline int Fxch_DivNormalize( Vec_Int_t* vCubeFree )
+{
+    int * L = Vec_IntArray(vCubeFree);
+    int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1;
+    assert( Vec_IntSize(vCubeFree) == 4 );
+    if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars
+    {
+        if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) )
+            return -1;
+        LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]);
+        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) )
+        {
+            assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) );
+            LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]);
+        }
+        else
+        {
+            assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) );
+            assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) );
+            LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]);
+        }
+    }
+    else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) )
+    {
+        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) )
+            return -1;
+        LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]);
+        if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) )
+            LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]);
+        else
+            LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]);
+    }
+    else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) )
+    {
+        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) )
+            return -1;
+        LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]);
+        if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) )
+            LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]);
+        else
+            LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]);
+    }
+    else
+        return -1;
+    assert( LitA0 == Abc_LitNot(LitB0) );
+    if ( Abc_LitIsCompl(LitA0) )
+    {
+        ABC_SWAP( int, LitA0, LitB0 );
+        ABC_SWAP( int, LitA1, LitB1 );
+    }
+    assert( !Abc_LitIsCompl(LitA0) );
+    if ( Abc_LitIsCompl(LitA1) )
+    {
+        LitA1 = Abc_LitNot(LitA1);
+        LitB1 = Abc_LitNot(LitB1);
+        RetValue = 1;
+    }
+    assert( !Abc_LitIsCompl(LitA1) );
+    // arrange literals in such as a way that
+    // - the first two literals are control literals from different cubes
+    // - the third literal is non-complented data input
+    // - the forth literal is possibly complemented data input
+    L[0] = Abc_Var2Lit( LitA0, 0 );
+    L[1] = Abc_Var2Lit( LitB0, 1 );
+    L[2] = Abc_Var2Lit( LitA1, 0 );
+    L[3] = Abc_Var2Lit( LitB1, 1 );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Creates a Divisor. ]
+
+  Description [ This functions receive as input two sub-cubes and creates
+                a divisor using their information. The divisor is stored 
+                in vCubeFree vector of the pFxchMan structure.
+                
+                It returns the base value, which is the number of elements
+                that the cubes pair used to generate the devisor have in
+                common. ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
+                    Fxch_SubCube_t* pSubCube0,
+                    Fxch_SubCube_t* pSubCube1 )
+{
+    int Base = 0;
+
+    Vec_IntClear( pFxchMan->vCubeFree );
+
+    int SC0_Lit0,
+        SC0_Lit1,
+        SC1_Lit0,
+        SC1_Lit1;
+
+    SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
+    SC0_Lit1 = 0;
+    SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
+    SC1_Lit1 = 0;
+
+    if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
+    {
+        Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
+        Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
+    }
+    else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
+    {
+        SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
+        SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
+
+        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 ) );
+
+        int RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
+        if ( RetValue == -1 )
+            return -1;
+    } 
+    else
+    {
+        if ( pSubCube0->iLit1 > 0 )
+        {
+            SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
+
+            Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
+            if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
+                Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
+            else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
+                Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
+        }
+        else 
+        {
+            SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
+
+            Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
+            if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
+                Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
+            else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
+                Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
+        }
+    }
+
+    if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
+        return -1;
+
+    if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
+    {
+        Vec_IntSort( pFxchMan->vCubeFree, 0 );
+
+        Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
+        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 ) );
+    if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
+    {
+        Base = Abc_MinInt( Cube0Size, Cube1Size )
+               -( Vec_IntSize( pFxchMan->vCubeFree ) / 2)  - 1; /* 1 or 2 Lits, 1 SOP NodeID */
+    }
+    else
+        return -1;
+
+    return Base;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Add a divisor to the divisors hash table. ]
+
+  Description [ This functions will try to add the divisor store in 
+                vCubeFree to the divisor hash table. If the divisor
+                is already present in the hash table it will just 
+                increment its weight, otherwise it will add the divisor
+                and asign an initial weight. ]
+
+  SideEffects [ If the fUpdate option is set, the function will also
+                update the divisor priority queue. ]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_DivAdd( Fxch_Man_t* pFxchMan,
+                 int fUpdate,
+                 int fSingleCube,
+                 int fBase )
+{
+    int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
+
+    /* Verify if the divisor already exist */ 
+    if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
+    {
+        if ( pFxchMan->SMode == 0 )
+            Vec_WecPushLevel( pFxchMan->vDivCubePairs );
+
+        /* Assign initial weight */
+        if ( fSingleCube )
+        {
+            Vec_FltPush( pFxchMan->vDivWeights,
+                         -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
+                         -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
+        }
+        else
+        {
+            Vec_FltPush( pFxchMan->vDivWeights,
+                         -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
+                         -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
+        }
+
+    }
+
+    /* Increment weight */
+    if ( fSingleCube )
+        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
+    else
+        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );
+
+    assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
+
+    if ( fUpdate )
+        if ( pFxchMan->vDivPrio )
+        {
+            if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
+                Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
+            else
+                Vec_QuePush( pFxchMan->vDivPrio, iDiv );
+        }
+
+    return iDiv;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Removes a divisor to the divisors hash table. ]
+
+  Description [ This function don't effectively removes a divisor from
+                the hash table (the hash table implementation don't 
+                support such operation). It only assures its existence
+                and decrement its weight. ]
+
+  SideEffects [ If the fUpdate option is set, the function will also
+                update the divisor priority queue. ]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_DivRemove( Fxch_Man_t* pFxchMan,
+                    int fUpdate,
+                    int fSingleCube,
+                    int fBase )
+{
+    int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
+
+    assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
+
+    /* Decrement weight */
+    if ( fSingleCube )
+        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
+    else
+        Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );
+
+    if ( fUpdate )
+        if ( pFxchMan->vDivPrio )
+        {
+            if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
+                Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
+        }
+
+    return iDiv;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Separete the cubes in present in a divisor ]
+
+  Description [ In this implementation *all* stored divsors are composed 
+                of two cubes. 
+
+                In order to save space and to be able to use the Vec_Int_t
+                hash table both cubes are stored in the same vector - using
+                a little hack to differentiate which literal belongs to each
+                cube.
+
+                This function separetes the two cubes in their own vectors
+                so that they can be added to the cover.
+
+                *Note* that this also applies to single cube 
+                divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxch_DivSepareteCubes( Vec_Int_t* vDiv,
+                            Vec_Int_t* vCube0,
+                            Vec_Int_t* vCube1 )
+{
+    int* pArray;
+    int i,
+        Lit;
+
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( Abc_LitIsCompl(Lit) )
+            Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
+        else
+            Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );
+
+    if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
+    {
+        assert( Vec_IntSize( vCube1 ) == 3 );
+
+        pArray = Vec_IntArray( vCube0 );
+        if ( pArray[1] > pArray[2] )
+            ABC_SWAP( int, pArray[1], pArray[2] );
+
+        pArray = Vec_IntArray( vCube1 );
+        if ( pArray[1] > pArray[2] )
+            ABC_SWAP( int, pArray[1], pArray[2] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Removes the literals present in the divisor from their 
+               original cubes. ]
+
+  Description [ This function returns the numeber of removed literals
+                which should be equal to the size of the divisor. ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_DivRemoveLits( Vec_Int_t* vCube0,
+                        Vec_Int_t* vCube1,
+                        Vec_Int_t* vDiv,
+                        int *fCompl )
+{
+    int i,
+        Lit,
+        CountP = 0,
+        CountN = 0,
+        Count = 0,
+        ret = 0;
+
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
+            CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
+        else
+            CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
+
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );
+
+   if ( Vec_IntSize( vDiv ) == 2 )
+       Vec_IntForEachEntry( vDiv, Lit, i )
+       {
+           Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
+           Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
+       }
+
+    ret = Count + CountP + CountN;
+
+    if ( Vec_IntSize( vDiv ) == 4 )
+    {
+        int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
+            Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
+            Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
+            Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );
+
+        if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
+            *fCompl = 1;
+
+        if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
+        {
+            *fCompl = 1;
+
+            Vec_IntForEachEntry( vDiv, Lit, i )
+                ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
+
+            Vec_IntForEachEntry( vDiv, Lit, i )
+                ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
+        }
+    }
+
+    return ret;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [ Print the divisor identified by iDiv. ]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxch_DivPrint( Fxch_Man_t* pFxchMan,
+                    int iDiv )
+{
+    Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
+    int i,
+        Lit;
+
+    printf( "Div %7d : ", iDiv );
+    printf( "Weight %12.5f  ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );
+
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( !Abc_LitIsCompl( Lit ) )
+            printf( "%d(1)", Abc_Lit2Var( Lit ) );
+
+    printf( " + " );
+
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( Abc_LitIsCompl( Lit ) )
+            printf( "%d(2)", Abc_Lit2Var( Lit ) );
+
+    printf( " Lits =%7d  ", pFxchMan->nLits );
+    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;
+
+        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 ( int i_ = 0; i_ < i; i_++ )
+            for ( int 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                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END

src/opt/fxch/FxchMan.c

+/**CFile****************************************************************
+
+  FileName    [ FxchMan.c ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ Fxch Manager implementation ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************/
+
+#include "Fxch.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                LOCAL FUNCTIONS DEFINITIONS                       ///
+////////////////////////////////////////////////////////////////////////
+static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan,
+                                       unsigned int SubCubeID, 
+                                       unsigned int iSubCube,
+                                       unsigned int iCube, 
+                                       unsigned int iLit0, 
+                                       unsigned int iLit1,
+                                       char fAdd,
+                                       char fUpdate ) 
+{
+    int ret = 0;
+
+    if ( fAdd )
+    {
+        ret = Fxch_SCHashTableInsert( pFxchMan->pSCHashTable, pFxchMan->vCubes,
+                                      SubCubeID, iSubCube,
+                                      iCube, iLit0, iLit1, fUpdate );
+    }
+    else
+    {
+        ret = Fxch_SCHashTableRemove( pFxchMan->pSCHashTable, pFxchMan->vCubes,
+                                      SubCubeID, iSubCube,
+                                      iCube, iLit0, iLit1, fUpdate );
+    }
+
+    return ret;
+}
+
+
+static inline int Fxch_ManDivSingleCube( Fxch_Man_t* pFxchMan,
+                                         int iCube,
+                                         int fAdd,
+                                         int fUpdate )
+{
+    Vec_Int_t* vCube = Vec_WecEntry( pFxchMan->vCubes, iCube );
+    int i, k,
+        Lit0,
+        Lit1,
+        fSingleCube = 1,
+        fBase = 0;
+
+    if ( Vec_IntSize(vCube) < 2 )
+        return 0;
+
+    Vec_IntForEachEntryStart( vCube, Lit0, i, 1)
+    Vec_IntForEachEntryStart( vCube, Lit1, k, (i + 1) )
+    {
+        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 ) );
+
+        if (fAdd)
+        {
+            Fxch_DivAdd( pFxchMan, fUpdate, fSingleCube, fBase );
+            pFxchMan->nPairsS++;
+        }
+        else
+        {
+            Fxch_DivRemove( pFxchMan, fUpdate, fSingleCube, fBase );
+            pFxchMan->nPairsS--;
+        }
+    }
+
+    return Vec_IntSize( vCube ) * ( Vec_IntSize( vCube ) - 1 ) / 2;
+}
+
+static inline void Fxch_ManDivDoubleCube( Fxch_Man_t* pFxchMan,
+                                          int iCube,
+                                          int fAdd,
+                                          int fUpdate )
+{
+    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++,
+                         iCube, 0, 0,
+                         fAdd, fUpdate );
+
+    Vec_IntForEachEntryStart( vCube, Lit0, iLit0, 1)
+    {
+        /* 1 Lit remove */
+        SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit0 );
+
+        pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
+                                                  SubCubeID, nHashedSC++,
+                                                  iCube, iLit0, 0,
+                                                  fAdd, fUpdate );
+
+        if ( Vec_IntSize( vCube ) > 3 )
+        {
+            int Lit1,
+                iLit1;
+
+            Vec_IntForEachEntryStart( vCube, Lit1, iLit1, iLit0 + 1)
+            {
+                /* 2 Lit remove */
+                SubCubeID -= Vec_IntEntry( vLitHashKeys, Lit1 );
+
+                pFxchMan->nPairsD += Fxch_ManSCAddRemove( pFxchMan,
+                                                          SubCubeID, nHashedSC++,
+                                                          iCube, iLit0, iLit1,
+                                                          fAdd, fUpdate );
+
+                SubCubeID += Vec_IntEntry( vLitHashKeys, Lit1 );
+            }
+        }
+
+        SubCubeID += Vec_IntEntry( vLitHashKeys, Lit0 );
+    }
+}
+
+static inline void Fxch_ManCompressCubes( Vec_Wec_t* vCubes,
+                                          Vec_Int_t* vLit2Cube )
+{
+    int i,
+        k = 0,
+        CubeId;
+
+    Vec_IntForEachEntry( vLit2Cube, CubeId, i )
+        if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 )
+            Vec_IntWriteEntry( vLit2Cube, k++, CubeId );
+
+    Vec_IntShrink( vLit2Cube, k );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     PUBLIC INTERFACE                             ///
+////////////////////////////////////////////////////////////////////////
+Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes,
+                           char SMode )
+{
+    Fxch_Man_t* pFxchMan = ABC_CALLOC( Fxch_Man_t, 1 );
+
+    pFxchMan->vCubes = vCubes;
+    pFxchMan->pDivHash    = Hsh_VecManStart( 1000 );
+    pFxchMan->vDivWeights = Vec_FltAlloc( 1000 );
+
+    pFxchMan->SMode = SMode;
+    if ( pFxchMan->SMode == 0 )
+        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 );
+
+    return pFxchMan;
+}
+
+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_IntFree( pFxchMan->vLevels );
+
+    Vec_IntFree( pFxchMan->vCubeFree );
+    Vec_IntFree( pFxchMan->vDiv );
+    Vec_IntFree( pFxchMan->vCubesS );
+    Vec_IntFree( pFxchMan->vPairs );
+
+    ABC_FREE( pFxchMan );
+}
+
+void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan,
+                                   int nVars )
+{
+
+    Vec_Int_t* vCube;
+    int i, k,
+        Lit,
+        Count;
+
+    pFxchMan->nVars = 0;
+    pFxchMan->nLits = 0;
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+    {
+        assert( Vec_IntSize(vCube) > 0 );
+        pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Vec_IntEntry( vCube, 0 ) );
+        pFxchMan->nLits += Vec_IntSize(vCube) - 1;
+        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+            pFxchMan->nVars = Abc_MaxInt( pFxchMan->nVars, Abc_Lit2Var( Lit ) );
+    }
+
+    assert( pFxchMan->nVars < nVars );
+    pFxchMan->nVars = nVars;
+
+    /* Count the number of time each literal appears on the SOP */
+    pFxchMan->vLitCount = Vec_IntStart( 2 * pFxchMan->nVars );
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+            Vec_IntAddToEntry( pFxchMan->vLitCount, Lit, 1 );
+
+    /* Allocate space to the array of arrays wich maps Literals into cubes which uses them */
+    pFxchMan->vLits = Vec_WecStart( 2 * pFxchMan->nVars );
+    Vec_IntForEachEntry( pFxchMan->vLitCount, Count, Lit )
+        Vec_IntGrow( Vec_WecEntry( pFxchMan->vLits, Lit ), Count );
+
+    /* Maps Literals into cubes which uses them */
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+            Vec_WecPush( pFxchMan->vLits, Lit, i );
+}
+
+void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan )
+{
+    /* 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++ )
+        Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
+}
+
+void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan )
+{
+    Vec_Wec_t* vCubes = pFxchMan->vCubes;
+    Vec_Int_t* vCube,
+             * vCubeLinks;
+    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 : ( nLits * nLits + nLits ) / 2;
+
+        Vec_IntPush( vCubeLinks, ( nTotalHashed + 1 ) );
+        nTotalHashed += nSubCubes + 1;
+    }
+
+    pFxchMan->pSCHashTable = Fxch_SCHashTableCreate( pFxchMan, vCubeLinks, nTotalHashed );
+}
+
+void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan )
+{
+    Fxch_SCHashTableDelete( pFxchMan->pSCHashTable );
+}
+
+void Fxch_ManDivCreate( Fxch_Man_t* pFxchMan )
+{
+    Vec_Int_t* vCube;
+    float Weight;
+    int fAdd = 1,
+        fUpdate = 0,
+        iCube;
+
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, iCube )
+    {
+        Fxch_ManDivSingleCube( pFxchMan, iCube, fAdd, fUpdate );
+        Fxch_ManDivDoubleCube( pFxchMan, iCube, fAdd, fUpdate );
+    }
+
+    pFxchMan->vDivPrio = Vec_QueAlloc( Vec_FltSize( pFxchMan->vDivWeights ) );
+    Vec_QueSetPriority( pFxchMan->vDivPrio, Vec_FltArrayP( pFxchMan->vDivWeights ) );
+    Vec_FltForEachEntry( pFxchMan->vDivWeights, Weight, iCube )
+    {
+        if ( Weight > 0.0 )
+            Vec_QuePush( pFxchMan->vDivPrio, iCube );
+    }
+}
+
+/* Level Computation */
+int Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan,
+                             Vec_Int_t* vCubeFree )
+{
+    int i,
+        Lit,
+        Level = 0;
+
+    Vec_IntForEachEntry( vCubeFree, Lit, i )
+        Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Abc_Lit2Var( Lit ) ) ) );
+
+    return Abc_MinInt( Level, 800 );
+}
+
+int Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan,
+                              Vec_Int_t * vCube )
+{
+    int k,
+        Lit,
+        Level = 0;
+
+    Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+        Level = Abc_MaxInt( Level, Vec_IntEntry( pFxchMan->vLevels, Abc_Lit2Var( Lit ) ) );
+
+    return Level;
+}
+
+void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan )
+{
+    Vec_Int_t* vCube;
+    int i,
+        iVar,
+        iFirst = 0;
+
+    iVar = Vec_IntEntry( Vec_WecEntry( pFxchMan->vCubes, 0 ), 0 );
+    pFxchMan->vLevels = Vec_IntStart( pFxchMan->nVars );
+
+    Vec_WecForEachLevel( pFxchMan->vCubes, vCube, i )
+    {
+        if ( iVar != Vec_IntEntry( vCube, 0 ) )
+        {
+            Vec_IntAddToEntry( pFxchMan->vLevels, iVar, i - iFirst );
+            iVar = Vec_IntEntry( vCube, 0 );
+            iFirst = i;
+        }
+        Vec_IntUpdateEntry( pFxchMan->vLevels, iVar, Fxch_ManComputeLevelCube( pFxchMan, vCube ) );
+    }
+}
+
+void Fxch_ManUpdate( Fxch_Man_t* pFxchMan,
+                     int iDiv )
+{
+    int i,
+        iCube0, 
+        iCube1,
+        Lit0 = -1, 
+        Lit1 = -1;
+
+    Vec_Int_t* vCube0,
+             * vCube1,
+             * vLitP, 
+             * vLitN,
+             * vDivCubePairs;
+
+    /* Get the selected candidate (divisor) */
+    Vec_IntClear( pFxchMan->vDiv );
+    Vec_IntAppend( pFxchMan->vDiv, Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ) );
+
+    /* Find cubes associated with the single divisor */
+    Vec_IntClear( pFxchMan->vCubesS );
+    if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
+    {
+        Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) );
+        Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) );
+
+        Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) );
+        Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) );
+        Vec_IntTwoRemoveCommon( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ),
+                                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 );
+    }
+
+    Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
+    {
+        assert( Fxch_ManGetLit( pFxchMan, iCube0, 0) == Fxch_ManGetLit( pFxchMan, iCube1, 0) );
+        if (iCube0 > iCube1)
+        {
+            Vec_IntSetEntry( pFxchMan->vPairs, i, iCube1);
+            Vec_IntSetEntry( pFxchMan->vPairs, i+1, iCube0);
+        }
+    }
+
+    Vec_IntUniqifyPairs( pFxchMan->vPairs );
+    assert( Vec_IntSize( pFxchMan->vPairs ) % 2 == 0 );
+
+    /* 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 */
+
+    /* 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 */
+    }
+
+    Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
+    {
+        if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */
+
+    }
+
+    /* Create a new variable */
+    int iVarNew = pFxchMan->nVars;
+    pFxchMan->nVars++;
+
+    /* Create new Lit hash keys */
+    Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
+    Vec_IntPush( pFxchMan->vLitHashKeys, Gia_ManRandom(0) & 0x3FFFFFF );
+
+    /* Create new Cube */
+    vCube0 = Vec_WecPushLevel( pFxchMan->vCubes );
+    Vec_IntPush( vCube0, iVarNew );
+
+    int Level;
+    if ( Vec_IntSize( pFxchMan->vDiv ) == 2 )
+    {
+        if ( Lit0 > Lit1 )
+            ABC_SWAP(int, Lit0, Lit1);
+
+        Vec_IntPush( vCube0, Abc_LitNot( Lit0 ) );
+        Vec_IntPush( vCube0, Abc_LitNot( Lit1 ) );
+        Level = 1 + Fxch_ManComputeLevelCube( pFxchMan, vCube0 );
+    }
+    else
+    {
+        vCube1 = Vec_WecPushLevel( pFxchMan->vCubes );
+        vCube0 = Fxch_ManGetCube( pFxchMan, Vec_WecSize( pFxchMan->vCubes ) - 2 );
+        Vec_IntPush( vCube1, iVarNew );
+        Fxch_DivSepareteCubes( pFxchMan->vDiv, vCube0, vCube1 );
+        Level = 2 + Abc_MaxInt( Fxch_ManComputeLevelCube( pFxchMan, vCube0 ),
+                                Fxch_ManComputeLevelCube( pFxchMan, vCube1 ) );
+    }
+    assert( Vec_IntSize( pFxchMan->vLevels ) == iVarNew );
+    Vec_IntPush( pFxchMan->vLevels, Level );
+
+    pFxchMan->nLits += Vec_IntSize( pFxchMan->vDiv );
+
+    /* Create new literals */
+    vLitP = Vec_WecPushLevel( pFxchMan->vLits );
+    vLitN = Vec_WecPushLevel( pFxchMan->vLits );
+    vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 );
+
+    /* Extract divisor from single-cubes */
+    Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+    {
+        int RetValue;
+
+        vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 );
+        RetValue  = Vec_IntRemove1( vCube0, Abc_LitNot( Lit0 ) );
+        RetValue += Vec_IntRemove1( vCube0, Abc_LitNot( Lit1 ) );
+        assert( RetValue == 2 );
+
+        Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
+        Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+
+        pFxchMan->nLits--;
+    }
+
+    /* For each pair (Ci, Cj) */
+    /* Extract divisor from cube pairs */
+    int k = 0,
+        nCompls = 0;
+    Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i )
+    {
+        int RetValue, fCompl = 0;
+
+        vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 );
+        vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 );
+
+        RetValue  = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl );
+        nCompls += fCompl;
+
+        assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) );
+
+        if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl )
+        {
+            Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) );
+            Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+        }
+        else
+        {
+            Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) );
+            Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+        }
+        pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2;
+
+        /* Remove second cube */
+        Vec_IntClear( vCube1 );
+        Vec_IntWriteEntry( pFxchMan->vPairs, k++, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) );
+    }
+    assert( k == Vec_IntSize( pFxchMan->vPairs ) / 2 );
+    Vec_IntShrink( pFxchMan->vPairs, k );
+
+    /* Add cost of single-cube divisors */
+    Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i )
+        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+    Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
+        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 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 */
+
+    Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i )
+        if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) )
+            Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */
+
+    /* If it's a double-cube devisor add its cost */
+    if ( Vec_IntSize( pFxchMan->vDiv ) > 2 )
+    {
+        iCube0 = Vec_WecSize( pFxchMan->vCubes ) - 2;
+        iCube1 = Vec_WecSize( pFxchMan->vCubes ) - 1;
+
+        Fxch_ManDivSingleCube( pFxchMan, iCube0, 1, 1 );  /* fAdd = 1 - fUpdate = 1 */
+        Fxch_ManDivSingleCube( pFxchMan, iCube1, 1, 1 );  /* fAdd = 1 - fUpdate = 1 */
+
+        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 ) );
+    }
+
+    /* remove these cubes from the lit array of the divisor */
+    Vec_IntForEachEntry( pFxchMan->vDiv, Lit0, i )
+    {
+        Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_Lit2Var( Lit0 ) ), pFxchMan->vPairs );
+        Vec_IntTwoRemove( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Abc_Lit2Var( Lit0 ) ) ), pFxchMan->vPairs );
+    }
+
+    pFxchMan->nExtDivs++;
+}
+
+/* Print */
+void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan )
+{
+    int iDiv;
+
+    for ( iDiv = 0; iDiv < Vec_FltSize( pFxchMan->vDivWeights ); iDiv++ )
+        Fxch_DivPrint( pFxchMan, iDiv );
+}
+
+void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan )
+{
+    printf( "[FXCH] ");
+    printf( "Cubes =%8d  ", Vec_WecSizeUsed( pFxchMan->vCubes ) );
+    printf( "Lits  =%8d  ", Vec_WecSizeUsed( pFxchMan->vLits ) );
+    printf( "Divs  =%8d  ", Hsh_VecSize( pFxchMan->pDivHash ) );
+    printf( "Divs+ =%8d  ", Vec_QueSize( pFxchMan->vDivPrio ) );
+    printf( "Extr  =%7d  \n", pFxchMan->nExtDivs );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END

src/opt/fxch/FxchSCHashTable.c

+/**CFile****************************************************************
+
+  FileName    [ FxchSCHashTable.c ]
+
+  PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
+
+  Synopsis    [ Sub-cubes hash table implementation ]
+
+  Author      [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
+
+  Affiliation [ UFRGS ]
+
+  Date        [ Ver. 1.0. Started - March 6, 2016. ]
+
+  Revision    []
+
+***********************************************************************/
+#include "Fxch.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+static inline void MurmurHash3_x86_32 ( const void* key,
+                                        int len,
+                                        uint32_t seed,
+                                        void* out )
+{
+    const uint8_t* data = (const uint8_t*)key;
+    const int nblocks = len / 4;
+
+    uint32_t h1 = seed;
+
+    const uint32_t c1 = 0xcc9e2d51;
+    const uint32_t c2 = 0x1b873593;
+
+    //----------
+    // body
+
+    const uint32_t * blocks = (const uint32_t *)(data + nblocks*4);
+
+    for(int i = -nblocks; i; i++)
+    {
+        uint32_t k1 = blocks[i];
+
+        k1 *= c1;
+        k1 = (k1 << 15) | (k1 >> (32 - 15));
+        k1 *= c2;
+
+        h1 ^= k1;
+        h1 = (h1 << 13) | (h1 >> (32 - 13));
+        h1 = h1*5+0xe6546b64;
+    }
+
+    //----------
+    // tail
+
+    const uint8_t * tail = (const uint8_t*)(data + nblocks*4);
+
+    uint32_t k1 = 0;
+
+    switch(len & 3)
+    {
+        case 3: k1 ^= tail[2] << 16;
+        case 2: k1 ^= tail[1] << 8;
+        case 1: k1 ^= tail[0];
+              k1 *= c1; k1 = (k1 << 15) | (k1 >> (32 - 15)); k1 *= c2; h1 ^= k1;
+    };
+
+    //----------
+    // finalization
+
+    h1 ^= len;
+
+    h1 ^= h1 >> 16;
+    h1 *= 0x85ebca6b;
+    h1 ^= h1 >> 13;
+    h1 *= 0xc2b2ae35;
+    h1 ^= h1 >> 16;
+
+    *(uint32_t*)out = h1;
+}
+
+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 );
+    int nBits = Abc_Base2Log( nEntries + 1 ) + 1;
+
+
+    pSCHashTable->pFxchMan = pFxchMan;
+    pSCHashTable->SizeMask = (1 << nBits) - 1;
+    pSCHashTable->vCubeLinks = vCubeLinks;
+    pSCHashTable->pBins = ABC_CALLOC( Fxch_SCHashTable_Entry_t, pSCHashTable->SizeMask + 1 );
+
+    return pSCHashTable;
+}
+
+void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* pSCHashTable )
+{
+    Vec_IntFree( pSCHashTable->vCubeLinks );
+    Vec_IntErase( &pSCHashTable->vSubCube0 );
+    Vec_IntErase( &pSCHashTable->vSubCube1 );
+    ABC_FREE( pSCHashTable->pBins );
+    ABC_FREE( pSCHashTable );
+}
+
+static inline Fxch_SCHashTable_Entry_t* Fxch_SCHashTableBin( Fxch_SCHashTable_t* pSCHashTable,
+                                                             unsigned int SubCubeID )
+{
+    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( pEntry0->iNext == iEntry1 );
+    assert( pEntry1->iPrev == iEntry0 );
+    assert( 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,
+                                                Fxch_SubCube_t* pSCData1 )
+{
+    Vec_Int_t* vCube0 = Vec_WecEntry( vCubes, pSCData0->iCube ),
+             * vCube1 = Vec_WecEntry( vCubes, pSCData1->iCube );
+
+    if ( !Vec_IntSize( vCube0 ) ||
+         !Vec_IntSize( vCube1 ) ||
+         Vec_IntEntry( vCube0, 0 ) != Vec_IntEntry( vCube1, 0 ) ||
+         pSCData0->Id != pSCData1->Id )
+        return 0;
+
+    Vec_IntClear( &pSCHashTable->vSubCube0 );
+    Vec_IntClear( &pSCHashTable->vSubCube1 );
+
+    if ( pSCData0->iLit1 == 0 && pSCData1->iLit1 == 0 &&
+         Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Abc_LitNot( Vec_IntEntry( vCube1, pSCData1->iLit0 ) ) )
+        return 0;
+
+    if ( pSCData0->iLit1 > 0 && pSCData1->iLit1 > 0 &&
+         ( Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) ||
+           Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ||
+           Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) ||
+           Vec_IntEntry( vCube0, pSCData0->iLit1 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) ) )
+        return 0;
+
+
+    if ( pSCData0->iLit0 > 0 )
+        Vec_IntAppendSkip( &pSCHashTable->vSubCube0, vCube0, pSCData0->iLit0 );
+    else
+        Vec_IntAppend( &pSCHashTable->vSubCube0, vCube0 );
+
+    if ( pSCData1->iLit0 > 0 )
+        Vec_IntAppendSkip( &pSCHashTable->vSubCube1, vCube1, pSCData1->iLit0 );
+    else
+        Vec_IntAppend( &pSCHashTable->vSubCube1, vCube1 );
+
+
+    if ( pSCData0->iLit1 > 0)
+        Vec_IntDrop( &pSCHashTable->vSubCube0,
+                       pSCData0->iLit0 < pSCData0->iLit1 ? pSCData0->iLit1 - 1 : pSCData0->iLit1 );
+
+    if ( pSCData1->iLit1 > 0 )
+        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,
+                            char fUpdate )
+{
+    unsigned int BinID;
+    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 );
+
+    assert( pNewEntry->Used == 0 );
+
+    pNewEntry->SCData.Id = SubCubeID;
+    pNewEntry->SCData.iCube = iCube;
+    pNewEntry->SCData.iLit0 = iLit0;
+    pNewEntry->SCData.iLit1 = iLit1;
+
+    pNewEntry->Used = 1;
+    pSCHashTable->nEntries++;
+    if ( pBin->iTable == 0 )
+    {
+        pBin->iTable = iNewEntry;
+        pNewEntry->iNext = iNewEntry;
+        pNewEntry->iPrev = iNewEntry;
+        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 )
+    {
+        pEntry = Fxch_SCHashTableBin( pSCHashTable, iEntry );
+
+        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) )
+            continue;
+
+        if ( pEntry->SCData.iLit0 == 0 )
+        {
+            printf("[FXCH] SCC detected\n");
+            continue;
+        }
+        if ( pNewEntry->SCData.iLit0 == 0 )
+        {
+            printf("[FXCH] SCC detected\n");
+            continue;
+        }
+
+        int Base;
+        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 ) );
+
+        if ( Base < 0 ) 
+            continue;
+
+        int 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++;
+    }
+    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,
+                            char fUpdate )
+{
+    unsigned int BinID;
+    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 );
+    
+    assert( pEntry->Used == 1 );
+    assert( pEntry->SCData.iCube == iCube );
+
+    if ( pEntry->iNext == iEntry )
+    {
+        assert( pEntry->iPrev == iEntry );
+        pBin->iTable = 0;
+        pEntry->iNext = 0;
+        pEntry->iPrev = 0;
+        pEntry->Used = 0;
+        return 0;
+    }
+
+    Fxch_SCHashTable_Entry_t* pNextEntry;
+    int iNextEntry,
+        Pairs = 0,
+        fStart = 1;
+    for ( iNextEntry = pEntry->iNext; iNextEntry != iEntry; iNextEntry = pNextEntry->iNext, fStart = 0 )
+    {
+        pNextEntry = Fxch_SCHashTableBin( pSCHashTable, iNextEntry );
+
+        if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNextEntry->SCData ) ) 
+             || pEntry->SCData.iLit0 == 0
+             || pNextEntry->SCData.iLit0 == 0 )
+            continue;
+
+        int Base;
+        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 ) );
+
+        if ( Base < 0 ) 
+            continue;
+
+        int iDiv = Fxch_DivRemove( pSCHashTable->pFxchMan, fUpdate, 0, Base );
+
+        if ( pSCHashTable->pFxchMan->SMode == 0 )
+        {
+            int i,
+                iCube0,
+                iCube1;
+
+            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 ) )
+                {
+                    Vec_IntDrop( vDivCubePairs, i+1 );
+                    Vec_IntDrop( vDivCubePairs, i );
+                }
+            if ( Vec_IntSize( vDivCubePairs ) == 0 )
+                Vec_IntErase( vDivCubePairs );
+        }
+
+        Pairs++;
+    }
+
+    if ( pBin->iTable == iEntry )
+        pBin->iTable = ( pEntry->iNext != iEntry ) ? pEntry->iNext : 0;
+
+    pEntry->Used = 0;
+    Fxch_SCHashTableRemoveLink( pSCHashTable, pEntry->iPrev, iEntry );
+    return Pairs;
+}
+
+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;
+}
+
+void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* pHashTable )
+{
+    printf( "SubCube Hash Table at %p\n", ( void* )pHashTable );
+    printf("%20s %20s\n", "nEntries",
+                          "Memory Usage (MB)" );
+
+    int Memory = Fxch_SCHashTableMemory( pHashTable );
+    printf("%20d %18.2f\n", pHashTable->nEntries,
+                            ( ( double ) Memory / 1048576 ) );
+}
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_IMPL_END

src/opt/fxch/module.make

+SRC +=  src/opt/fxch/Fxch.c \
+    src/opt/fxch/FxchDiv.c \
+    src/opt/fxch/FxchMan.c  \
+    src/opt/fxch/FxchSCHashTable.c \