abc/src/aig/cec/cecClass.c

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

  FileName    [cecClass.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Combinatinoal equivalence checking.]

  Synopsis    [Equivalence class representation.]

  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"

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

static inline int        Cec_ObjRepr( Cec_ManCsw_t * p, int Id )               { return p->pObjs[Id].iRepr;               }
static inline void       Cec_ObjSetRepr( Cec_ManCsw_t * p, int Id, int Num )   { p->pObjs[Id].iRepr = Num;                }

static inline int        Cec_ObjProved( Cec_ManCsw_t * p, int Id )             { return p->pObjs[Id].iProved;             }
static inline void       Cec_ObjSetProved( Cec_ManCsw_t * p, int Id )          { p->pObjs[Id].iProved = 1;                }

static inline int        Cec_ObjFailed( Cec_ManCsw_t * p, int Id )             { return p->pObjs[Id].iFailed;             }
static inline void       Cec_ObjSetFailed( Cec_ManCsw_t * p, int Id )          { p->pObjs[Id].iFailed = 1;                }

static inline int        Cec_ObjNext( Cec_ManCsw_t * p, int Id )               { return p->pObjs[Id].iNext;               }
static inline void       Cec_ObjSetNext( Cec_ManCsw_t * p, int Id, int Num )   { p->pObjs[Id].iNext = Num;                }

static inline unsigned   Cec_ObjSim( Cec_ManCsw_t * p, int Id )                { return p->pObjs[Id].SimNum;              }
static inline unsigned * Cec_ObjSimP1( Cec_ManCsw_t * p, int Id )              { return &p->pObjs[Id].SimNum;             }
static inline unsigned * Cec_ObjSimP( Cec_ManCsw_t * p, int Id )               { return p->pMems + Cec_ObjSim(p, Id) + 1; }
static inline void       Cec_ObjSetSim( Cec_ManCsw_t * p, int Id, unsigned n ) { p->pObjs[Id].SimNum = n;                 }

static inline int        Cec_ObjIsConst( Cec_ManCsw_t * p, int Id )            { return Cec_ObjRepr(p, Id) == 0;                           }
static inline int        Cec_ObjIsHead( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) > 0;  }
static inline int        Cec_ObjIsNone( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) == 0; }
static inline int        Cec_ObjIsTail( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) > 0 && Cec_ObjNext(p, Id) == 0; }
static inline int        Cec_ObjIsClass( Cec_ManCsw_t * p, int Id )            { return Cec_ObjRepr(p, Id) > 0 || Cec_ObjNext(p, Id) > 0;  }

#define Cec_ManForEachObj( p, i )                              \
    for ( i = 0; i < Gia_ManObjNum(p->pAig); i++ )
#define Cec_ManForEachObj1( p, i )                             \
    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
#define Cec_ManForEachClass( p, i )                            \
    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) if ( !Cec_ObjIsHead(p, i) ) {} else
#define Cec_ClassForEachObj( p, i, iObj )                      \
    for ( assert(Cec_ObjIsHead(p, i)), iObj = i; iObj; iObj = Cec_ObjNext(p, iObj) )
