New fast extract.

11 files changed, 1624 insertions, 127 deletions

diff --git a/abclib.dsp b/abclib.dsp
index f636f2eb..c7883f1f 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -259,6 +259,10 @@ SOURCE=.\src\base\abci\abcFraig.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcFx.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcFxu.c
 # End Source File
 # Begin Source File
@@ -2651,6 +2655,10 @@ SOURCE=.\src\misc\vec\vecFlt.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\vec\vecHsh.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\vec\vecInt.h
 # End Source File
 # Begin Source File
@@ -2679,6 +2687,10 @@ SOURCE=.\src\misc\vec\vecVec.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\vec\vecWec.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\vec\vecWrd.h
 # End Source File
 # End Group
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 533db448..2f785a22 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3527,13 +3527,14 @@ usage:
 ***********************************************************************/
 int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Fxu_Data_t Params, * p = &Params;
-    int c;
+    int c, fNewAlgo = 0;
     // set the defaults
     Abc_NtkSetDefaultParams( p );
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcvh")) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcnvh")) != EOF )
     {
         switch (c)
         {
@@ -3593,6 +3594,9 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
             case 'c':
                 p->fUseCompl ^= 1;
                 break;
+            case 'n':
+                fNewAlgo ^= 1;
+                break;
             case 'v':
                 p->fVerbose ^= 1;
                 break;
@@ -3615,17 +3619,25 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsLogic(pNtk) )
     {
-        Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\").\n" );
+        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;
     }
 
     // the nodes to be merged are linked into the special linked list
-    Abc_NtkFastExtract( pNtk, p );
+    if ( fNewAlgo )
+        Abc_NtkFxPerform( pNtk, p->fVerbose );
+    else
+        Abc_NtkFastExtract( pNtk, p );
     Abc_NtkFxuFreeInfo( p );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: fx [-SDNW <num>] [-sdzcvh]\n");
