New fast extract.

10 files changed, 749 insertions, 226 deletions

diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index 7f43e24f..1c913eea 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -104,7 +104,7 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
-  Synopsis    [Makes nodes of the network fanin-dup-ABC_FREE.]
+  Synopsis    [Makes nodes of the network fanin-dup-free.]
 
   Description [Returns the number of pairs of duplicated fanins.]
                
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index 69cfb352..0d58ac9e 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Interface with the fast extract package.]
+  Synopsis    [Interface with the fast_extract package.]
 
   Author      [Alan Mishchenko]
   
@@ -219,7 +219,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes )
             }
             pCube += Abc_ObjFaninNum(pNode) + 3;
         }
-        if ( Abc_SopIsComplement((char *)pNode->pData) )
+        if ( pNode->pData && Abc_SopIsComplement((char *)pNode->pData) )
             Abc_SopComplement( pSop );
         pNode->pData = pSop;
         // clean fanins
@@ -302,20 +302,36 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose )
 typedef struct Fx_Man_t_ Fx_Man_t;
 struct Fx_Man_t_
 {
-    int             nVars;   // original problem variables
-    int             nPairsS; // number of lit pairs
-    int             nPairsD; // number of cube pairs
-    int             nDivsS;  // single cube divisors
-    Vec_Wec_t *     vCubes;  // cube -> lit (user data)
-    Vec_Wec_t *     vLits;   // lit -> cube
-    Vec_Int_t *     vCounts; // literal counts
-    Hsh_VecMan_t *  pHash;   // divisors 
-    Vec_Flt_t *     vWeights;// divisor weights
-    Vec_Que_t *     vPrio;   // priority queue
-    // temporary variables
-    Vec_Int_t *     vCube; 
+    Vec_Wec_t *     vCubes;   // cube -> lit (user data)
+    Vec_Wec_t *     vLits;    // lit -> cube
+    Vec_Int_t *     vCounts;  // literal counts
+    Hsh_VecMan_t *  pHash;    // divisors 
+    Vec_Flt_t *     vWeights; // divisor weights
+    Vec_Que_t *     vPrio;    // priority queue
+    Vec_Int_t *     vVarCube; // mapping var into its first cube
+    // temporary arrays used for updating
+    Vec_Int_t *     vCubesS;  // single cube divisors
+    Vec_Int_t *     vCubesD;  // double cube divisors
+    Vec_Int_t *     vPart0;   // cubes of given literal
+    Vec_Int_t *     vPart1;   // cubes of given literal
+    Vec_Int_t *     vFree;    // cube-free divisor
+    Vec_Int_t *     vCube;    // one cube
+    Vec_Int_t *     vDiv;     // divisor
+    // statistics 
+    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             nDivsS;   // single cube divisors
 };
 
+static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { return Vec_IntEntry( p->vVarCube, Vec_IntEntry(vCube, 0) ); }
+
+#define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i )           \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )
+#define Fx_ManForEachPairVec( vVec, vCubes, vCube1, vCube2, i )  \
+    for ( i = 0; (i+1 < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))) && ((vCube2) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i+1))); i += 2 )
+
 /**Function*************************************************************
 
   Synopsis    [Create literals.]
@@ -389,6 +405,92 @@ int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented
   SeeAlso     []
 
 ***********************************************************************/
+static inline char Fx_PrintDivLit( int Lit ) { return (Abc_LitIsCompl(Lit) ? 'A' : 'a') + Abc_Lit2Var(Lit); }
+static inline void Fx_PrintDivOne( Vec_Int_t * vDiv )
+{
+    int i, Lit;
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( !Abc_LitIsCompl(Lit) )
+            printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) );
+    printf( " + " );
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( Abc_LitIsCompl(Lit) )
+            printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) );
+}
+static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv )
+{
+    printf( "Div %6d : ", iDiv );
+    printf( "Cost %4d  ", (int)Vec_FltEntry(p->vWeights, iDiv) );
+    Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) );
+    printf( "\n" );
+}
+static void Fx_PrintDivisors( Fx_Man_t * p )
+{
+    int iDiv;
+    for ( iDiv = 0; iDiv < Vec_FltSize(p->vWeights); iDiv++ )
+        Fx_PrintDiv( p, iDiv );
+}
+static void Fx_PrintLiterals( Fx_Man_t * p )
+{
+    Vec_Int_t * vTemp;
+    int i;
+    Vec_WecForEachLevel( p->vLits, vTemp, i )
+    {
+        printf( "%c : ", Fx_PrintDivLit(i) );
+        Vec_IntPrint( vTemp );
+    }
+}
+static void Fx_PrintMatrix( Fx_Man_t * p )
+{
+    Vec_Int_t * vCube;
+    int i, v, Lit, nObjs;
+    char * pLine;
+    printf( "         " );
+    nObjs = Vec_WecSize(p->vLits)/2;
+    for ( i = 0; i < Abc_MinInt(nObjs, 26); i++ )
+        printf( "%c", 'a' + i );
+    printf( "\n" );
+    pLine = ABC_CALLOC( char, nObjs+1 );
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+    {
+        if ( Vec_IntSize(vCube) == 0 )
+            continue;
+        memset( pLine, '-', nObjs );
+        Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+        {
+            assert( Abc_Lit2Var(Lit) < nObjs );
+            pLine[Abc_Lit2Var(Lit)] = Abc_LitIsCompl(Lit) ? '0' : '1';
+        }
+        printf( "%6d : %s %4d\n", i, pLine, Vec_IntEntry(vCube, 0) );
+    }
+    ABC_FREE( pLine );
+    Fx_PrintLiterals( p );
+    Fx_PrintDivisors( p );
+}
+static void Fx_PrintStats( Fx_Man_t * p, clock_t clk )
+{
+    printf( "Cubes =%6d  ", Vec_WecSizeUsed(p->vCubes) );
+    printf( "Lits  =%6d  ", Vec_WecSizeUsed(p->vLits) );
+    printf( "Divs  =%6d  ", Hsh_VecSize(p->pHash) );
+    printf( "Divs+ =%6d  ", Vec_QueSize(p->vPrio) );
+    printf( "DivsS =%6d  ", p->nDivsS );
+    printf( "PairS =%6d  ", p->nPairsS );
+    printf( "PairD =%6d  ", p->nPairsD );
+    Abc_PrintTime( 1, "Time", clk );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFree )
 {
     int * pBeg1 = vArr1->pArray + 1;
@@ -414,7 +516,7 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFr
         Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
     while ( pBeg2 < pEnd2 )
         Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
-    assert( Vec_IntSize(vFree) > 1 );
+    assert( Vec_IntSize(vFree) > 1 ); // the cover is not SCC-free
     assert( !Abc_LitIsCompl(Vec_IntEntry(vFree, 0)) );
     return Counter;
 }