#define Cec_ClassForEachObj1( p, i, iObj )                     \
    for ( assert(Cec_ObjIsHead(p, i)), iObj = Cec_ObjNext(p, i); iObj; iObj = Cec_ObjNext(p, iObj) )

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

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

  Synopsis    [Creates the set of representatives.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p )
{
    int i, * pReprs = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
        if ( Cec_ObjProved(p, i) )
        {
            assert( Cec_ObjRepr(p, i) >= 0 );
            pReprs[i] = Cec_ObjRepr(p, i);
        }
    return pReprs;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Cec_ManCswDupWithClasses( Cec_ManCsw_t * p )
{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    int iRes0, iRes1, iRepr, iNode;
    int i, fCompl, * piCopies;
    Vec_IntClear( p->vXorNodes );
    Gia_ManLevelNum( p->pAig );
    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
    Gia_ManHashAlloc( pNew );
    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
    piCopies[0] = 0;
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) ) 
        {
            piCopies[i] = Gia_ManAppendCi( pNew );
            continue;
        }
        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
        if ( Gia_ObjIsCo(pObj) ) 
        {
            Gia_ManAppendCo( pNew, iRes0 );
            continue;
        }
        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
        if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
            continue;
        assert( Cec_ObjRepr(p, i) < i );
        iRepr = piCopies[Cec_ObjRepr(p, i)];
        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
            continue;
        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
    }
    ABC_FREE( piCopies );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, 0 );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Cec_ManCswSpecReduction( Cec_ManCsw_t * p )
{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    int iRes0, iRes1, iRepr, iNode, iMiter;
    int i, fCompl, * piCopies, * pDepths;
    Vec_IntClear( p->vXorNodes );
//    Gia_ManLevelNum( p->pAig );
    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
    Gia_ManHashAlloc( pNew );
    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
    pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
    piCopies[0] = 0;
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) ) 
        {
            piCopies[i] = Gia_ManAppendCi( pNew );
            continue;
        }
        if ( Gia_ObjIsCo(pObj) ) 
            continue;
        if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
             piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
             continue;
        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
        pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
        if ( Cec_ObjRepr(p, i) < 0 || Cec_ObjFailed(p, i) )
            continue;
        assert( Cec_ObjRepr(p, i) < i );
        iRepr = piCopies[Cec_ObjRepr(p, i)];
        if ( iRepr == -1 )
            continue;
        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
            continue;
        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
        if ( Cec_ObjProved(p, i) )
            continue;
//        if ( p->pPars->nLevelMax && 
//            (Gia_ObjLevel(p->pAig, pObj)  > p->pPars->nLevelMax || 
//             Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
//            continue;
        // produce speculative miter
        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
        Gia_ManAppendCo( pNew, iMiter );
        Vec_IntPush( p->vXorNodes, Cec_ObjRepr(p, i) );
        Vec_IntPush( p->vXorNodes, i );
        // add to the depth of this node
        pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Cec_ObjRepr(p, i)] );
        if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
            piCopies[i] = -1;
    }
    ABC_FREE( piCopies );
    ABC_FREE( pDepths );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, 0 );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
