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

  FileName    [bdcSpfd.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Truth-table-based bi-decomposition engine.]

  Synopsis    [The gateway to bi-decomposition.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - January 30, 2007.]

  Revision    [$Id: bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]

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

#include "bdcInt.h"
#include "aig/aig/aig.h"
#include "misc/extra/extra.h"

ABC_NAMESPACE_IMPL_START


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

typedef struct Bdc_Nod_t_ Bdc_Nod_t;
struct Bdc_Nod_t_
{
    unsigned         iFan0g :  8;
    unsigned         iFan0n : 12;
    unsigned         Type   : 12;  // 0-3 = AND; 4 = XOR

    unsigned         iFan1g :  8;
    unsigned         iFan1n : 12;
    unsigned         Weight : 12;

    word             Truth;
};

static word Truths[6] = {
    ABC_CONST(0xAAAAAAAAAAAAAAAA),
    ABC_CONST(0xCCCCCCCCCCCCCCCC),
    ABC_CONST(0xF0F0F0F0F0F0F0F0),
    ABC_CONST(0xFF00FF00FF00FF00),
    ABC_CONST(0xFFFF0000FFFF0000),
    ABC_CONST(0xFFFFFFFF00000000)
};

static inline int Bdc_CountOnes( word t )
{
    t =    (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
    t =    (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
    t =    (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
    t =    (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
    t =    (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
    return (t & ABC_CONST(0x00000000FFFFFFFF)) +  (t>>32);
}

static inline int Bdc_CountSpfd( word t, word f )
{
    int n00 = Bdc_CountOnes( ~t & ~f );
    int n01 = Bdc_CountOnes(  t & ~f );
    int n10 = Bdc_CountOnes( ~t &  f );
    int n11 = Bdc_CountOnes(  t &  f );
    return n00 * n11 + n10 * n01;
}

static inline word Bdc_Cof6( word t, int iVar, int fCof1 )
{
    assert( iVar >= 0 && iVar < 6 );
    if ( fCof1 )
        return (t & Truths[iVar]) | ((t & Truths[iVar]) >> (1<<iVar));
    else
        return (t &~Truths[iVar]) | ((t &~Truths[iVar]) << (1<<iVar));
}

int Bdc_SpfdAdjCost( word t )
{
    word c0, c1;
    int v, Cost = 0;
    for ( v = 0; v < 6; v++ )
    {
        c0 = Bdc_Cof6( t, v, 0 );
        c1 = Bdc_Cof6( t, v, 1 );
        Cost += Bdc_CountOnes( c0 ^ c1 );
    }
    return Cost;
}


extern void  Abc_Show6VarFunc( word F0, word F1 );

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdPrint_rec( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels )
{
    assert( Level > 0 );
    printf( "(" );

    if ( pNode->Type & 1 )
        printf( "!" );
    if ( pNode->iFan0g == 0 )
        printf( "%c", 'a' + pNode->iFan0n );
    else
    {
        Bdc_Nod_t * pNode0 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan0g);
        Bdc_SpfdPrint_rec( pNode0 + pNode->iFan0n, pNode->iFan0g, vLevels );
    }

    if ( pNode->Type & 4 )
        printf( "+" );
    else
        printf( "*" );

    if ( pNode->Type & 2 )
        printf( "!" );
    if ( pNode->iFan1g == 0 )
        printf( "%c", 'a' + pNode->iFan1n );
    else
    {
        Bdc_Nod_t * pNode1 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan1g);
        Bdc_SpfdPrint_rec( pNode1 + pNode->iFan1n, pNode->iFan1g, vLevels );
    }

    printf( ")" );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdPrint( Bdc_Nod_t * pNode, int Level, Vec_Ptr_t * vLevels, word Truth )
{
    word Diff = Truth ^ pNode->Truth;
    Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( "   " );
    Extra_PrintHex( stdout, (unsigned *)&Diff, 6 );         printf( "   " );
    Bdc_SpfdPrint_rec( pNode, Level, vLevels );
    printf( "    %d\n", pNode->Weight );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdDecompose( word Truth, int nVars, int nCands, int nGatesMax )
{
    int nSize = nCands * nCands * (nGatesMax + 1) * 5;
    Vec_Ptr_t * vLevels;
    Vec_Int_t * vBegs, * vWeight;
    Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2;
    int Count0, Count1, * pPerm;
    int i, j, k, c, n;
    abctime clk;
    assert( nGatesMax < (1<<8) );
    assert( nCands < (1<<12) );
    assert( (1<<(nVars-1))*(1<<(nVars-1)) < (1<<12) ); // max SPFD

    printf( "Storage size = %d (%d * %d * %d * %d).\n", nSize, nCands, nCands, nGatesMax + 1, 5 );

    printf( "SPFD = %d.\n", Bdc_CountOnes(Truth) * Bdc_CountOnes(~Truth) );

    // consider elementary functions
    if ( Truth == 0 || Truth == ~0 )
    {
        printf( "Function is a constant.\n" );
        return;
    }
    for ( i = 0; i < nVars; i++ )
        if ( Truth == Truths[i] || Truth == ~Truths[i] )
        {
            printf( "Function is an elementary variable.\n" );
            return;
        }

    // allocate
    vLevels = Vec_PtrAlloc( 100 );
    vBegs = Vec_IntAlloc( 100 );
    vWeight = Vec_IntAlloc( 100 );

    // initialize elementary variables
    pNode = ABC_CALLOC( Bdc_Nod_t, nVars );
    for ( i = 0; i < nVars; i++ )
        pNode[i].Truth  = Truths[i];
    for ( i = 0; i < nVars; i++ )
        pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
    Vec_PtrPush( vLevels, pNode );
    Vec_IntPush( vBegs, nVars );

    // the next level
clk = Abc_Clock();
    pNode0 = pNode;
    pNode  = ABC_CALLOC( Bdc_Nod_t, 5 * nVars * (nVars - 1) / 2 );
    for ( c = i = 0; i < nVars; i++ )
    for ( j = i+1; j < nVars; j++ )
    {
        pNode[c].Truth =  pNode0[i].Truth &  pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 0;
        pNode[c].Truth = ~pNode0[i].Truth &  pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 1;
        pNode[c].Truth =  pNode0[i].Truth & ~pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 2;
        pNode[c].Truth = ~pNode0[i].Truth & ~pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 3;
        pNode[c].Truth =  pNode0[i].Truth ^  pNode0[j].Truth;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 4;
    }
    assert( c == 5 * nVars * (nVars - 1) / 2 );
    Vec_PtrPush( vLevels, pNode );
    Vec_IntPush( vBegs, c );
    for ( i = 0; i < c; i++ )
    {
        pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
//Bdc_SpfdPrint( pNode + i, 1, vLevels );
        if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
        {
            printf( "Function can be implemented using 1 gate.\n" );
            pNode = NULL;
            goto cleanup;
        }
    }
printf( "Selected %6d gates on level %2d.   ", c, 1 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );


    // iterate through levels
    pNode = ABC_CALLOC( Bdc_Nod_t, nSize );
    for ( n = 2; n <= nGatesMax; n++ )
    {
clk = Abc_Clock();
        c = 0;
        pNode1 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, n-1 );
        Count1 = Vec_IntEntry( vBegs, n-1 );
        // go through previous levels
        for ( k = 0; k < n-1; k++ )
        {
            pNode0 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, k );
            Count0 = Vec_IntEntry( vBegs, k );
            for ( i = 0; i < Count0; i++ )
            for ( j = 0; j < Count1; j++ )
            {
                pNode[c].Truth =  pNode0[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 0;
                pNode[c].Truth = ~pNode0[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 1;
                pNode[c].Truth =  pNode0[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 2;
                pNode[c].Truth = ~pNode0[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 3;
                pNode[c].Truth =  pNode0[i].Truth ^  pNode1[j].Truth;  pNode[c].iFan0g = k; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 4;
            }
            assert( c < nSize );
        }
        // go through current level
        for ( i = 0; i < Count1; i++ )
        for ( j = i+1; j < Count1; j++ )
        {
            pNode[c].Truth =  pNode1[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 0;
            pNode[c].Truth = ~pNode1[i].Truth &  pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 1;
            pNode[c].Truth =  pNode1[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 2;
            pNode[c].Truth = ~pNode1[i].Truth & ~pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 3;
            pNode[c].Truth =  pNode1[i].Truth ^  pNode1[j].Truth;  pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1;  pNode[c].iFan0n = i; pNode[c].iFan1n = j;  pNode[c++].Type = 4;
        }
        assert( c < nSize );
        // sort
        Vec_IntClear( vWeight );
        for ( i = 0; i < c; i++ )
        {
            pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
if ( pNode[i].Weight > 300 )
Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
            Vec_IntPush( vWeight, pNode[i].Weight );

            if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
            {
                printf( "Function can be implemented using %d gates.\n", n );
                Bdc_SpfdPrint( pNode + i, n, vLevels, Truth );
                goto cleanup;
            }
        }
        pPerm = Abc_MergeSortCost( Vec_IntArray(vWeight), c );
        assert( Vec_IntEntry(vWeight, pPerm[0]) <= Vec_IntEntry(vWeight, pPerm[c-1]) );

        printf( "Best SPFD = %d.\n", Vec_IntEntry(vWeight, pPerm[c-1]) );
//        for ( i = 0; i < c; i++ )
//printf( "%d ", Vec_IntEntry(vWeight, pPerm[i]) );

        // choose the best ones
        pNode2 = ABC_CALLOC( Bdc_Nod_t, nCands );
        for ( j = 0, i = c-1; i >= 0; i-- )
        {
            pNode2[j++] = pNode[pPerm[i]];
            if ( j == nCands )
                break;
        }
        ABC_FREE( pPerm );
        Vec_PtrPush( vLevels, pNode2 );
        Vec_IntPush( vBegs, j );

printf( "Selected %6d gates (out of %6d) on level %2d.   ", j, c, n );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

        for ( i = 0; i < 10; i++ )
            Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
    }

cleanup:
    ABC_FREE( pNode );
    Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i )
        ABC_FREE( pNode );
    Vec_PtrFree( vLevels );
    Vec_IntFree( vBegs );
    Vec_IntFree( vWeight );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdDecomposeTest_()
{
    int fTry = 0;
//    word T[17];
//    int i;

//    word Truth    = Truths[0] & ~Truths[3];
//    word Truth    = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]);
//    word Truth    = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5]));
//    word Truth    = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]);
//    word Truth = 0x9ef7a8d9c7193a0f;  // AAFFAAFF0A0F0A0F
//    word Truth = 0x34080226CD163000;
    word Truth = ABC_CONST(0x5052585a0002080a);
    int nVars     =    6;
    int nCands    =  200;// 75;
    int nGatesMax =   20;

    if ( fTry )
    Bdc_SpfdDecompose( Truth, nVars, nCands, nGatesMax );
/*
    for ( i = 0; i < 6; i++ )
        T[i] = Truths[i];
    T[7]  = 0;
    T[8]  = ~T[1]  &  T[3];
    T[9]  = ~T[8]  &  T[0];
    T[10] =  T[1]  &  T[4];
    T[11] =  T[10] &  T[2];
    T[12] =  T[11] &  T[9];
    T[13] = ~T[0]  &  T[5];
    T[14] =  T[2]  &  T[13];
    T[15] = ~T[12] & ~T[14];
    T[16] = ~T[15];
//    if ( T[16] != Truth )
//        printf( "Failed\n" );

    for ( i = 0; i < 17; i++ )
    {
//        printf( "%2d = %3d  ", i, Bdc_CountSpfd(T[i], Truth) );
        printf( "%2d = %3d  ", i, Bdc_CountSpfd(T[i], T[16]) );
        Extra_PrintBinary( stdout, (unsigned *)&T[i], 64 ); printf( "\n" );
    }
//    Extra_PrintBinary( stdout, (unsigned *)&Truth, 64 ); printf( "\n" );
*/
}


typedef struct Bdc_Ent_t_ Bdc_Ent_t; // 24 bytes
struct Bdc_Ent_t_
{
    unsigned         iFan0   : 29;
    unsigned         fCompl0 :  1;
    unsigned         fCompl  :  1;
    unsigned         fMark0  :  1;
    unsigned         iFan1   : 29;
    unsigned         fCompl1 :  1;
    unsigned         fExor   :  1;
    unsigned         fMark1  :  1;
    int              iNext;
    int              iList;
    word             Truth;
};

#define BDC_TERM 0x1FFFFFFF


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bdc_SpfdMark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
{
    if ( pEnt->iFan0 == BDC_TERM )
        return 0;
    if ( pEnt->fMark0 )
        return 0;
    pEnt->fMark0 = 1;
    return pEnt->fMark1 + 
        Bdc_SpfdMark0(p, p + pEnt->iFan0) + 
        Bdc_SpfdMark0(p, p + pEnt->iFan1);
}
int Bdc_SpfdMark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
{
    if ( pEnt->iFan0 == BDC_TERM )
        return 0;
    if ( pEnt->fMark1 )
        return 0;
    pEnt->fMark1 = 1;
    return pEnt->fMark0 + 
        Bdc_SpfdMark1(p, p + pEnt->iFan0) + 
        Bdc_SpfdMark1(p, p + pEnt->iFan1);
}
void Bdc_SpfdUnmark0( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
{
    if ( pEnt->iFan0 == BDC_TERM )
        return;
    pEnt->fMark0 = 0;
    Bdc_SpfdUnmark0( p, p + pEnt->iFan0 );
    Bdc_SpfdUnmark0( p, p + pEnt->iFan1 );
}
void Bdc_SpfdUnmark1( Bdc_Ent_t * p, Bdc_Ent_t * pEnt )
{
    if ( pEnt->iFan0 == BDC_TERM )
        return;
    pEnt->fMark1 = 0;
    Bdc_SpfdUnmark1( p, p + pEnt->iFan0 );
    Bdc_SpfdUnmark1( p, p + pEnt->iFan1 );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bdc_SpfdCheckOverlap( Bdc_Ent_t * p, Bdc_Ent_t * pEnt0, Bdc_Ent_t * pEnt1 )
{
    int RetValue;
    RetValue = Bdc_SpfdMark0( p, pEnt0 );
    assert( RetValue == 0 );
    RetValue = Bdc_SpfdMark1( p, pEnt1 );
    Bdc_SpfdUnmark0( p, pEnt0 );
    Bdc_SpfdUnmark1( p, pEnt1 );
    return RetValue;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bdc_SpfdHashValue( word t, int Size )
{
    // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html
    // 53,
    // 97,
    // 193,
    // 389,
    // 769,
    // 1543,
    // 3079,
    // 6151,
    // 12289,
    // 24593,
    // 49157,
    // 98317,
    // 196613,
    // 393241,
    // 786433,
    // 1572869,
    // 3145739,
    // 6291469,
    // 12582917,
    // 25165843,
    // 50331653,
    // 100663319,
    // 201326611,
    // 402653189,
    // 805306457,
    // 1610612741,
    static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
    unsigned char * s = (unsigned char *)&t;
    unsigned i, Value = 0;
    for ( i = 0; i < 8; i++ )
        Value ^= BigPrimes[i] * s[i];
    return Value % Size;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int * Bdc_SpfdHashLookup( Bdc_Ent_t * p, int Size, word t )
{
    Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size );
    if ( pBin->iList == 0 )
        return &pBin->iList;
    for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext )
    {
        if ( pBin->Truth == t )
            return NULL;
        if ( pBin->iNext == 0 )
            return &pBin->iNext;
    }
    assert( 0 );
    return NULL;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
{
//    int nFuncs = 8000000; // the number of functions to compute
//    int nSize  = 2777111; // the hash table size to use
//    int Limit  = 6;
    
//    int nFuncs = 51000000; // the number of functions to compute
//    int nSize  = 50331653; // the hash table size to use
//    int Limit  = 6;
    
    int nFuncs = 250000000; // the number of functions to compute
    int nSize  = 201326611; // the hash table size to use
    int Limit  = 6;

    int * pPlace, i, n, m, k, s, fCompl;
    abctime clk = Abc_Clock(), clk2;
    Vec_Int_t * vStops;
    Vec_Wrd_t * vTruths;
    Vec_Int_t * vWeights;
    Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1;
    word t0, t1, t;
    assert( nSize <= nFuncs );

    printf( "Allocating %.2f MB of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) );

    p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) );
    memset( p, 255, sizeof(Bdc_Ent_t) );
    p->iList = 0;
    for ( q = p; q < p+nFuncs; q++ )
       q->iList = 0;
    q = p + 1;
    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );

    vTruths  = Vec_WrdStart( nFuncs );
    vWeights = Vec_IntStart( nFuncs );
    Vec_WrdClear( vTruths );
    Vec_IntClear( vWeights );

    // create elementary vars
    vStops = Vec_IntAlloc( 10 );
    Vec_IntPush( vStops, 1 );
    for ( i = 0; i < 6; i++ )
    {
        q->iFan0 = BDC_TERM;
        q->iFan1 = i;
        q->Truth = Truths[i];
        pPlace   = Bdc_SpfdHashLookup( p, nSize, q->Truth );
        *pPlace  = q-p;
        q++;
        Vec_WrdPush( vTruths, Truths[i] );
        Vec_IntPush( vWeights, 0 );
    }
    Vec_IntPush( vStops, 7 );
    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );

    // create gates
    for ( n = 0; n < Limit; n++ )
    {
        // try previous
        for ( k = 0; k < Limit; k++ )
        for ( m = 0; m < Limit; m++ )
        {
            if ( k + m != n || k > m )
                continue;
            // set the start and stop
            pBeg0 = p + Vec_IntEntry( vStops, k );
            pEnd0 = p + Vec_IntEntry( vStops, k+1 );
            // set the start and stop
            pBeg1 = p + Vec_IntEntry( vStops, m );
            pEnd1 = p + Vec_IntEntry( vStops, m+1 );

            clk2 = Abc_Clock();
            printf( "Trying %7d  x %7d.  ", (int)(pEnd0-pBeg0), (int)(pEnd1-pBeg1) );
            for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
            for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
            if ( k < m || pThis1 > pThis0 )
//            if ( n < 5 || Bdc_SpfdCheckOverlap(p, pThis0, pThis1) )
            for ( s = 0; s < 5; s++ )
            {
                t0 = (s&1)      ? ~pThis0->Truth : pThis0->Truth;
                t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
                t  = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
                fCompl = t & 1;
                if ( fCompl )
                    t = ~t;
                if ( t == 0 )
                    continue;
                pPlace = Bdc_SpfdHashLookup( p, nSize, t );
                if ( pPlace == NULL )
                    continue;
                q->iFan0   = pThis0-p;
                q->fCompl0 = s&1;
                q->iFan1   = pThis1-p;
                q->fCompl1 = (s>>1)&1;
                q->fExor   = (s>>2)&1;
                q->Truth   = t;
                q->fCompl  = fCompl;
                *pPlace = q-p;
                q++;
                Vec_WrdPush( vTruths, t );
//                Vec_IntPush( vWeights, n == 5 ? n : n+1 );
                Vec_IntPush( vWeights, n+1 );
                if ( q-p == nFuncs )
                {
                    printf( "Reached limit of %d functions.\n", nFuncs );
                    goto finish;
                }
            }
            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", k, m, n+1, (int)(q-p) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
        }
        Vec_IntPush( vStops, q-p );
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );


    {
        FILE * pFile = fopen( "func6v6n_bin.txt", "wb" );
        fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
        fclose( pFile );
    }
    {
        FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" );
        fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
        fclose( pFile );
    }


finish:
    Vec_IntFree( vStops );
    free( p );

    *pvWeights = vWeights;
//    Vec_WrdFree( vTruths );
    return vTruths;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Wrd_t * Bdc_SpfdReadFiles5( Vec_Int_t ** pvWeights )
{
    Vec_Int_t * vWeights;
    Vec_Wrd_t * vDivs;
    FILE * pFile;
    int RetValue;
    
    vDivs = Vec_WrdStart( 3863759 );
    pFile = fopen( "func6v5n_bin.txt", "rb" );
    RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
    fclose( pFile );

    vWeights = Vec_IntStart( 3863759 );
    pFile = fopen( "func6v5nW_bin.txt", "rb" );
    RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
    fclose( pFile );

    *pvWeights = vWeights;
    return vDivs;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Wrd_t * Bdc_SpfdReadFiles6( Vec_Int_t ** pvWeights )
{
    Vec_Int_t * vWeights;
    Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 );
    FILE * pFile = fopen( "func6v6n_bin.txt", "rb" );
    int RetValue;
    RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
    fclose( pFile );

    vWeights = Vec_IntStart( 12776759 );
    pFile = fopen( "func6v6nW_bin.txt", "rb" );
    RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
    fclose( pFile );

    *pvWeights = vWeights;
    return vDivs;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights )
{
    int Ones = Bdc_CountOnes(f);
    if ( Ones == 0 )
        return -1;
    return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i));
//    return Bdc_CountOnes(f);
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost )
{
    word Func, FuncBest;
    int i, Cost, CostBest = -1, NumBest = -1;
    Vec_WrdForEachEntry( vDivs, Func, i )
    {
        if ( (Func & F0) == 0 )
        {
            Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights);
            if ( CostBest < Cost )
            {
                CostBest = Cost;
                FuncBest = Func;
                NumBest  = i;
            }
        }
        if ( (Func & F1) == 0 )
        {
            Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights);
            if ( CostBest < Cost )
            {
                CostBest = Cost;
                FuncBest = Func;
                NumBest  = i;
            }
        }
        if ( (~Func & F0) == 0 )
        {
            Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights);
            if ( CostBest < Cost )
            {
                CostBest = Cost;
                FuncBest = ~Func;
                NumBest  = i;
            }
        }
        if ( (~Func & F1) == 0 )
        {
            Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights);
            if ( CostBest < Cost )
            {
                CostBest = Cost;
                FuncBest = ~Func;
                NumBest  = i;
            }
        }
    }
    (*pCost) += Vec_IntEntry(vWeights, NumBest);
    assert( CostBest > 0 );
    printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) );
    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
    return FuncBest;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights )
{
    word F1 = t;
    word F0 = ~F1;
    word Func;
    int i, Cost = 0;
    printf( "Trying: " );
    Extra_PrintHex( stdout, (unsigned *)&t, 6 ); printf( "\n" );
//    Abc_Show6VarFunc( F0, F1 );   
    for ( i = 0; F0 && F1; i++ )
    {
        printf( "*** ITER %2d   ", i );
        Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost );
        F0 &= ~Func;
        F1 &= ~Func;
//        Abc_Show6VarFunc( F0, F1 );    
    }
    Cost += (i-1);
    printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) );
    return Cost;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdDecomposeTest44()
{
//    word t = 0x5052585a0002080a;

    word t = ABC_CONST(0x9ef7a8d9c7193a0f);
//    word t = 0x6BFDA276C7193A0F;
//    word t = 0xA3756AFE0B1DF60B;

//    word t = 0xFEF7AEBFCE80AA0F;
//    word t = 0x9EF7FDBFC77F6F0F;
//    word t = 0xDEF7FDFF377F6FFF;

//    word t = 0x345D02736DB390A5; // xor with var 0

//    word t = 0x3EFDA2736D139A0F; // best solution after changes

    Vec_Int_t * vWeights;
    Vec_Wrd_t * vDivs;
    word c0, c1, s, tt, tbest;
    int i, j, Cost, CostBest = 100000;
    abctime clk = Abc_Clock();

    return;

//    printf( "%d\n", RAND_MAX );

    vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
//    vDivs = Bdc_SpfdReadFiles5( &vWeights );

//    Abc_Show6VarFunc( ~t, t );  

    // try function
    tt = t;
    Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
    if ( CostBest > Cost )
    {
        CostBest = Cost;
        tbest = tt;
    }
    printf( "\n" );

    // try complemented output
    for ( i = 0; i < 6; i++ )
    {
        tt = t ^ Truths[i];
        Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
        if ( CostBest > Cost )
        {
            CostBest = Cost;
            tbest = tt;
        }
    }
    printf( "\n" );

    // try complemented input
    for ( i = 0; i < 6; i++ )
    for ( j = 0; j < 6; j++ )
    {
        if ( i == j )
            continue;
        c0 = Bdc_Cof6( t, i, 0 );
        c1 = Bdc_Cof6( t, i, 1 );
        s  = Truths[i] ^ Truths[j];
        tt = (~s & c0) | (s & c1);

        Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
        if ( CostBest > Cost )
        {
            CostBest = Cost;
            tbest = tt;
        }
    }

/*
    for ( i = 0; i < 6; i++ )
    for ( j = 0; j < 6; j++ )
    {
        if ( i == j )
            continue;
        c0 = Bdc_Cof6( t, i, 0 );
        c1 = Bdc_Cof6( t, i, 1 );
        s  = Truths[i] ^ Truths[j];
        tt = (~s & c0) | (s & c1);

        for ( k = 0; k < 6; k++ )
        for ( n = 0; n < 6; n++ )
        {
            if ( k == n )
                continue;
            c0 = Bdc_Cof6( tt, k, 0 );
            c1 = Bdc_Cof6( tt, k, 1 );
            s  = Truths[k] ^ Truths[n];
            ttt= (~s & c0) | (s & c1);

            Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights );
            if ( CostBest > Cost )
            {
                CostBest = Cost;
                tbest = ttt;
            }
        }
    }
*/

    printf( "Best solution found with cost %d.  ", CostBest );
    Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
    Abc_PrintTime( 1, "  Time", Abc_Clock() - clk );

    Vec_WrdFree( vDivs );
    Vec_IntFree( vWeights );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdDecomposeTest3()
{
    int nSizeM = (1 << 26);
    int nSizeK = (1 << 3);
    Vec_Wrd_t * v1M;
    Vec_Wrd_t * v1K;
    int i, k, Counter;
    abctime clk;
//    int EntryM, EntryK;
    Aig_ManRandom64( 1 );

    v1M = Vec_WrdAlloc( nSizeM );
    for ( i = 0; i < nSizeM; i++ )
        Vec_WrdPush( v1M, Aig_ManRandom64(0) );

    v1K = Vec_WrdAlloc( nSizeK );
    for ( i = 0; i < nSizeK; i++ )
        Vec_WrdPush( v1K, Aig_ManRandom64(0) );

    clk = Abc_Clock();
    Counter = 0;
    for ( i = 0; i < nSizeM; i++ )
    for ( k = 0; k < nSizeK; k++ )
        Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
//    Vec_WrdForEachEntry( v1M, EntryM, i )
//    Vec_WrdForEachEntry( v1K, EntryK, k )
//        Counter += ((EntryM & EntryK) == EntryK);

    printf( "Total = %8d.  ", Counter );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

    clk = Abc_Clock();
    Counter = 0;
    for ( k = 0; k < nSizeK; k++ )
    for ( i = 0; i < nSizeM; i++ )
        Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
    printf( "Total = %8d.  ", Counter );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdDecomposeTest8()
{
//    word t = 0x9ef7a8d9c7193a0f;
//    word t = 0x9EF7FDBFC77F6F0F;
    word t = ABC_CONST(0x513B57150819050F);

    Vec_Int_t * vWeights;
    Vec_Wrd_t * vDivs;
    word Func, FuncBest;
    int Cost, CostBest = ABC_INFINITY;
    int i;
    abctime clk = Abc_Clock();

//    return;

    vDivs = Bdc_SpfdReadFiles5( &vWeights );

    printf( "Best init = %4d.  ", Bdc_SpfdAdjCost(t) );
    Extra_PrintHex( stdout, (unsigned *)&t, 6 ); //printf( "\n" );
    Abc_PrintTime( 1, "  Time", Abc_Clock() - clk );

    Vec_WrdForEachEntry( vDivs, Func, i )
    {
        Cost = Bdc_SpfdAdjCost( t ^ Func );
        if ( CostBest > Cost )
        {
            CostBest = Cost;
            FuncBest = Func;
        }
    }

    printf( "Best cost = %4d.  ", CostBest );
    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); //printf( "\n" );
    Abc_PrintTime( 1, "  Time", Abc_Clock() - clk );

Abc_Show6VarFunc( 0, t );
Abc_Show6VarFunc( 0, FuncBest );
Abc_Show6VarFunc( 0, (FuncBest ^ t) );

    FuncBest ^= t;
    Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );

}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bdc_SpfdDecomposeTest()
{
  int nSizeM = (1 << 26);  // big array size
  int nSizeK = (1 << 3);   // small array size
  Vec_Wrd_t * v1M, * v1K;
  int EntryM, EntryK;
  int i, k, Counter;
  abctime clk;

  Aig_ManRandom64( 1 );

  v1M = Vec_WrdAlloc( nSizeM );
  for ( i = 0; i < nSizeM; i++ )
      Vec_WrdPush( v1M, Aig_ManRandom64(0) );

  v1K = Vec_WrdAlloc( nSizeK );
  for ( i = 0; i < nSizeK; i++ )
      Vec_WrdPush( v1K, Aig_ManRandom64(0) );

  clk = Abc_Clock();
  Counter = 0;
//  for ( i = 0; i < nSizeM; i++ )
//  for ( k = 0; k < nSizeK; k++ )
//      Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
  Vec_WrdForEachEntry( v1M, EntryM, i )
  Vec_WrdForEachEntry( v1K, EntryK, k )
      Counter += ((EntryM & EntryK) == EntryK);
  printf( "Total = %8d.  ", Counter );
  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );

  clk = Abc_Clock();
  Counter = 0;
//  for ( k = 0; k < nSizeK; k++ )
//  for ( i = 0; i < nSizeM; i++ )
//      Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
  Vec_WrdForEachEntry( v1K, EntryK, k )
  Vec_WrdForEachEntry( v1M, EntryM, i )
      Counter += ((EntryM & EntryK) == EntryK);
  printf( "Total = %8d.  ", Counter );
  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}


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


ABC_NAMESPACE_IMPL_END