@@ -430,100 +532,49 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFr
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Wec_t * Fx_ManCreateLiterals( Vec_Wec_t * vCubes, Vec_Int_t ** pvCounts )
+static inline void Fx_ManDivFindPivots( Vec_Int_t * vDiv, int * pLit0, int * pLit1 )
 {
-    Vec_Wec_t * vLits;
-    Vec_Int_t * vCube, * vCounts;
-    int i, k, Count, Lit, LitMax = 0;
-    // find max literal
-    Vec_WecForEachLevel( vCubes, vCube, i )
-        Vec_IntForEachEntry( vCube, Lit, k )
-            LitMax = Abc_MaxInt( LitMax, Lit );
-    // count literals
-    vCounts = Vec_IntStart( LitMax + 2 );
-    Vec_WecForEachLevel( vCubes, vCube, i )
-        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
-            Vec_IntAddToEntry( vCounts, Lit, 1 );
-    // start literals
-    vLits = Vec_WecStart( 2 * LitMax );
-    Vec_IntForEachEntry( vCounts, Count, Lit )
-        Vec_IntGrow( Vec_WecEntry(vLits, Lit), Count );
-    // fill out literals
-    Vec_WecForEachLevel( vCubes, vCube, i )
-        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
-            Vec_WecPush( vLits, Lit, i );
-    *pvCounts = vCounts;
-    return vLits;
-}
-Hsh_VecMan_t * Fx_ManCreateDivisors( Vec_Wec_t * vCubes, Vec_Flt_t ** pvWeights, int * pnPairsS, int * pnPairsD, int * pnDivsS )
-{
-    Hsh_VecMan_t * p;
-    Vec_Flt_t * vWeights;
-    Vec_Int_t * vCube, * vCube2, * vFree;
-    int i, k, n, Lit, Lit2, iDiv, Base;
-    p = Hsh_VecManStart( 10000 );
-    vWeights = Vec_FltAlloc( 10000 );
-    vFree = Vec_IntAlloc( 100 );
-    // create two-literal divisors
-    Vec_WecForEachLevel( vCubes, vCube, i )
-        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
-            Vec_IntForEachEntryStart( vCube, Lit2, n, k+1 )
-            {
-                assert( Lit < Lit2 );
-                Vec_IntClear( vFree );
-                Vec_IntPush( vFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) );
-                Vec_IntPush( vFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) );
-                iDiv = Hsh_VecManAdd( p, vFree );
-                if ( Vec_FltSize(vWeights) == iDiv )
-                    Vec_FltPush(vWeights, -2);
-                assert( iDiv < Vec_FltSize(vWeights) );
-                Vec_FltAddToEntry( vWeights, iDiv, 1 );
-                (*pnPairsS)++;
-            }
-    *pnDivsS = Vec_FltSize(vWeights);
-    // create two-cube divisors
-    Vec_WecForEachLevel( vCubes, vCube, i )
+    int i, Lit;
+    *pLit0 = -1;
+    *pLit1 = -1;
+    Vec_IntForEachEntry( vDiv, Lit, i )
     {
-        Vec_WecForEachLevelStart( vCubes, vCube2, k, i+1 )
-            if ( Vec_IntEntry(vCube, 0) == Vec_IntEntry(vCube2, 0) )
-            {
-//                extern void Fx_PrintDivOne( Vec_Int_t * p );
-                Base = Fx_ManDivFindCubeFree( vCube, vCube2, vFree );
-//                printf( "Cubes %2d %2d : ", i, k );
-//                Fx_PrintDivOne( vFree ); printf( "\n" );
-
-//                if ( Vec_IntSize(vFree) == 4 )
-//                    Fx_ManDivCanonicize( vFree );
-                iDiv = Hsh_VecManAdd( p, vFree );
-                if ( Vec_FltSize(vWeights) == iDiv )
-                    Vec_FltPush(vWeights, -Vec_IntSize(vFree));
-                assert( iDiv < Vec_FltSize(vWeights) );
-                Vec_FltAddToEntry( vWeights, iDiv, Base + Vec_IntSize(vFree) - 1 );
-                (*pnPairsD)++;
-            }
-            else
-                break;
+        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;
     }
-    Vec_IntFree( vFree );
-    *pvWeights = vWeights;
-    return p;
 }
-Vec_Que_t * Fx_ManCreateQueue( Vec_Flt_t * vWeights )
+static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv )
 {
-    Vec_Que_t * p;
-    float Weight;
-    int i;
-    p = Vec_QueAlloc( Vec_FltSize(vWeights) );
-    Vec_QueSetCosts( p, Vec_FltArray(vWeights) );
-    Vec_FltForEachEntry( vWeights, Weight, i )
-        if ( Weight > 0.0 )
-            Vec_QuePush( p, i );
-    return p;
+    int i, Lit, Count = 0;
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) );
+    return Count;
+}
+static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_Int_t * vDiv )
+{
+    int i, Lit;
+//    Vec_IntClear( vCube );
+//    Vec_IntClear( vCube2 );
+    Vec_IntForEachEntry( vDiv, Lit, i )
+        if ( Abc_LitIsCompl(Lit) )
+            Vec_IntPush( vCube2, Abc_Lit2Var(Lit) );
+        else
+            Vec_IntPush( vCube, Abc_Lit2Var(Lit) );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Removes 0-size cubes and sorts them by the first entry.]
+  Synopsis    []
 
   Description []
                