Gia_Man_t * Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p )
{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    int iRes0, iRes1, iRepr, iNode, iMiter;
    int i, fCompl, * piCopies;
    Vec_IntClear( p->vXorNodes );
    Gia_ManLevelNum( p->pAig );
    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
    Gia_ManHashAlloc( pNew );
    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
    piCopies[0] = 0;
    Gia_ManForEachObj1( p->pAig, pObj, i )
    {
        if ( Gia_ObjIsCi(pObj) ) 
        {
            piCopies[i] = Gia_ManAppendCi( pNew );
            continue;
        }
        if ( Gia_ObjIsCo(pObj) ) 
            continue;
        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
        if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
            continue;
        assert( Cec_ObjRepr(p, i) < i );
        iRepr = piCopies[Cec_ObjRepr(p, i)];
        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
            continue;
        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
        // add speculative miter
        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
        Gia_ManAppendCo( pNew, iMiter );
    }
    ABC_FREE( piCopies );
    Gia_ManHashStop( pNew );
    Gia_ManSetRegNum( pNew, 0 );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    return pNew;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswCountOne( Cec_ManCsw_t * p, int i )
{
    int Ent, nLits = 1;
    Cec_ClassForEachObj1( p, i, Ent )
    {
        assert( Cec_ObjRepr(p, Ent) == i );
        nLits++;
    }
    return nLits;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswCountLitsAll( Cec_ManCsw_t * p )
{
    int i, nLits = 0;
    Cec_ManForEachObj( p, i )
        nLits += (Cec_ObjRepr(p, i) >= 0);
    return nLits;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter )
{
    int Ent;
    printf( "Class %4d :  Num = %2d  {", Counter, Cec_ManCswCountOne(p, i) );
    Cec_ClassForEachObj( p, i, Ent )
        printf(" %d", Ent );
    printf( " }\n" );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose )
{
    int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits;
    Cec_ManForEachObj1( p, i )
    {
        if ( Cec_ObjIsHead(p, i) )
            Counter++;
        else if ( Cec_ObjIsConst(p, i) )
            Counter1++;
        else if ( Cec_ObjIsNone(p, i) )
            CounterX++;
    }
    nLits = Cec_ManCswCountLitsAll( p );
    printf( "Class =%7d. Const =%7d. Unsed =%7d. Lits =%8d. All =%8d. Mem = %5.2f Mb\n", 
        Counter, Counter1, CounterX, nLits-Counter1, nLits, 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20) );
    if ( fVerbose )
    {
        Counter = 0;
        Cec_ManForEachClass( p, i )
            Cec_ManCswPrintOne( p, i, ++Counter );
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswCompareEqual( 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    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswCompareConst( 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    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass )
{
    int Repr = -1, EntPrev = -1, Ent, i;
    assert( Vec_IntSize(vClass) > 0 );
    Vec_IntForEachEntry( vClass, Ent, i )
    {
        if ( i == 0 )
        {
            Repr = Ent;
            Cec_ObjSetRepr( p, Ent, -1 );
            EntPrev = Ent;
        }
        else
        {
            Cec_ObjSetRepr( p, Ent, Repr );
            Cec_ObjSetNext( p, EntPrev, Ent );
            EntPrev = Ent;
        }
    }
    Cec_ObjSetNext( p, EntPrev, 0 );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst )
{
    unsigned * pSim0, * pSim1;
    int Ent;
    Vec_IntClear( p->vClassOld );
    Vec_IntClear( p->vClassNew );
    Vec_IntPush( p->vClassOld, i );
    pSim0 = fFirst? Cec_ObjSimP1(p, i) : Cec_ObjSimP(p, i);
    Cec_ClassForEachObj1( p, i, Ent )
    {
        pSim1 = fFirst? Cec_ObjSimP1(p, Ent) : Cec_ObjSimP(p, Ent);
        if ( Cec_ManCswCompareEqual( pSim0, pSim1, p->nWords ) )
            Vec_IntPush( p->vClassOld, Ent );
        else
            Vec_IntPush( p->vClassNew, Ent );
    }
    if ( Vec_IntSize( p->vClassNew ) == 0 )
        return 0;
    Cec_ManCswClassCreate( p, p->vClassOld );
    Cec_ManCswClassCreate( p, p->vClassNew );
    if ( Vec_IntSize(p->vClassNew) > 1 )
        return 1 + Cec_ManCswClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), fFirst );
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswHashKey( 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    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswClassesCreate( Cec_ManCsw_t * p )
{
    int * pTable, nTableSize, i, Key;
    p->nWords = 1;
    nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p->pAig) / 10 );
    pTable = ABC_CALLOC( int, nTableSize );
    Cec_ObjSetRepr( p, 0, -1 );
    Cec_ManForEachObj1( p, i )
    {
        if ( Gia_ObjIsCo(Gia_ManObj(p->pAig, i)) ) 
        {
            Cec_ObjSetRepr( p, i, -1 );
            continue;
        }
        if ( Cec_ManCswCompareConst( Cec_ObjSimP1(p, i), p->nWords ) )
        {
            Cec_ObjSetRepr( p, i, 0 );
            continue;
        }
        Key = Cec_ManCswHashKey( Cec_ObjSimP1(p, i), p->nWords, nTableSize );
        if ( pTable[Key] == 0 )
            Cec_ObjSetRepr( p, i, -1 );
        else
        {
            Cec_ObjSetNext( p, pTable[Key], i );
            Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
            if ( Cec_ObjRepr(p, i) == -1 )
                Cec_ObjSetRepr( p, i, pTable[Key] );
        }
        pTable[Key] = i;
    }
    ABC_FREE( pTable );
    if ( p->pPars->fVeryVerbose )
    Cec_ManCswPrintClasses( p, 0 );
    // refine classes
    Cec_ManForEachClass( p, i )
        Cec_ManCswClassRefineOne( p, i, 1 );
    // clean memory
    Cec_ManForEachObj( p, i )
        Cec_ObjSetSim( p, i, 0 );
    if ( p->pPars->fVeryVerbose )
    Cec_ManCswPrintClasses( p, 0 );
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswSimulateSimple( Cec_ManCsw_t * p )
{
    Gia_Obj_t * pObj;
    unsigned Res0, Res1;
    int i;
    Gia_ManForEachCi( p->pAig, pObj, i )
        Cec_ObjSetSim( p, i, Aig_ManRandom(0) );
    Gia_ManForEachAnd( p->pAig, pObj, i )
    {
        Res0 = Cec_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
        Res1 = Cec_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
        Cec_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
                             (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
    }
}

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

  Synopsis    [References simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
{
    unsigned * pPlace, Ent;
    pPlace = &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;
}

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

  Synopsis    [References simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
{
    unsigned * pSim;
    assert( p->pObjs[i].SimNum == 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_ManCswSimMemRelink( p );
    }
    p->pObjs[i].SimNum = 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    [Dereference simulaton info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
{
    unsigned * pSim;
    assert( p->pObjs[i].SimNum > 0 );
    pSim = p->pMems + p->pObjs[i].SimNum;
    if ( --pSim[0] == 0 )
    {
        pSim[0] = p->MemFree;
        p->MemFree = p->pObjs[i].SimNum;
        p->pObjs[i].SimNum = 0;
        p->nMems--;
    }
    return pSim;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined )
{
    unsigned * pSim;
    int * pTable, nTableSize, i, k, Key;
    if ( Vec_IntSize(vRefined) == 0 )
        return;
    nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
    pTable = ABC_CALLOC( int, nTableSize );
    Vec_IntForEachEntry( vRefined, i, k )
    {
        if ( i == 7720 )
        {
            int s = 0;
        }
        pSim = Cec_ObjSimP( p, i );
        assert( !Cec_ManCswCompareConst( pSim, p->nWords ) );
        Key = Cec_ManCswHashKey( pSim, p->nWords, nTableSize );
        if ( pTable[Key] == 0 )
        {
            assert( Cec_ObjRepr(p, i) == 0 );
            assert( Cec_ObjNext(p, i) == 0 );
            Cec_ObjSetRepr( p, i, -1 );
        }
        else
        {
            Cec_ObjSetNext( p, pTable[Key], i );
            Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
            if ( Cec_ObjRepr(p, i) == -1 )
                Cec_ObjSetRepr( p, i, pTable[Key] );
            assert( Cec_ObjRepr(p, i) > 0 );
        }
        pTable[Key] = i;
    }
    Vec_IntForEachEntry( vRefined, i, k )
    {
        if ( Cec_ObjIsHead( p, i ) )
            Cec_ManCswClassRefineOne( p, i, 0 );
    }
    Vec_IntForEachEntry( vRefined, i, k )
        Cec_ManCswSimDeref( p, i );
    ABC_FREE( pTable );
}


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

  Synopsis    [Simulates one round.]

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

  SeeAlso     []

***********************************************************************/
void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, int iSeries, int fRandomize )
{
    static int nCountRand = 0;
    Gia_Obj_t * pObj;
    unsigned * pRes0, * pRes1, * pRes;
    int i, k, w, Ent, iCiId = 0, iCoId = 0;
    p->nMemsMax = 0;
    Vec_IntClear( p->vRefinedC );
    if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
    {
        pRes = Cec_ManCswSimRef( 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_ManCswSimRef( p, i );
            if ( vInfoCis ) 
            {
                pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
                for ( w = 1; w <= p->nWords; w++ )
                {
                    pRes[w] = pRes0[iSeries*p->nWords+w-1];
                    if ( fRandomize )
                        pRes[w] ^= (1 << (nCountRand++ & 0x1f));
                }
            }
            else
            {
                for ( w = 1; w <= p->nWords; w++ )
                    pRes[w] = Aig_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_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
            if ( vInfoCos )
            {
                pRes = 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_ManCswSimRef( p, i );
        pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
        pRes1 = Cec_ManCswSimDeref( p, Gia_ObjFaninId1(pObj,i) );
        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 ( Cec_ObjIsConst(p, i) && !Cec_ManCswCompareConst(pRes + 1, p->nWords) )
        {
            pRes[0]++;
            Vec_IntPush( p->vRefinedC, i );
        }
        // if the node belongs to a class, save it
        if ( Cec_ObjIsClass(p, i) )
            pRes[0]++;
        // if this is the last node of the class, process it
        if ( Cec_ObjIsTail(p, i) )
        {
            Vec_IntClear( p->vClassTemp );
            Cec_ClassForEachObj( p, Cec_ObjRepr(p, i), Ent )
                Vec_IntPush( p->vClassTemp, Ent );
            Cec_ManCswClassRefineOne( p, Cec_ObjRepr(p, i), 0 );
            Vec_IntForEachEntry( p->vClassTemp, Ent, k )
                Cec_ManCswSimDeref( p, Ent );
        }
    }
    if ( Vec_IntSize(p->vRefinedC) > 0 )
        Cec_ManCswProcessRefined( 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->pPars->fVeryVerbose )
        Cec_ManCswPrintClasses( p, 0 );
/*
    if ( p->nMems > 1 )
    {
        for ( i = 1; i < p->nObjs; i++ )
        if ( p->pSims[i] )
        {
            int x = 0;
        }
    }
*/
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p )
{
    int i;
    Gia_ManSetRefs( p->pAig );
    Cec_ManCswSimulateSimple( p );
    Cec_ManCswClassesCreate( p );
    for ( i = 0; i < p->pPars->nRounds; i++ )
    {
        p->nWords = i + 1;
        Cec_ManCswSimMemRelink( p );
        Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
    }
    p->nWords = p->pPars->nWords;
    Cec_ManCswSimMemRelink( p );
    for ( i = 0; i < p->pPars->nRounds; i++ )
        Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
    return 1;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj )
{
    int Result;
    if ( pObj->fMark0 )
        return 1;
    if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
        return 0;
    Result = (Cec_ManCswClassesUpdate_rec( Gia_ObjFanin0(pObj) ) |
              Cec_ManCswClassesUpdate_rec( Gia_ObjFanin1(pObj) ));
    return pObj->fMark0 = Result;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew )
{
    Vec_Ptr_t * vInfo;
    Gia_Obj_t * pObj, * pObjOld, * pReprOld;
    int i, k, iRepr, iNode;
    vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), p->pPars->nWords );
    if ( vInfo != NULL )
    {
        for ( i = 0; i < pPat->nSeries; i++ )
            Cec_ManCswSimulateRound( p, vInfo, NULL, i, 0 );
        Vec_PtrFree( vInfo );
    }
    assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
    // mark the transitive fanout of failed nodes
    if ( p->pPars->nDepthMax != 1 )
    {
        Gia_ManCleanMark0( p->pAig );
        Gia_ManCleanMark1( p->pAig );
        Gia_ManForEachCo( pNew, pObj, k )
        {
            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
                continue;
//            Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
            Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
        }
        // mark the nodes reachable through the failed nodes
        Gia_ManForEachAnd( p->pAig, pObjOld, k )
            pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
        // unmark the disproved nodes
        Gia_ManForEachCo( pNew, pObj, k )
        {
            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
                continue; 
            pObjOld = Gia_ManObj(p->pAig, iNode);
            assert( pObjOld->fMark0 == 1 );
            if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
                pObjOld->fMark1 = 1;
        }
        // clean marks
        Gia_ManForEachAnd( p->pAig, pObjOld, k )
            if ( pObjOld->fMark1 )
            {
                pObjOld->fMark0 = 0;
                pObjOld->fMark1 = 0;
            }
    }
    // set the results
    Gia_ManForEachCo( pNew, pObj, k )
    {
        iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
        iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
        pReprOld = Gia_ManObj(p->pAig, iRepr);
        pObjOld = Gia_ManObj(p->pAig, iNode);
        if ( pObj->fMark1 )
        { // proved
            assert( pObj->fMark0 == 0 );
            assert( !Cec_ObjProved(p, iNode) );
            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
//            if ( pObjOld->fMark0 == 0 )
            {
                assert( iRepr == Cec_ObjRepr(p, iNode) );
                Cec_ObjSetProved( p, iNode );
                p->nAllProved++;
            }
        }
        else if ( pObj->fMark0 )
        { // disproved
            assert( pObj->fMark1 == 0 );
            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
//            if ( pObjOld->fMark0 == 0 )
            {
                if ( iRepr == Cec_ObjRepr(p, iNode) )
                    printf( "Cec_ManCswClassesUpdate(): Error! Node is not refined!\n" );
                p->nAllDisproved++;
            }
        }
        else
        { // failed
            assert( pObj->fMark0 == 0 );
            assert( pObj->fMark1 == 0 );
            assert( !Cec_ObjFailed(p, iNode) );
            assert( !Cec_ObjProved(p, iNode) );
            Cec_ObjSetFailed( p, iNode );
            p->nAllFailed++;
        }
    } 
    return 0;
}


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