/**CFile****************************************************************

  FileName    [giaKf.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Cut computation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: giaKf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "gia.h"
#include "misc/vec/vecSet.h"

#ifdef ABC_USE_PTHREADS

#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif

#endif

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

#ifndef ABC_USE_PTHREADS

void Kf_ManSetDefaultPars( Jf_Par_t * pPars ) {}
Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) { return NULL; }

#else // pthreads are used

#define KF_LEAF_MAX  16
#define KF_CUT_MAX   32
#define KF_PROC_MAX  32
#define KF_WORD_MAX  ((KF_LEAF_MAX > 6) ? 1 << (KF_LEAF_MAX-6) : 1)
#define KF_LOG_TABLE  8

#define KF_ADD_ON1    2  // offset in cut storage for each node (cut count; best cut)
#define KF_ADD_ON2    4  // offset in cut storage for each cut (leaf count; function, cut delay; cut area)

typedef struct Kf_Cut_t_ Kf_Cut_t; 
typedef struct Kf_Set_t_ Kf_Set_t; 
typedef struct Kf_Man_t_ Kf_Man_t; 

struct Kf_Cut_t_
{
    word            Sign;        // signature
    int             Polar;       // polarity
    int             Delay;       // delay
    float           Area;        // area 
    int             iFunc;       // function 
    int             iNext;       // next cut
    int             nLeaves;     // number of leaves
    int             pLeaves[KF_LEAF_MAX]; 
};
struct Kf_Set_t_
{
    Kf_Man_t *      pMan;        // manager
    unsigned short  nLutSize;    // lut size
    unsigned short  nCutNum;     // cut count
    int             nCuts0;      // fanin0 cut count
    int             nCuts1;      // fanin1 cut count
    int             nCuts;       // resulting cut count
    int             nTEntries;   // hash table entries 
    int             TableMask;   // hash table mask
    int             pTable[1 << KF_LOG_TABLE];
    int             pValue[1 << KF_LOG_TABLE];
    int             pPlace[KF_LEAF_MAX];
    int             pList [KF_LEAF_MAX+1];
    Kf_Cut_t        pCuts0[KF_CUT_MAX];
    Kf_Cut_t        pCuts1[KF_CUT_MAX];
    Kf_Cut_t        pCutsR[KF_CUT_MAX*KF_CUT_MAX];
    Kf_Cut_t *      ppCuts[KF_CUT_MAX];
    Kf_Cut_t *      pCutBest;
    word            CutCount[4]; // statistics
};
struct Kf_Man_t_
{
    Gia_Man_t *     pGia;        // user's manager
    Jf_Par_t *      pPars;       // user's parameters
    Vec_Set_t       pMem;        // cut storage
    Vec_Int_t       vCuts;       // node params
    Vec_Int_t       vTime;       // node params
    Vec_Flt_t       vArea;       // node params
    Vec_Flt_t       vRefs;       // node params
    Vec_Int_t *     vTemp;       // temporary
    abctime         clkStart;    // starting time
    Kf_Set_t        pSett[KF_PROC_MAX];
};

static inline int   Kf_SetCutId( Kf_Set_t * p, Kf_Cut_t * pCut )           { return pCut - p->pCutsR;               }
static inline Kf_Cut_t * Kf_SetCut( Kf_Set_t * p, int i )                  { return i >= 0 ? p->pCutsR + i : NULL;  }

static inline int   Kf_ObjTime( Kf_Man_t * p, int i )                      { return Vec_IntEntry(&p->vTime, i);     }
static inline float Kf_ObjArea( Kf_Man_t * p, int i )                      { return Vec_FltEntry(&p->vArea, i);     }
static inline float Kf_ObjRefs( Kf_Man_t * p, int i )                      { return Vec_FltEntry(&p->vRefs, i);     }

static inline void  Kf_ObjSetCuts( Kf_Man_t * p, int i, Vec_Int_t * vVec ) { Vec_IntWriteEntry(&p->vCuts, i, Vec_SetAppend(&p->pMem, Vec_IntArray(vVec), Vec_IntSize(vVec)));  }
static inline int * Kf_ObjCuts( Kf_Man_t * p, int i )                      { return (int *)Vec_SetEntry(&p->pMem, Vec_IntEntry(&p->vCuts, i));    }
static inline int * Kf_ObjCuts0( Kf_Man_t * p, int i )                     { return Kf_ObjCuts(p, Gia_ObjFaninId0(Gia_ManObj(p->pGia, i), i));    }
static inline int * Kf_ObjCuts1( Kf_Man_t * p, int i )                     { return Kf_ObjCuts(p, Gia_ObjFaninId1(Gia_ManObj(p->pGia, i), i));    }
static inline int * Kf_ObjCutBest( Kf_Man_t * p, int i )                   { int * pCuts = Kf_ObjCuts(p, i); return pCuts + pCuts[1];             }

#define Kf_ObjForEachCutInt( pList, pCut, i )        for ( i = 0, pCut = pList + KF_ADD_ON1; i < pList[0]; i++, pCut += pCut[0] + KF_ADD_ON2 )
#define Kf_ListForEachCut( p, iList, pCut )          for ( pCut = Kf_SetCut(p, p->pList[iList]); pCut; pCut = Kf_SetCut(p, pCut->iNext) )
#define Kf_ListForEachCutP( p, iList, pCut, pPlace ) for ( pPlace = p->pList+iList, pCut = Kf_SetCut(p, *pPlace); pCut; pCut = Kf_SetCut(p, *pPlace) )

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Kf_SetLoadCuts( Kf_Cut_t * pCuts, int * pIntCuts )
{
    Kf_Cut_t * pCut;
    int k, * pIntCut, nCuts = 0; 
    Kf_ObjForEachCutInt( pIntCuts, pIntCut, nCuts )
    {
        pCut = pCuts + nCuts;
        pCut->Sign  = 0;
        pCut->Polar = 0;
        pCut->iFunc = pIntCut[pIntCut[0] + 1];
        pCut->Delay = pIntCut[pIntCut[0] + 2];
        pCut->Area  = Abc_Int2Float(pIntCut[pIntCut[0] + 3]);
        pCut->nLeaves = pIntCut[0];    
        for ( k = 0; k < pIntCut[0]; k++ )
        {
            pCut->pLeaves[k] = Abc_Lit2Var(pIntCut[k+1]);
            pCut->Sign |= ((word)1) << (pCut->pLeaves[k] & 0x3F);
            if ( Abc_LitIsCompl(pIntCut[k+1]) )
                pCut->Polar |= (1 << k);
        }
    }
    return nCuts;
}
static inline void Kf_SetPrepare( Kf_Set_t * p, int * pCuts0, int * pCuts1 )
{
    int i;
    // prepare hash table
//    for ( i = 0; i <= p->TableMask; i++ )
//        assert( p->pTable[i] == 0 );
    // prepare cut storage
    for ( i = 0; i <= p->nLutSize; i++ )
        p->pList[i] = -1;
    // transfer cuts
    p->nCuts0 = Kf_SetLoadCuts( p->pCuts0, pCuts0 );
    p->nCuts1 = Kf_SetLoadCuts( p->pCuts1, pCuts1 );
    p->nCuts = 0;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Kf_ManStoreStart( Vec_Int_t * vTemp, int nCuts )
{
    Vec_IntClear( vTemp );
    Vec_IntPush( vTemp, nCuts );                // cut count
    Vec_IntPush( vTemp, -1 );                   // best offset
}
static inline void Kf_ManStoreAddUnit( Vec_Int_t * vTemp, int iObj, int Time, float Area )
{
    Vec_IntAddToEntry( vTemp, 0, 1 );
    Vec_IntPush( vTemp, 1 );                    // cut size
    Vec_IntPush( vTemp, Abc_Var2Lit(iObj, 0) ); // leaf
    Vec_IntPush( vTemp, 2 );                    // function
    Vec_IntPush( vTemp, Time );                 // delay
    Vec_IntPush( vTemp, Abc_Float2Int(Area) );  // area
}
static inline void Kf_ManSaveResults( Kf_Cut_t ** ppCuts, int nCuts, Kf_Cut_t * pCutBest, Vec_Int_t * vTemp )
{
    int i, k;
    assert( nCuts > 0 && nCuts < KF_CUT_MAX );
    Kf_ManStoreStart( vTemp, nCuts );
    for ( i = 0; i < nCuts; i++ )
    {
        if ( ppCuts[i] == pCutBest )
            Vec_IntWriteEntry( vTemp, 1, Vec_IntSize(vTemp) );
        Vec_IntPush( vTemp, ppCuts[i]->nLeaves );
//        Vec_IntPushArray( vTemp, ppCuts[i]->pLeaves, ppCuts[i]->nLeaves );
        for ( k = 0; k < ppCuts[i]->nLeaves; k++ )
            Vec_IntPush( vTemp, Abc_Var2Lit(ppCuts[i]->pLeaves[k], 0) );
        Vec_IntPush( vTemp, ppCuts[i]->iFunc );
        Vec_IntPush( vTemp, ppCuts[i]->Delay );
        Vec_IntPush( vTemp, Abc_Float2Int(ppCuts[i]->Area) );
    }
    assert( Vec_IntEntry(vTemp, 1) > 0 );
}
static inline int Kf_SetCompareCuts( Kf_Cut_t * p1, Kf_Cut_t * p2 )
{
    if ( p1 == NULL || p2 == NULL )
        return (p1 != NULL) - (p2 != NULL);
    if ( p1->nLeaves != p2->nLeaves )
        return p1->nLeaves - p2->nLeaves;
    return memcmp( p1->pLeaves, p2->pLeaves, sizeof(int)*p1->nLeaves );
}
static inline void Kf_SetAddToList( Kf_Set_t * p, Kf_Cut_t * pCut, int fSort )
{
    if ( !fSort )
        pCut->iNext = p->pList[pCut->nLeaves], p->pList[pCut->nLeaves] = Kf_SetCutId(p, pCut);
    else
    {
        int Value, * pPlace;
        Kf_Cut_t * pTemp;
        Vec_IntSelectSort( pCut->pLeaves, pCut->nLeaves );
        Kf_ListForEachCutP( p, pCut->nLeaves, pTemp, pPlace )
        {
            if ( (Value = Kf_SetCompareCuts(pTemp, pCut)) > 0 )
                break;
            assert( Value < 0 );
            pPlace = &pTemp->iNext;
        }
        pCut->iNext = *pPlace, *pPlace = Kf_SetCutId(p, pCut);
    }
}
static inline int Kf_CutCompare( Kf_Cut_t * pCut0, Kf_Cut_t * pCut1, int fArea )
{
    if ( fArea )
    {
        if ( pCut0->Area    < pCut1->Area )    return -1;
        if ( pCut0->Area    > pCut1->Area )    return  1;
        if ( pCut0->Delay   < pCut1->Delay )   return -1;
        if ( pCut0->Delay   > pCut1->Delay )   return  1;
        if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
        if ( pCut0->nLeaves > pCut1->nLeaves ) return  1;
    }
    else
    {
        if ( pCut0->Delay   < pCut1->Delay )   return -1;
        if ( pCut0->Delay   > pCut1->Delay )   return  1;
        if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
        if ( pCut0->nLeaves > pCut1->nLeaves ) return  1;
        if ( pCut0->Area    < pCut1->Area )    return -1;
        if ( pCut0->Area    > pCut1->Area )    return  1;
    }
    return 0;
}
static inline int Kf_SetStoreAddOne( Kf_Set_t * p, int nCuts, int nCutNum, Kf_Cut_t * pCut, int fArea )
{
    int i;
    p->ppCuts[nCuts] = pCut;
    if ( nCuts == 0 )
        return 1;
    for ( i = nCuts; i > 0; i-- )
        if ( Kf_CutCompare(p->ppCuts[i-1], p->ppCuts[i], fArea) > 0 )
            ABC_SWAP( Kf_Cut_t *, p->ppCuts[i-1], p->ppCuts[i] )
        else
            break;
    return Abc_MinInt( nCuts+1, nCutNum );
}
static inline void Kf_SetSelectBest( Kf_Set_t * p, int fArea, int fSort )
{
//    int fArea = p->pMan->pPars->fArea;
    Kf_Cut_t * pCut;
    int i, nCuts = 0;
    for ( i = 0; i <= p->nLutSize; i++ )
        Kf_ListForEachCut( p, i, pCut )
            nCuts = Kf_SetStoreAddOne( p, nCuts, p->nCutNum-1, pCut, fArea );
    assert( nCuts > 0 && nCuts < p->nCutNum );
    p->nCuts = nCuts;
    p->pCutBest = p->ppCuts[0];
    if ( !fSort )
        return;
    // sort by size in the reverse order
    for ( i = 0; i <= p->nLutSize; i++ )
        p->pList[i] = -1;
    for ( i = 0; i < nCuts; i++ )
        Kf_SetAddToList( p, p->ppCuts[i], 0 );
    p->nCuts = 0;
    for ( i = p->nLutSize; i >= 0; i-- )
        Kf_ListForEachCut( p, i, pCut )
            p->ppCuts[p->nCuts++] = pCut;
    assert( p->nCuts == nCuts );
}

/**Function*************************************************************

  Synopsis    [Check correctness of cuts.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Kf_CheckCut( Kf_Cut_t * pBase, Kf_Cut_t * pCut ) // check if pCut is contained in pBase
{
    int nSizeB = pBase->nLeaves;
    int nSizeC = pCut->nLeaves;
    int * pB = pBase->pLeaves;
    int * pC = pCut->pLeaves;
    int i, k;
    for ( i = 0; i < nSizeC; i++ )
    {
        for ( k = 0; k < nSizeB; k++ )
            if ( pC[i] == pB[k] )
                break;
        if ( k == nSizeB )
            return 0;
    }
    return 1;
}
static inline int Kf_CheckCuts( Kf_Set_t * p )
{
    Kf_Cut_t * pCut0, * pCut1; 
    int i, k, m, n, Value;
    assert( p->nCuts > 0 );
    for ( i = 0; i <= p->nLutSize; i++ )
    Kf_ListForEachCut( p, i, pCut0 )
    {
        // check duplicates
        for ( m = 0; m < pCut0->nLeaves; m++ )
        for ( n = m+1; n < pCut0->nLeaves; n++ )
            assert( pCut0->pLeaves[m] != pCut0->pLeaves[n] );
        // check pairs
        for ( k = 0; k <= p->nLutSize; k++ )
        Kf_ListForEachCut( p, k, pCut1 )
        {
            if ( pCut0 == pCut1 )
                continue;
            // check containments
            Value = Kf_CheckCut( pCut0, pCut1 );
            assert( Value == 0 );
        }
    }
    return 1;
}

/**Function*************************************************************

  Synopsis    [Hash table.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Kf_HashLookup( Kf_Set_t * p, int i )
{
    int k;
    assert( i > 0 );
    for ( k = i & p->TableMask; p->pTable[k]; k = (k + 1) & p->TableMask )
        if ( p->pTable[k] == i )
            return -1;
    return k;
}
static inline int Kf_HashFindOrAdd( Kf_Set_t * p, int i )
{
    int k = Kf_HashLookup( p, i );
    if ( k == -1 )
        return 0;
    if ( p->nTEntries == p->nLutSize )
        return 1;
    assert( p->pTable[k] == 0 );
    p->pTable[k] = i;
    p->pPlace[p->nTEntries] = k;
    p->pValue[k] = p->nTEntries++;
    return 0;
}
static inline void Kf_HashPopulate( Kf_Set_t * p, Kf_Cut_t * pCut )
{
    int i;
    assert( p->nTEntries == 0 );
    for ( i = 0; i < pCut->nLeaves; i++ )
        Kf_HashFindOrAdd( p, pCut->pLeaves[i] );
    assert( p->nTEntries == pCut->nLeaves );
}
static inline void Kf_HashCleanup( Kf_Set_t * p, int iStart )
{
    int i;
    for ( i = iStart; i < p->nTEntries; i++ )
        p->pTable[p->pPlace[i]] = 0;
    p->nTEntries = iStart;
}

/**Function*************************************************************

  Synopsis    [Cut merging with arbitary order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Kf_SetCountBits( word i )
{
    i = i - ((i >> 1) & 0x5555555555555555);
    i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
    i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
    return (i*(0x0101010101010101))>>56;
}
static inline word Kf_SetCutGetSign( Kf_Cut_t * p )
{
    word Sign = 0; int i; 
    for ( i = 0; i < p->nLeaves; i++ )
        Sign |= ((word)1) << (p->pLeaves[i] & 0x3F);
    return Sign;
}
// returns 1 if the cut in hash table is dominated by the given one
static inline int Kf_SetCutDominatedByThis( Kf_Set_t * p, Kf_Cut_t * pCut )
{
    int i;
    for ( i = 0; i < pCut->nLeaves; i++ )
        if ( Kf_HashLookup(p, pCut->pLeaves[i]) >= 0 )
            return 0;
    return 1;
}
static inline int Kf_SetRemoveDuplicates( Kf_Set_t * p, int nLeaves, word Sign )
{
    Kf_Cut_t * pCut; 
    Kf_ListForEachCut( p, nLeaves, pCut )
        if ( pCut->Sign == Sign && Kf_SetCutDominatedByThis(p, pCut) )
            return 1;
    return 0;
}
static inline void Kf_SetFilter( Kf_Set_t * p )
{
    Kf_Cut_t * pCut0, * pCut1; 
    int i, k, * pPlace;
    assert( p->nCuts > 0 );
    for ( i = 0; i <= p->nLutSize; i++ )
        Kf_ListForEachCutP( p, i, pCut0, pPlace )
        {
            Kf_HashPopulate( p, pCut0 );
            for ( k = 0; k < pCut0->nLeaves; k++ )
                Kf_ListForEachCut( p, k, pCut1 )
                    if ( (pCut0->Sign & pCut1->Sign) == pCut1->Sign && Kf_SetCutDominatedByThis(p, pCut1) )
                        { k = pCut0->nLeaves; p->nCuts--; break; }
            if ( k == pCut0->nLeaves + 1 ) // remove pCut0
                *pPlace = pCut0->iNext;
            else
                pPlace = &pCut0->iNext;
            Kf_HashCleanup( p, 0 );
        }
    assert( p->nCuts > 0 );
}
static inline void Kf_SetMergePairs( Kf_Set_t * p, Kf_Cut_t * pCut0, Kf_Cut_t * pCuts, int nCuts, int fArea )
{
    Kf_Cut_t * pCut1, * pCutR;  int i;
    Kf_HashPopulate( p, pCut0 );
    for ( pCut1 = pCuts; pCut1 < pCuts + nCuts; pCut1++ )
    {
        if ( pCut0->nLeaves + pCut1->nLeaves > p->nLutSize && Kf_SetCountBits(pCut0->Sign | pCut1->Sign) > p->nLutSize )
            continue;
        Kf_HashCleanup( p, pCut0->nLeaves );
        for ( i = 0; i < pCut1->nLeaves; i++ )
            if ( Kf_HashFindOrAdd(p, pCut1->pLeaves[i]) )
                break;
        if ( i < pCut1->nLeaves )
            continue;
        p->CutCount[1]++;        
        if ( Kf_SetRemoveDuplicates(p, p->nTEntries, pCut0->Sign | pCut1->Sign) )
            continue;
        // create new cut
        pCutR = p->pCutsR + p->nCuts++;
        pCutR->nLeaves = p->nTEntries;
        for ( i = 0; i < p->nTEntries; i++ )
            pCutR->pLeaves[i] = p->pTable[p->pPlace[i]];
        pCutR->Sign  = pCut0->Sign | pCut1->Sign;
        pCutR->Delay = Abc_MaxInt(pCut0->Delay, pCut1->Delay);
        pCutR->Area  = pCut0->Area + pCut1->Area;
        // add new cut
        Kf_SetAddToList( p, pCutR, 0 );
    }
    Kf_HashCleanup( p, 0 );
}
static inline void Kf_SetMerge( Kf_Set_t * p, int * pCuts0, int * pCuts1, int fArea, int fCutMin )
{
    int c0, c1;
    Kf_SetPrepare( p, pCuts0, pCuts1 );
    p->CutCount[0] += p->nCuts0 * p->nCuts1;
//    for ( c0 = 1; c0 < p->nCuts0; c0++ )
//        assert( p->pCuts0[c0-1].nLeaves >= p->pCuts0[c0].nLeaves );
    for ( c0 = c1 = 0; c0 < p->nCuts0 && c1 < p->nCuts1; )
    {
        if ( p->pCuts0[c0].nLeaves >= p->pCuts1[c1].nLeaves )
            Kf_SetMergePairs( p, p->pCuts0 + c0++, p->pCuts1 + c1, p->nCuts1 - c1, fArea );
        else 
            Kf_SetMergePairs( p, p->pCuts1 + c1++, p->pCuts0 + c0, p->nCuts0 - c0, fArea );
    }
    p->CutCount[2] += p->nCuts;        
    Kf_SetFilter( p );
//    Kf_CheckCuts( p );
    p->CutCount[3] += Abc_MinInt( p->nCuts, p->nCutNum-1 );
    Kf_SetSelectBest( p, fArea, 1 );
}

/**Function*************************************************************

  Synopsis    [Cut merging with fixed order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Kf_SetCutIsContainedSimple( Kf_Cut_t * pBase, Kf_Cut_t * pCut ) // check if pCut is contained in pBase
{
    int nSizeB = pBase->nLeaves;
    int nSizeC = pCut->nLeaves;
    int * pB = pBase->pLeaves;
    int * pC = pCut->pLeaves;
    int i, k;
    assert( nSizeB >= nSizeC ); 
    for ( i = 0; i < nSizeC; i++ )
    {
        for ( k = 0; k < nSizeB; k++ )
            if ( pC[i] == pB[k] )
                break;
        if ( k == nSizeB )
            return 0;
    }
    return 1;
}
static inline int Kf_SetMergeSimpleOne( Kf_Cut_t * pCut0, Kf_Cut_t * pCut1, Kf_Cut_t * pCut, int nLutSize )
{ 
    int nSize0 = pCut0->nLeaves;
    int nSize1 = pCut1->nLeaves;
    int * pC0 = pCut0->pLeaves;
    int * pC1 = pCut1->pLeaves;
    int * pC = pCut->pLeaves;
    int i, k, c;
    // compare two cuts with different numbers
    c = nSize0;
    for ( i = 0; i < nSize1; i++ )
    {
        for ( k = 0; k < nSize0; k++ )
            if ( pC1[i] == pC0[k] )
                break;
        if ( k < nSize0 )
            continue;
        if ( c == nLutSize )
            return 0;
        pC[c++] = pC1[i];
    }
    for ( i = 0; i < nSize0; i++ )
        pC[i] = pC0[i];
    pCut->nLeaves = c;
    return 1;
}
static inline int Kf_SetRemoveDuplicatesSimple( Kf_Set_t * p, Kf_Cut_t * pCutNew )
{
    Kf_Cut_t * pCut;
    Kf_ListForEachCut( p, pCutNew->nLeaves, pCut )
        if ( pCut->Sign == pCutNew->Sign && Kf_SetCutIsContainedSimple(pCut, pCutNew) )
            return 1;
    return 0;
}
static inline void Kf_SetFilterSimple( Kf_Set_t * p )
{
    Kf_Cut_t * pCut0, * pCut1; 
    int i, k, * pPlace;
    assert( p->nCuts > 0 );
    for ( i = 0; i <= p->nLutSize; i++ )
        Kf_ListForEachCutP( p, i, pCut0, pPlace )
        {
            for ( k = 0; k < pCut0->nLeaves; k++ )
                Kf_ListForEachCut( p, k, pCut1 )
                    if ( (pCut0->Sign & pCut1->Sign) == pCut1->Sign && Kf_SetCutIsContainedSimple(pCut0, pCut1) )
                        { k = pCut0->nLeaves; p->nCuts--; break; }
            if ( k == pCut0->nLeaves + 1 ) // remove pCut0
                *pPlace = pCut0->iNext;
            else
                pPlace = &pCut0->iNext;
        }
    assert( p->nCuts > 0 );
}
static inline void Kf_SetMergeSimple( Kf_Set_t * p, int * pCuts0, int * pCuts1, int fArea, int fCutMin )
{
    Kf_Cut_t * pCut0, * pCut1, * pCutR;
    Kf_SetPrepare( p, pCuts0, pCuts1 );
    p->CutCount[0] += p->nCuts0 * p->nCuts1;
    for ( pCut0 = p->pCuts0; pCut0 < p->pCuts0 + p->nCuts0; pCut0++ )
    for ( pCut1 = p->pCuts1; pCut1 < p->pCuts1 + p->nCuts1; pCut1++ )
    {
        if ( pCut0->nLeaves + pCut1->nLeaves > p->nLutSize && Kf_SetCountBits(pCut0->Sign | pCut1->Sign) > p->nLutSize )
            continue;
        p->CutCount[1]++;        
        pCutR = p->pCutsR + p->nCuts;
        if ( !Kf_SetMergeSimpleOne(pCut0, pCut1, pCutR, p->nLutSize) )
            continue;
        p->CutCount[2]++;        
        pCutR->Sign = pCut0->Sign | pCut1->Sign;
        if ( Kf_SetRemoveDuplicatesSimple(p, pCutR) )
            continue;
        p->nCuts++;
        if ( fCutMin )
        {
            int nOldSupp = pCutR->nLeaves;
//            pCutR->iFunc = Kf_SetComputeTruth( p, pCut0->iFunc, pCut1->iFunc, pCut0, pCut1, pCutR );
            assert( pCutR->nLeaves <= nOldSupp );
            if ( pCutR->nLeaves < nOldSupp )
                pCutR->Sign = Kf_SetCutGetSign( pCutR );
            // delay and area are inaccurate
        }
        assert( pCutR->nLeaves > 1 );
        pCutR->Delay = Abc_MaxInt(pCut0->Delay, pCut1->Delay);
        pCutR->Area  = pCut0->Area + pCut1->Area;
        // add new cut
        Kf_SetAddToList( p, pCutR, 0 );
    }
    Kf_SetFilterSimple( p );
//    Kf_CheckCuts( p );
    p->CutCount[3] += Abc_MinInt( p->nCuts, p->nCutNum-1 );
    Kf_SetSelectBest( p, fArea, 1 );
}

/**Function*************************************************************

  Synopsis    [Cut merging with fixed order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Kf_SetCutIsContainedOrder( Kf_Cut_t * pBase, Kf_Cut_t * pCut ) // check if pCut is contained in pBase
{
    int nSizeB = pBase->nLeaves;
    int nSizeC = pCut->nLeaves;
    int i, k;
    if ( nSizeB == nSizeC )
    {
        for ( i = 0; i < nSizeB; i++ )
            if ( pBase->pLeaves[i] != pCut->pLeaves[i] )
                return 0;
        return 1;
    }
    assert( nSizeB > nSizeC ); 
    for ( i = k = 0; i < nSizeB; i++ )
    {
        if ( pBase->pLeaves[i] > pCut->pLeaves[k] )
            return 0;
        if ( pBase->pLeaves[i] == pCut->pLeaves[k] )
        {
            if ( ++k == nSizeC )
                return 1;
        }
    }
    return 0;
}
static inline int Kf_SetMergeOrderOne( Kf_Cut_t * pCut0, Kf_Cut_t * pCut1, Kf_Cut_t * pCut, int nLutSize )
{ 
    int nSize0 = pCut0->nLeaves;
    int nSize1 = pCut1->nLeaves;
    int * pC0 = pCut0->pLeaves;
    int * pC1 = pCut1->pLeaves;
    int * pC = pCut->pLeaves;
    int i, k, c;
    // the case of the largest cut sizes
    if ( nSize0 == nLutSize && nSize1 == nLutSize )
    {
        for ( i = 0; i < nSize0; i++ )
        {
            if ( pC0[i] != pC1[i] )  return 0;
            pC[i] = pC0[i];
        }
        pCut->nLeaves = nLutSize;
        return 1;
    }
    // compare two cuts with different numbers
    i = k = c = 0;
    while ( 1 )
    {
        if ( c == nLutSize ) return 0;
        if ( pC0[i] < pC1[k] )
        {
            pC[c++] = pC0[i++];
            if ( i >= nSize0 ) goto FlushCut1;
        }
        else if ( pC0[i] > pC1[k] )
        {
            pC[c++] = pC1[k++];
            if ( k >= nSize1 ) goto FlushCut0;
        }
        else
        {
            pC[c++] = pC0[i++]; k++;
            if ( i >= nSize0 ) goto FlushCut1;
            if ( k >= nSize1 ) goto FlushCut0;
        }
    }

FlushCut0:
    if ( c + nSize0 > nLutSize + i ) return 0;
    while ( i < nSize0 )
        pC[c++] = pC0[i++];
    pCut->nLeaves = c;
    return 1;

FlushCut1:
    if ( c + nSize1 > nLutSize + k ) return 0;
    while ( k < nSize1 )
        pC[c++] = pC1[k++];
    pCut->nLeaves = c;
    return 1;
}
static inline int Kf_SetRemoveDuplicatesOrder( Kf_Set_t * p, Kf_Cut_t * pCutNew )
{
    Kf_Cut_t * pCut;
    Kf_ListForEachCut( p, pCutNew->nLeaves, pCut )
        if ( pCut->Sign == pCutNew->Sign && Kf_SetCutIsContainedOrder(pCut, pCutNew) )
            return 1;
    return 0;
}
static inline void Kf_SetFilterOrder( Kf_Set_t * p )
{
    Kf_Cut_t * pCut0, * pCut1; 
    int i, k, * pPlace;
    assert( p->nCuts > 0 );
    for ( i = 0; i <= p->nLutSize; i++ )
        Kf_ListForEachCutP( p, i, pCut0, pPlace )
        {
            for ( k = 0; k < pCut0->nLeaves; k++ )
                Kf_ListForEachCut( p, k, pCut1 )
                    if ( (pCut0->Sign & pCut1->Sign) == pCut1->Sign && Kf_SetCutIsContainedOrder(pCut0, pCut1) )
                        { k = pCut0->nLeaves; p->nCuts--; break; }
            if ( k == pCut0->nLeaves + 1 ) // remove pCut0
                *pPlace = pCut0->iNext;
            else
                pPlace = &pCut0->iNext;
        }
    assert( p->nCuts > 0 );
}
/*
int Kf_SetComputeTruth( Kf_Man_t * p, int iFuncLit0, int iFuncLit1, int * pCut0, int * pCut1, int * pCutOut )
{
    word uTruth[JF_WORD_MAX], uTruth0[JF_WORD_MAX], uTruth1[JF_WORD_MAX];
    int fCompl, truthId;
    int LutSize    = p->pPars->nLutSize;
    int nWords     = Abc_Truth6WordNum(p->pPars->nLutSize);
    word * pTruth0 = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(iFuncLit0));
    word * pTruth1 = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(iFuncLit1));
    Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(iFuncLit0) );
    Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(iFuncLit1) );
    Abc_TtExpand( uTruth0, LutSize, pCut0 + 1, Kf_CutSize(pCut0), pCutOut + 1, Kf_CutSize(pCutOut) );
    Abc_TtExpand( uTruth1, LutSize, pCut1 + 1, Kf_CutSize(pCut1), pCutOut + 1, Kf_CutSize(pCutOut) );
    fCompl         = (int)(uTruth0[0] & uTruth1[0] & 1);
    Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, fCompl );
    pCutOut[0]     = Abc_TtMinBase( uTruth, pCutOut + 1, pCutOut[0], LutSize );
    assert( (uTruth[0] & 1) == 0 );
    truthId        = Vec_MemHashInsert(p->vTtMem, uTruth);
    return Abc_Var2Lit( truthId, fCompl );
}
*/
static inline void Kf_SetMergeOrder( Kf_Set_t * p, int * pCuts0, int * pCuts1, int fArea, int fCutMin )
{
    Kf_Cut_t * pCut0, * pCut1, * pCutR;
    Kf_SetPrepare( p, pCuts0, pCuts1 );
    p->CutCount[0] += p->nCuts0 * p->nCuts1;
    for ( pCut0 = p->pCuts0; pCut0 < p->pCuts0 + p->nCuts0; pCut0++ )
    for ( pCut1 = p->pCuts1; pCut1 < p->pCuts1 + p->nCuts1; pCut1++ )
    {
        if ( pCut0->nLeaves + pCut1->nLeaves > p->nLutSize && Kf_SetCountBits(pCut0->Sign | pCut1->Sign) > p->nLutSize )
            continue;
        p->CutCount[1]++;        
        pCutR = p->pCutsR + p->nCuts;
        if ( !Kf_SetMergeOrderOne(pCut0, pCut1, pCutR, p->nLutSize) )
            continue;
        p->CutCount[2]++;        
        pCutR->Sign = pCut0->Sign | pCut1->Sign;
        if ( Kf_SetRemoveDuplicatesOrder(p, pCutR) )
            continue;
        p->nCuts++;
        if ( fCutMin )
        {
            int nOldSupp = pCutR->nLeaves;
//            pCutR->iFunc = Kf_SetComputeTruth( p, pCut0->iFunc, pCut1->iFunc, pCut0, pCut1, pCutR );
            assert( pCutR->nLeaves <= nOldSupp );
            if ( pCutR->nLeaves < nOldSupp )
                pCutR->Sign = Kf_SetCutGetSign( pCutR );
            // delay and area are inaccurate
        }
        assert( pCutR->nLeaves > 1 );
        pCutR->Delay = Abc_MaxInt(pCut0->Delay, pCut1->Delay);
        pCutR->Area  = pCut0->Area + pCut1->Area;
        // add new cut
        Kf_SetAddToList( p, pCutR, 0 );
    }
    Kf_SetFilterOrder( p );
//    Kf_CheckCuts( p );
    p->CutCount[3] += Abc_MinInt( p->nCuts, p->nCutNum-1 );
    Kf_SetSelectBest( p, fArea, 1 );
}


