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

  FileName    [exp.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Boolean expression.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

***********************************************************************/
 
#ifndef ABC__map__mio__exp_h
#define ABC__map__mio__exp_h

////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_HEADER_START

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

#define EXP_CONST0 -1
#define EXP_CONST1 -2

static inline Vec_Int_t * Exp_Const0()
{
    Vec_Int_t * vExp;
    vExp = Vec_IntAlloc( 1 );
    Vec_IntPush( vExp, EXP_CONST0 );
    return vExp;
}
static inline Vec_Int_t * Exp_Const1()
{
    Vec_Int_t * vExp;
    vExp = Vec_IntAlloc( 1 );
    Vec_IntPush( vExp, EXP_CONST1 );
    return vExp;
}
static inline int Exp_IsConst( Vec_Int_t * p )
{
    return Vec_IntEntry(p,0) == EXP_CONST0 || Vec_IntEntry(p,0) == EXP_CONST1;
}
static inline int Exp_IsConst0( Vec_Int_t * p )
{
    return Vec_IntEntry(p,0) == EXP_CONST0;
}
static inline int Exp_IsConst1( Vec_Int_t * p )
{
    return Vec_IntEntry(p,0) == EXP_CONST1;
}
static inline Vec_Int_t * Exp_Var( int iVar )
{
    Vec_Int_t * vExp;
    vExp = Vec_IntAlloc( 1 );
    Vec_IntPush( vExp, 2 * iVar );
    return vExp;
}
static inline int Exp_LitShift( int nVars, int Lit, int Shift )
{
    if ( Lit < 2 * nVars )
        return Lit;
    return Lit + 2 * Shift;
}
static inline int Exp_IsLit( Vec_Int_t * p )
{
    return Vec_IntSize(p) == 1 && !Exp_IsConst(p);
}
static inline int Exp_NodeNum( Vec_Int_t * p )
{
    return Vec_IntSize(p)/2;
}
static inline Vec_Int_t * Exp_Not( Vec_Int_t * p )
{
    Vec_IntWriteEntry( p, 0, Vec_IntEntry(p,0) ^ 1 );
    return p;
}
static inline void Exp_PrintLit( int nVars, int Lit )
{
    if ( Lit == EXP_CONST0 )
        Abc_Print( 1, "Const0" );
    else if ( Lit == EXP_CONST1 )
        Abc_Print( 1, "Const1" );
    else if ( Lit < 2 * nVars )
        Abc_Print( 1, "%s%c", (Lit&1) ? "!" : " ", 'a' + Lit/2 );
    else
        Abc_Print( 1, "%s%d", (Lit&1) ? "!" : " ", Lit/2 );
}
static inline void Exp_Print( int nVars, Vec_Int_t * p )
{
    int i;
    for ( i = 0; i < Exp_NodeNum(p); i++ )
    {
        Abc_Print( 1, "%2d = ", nVars + i );
        Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+0) );
        Abc_Print( 1, " & " );
        Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+1) );
        Abc_Print( 1, "\n" );
    }
    Abc_Print( 1, " F = " );
    Exp_PrintLit( nVars, Vec_IntEntryLast(p) );
    Abc_Print( 1, "\n" );
}
static inline Vec_Int_t * Exp_Reverse( Vec_Int_t * p )
{
    Vec_IntReverseOrder( p );
    return p;
}
static inline void Exp_PrintReverse( int nVars, Vec_Int_t * p )
{
    Exp_Reverse( p );
    Exp_Print( nVars, p );
    Exp_Reverse( p );
}
static inline Vec_Int_t * Exp_And( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1, int fCompl0, int fCompl1 )
{
    int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
    Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 1 );
    assert( (Len0 & 1) && (Len1 & 1) );
    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2) );
    Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ fCompl0, Len1/2 ) );
    Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ fCompl1 );
    for ( i = 1; i < Len0; i++ )
        Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
    for ( i = 1; i < Len1; i++ )
        Vec_IntPush( r, Vec_IntEntry(p1, i) );
    assert( Vec_IntSize(r) == Len0 + Len1 + 1 );
    return r;
}
static inline Vec_Int_t * Exp_Or( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
{
    return Exp_Not( Exp_And(pMan, nVars, p0, p1, 1, 1) );
}
static inline Vec_Int_t * Exp_Xor( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
{
    int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
    Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 5 );
    assert( (Len0 & 1) && (Len1 & 1) );
    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 2)     );
    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 1) + 1 );
    Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 0) + 1 );
    Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ 1, Len1/2 ) );
    Vec_IntPush( r, Vec_IntEntry(p1, 0) );
    Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0), Len1/2 ) );
    Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ 1 );
    for ( i = 1; i < Len0; i++ )
        Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
    for ( i = 1; i < Len1; i++ )
        Vec_IntPush( r, Vec_IntEntry(p1, i) );
    assert( Vec_IntSize(r) == Len0 + Len1 + 5 );
    return Exp_Not( r );
}
static inline word Exp_Truth6Lit( int nVars, int Lit, word * puFanins, word * puNodes )
{
    if ( Lit == EXP_CONST0 )
        return 0;
    if ( Lit == EXP_CONST1 )
        return ~(word)0;
    if ( Lit < 2 * nVars )
        return  (Lit&1) ? ~puFanins[Lit/2] : puFanins[Lit/2];
    return (Lit&1) ? ~puNodes[Lit/2-nVars] : puNodes[Lit/2-nVars];
}
static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )
{
    static word Truth6[6] = {
        ABC_CONST(0xAAAAAAAAAAAAAAAA),
        ABC_CONST(0xCCCCCCCCCCCCCCCC),
        ABC_CONST(0xF0F0F0F0F0F0F0F0),
        ABC_CONST(0xFF00FF00FF00FF00),
        ABC_CONST(0xFFFF0000FFFF0000),
        ABC_CONST(0xFFFFFFFF00000000)
    };
    word * puNodes, Res;
    int i;
    if ( puFanins == NULL )
        puFanins = (word *)Truth6;
    puNodes = ABC_CALLOC( word, Exp_NodeNum(p) );
    for ( i = 0; i < Exp_NodeNum(p); i++ )
        puNodes[i] = Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes ) & 
                     Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes );
    Res = Exp_Truth6Lit( nVars, Vec_IntEntryLast(p), puFanins, puNodes );
    ABC_FREE( puNodes );
    return Res;
}
static inline void Exp_Truth8( int nVars, Vec_Int_t * p, word ** puFanins, word * puRes )
{
    word Truth8[8][4] = {
        { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
        { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
        { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
        { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
        { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
        { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
        { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
        { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
    };
    word * puFaninsInt[8], * pStore, * pThis = NULL;
    int i, k, iRoot = Vec_IntEntryLast(p);
    if ( puFanins == NULL )
    {
        puFanins = puFaninsInt;
        for ( k = 0; k < 8; k++ )
            puFanins[k] = Truth8[k];
    }
    if ( Exp_NodeNum(p) == 0 )
    {
        assert( iRoot < 2 * nVars );
        if ( iRoot == EXP_CONST0 || iRoot == EXP_CONST1 )
            for ( k = 0; k < 4; k++ )
                puRes[k] = iRoot == EXP_CONST0 ? 0 : ~(word)0;
        else
            for ( k = 0; k < 4; k++ )
                puRes[k] = Abc_LitIsCompl(iRoot) ? ~puFanins[Abc_Lit2Var(iRoot)][k] : puFanins[Abc_Lit2Var(iRoot)][k];
        return;
    }
    pStore = ABC_CALLOC( word, 4 * Exp_NodeNum(p) );
    for ( i = 0; i < Exp_NodeNum(p); i++ )
    {
        int iVar0 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+0) );
        int iVar1 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+1) );
        int fCompl0 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+0) );
        int fCompl1 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+1) );
        word * pIn0 = iVar0 < nVars ? puFanins[iVar0] : pStore + 4 * (iVar0 - nVars);
        word * pIn1 = iVar1 < nVars ? puFanins[iVar1] : pStore + 4 * (iVar1 - nVars);
        pThis = pStore + 4 * i;
        if ( fCompl0 && fCompl1 )
            for ( k = 0; k < 4; k++ )
                pThis[k] = ~pIn0[k] & ~pIn1[k];
        else if ( fCompl0 && !fCompl1 )
            for ( k = 0; k < 4; k++ )
                pThis[k] = ~pIn0[k] &  pIn1[k];
        else if ( !fCompl0 && fCompl1 )
            for ( k = 0; k < 4; k++ )
                pThis[k] =  pIn0[k] & ~pIn1[k];
        else //if ( !fCompl0 && !fCompl1 )
            for ( k = 0; k < 4; k++ )
                pThis[k] =  pIn0[k] &  pIn1[k];
    }
    assert( Abc_Lit2Var(iRoot) - nVars == i - 1 );
    for ( k = 0; k < 4; k++ )
        puRes[k] = Abc_LitIsCompl(iRoot) ? ~pThis[k] : pThis[k];
    ABC_FREE( pStore );
}
static inline void Exp_TruthLit( int nVars, int Lit, word ** puFanins, word ** puNodes, word * pRes, int nWords )
{
    int w;
    if ( Lit == EXP_CONST0 )
        for ( w = 0; w < nWords; w++ )
            pRes[w] = 0;
    else if ( Lit == EXP_CONST1 )
        for ( w = 0; w < nWords; w++ )
            pRes[w] = ~(word)0;
    else if ( Lit < 2 * nVars )
        for ( w = 0; w < nWords; w++ )
            pRes[w] = (Lit&1) ? ~puFanins[Lit/2][w] : puFanins[Lit/2][w];
    else
        for ( w = 0; w < nWords; w++ )
            pRes[w] = (Lit&1) ? ~puNodes[Lit/2-nVars][w] : puNodes[Lit/2-nVars][w];
}
static inline void Exp_Truth( int nVars, Vec_Int_t * p, word * pRes )
{
    static word Truth6[6] = {
        ABC_CONST(0xAAAAAAAAAAAAAAAA),
        ABC_CONST(0xCCCCCCCCCCCCCCCC),
        ABC_CONST(0xF0F0F0F0F0F0F0F0),
        ABC_CONST(0xFF00FF00FF00FF00),
        ABC_CONST(0xFFFF0000FFFF0000),
        ABC_CONST(0xFFFFFFFF00000000)
    };
    word ** puFanins, ** puNodes, * pTemp0, * pTemp1;
    int i, w, nWords = (nVars <= 6 ? 1 : 1 << (nVars-6));
    // create elementary variables
    puFanins = ABC_ALLOC( word *, nVars );
    for ( i = 0; i < nVars; i++ )
        puFanins[i] = ABC_ALLOC( word, nWords );
    // assign elementary truth tables
    for ( i = 0; i < nVars; i++ )
        if ( i < 6 )
            for ( w = 0; w < nWords; w++ )
                puFanins[i][w] = Truth6[i];
        else
            for ( w = 0; w < nWords; w++ )
                puFanins[i][w] = (w & (1 << (i-6))) ? ~(word)0 : 0;
    // create intermediate nodes
    puNodes = ABC_ALLOC( word *, Exp_NodeNum(p) );
    for ( i = 0; i < Exp_NodeNum(p); i++ )
        puNodes[i] = ABC_ALLOC( word, nWords );
    // evaluate the expression
    pTemp0 = ABC_ALLOC( word, nWords );
    pTemp1 = ABC_ALLOC( word, nWords );
    for ( i = 0; i < Exp_NodeNum(p); i++ )
    {
        Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes, pTemp0, nWords );
        Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes, pTemp1, nWords );
        for ( w = 0; w < nWords; w++ )
            puNodes[i][w] = pTemp0[w] & pTemp1[w];
    }
    ABC_FREE( pTemp0 );
    ABC_FREE( pTemp1 );
    // copy the final result
    Exp_TruthLit( nVars, Vec_IntEntryLast(p), puFanins, puNodes, pRes, nWords );
    // cleanup
    for ( i = 0; i < nVars; i++ )
        ABC_FREE( puFanins[i] );
    ABC_FREE( puFanins );
    for ( i = 0; i < Exp_NodeNum(p); i++ )
        ABC_FREE( puNodes[i] );
    ABC_FREE( puNodes );
}

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

ABC_NAMESPACE_HEADER_END


#endif

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