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

  FileName    [cecClass.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Combinational equivalence checking.]

  Synopsis    [Equivalence class refinement.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "cecInt.h"

ABC_NAMESPACE_IMPL_START


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

static inline unsigned * Cec_ObjSim( Cec_ManSim_t * p, int Id )            { return p->pMems + p->pSimInfo[Id] + 1;   }
static inline void       Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n )  { p->pSimInfo[Id] = n;                     }

static inline float      Cec_MemUsage( Cec_ManSim_t * p )                  { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20);   }

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

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

  Synopsis    [Compares simulation info of one node with constant 0.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimCompareConst( unsigned * p, int nWords )
{
    int w;
    if ( p[0] & 1 )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p[w] != ~0 )
                return 0;
        return 1;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p[w] != 0 )
                return 0;
        return 1;
    }
}

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

  Synopsis    [Compares simulation info of two nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords )
{
    int w;
    if ( (p0[0] & 1) == (p1[0] & 1) )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != p1[w] )
                return 0;
        return 1;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != ~p1[w] )
                return 0;
        return 1;
    }
}

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

  Synopsis    [Returns the number of the first non-equal bit.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
{
    int w;
    if ( p[0] & 1 )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p[w] != ~0 )
                return 32*w + Gia_WordFindFirstBit( ~p[w] );
        return -1;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p[w] != 0 )
                return 32*w + Gia_WordFindFirstBit( p[w] );
        return -1;
    }
}

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

  Synopsis    [Compares simulation info of two nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
{
    int w;
    if ( (p0[0] & 1) == (p1[0] & 1) )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != p1[w] )
                return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] );
        return -1;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != ~p1[w] )
                return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] );
        return -1;
    }
}

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

  Synopsis    [Returns the number of the first non-equal bit.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimCompareConstScore( unsigned * p, int nWords, int * pScores )
{
    int w, b;
    if ( p[0] & 1 )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p[w] != ~0 )
                for ( b = 0; b < 32; b++ )
                    if ( ((~p[w]) >> b ) & 1 )
                        pScores[32*w + b]++;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p[w] != 0 )
                for ( b = 0; b < 32; b++ )
                    if ( ((p[w]) >> b ) & 1 )
                        pScores[32*w + b]++;
    }
}

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

  Synopsis    [Compares simulation info of two nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimCompareEqualScore( unsigned * p0, unsigned * p1, int nWords, int * pScores )
{
    int w, b;
    if ( (p0[0] & 1) == (p1[0] & 1) )
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != p1[w] )
                for ( b = 0; b < 32; b++ )
                    if ( ((p0[w] ^ p1[w]) >> b ) & 1 )
                        pScores[32*w + b]++;
    }
    else
    {
        for ( w = 0; w < nWords; w++ )
            if ( p0[w] != ~p1[w] )
                for ( b = 0; b < 32; b++ )
                    if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 )
                        pScores[32*w + b]++;
    }
}

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

  Synopsis    [Creates equivalence class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
{
    int Repr = GIA_VOID, EntPrev = -1, Ent, i;
    assert( Vec_IntSize(vClass) > 0 );
    Vec_IntForEachEntry( vClass, Ent, i )
    {
        if ( i == 0 )
        {
            Repr = Ent;
            Gia_ObjSetRepr( p, Ent, GIA_VOID );
            EntPrev = Ent;
        }
        else
        {
            assert( Repr < Ent );
            Gia_ObjSetRepr( p, Ent, Repr );
            Gia_ObjSetNext( p, EntPrev, Ent );
            EntPrev = Ent;
        }
    }
    Gia_ObjSetNext( p, EntPrev, 0 );
}

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

  Synopsis    [Refines one equivalence class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
{
    unsigned * pSim0, * pSim1;
    int Ent;
    Vec_IntClear( p->vClassOld );
    Vec_IntClear( p->vClassNew );
    Vec_IntPush( p->vClassOld, i );
    pSim0 = Cec_ObjSim(p, i);
    Gia_ClassForEachObj1( p->pAig, i, Ent )
    {
        pSim1 = Cec_ObjSim(p, Ent);
        if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
            Vec_IntPush( p->vClassOld, Ent );
        else
        {
            Vec_IntPush( p->vClassNew, Ent );
            if ( p->pBestState )
                Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores );
        }
    }
    if ( Vec_IntSize( p->vClassNew ) == 0 )
        return 0;
    Cec_ManSimClassCreate( p->pAig, p->vClassOld );
    Cec_ManSimClassCreate( p->pAig, p->vClassNew );
    if ( Vec_IntSize(p->vClassNew) > 1 )
        return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
    return 1;
}

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

  Synopsis    [Refines one equivalence class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i )
{
    int iRepr, Ent;
    if ( Gia_ObjIsConst(p->pAig, i) )
    {
        Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
        return 1;
    }
    if ( !Gia_ObjIsClass(p->pAig, i) )
        return 0;
    assert( Gia_ObjIsClass(p->pAig, i) );
    iRepr = Gia_ObjRepr( p->pAig, i );
    if ( iRepr == GIA_VOID )
        iRepr = i;
    // collect nodes
    Vec_IntClear( p->vClassOld );
    Vec_IntClear( p->vClassNew );
    Gia_ClassForEachObj( p->pAig, iRepr, Ent )
    {
        if ( Ent == i )
            Vec_IntPush( p->vClassNew, Ent );
        else
            Vec_IntPush( p->vClassOld, Ent );
    }
    assert( Vec_IntSize( p->vClassNew ) == 1 );
    Cec_ManSimClassCreate( p->pAig, p->vClassOld );
    Cec_ManSimClassCreate( p->pAig, p->vClassNew );
    assert( !Gia_ObjIsClass(p->pAig, i) );
    return 1;
}

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

  Synopsis    [Computes hash key of the simuation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize )
{
    static int s_Primes[16] = { 
        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
    unsigned uHash = 0;
    int i;
    if ( pSim[0] & 1 )
        for ( i = 0; i < nWords; i++ )
            uHash ^= ~pSim[i] * s_Primes[i & 0xf];
    else
        for ( i = 0; i < nWords; i++ )
            uHash ^= pSim[i] * s_Primes[i & 0xf];
    return (int)(uHash % nTableSize);

}

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

  Synopsis    [Resets pointers to the simulation memory.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimMemRelink( Cec_ManSim_t * p )
{
    unsigned * pPlace, Ent;
    pPlace = (unsigned *)&p->MemFree;
    for ( Ent = p->nMems * (p->nWords + 1); 
          Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc; 
          Ent += p->nWords + 1 )
    {
        *pPlace = Ent;
        pPlace = p->pMems + Ent;
    }
    *pPlace = 0;
    p->nWordsOld = p->nWords;
}

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

  Synopsis    [References simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i )
{
    unsigned * pSim;
    assert( p->pSimInfo[i] == 0 );
    if ( p->MemFree == 0 )
    {
        if ( p->nWordsAlloc == 0 )
        {
            assert( p->pMems == NULL );
            p->nWordsAlloc = (1<<17); // -> 1Mb
            p->nMems = 1;
        }
        p->nWordsAlloc *= 2;
        p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
        Cec_ManSimMemRelink( p );
    }
    p->pSimInfo[i] = p->MemFree;
    pSim = p->pMems + p->MemFree;
    p->MemFree = pSim[0];
    pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) );
    p->nMems++;
    if ( p->nMemsMax < p->nMems )
        p->nMemsMax = p->nMems;
    return pSim;
}

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

  Synopsis    [Dereferences simulaton info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i )
{
    unsigned * pSim;
    assert( p->pSimInfo[i] > 0 );
    pSim = p->pMems + p->pSimInfo[i];
    if ( --pSim[0] == 0 )
    {
        pSim[0] = p->MemFree;
        p->MemFree = p->pSimInfo[i];
        p->pSimInfo[i] = 0;
        p->nMems--;
    }
    return pSim;
}

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

  Synopsis    [Refines nodes belonging to candidate constant class.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
{
    unsigned * pSim;
    int * pTable, nTableSize, i, k, Key;
    if ( Vec_IntSize(vRefined) == 0 )
        return;
    nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
    pTable = ABC_CALLOC( int, nTableSize );
    Vec_IntForEachEntry( vRefined, i, k )
    {
        pSim = Cec_ObjSim( p, i );
        assert( !Cec_ManSimCompareConst( pSim, p->nWords ) );
        Key = Cec_ManSimHashKey( pSim, p->nWords, nTableSize );
        if ( pTable[Key] == 0 )
        {
            assert( Gia_ObjRepr(p->pAig, i) == 0 );
            assert( Gia_ObjNext(p->pAig, i) == 0 );
            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
        }
        else
        {
            Gia_ObjSetNext( p->pAig, pTable[Key], i );
            Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
            if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
                Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
            assert( Gia_ObjRepr(p->pAig, i) > 0 );
        }
        pTable[Key] = i;
    }
    Vec_IntForEachEntry( vRefined, i, k )
    {
        if ( Gia_ObjIsHead( p->pAig, i ) )
            Cec_ManSimClassRefineOne( p, i );
    }
    Vec_IntForEachEntry( vRefined, i, k )
        Cec_ManSimSimDeref( p, i );
    ABC_FREE( pTable );
}


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

  Synopsis    [Saves the input pattern with the given number.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
{
    unsigned * pInfo;
    int i;
    assert( p->pCexComb == NULL );
    assert( iPat >= 0 && iPat < 32 * p->nWords );
    p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char, 
        sizeof(Abc_Cex_t) + sizeof(unsigned) * Abc_BitWordNum(Gia_ManCiNum(p->pAig)) );
    p->pCexComb->iPo = p->iOut;
    p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
    p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
    for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
        if ( Abc_InfoHasBit( pInfo, iPat ) )
            Abc_InfoSetBit( p->pCexComb->pData, i );
    }
}

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

  Synopsis    [Find the best pattern using the scores.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
{ 
    unsigned * pInfo;
    int i, ScoreBest = 0, iPatBest = 1; // set the first pattern
    // find the best pattern
    for ( i = 0; i < 32 * p->nWords; i++ )
        if ( ScoreBest < p->pScores[i] )
        {
            ScoreBest = p->pScores[i];
            iPatBest = i;
        }
    // compare this with the available patterns - and save
    if ( p->pBestState->iPo <= ScoreBest )
    {
        assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) );
        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
        {
            pInfo = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
            if ( Abc_InfoHasBit(p->pBestState->pData, i) != Abc_InfoHasBit(pInfo, iPatBest) )
                Abc_InfoXorBit( p->pBestState->pData, i );
        }
        p->pBestState->iPo = ScoreBest;
    }
}

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

  Synopsis    [Returns 1 if computation should stop.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
{
    unsigned * pInfo, * pInfo2;
    int i;
    if ( !p->pPars->fCheckMiter )
        return 0;
    assert( p->vCoSimInfo != NULL );
    // compare outputs with 0
    if ( p->pPars->fDualOut )
    {
        assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
        for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
        {
            pInfo  = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
            pInfo2 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, ++i );
            if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) )
            {
                if ( p->iOut == -1 )
                {
                    p->iOut = i/2;
                    Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
                }
                if ( p->pCexes == NULL )
                    p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 );
                if ( p->pCexes[i/2] == NULL )
                {
                    p->nOuts++;
                    p->pCexes[i/2] = (void *)1;
                }
            }
        }
    }
    else
    {
        for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
        {
            pInfo = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, i );
            if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
            {
                if ( p->iOut == -1 )
                {
                    p->iOut = i;
                    Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
                }
                if ( p->pCexes == NULL )
                    p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) );
                if ( p->pCexes[i] == NULL )
                {
                    p->nOuts++;
                    p->pCexes[i] = (void *)1;
                }
            }
        }
    }
    return p->pCexes != NULL;
}

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

  Synopsis    [Simulates one round.]

  Description [Returns the number of PO entry if failed; 0 otherwise.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
{
    Gia_Obj_t * pObj;
    unsigned * pRes0, * pRes1, * pRes;
    int i, k, w, Ent, iCiId = 0, iCoId = 0;
    // prepare internal storage
    if ( p->nWordsOld != p->nWords )
        Cec_ManSimMemRelink( p );
    p->nMemsMax = 0;
    // allocate score counters
    ABC_FREE( p->pScores );
    if ( p->pBestState )
        p->pScores = ABC_CALLOC( int, 32 * p->nWords );
    // simulate nodes
    Vec_IntClear( p->vRefinedC );
    if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
    {
        pRes = Cec_ManSimSimRef( p, 0 );
        for ( w = 1; w <= p->nWords; w++ )
            pRes[w] = 0;
    }
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) ) 
        {
            if ( Gia_ObjValue(pObj) == 0 )
            {
                iCiId++;
                continue;
            }
            pRes = Cec_ManSimSimRef( p, i );
            if ( vInfoCis ) 
            {
                pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, iCiId++ );
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = pRes0[w-1];
            }
            else
            {
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = Gia_ManRandom( 0 );
            }
            // make sure the first pattern is always zero
            pRes[1] ^= (pRes[1] & 1);
            goto references;
        }
        if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
        {
            pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
            if ( vInfoCos )
            {
                pRes = (unsigned *)Vec_PtrEntry( vInfoCos, iCoId++ );
                if ( Gia_ObjFaninC0(pObj) )
                    for ( w = 1; w <= p->nWords; w++ )
                        pRes[w-1] = ~pRes0[w];
                else 
                    for ( w = 1; w <= p->nWords; w++ )
                        pRes[w-1] = pRes0[w];
            }
            continue;
        }
        assert( Gia_ObjValue(pObj) );
        pRes  = Cec_ManSimSimRef( p, i );
        pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
        pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );

//        Abc_Print( 1, "%d,%d  ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );

        if ( Gia_ObjFaninC0(pObj) )
        {
            if ( Gia_ObjFaninC1(pObj) )
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = ~(pRes0[w] | pRes1[w]);
            else
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = ~pRes0[w] & pRes1[w];
        }
        else
        {
            if ( Gia_ObjFaninC1(pObj) )
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = pRes0[w] & ~pRes1[w];
            else
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = pRes0[w] & pRes1[w];
        }

references:
        // if this node is candidate constant, collect it
        if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
        {
            pRes[0]++;
            Vec_IntPush( p->vRefinedC, i );
            if ( p->pBestState )
                Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores );
        }
        // if the node belongs to a class, save it
        if ( Gia_ObjIsClass(p->pAig, i) )
            pRes[0]++;
        // if this is the last node of the class, process it
        if ( Gia_ObjIsTail(p->pAig, i) )
        {
            Vec_IntClear( p->vClassTemp );
            Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent )
                Vec_IntPush( p->vClassTemp, Ent );
            Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) );
            Vec_IntForEachEntry( p->vClassTemp, Ent, k )
                Cec_ManSimSimDeref( p, Ent );
        }
    }

    if ( p->pPars->fConstCorr )
    {
        Vec_IntForEachEntry( p->vRefinedC, i, k )
        {
            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
            Cec_ManSimSimDeref( p, i );
        }
        Vec_IntClear( p->vRefinedC );
    }

    if ( Vec_IntSize(p->vRefinedC) > 0 )
        Cec_ManSimProcessRefined( p, p->vRefinedC );
    assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
    assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
    assert( p->nMems == 1 );
    if ( p->nMems != 1 )
        Abc_Print( 1, "Cec_ManSimSimulateRound(): Memory management error!\n" );
    if ( p->pPars->fVeryVerbose )
        Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
    if ( p->pBestState )
        Cec_ManSimFindBestPattern( p );