/**Function*************************************************************

  Synopsis    [Cut operations.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int  Kf_CutSize( int * pCut )         { return pCut[0];                          } 
static inline int  Kf_CutFunc( int * pCut )         { return pCut[pCut[0] + 1];                } 
static inline int  Kf_CutLeaf( int * pCut, int i )  { assert(i); return Abc_Lit2Var(pCut[i]);  }
static inline int  Kf_CutTime( Kf_Man_t * p, int * pCut )
{
    int i, Time = 0;
    for ( i = 1; i <= Kf_CutSize(pCut); i++ )
        Time = Abc_MaxInt( Time, Kf_ObjTime(p, Kf_CutLeaf(pCut, i)) );
    return Time + 1; 
}
static inline void Kf_CutRef( Kf_Man_t * p, int * pCut )
{
    int i;
    for ( i = 1; i <= Kf_CutSize(pCut); i++ )
        Gia_ObjRefIncId( p->pGia, Kf_CutLeaf(pCut, i) );
}
static inline void Kf_CutDeref( Kf_Man_t * p, int * pCut )
{
    int i;
    for ( i = 1; i <= Kf_CutSize(pCut); i++ )
        Gia_ObjRefDecId( p->pGia, Kf_CutLeaf(pCut, i) );
}
static inline void Kf_CutPrint( int * pCut )
{
    int i; 
    printf( "%d {", Kf_CutSize(pCut) );
    for ( i = 1; i <= Kf_CutSize(pCut); i++ )
        printf( " %d", Kf_CutLeaf(pCut, i) );
    printf( " } Func = %d\n", Kf_CutFunc(pCut) );
}
static inline void Gia_CutSetPrint( int * pCuts )
{
    int i, * pCut; 
    Kf_ObjForEachCutInt( pCuts, pCut, i )
        Kf_CutPrint( pCut );
    printf( "\n" );
}

/**Function*************************************************************

  Synopsis    [Computing delay/area.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Kf_ManComputeDelay( Kf_Man_t * p, int fEval )
{
    Gia_Obj_t * pObj; 
    int i, Delay = 0;
    if ( fEval )
    {
        Gia_ManForEachAnd( p->pGia, pObj, i )
            if ( Gia_ObjRefNum(p->pGia, pObj) > 0 )
                Vec_IntWriteEntry( &p->vTime, i, Kf_CutTime(p, Kf_ObjCutBest(p, i)) );
    }
    Gia_ManForEachCoDriver( p->pGia, pObj, i )
    {
        assert( Gia_ObjRefNum(p->pGia, pObj) > 0 );
        Delay = Abc_MaxInt( Delay, Kf_ObjTime(p, Gia_ObjId(p->pGia, pObj)) );
    }
    return Delay;
}
int Kf_ManComputeRefs( Kf_Man_t * p )
{
    Gia_Obj_t * pObj; 
    float nRefsNew; int i, * pCut;
    float * pRefs = Vec_FltArray(&p->vRefs);
    float * pFlow = Vec_FltArray(&p->vArea);
    assert( p->pGia->pRefs != NULL );
    memset( p->pGia->pRefs, 0, sizeof(int) * Gia_ManObjNum(p->pGia) );
    p->pPars->Area = p->pPars->Edge = 0;
    Gia_ManForEachObjReverse( p->pGia, pObj, i )
    {
        if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBuf(pObj) )
            Gia_ObjRefInc( p->pGia, Gia_ObjFanin0(pObj) );
        else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
        {
            pCut = Kf_ObjCutBest(p, i);
            Kf_CutRef( p, pCut );
            p->pPars->Edge += Kf_CutSize(pCut);
            p->pPars->Area++;
        }
    }
    // blend references and normalize flow
    for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
    {
        if ( p->pPars->fOptEdge )
            nRefsNew = Abc_MaxFloat( 1, 0.8 * pRefs[i] + 0.2 * p->pGia->pRefs[i] );
        else
            nRefsNew = Abc_MaxFloat( 1, 0.2 * pRefs[i] + 0.8 * p->pGia->pRefs[i] );
        pFlow[i] = pFlow[i] * pRefs[i] / nRefsNew;
        pRefs[i] = nRefsNew;
        assert( pFlow[i] >= 0 );
    }
    // compute delay
    p->pPars->Delay = Kf_ManComputeDelay( p, 1 );
    return p->pPars->Area;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
#define PAR_THR_MAX 100
typedef struct Kf_ThData_t_
{
    Kf_Set_t *  pSett;
    int         Id;
    int         Status;
    abctime     clkUsed;
} Kf_ThData_t;
void * Kf_WorkerThread( void * pArg )
{
    Kf_ThData_t * pThData = (Kf_ThData_t *)pArg;
    Kf_Man_t * pMan = pThData->pSett->pMan;
    int fAreaOnly = pThData->pSett->pMan->pPars->fAreaOnly;
    int fCutMin = pThData->pSett->pMan->pPars->fCutMin;
    volatile int * pPlace = &pThData->Status;
    abctime clk;
    while ( 1 )
    {
        while ( *pPlace == 0 );
        assert( pThData->Status == 1 );
        if ( pThData->Id == -1 )
        {
            pthread_exit( NULL );
            assert( 0 );
            return NULL;
        }
        assert( pThData->Id >= 0 );
        clk = Abc_Clock();
        Kf_SetMergeOrder( pThData->pSett, Kf_ObjCuts0(pMan, pThData->Id), Kf_ObjCuts1(pMan, pThData->Id), fAreaOnly, fCutMin );
        pThData->clkUsed += Abc_Clock() - clk;
        pThData->Status = 0;
//        printf( "Finished object %d\n", pThData->Id );
    }
    assert( 0 );
    return NULL;
}
Vec_Int_t * Kf_ManCreateFaninCounts( Gia_Man_t * p )  
{
    Vec_Int_t * vCounts;
    Gia_Obj_t * pObj; int i;
    vCounts = Vec_IntAlloc( Gia_ManObjNum(p) );
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            Vec_IntPush( vCounts, 2 - Gia_ObjIsCi(Gia_ObjFanin0(pObj)) - Gia_ObjIsCi(Gia_ObjFanin1(pObj)) );
        else
            Vec_IntPush( vCounts, 0 );
    }
    assert( Vec_IntSize(vCounts) == Gia_ManObjNum(p) );
    return vCounts;
}
void Kf_ManComputeCuts( Kf_Man_t * p )
{
    pthread_t WorkerThread[PAR_THR_MAX];
    Kf_ThData_t ThData[PAR_THR_MAX];
    Vec_Int_t * vStack, * vFanins;
    Gia_Obj_t * pObj;
    int nProcs = p->pPars->nProcNum;
    int i, k, iFan, status, nCountFanins, fRunning;
    abctime clk, clkUsed = 0;
    assert( nProcs <= PAR_THR_MAX );
    // start fanins
    vFanins = Kf_ManCreateFaninCounts( p->pGia );
    Gia_ManStaticFanoutStart( p->pGia );
    // start the stack
    vStack = Vec_IntAlloc( 1000 );
    Gia_ManForEachObjReverse( p->pGia, pObj, k )
        if ( Gia_ObjIsAnd(pObj) && Vec_IntEntry(vFanins, k) == 0 )
            Vec_IntPush( vStack, k );
    // start the threads
    for ( i = 0; i < nProcs; i++ )
    {
        ThData[i].pSett = p->pSett + i;
        ThData[i].Id = -1;
        ThData[i].Status = 0;
        ThData[i].clkUsed = 0;
        status = pthread_create( WorkerThread + i, NULL, Kf_WorkerThread, (void *)(ThData + i) );  assert( status == 0 );
    }
    nCountFanins = Vec_IntSum(vFanins);
    fRunning = 1;
    while ( nCountFanins > 0 || Vec_IntSize(vStack) > 0 || fRunning )
    {
        for ( i = 0; i < nProcs; i++ )
        {
            if ( ThData[i].Status )
                continue;
            assert( ThData[i].Status == 0 );
            if ( ThData[i].Id >= 0 )
            {
                int iObj = ThData[i].Id;
                Kf_Set_t * pSett = p->pSett + i;
                //printf( "Closing obj %d with Thread %d:\n", iObj, i );
                clk = Abc_Clock();
                // finalize the results
                Kf_ManSaveResults( pSett->ppCuts, pSett->nCuts, pSett->pCutBest, p->vTemp );
                Vec_IntWriteEntry( &p->vTime, iObj, pSett->pCutBest->Delay + 1 );
                Vec_FltWriteEntry( &p->vArea, iObj, (pSett->pCutBest->Area + 1)/Kf_ObjRefs(p, iObj) );
                if ( pSett->pCutBest->nLeaves > 1 )
                    Kf_ManStoreAddUnit( p->vTemp, iObj, Kf_ObjTime(p, iObj), Kf_ObjArea(p, iObj) );
                Kf_ObjSetCuts( p, iObj, p->vTemp );
                //Gia_CutSetPrint( Kf_ObjCuts(p, iObj) );
                clkUsed += Abc_Clock() - clk;
                // schedule other nodes
                Gia_ObjForEachFanoutStaticId( p->pGia, iObj, iFan, k )
                {
                    if ( !Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFan)) )
                        continue;
                    assert( Vec_IntEntry(vFanins, iFan) > 0 );
                    if ( Vec_IntAddToEntry(vFanins, iFan, -1) == 0 )
                        Vec_IntPush( vStack, iFan );
                    assert( nCountFanins > 0 );
                    nCountFanins--;
                }
                ThData[i].Id = -1;
            }
            if ( Vec_IntSize(vStack) > 0 )
            {
                ThData[i].Id = Vec_IntPop( vStack );
                ThData[i].Status = 1;
                //printf( "Scheduling %d for Thread %d\n", ThData[i].Id, i );
            }
        }
        fRunning = 0;
        for ( i = 0; i < nProcs; i++ )
            if ( ThData[i].Status == 1 || (ThData[i].Status == 0 && ThData[i].Id >= 0) )
                fRunning = 1;
//        printf( "fRunning %d\n", fRunning );
    }
    Vec_IntForEachEntry( vFanins, iFan, k )
        if ( iFan != 0 )
        {
            printf( "%d -> %d    ", k, iFan );
            Gia_ObjPrint( p->pGia, Gia_ManObj(p->pGia, k) );
        }
    assert( Vec_IntSum(vFanins) == 0 );
    // stop the threads
    for ( i = 0; i < nProcs; i++ )
    {
        assert( ThData[i].Status == 0 );
        ThData[i].Id = -1;
        ThData[i].Status = 1;
    }
    Gia_ManStaticFanoutStop( p->pGia );
    Vec_IntFree( vStack );
    Vec_IntFree( vFanins );
    if ( !p->pPars->fVerbose )
        return;
    // print runtime statistics
    printf( "Main     : " );
    Abc_PrintTime( 1, "Time", clkUsed );
    for ( i = 0; i < nProcs; i++ )
    {
        printf( "Thread %d : ", i );
        Abc_PrintTime( 1, "Time", ThData[i].clkUsed );
    }

}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Kf_ManPrintStats( Kf_Man_t * p, char * pTitle )
{
    if ( !p->pPars->fVerbose )
        return;
    printf( "%s :  ", pTitle );
    printf( "Level =%6lu   ", (long)p->pPars->Delay );
    printf( "Area =%9lu   ",  (long)p->pPars->Area );
    printf( "Edge =%9lu   ",  (long)p->pPars->Edge );
    Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
    fflush( stdout );
}
void Kf_ManComputeMapping( Kf_Man_t * p )
{
    Gia_Obj_t * pObj; int i, iPi;
    if ( p->pPars->fVerbose )
    {
        printf( "Aig: CI = %d  CO = %d  AND = %d    ", Gia_ManCiNum(p->pGia), Gia_ManCoNum(p->pGia), Gia_ManAndNum(p->pGia) );
        printf( "LutSize = %d  CutMax = %d  Threads = %d\n", p->pPars->nLutSize, p->pPars->nCutNum, p->pPars->nProcNum );
        printf( "Computing cuts...\r" );
        fflush( stdout );
    }
    Gia_ManForEachCi( p->pGia, pObj, iPi )
    {
        i = Gia_ObjId(p->pGia, pObj);
        Kf_ManStoreStart( p->vTemp, 0 );
        Kf_ManStoreAddUnit( p->vTemp, i, 0, 0 );
        assert( Vec_IntSize(p->vTemp) == 1 + KF_ADD_ON1 + KF_ADD_ON2 );
        Kf_ObjSetCuts( p, i, p->vTemp );
    }
    if ( p->pPars->nProcNum > 0 )
        Kf_ManComputeCuts( p );
    else
    {
        Gia_ManForEachAnd( p->pGia, pObj, i )
        {
            if ( p->pPars->fCutHashing )
                Kf_SetMerge( p->pSett, Kf_ObjCuts0(p, i), Kf_ObjCuts1(p, i), p->pPars->fAreaOnly, p->pPars->fCutMin );
            else if ( p->pPars->fCutSimple )
                Kf_SetMergeSimple( p->pSett, Kf_ObjCuts0(p, i), Kf_ObjCuts1(p, i), p->pPars->fAreaOnly, p->pPars->fCutMin );
            else 
                Kf_SetMergeOrder( p->pSett, Kf_ObjCuts0(p, i), Kf_ObjCuts1(p, i), p->pPars->fAreaOnly, p->pPars->fCutMin );
            Kf_ManSaveResults( p->pSett->ppCuts, p->pSett->nCuts, p->pSett->pCutBest, p->vTemp );
            Vec_IntWriteEntry( &p->vTime, i, p->pSett->pCutBest->Delay + 1 );
            Vec_FltWriteEntry( &p->vArea, i, (p->pSett->pCutBest->Area + 1)/Kf_ObjRefs(p, i) );
            if ( p->pSett->pCutBest->nLeaves > 1 )
                Kf_ManStoreAddUnit( p->vTemp, i, Kf_ObjTime(p, i), Kf_ObjArea(p, i) );
            Kf_ObjSetCuts( p, i, p->vTemp );
            //Gia_CutSetPrint( Kf_ObjCuts(p, i) );
        }
    }
    Kf_ManComputeRefs( p );
    if ( p->pPars->fVerbose )
    {
        printf( "CutPair = %lu  ", (long)p->pSett->CutCount[0] );
        printf( "Merge = %lu  ",   (long)p->pSett->CutCount[1] );
        printf( "Eval = %lu  ",    (long)p->pSett->CutCount[2] );
        printf( "Cut = %lu  ",     (long)p->pSett->CutCount[3] );
        Abc_PrintTime( 1, "Time",  Abc_Clock() - p->clkStart );
        printf( "Memory:  " );
        printf( "Gia = %.2f MB  ", Gia_ManMemory(p->pGia) / (1<<20) );
        printf( "Man = %.2f MB  ", 4.0 * sizeof(int) * Gia_ManObjNum(p->pGia) / (1<<20) );
        printf( "Cuts = %.2f MB  ",Vec_ReportMemory(&p->pMem) / (1<<20) );
        printf( "Set = %.2f KB  ", 1.0 * sizeof(Kf_Set_t) / (1<<10) );
        printf( "\n" );
        fflush( stdout );
        Kf_ManPrintStats( p, "Start" );
    }
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Kf_ManSetInitRefs( Gia_Man_t * p, Vec_Flt_t * vRefs )
{
    Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1; int i;
    Vec_FltFill( vRefs, Gia_ManObjNum(p), 0 );
    Gia_ManForEachAnd( p, pObj, i )
    {
        Vec_FltAddToEntry( vRefs, Gia_ObjFaninId0(pObj, i), 1 );
        Vec_FltAddToEntry( vRefs, Gia_ObjFaninId1(pObj, i), 1 );
        if ( !Gia_ObjIsMuxType(pObj) )
            continue;
        // discount XOR/MUX
        pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
        Vec_FltAddToEntry( vRefs, Gia_ObjId(p, Gia_Regular(pCtrl)), -1 );
        if ( Gia_Regular(pData0) == Gia_Regular(pData1) )
            Vec_FltAddToEntry( vRefs, Gia_ObjId(p, Gia_Regular(pData0)), -1 );
    }
    Gia_ManForEachCo( p, pObj, i )
        Vec_FltAddToEntry( vRefs, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj)), 1 );
    for ( i = 0; i < Gia_ManObjNum(p); i++ )
        Vec_FltUpdateEntry( vRefs, i, 1 );
}
Kf_Man_t * Kf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
{
    Kf_Man_t * p; int i;
    assert( pPars->nLutSize <= KF_LEAF_MAX );
    assert( pPars->nCutNum  <= KF_CUT_MAX  );
    assert( pPars->nProcNum <= KF_PROC_MAX );
    Vec_IntFreeP( &pGia->vMapping );
    p = ABC_CALLOC( Kf_Man_t, 1 );
    p->clkStart  = Abc_Clock();
    p->pGia      = pGia;
    p->pPars     = pPars;
    Vec_SetAlloc_( &p->pMem, 20 );
    Vec_IntFill( &p->vCuts, Gia_ManObjNum(pGia), 0 );
    Vec_IntFill( &p->vTime, Gia_ManObjNum(pGia), 0 );
    Vec_FltFill( &p->vArea, Gia_ManObjNum(pGia), 0 );
    Kf_ManSetInitRefs( pGia, &p->vRefs );
    p->vTemp     = Vec_IntAlloc( 1000 );
    pGia->pRefs  = ABC_CALLOC( int, Gia_ManObjNum(pGia) );
    // prepare cut sets
    for ( i = 0; i < Abc_MaxInt(1, pPars->nProcNum); i++ )
    {
        (p->pSett + i)->pMan      = p;
        (p->pSett + i)->nLutSize  = (unsigned short)pPars->nLutSize;
        (p->pSett + i)->nCutNum   = (unsigned short)pPars->nCutNum;
        (p->pSett + i)->TableMask = (1 << KF_LOG_TABLE) - 1;
    }
    return p;
}
void Kf_ManFree( Kf_Man_t * p )
{
    ABC_FREE( p->pGia->pRefs );
    ABC_FREE( p->vCuts.pArray );
    ABC_FREE( p->vTime.pArray );
    ABC_FREE( p->vArea.pArray );
    ABC_FREE( p->vRefs.pArray );
    Vec_IntFreeP( &p->vTemp );
    Vec_SetFree_( &p->pMem );
    ABC_FREE( p );
}
Gia_Man_t * Kf_ManDerive( Kf_Man_t * p )
{
    Vec_Int_t * vMapping;
    Gia_Obj_t * pObj; 
    int i, k, * pCut;
    assert( !p->pPars->fCutMin );
    vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + (int)p->pPars->Area * 2 );
    Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
    Gia_ManForEachAnd( p->pGia, pObj, i )
    {
        if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
            continue;
        pCut = Kf_ObjCutBest( p, i );
        Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
        Vec_IntPush( vMapping, Kf_CutSize(pCut) );
        for ( k = 1; k <= Kf_CutSize(pCut); k++ )
            Vec_IntPush( vMapping, Kf_CutLeaf(pCut, k) );
        Vec_IntPush( vMapping, i );
    }
    assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
    p->pGia->vMapping = vMapping;
//    Gia_ManMappingVerify( p->pGia );
    return p->pGia;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Kf_ManSetDefaultPars( Jf_Par_t * pPars )
{
    memset( pPars, 0, sizeof(Jf_Par_t) );
    pPars->nLutSize     =  6;
    pPars->nCutNum      =  8;
    pPars->nProcNum     =  0;
    pPars->nRounds      =  1;
    pPars->nVerbLimit   =  5;
    pPars->DelayTarget  = -1;
    pPars->fAreaOnly    =  0;
    pPars->fOptEdge     =  1; 
    pPars->fCoarsen     =  0;
    pPars->fCutMin      =  0;
    pPars->fFuncDsd     =  0;
    pPars->fGenCnf      =  0;
    pPars->fPureAig     =  0;
    pPars->fCutHashing  =  0;
    pPars->fCutSimple   =  0;
    pPars->fVerbose     =  0;
    pPars->fVeryVerbose =  0;
    pPars->nLutSizeMax  =  KF_LEAF_MAX;
    pPars->nCutNumMax   =  KF_CUT_MAX;
    pPars->nProcNumMax  =  KF_PROC_MAX;
}
Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
{
    Kf_Man_t * p;
    Gia_Man_t * pNew;
    p = Kf_ManAlloc( pGia, pPars );
    Kf_ManComputeMapping( p );
    pNew = Kf_ManDerive( p );
    Kf_ManFree( p );
    return pNew;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////

#endif // pthreads are used

ABC_NAMESPACE_IMPL_END