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

  FileName    [giaEsop.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [ESOP computation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"
#include "misc/extra/extra.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"

ABC_NAMESPACE_IMPL_START


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

typedef struct Eso_Man_t_ Eso_Man_t;
struct Eso_Man_t_
{
    Gia_Man_t *     pGia;     // user's AIG
    int             nVars;    // number of variables
    int             Cube1;    // ID of const1 cube
    Vec_Wec_t *     vEsops;   // ESOP for each node
    Hsh_VecMan_t *  pHash;    // hash table for cubes
    Vec_Wec_t *     vCubes;   // cover during minimization
    // internal
    Vec_Int_t *     vCube1;   // first cube
    Vec_Int_t *     vCube2;   // second cube
    Vec_Int_t *     vCube;    // resulting cube
};

static inline Vec_Int_t * Eso_ManCube( Eso_Man_t * p, int iCube ) { assert( iCube >= 0 ); return Hsh_VecReadEntry(p->pHash, iCube); }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
    
/**Function*************************************************************

  Synopsis    [Computation manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Eso_Man_t * Eso_ManAlloc( Gia_Man_t * pGia )
{
    int i, n, Id;
    Eso_Man_t * p = ABC_CALLOC( Eso_Man_t, 1 );
    p->pGia   = pGia;
    p->nVars  = Gia_ManCiNum(pGia);
    p->Cube1  = ABC_INFINITY;
    p->vEsops = Vec_WecStart( Gia_ManObjNum(pGia) );
    p->pHash  = Hsh_VecManStart( 1000 );
    p->vCubes = Vec_WecStart(Gia_ManCiNum(pGia)+1);
    p->vCube1 = Vec_IntAlloc(Gia_ManCiNum(pGia));
    p->vCube2 = Vec_IntAlloc(Gia_ManCiNum(pGia));
    p->vCube  = Vec_IntAlloc(Gia_ManCiNum(pGia));
    Gia_ManForEachCiId( pGia, Id, i )
    {
        for ( n = 0; n < 2; n++ )
        {
            Vec_IntFill( p->vCube, 1, Abc_Var2Lit(i, n) );
            Hsh_VecManAdd( p->pHash, p->vCube );
        }
        Vec_IntPush( Vec_WecEntry(p->vEsops, Id), Abc_Var2Lit(i, 0) );
    }
    return p;
}
void Eso_ManStop( Eso_Man_t * p )
{
    Vec_WecFree( p->vEsops );
    Hsh_VecManStop( p->pHash );
    Vec_WecFree( p->vCubes );
    Vec_IntFree( p->vCube1 );
    Vec_IntFree( p->vCube2 );
    Vec_IntFree( p->vCube );
    ABC_FREE( p );
}
    

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

  Synopsis    [Printing/transforming the cover.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Eso_ManCoverPrint( Eso_Man_t * p, Vec_Int_t * vEsop )
{
    Vec_Str_t * vStr;
    Vec_Int_t * vCube;
    int i, k, Lit, Cube;
    if ( Vec_IntSize(vEsop) == 0 )
    {
        printf( "Const 0\n" );
        return;
    }
    vStr = Vec_StrAlloc( p->nVars + 4 );
    Vec_StrFill( vStr, p->nVars, '-' );
    Vec_StrPush( vStr, ' ' );
    Vec_StrPush( vStr, '1' );
    Vec_StrPush( vStr, '\n' );
    Vec_StrPush( vStr, '\0' );
    assert( Vec_IntSize(vEsop) > 0 );
    Vec_IntForEachEntry( vEsop, Cube, i )
    {
        if ( Cube == p->Cube1 )
            printf( "%s", Vec_StrArray(vStr) );
        else 
        {
            vCube = Eso_ManCube( p, Cube );
            Vec_IntForEachEntry( vCube, Lit, k )
                Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit)?'0':'1') );
            printf( "%s", Vec_StrArray(vStr) );
            Vec_IntForEachEntry( vCube, Lit, k )
                Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), '-' );
        }
    }
    printf( "\n" );
    Vec_StrFree( vStr );
}
Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover )
{
    Vec_Wec_t * vRes;
    Vec_Int_t * vEsop, * vLevel;  int i;
    vRes = Vec_WecAlloc( Vec_VecSizeSize((Vec_Vec_t *)vCover) );
    Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i )
    {
        if ( Vec_IntSize(vEsop) > 0 )
        {
            int c, Cube;
            Vec_IntForEachEntry( vEsop, Cube, c )
            {
                vLevel = Vec_WecPushLevel( vRes );
                if ( Cube != p->Cube1 )
                {
                    int k, Lit;
                    Vec_Int_t * vCube = Eso_ManCube( p, Cube );
                    Vec_IntForEachEntry( vCube, Lit, k )
                        Vec_IntPush( vLevel, Lit );
                }
                Vec_IntPush( vLevel, -i-1 );
            }
        }
    }
    //assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) );
    return vRes;
}
Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover )
{
    Vec_Int_t * vEsop;
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj;  int i;
    pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
    pNew->pName = Abc_UtilStrsav( p->pGia->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
    Gia_ManHashAlloc( pNew );
    Gia_ManConst0(p->pGia)->Value = 0;
    Gia_ManForEachCi( p->pGia, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i )
    {
        if ( Vec_IntSize(vEsop) > 0 )
        {
            int c, Cube, iRoot = 0;
            Vec_IntForEachEntry( vEsop, Cube, c )
            {
                int k, Lit, iAnd = 1;
                if ( Cube != p->Cube1 )
                {
                    Vec_Int_t * vCube = Eso_ManCube( p, Cube );
                    Vec_IntForEachEntry( vCube, Lit, k )
                        iAnd = Gia_ManHashAnd( pNew, iAnd, Lit + 2 );
                }
                iRoot = Gia_ManHashXor( pNew, iRoot, iAnd );
            }
            Gia_ManAppendCo( pNew, iRoot );
        }
        else
            Gia_ManAppendCo( pNew, 0 );
    }
    // cleanup
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

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

  Synopsis    [Minimization.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Eso_ManFindDistOneLitEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 and pCube2 both have nLits
{
    int i, iDiff = -1;
    for ( i = 0; i < nLits; i++ )
        if ( pCube1[i] != pCube2[i] )
        {
            if ( iDiff != -1 )
                return -1;
            if ( Abc_Lit2Var(pCube1[i]) != Abc_Lit2Var(pCube2[i]) )
                return -1;
            iDiff = i;
        }
    return iDiff;
}
int Eso_ManFindDistOneLitNotEqual( int * pCube1, int * pCube2, int nLits ) // pCube1 has nLits; pCube2 has nLits + 1
{
    int i, k, iDiff = -1;
    for ( i = k = 0; i < nLits; i++, k++ )
        if ( pCube1[i] != pCube2[k] )
        {
            if ( iDiff != -1 )
                return -1;
            iDiff = i;
            i--;
        }
    if ( iDiff == -1 )
        iDiff = nLits;
    return iDiff;
}
void Eso_ManMinimizeAdd( Eso_Man_t * p, int Cube )
{
    int fMimimize = 1;
    Vec_Int_t * vCube      = (Cube == p->Cube1) ? NULL : Eso_ManCube(p, Cube); 
    int * pCube2, * pCube  = (Cube == p->Cube1) ? NULL : Vec_IntArray(vCube); 
    int Cube2, nLits       = (Cube == p->Cube1) ? 0 : Vec_IntSize(vCube);
    Vec_Int_t * vLevel     = Vec_WecEntry( p->vCubes, nLits );
    int c, k, iLit, iPlace = Vec_IntFind( vLevel, Cube );
    if ( iPlace >= 0 ) // identical found
    {
        Vec_IntDrop( vLevel, iPlace );
        return;
    }
    if ( Cube == p->Cube1 ) // simple case
    {
        assert( Vec_IntSize(vLevel) == 0 );
        Vec_IntPush( vLevel, Cube );
        return;
    }
    // look for distance-1 in next bin
    if ( fMimimize && nLits < p->nVars - 1 )
    {
        Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits+1 );
        Vec_IntForEachEntry( vLevel, Cube2, c )
        {
            pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
            iLit = Eso_ManFindDistOneLitNotEqual( pCube, pCube2, nLits );
            if ( iLit == -1 )
                continue;
            // remove this cube
            Vec_IntDrop( vLevel, c );
            // create new cube
            Vec_IntClear( p->vCube );
            for ( k = 0; k <= nLits; k++ )
                Vec_IntPush( p->vCube, Abc_LitNotCond(pCube2[k], k == iLit) );
            Cube = Hsh_VecManAdd( p->pHash, p->vCube );
            // try to add new cube
            Eso_ManMinimizeAdd( p, Cube );
            return;
        }
    }
    // look for distance-1 in the same bin
    if ( fMimimize )
    {
        Vec_IntForEachEntry( vLevel, Cube2, c )
        {
            pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
            iLit = Eso_ManFindDistOneLitEqual( pCube2, pCube, nLits );
            if ( iLit == -1 )
                continue;
            // remove this cube
            Vec_IntDrop( vLevel, c );
            // create new cube
            Vec_IntClear( p->vCube );
            for ( k = 0; k < nLits; k++ )
                if ( k != iLit )
                    Vec_IntPush( p->vCube, pCube[k] );
            if ( Vec_IntSize(p->vCube) == 0 )
                Cube = p->Cube1;
            else
                Cube = Hsh_VecManAdd( p->pHash, p->vCube );
            // try to add new cube
            Eso_ManMinimizeAdd( p, Cube );
            return;
        }
    }
    assert( nLits > 0 );
    if ( fMimimize && nLits > 0 )
    {
        // look for distance-1 in the previous bin
        Vec_Int_t * vLevel = Vec_WecEntry( p->vCubes, nLits-1 );
        // check for the case of one-literal cube
        if ( nLits == 1 && Vec_IntSize(vLevel) == 1 )
        {
            Vec_IntDrop( vLevel, 0 );
            Cube = Abc_LitNot( Cube );
        }
        else
        Vec_IntForEachEntry( vLevel, Cube2, c )
        {
            pCube2 = Hsh_VecReadArray( p->pHash, Cube2 ); 
            iLit = Eso_ManFindDistOneLitNotEqual( pCube2, pCube, nLits-1 );
            if ( iLit == -1 )
                continue;
            // remove this cube
            Vec_IntDrop( vLevel, c );
            // create new cube
            Vec_IntClear( p->vCube );
            for ( k = 0; k < nLits; k++ )
                Vec_IntPush( p->vCube, Abc_LitNotCond(pCube[k], k == iLit) );
            Cube = Hsh_VecManAdd( p->pHash, p->vCube );
            // try to add new cube
            Eso_ManMinimizeAdd( p, Cube );
            return;
        }
    }
    // could not find - simply add this cube
    Vec_IntPush( vLevel, Cube );
}

void Eso_ManMinimizeCopy( Eso_Man_t * p, Vec_Int_t * vEsop )
{
    Vec_Int_t * vLevel;
    int i;
    Vec_IntClear( vEsop );
    Vec_WecForEachLevel( p->vCubes, vLevel, i )
    {
        Vec_IntAppend( vEsop, vLevel );
        if ( i > 0 )
        {
            int k, Cube;
            Vec_IntForEachEntry( vLevel, Cube, k )
                assert( Vec_IntSize(Eso_ManCube(p, Cube)) == i );
        }
        Vec_IntClear( vLevel );
    }
}

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

  Synopsis    [Compute the produce of two covers.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Eso_ManComputeAnd( Eso_Man_t * p, Vec_Int_t * vCube1, Vec_Int_t * vCube2, Vec_Int_t * vCube )
{
    int * pBeg  = vCube->pArray;
    int * pBeg1 = vCube1->pArray;
    int * pBeg2 = vCube2->pArray;
    int * pEnd1 = vCube1->pArray + vCube1->nSize;
    int * pEnd2 = vCube2->pArray + vCube2->nSize;
    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
    {
        if ( *pBeg1 == *pBeg2 )
            *pBeg++ = *pBeg1++, pBeg2++;
        else if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) )
            return -1;
        else if ( *pBeg1 < *pBeg2 )
            *pBeg++ = *pBeg1++;
        else 
            *pBeg++ = *pBeg2++;
    }
    while ( pBeg1 < pEnd1 )
        *pBeg++ = *pBeg1++;
    while ( pBeg2 < pEnd2 )
        *pBeg++ = *pBeg2++;
    vCube->nSize = pBeg - vCube->pArray;
    assert( vCube->nSize <= vCube->nCap );
    assert( vCube->nSize >= vCube1->nSize );
    assert( vCube->nSize >= vCube2->nSize );
    return Hsh_VecManAdd( p->pHash, vCube );
}
void Eso_ManComputeOne( Eso_Man_t * p, Vec_Int_t * vEsop1, Vec_Int_t * vEsop2, Vec_Int_t * vEsop )
{
    Vec_Int_t vCube1, vCube2;
    int i, k, Cube1, Cube2, Cube;
    Vec_IntClear( vEsop );
    if ( Vec_IntSize(vEsop1) == 0 || Vec_IntSize(vEsop2) == 0 )
        return;
    Cube1 = Vec_IntEntry(vEsop1, 0);
    Cube2 = Vec_IntEntry(vEsop2, 0);
    Vec_IntForEachEntry( vEsop1, Cube1, i )
    {
        if ( Cube1 == p->Cube1 )
        {
            Vec_IntForEachEntry( vEsop2, Cube2, k )
                Eso_ManMinimizeAdd( p, Cube2 );
            continue;
        }
        Vec_IntForEachEntry( vEsop2, Cube2, k )
        {
            if ( Cube2 == p->Cube1 )
            {
                Eso_ManMinimizeAdd( p, Cube1 );
                continue;
            }
            vCube1 = *Hsh_VecReadEntry( p->pHash, Cube1 );
            vCube2 = *Hsh_VecReadEntry( p->pHash, Cube2 );
            Cube = Eso_ManComputeAnd( p, &vCube1, &vCube2, p->vCube );
            if ( Cube >= 0 )
                Eso_ManMinimizeAdd( p, Cube );
        }
    }
    Eso_ManMinimizeCopy( p, vEsop );
}

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

  Synopsis    [Complements the cover if needed, or just copy it.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Eso_ManTransformOne( Eso_Man_t * p, Vec_Int_t * vEsop, int fCompl, Vec_Int_t * vRes )
{
    int i, Cube, Start = 0;
    Vec_IntClear( vRes );
    if ( fCompl )
    {
        if ( Vec_IntSize(vEsop) == 0 )
            Vec_IntPush( vRes, p->Cube1 );
        else
        {
            Cube = Vec_IntEntry(vEsop, 0);
            if ( Cube == p->Cube1 )
                Start = 1;
            else if ( Cube < 2 * p->nVars )
                Vec_IntPush( vRes, Abc_LitNot(Cube) ), Start = 1;
            else
                Vec_IntPush( vRes, p->Cube1 );
        }
    }
    Vec_IntForEachEntryStart( vEsop, Cube, i, Start )
        Vec_IntPush( vRes, Cube );
    return vRes;
}

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

  Synopsis    [Computes ESOP from AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes )
{
    abctime clk = Abc_Clock();
    Vec_Ptr_t * vCover;
    Gia_Man_t * pNew = NULL;
    Gia_Obj_t * pObj; 
    int i, nCubes = 0, nCubesUsed = 0;
    Vec_Int_t * vEsop1, * vEsop2, * vEsop;
    Eso_Man_t * p = Eso_ManAlloc( pGia ); 
    Gia_ManForEachAnd( pGia, pObj, i )
    {
        vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0(pObj, i) );
        vEsop2 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId1(pObj, i) );
        vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
        vEsop2 = Eso_ManTransformOne( p, vEsop2, Gia_ObjFaninC1(pObj), p->vCube2 );
        vEsop  = Vec_WecEntry( p->vEsops, i );
        Eso_ManComputeOne( p, vEsop1, vEsop2, vEsop );
        nCubes += Vec_IntSize(vEsop);
    }
    vCover = Vec_PtrAlloc( Gia_ManCoNum(pGia) );
    Gia_ManForEachCo( pGia, pObj, i )
    {
        vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0p(pGia, pObj) );
        vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
        if ( fVerbose )
            printf( "Output %3d:  ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) );
//        if ( fVerbose )
//            Eso_ManCoverPrint( p, vEsop1 );
        Vec_PtrPush( vCover, Vec_IntDup(vEsop1) );
        nCubesUsed += Vec_IntSize(vEsop1);
    }
    if ( fVerbose )
    {
        printf( "Outs = %d.  Cubes = %d.  Used = %d.  Hashed = %d. ", 
            Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    if ( pvRes )
        *pvRes = Eso_ManCoverDerive( p, vCover );
    else
        pNew = Eso_ManCoverConvert( p, vCover );
    Vec_VecFree( (Vec_Vec_t *)vCover );
    Eso_ManStop( p );
    return pNew;
}

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


ABC_NAMESPACE_IMPL_END