@@ -532,50 +583,162 @@ Vec_Que_t * Fx_ManCreateQueue( Vec_Flt_t * vWeights )
   SeeAlso     []
 
 ***********************************************************************/
-void Vec_WecSortSpecial( Vec_Wec_t * vCubes )
+void Fx_ManCreateLiterals( Fx_Man_t * p, int nVars )
 {
     Vec_Int_t * vCube;
-    int i, k = 0;
-    Vec_WecForEachLevel( vCubes, vCube, i )
-        if ( Vec_IntSize(vCube) > 0 )
-            vCubes->pArray[k++] = *vCube;
+    int i, k, Lit, Count;
+    // find the number of variables
+    p->nVars = p->nLits = 0;
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+    {
+        assert( Vec_IntSize(vCube) > 0 );
+        p->nVars = Abc_MaxInt( p->nVars, Vec_IntEntry(vCube, 0) );
+        p->nLits += Vec_IntSize(vCube) - 1;
+        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+            p->nVars = Abc_MaxInt( p->nVars, Abc_Lit2Var(Lit) );
+    }
+//    p->nVars++;
+    assert( p->nVars < nVars );
+    p->nVars = nVars;
+    // count literals
+    p->vCounts = Vec_IntStart( 2*p->nVars );
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+            Vec_IntAddToEntry( p->vCounts, Lit, 1 );
+    // start literals
+    p->vLits = Vec_WecStart( 2*p->nVars );
+    Vec_IntForEachEntry( p->vCounts, Count, Lit )
+        Vec_IntGrow( Vec_WecEntry(p->vLits, Lit), Count );
+    // fill out literals
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+        Vec_IntForEachEntryStart( vCube, Lit, k, 1 )
+            Vec_WecPush( p->vLits, Lit, i );
+    // create mapping of variable into the first cube
+    p->vVarCube = Vec_IntStartFull( p->nVars );
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+        if ( Vec_IntEntry(p->vVarCube, Vec_IntEntry(vCube, 0)) == -1 )
+            Vec_IntWriteEntry( p->vVarCube, Vec_IntEntry(vCube, 0), i );
+}
+int Fx_ManCubeSingleCubeDivisors( Fx_Man_t * p, Vec_Int_t * vPivot, int fRemove, int fUpdate )
+{
+    int k, n, Lit, Lit2, iDiv;
+    if ( Vec_IntSize(vPivot) < 2 )
+        return 0;
+    Vec_IntForEachEntryStart( vPivot, Lit, k, 1 )
+    Vec_IntForEachEntryStart( vPivot, Lit2, n, k+1 )
+    {
+        assert( Lit < Lit2 );
+        Vec_IntClear( p->vFree );
+        Vec_IntPush( p->vFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) );
+        Vec_IntPush( p->vFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) );
+        iDiv = Hsh_VecManAdd( p->pHash, p->vFree );
+        if ( !fRemove )
+        {
+            if ( Vec_FltSize(p->vWeights) == iDiv )
+            {
+                float * pArray = Vec_FltArray(p->vWeights);
+                Vec_FltPush(p->vWeights, -2);
+                if ( p->vPrio && pArray != Vec_FltArray(p->vWeights) )
+                    Vec_QueSetCosts( p->vPrio, Vec_FltArray(p->vWeights) );
+                p->nDivsS++;
+            }
+            assert( iDiv < Vec_FltSize(p->vWeights) );
+            Vec_FltAddToEntry( p->vWeights, iDiv, 1 );
+            p->nPairsS++;
+        }
         else
-            ABC_FREE( vCube->pArray );
-    Vec_WecShrink( vCubes, k );
-    Vec_WecSortByFirstInt( vCubes, 0 );
+        {
+            assert( iDiv < Vec_FltSize(p->vWeights) );
+            Vec_FltAddToEntry( p->vWeights, iDiv, -1 );
+            p->nPairsS--;
+        }
+        if ( fUpdate )
+        {
+            if ( Vec_QueIsMember(p->vPrio, iDiv) )
+                Vec_QueUpdate( p->vPrio, iDiv );
+            else if ( !fRemove )
+                Vec_QuePush( p->vPrio, iDiv );
+        }
+    }
+    return Vec_IntSize(vPivot) * (Vec_IntSize(vPivot) - 1) / 2;
 }