/*
    if ( p->nMems > 1 ) {
        for ( i = 1; i < p->nObjs; i++ )
        if ( p->pSims[i] ) {
            int x = 0;
        }
    }
*/
    return Cec_ManSimAnalyzeOutputs( p );
}


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

  Synopsis    [Creates simulation info for this round.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
{
    unsigned * pRes0, * pRes1;
    int i, w;
    if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 )
    {
        assert( vInfoCis && vInfoCos );
        for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
        {
            pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
            for ( w = 0; w < p->nWords; w++ )
                pRes0[w] = Gia_ManRandom( 0 );
        }
        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
        {
            pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
            pRes1 = (unsigned *)Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
            for ( w = 0; w < p->nWords; w++ )
                pRes0[w] = pRes1[w];
        }
    }
    else 
    {
        for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
        {
            pRes0 = (unsigned *)Vec_PtrEntry( vInfoCis, i );
            for ( w = 0; w < p->nWords; w++ )
                pRes0[w] = Gia_ManRandom( 0 );
        }
    }
}

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

  Synopsis    [Returns 1 if the bug is found.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
{
    Gia_Obj_t * pObj;
    int i;
    assert( p->pAig->pReprs == NULL );
    // allocate representation
    p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
    p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
    // create references
    Gia_ManCreateValueRefs( p->pAig );
    // set starting representative of internal nodes to be constant 0
    if ( p->pPars->fLatchCorr )
        Gia_ManForEachObj( p->pAig, pObj, i )
            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
    else if ( LevelMax == -1 )
        Gia_ManForEachObj( p->pAig, pObj, i )
            Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
    else
    {
        Gia_ManLevelNum( p->pAig );
        Gia_ManForEachObj( p->pAig, pObj, i )
            Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) && Gia_ObjLevel(p->pAig,pObj) <= LevelMax) ? 0 : GIA_VOID );
        Vec_IntFreeP( &p->pAig->vLevels );
    }
    // if sequential simulation, set starting representative of ROs to be constant 0
    if ( p->pPars->fSeqSimulate )
        Gia_ManForEachRo( p->pAig, pObj, i )
            if ( pObj->Value )
                Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
    // perform simulation
    p->nWords = 1;
    do {
        if ( p->pPars->fVerbose )
            Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
        for ( i = 0; i < 4; i++ )
        {
            Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
            if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
                return 1;
        }
        p->nWords = 2 * p->nWords + 1;
    }
    while ( p->nWords <= p->pPars->nWords );
    return 0;
}

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

  Synopsis    [Returns 1 if the bug is found.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
{
    int i;
    Gia_ManCreateValueRefs( p->pAig );
    p->nWords = p->pPars->nWords;
    for ( i = 0; i < p->pPars->nRounds; i++ )
    {
        if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose )
            Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
        Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
            return 1;
    }
    if ( p->pPars->fVerbose )
        Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
    return 0;
}
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END