+    Abc_Print( -2, "usage: fx [-SDNW <num>] [-sdzcnvh]\n");
     Abc_Print( -2, "\t           performs unate fast extract on the current network\n");
     Abc_Print( -2, "\t-S <num> : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
     Abc_Print( -2, "\t-D <num> : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
@@ -3635,6 +3647,7 @@ usage:
     Abc_Print( -2, "\t-d       : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
     Abc_Print( -2, "\t-z       : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
     Abc_Print( -2, "\t-c       : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" );
+    Abc_Print( -2, "\t-n       : use new implementation of fast extract [default = %s]\n", fNewAlgo? "yes": "no" );
     Abc_Print( -2, "\t-v       : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
new file mode 100644
index 00000000..8f1c724a
--- /dev/null
+++ b/src/base/abci/abcFx.c
@@ -0,0 +1,733 @@
+/**CFile****************************************************************
+
+  FileName    [abcFx.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the fast extract package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 26, 2013.]
+
+  Revision    [$Id: abcFx.c,v 1.00 2013/04/26 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "misc/vec/vecWec.h"
+#include "misc/vec/vecQue.h"
+#include "misc/vec/vecHsh.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reroders fanins of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vOrder;
+    Abc_Obj_t * pNode;
+    char * pSop, * pSopNew;
+    char * pCube, * pCubeNew;
+    int nVars, i, v, * pOrder;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    vOrder = Vec_IntAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        pSop = (char *)pNode->pData;
+        nVars = Abc_SopGetVarNum(pSop);
+        assert( nVars == Abc_ObjFaninNum(pNode) );
+        Vec_IntClear( vOrder );
+        for ( v = 0; v < nVars; v++ )
+            Vec_IntPush( vOrder, v );
+        pOrder = Vec_IntArray(vOrder);
+        Vec_IntSelectSortCost( pOrder, nVars, &pNode->vFanins );
+        pSopNew = pCubeNew = Abc_SopStart( pNtk->pManFunc, Abc_SopGetCubeNum(pSop), nVars );
+        Abc_SopForEachCube( pSop, nVars, pCube )
+        {
+            for ( v = 0; v < nVars; v++ )
+                if ( pCube[pOrder[v]] == '0' )
+                    pCubeNew[v] = '0';
+                else if ( pCube[pOrder[v]] == '1' )
+                    pCubeNew[v] = '1';
+            pCubeNew += nVars + 3;
+        }
+        pNode->pData = pSopNew;
+        Vec_IntSort( &pNode->vFanins, 0 );
+//        Vec_IntPrint( vOrder );
+    }
+    Vec_IntFree( vOrder );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts SOP information.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk )
+{
+    Vec_Wec_t * vCubes;
+    Vec_Int_t * vCube;
+    Abc_Obj_t * pNode;
+    char * pCube, * pSop;
+    int nVars, i, v, Lit;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    vCubes = Vec_WecAlloc( 1000 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        pSop = (char *)pNode->pData;
+        nVars = Abc_SopGetVarNum(pSop);
+        assert( nVars == Abc_ObjFaninNum(pNode) );
+        if ( nVars < 2 )
+            continue;
+        Abc_SopForEachCube( pSop, nVars, pCube )
+        {
+            vCube = Vec_WecPushLevel( vCubes );
+            Vec_IntPush( vCube, Abc_ObjId(pNode) );
+            Abc_CubeForEachVar( pCube, Lit, v )
+            {
+                if ( Lit == '0' )
+                    Vec_IntPush( vCube, Abc_Var2Lit(Abc_ObjFaninId(pNode, v), 1) );
+                else if ( Lit == '1' )
+                    Vec_IntPush( vCube, Abc_Var2Lit(Abc_ObjFaninId(pNode, v), 0) );
+            }
+            Vec_IntSelectSort( Vec_IntArray(vCube) + 1, Vec_IntSize(vCube) - 1 );
+        }
+    }
+    return vCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts SOP information.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes )
+{
+    Vec_Int_t * vCube, * vPres, * vFirst, * vCount;
+    Abc_Obj_t * pNode, * pFanin;
+    char * pCube, * pSop;
+    int i, k, v, Lit, iFanin, iNodeMax = 0;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    // check that cubes have no gaps and are ordered by first node
+    Lit = -1;
+    Vec_WecForEachLevel( vCubes, vCube, i )
+    {
+        assert( Vec_IntSize(vCube) > 0 );
+        assert( Lit <= Vec_IntEntry(vCube, 0) );
+        Lit = Vec_IntEntry(vCube, 0);
+    }
+    // find the largest index
+    Vec_WecForEachLevel( vCubes, vCube, i )
+        iNodeMax = Abc_MaxInt( iNodeMax, Vec_IntEntry(vCube, 0) );
+    // quit if nothing new
+/*
+    if ( iNodeMax < Abc_NtkObjNumMax(pNtk) )
+    {
+        printf( "The network is unchanged by fast extract.\n" );
+        return;
+    }
+*/
+    // create new nodes
+    for ( i = Abc_NtkObjNumMax(pNtk); i <= iNodeMax; i++ )
+    {
+        pNode = Abc_NtkCreateNode( pNtk );
+        assert( i == (int)Abc_ObjId(pNode) );
+    }
+    // create node fanins
+    vFirst = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    vCount = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    Vec_WecForEachLevel( vCubes, vCube, i )
+    {
+        iFanin = Vec_IntEntry( vCube, 0 );
+        if ( Vec_IntEntry(vCount, iFanin) == 0 )
+            Vec_IntWriteEntry( vFirst, iFanin, i );
+        Vec_IntAddToEntry( vCount, iFanin, 1 );
+    }
+    // create node SOPs
+    vPres = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Vec_IntEntry(vCount, i) == 0 )
+        {
+            assert( Abc_ObjFaninNum(pNode) < 2 );
+            continue;
+        }
+        Abc_ObjRemoveFanins( pNode );
+        // create fanins
+        assert( Vec_IntEntry(vCount, i) > 0 );
+        for ( k = 0; k < Vec_IntEntry(vCount, i); k++ )
+        {
+            vCube = Vec_WecEntry( vCubes, Vec_IntEntry(vFirst, i) + k );
+            assert( Vec_IntEntry( vCube, 0 ) == i );
+            Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+            {
+                pFanin = Abc_NtkObj(pNtk, Abc_Lit2Var(Lit));
+                if ( Vec_IntEntry(vPres, Abc_ObjId(pFanin)) >= 0 )
+                    continue;
+                Vec_IntWriteEntry(vPres, Abc_ObjId(pFanin), Abc_ObjFaninNum(pNode));
+                Abc_ObjAddFanin( pNode, pFanin );
+            }
+        }
+        // create SOP
+        pSop = pCube = Abc_SopStart( pNtk->pManFunc, Vec_IntEntry(vCount, i), Abc_ObjFaninNum(pNode) );
+        for ( k = 0; k < Vec_IntEntry(vCount, i); k++ )
+        {
+            vCube = Vec_WecEntry( vCubes, Vec_IntEntry(vFirst, i) + k );
+            assert( Vec_IntEntry( vCube, 0 ) == i );
+            Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
+            {
+                pFanin = Abc_NtkObj(pNtk, Abc_Lit2Var(Lit));
+                iFanin = Vec_IntEntry(vPres, Abc_ObjId(pFanin));
+                assert( iFanin >= 0 && iFanin < Abc_ObjFaninNum(pNode) );
+                pCube[iFanin] = Abc_LitIsCompl(Lit) ? '0' : '1';
+            }
+            pCube += Abc_ObjFaninNum(pNode) + 3;
+        }
+        if ( Abc_SopIsComplement((char *)pNode->pData) )
+            Abc_SopComplement( pSop );
+        pNode->pData = pSop;
+        // clean fanins
+        Abc_ObjForEachFanin( pNode, pFanin, v )
+            Vec_IntWriteEntry( vPres, Abc_ObjId(pFanin), -1 );
+    }
+    Vec_IntFree( vFirst );
+    Vec_IntFree( vCount );
+    Vec_IntFree( vPres );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure the nodes do not have complemented and duplicated fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFxCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+//    Abc_NtkForEachObj( pNtk, pNode, i )
+//        Abc_ObjPrint( stdout, pNode );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( !Vec_IntCheckUniqueSmall( &pNode->vFanins ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Vec_Wec_t * vCubes;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    // check unique fanins
+    if ( !Abc_NtkFxCheck(pNtk) )
+    {
+        printf( "Abc_NtkFastExtract: Nodes have duplicated fanins. FX is not performed.\n" );
+        return 0;
+    }
+    // sweep removes useless nodes
+    Abc_NtkCleanup( pNtk, 0 );
+//    Abc_NtkOrderFanins( pNtk );
+    // collect information about the covers
+    vCubes = Abc_NtkFxExtract( pNtk );
+    // call the fast extract procedure
+    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), fVerbose ) > 0 )
+    {
+        // update the network
+        Abc_NtkFxInsert( pNtk, vCubes );
+        Vec_WecFree( vCubes );
+        if ( !Abc_NtkCheck( pNtk ) )
+            printf( "Abc_NtkFxPerform: The network check has failed.\n" );
+        return 1;
+    }
+    else
+        printf( "Warning: The network has not been changed by \"fx\".\n" );
+    Vec_WecFree( vCubes );
+    return 0;
+}
+
+
+
+
+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; 
+};
+
+/**Function*************************************************************
+
+  Synopsis    [Create literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented
+{
+    int * A = Vec_IntArray(vFree);
+    int C[4] = { Abc_Lit2Var(A[0]), Abc_Lit2Var(A[1]), Abc_Lit2Var(A[2]), Abc_Lit2Var(A[3]) };
+    int L[4] = { Abc_Lit2Var(A[0]), Abc_Lit2Var(A[1]), Abc_Lit2Var(A[2]), Abc_Lit2Var(A[3]) };
+    int V[4] = { Abc_Lit2Var(L[0]), Abc_Lit2Var(L[1]), Abc_Lit2Var(L[2]), Abc_Lit2Var(L[3]) };
+    assert( Vec_IntSize(vFree) == 4 );
+    if ( V[0] == V[1] && V[2] == V[3] ) // 2,2,2
+    {
+        assert( !Abc_LitIsCompl(L[0]) );
+        assert(  Abc_LitIsCompl(L[1]) );
+        if ( !Abc_LitIsCompl(L[2]) )
+        {
+            C[2] ^= 2;
+            C[3] ^= 2;
+            return 1;
+        }
+        return 0;
+    }
+    if ( V[0] == V[1] )
+    {
+        assert( V[0] != V[2] && V[0] != V[3] );
+        if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) && Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) )  // 2,2,3
+        {
+            if ( Abc_LitIsCompl(Abc_Lit2Var(L[0])) == Abc_LitIsCompl(Abc_Lit2Var(L[2])) )
+            {
+                L[2] = Abc_LitNot(L[2]);
+                L[3] = Abc_LitNot(L[3]);
+                return 1;
+            }
+            return 0;
+        }
+    }
+    if ( V[0] == V[2] )
+    {
+    }
+    if ( V[0] == V[3] )
+    {
+    }
+    if ( V[1] == V[2] )
+    {
+    }
+    if ( V[1] == V[3] )
+    {
+    }
+    if ( V[2] == V[3] )
+    {
+    }
+    return 0;
+}
+
+/**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;
+    int * pBeg2 = vArr2->pArray + 1;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    int Counter = 0, fAttr0 = 0, fAttr1 = 1;
+    Vec_IntClear( vFree );
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            pBeg1++, pBeg2++, Counter++;
+        else if ( *pBeg1 < *pBeg2 )
+            Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
+        else 
+        {
+            if ( Vec_IntSize(vFree) == 0 )
+                fAttr0 = 1, fAttr1 = 0;
+            Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
+        }
+    }
+    while ( pBeg1 < pEnd1 )
+        Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
+    while ( pBeg2 < pEnd2 )
+        Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
+    assert( Vec_IntSize(vFree) > 1 );
+    assert( !Abc_LitIsCompl(Vec_IntEntry(vFree, 0)) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Fx_ManCreateLiterals( Vec_Wec_t * vCubes, Vec_Int_t ** pvCounts )
+{
+    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 )
+    {
+        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;
+    }
+    Vec_IntFree( vFree );
+    *pvWeights = vWeights;
+    return p;
+}
+Vec_Que_t * Fx_ManCreateQueue( Vec_Flt_t * vWeights )
+{
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes 0-size cubes and sorts them by the first entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Vec_WecSortSpecial( 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 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the data-structure when divisor is selected.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
+{
+//    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)
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes, int nVars )
+{
+    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 );
+    return p;
+}
+void Fx_ManStop( Fx_Man_t * p )
+{
+//    Vec_WecFree( p->vCubes );
+    Vec_WecFree( p->vLits );
+    Vec_IntFree( p->vCounts );
+    Hsh_VecManStop( p->pHash );
+    Vec_FltFree( p->vWeights );
+    Vec_QueFree( p->vPrio );
+    Vec_IntFree( p->vCube );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Fx_PrintMatrix( Vec_Wec_t * vCubes, int nObjs )
+{
+    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 )
+    {
+        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 );
+}
+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 )
+{
+    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_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose )
+{
+    Fx_Man_t * p;
+    clock_t clk = clock();
+    p = Fx_ManStart( vCubes, nVars );
+
+    if ( fVerbose )
+    {
+        Fx_PrintMatrix( vCubes, nVars );
+        Fx_PrintDivisors( p );
+        printf( "Selecting divisors:\n" );
+    }
+
+    Fx_PrintStats( p, clock() - clk );
+    while ( Vec_QueTopCost(p->vPrio) > 0.0 )
+    {
+        int iDiv = Vec_QuePop(p->vPrio);
+        if ( fVerbose )
+            Fx_PrintDiv( p, iDiv );
+        Fx_ManUpdate( p, iDiv );
+    }
+
+    Fx_ManStop( p );
+    return 1;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 7846b268..89e1849b 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -17,6 +17,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcExtract.c \
     src/base/abci/abcFraig.c \
+        src/base/abci/abcFx.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
     src/base/abci/abcHaig.c \
diff --git a/src/misc/vec/vecHsh.h b/src/misc/vec/vecHsh.h
new file mode 100644
index 00000000..04f1e9f2
--- /dev/null
+++ b/src/misc/vec/vecHsh.h
@@ -0,0 +1,360 @@
+/**CFile****************************************************************
+
+  FileName    [vecHsh.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Hashing vector entries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecHsh.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__misc__vec__vecHsh_h
+#define ABC__misc__vec__vecHsh_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Hsh_IntObj_t_ Hsh_IntObj_t;
+struct Hsh_IntObj_t_
+{
+    int          iData;
+    int          iNext;
+};
+
+typedef struct Hsh_IntMan_t_ Hsh_IntMan_t;
+struct Hsh_IntMan_t_
+{
+    int          nSize;       // data size
+    Vec_Int_t *  vData;       // data storage
+    Vec_Int_t *  vTable;      // hash table
+    Vec_Wrd_t *  vObjs;       // hash objects
+};
+
+
+
+typedef struct Hsh_VecObj_t_ Hsh_VecObj_t;
+struct Hsh_VecObj_t_
+{
+    int          nSize;
+    int          iNext;
+    int          pArray[0];
+};
+
+typedef struct Hsh_VecMan_t_ Hsh_VecMan_t;
+struct Hsh_VecMan_t_
+{
+    Vec_Int_t *  vTable;      // hash table
+    Vec_Int_t *  vData;       // data storage
+    Vec_Int_t *  vMap;        // mapping entries into data;
+    Vec_Int_t    vTemp;       // temporary array
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned *      Hsh_IntData( Hsh_IntMan_t * p, int iData )  { return (unsigned *)Vec_IntEntryP( p->vData, p->nSize * iData );             }
+static inline Hsh_IntObj_t *  Hsh_IntObj( Hsh_IntMan_t * p, int iObj )    { return iObj == -1 ? NULL : (Hsh_IntObj_t *)Vec_WrdEntryP( p->vObjs, iObj ); }
+static inline word            Hsh_IntWord( int iData, int iNext )         { Hsh_IntObj_t Obj = {iData, iNext}; return *((word *)&Obj);                  }
+
+static inline Hsh_VecObj_t *  Hsh_VecObj( Hsh_VecMan_t * p, int i )  { return i == -1 ? NULL : (Hsh_VecObj_t *)Vec_IntEntryP(p->vData, Vec_IntEntry(p->vMap, i));  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Hashing data entries composed of nSize integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hsh_IntMan_t * Hsh_IntManStart( Vec_Int_t * vData, int nSize, int nEntries )
+{
+    Hsh_IntMan_t * p;
+    p = ABC_CALLOC( Hsh_IntMan_t, 1 );
+    p->nSize  = nSize;
+    p->vData  = vData;
+    p->vTable = Vec_IntStartFull( Abc_PrimeCudd(nEntries) );
+    p->vObjs  = Vec_WrdAlloc( nEntries );
+    return p;
+}
+static inline void Hsh_IntManStop( Hsh_IntMan_t * p )
+{
+    Vec_IntFree( p->vTable );
+    Vec_WrdFree( p->vObjs );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Hsh_IntManHash( unsigned * pData, int nSize, int nTableSize )
+{
+    static int s_Primes[7] = { 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
+    unsigned char * pDataC = (unsigned char *)pData;
+    int c, nChars = nSize * 4;
+    unsigned Key = 0;
+    for ( c = 0; c < nChars; c++ )
+        Key += pDataC[c] * s_Primes[c % 7];
+    return (int)(Key % nTableSize);
+}
+static inline int Hsh_IntManAdd( Hsh_IntMan_t * p, int iData )
+{
+    Hsh_IntObj_t * pObj;
+    unsigned * pData = Hsh_IntData( p, iData );
+    int i, * pPlace;
+    if ( Vec_WrdSize(p->vObjs) > Vec_IntSize(p->vTable) )
+    {
+        Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), -1 );
+        for ( i = 0; i < Vec_WrdSize(p->vObjs); i++ )
+        {
+            pPlace = Vec_IntEntryP( p->vTable, Hsh_IntManHash(Hsh_IntData(p, i), p->nSize, Vec_IntSize(p->vTable)) );
+            Hsh_IntObj(p, i)->iNext = *pPlace;  *pPlace = i;
+        }
+    }
+    pPlace = Vec_IntEntryP( p->vTable, Hsh_IntManHash(pData, p->nSize, Vec_IntSize(p->vTable)) );
+    for ( ; (pObj = Hsh_IntObj(p, *pPlace)); pPlace = &pObj->iNext )
+        if ( !memcmp( pData, Hsh_IntData(p, pObj->iData), sizeof(int) * p->nSize ) )
+            return (word *)pObj - Vec_WrdArray(p->vObjs);
+    *pPlace = Vec_WrdSize(p->vObjs);
+    Vec_WrdPush( p->vObjs, Hsh_IntWord(iData, -1) );
+    return Vec_WrdSize(p->vObjs)-1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Hashes data by value.]
+
+  Description [Array vData contains data entries, each of 'nSize' integers.
+  The resulting array contains the indexes of unique data entries.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Hsh_IntManHashArray( Vec_Int_t * vData, int nSize )
+{
+    Hsh_IntMan_t * p;
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    int i, nEntries = Vec_IntSize(vData) / nSize;
+    assert( Vec_IntSize(vData) % nSize == 0 );
+    p = Hsh_IntManStart( vData, nSize, nEntries );
+    for ( i = 0; i < nEntries; i++ )
+        Vec_IntPush( vRes, Hsh_IntManAdd(p, i) );
+    Hsh_IntManStop( p );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Test procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Hsh_IntManHashArrayTest()
+{
+    Vec_Int_t * vData = Vec_IntAlloc( 10 );
+    Vec_Int_t * vRes;
+    Vec_IntPush( vData, 12 );
+    Vec_IntPush( vData, 17 );
+    Vec_IntPush( vData, 13 );
+    Vec_IntPush( vData, 12 );
+    Vec_IntPush( vData, 15 );
+    Vec_IntPush( vData, 3 );
+    Vec_IntPush( vData, 16 );
+    Vec_IntPush( vData, 16 );
+    Vec_IntPush( vData, 12 );
+    Vec_IntPush( vData, 17 );
+    Vec_IntPush( vData, 12 );
+    Vec_IntPush( vData, 12 );
+
+    vRes = Hsh_IntManHashArray( vData, 2 );
+
+    Vec_IntPrint( vData );
+    Vec_IntPrint( vRes );
+
+    Vec_IntFree( vData );
+    Vec_IntFree( vRes );
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Hashing integer arrays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Hsh_VecMan_t * Hsh_VecManStart( int nEntries )
+{
+    Hsh_VecMan_t * p;
+    p = ABC_CALLOC( Hsh_VecMan_t, 1 );
+    p->vTable = Vec_IntStartFull( Abc_PrimeCudd(nEntries) );
+    p->vData  = Vec_IntAlloc( nEntries * 4 );
+    p->vMap   = Vec_IntAlloc( nEntries );
+    return p;
+}
+static inline void Hsh_VecManStop( Hsh_VecMan_t * p )
+{
+    Vec_IntFree( p->vTable );
+    Vec_IntFree( p->vData );
+    Vec_IntFree( p->vMap );
+    ABC_FREE( p );
+}
+static inline Vec_Int_t * Hsh_VecReadEntry( Hsh_VecMan_t * p, int i )
+{
+    Hsh_VecObj_t * pObj = Hsh_VecObj( p, i );
+    p->vTemp.nSize = p->vTemp.nCap = pObj->nSize;
+    p->vTemp.pArray = (int*)pObj + 2;
+    return &p->vTemp;
+}
+static inline int Hsh_VecSize( Hsh_VecMan_t * p )
+{
+    return Vec_IntSize(p->vMap);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Hsh_VecManHash( Vec_Int_t * vVec, int nTableSize )
+{
+    static unsigned s_Primes[7] = {4177, 5147, 5647, 6343, 7103, 7873, 8147};
+    unsigned Key = 0;
+    int i, Entry;
+    Vec_IntForEachEntry( vVec, Entry, i )
+        Key += (unsigned)Entry * s_Primes[i % 7];
+    return (int)(Key % nTableSize);
+}
+static inline int Hsh_VecManAdd( Hsh_VecMan_t * p, Vec_Int_t * vVec )
+{
+    Hsh_VecObj_t * pObj;
+    int i, Ent, * pPlace;
+    if ( Vec_IntSize(p->vMap) > Vec_IntSize(p->vTable) )
+    {
+        Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), -1 );
+        for ( i = 0; i < Vec_IntSize(p->vMap); i++ )
+        {
+            pPlace = Vec_IntEntryP( p->vTable, Hsh_VecManHash(Hsh_VecReadEntry(p, i), Vec_IntSize(p->vTable)) );
+            Hsh_VecObj(p, i)->iNext = *pPlace; *pPlace = i;
+        }
+    }
+    pPlace = Vec_IntEntryP( p->vTable, Hsh_VecManHash(vVec, Vec_IntSize(p->vTable)) );
+    for ( ; (pObj = Hsh_VecObj(p, *pPlace)); pPlace = &pObj->iNext )
+        if ( pObj->nSize == Vec_IntSize(vVec) && !memcmp( pObj->pArray, Vec_IntArray(vVec), sizeof(int) * pObj->nSize ) )
+            return *pPlace;
+    *pPlace = Vec_IntSize(p->vMap);
+    assert( Vec_IntSize(p->vData) % 2 == 0 );
+    Vec_IntPush( p->vMap, Vec_IntSize(p->vData) );
+    Vec_IntPush( p->vData, Vec_IntSize(vVec) );
+    Vec_IntPush( p->vData, -1 );
+    Vec_IntForEachEntry( vVec, Ent, i )
+        Vec_IntPush( p->vData, Ent );
+    if ( Vec_IntSize(vVec) & 1 )
+        Vec_IntPush( p->vData, -1 );
+    return Vec_IntSize(p->vMap) - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Test procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Hsh_VecManHashTest()
+{
+    Hsh_VecMan_t * p;
+    Vec_Int_t * vTemp;
+    Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+    int i;
+    
+    p = Hsh_VecManStart( 5 );
+    for ( i = 0; i < 20; i++ )
+    {
+        vTemp = Vec_IntStartNatural( i );
+        Vec_IntPush( vRes, Hsh_VecManAdd( p, vTemp ) );
+        Vec_IntFree( vTemp );
+    }
+    for ( ; i > 0; i-- )
+    {
+        vTemp = Vec_IntStartNatural( i );
+        Vec_IntPush( vRes, Hsh_VecManAdd( p, vTemp ) );
+        Vec_IntFree( vTemp );
+    }
+    Vec_IntPrint( vRes );
+    Vec_IntFree( vRes );
+
+    Hsh_VecManStop( p );
+}
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 9744a031..60352a0f 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1193,6 +1193,24 @@ static inline int Vec_IntUniqify( Vec_Int_t * p )
     p->nSize = k;
     return RetValue;
 }
+static inline int Vec_IntCountDuplicates( Vec_Int_t * p )
+{
+    int RetValue;
+    Vec_Int_t * pDup = Vec_IntDup( p );
+    Vec_IntUniqify( pDup );
+    RetValue = Vec_IntSize(p) - Vec_IntSize(pDup);
+    Vec_IntFree( pDup );
+    return RetValue;
+}
+static inline int Vec_IntCheckUniqueSmall( Vec_Int_t * p )
+{
+    int i, k;
+    for ( i = 0; i < p->nSize; i++ )
+        for ( k = i+1; k < p->nSize; k++ )
+            if ( p->pArray[i] == p->pArray[k] )
+                return 0;
+    return 1;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecQue.h b/src/misc/vec/vecQue.h
index aaa1c01d..1b6bc4bb 100644
--- a/src/misc/vec/vecQue.h
+++ b/src/misc/vec/vecQue.h
@@ -140,6 +140,10 @@ static inline int Vec_QueTop( Vec_Que_t * p )
 {
     return Vec_QueSize(p) > 0 ? p->pHeap[1] : -1;
 }
+static inline float Vec_QueTopCost( Vec_Que_t * p )
+{
+    return Vec_QueSize(p) > 0 ? Vec_QueCost(p, p->pHeap[1]) : -ABC_INFINITY;
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index d935be0f..f8f36d8b 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -253,6 +253,7 @@ static inline int Vec_VecCap( Vec_Vec_t * p )
 ***********************************************************************/
 static inline int Vec_VecLevelSize( Vec_Vec_t * p, int i )
 {
+    assert( i >= 0 && i < p->nSize );
     return Vec_PtrSize( (Vec_Ptr_t *)p->pArray[i] );
 }
 