-
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the data-structure when divisor is selected.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
+void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, int fRemove, int fUpdate )
 {
-//    Vec_Int_t * vDiv = Hsh_VecReadEntry( p->pHash, iDiv );
-
-    // select pivot variables
-
-    // collect single-cube-divisor cubes
-
-    // collect double-cube-divisor cube pairs
-
-    // subtract old costs
-
-    // create updated single-cube divisor cubes
-
-    // create updated double-cube-divisor cube pairs
-
-    // add new costs
-
-    // assert (divisor weight == old cost - new cost)
+    Vec_Int_t * vCube;
+    int i, iDiv, Base;
+    Vec_WecForEachLevelStart( p->vCubes, vCube, i, iFirst )
+    {
+        if ( Vec_IntSize(vCube) == 0 || vCube == vPivot )
+            continue;
+        if ( Vec_WecIntHasMark(vCube) && Vec_WecIntHasMark(vPivot) && vCube > vPivot )
+            continue;
+        if ( Vec_IntEntry(vCube, 0) != Vec_IntEntry(vPivot, 0) )
+            break;
+        Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vFree );
+/*
+        if ( fUpdate )
+        {
+            printf( "Cubes %2d %2d : ", Vec_WecLevelId(p->vCubes, vCube), Vec_WecLevelId(p->vCubes, vPivot) );
+            if ( fRemove )
+                printf( "Rem " );
+            else
+                printf( "Add " );
+            Fx_PrintDivOne( p->vFree ); printf( "\n" );
+        }
+*/
+//        if ( Vec_IntSize(p->vFree) == 4 )
+//            Fx_ManDivCanonicize( p->vFree );
+        iDiv = Hsh_VecManAdd( p->pHash, p->vFree );
+        if ( !fRemove )
+        {
+            if ( iDiv == Vec_FltSize(p->vWeights) )
+            {
+                float * pArray = Vec_FltArray(p->vWeights);
+                Vec_FltPush(p->vWeights, -Vec_IntSize(p->vFree));
+                if ( p->vPrio && pArray != Vec_FltArray(p->vWeights) )
+                    Vec_QueSetCosts( p->vPrio, Vec_FltArray(p->vWeights) );
+            }
+            assert( iDiv < Vec_FltSize(p->vWeights) );
+            Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vFree) - 1 );
+            p->nPairsD++;
+        }
+        else
+        {
+            assert( iDiv < Vec_FltSize(p->vWeights) );
+            Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vFree) - 1) );
+            p->nPairsD--;
+        }
+        if ( fUpdate )
+        {
+            if ( Vec_QueIsMember(p->vPrio, iDiv) )
+                Vec_QueUpdate( p->vPrio, iDiv );
+            else if ( !fRemove )
+                Vec_QuePush( p->vPrio, iDiv );
+        }
+    }
+}
+void Fx_ManCreateDivisors( Fx_Man_t * p )
+{
+    Vec_Int_t * vCube;
+    float Weight;
+    int i;
+    // alloc hash table
+    assert( p->pHash == NULL );
+    p->pHash = Hsh_VecManStart( 1000 );
+    p->vWeights = Vec_FltAlloc( 1000 );
+    // create single-cube two-literal divisors
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+        Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 0 ); // add - no update
+    assert( p->nDivsS == Vec_FltSize(p->vWeights) );
+    // create two-cube divisors
+    Vec_WecForEachLevel( p->vCubes, vCube, i )
+        Fx_ManCubeDoubleCubeDivisors( p, i+1, vCube, 0, 0 ); // add - no update
+    // create queue with all divisors
+    p->vPrio = Vec_QueAlloc( Vec_FltSize(p->vWeights) );
+    Vec_QueSetCosts( p->vPrio, Vec_FltArray(p->vWeights) );
+    Vec_FltForEachEntry( p->vWeights, Weight, i )
+        if ( Weight > 0.0 )
+            Vec_QuePush( p->vPrio, i );
 }
 
 
@@ -590,16 +753,19 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
   SeeAlso     []
 
 ***********************************************************************/
-Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes, int nVars )
+Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes )
 {
     Fx_Man_t * p;
     p = ABC_CALLOC( Fx_Man_t, 1 );
-    p->nVars  = nVars;
-    p->vCubes = vCubes;
-    p->vLits  = Fx_ManCreateLiterals( vCubes, &p->vCounts );
-    p->pHash  = Fx_ManCreateDivisors( vCubes, &p->vWeights, &p->nPairsS, &p->nPairsD, &p->nDivsS );
-    p->vPrio  = Fx_ManCreateQueue( p->vWeights );
-    p->vCube  = Vec_IntAlloc( 100 );
+    p->vCubes   = vCubes;
+    // temporary data
+    p->vCubesS  = Vec_IntAlloc( 100 );
+    p->vCubesD  = Vec_IntAlloc( 100 );
+    p->vPart0   = Vec_IntAlloc( 100 );
+    p->vPart1   = Vec_IntAlloc( 100 );
+    p->vFree    = Vec_IntAlloc( 100 );
+    p->vCube    = Vec_IntAlloc( 100 );
+    p->vDiv     = Vec_IntAlloc( 100 );
     return p;
 }
 void Fx_ManStop( Fx_Man_t * p )
@@ -610,7 +776,15 @@ void Fx_ManStop( Fx_Man_t * p )
     Hsh_VecManStop( p->pHash );
     Vec_FltFree( p->vWeights );
     Vec_QueFree( p->vPrio );
+    Vec_IntFree( p->vVarCube );
+    // temporary data
+    Vec_IntFree( p->vCubesS );
+    Vec_IntFree( p->vCubesD );
+    Vec_IntFree( p->vPart0 );
+    Vec_IntFree( p->vPart1 );
+    Vec_IntFree( p->vFree );
     Vec_IntFree( p->vCube );
+    Vec_IntFree( p->vDiv );
     ABC_FREE( p );
 }
 
@@ -625,71 +799,224 @@ void Fx_ManStop( Fx_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static void Fx_PrintMatrix( Vec_Wec_t * vCubes, int nObjs )
+static inline void Fx_ManCompressCubes( Vec_Wec_t * vCubes, Vec_Int_t * vLit2Cube )
 {
-    Vec_Int_t * vCube;
-    char * pLine;
-    int i, v, Lit;
-    printf( "         " );
-    for ( i = 0; i < Abc_MinInt(nObjs, 26); i++ )
-        printf( "%c", 'a' + i );
-    printf( "\n" );
-    pLine = ABC_CALLOC( char, nObjs + 1 );
-    Vec_WecForEachLevel( vCubes, vCube, i )
+    int i, CubeId, k = 0;
+    Vec_IntForEachEntry( vLit2Cube, CubeId, i )
+        if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 )
+            Vec_IntWriteEntry( vLit2Cube, k++, CubeId );
+    Vec_IntShrink( vLit2Cube, k );
+}
+static inline int Fx_ManGetCubeVar( Vec_Wec_t * vCubes, int iCube )        { return Vec_IntEntry( Vec_WecEntry(vCubes, iCube), 0 );      }
+void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t * vPart1, Vec_Int_t * vPairs, Vec_Int_t * vDiv, Vec_Int_t * vFree )
+{
+    int * pBeg1 = vPart0->pArray;
+    int * pBeg2 = vPart1->pArray;
+    int * pEnd1 = vPart0->pArray + vPart0->nSize;
+    int * pEnd2 = vPart1->pArray + vPart1->nSize;
+    int i, k, i_, k_, Counter = 0;
+    Vec_IntClear( vPairs );
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
     {
-        memset( pLine, '-', nObjs );
-        Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+        int CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1);
+        int CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2);
+        if ( CubeId1 == CubeId2 )
         {
-            assert( Abc_Lit2Var(Lit) < nObjs );
-            pLine[Abc_Lit2Var(Lit)] = Abc_LitIsCompl(Lit) ? '0' : '1';
+            for ( i = 1; pBeg1+i < pEnd1; i++ )
+                if ( CubeId1 != Fx_ManGetCubeVar(vCubes, pBeg1[i]) )
+                    break;
+            for ( k = 1; pBeg2+k < pEnd2; k++ )
+                if ( CubeId1 != Fx_ManGetCubeVar(vCubes, pBeg2[k]) )
+                    break;
+            for ( i_ = 0; i_ < i; i_++ )
+            for ( k_ = 0; k_ < k; k_++ )
+            {
+                if ( pBeg1[i_] == pBeg2[k_] )
+                    continue;
+                Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vFree );
+                if ( !Vec_IntEqual( vDiv, vFree ) )
+                    continue;
+                Vec_IntPush( vPairs, pBeg1[i_] );
+                Vec_IntPush( vPairs, pBeg2[k_] );
+            }
+            pBeg1 += i;
+            pBeg2 += k;
         }
