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

  FileName    [giaEra.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Explicit reachability analysis.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"
#include "src/misc/mem/mem.h"

ABC_NAMESPACE_IMPL_START


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

// explicit state representation
typedef struct Gia_ObjEra_t_ Gia_ObjEra_t;
struct Gia_ObjEra_t_
{
    int            Num;          // ID of this state
    int            Cond;         // input condition
    int            iPrev;        // previous state
    int            iNext;        // next state in the hash table
    unsigned       pData[0];     // state bits
};

// explicit state reachability
typedef struct Gia_ManEra_t_ Gia_ManEra_t;
struct Gia_ManEra_t_
{
    Gia_Man_t *    pAig;         // user's AIG manager
    int            nWordsSim;       // 2^(PInum)
    int            nWordsDat;   // Abc_BitWordNum
    unsigned *     pDataSim;     // simulation data
    Mem_Fixed_t *  pMemory;      // memory manager
    Vec_Ptr_t *    vStates;      // reached states
    Gia_ObjEra_t * pStateNew;    // temporary state
    int            iCurState;    // the current state
    Vec_Int_t *    vBugTrace;    // the sequence of transitions
    // hash table for states
    int            nBins;         
    unsigned *     pBins;
};

static inline unsigned *     Gia_ManEraData( Gia_ManEra_t * p, int i )    { return p->pDataSim + i * p->nWordsSim;  }
static inline Gia_ObjEra_t * Gia_ManEraState( Gia_ManEra_t * p, int i )   { return (Gia_ObjEra_t *)Vec_PtrEntry(p->vStates, i);  }

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

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

  Synopsis    [Creates reachability manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig )
{
    Vec_Ptr_t * vTruths;
    Gia_ManEra_t * p;
    unsigned * pTruth, * pSimInfo;
    int i;
    p = ABC_CALLOC( Gia_ManEra_t, 1 );
    p->pAig      = pAig;
    p->nWordsSim = Abc_TruthWordNum( Gia_ManPiNum(pAig) );
    p->nWordsDat = Abc_BitWordNum( Gia_ManRegNum(pAig) );
    p->pDataSim  = ABC_ALLOC( unsigned, p->nWordsSim*Gia_ManObjNum(pAig) );
    p->pMemory   = Mem_FixedStart( sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat );
    p->vStates   = Vec_PtrAlloc( 100000 );
    p->nBins     = Abc_PrimeCudd( 100000 );
    p->pBins     = ABC_CALLOC( unsigned, p->nBins );
    Vec_PtrPush( p->vStates, NULL );
    // assign primary input values
    vTruths = Vec_PtrAllocTruthTables( Gia_ManPiNum(pAig) );
    Vec_PtrForEachEntry( unsigned *, vTruths, pTruth, i )
    {
        pSimInfo = Gia_ManEraData( p, Gia_ObjId(pAig, Gia_ManPi(pAig, i)) );
        memcpy( pSimInfo, pTruth, sizeof(unsigned) * p->nWordsSim );
    }
    Vec_PtrFree( vTruths );
    // assign constant zero node
    pSimInfo = Gia_ManEraData( p, 0 );
    memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim );
    return p;
}

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

  Synopsis    [Deletes reachability manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManEraFree( Gia_ManEra_t * p )
{
    Mem_FixedStop( p->pMemory, 0 );
    Vec_PtrFree( p->vStates );
    if ( p->vBugTrace ) Vec_IntFree( p->vBugTrace );
    ABC_FREE( p->pDataSim );
    ABC_FREE( p->pBins );
    ABC_FREE( p );
}

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

  Synopsis    [Creates new state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_ObjEra_t * Gia_ManEraCreateState( Gia_ManEra_t * p )
{
    Gia_ObjEra_t * pNew;
    pNew = (Gia_ObjEra_t *)Mem_FixedEntryFetch( p->pMemory );
    pNew->Num = Vec_PtrSize( p->vStates );
    pNew->iPrev = 0;
    Vec_PtrPush( p->vStates, pNew );
    return pNew;
}


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

  Synopsis    [Computes hash value of the node using its simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManEraStateHash( unsigned * pState, int nWordsSim, int nTableSize )
{
    static int s_FPrimes[128] = { 
        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
    };
    unsigned uHash;
    int i;
    uHash = 0;
    for ( i = 0; i < nWordsSim; i++ )
        uHash ^= pState[i] * s_FPrimes[i & 0x7F];
    return uHash % nTableSize;
}

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

  Synopsis    [Returns the place of this state in the table or NULL if it exists.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline unsigned * Gia_ManEraHashFind( Gia_ManEra_t * p, Gia_ObjEra_t * pState )
{
    Gia_ObjEra_t * pThis;
    unsigned * pPlace = p->pBins + Gia_ManEraStateHash( pState->pData, p->nWordsDat, p->nBins );
    for ( pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL; pThis; 
          pPlace = (unsigned *)&pThis->iNext, pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL )
              if ( !memcmp( pState->pData, pThis->pData, sizeof(unsigned) * p->nWordsDat ) )
                  return NULL;
    return pPlace;
}

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

  Synopsis    [Resizes the hash table.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManEraHashResize( Gia_ManEra_t * p )
{
    Gia_ObjEra_t * pThis;
    unsigned * pBinsOld, * piPlace;
    int nBinsOld, iNext, Counter, i;
    assert( p->pBins != NULL );
    // replace the table
    pBinsOld = p->pBins;
    nBinsOld = p->nBins;
    p->nBins = Abc_PrimeCudd( 3 * p->nBins ); 
    p->pBins = ABC_CALLOC( unsigned, p->nBins );
    // rehash the entries from the old table
    Counter = 0;
    for ( i = 0; i < nBinsOld; i++ )
    for ( pThis = (pBinsOld[i]? Gia_ManEraState(p, pBinsOld[i]) : NULL),
          iNext = (pThis? pThis->iNext : 0);  
          pThis;  pThis = (iNext? Gia_ManEraState(p, iNext) : NULL),   
          iNext = (pThis? pThis->iNext : 0)  )
    {
        assert( pThis->Num );
        pThis->iNext = 0;
        piPlace = Gia_ManEraHashFind( p, pThis );
        assert( *piPlace == 0 ); // should not be there
        *piPlace = pThis->Num;
        Counter++;
    }
    assert( Counter == Vec_PtrSize( p->vStates ) - 1 );
    ABC_FREE( pBinsOld );
}

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

  Synopsis    [Initialize register output to the given state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManInsertState( Gia_ManEra_t * p, Gia_ObjEra_t * pState )
{
    Gia_Obj_t * pObj;
    unsigned * pSimInfo;
    int i;
    Gia_ManForEachRo( p->pAig, pObj, i )
    {
        pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
        if ( Abc_InfoHasBit(pState->pData, i) )
            memset( pSimInfo, 0xff, sizeof(unsigned) * p->nWordsSim );
        else
            memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim );
    }
}

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

  Synopsis    [Returns -1 if outputs are not asserted.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Gia_ManOutputAsserted( Gia_ManEra_t * p, Gia_Obj_t * pObj )
{
    unsigned * pInfo  = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
    int w;
    for ( w = 0; w < p->nWordsSim; w++ )
        if ( pInfo[w] )
            return 32*w + Gia_WordFindFirstBit( pInfo[w] );
    return -1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Gia_ManSimulateCo( Gia_ManEra_t * p, Gia_Obj_t * pObj )
{
    int Id = Gia_ObjId(p->pAig, pObj);
    unsigned * pInfo  = Gia_ManEraData( p, Id );
    unsigned * pInfo0 = Gia_ManEraData( p, Gia_ObjFaninId0(pObj, Id) );
    int w;
    if ( Gia_ObjFaninC0(pObj) )
        for ( w = p->nWordsSim-1; w >= 0; w-- )
            pInfo[w] = ~pInfo0[w];
    else 
        for ( w = p->nWordsSim-1; w >= 0; w-- )
            pInfo[w] = pInfo0[w];
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Gia_ManSimulateNode( Gia_ManEra_t * p, Gia_Obj_t * pObj )
{
    int Id = Gia_ObjId(p->pAig, pObj);
    unsigned * pInfo  = Gia_ManEraData( p, Id );
    unsigned * pInfo0 = Gia_ManEraData( p, Gia_ObjFaninId0(pObj, Id) );
    unsigned * pInfo1 = Gia_ManEraData( p, Gia_ObjFaninId1(pObj, Id) );
    int w;
    if ( Gia_ObjFaninC0(pObj) )
    {
        if (  Gia_ObjFaninC1(pObj) )
            for ( w = p->nWordsSim-1; w >= 0; w-- )
                pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
        else 
            for ( w = p->nWordsSim-1; w >= 0; w-- )
                pInfo[w] = ~pInfo0[w] & pInfo1[w];
    }
    else 
    {
        if (  Gia_ObjFaninC1(pObj) )
            for ( w = p->nWordsSim-1; w >= 0; w-- )
                pInfo[w] = pInfo0[w] & ~pInfo1[w];
        else 
            for ( w = p->nWordsSim-1; w >= 0; w-- )
                pInfo[w] = pInfo0[w] & pInfo1[w];
    }
}

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

  Synopsis    [Performs one iteration of reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManPerformOneIter( Gia_ManEra_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            Gia_ManSimulateNode( p, pObj );
        else if ( Gia_ObjIsCo(pObj) )
            Gia_ManSimulateCo( p, pObj );
    }
}

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

  Synopsis    [Performs one iteration of reachability analysis.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_ManCollectBugTrace( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int iCond )
{
    Vec_Int_t * vTrace;
    vTrace = Vec_IntAlloc( 10 );
    Vec_IntPush( vTrace, iCond );
    for ( ; pState; pState = pState->iPrev ? Gia_ManEraState(p, pState->iPrev) : NULL )
        Vec_IntPush( vTrace, pState->Cond );
    Vec_IntReverseOrder( vTrace );
    return vTrace;
}

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

  Synopsis    [Counts the depth of state transitions leading ot this state.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCountDepth( Gia_ManEra_t * p )
{
    Gia_ObjEra_t * pState;
    int Counter = 0;
    pState = (Gia_ObjEra_t *)Vec_PtrEntryLast( p->vStates );
    if ( pState->iPrev == 0 && Vec_PtrSize(p->vStates) > 3 )
        pState = (Gia_ObjEra_t *)Vec_PtrEntry( p->vStates, Vec_PtrSize(p->vStates) - 2 );
    for ( ; pState; pState = pState->iPrev ? Gia_ManEraState(p, pState->iPrev) : NULL )
        Counter++;
    return Counter;
}

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

  Synopsis    [Analized reached states.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter )
{
    Gia_Obj_t * pObj;
    unsigned * pSimInfo, * piPlace;
    int i, k, iCond, nMints;
    // check if the miter is asserted
    if ( fMiter )
    {
        Gia_ManForEachPo( p->pAig, pObj, i )
        {
            iCond = Gia_ManOutputAsserted( p, pObj );
            if ( iCond >= 0 )
            {
                p->vBugTrace = Gia_ManCollectBugTrace( p, pState, iCond );
                return 1;
            }
        }
    }
    // collect reached states 
    nMints = (1 << Gia_ManPiNum(p->pAig));
    for ( k = 0; k < nMints; k++ )
    {
        if ( p->pStateNew == NULL )
            p->pStateNew = Gia_ManEraCreateState( p );
        p->pStateNew->pData[p->nWordsDat-1] = 0;
        Gia_ManForEachRi( p->pAig, pObj, i )
        {
            pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
            if ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) )
                Abc_InfoXorBit( p->pStateNew->pData, i );
        }
        piPlace = Gia_ManEraHashFind( p, p->pStateNew );
        if ( piPlace == NULL )
            continue;
//printf( "Inserting %d ", Vec_PtrSize(p->vStates) );
//Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) );  printf( "\n" );
        assert( *piPlace == 0 );
        *piPlace = p->pStateNew->Num;
        p->pStateNew->Cond = k;
        p->pStateNew->iPrev = pState->Num;
        p->pStateNew->iNext = 0;
        p->pStateNew = NULL;
        // expand hash table if needed
        if ( Vec_PtrSize(p->vStates) > 2 * p->nBins )
            Gia_ManEraHashResize( p );
    }
    return 0;
}

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

  Synopsis    [Resizes the hash table.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose )
{ 
    Gia_ManEra_t * p;
    Gia_ObjEra_t * pState;
    int Hash;
    clock_t clk = clock();
    int RetValue = 1;
    assert( Gia_ManPiNum(pAig) <= 12 );
    assert( Gia_ManRegNum(pAig) > 0 );
    p = Gia_ManEraCreate( pAig );
    // create init state
    pState = Gia_ManEraCreateState( p );
    pState->Cond  = 0; 
    pState->iPrev = 0;
    pState->iNext = 0; 
    memset( pState->pData, 0, sizeof(unsigned) * p->nWordsDat );
    Hash = Gia_ManEraStateHash(pState->pData, p->nWordsDat, p->nBins);
    p->pBins[ Hash ] = pState->Num;
    // process reachable states
    while ( p->iCurState < Vec_PtrSize( p->vStates ) - 1 )
    {
        if ( Vec_PtrSize(p->vStates) >= nStatesMax )
        {
            printf( "Reached the limit on states traversed (%d).  ", nStatesMax );
            RetValue = -1;
            break;
        }
        pState = Gia_ManEraState( p, ++p->iCurState );
        if ( p->iCurState > 1 && pState->iPrev == 0 )
            continue;
//printf( "Extracting %d  ", p->iCurState );
//Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) );  printf( "\n" );
        Gia_ManInsertState( p, pState );
        Gia_ManPerformOneIter( p );
        if ( Gia_ManAnalyzeResult( p, pState, fMiter ) && fMiter )
        {
            RetValue = 0;
            printf( "Miter failed in state %d after %d transitions.  ", 
                p->iCurState, Vec_IntSize(p->vBugTrace)-1 );
            break;
        }
        if ( fVerbose && p->iCurState % 5000 == 0 )
        {
            printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f Mb.  ", 
                p->iCurState, Vec_PtrSize(p->vStates), 1.0*p->iCurState/Vec_PtrSize(p->vStates), Gia_ManCountDepth(p), 
                (1.0/(1<<20))*(1.0*Vec_PtrSize(p->vStates)*(sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat) + 
                   1.0*p->nBins*sizeof(unsigned) + 1.0*p->vStates->nCap * sizeof(void*)) );
            ABC_PRT( "Time", clock() - clk );
        }
    }
    printf( "Reachability analysis traversed %d states with depth %d.  ", p->iCurState-1, Gia_ManCountDepth(p) );
    ABC_PRT( "Time", clock() - clk );
    Gia_ManEraFree( p );
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END