Scalable SOP manipulation package.

1 files changed, 854 insertions, 0 deletions

diff --git a/src/base/pla/plaFxch.c b/src/base/pla/plaFxch.c
new file mode 100644
index 00000000..fd06b9a5
--- /dev/null
+++ b/src/base/pla/plaFxch.c
@@ -0,0 +1,854 @@
+/**CFile****************************************************************
+
+  FileName    [plaFxch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SOP manager.]
+
+  Synopsis    [Scalable SOP transformations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - March 18, 2015.]
+
+  Revision    [$Id: plaFxch.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "pla.h"
+#include "misc/vec/vecHash.h"
+#include "misc/vec/vecQue.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Fxch_Obj_t_ Fxch_Obj_t;
+struct Fxch_Obj_t_
+{
+    unsigned        Table : 30;
+    unsigned        MarkN :  1;
+    unsigned        MarkP :  1;
+    int             Next;
+    int             Prev;
+    int             Cube;
+};
+
+typedef struct Fxch_Man_t_ Fxch_Man_t;
+struct Fxch_Man_t_
+{
+    // user's data
+    Vec_Wec_t       vCubes;     // cube -> lit
+    // internal data
+    Vec_Wec_t       vLits;      // lit -> cube
+    Vec_Int_t       vRands;     // random numbers for each literal
+    Vec_Int_t       vCubeLinks; // first link for each cube
+    Fxch_Obj_t *    pBins;      // hash table (lits -> cube + lit)
+    Hash_IntMan_t * vHash;      // divisor hash table
+    Vec_Que_t *     vPrio;      // priority queue for divisors by weight
+    Vec_Flt_t       vWeights;   // divisor weights
+    Vec_Wec_t       vPairs;     // cube pairs for each div
+    Vec_Wrd_t       vDivs;      // extracted divisors
+    // temporary data 
+    Vec_Int_t       vCubesS;    // cube pairs for single
+    Vec_Int_t       vCubesD;    // cube pairs for double
+    Vec_Int_t       vCube1;     // first cube
+    Vec_Int_t       vCube2;     // second cube
+    // statistics 
+    abctime         timeStart;  // starting time
+    int             SizeMask;   // hash table mask
+    int             nVars;      // original problem variables
+    int             nLits;      // the number of SOP literals
+    int             nCompls;    // the number of complements
+    int             nPairsS;    // number of lit pairs
+    int             nPairsD;    // number of cube pairs
+};
+
+#define Fxch_ManForEachCubeVec( vVec, vCubes, vCube, i )           \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )
+
+static inline Vec_Int_t * Fxch_ManCube( Fxch_Man_t * p, int hCube ) { return Vec_WecEntry(&p->vCubes, Pla_CubeNum(hCube)); }
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the current state of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxch_ManWriteBlif( char * pFileName, Vec_Wec_t * vCubes, Vec_Wrd_t * vDivs )
+{
+    // find the number of original variables
+    int nVarsInit = Vec_WrdCountZero(vDivs);
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+    else
+    {
+        char * pLits = "-01?";
+        Vec_Str_t * vStr;
+        Vec_Int_t * vCube;
+        int i, k, Lit;
+        word Div;
+        // comment
+        fprintf( pFile, "# BLIF file written via PLA package in ABC on " );
+        fprintf( pFile, "%s", Extra_TimeStamp() );
+        fprintf( pFile, "\n\n" );
+        // header
+        fprintf( pFile, ".model %s\n", pFileName );
+        fprintf( pFile, ".inputs" );
+        for ( i = 0; i < nVarsInit; i++ )
+            fprintf( pFile, " i%d", i );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, ".outputs o" );
+        fprintf( pFile, "\n" );
+        // SOP header
+        fprintf( pFile, ".names" );
+        for ( i = 0; i < Vec_WrdSize(vDivs); i++ )
+            fprintf( pFile, " i%d", i );
+        fprintf( pFile, " o\n" );
+        // SOP cubes
+        vStr = Vec_StrStart( Vec_WrdSize(vDivs) + 1 );
+        Vec_WecForEachLevel( vCubes, vCube, i )
+        {
+            if ( !Vec_IntSize(vCube) )
+                continue;
+            for ( k = 0; k < Vec_WrdSize(vDivs); k++ )
+                Vec_StrWriteEntry( vStr, k, '-' );
+            Vec_IntForEachEntry( vCube, Lit, k )
+                Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
+            fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) );
+        }
+        Vec_StrFree( vStr );
+        // divisors
+        Vec_WrdForEachEntryStart( vDivs, Div, i, nVarsInit )
+        {
+            int pLits[2] = { (int)(Div & 0xFFFFFFFF), (int)(Div >> 32) };
+            fprintf( pFile, ".names" );
+            fprintf( pFile, " i%d", Abc_Lit2Var(pLits[0]) );
+            fprintf( pFile, " i%d", Abc_Lit2Var(pLits[1]) );
+            fprintf( pFile, " i%d\n", i );
+            fprintf( pFile, "%d%d 1\n", !Abc_LitIsCompl(pLits[0]), !Abc_LitIsCompl(pLits[1]) );
+        }
+        fprintf( pFile, ".end\n\n" );
+        fclose( pFile );
+        printf( "Written BLIF file \"%s\".\n", pFileName );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starting the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fxch_Man_t * Fxch_ManStart( Vec_Wec_t * vCubes, Vec_Wec_t * vLits )
+{
+    Vec_Int_t * vCube;  int i, LogSize;
+    Fxch_Man_t * p = ABC_CALLOC( Fxch_Man_t, 1 );
+    p->vCubes = *vCubes;
+    p->vLits  = *vLits;
+    p->nVars  = Vec_WecSize(vLits)/2;
+    p->nLits  = 0;
+    // random numbers
+    Gia_ManRandom( 1 );
+    Vec_IntGrow( &p->vRands, 2*p->nVars );
+    for ( i = 0; i < 2*p->nVars; i++ )
+        Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); // assert( LogSize <= 26 );
+    // create cube links
+    Vec_IntGrow( &p->vCubeLinks, Vec_WecSize(&p->vCubes) );
+    Vec_WecForEachLevel( vCubes, vCube, i )
+    {
+        Vec_IntPush( &p->vCubeLinks, p->nLits+1 );
+        p->nLits += Vec_IntSize(vCube);
+    }
+    assert( Vec_IntSize(&p->vCubeLinks) == Vec_WecSize(&p->vCubes) );
+    // create table
+    LogSize = Abc_Base2Log( p->nLits+1 );
+    assert( LogSize <= 26 );
+    p->SizeMask = (1 << LogSize) - 1;
+    p->pBins = ABC_CALLOC( Fxch_Obj_t, p->SizeMask + 1 );
+    assert( p->nLits+1 < p->SizeMask+1 );
+    // divisor weights and cube pairs
+    Vec_FltGrow( &p->vWeights, 1000 );
+    Vec_FltPush( &p->vWeights, -1 );
+    Vec_WecGrow( &p->vPairs, 1000 );
+    Vec_WecPushLevel( &p->vPairs );
+    // prepare divisors
+    Vec_WrdGrow( &p->vDivs, p->nVars + 1000 );
+    Vec_WrdFill( &p->vDivs, p->nVars, 0 );
+    return p;
+}
+void Fxch_ManStop( Fxch_Man_t * p )
+{
+    Vec_WecErase( &p->vCubes );
+    Vec_WecErase( &p->vLits );
+    Vec_IntErase( &p->vRands );
+    Vec_IntErase( &p->vCubeLinks );
+    Hash_IntManStop( p->vHash );
+    Vec_QueFree( p->vPrio );
+    Vec_FltErase( &p->vWeights );
+    Vec_WecErase( &p->vPairs );
+    Vec_WrdErase( &p->vDivs );
+    Vec_IntErase( &p->vCubesS );
+    Vec_IntErase( &p->vCubesD );
+    Vec_IntErase( &p->vCube1 );
+    Vec_IntErase( &p->vCube2 );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fxch_TabCompare( Fxch_Man_t * p, int hCube1, int hCube2 )
+{
+    Vec_Int_t * vCube1 = Fxch_ManCube( p, hCube1 );
+    Vec_Int_t * vCube2 = Fxch_ManCube( p, hCube2 );
+    if ( !Vec_IntSize(vCube1) || !Vec_IntSize(vCube2) || Vec_IntSize(vCube1) != Vec_IntSize(vCube2) )
+        return 0;
+    Vec_IntClear( &p->vCube1 );
+    Vec_IntClear( &p->vCube2 );
+    Vec_IntAppendSkip( &p->vCube1, vCube1, Pla_CubeLit(hCube1) );
+    Vec_IntAppendSkip( &p->vCube2, vCube2, Pla_CubeLit(hCube2) );
+    return Vec_IntEqual( &p->vCube1, &p->vCube2 );
+}
+static inline void Fxch_CompressCubes( Fxch_Man_t * p, Vec_Int_t * vLit2Cube )
+{
+    int i, hCube, k = 0;
+    Vec_IntForEachEntry( vLit2Cube, hCube, i )
+        if ( Vec_IntSize(Vec_WecEntry(&p->vCubes, hCube)) > 0 )
+            Vec_IntWriteEntry( vLit2Cube, k++, hCube );
+    Vec_IntShrink( vLit2Cube, k );
+}
+static inline int Fxch_CollectSingles( 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 ( Pla_CubeNum(*pBeg1) == Pla_CubeNum(*pBeg2) )
+            Vec_IntPushTwo( vArr, *pBeg1, *pBeg2 ), 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);
+}
+static inline void Fxch_CollectDoubles( Fxch_Man_t * p, Vec_Int_t * vPairs, Vec_Int_t * vRes, int Lit0, int Lit1 )
+{
+    int i, hCube1, hCube2;
+    Vec_IntClear( vRes );
+    Vec_IntForEachEntryDouble( vPairs, hCube1, hCube2, i )
+        if ( Fxch_TabCompare(p, hCube1, hCube2) && 
+             Vec_IntEntry(Fxch_ManCube(p, hCube1), Pla_CubeLit(hCube1)) == Lit0 && 
+             Vec_IntEntry(Fxch_ManCube(p, hCube2), Pla_CubeLit(hCube2)) == Lit1 )
+            Vec_IntPushTwo( vRes, hCube1, hCube2 );
+    Vec_IntClear( vPairs );
+    // order pairs in the increasing order of the first cube
+    //Vec_IntSortPairs( vRes );
+}
+static inline void Fxch_CompressLiterals2( Vec_Int_t * p, int iInd1, int iInd2 )
+{
+    int i, Lit, k = 0;
+    assert( iInd1 >= 0 && iInd1 < Vec_IntSize(p) );
+    if ( iInd2 != -1 )
+    assert( iInd1 >= 0 && iInd1 < Vec_IntSize(p) );
+    Vec_IntForEachEntry( p, Lit, i )
+        if ( i != iInd1 && i != iInd2 )
+            Vec_IntWriteEntry( p, k++, Lit );
+    Vec_IntShrink( p, k );
+}
+static inline void Fxch_CompressLiterals( Vec_Int_t * p, int iLit1, int iLit2 )
+{
+    int i, Lit, k = 0;
+    Vec_IntForEachEntry( p, Lit, i )
+        if ( Lit != iLit1 && Lit != iLit2 )
+            Vec_IntWriteEntry( p, k++, Lit );
+    assert( Vec_IntSize(p) == k + 2 );
+    Vec_IntShrink( p, k );
+}
+static inline void Fxch_FilterCubes( Fxch_Man_t * p, Vec_Int_t * vCubesS, int Lit0, int Lit1 )
+{
+    Vec_Int_t * vCube;
+    int i, k, Lit, iCube, n = 0;
+    int fFound0, fFound1;
+    Vec_IntForEachEntry( vCubesS, iCube, i )
+    {
+        vCube = Vec_WecEntry( &p->vCubes, iCube );
+        fFound0 = fFound1 = 0;
+        Vec_IntForEachEntry( vCube, Lit, k )
+        {
+            if ( Lit == Lit0 )
+                fFound0 = 1;
+            else if ( Lit == Lit1 )
+                fFound1 = 1;
+        }
+        if ( fFound0 && fFound1 )
+            Vec_IntWriteEntry( vCubesS, n++, Pla_CubeHandle(iCube, 255) );
+    }
+    Vec_IntShrink( vCubesS, n );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Divisor addition removal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_DivisorAdd( Fxch_Man_t * p, int Lit0, int Lit1, int Weight )
+{
+    int iDiv;
+    assert( Lit0 != Lit1 );
+    if ( Lit0 < Lit1 )
+        iDiv = Hash_Int2ManInsert( p->vHash, Lit0, Lit1, 0 );
+    else
+        iDiv = Hash_Int2ManInsert( p->vHash, Lit1, Lit0, 0 );
+    if ( iDiv == Vec_FltSize(&p->vWeights) )
+    {
+        Vec_FltPush( &p->vWeights, -2 );
+        Vec_WecPushLevel( &p->vPairs );
+        assert( Vec_FltSize(&p->vWeights) == Vec_WecSize(&p->vPairs) );
+    }
+    Vec_FltAddToEntry( &p->vWeights, iDiv, Weight );
+    if ( p->vPrio )
+    {
+        if ( Vec_QueIsMember(p->vPrio, iDiv) )
+            Vec_QueUpdate( p->vPrio, iDiv );
+        else 
+            Vec_QuePush( p->vPrio, iDiv );
+        //assert( iDiv < Vec_QueSize(p->vPrio) );
+    }
+    return iDiv;
+}
+void Fxch_DivisorRemove( Fxch_Man_t * p, int Lit0, int Lit1, int Weight )
+{
+    int iDiv;
+    assert( Lit0 != Lit1 );
+    if ( Lit0 < Lit1 )
+        iDiv = *Hash_Int2ManLookup( p->vHash, Lit0, Lit1 );
+    else
+        iDiv = *Hash_Int2ManLookup( p->vHash, Lit1, Lit0 );
+    assert( iDiv > 0 && iDiv < Vec_FltSize(&p->vWeights) );
+    Vec_FltAddToEntry( &p->vWeights, iDiv, -Weight );
+    if ( Vec_QueIsMember(p->vPrio, iDiv) )
+        Vec_QueUpdate( p->vPrio, iDiv );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starting the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Fxch_Obj_t * Fxch_TabBin( Fxch_Man_t * p, int Value )             { return p->pBins + (Value & p->SizeMask);         }
+static inline Fxch_Obj_t * Fxch_TabEntry( Fxch_Man_t * p, int i )               { return i ? p->pBins + i : NULL;                  }
+static inline int          Fxch_TabEntryId( Fxch_Man_t * p, Fxch_Obj_t * pEnt ) { assert(pEnt > p->pBins); return pEnt - p->pBins; }
+
+static inline void Fxch_TabMarkPair( Fxch_Man_t * p, int i, int j )
+{
+    Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+    Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+    assert( pI->Next == j );
+    assert( pJ->Prev == i );
+    assert( pI->MarkN == 0 );
+    assert( pI->MarkP == 0 );
+    assert( pJ->MarkN == 0 );
+    assert( pJ->MarkP == 0 );
+    pI->MarkN = 1;
+    pJ->MarkP = 1;
+}
+static inline void Fxch_TabUnmarkPair( Fxch_Man_t * p, int i, int j )
+{
+    Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+    Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+    assert( pI->Next == j );
+    assert( pJ->Prev == i );
+    assert( pI->MarkN == 1 );
+    assert( pI->MarkP == 0 );
+    assert( pJ->MarkN == 0 );
+    assert( pJ->MarkP == 1 );
+    pI->MarkN = 0;
+    pJ->MarkP = 0;
+}
+static inline void Fxch_TabInsertLink( Fxch_Man_t * p, int i, int j, int fSkipCheck )
+{
+    Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+    Fxch_Obj_t * pN = Fxch_TabEntry(p, pI->Next);
+    Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+    //assert( pJ->Cube != 0 );
+    assert( pN->Prev == i );
+    assert( fSkipCheck || pI->MarkN == 0 );
+    assert( fSkipCheck || pN->MarkP == 0 );
+    assert( fSkipCheck || pJ->MarkN == 0 );
+    assert( fSkipCheck || pJ->MarkP == 0 );
+    pJ->Next = pI->Next;  pI->Next = j;
+    pJ->Prev = i;         pN->Prev = j;
+}
+static inline void Fxch_TabExtractLink( Fxch_Man_t * p, int i, int j )
+{
+    Fxch_Obj_t * pI = Fxch_TabEntry(p, i);
+    Fxch_Obj_t * pJ = Fxch_TabEntry(p, j);
+    Fxch_Obj_t * pN = Fxch_TabEntry(p, pJ->Next);
+    //assert( pJ->Cube != 0 );
+    assert( pI->Next == j );
+    assert( pJ->Prev == i );
+    assert( pN->Prev == j );
+    assert( pI->MarkN == 0 );
+    assert( pJ->MarkP == 0 );
+    assert( pJ->MarkN == 0 );
+    assert( pN->MarkP == 0 );
+    pI->Next = pJ->Next;  pJ->Next = 0;
+    pN->Prev = pJ->Prev;  pJ->Prev = 0;
+}
+static inline void Fxch_TabInsert( Fxch_Man_t * p, int iLink, int Value, int hCube )
+{
+    int iEnt, iDiv, Lit0, Lit1, fStart = 1;
+    Fxch_Obj_t * pEnt;
+    Fxch_Obj_t * pBin  = Fxch_TabBin( p, Value );
+    Fxch_Obj_t * pCell = Fxch_TabEntry( p, iLink );
+    assert( pCell->MarkN == 0 );
+    assert( pCell->MarkP == 0 );
+    assert( pCell->Cube == 0 );
+    pCell->Cube = hCube;
+    if ( pBin->Table == 0 )
+    {
+        pBin->Table = pCell->Next = pCell->Prev = iLink;
+        return;
+    }
+    // find equal cubes
+    for ( iEnt = pBin->Table; iEnt != (int)pBin->Table || fStart; iEnt = pEnt->Next, fStart = 0 )
+    {
+        pEnt = Fxch_TabBin( p, iEnt );
+        if ( pEnt->MarkN || pEnt->MarkP || !Fxch_TabCompare(p, pEnt->Cube, hCube) )
+            continue;
+        Fxch_TabInsertLink( p, iEnt, iLink, 0 );
+        Fxch_TabMarkPair( p, iEnt, iLink );
+        // get literals
+        Lit0 = Vec_IntEntry( Fxch_ManCube(p, hCube),      Pla_CubeLit(hCube) );
+        Lit1 = Vec_IntEntry( Fxch_ManCube(p, pEnt->Cube), Pla_CubeLit(pEnt->Cube) );
+        // increment divisor weight
+        iDiv = Fxch_DivisorAdd( p, Abc_LitNot(Lit0), Abc_LitNot(Lit1), Vec_IntSize(Fxch_ManCube(p, hCube)) );
+        // add divisor pair
+        assert( iDiv < Vec_WecSize(&p->vPairs) );
+        if ( Lit0 < Lit1 )
+        {
+            Vec_WecPush( &p->vPairs, iDiv, hCube );
+            Vec_WecPush( &p->vPairs, iDiv, pEnt->Cube );
+        }
+        else
+        {
+            Vec_WecPush( &p->vPairs, iDiv, pEnt->Cube );
+            Vec_WecPush( &p->vPairs, iDiv, hCube );
+        }
+        p->nPairsD++;
+        return;
+    }
+    assert( iEnt == (int)pBin->Table );
+    pEnt = Fxch_TabBin( p, iEnt );
+    Fxch_TabInsertLink( p, pEnt->Prev, iLink, 1 );
+}
+static inline void Fxch_TabExtract( Fxch_Man_t * p, int iLink, int Value, int hCube )
+{
+    int Lit0, Lit1;
+    Fxch_Obj_t * pPair = NULL;
+    Fxch_Obj_t * pBin  = Fxch_TabBin( p, Value );
+    Fxch_Obj_t * pLink = Fxch_TabEntry( p, iLink );
+    assert( pLink->Cube == hCube );
+    if ( pLink->MarkN )
+    {
+        pPair = Fxch_TabEntry( p, pLink->Next );
+        Fxch_TabUnmarkPair( p, iLink, pLink->Next );
+    }
+    else if ( pLink->MarkP )
+    {
+        pPair = Fxch_TabEntry( p, pLink->Prev );
+        Fxch_TabUnmarkPair( p, pLink->Prev, iLink );
+    }
+    if ( (int)pBin->Table == iLink )
+        pBin->Table = pLink->Next != iLink ? pLink->Next : 0;
+    if ( pLink->Next == iLink )
+    {
+        assert( pLink->Prev == iLink );
+        pLink->Next = pLink->Prev = 0;
+    }
+    else
+        Fxch_TabExtractLink( p, pLink->Prev, iLink );
+    pLink->Cube = 0;
+    if ( pPair == NULL )
+        return;
+    assert( Fxch_TabCompare(p, pPair->Cube, hCube) );
+    // get literals
+    Lit0 = Vec_IntEntry( Fxch_ManCube(p, hCube),       Pla_CubeLit(hCube) );
+    Lit1 = Vec_IntEntry( Fxch_ManCube(p, pPair->Cube), Pla_CubeLit(pPair->Cube) );
+    // decrement divisor weight
+    Fxch_DivisorRemove( p, Abc_LitNot(Lit0), Abc_LitNot(Lit1), Vec_IntSize(Fxch_ManCube(p, hCube)) );
+    p->nPairsD--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starting the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fxch_TabSingleDivisors( Fxch_Man_t * p, int iCube, int fAdd )
+{
+    Vec_Int_t * vCube = Vec_WecEntry( &p->vCubes, iCube );
+    int i, k, Lit, Lit2;
+    if ( Vec_IntSize(vCube) < 2 )
+        return 0;
+    Vec_IntForEachEntry( vCube, Lit, i )
+    Vec_IntForEachEntryStart( vCube, Lit2, k, i+1 )
+    {
+        assert( Lit < Lit2 );
+        if ( fAdd )
+            Fxch_DivisorAdd( p, Lit, Lit2, 1 ), p->nPairsS++;
+        else
+            Fxch_DivisorRemove( p, Lit, Lit2, 1 ), p->nPairsS--;
+    }
+    return Vec_IntSize(vCube) * (Vec_IntSize(vCube) - 1) / 2;
+}
+int Fxch_TabDoubleDivisors( Fxch_Man_t * p, int iCube, int fAdd )
+{
+    Vec_Int_t * vCube = Vec_WecEntry( &p->vCubes, iCube );
+    int iLinkFirst = Vec_IntEntry( &p->vCubeLinks, iCube );
+    int k, Lit, Value = 0;
+    Vec_IntForEachEntry( vCube, Lit, k )
+        Value += Vec_IntEntry(&p->vRands, Lit);
+    Vec_IntForEachEntry( vCube, Lit, k )
+    {
+        Value -= Vec_IntEntry(&p->vRands, Lit);
+        if ( fAdd )
+            Fxch_TabInsert( p, iLinkFirst + k, Value, Pla_CubeHandle(iCube, k) );
+        else
+            Fxch_TabExtract( p, iLinkFirst + k, Value, Pla_CubeHandle(iCube, k) );
+        Value += Vec_IntEntry(&p->vRands, Lit);
+    }
+    return 1;
+}
+void Fxch_ManCreateDivisors( Fxch_Man_t * p )
+{
+    float Weight;  int i;
+    // alloc hash table
+    assert( p->vHash == NULL );
+    p->vHash = Hash_IntManStart( 1000 );
+    // create single-cube two-literal divisors
+    for ( i = 0; i < Vec_WecSize(&p->vCubes); i++ )
+        Fxch_TabSingleDivisors( p, i, 1 ); // add - no update
+    // create two-cube divisors
+    for ( i = 0; i < Vec_WecSize(&p->vCubes); i++ )
+        Fxch_TabDoubleDivisors( p, i, 1 ); // add - no update
+    // create queue with all divisors
+    p->vPrio = Vec_QueAlloc( Vec_FltSize(&p->vWeights) );
+    Vec_QueSetPriority( p->vPrio, Vec_FltArrayP(&p->vWeights) );
+    Vec_FltForEachEntry( &p->vWeights, Weight, i )
+        if ( Weight > 0.0 )
+            Vec_QuePush( p->vPrio, i );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the data-structure when one divisor is selected.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxch_ManUpdate( Fxch_Man_t * p, int iDiv )
+{
+    Vec_Int_t * vCube1, * vCube2, * vLitP, * vLitN;
+    int nLitsNew = p->nLits - (int)Vec_FltEntry(&p->vWeights, iDiv);
+    int i, Lit0, Lit1, hCube1, hCube2, iVarNew;
+    //float Diff = Vec_FltEntry(&p->vWeights, iDiv) - (float)((int)Vec_FltEntry(&p->vWeights, iDiv));
+    //assert( Diff > 0.0 && Diff < 1.0 );
+
+    // get the divisor and select pivot variables
+    Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); 
+    Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF );
+    Lit0 = Hash_IntObjData0( p->vHash, iDiv );
+    Lit1 = Hash_IntObjData1( p->vHash, iDiv );
+    assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 );
+    Vec_WrdPush( &p->vDivs, ((word)Lit1 << 32) | (word)Lit0 );
+
+    // if the input cover is not prime, it may happen that we are extracting divisor (x + !x)
+    // although it is not strictly correct, it seems to be fine to just skip such divisors
+//    if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->vHash, iDiv)) == 2 )
+//        return;
+
+    // collect single-cube-divisor cubes
+    vLitP = Vec_WecEntry(&p->vLits, Lit0);
+    vLitN = Vec_WecEntry(&p->vLits, Lit1);
+    Fxch_CompressCubes( p, vLitP );
+    Fxch_CompressCubes( p, vLitN );
+//    Fxch_CollectSingles( vLitP, vLitN, &p->vCubesS );
+//    assert( Vec_IntSize(&p->vCubesS) % 2 == 0 );
+    Vec_IntTwoRemoveCommon( vLitP, vLitN, &p->vCubesS );
+    Fxch_FilterCubes( p, &p->vCubesS, Lit0, Lit1 );
+
+    // collect double-cube-divisor cube pairs
+    Fxch_CollectDoubles( p, Vec_WecEntry(&p->vPairs, iDiv), &p->vCubesD, Abc_LitNot(Lit0), Abc_LitNot(Lit1) );
+    assert( Vec_IntSize(&p->vCubesD) % 2 == 0 );
+    Vec_IntUniqifyPairs( &p->vCubesD );
+    assert( Vec_IntSize(&p->vCubesD) % 2 == 0 );
+
+    // subtract cost of single-cube divisors
+//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 );  // remove - update
+    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 ),  // remove - update
+        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube2), 0 );  // remove - update
+
+    // subtract cost of double-cube divisors
+//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+    {
+        //printf( "%d ", Pla_CubeNum(hCube1) );
+        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 );  // remove - update
+    }
+    //printf( "\n" );
+
+    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+    {
+        //printf( "%d ", Pla_CubeNum(hCube1) );
+        //printf( "%d  ", Pla_CubeNum(hCube2) );
+        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 ),  // remove - update
+        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube2), 0 );  // remove - update
+    }
+    //printf( "\n" );
+
+    // create new literals
+    p->nLits += 2;
+    iVarNew = Vec_WecSize( &p->vLits ) / 2;
+    vLitP = Vec_WecPushLevel( &p->vLits );
+    vLitN = Vec_WecPushLevel( &p->vLits );
+    vLitP = Vec_WecEntry( &p->vLits, Vec_WecSize(&p->vLits) - 2 );
+    // update single-cube divisor cubes
+//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+    {
+//        int Lit0s, Lit1s;
+        vCube1 = Fxch_ManCube( p, hCube1 );
+//        Lit0s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube1));
+//        Lit1s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube2));
+//        assert( Pla_CubeNum(hCube1) == Pla_CubeNum(hCube2) );
+//        assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Lit0 );
+//        assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube2)) == Lit1 );
+        Fxch_CompressLiterals( vCube1, Lit0, Lit1 );
+//        Vec_IntPush( vLitP, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) );
+        Vec_IntPush( vLitP, Pla_CubeNum(hCube1) );
+        Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 0) );
+
+        //if ( Pla_CubeNum(hCube1) == 3 )
+        //    printf( "VecSize = %d\n", Vec_IntSize(vCube1) );
+
+        p->nLits--;
+    }
+    // update double-cube divisor cube pairs
+    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+    {
+        vCube1 = Fxch_ManCube( p, hCube1 );
+        vCube2 = Fxch_ManCube( p, hCube2 );
+        assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Abc_LitNot(Lit0) );
+        assert( Vec_IntEntry(vCube2, Pla_CubeLit(hCube2)) == Abc_LitNot(Lit1) );
+        Fxch_CompressLiterals2( vCube1, Pla_CubeLit(hCube1), -1 );
+//        Vec_IntPush( vLitN, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) );
+        Vec_IntPush( vLitN, Pla_CubeNum(hCube1) );
+        Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 1) );
+        p->nLits -= Vec_IntSize(vCube2);
+
+        //if ( Pla_CubeNum(hCube1) == 3 )
+        //    printf( "VecSize = %d\n", Vec_IntSize(vCube1) );
+
+        // remove second cube
+        Vec_IntClear( vCube2 ); 
+    }
+    Vec_IntSort( vLitN, 0 );
+    Vec_IntSort( vLitP, 0 );
+
+    // add cost of single-cube divisors
+//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
+    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+        Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
+
+    // add cost of double-cube divisors
+//    Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i )
+    Vec_IntForEachEntry( &p->vCubesS, hCube1, i )
+        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
+    Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i )
+        Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 );  // add - update
+    
+    // check predicted improvement: (new SOP lits == old SOP lits - divisor weight)
+    //assert( p->nLits == nLitsNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the improved fast_extract algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Fxch_PrintStats( Fxch_Man_t * p, abctime clk )
+{
+    printf( "Num =%6d  ", Vec_WrdSize(&p->vDivs) - p->nVars );
+    printf( "Cubes =%8d  ", Vec_WecSizeUsed(&p->vCubes) );
+    printf( "Lits  =%8d  ", p->nLits );
+    printf( "Divs  =%8d  ", Hash_IntManEntryNum(p->vHash) );
+    printf( "Divs+ =%8d  ", Vec_QueSize(p->vPrio) );
+    printf( "PairS =%6d  ", p->nPairsS );
+    printf( "PairD =%6d  ", p->nPairsD );
+    Abc_PrintTime( 1, "Time", clk );
+//    printf( "\n" );
+}
+static inline void Fxch_PrintDivOne( Fxch_Man_t * p, int iDiv )
+{
+    int i;
+    int Lit0 = Hash_IntObjData0( p->vHash, iDiv );
+    int Lit1 = Hash_IntObjData1( p->vHash, iDiv );
+    assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 );
+    printf( "Div %4d : ", iDiv );
+    printf( "Weight %12.5f  ", Vec_FltEntry(&p->vWeights, iDiv) );
+    printf( "Pairs = %5d  ",   Vec_IntSize(Vec_WecEntry(&p->vPairs, iDiv))/2 );
+    for ( i = 0; i < Vec_WrdSize(&p->vDivs); i++ )
+    {
+        if ( i == Abc_Lit2Var(Lit0) )
+            printf( "%d", !Abc_LitIsCompl(Lit0) );
+        else if ( i == Abc_Lit2Var(Lit1) )
+            printf( "%d", !Abc_LitIsCompl(Lit1) );
+        else
+            printf( "-" );
+    }
+    printf( "\n" );
+}
+static void Fxch_PrintDivisors( Fxch_Man_t * p )
+{
+    int iDiv;
+    for ( iDiv = 1; iDiv < Vec_FltSize(&p->vWeights); iDiv++ )
+        Fxch_PrintDivOne( p, iDiv );
+    printf( "\n" );
+}
+
+int Fxch_ManFastExtract( Fxch_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+    int nNewNodesMax = ABC_INFINITY;
+    abctime clk = Abc_Clock();
+    int i, iDiv;
+    Fxch_ManCreateDivisors( p );
+//    Fxch_PrintDivisors( p );
+    if ( fVerbose )
+        Fxch_PrintStats( p, Abc_Clock() - clk );
+    p->timeStart = Abc_Clock();
+    for ( i = 0; i < nNewNodesMax && Vec_QueTopPriority(p->vPrio) > 0.0; i++ )
+    {
+        iDiv = Vec_QuePop(p->vPrio);
+        //if ( fVerbose )
+        //    Fxch_PrintStats( p, Abc_Clock() - clk );
+        if ( fVeryVerbose )
+            Fxch_PrintDivOne( p, iDiv );
+        Fxch_ManUpdate( p, iDiv );
+    }
+    if ( fVerbose )
+        Fxch_PrintStats( p, Abc_Clock() - clk );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the improved fast_extract algorithm.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pla_ManPerformFxch( Pla_Man_t * p )
+{
+    char pFileName[1000];
+    Fxch_Man_t * pFxch;
+    Pla_ManConvertFromBits( p );
+    pFxch = Fxch_ManStart( &p->vCubeLits, &p->vOccurs );
+    Vec_WecZero( &p->vCubeLits );
+    Vec_WecZero( &p->vOccurs );
+    Fxch_ManFastExtract( pFxch, 1, 0 );
+    sprintf( pFileName, "%s.blif", Pla_ManName(p) );
+    //Fxch_ManWriteBlif( pFileName, &pFxch->vCubes, &pFxch->vDivs );
+    Fxch_ManStop( pFxch );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+