-        printf( "%6d : %s %4d\n", i, pLine, Vec_IntEntry(vCube, 0) );
+        else if ( CubeId1 < CubeId2 )
+            pBeg1++;
+        else 
+            pBeg2++;
     }
-    ABC_FREE( pLine );
 }
-static inline char Fx_PrintDivLit( int Lit ) { return (Abc_LitIsCompl(Abc_Lit2Var(Lit)) ? 'A' : 'a') + Abc_Lit2Var(Abc_Lit2Var(Lit)); }
-static inline void Fx_PrintDivOne( Vec_Int_t * vDiv )
-{
-    int i, Lit;
-    Vec_IntForEachEntry( vDiv, Lit, i )
-        if ( !Abc_LitIsCompl(Lit) )
-            printf( "%c", Fx_PrintDivLit(Lit) );
-    printf( " + " );
-    Vec_IntForEachEntry( vDiv, Lit, i )
-        if ( Abc_LitIsCompl(Lit) )
-            printf( "%c", Fx_PrintDivLit(Lit) );
-}
-static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv )
-{
-    printf( "Div %6d : ", iDiv );
-    printf( "Cost %4d  ", (int)Vec_FltEntry(p->vWeights, iDiv) );
-    Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) );
-    printf( "\n" );
-}
-static void Fx_PrintDivisors( Fx_Man_t * p )
-{
-    int iDiv;
-    for ( iDiv = 0; iDiv < Vec_FltSize(p->vWeights); iDiv++ )
-        Fx_PrintDiv( p, iDiv );
-}
-static void Fx_PrintStats( Fx_Man_t * p, clock_t clk )
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the data-structure when divisor is selected.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
 {
-    printf( "Cubes =%6d  ", Vec_WecSizeUsed(p->vCubes) );
-    printf( "Lits  =%6d  ", Vec_WecSizeUsed(p->vLits) );
-    printf( "Divs  =%6d  ", Hsh_VecSize(p->pHash) );
-    printf( "Divs+ =%6d  ", Vec_QueSize(p->vPrio) );
-    printf( "DivsS =%6d  ", p->nDivsS );
-    printf( "PairS =%6d  ", p->nPairsS );
-    printf( "PairD =%6d  ", p->nPairsD );
-    Abc_PrintTime( 1, "Time", clk );
-//    printf( "\n" );
+    Vec_Int_t * vCube, * vCube2, * vLitP, * vLitN;
+    Vec_Int_t * vDiv = p->vDiv;
+    int nLitsNew = p->nLits - (int)Vec_FltEntry(p->vWeights, iDiv);
+    int i, k, Lit0, Lit1, iVarNew, RetValue;
+    // get the divisor
+    Vec_IntClear( vDiv );
+    Vec_IntAppend( vDiv, Hsh_VecReadEntry(p->pHash, iDiv) );
+    // select pivot variables
+    Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 );
+    assert( Lit0 >= 0 && Lit1 >= 0 );
+
+    // collect single-cube-divisor cubes
+    Vec_IntClear( p->vCubesS );
+    if ( Vec_IntSize(vDiv) == 2 )
+    {
+        Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)) );
+        Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)) );
+        Vec_IntTwoRemoveCommon( Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)), Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)), p->vCubesS );
+    }
+//Vec_IntPrint( p->vCubesS );
+
+    // collect double-cube-divisor cube pairs
+    Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit0) );
+    Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit1) );
+    Fx_ManFindCommonPairs( p->vCubes, Vec_WecEntry(p->vLits, Lit0), Vec_WecEntry(p->vLits, Lit1), p->vCubesD, vDiv, p->vFree );
+//Vec_IntPrint( p->vCubesD );
+
+    // subtract cost of single-cube divisors
+    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
+        Fx_ManCubeSingleCubeDivisors( p, vCube, 1, 1 );  // remove - update
+    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
+        Fx_ManCubeSingleCubeDivisors( p, vCube, 1, 1 );  // remove - update
+
+    // mark the cubes to be removed
+    Vec_WecMarkLevels( p->vCubes, p->vCubesS );
+    Vec_WecMarkLevels( p->vCubes, p->vCubesD );
+
+    // subtract cost of double-cube divisors
+    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
+        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1 );  // remove - update
+    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
+        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1 );  // remove - update
+
+    // unmark the cubes to be removed
+    Vec_WecUnmarkLevels( p->vCubes, p->vCubesS );
+    Vec_WecUnmarkLevels( p->vCubes, p->vCubesD );
+
+    // create new divisor
+    iVarNew = Vec_WecSize( p->vLits ) / 2;
+    assert( Vec_IntSize(p->vVarCube) == iVarNew );
+    Vec_IntPush( p->vVarCube, Vec_WecSize(p->vCubes) );
+    vCube = Vec_WecPushLevel( p->vCubes );
+    Vec_IntPush( vCube, iVarNew );
+    if ( Vec_IntSize(vDiv) == 2 )
+    {
+        Vec_IntPush( vCube, Abc_LitNot(Lit0) );
+        Vec_IntPush( vCube, Abc_LitNot(Lit1) );
+    }
+    else
+    {
+        vCube2 = Vec_WecPushLevel( p->vCubes );
+        vCube = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 );
+        Vec_IntPush( vCube2, iVarNew );
+        Fx_ManDivAddLits( vCube, vCube2, vDiv );
+    }
+    // do not add new cubes to the matrix 
+    p->nLits += Vec_IntSize( vDiv );
+    // create new literals
+    vLitP = Vec_WecPushLevel( p->vLits );
+    vLitN = Vec_WecPushLevel( p->vLits );
+    vLitP = Vec_WecEntry( p->vLits, Vec_WecSize(p->vLits) - 2 );
+    // create updated single-cube divisor cubes
+    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
+    {
+        RetValue  = Vec_IntRemove1( vCube, Abc_LitNot(Lit0) );
+        RetValue += Vec_IntRemove1( vCube, Abc_LitNot(Lit1) );
+        assert( RetValue == 2 );
+        Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
+        Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) );
+        p->nLits--;
+    }
+    // create updated double-cube divisor cube pairs
+    k = 0;
+    assert( Vec_IntSize(p->vCubesD) % 2 == 0 );
+    Fx_ManForEachPairVec( p->vCubesD, p->vCubes, vCube, vCube2, i )
+    {
+        RetValue  = Fx_ManDivRemoveLits( vCube, vDiv );  // cube 2*i
+        RetValue += Fx_ManDivRemoveLits( vCube2, vDiv ); // cube 2*i+1
+        assert( RetValue == Vec_IntSize(vDiv) );
+        if ( Vec_IntSize(vDiv) == 2 )
+        {
+            Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) );
+            Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) );
+        }
+        else
+        {
+            Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
+            Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) );
+        }
+        p->nLits -= Vec_IntSize(vDiv) + Vec_IntSize(vCube2) - 2;
+        // remove second cube
+        Vec_IntWriteEntry( p->vCubesD, k++, Vec_WecLevelId(p->vCubes, vCube) );
+        Vec_IntClear( vCube2 ); 
+    }
+    assert( k == Vec_IntSize(p->vCubesD) / 2 );
+    Vec_IntShrink( p->vCubesD, k );
+    Vec_IntSort( p->vCubesD, 0 );
+
+    // add cost of single-cube divisors
+    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
+        Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 );  // add - update
+    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
+        Fx_ManCubeSingleCubeDivisors( p, vCube, 0, 1 );  // add - update
+
+    // mark the cubes to be removed
+    Vec_WecMarkLevels( p->vCubes, p->vCubesS );
+    Vec_WecMarkLevels( p->vCubes, p->vCubesD );
+
+    // add cost of double-cube divisors
+    Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
+        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 0, 1 );  // add - update
+    Fx_ManForEachCubeVec( p->vCubesD, p->vCubes, vCube, i )
+        Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 0, 1 );  // add - update
+
+    // unmark the cubes to be removed
+    Vec_WecUnmarkLevels( p->vCubes, p->vCubesS );
+    Vec_WecUnmarkLevels( p->vCubes, p->vCubesD );
+
+    // add cost of the new divisor
+    if ( Vec_IntSize(vDiv) > 2 )
+    {
+        vCube  = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 2 );
+        vCube2 = Vec_WecEntry( p->vCubes, Vec_WecSize(p->vCubes) - 1 );
+        Fx_ManCubeSingleCubeDivisors( p, vCube,  0, 1 );  // add - update
+        Fx_ManCubeSingleCubeDivisors( p, vCube2, 0, 1 );  // add - update
+        Vec_IntForEachEntryStart( vCube, Lit0, i, 1 )
+            Vec_WecPush( p->vLits, Lit0, Vec_WecLevelId(p->vCubes, vCube) );
+        Vec_IntForEachEntryStart( vCube2, Lit0, i, 1 )
+            Vec_WecPush( p->vLits, Lit0, Vec_WecLevelId(p->vCubes, vCube2) );
+    }
+
+    // remove these cubes from the lit array of the divisor
+    Vec_IntForEachEntry( vDiv, Lit0, i )
+        Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_Lit2Var(Lit0)), p->vCubesD );
+
+    assert( p->nLits == nLitsNew ); // new SOP lits == old SOP lits - divisor weight
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Implements the traditional fast_extract algorithm.]
 