@@ -617,7 +618,7 @@ static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles )
     int i, k, Entry;
     Vec_VecForEachEntryInt( p, Entry, i, k )
     {
-        if ( Vec_VecLevelSize(p, i) == 1 )
+        if ( fSkipSingles && Vec_VecLevelSize(p, i) == 1 )
             break;
         if ( k == 0 )
             printf( " %4d : {", i );
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
new file mode 100644
index 00000000..49ecb3da
--- /dev/null
+++ b/src/misc/vec/vecWec.h
@@ -0,0 +1,476 @@
+/**CFile****************************************************************
+
+  FileName    [vecWec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable vector of resizable vectors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecWec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__misc__vec__vecWec_h
+#define ABC__misc__vec__vecWec_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Wec_t_       Vec_Wec_t;
+struct Vec_Wec_t_ 
+{
+    int              nCap;
+    int              nSize;
+    Vec_Int_t *      pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// 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_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 )                               \
+    for ( i = 0; (i < LevelStop) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ )
+#define Vec_WecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )              \
+    for ( i = LevelStart; (i < LevelStop) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ )
+#define Vec_WecForEachLevelReverse( vGlob, vVec, i )                                       \
+    for ( i = Vec_WecSize(vGlob)-1; (i >= 0) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i-- )
+#define Vec_WecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop )       \
+    for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i-- )
+#define Vec_WecForEachLevelTwo( vGlob1, vGlob2, vVec1, vVec2, i )                          \
+    for ( i = 0; (i < Vec_WecSize(vGlob1)) && (((vVec1) = Vec_WecEntry(vGlob1, i)), 1) && (((vVec2) = Vec_WecEntry(vGlob2, i)), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Wec_t * Vec_WecAlloc( int nCap )
+{
+    Vec_Wec_t * p;
+    p = ABC_ALLOC( Vec_Wec_t, 1 );
+    if ( nCap > 0 && nCap < 8 )
+        nCap = 8;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL;
+    return p;
+}
+static inline Vec_Wec_t * Vec_WecStart( int nSize )
+{
+    Vec_Wec_t * p;
+    p = Vec_WecAlloc( nSize );
+    p->nSize = nSize;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecGrow( Vec_Wec_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = ABC_REALLOC( Vec_Int_t, p->pArray, nCapMin ); 
+    memset( p->pArray + p->nCap, 0, sizeof(Vec_Int_t) * (nCapMin - p->nCap) );
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Vec_WecEntry( Vec_Wec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray + i;
+}
+static inline Vec_Int_t * Vec_WecEntryLast( Vec_Wec_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray + p->nSize - 1;
+}
+static inline int Vec_WecEntryEntry( Vec_Wec_t * p, int i, int k )
+{
+    return Vec_IntEntry( Vec_WecEntry(p, i), k );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_WecCap( Vec_Wec_t * p )
+{
+    return p->nCap;
+}
+static inline int Vec_WecSize( Vec_Wec_t * p )
+{
+    return p->nSize;
+}
+static inline int Vec_WecLevelSize( Vec_Wec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return Vec_IntSize( p->pArray + i );
+}
+static inline int Vec_WecSizeSize( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i, Counter = 0;
+    Vec_WecForEachLevel( p, vVec, i )
+        Counter += Vec_IntSize(vVec);
+    return Counter;
+}
+static inline int Vec_WecSizeUsed( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i, Counter = 0;
+    Vec_WecForEachLevel( p, vVec, i )
+        Counter += (int)(Vec_IntSize(vVec) > 0);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecShrink( Vec_Wec_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecClear( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i;
+    Vec_WecForEachLevel( p, vVec, i )
+        Vec_IntClear( vVec );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry )
+{
+    if ( p->nSize < Level + 1 )
+    {
+        Vec_WecGrow( p, 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 );
+    return Vec_WecEntryLast( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline double Vec_WecMemory( Vec_Wec_t * p )
+{
+    int i;
+    double Mem;
+    if ( p == NULL )  return 0.0;
+    Mem = sizeof(Vec_Int_t) * Vec_WecCap(p);
+    for ( i = 0; i < p->nSize; i++ )
+        Mem += sizeof(int) * Vec_IntCap( Vec_WecEntry(p, i) );
+    return Mem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecFree( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i;
+    Vec_WecForEachLevel( p, vVec, i )
+        ABC_FREE( vVec->pArray );
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
+}
+static inline void Vec_WecFreeP( Vec_Wec_t ** p )
+{
+    if ( *p == NULL )
+        return;
+    Vec_WecFree( *p );
+    *p = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecPushUnique( Vec_Wec_t * p, int Level, int Entry )
+{
+    if ( p->nSize < Level + 1 )
+        Vec_WecPush( p, Level, Entry );
+    else
+        Vec_IntPushUnique( Vec_WecEntry(p, Level), Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Wec_t * Vec_WecDup( Vec_Wec_t * p )
+{
+    Vec_Wec_t * vNew;
+    Vec_Int_t * vVec;
+    int i, k, Entry;
+    vNew = Vec_WecAlloc( Vec_WecSize(p) );
+    Vec_WecForEachLevel( p, vVec, i )
+        Vec_IntForEachEntry( vVec, Entry, k )
+            Vec_WecPush( vNew, i, Entry );
+    return vNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two arrays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Vec_WecSortCompare1( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    if ( Vec_IntSize(p1) < Vec_IntSize(p2) )
+        return -1;
+    if ( Vec_IntSize(p1) > Vec_IntSize(p2) ) 
+        return 1;
+    return 0; 
+}
+static int Vec_WecSortCompare2( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    if ( Vec_IntSize(p1) > Vec_IntSize(p2) )
+        return -1;
+    if ( Vec_IntSize(p1) < Vec_IntSize(p2) ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecSort( Vec_Wec_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), 
+                (int (*)(const void *, const void *)) Vec_WecSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), 
+                (int (*)(const void *, const void *)) Vec_WecSortCompare1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two integers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Vec_WecSortCompare3( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    if ( Vec_IntEntry(p1,0) < Vec_IntEntry(p2,0) )
+        return -1;
+    if ( Vec_IntEntry(p1,0) > Vec_IntEntry(p2,0) ) 
+        return 1;
+    return 0; 
+}
+static int Vec_WecSortCompare4( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+    if ( Vec_IntEntry(p1,0) > Vec_IntEntry(p2,0) )
+        return -1;
+    if ( Vec_IntEntry(p1,0) < Vec_IntEntry(p2,0) ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecSortByFirstInt( Vec_Wec_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), 
+                (int (*)(const void *, const void *)) Vec_WecSortCompare4 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(Vec_Int_t), 
+                (int (*)(const void *, const void *)) Vec_WecSortCompare3 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
+{
+    Vec_Int_t * vVec;
+    int i, k, Entry;
+    Vec_WecForEachLevel( p, vVec, i )
+    {
+        if ( fSkipSingles && Vec_IntSize(vVec) == 1 )
+            break;
+        printf( " %4d : {", i );
+        Vec_IntForEachEntry( vVec, Entry, k )
+            printf( " %d", Entry );
+        printf( " }\n" );
+    }
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index e05959a2..4063757c 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1153,27 +1153,6 @@ void Ga2_ManRestart( Ga2_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Vec_IntCheckUnique( Vec_Int_t * p )
-{
-    int RetValue;
-    Vec_Int_t * pDup = Vec_IntDup( p );
-    Vec_IntUniqify( pDup );
-    RetValue = Vec_IntSize(p) - Vec_IntSize(pDup);
-    Vec_IntFree( pDup );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
 {
     int Lit = Ga2_ObjFindLit( p, pObj, f );
diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c
index efabe545..21d78f85 100644
--- a/src/proof/ssc/sscUtil.c
+++ b/src/proof/ssc/sscUtil.c
@@ -27,27 +27,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Hsh_Obj_t_ Hsh_Obj_t;
-struct Hsh_Obj_t_
-{
-    int              iThis;
-    int              iNext;
-};
-
-typedef struct Hsh_Man_t_ Hsh_Man_t;
-struct Hsh_Man_t_
-{
-    unsigned *       pData;   // user's data
-    int *            pTable;  // hash table
-    Hsh_Obj_t *      pObjs;
-    int              nObjs;
-    int              nSize;
-    int              nTableSize;
-};
-
-static inline unsigned *   Hsh_ObjData( Hsh_Man_t * p, int iThis )      { return p->pData + p->nSize * iThis;         }
-static inline Hsh_Obj_t *  Hsh_ObjGet( Hsh_Man_t * p, int iObj )        { return iObj == -1 ? NULL : p->pObjs + iObj;  }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -63,85 +42,6 @@ static inline Hsh_Obj_t *  Hsh_ObjGet( Hsh_Man_t * p, int iObj )        { return
   SeeAlso     []
 
 ***********************************************************************/
-Hsh_Man_t * Hsh_ManStart( unsigned * pData, int nDatas, int nSize )
-{
-    Hsh_Man_t * p;
-    p = ABC_CALLOC( Hsh_Man_t, 1 );
-    p->pData = pData;
-    p->nSize = nSize;
-    p->nTableSize = Abc_PrimeCudd( nDatas );
-    p->pTable = ABC_FALLOC( int, p->nTableSize );
-    p->pObjs  = ABC_FALLOC( Hsh_Obj_t, p->nTableSize );
-    return p;
-}
-void Hsh_ManStop( Hsh_Man_t * p )
-{
-    ABC_FREE( p->pObjs );
-    ABC_FREE( p->pTable );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Hsh_ManHash( unsigned * pData, int nSize, int nTableSize )
-{
-    static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
-    unsigned char * pDataC = (unsigned char *)pData;
-    int c, nChars = nSize * 4, Key = 0;
-    for ( c = 0; c < nChars; c++ )
-        Key += pDataC[c] * s_BigPrimes[c % 7];
-    return Key % nTableSize;
-}
-int Hsh_ManAdd( Hsh_Man_t * p, int iThis )
-{
-    Hsh_Obj_t * pObj;
-    unsigned * pThis = Hsh_ObjData( p, iThis );
-    int * pPlace = p->pTable + Hsh_ManHash( pThis, p->nSize, p->nTableSize );
-    for ( pObj = Hsh_ObjGet(p, *pPlace); pObj; pObj = Hsh_ObjGet(p, pObj->iNext) )
-        if ( !memcmp( pThis, Hsh_ObjData(p, pObj->iThis), sizeof(unsigned) * p->nSize ) )
-            return pObj - p->pObjs;
-    assert( p->nObjs < p->nTableSize );
-    pObj = p->pObjs + p->nObjs;
-    pObj->iThis = iThis;
-    return (*pPlace = p->nObjs++);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Hashes data by value.]
-
-  Description [Array of 'nTotal' int entries, each of size 'nSize' ints,
-  is hashed and the resulting unique numbers is returned in the array.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Hsh_ManHashData( unsigned * pData, int nDatas, int nSize, int nInts )
-{
-    Vec_Int_t * vRes;
-    Hsh_Man_t * p;
-    int i;
-    assert( nDatas * nSize == nInts );
-    p = Hsh_ManStart( pData, nDatas, nSize );
-    vRes = Vec_IntAlloc( 1000 );
-    for ( i = 0; i < nDatas; i++ )
-        Vec_IntPush( vRes, Hsh_ManAdd(p, i) );
-    Hsh_ManStop( p );
-    return vRes;
-}
-
-
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///