-  Description []
+  Description [J. Rajski and J. Vasudevamurthi, "The testability-
+  preserving concurrent decomposition and factorization of Boolean
+  expressions", IEEE TCAD, Vol. 11, No. 6, June 1992, pp. 778-793.]
                
   SideEffects []
 
@@ -698,27 +1025,32 @@ static void Fx_PrintStats( Fx_Man_t * p, clock_t clk )
 ***********************************************************************/
 int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose )
 {
+    int fVeryVerbose = 0;
     Fx_Man_t * p;
     clock_t clk = clock();
-    p = Fx_ManStart( vCubes, nVars );
-
+    // initialize the data-structure
+    p = Fx_ManStart( vCubes );
+    Fx_ManCreateLiterals( p, nVars );
+    Fx_ManCreateDivisors( p );
+    if ( fVeryVerbose )
+        Fx_PrintMatrix( p );
     if ( fVerbose )
-    {
-        Fx_PrintMatrix( vCubes, nVars );
-        Fx_PrintDivisors( p );
-        printf( "Selecting divisors:\n" );
-    }
-
-    Fx_PrintStats( p, clock() - clk );
+        Fx_PrintStats( p, clock() - clk );
+    // perform extraction
     while ( Vec_QueTopCost(p->vPrio) > 0.0 )
     {
         int iDiv = Vec_QuePop(p->vPrio);
         if ( fVerbose )
             Fx_PrintDiv( p, iDiv );
         Fx_ManUpdate( p, iDiv );
+        if ( fVeryVerbose )
+            Fx_PrintMatrix( p );
+        if ( fVerbose )
+            Fx_PrintStats( p, clock() - clk );
     }
-
     Fx_ManStop( p );
+    // return the result
+    Vec_WecRemoveEmpty( vCubes );
     return 1;
 }
 
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index d6744536..b2a56a7d 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -83,9 +83,9 @@ int Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
     assert( Abc_NtkIsLogic(pNtk) );
     // if the network is already in the SOP form, it may come from BLIF file
-    // and it may not be SCC-ABC_FREE, in which case FXU will not work correctly
+    // and it may not be SCC-free, in which case FXU will not work correctly
     if ( Abc_NtkIsSopLogic(pNtk) )
-    { // to make sure the SOPs are SCC-ABC_FREE
+    { // to make sure the SOPs are SCC-free
 //        Abc_NtkSopToBdd(pNtk);
 //        Abc_NtkBddToSop(pNtk);
     }
diff --git a/src/bool/kit/kitSop.c b/src/bool/kit/kitSop.c
index 21ea69b8..f6e33496 100644
--- a/src/bool/kit/kitSop.c
+++ b/src/bool/kit/kitSop.c
@@ -299,7 +299,7 @@ static inline unsigned Kit_SopCommonCube( Kit_Sop_t * cSop )
 
 /**Function*************************************************************
 
-  Synopsis    [Makes the cover cube-ABC_FREE.]
+  Synopsis    [Makes the cover cube-free.]
 
   Description []
                
@@ -322,7 +322,7 @@ void Kit_SopMakeCubeFree( Kit_Sop_t * cSop )
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the cover is cube-ABC_FREE.]
+  Synopsis    [Checks if the cover is cube-free.]
 
   Description []
                
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 03427a0b..2fe15792 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -885,6 +885,20 @@ static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
     p->nSize--;
     return 1;
 }
+static inline int Vec_IntRemove1( Vec_Int_t * p, int Entry )
+{
+    int i;
+    for ( i = 1; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            break;
+    if ( i >= p->nSize )
+        return 0;
+    assert( i < p->nSize );
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -1298,6 +1312,18 @@ static inline int Vec_IntTwoCountCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
     }
     return Counter;
 }
+
+/**Function*************************************************************
+
+  Synopsis    [Collects common entries.]
+
+  Description [Assumes that the vectors are sorted in the increasing order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
 {
     int * pBeg1 = vArr1->pArray;
@@ -1319,6 +1345,77 @@ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Ve
 
 /**Function*************************************************************
 
+  Synopsis    [Collects and removes common entries]
+
+  Description [Assumes that the vectors are sorted in the increasing order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntTwoRemoveCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    int * pBeg1New = vArr1->pArray;
+    int * pBeg2New = vArr2->pArray;
+    Vec_IntClear( vArr );
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg1New++ = *pBeg1++;
+        else 
+            *pBeg2New++ = *pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg1New++ = *pBeg1++;
+    while ( pBeg2 < pEnd2 )
+        *pBeg2New++ = *pBeg2++;
+    Vec_IntShrink( vArr1, pBeg1New - vArr1->pArray );
+    Vec_IntShrink( vArr2, pBeg2New - vArr2->pArray );
+    return Vec_IntSize(vArr);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes entries of the second one from the first one.]
+
+  Description [Assumes that the vectors are sorted in the increasing order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntTwoRemove( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
+{
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    int * pBeg1New = vArr1->pArray;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            pBeg1++, pBeg2++;
+        else if ( *pBeg1 < *pBeg2 )
+            *pBeg1New++ = *pBeg1++;
+        else 
+            pBeg2++;
+    }
+    while ( pBeg1 < pEnd1 )
+        *pBeg1New++ = *pBeg1++;
+    Vec_IntShrink( vArr1, pBeg1New - vArr1->pArray );
+    return Vec_IntSize(vArr1);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the result of merging the two vectors.]
 
   Description [Assumes that the vectors are sorted in the increasing order.]
@@ -1358,7 +1455,7 @@ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the result of merging the two vectors.]
+  Synopsis    [Returns the result of splitting of the two vectors.]
 
   Description [Assumes that the vectors are sorted in the increasing order.]
                
diff --git a/src/misc/vec/vecQue.h b/src/misc/vec/vecQue.h
index 83be97a8..445c6fb3 100644
--- a/src/misc/vec/vecQue.h
+++ b/src/misc/vec/vecQue.h
@@ -94,7 +94,7 @@ static inline void Vec_QueFreeP( Vec_Que_t ** p )
 }
 static inline void Vec_QueSetCosts( Vec_Que_t * p, float * pCosts )
 {
-    assert( p->pCostsFlt == NULL );
+//    assert( p->pCostsFlt == NULL );
     p->pCostsFlt = pCosts;
 }
 static inline void Vec_QueGrow( Vec_Que_t * p, int nCapMin )
@@ -215,12 +215,15 @@ static inline void Vec_QueUpdate( Vec_Que_t * p, int v )
 ***********************************************************************/
 static inline int Vec_QueIsMember( Vec_Que_t * p, int v )
 {
-    return (int)( p->pOrder[v] >= 0 );
+    assert( v >= 0 );
+    return (int)( v < p->nCap && p->pOrder[v] >= 0 );
 }
 static inline void Vec_QuePush( Vec_Que_t * p, int v )
 {
-    if ( p->nSize == p->nCap )
-        Vec_QueGrow( p, 2 * p->nCap );
+    if ( p->nSize >= p->nCap )
+        Vec_QueGrow( p, Abc_MaxInt(p->nSize+1, 2*p->nCap) );
+    if ( v >= p->nCap )
+        Vec_QueGrow( p, Abc_MaxInt(v+1, 2*p->nCap) );
     assert( p->nSize < p->nCap );
     assert( p->pOrder[v] == -1 );
     assert( p->pHeap[p->nSize] == -1 );
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index 34d5d956..8a924f90 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -54,6 +54,8 @@ struct Vec_Wec_t_
 // iterators through levels 
 #define Vec_WecForEachLevel( vGlob, vVec, i )                                              \
     for ( i = 0; (i < Vec_WecSize(vGlob)) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ )
+#define Vec_WecForEachLevelVec( vLevels, vGlob, vVec, i )                                  \
+    for ( i = 0; (i < Vec_IntSize(vLevels)) && (((vVec) = Vec_WecEntry(vGlob, Vec_IntEntry(vLevels, i))), 1); i++ )
 #define Vec_WecForEachLevelStart( vGlob, vVec, i, LevelStart )                             \
     for ( i = LevelStart; (i < Vec_WecSize(vGlob)) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ )
 #define Vec_WecForEachLevelStop( vGlob, vVec, i, LevelStop )                               \
@@ -158,6 +160,27 @@ static inline int Vec_WecEntryEntry( Vec_Wec_t * p, int i, int k )
   SeeAlso     []
 
 ***********************************************************************/
+static inline Vec_Int_t * Vec_WecArray( Vec_Wec_t * p )
+{
+    return p->pArray;
+}
+static inline int Vec_WecLevelId( Vec_Wec_t * p, Vec_Int_t * vLevel )
+{
+    assert( p->pArray <= vLevel && vLevel < p->pArray + p->nSize );
+    return vLevel - p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_WecCap( Vec_Wec_t * p )
 {
     return p->nCap;
@@ -239,14 +262,21 @@ static inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry )
 {
     if ( p->nSize < Level + 1 )
     {
-        Vec_WecGrow( p, Level + 1 );
+        Vec_WecGrow( p, Abc_MaxInt(2*p->nCap, Level + 1) );
         p->nSize = Level + 1;
     }
     Vec_IntPush( Vec_WecEntry(p, Level), Entry );
 }
 static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p )
 {
-    Vec_WecGrow( p, ++p->nSize );
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_WecGrow( p, 16 );
+        else
+            Vec_WecGrow( p, 2 * p->nCap );
+    }
+    ++p->nSize;
     return Vec_WecEntryLast( p );
 }
 
@@ -557,6 +587,67 @@ static inline Vec_Ptr_t * Vec_WecConvertToVecPtr( Vec_Wec_t * p )
     return vCopy;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Temporary vector marking.]
+
+  Description [The vector should be static when the marking is used.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int  Vec_WecIntHasMark( Vec_Int_t * vVec ) { return (vVec->nCap >> 30) & 1; }
+static inline void Vec_WecIntSetMark( Vec_Int_t * vVec ) { vVec->nCap |= (1<<30);         }
+static inline void Vec_WecIntXorMark( Vec_Int_t * vVec ) { vVec->nCap ^= (1<<30);         }
+static inline void Vec_WecMarkLevels( Vec_Wec_t * vCubes, Vec_Int_t * vLevels )
+{
+    Vec_Int_t * vCube;
+    int i;
+    Vec_WecForEachLevelVec( vLevels, vCubes, vCube, i )
+    {
+        assert( !Vec_WecIntHasMark( vCube ) );
+        Vec_WecIntXorMark( vCube );
+    }
+}
+static inline void Vec_WecUnmarkLevels( Vec_Wec_t * vCubes, Vec_Int_t * vLevels )
+{
+    Vec_Int_t * vCube;
+    int i;
+    Vec_WecForEachLevelVec( vLevels, vCubes, vCube, i )
+    {
+        assert( Vec_WecIntHasMark( vCube ) );
+        Vec_WecIntXorMark( vCube );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes 0-size vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes )
+{
+    Vec_Int_t * vCube;
+    int i, k = 0;
+    Vec_WecForEachLevel( vCubes, vCube, i )
+        if ( Vec_IntSize(vCube) > 0 )
+            vCubes->pArray[k++] = *vCube;
+        else
+            ABC_FREE( vCube->pArray );
+    Vec_WecShrink( vCubes, k );
+//    Vec_WecSortByFirstInt( vCubes, 0 );
+}
+
+
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index c6fb5796..0095abf9 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -47,7 +47,7 @@ static int s_MemoryPeak;
   The entries corresponding to the PI and objects with trivial covers are NULL.
   The number of extracted covers (not exceeding p->nNodesExt) is returned. 
   Two other things are important for the correct operation of this procedure:
-  (1) The input covers do not have duplicated fanins and are SCC-ABC_FREE. 
+  (1) The input covers do not have duplicated fanins and are SCC-free. 
   (2) The fanins array contains the numbers of the fanin objects.]
                
   SideEffects []
diff --git a/src/opt/fxu/fxuPair.c b/src/opt/fxu/fxuPair.c
index d040abe9..32822592 100644
--- a/src/opt/fxu/fxuPair.c
+++ b/src/opt/fxu/fxuPair.c
@@ -89,7 +89,7 @@ void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
             pLit2 = pLit2->pHNext;
             continue;
         }
-        assert( pLit1 && pLit2 ); // this is true if the covers are SCC-ABC_FREE
+        assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
         if ( pLit1->iVar > pLit2->iVar )
         { // swap the cubes
             pCubeTemp = *ppCube1;
@@ -152,7 +152,7 @@ unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], i
   Synopsis    [Computes the hash key of the divisor represented by the pair of cubes.]
 
   Description [Goes through the variables in both cubes. Skips the identical
-  ones (this corresponds to making the cubes cube-ABC_FREE). Computes the hash 
+  ones (this corresponds to making the cubes cube-free). Computes the hash 
   value of the cubes. Assigns the number of literals in the base and in the 
   cubes without base.]
                
@@ -181,7 +181,7 @@ unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2,
         if ( pLit1 && pLit2 )
         {
             if ( pLit1->iVar == pLit2->iVar )
-            { // ensure cube-ABC_FREE
+            { // ensure cube-free
                 pLit1 = pLit1->pHNext;
                 pLit2 = pLit2->pHNext;
                 // add this literal to the base
diff --git a/src/opt/fxu/fxuSelect.c b/src/opt/fxu/fxuSelect.c
index c9945926..da55eb82 100644
--- a/src/opt/fxu/fxuSelect.c
+++ b/src/opt/fxu/fxuSelect.c
@@ -419,7 +419,7 @@ void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble,
         if ( pLit1 && pLit2 )
         {
             if ( pLit1->iVar == pLit2->iVar )
-            { // ensure cube-ABC_FREE
+            { // ensure cube-free
                 pLit1 = pLit1->pHNext;
                 pLit2 = pLit2->pHNext;
             }