Experimental simulation based code.

1 files changed, 0 insertions, 638 deletions

diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index da38ede6..001bd8ac 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -1223,644 +1223,6 @@ int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 )
 
 
 
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Wrd_t * Gia_ManSimPatGenRandom( int nWords )
-{
-    Vec_Wrd_t * vSims = Vec_WrdAlloc( nWords ); int i;
-    for ( i = 0; i < nWords; i++ )
-        Vec_WrdPush( vSims, Gia_ManRandomW(0) );
-    return vSims;
-}
-void Gia_ManSimPatAssignInputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsIn )
-{
-    int i, Id;
-    assert( Vec_WrdSize(vSims)   == nWords * Gia_ManObjNum(p) );
-    assert( Vec_WrdSize(vSimsIn) == nWords * Gia_ManCiNum(p) );
-    Gia_ManForEachCiId( p, Id, i )
-        memcpy( Vec_WrdEntryP(vSims, Id*nWords), Vec_WrdEntryP(vSimsIn, i*nWords), sizeof(word)*nWords );
-}
-static inline void Gia_ManSimPatSimAnd( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
-{
-    word pComps[2] = { 0, ~(word)0 };
-    word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
-    word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
-    word * pSims  = Vec_WrdArray(vSims);
-    word * pSims0 = pSims + nWords*Gia_ObjFaninId0(pObj, i);
-    word * pSims1 = pSims + nWords*Gia_ObjFaninId1(pObj, i);
-    word * pSims2 = pSims + nWords*i; int w;
-    for ( w = 0; w < nWords; w++ )
-        pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1);
-}
-static inline void Gia_ManSimPatSimPo( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims )
-{
-    word pComps[2] = { 0, ~(word)0 };
-    word Diff0     = pComps[Gia_ObjFaninC0(pObj)];
-    word * pSims   = Vec_WrdArray(vSims);
-    word * pSims0  = pSims + nWords*Gia_ObjFaninId0(pObj, i);
-    word * pSims2  = pSims + nWords*i; int w;
-    for ( w = 0; w < nWords; w++ )
-        pSims2[w] = (pSims0[w] ^ Diff0);
-}
-Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * pGia )
-{
-    Gia_Obj_t * pObj;
-    int i, nWords = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia);
-    Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
-    assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
-    Gia_ManSimPatAssignInputs( pGia, nWords, vSims, pGia->vSimsPi );
-    Gia_ManForEachAnd( pGia, pObj, i ) 
-        Gia_ManSimPatSimAnd( pGia, i, pObj, nWords, vSims );
-    Gia_ManForEachCo( pGia, pObj, i )
-        Gia_ManSimPatSimPo( pGia, Gia_ObjId(pGia, pObj), pObj, nWords, vSims );
-    return vSims;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/\
-Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddOn, int nWordsUse )
-{
-    int nWordsBase  = Vec_WrdSize(vBase)  / nInputs;
-    int nWordsAddOn = Vec_WrdSize(vAddOn) / nInputs; int i, w;
-    Vec_Wrd_t * vSimsIn = Vec_WrdAlloc( nInputs * (nWordsBase + nWordsUse) );
-    assert( Vec_WrdSize(vBase)  % nInputs == 0 );
-    assert( Vec_WrdSize(vAddOn) % nInputs == 0 );
-    assert( nWordsUse <= nWordsAddOn );
-    for ( i = 0; i < nInputs; i++ )
-    {
-        word * pSimsB = Vec_WrdEntryP( vBase,  i * nWordsBase );
-        word * pSimsA = Vec_WrdEntryP( vAddOn, i * nWordsAddOn );
-        for ( w = 0; w < nWordsBase; w++ )
-            Vec_WrdPush( vSimsIn, pSimsB[w] );
-        for ( w = 0; w < nWordsUse; w++ )
-            Vec_WrdPush( vSimsIn, pSimsA[w] );
-    }
-    assert( Vec_WrdSize(vSimsIn) == Vec_WrdCap(vSimsIn) );
-    return vSimsIn;
-}
-int Gia_ManSimBitPackOne( int nWords, Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsCare, int iPat, int * pLits, int nLits )
-{
-    word * pSimsI, * pSimsC; int i, k;
-    for ( i = 0; i < iPat; i++ )
-    {
-        for ( k = 0; k < nLits; k++ )
-        {
-            int iVar = Abc_Lit2Var( pLits[k] );
-            pSimsI = Vec_WrdEntryP( vSimsIn,   nWords * iVar );
-            pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar );
-            if ( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k])) )
-                break;
-        }
-        if ( k == nLits )
-            break;
-    }
-    for ( k = 0; k < nLits; k++ )
-    {
-        int iVar = Abc_Lit2Var( pLits[k] );
-        pSimsI = Vec_WrdEntryP( vSimsIn,   nWords * iVar );
-        pSimsC = Vec_WrdEntryP( vSimsCare, nWords * iVar );
-        if ( !Abc_TtGetBit(pSimsC, i) && Abc_TtGetBit(pSimsI, i) == Abc_LitIsCompl(pLits[k]) )
-            Abc_TtXorBit( pSimsI, i );
-        Abc_TtSetBit( pSimsC, i );
-        assert( Abc_TtGetBit(pSimsC, i) && (Abc_TtGetBit(pSimsI, i) != Abc_LitIsCompl(pLits[k])) );
-    }
-    return (int)(i == iPat);
-}
-Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCexes )
-{
-    int c, iCur = 0, iPat = 0;
-    int nWordsMax = Abc_Bit6WordNum( nCexes ); 
-    Vec_Wrd_t * vSimsIn   = Gia_ManSimPatGenRandom( Gia_ManCiNum(p) * nWordsMax );
-    Vec_Wrd_t * vSimsCare = Vec_WrdStart( Gia_ManCiNum(p) * nWordsMax );
-    Vec_Wrd_t * vSimsRes  = NULL;
-    for ( c = 0; c < nCexes; c++ )
-    {
-        int Out  = Vec_IntEntry( vCexStore, iCur++ );
-        int Size = Vec_IntEntry( vCexStore, iCur++ );
-        iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size );
-        iCur += Size;
-        assert( iPat <= nCexes );
-        Out = 0;
-    }
-    printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
-    assert( iCur == Vec_IntSize(vCexStore) );
-    vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) );
-    printf( "Combined %d words of the original info with %d words of additional info.\n", 
-        Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) );
-    Vec_WrdFree( vSimsIn );
-    Vec_WrdFree( vSimsCare );
-    return vSimsRes;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManSimPatHashPatterns( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int * pnC0, int * pnC1 )
-{
-    Gia_Obj_t * pObj; 
-    int i, nUnique;
-    Vec_Mem_t * vStore;
-    vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
-    Vec_MemHashAlloc( vStore, 1 << 12 );
-    Gia_ManForEachCand( p, pObj, i )
-    {
-        word * pSim = Vec_WrdEntryP(vSims, i*nWords);
-        if ( pnC0 && Abc_TtIsConst0(pSim, nWords) )
-            (*pnC0)++;
-        if ( pnC1 && Abc_TtIsConst1(pSim, nWords) )
-            (*pnC1)++;
-        Vec_MemHashInsert( vStore, pSim );
-    }
-    nUnique = Vec_MemEntryNum( vStore );
-    Vec_MemHashFree( vStore );
-    Vec_MemFree( vStore );
-    return nUnique;
-}
-Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims )
-{
-    Gia_Man_t * pNew;
-    Gia_Obj_t * pObj;
-    int i, nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(p);
-    pNew = Gia_ManStart( Gia_ManObjNum(p) + Gia_ManCoNum(p) );
-    Gia_ManHashStart( pNew );
-    Gia_ManConst0(p)->Value = 0;
-    Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = Gia_ManAppendCi( pNew );
-    Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        word * pSim = Vec_WrdEntryP(vSims, i*nWords);
-        if ( Abc_TtIsConst0(pSim, nWords) )
-            Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 0) );
-        if ( Abc_TtIsConst1(pSim, nWords) )
-            Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, 1) );
-    }
-    Gia_ManHashStop( pNew );
-    return pNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords )
-{
-    int k, Digit, nDigits = nWords*16;
-    for ( k = 0; k < nDigits; k++ )
-    {
-        Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15);
-        if ( Digit < 10 )
-            fprintf( pFile, "%d", Digit );
-        else
-            fprintf( pFile, "%c", 'A' + Digit-10 );
-    }
-    fprintf( pFile, "\n" );
-}
-void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
-{
-    int i, nNodes = Vec_WrdSize(vSimsIn) / nWords;
-    FILE * pFile = fopen( pFileName, "wb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
-        return;
-    }
-    assert( Vec_WrdSize(vSimsIn) % nWords == 0 );
-    for ( i = 0; i < nNodes; i++ )
-        Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords );
-    fclose( pFile );
-    printf( "Written %d words of simulation data.\n", nWords );
-}
-int Gia_ManSimPatReadOne( char c )
-{
-    int Digit = 0;
-    if ( c >= '0' && c <= '9' )
-        Digit = c - '0';
-    else if ( c >= 'A' && c <= 'F' )
-        Digit = c - 'A' + 10;
-    else if ( c >= 'a' && c <= 'f' )
-        Digit = c - 'a' + 10;
-    else assert( 0 );
-    assert( Digit >= 0 && Digit < 16 );
-    return Digit;
-}
-Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName )
-{
-    Vec_Wrd_t * vSimsIn = NULL; 
-    int c, nWords = -1, nChars = 0; word Num = 0;
-    FILE * pFile = fopen( pFileName, "rb" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
-        return NULL;
-    }
-    vSimsIn = Vec_WrdAlloc( 1000 );
-    while ( (c = fgetc(pFile)) != EOF )
-    {
-        if ( c == '\n' && nWords == -1 )
-            nWords = Vec_WrdSize(vSimsIn);
-        if ( c == '\n' || c == '\r' || c == '\t' || c == ' ' )
-            continue;
-        Num |= (word)Gia_ManSimPatReadOne((char)c) << (nChars * 4);
-        if ( ++nChars < 16 )
-            continue;
-        Vec_WrdPush( vSimsIn, Num );
-        nChars = 0; 
-        Num = 0;
-    }
-    assert( Vec_WrdSize(vSimsIn) % nWords == 0 );
-    fclose( pFile );
-    printf( "Read %d words of simulation data.\n", nWords );
-    return vSimsIn;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManSimProfile( Gia_Man_t * pGia )
-{
-    Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
-    int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
-    int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
-    printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n", 
-        nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
-    Vec_WrdFree( vSims );
-}
-void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
-{
-    extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
-    int i, Status, Counts[3] = {0};
-    Gia_Man_t * pGia;
-    Vec_Wrd_t * vSimsIn = NULL;
-    Vec_Str_t * vStatus = NULL;
-    Vec_Int_t * vCexStore = NULL;
-    Vec_Wrd_t * vSims = Gia_ManSimPatSim( p );
-    Gia_ManSimProfile( p );
-    pGia  = Gia_ManSimPatGenMiter( p, vSims );
-    vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 );
-    Gia_ManStop( pGia );
-    Vec_StrForEachEntry( vStatus, Status, i )
-    {
-        assert( Status >= -1 && Status <= 1 );
-        Counts[Status+1]++;
-    }
-    printf( "Total = %d : SAT = %d.  UNSAT = %d.  UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
-    if ( Counts[1] == 0 )
-        printf( "There are no counter-examples.  No need for more simulation.\n" );
-    else
-    {
-        vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1] );
-        Vec_WrdFreeP( &p->vSimsPi );
-        p->vSimsPi = vSimsIn;
-        Gia_ManSimProfile( p );
-    }
-    Vec_StrFree( vStatus );
-    Vec_IntFree( vCexStore );
-    Vec_WrdFree( vSims );
-}
-
-
-
-
-
-typedef struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t;
-struct Gia_SimRsbMan_t_
-{
-    Gia_Man_t *    pGia;
-    Vec_Int_t *    vTfo;
-    Vec_Int_t *    vCands;
-    Vec_Int_t *    vFanins;
-    Vec_Int_t *    vFanins2;
-    Vec_Wrd_t *    vSimsObj;
-    Vec_Wrd_t *    vSimsObj2;
-    int            nWords;
-    word *         pFunc[3];
-};
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_SimRsbMan_t * Gia_SimRsbAlloc( Gia_Man_t * pGia )
-{
-    Gia_SimRsbMan_t * p = ABC_CALLOC( Gia_SimRsbMan_t, 1 );
-    p->pGia      = pGia;
-    p->nWords    = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
-    p->pFunc[0]  = ABC_CALLOC( word, p->nWords );
-    p->pFunc[1]  = ABC_CALLOC( word, p->nWords );
-    p->pFunc[2]  = ABC_CALLOC( word, p->nWords );
-    p->vTfo      = Vec_IntAlloc( 1000 );
-    p->vCands    = Vec_IntAlloc( 1000 );
-    p->vFanins   = Vec_IntAlloc( 10 );
-    p->vFanins2  = Vec_IntAlloc( 10 );
-    p->vSimsObj  = Gia_ManSimPatSim( pGia );
-    p->vSimsObj2 = Vec_WrdStart( Vec_WrdSize(p->vSimsObj) );
-    assert( p->nWords == Vec_WrdSize(p->vSimsObj) / Gia_ManObjNum(pGia) );
-    Gia_ManStaticFanoutStart( pGia );
-    return p;
-}
-void Gia_SimRsbFree( Gia_SimRsbMan_t * p )
-{
-    Gia_ManStaticFanoutStop( p->pGia );
-    Vec_IntFree( p->vTfo );
-    Vec_IntFree( p->vCands );
-    Vec_IntFree( p->vFanins );
-    Vec_IntFree( p->vFanins2 );
-    Vec_WrdFree( p->vSimsObj );
-    Vec_WrdFree( p->vSimsObj2 );
-    ABC_FREE( p->pFunc[0] );
-    ABC_FREE( p->pFunc[1] );
-    ABC_FREE( p->pFunc[2] );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SimRsbTfo_rec( Gia_Man_t * p, int iObj, int iFanout, Vec_Int_t * vTfo )
-{
-    int i, iFan;
-    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
-        return;
-    Gia_ObjSetTravIdCurrentId(p, iObj);
-    Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i )
-        if ( iFanout == -1 || iFan == iFanout )
-            Gia_SimRsbTfo_rec( p, iFan, -1, vTfo );
-    Vec_IntPush( vTfo, iObj );
-}
-Vec_Int_t * Gia_SimRsbTfo( Gia_SimRsbMan_t * p, int iObj, int iFanout )
-{
-    assert( iObj > 0 );
-    Vec_IntClear( p->vTfo );
-    Gia_ManIncrementTravId( p->pGia );
-    Gia_SimRsbTfo_rec( p->pGia, iObj, iFanout, p->vTfo );
-    assert( Vec_IntEntryLast(p->vTfo) == iObj );
-    Vec_IntPop( p->vTfo );
-    Vec_IntReverseOrder( p->vTfo );
-    Vec_IntSort( p->vTfo, 0 );
-    return p->vTfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-word * Gia_SimRsbFunc( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins, int fOnSet )
-{
-    int nTruthWords = Abc_Truth6WordNum( Vec_IntSize(vFanins) );
-    word * pTruth   = ABC_CALLOC( word, nTruthWords ); 
-    word * pFunc    = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
-    word * pFanins[16] = {NULL};  int s, b, iMint, i, iFanin;
-    assert( Vec_IntSize(vFanins) <= 16 );
-    Vec_IntForEachEntry( vFanins, iFanin, i )
-        pFanins[i] = Vec_WrdEntryP( p->vSimsObj, p->nWords*iFanin );
-    for ( s = 0; s < 64*p->nWords; s++ )
-    {
-        if ( !Abc_TtGetBit(p->pFunc[2], s) || Abc_TtGetBit(pFunc, s) != fOnSet )
-            continue;
-        iMint = 0;
-        for ( b = 0; b < Vec_IntSize(vFanins); b++ )
-            if ( Abc_TtGetBit(pFanins[b], s) )
-                iMint |= 1 << b;
-        Abc_TtSetBit( pTruth, iMint );
-    }
-    return pTruth;
-}
-int Gia_SimRsbResubVerify( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins )
-{
-    word * pTruth0 = Gia_SimRsbFunc( p, iObj, p->vFanins, 0 );
-    word * pTruth1 = Gia_SimRsbFunc( p, iObj, p->vFanins, 1 );
-    int Res = !Abc_TtIntersect( pTruth0, pTruth1, p->nWords, 0 );
-    ABC_FREE( pTruth0 );
-    ABC_FREE( pTruth1 );
-    return Res;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Gia_SimRsbSimAndCareSet( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2 )
-{
-    word pComps[2] = { 0, ~(word)0 };
-    word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
-    word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
-    Vec_Wrd_t * vSims0 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ? vSims2 : vSims;
-    Vec_Wrd_t * vSims1 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ? vSims2 : vSims;
-    word * pSims0 = Vec_WrdEntryP( vSims0, nWords*Gia_ObjFaninId0(pObj, i) );
-    word * pSims1 = Vec_WrdEntryP( vSims1, nWords*Gia_ObjFaninId1(pObj, i) );
-    word * pSims2 = Vec_WrdEntryP( vSims2, nWords*i ); int w;
-    for ( w = 0; w < nWords; w++ )
-        pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1);
-}
-word * Gia_SimRsbCareSet( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vTfo )
-{
-    word * pSims  = Vec_WrdEntryP( p->vSimsObj,  p->nWords*iObj );
-    word * pSims2 = Vec_WrdEntryP( p->vSimsObj2, p->nWords*iObj );  int iNode, i;
-    Abc_TtCopy( pSims2, pSims, p->nWords, 1 );
-    Abc_TtClear( p->pFunc[2], p->nWords );
-    Vec_IntForEachEntry( vTfo, iNode, i )
-    {
-        Gia_Obj_t * pNode = Gia_ManObj(p->pGia, iNode);
-        if ( Gia_ObjIsAnd(pNode) )
-            Gia_SimRsbSimAndCareSet( p->pGia, iNode, pNode, p->nWords, p->vSimsObj, p->vSimsObj2 );
-        else if ( Gia_ObjIsCo(pNode) )
-        {
-            word * pSimsA = Vec_WrdEntryP( p->vSimsObj,  p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) );
-            word * pSimsB = Vec_WrdEntryP( p->vSimsObj2, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) );
-            Abc_TtOrXor( p->pFunc[2], pSimsA, pSimsB, p->nWords );
-        }
-        else assert( 0 );
-    }
-    return p->pFunc[2];
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ObjSimCollect( Gia_SimRsbMan_t * p )
-{
-    int i, k, iTemp, iFanout;
-    Vec_IntClear( p->vFanins2 );
-    assert( Vec_IntSize(p->vFanins) > 0 );
-    Vec_IntForEachEntry( p->vFanins, iTemp, i )
-    {
-        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iTemp );
-        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId0(pObj, iTemp) ) )
-            Vec_IntPush( p->vFanins2, Gia_ObjFaninId0(pObj, iTemp) );
-        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId1(pObj, iTemp) ) )
-            Vec_IntPush( p->vFanins2, Gia_ObjFaninId1(pObj, iTemp) );
-        Gia_ObjForEachFanoutStaticId( p->pGia, iTemp, iFanout, k )
-            if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanout)) && !Gia_ObjIsTravIdCurrentId( p->pGia, iFanout ) )
-                Vec_IntPush( p->vFanins2, iFanout );
-    }
-}
-Vec_Int_t * Gia_ObjSimCands( Gia_SimRsbMan_t * p, int iObj, int nCands )
-{
-    assert( iObj > 0 );
-    assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) );
-    Vec_IntClear( p->vCands );
-    Vec_IntFill( p->vFanins, 1, iObj );
-    while ( Vec_IntSize(p->vFanins) > 0 && Vec_IntSize(p->vCands) < nCands )
-    {
-        int i, iTemp;
-        Vec_IntForEachEntry( p->vFanins, iTemp, i )
-            Gia_ObjSetTravIdCurrentId( p->pGia, iTemp );
-        Gia_ObjSimCollect( p ); // p->vFanins -> p->vFanins2
-        Vec_IntAppend( p->vCands, p->vFanins2 );
-        ABC_SWAP( Vec_Int_t *, p->vFanins, p->vFanins2 );
-    }
-    assert( Vec_IntSize(p->vFanins) == 0 || Vec_IntSize(p->vCands) >= nCands );
-    if ( Vec_IntSize(p->vCands) > nCands )
-        Vec_IntShrink( p->vCands, nCands );
-    return p->vCands;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ObjSimRsb( Gia_SimRsbMan_t * p, int iObj, int nCands, int fVerbose, int * pnBufs, int * pnInvs )
-{
-    int i, iCand, RetValue = 0;
-    Vec_Int_t * vTfo   = Gia_SimRsbTfo( p, iObj, -1 );
-    word * pCareSet    = Gia_SimRsbCareSet( p, iObj, vTfo );
-    word * pFunc       = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
-    Vec_Int_t * vCands = Gia_ObjSimCands( p, iObj, nCands );
-    Abc_TtAndSharp( p->pFunc[0], pCareSet, pFunc, p->nWords, 1 );
-    Abc_TtAndSharp( p->pFunc[1], pCareSet, pFunc, p->nWords, 0 );
-
-/*
-printf( "Considering node %d with %d candidates:\n", iObj, Vec_IntSize(vCands) );
-Vec_IntPrint( vTfo );
-Vec_IntPrint( vCands );
-Extra_PrintBinary( stdout, (unsigned *)pCareSet,    64 );  printf( "\n" );
-Extra_PrintBinary( stdout, (unsigned *)pFunc,       64 );  printf( "\n" );
-Extra_PrintBinary( stdout, (unsigned *)p->pFunc[0], 64 );  printf( "\n" );
-Extra_PrintBinary( stdout, (unsigned *)p->pFunc[1], 64 );  printf( "\n" );
-*/
-    Vec_IntForEachEntry( vCands, iCand, i )
-    {
-        word * pDiv = Vec_WrdEntryP( p->vSimsObj, p->nWords*iCand );
-        if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 0) &&
-             !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 1) )
-            { (*pnBufs)++; if ( fVerbose ) printf( "Level %3d : %d = buf(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; }
-        if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 1) &&
-             !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 0) )
-            { (*pnInvs)++; if ( fVerbose ) printf( "Level %3d : %d = inv(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; }
-    }
-    return RetValue;
-}
-
-int Gia_ManSimRsb( Gia_Man_t * pGia, int nCands, int fVerbose )
-{
-    abctime clk = Abc_Clock();
-    Gia_Obj_t * pObj; int iObj, nCount = 0, nBufs = 0, nInvs = 0;
-    Gia_SimRsbMan_t * p = Gia_SimRsbAlloc( pGia );
-    assert( pGia->vSimsPi != NULL );
-    Gia_ManLevelNum( pGia );
-    Gia_ManForEachAnd( pGia, pObj, iObj )
-        //if ( iObj == 6 )
-        nCount += Gia_ObjSimRsb( p, iObj, nCands, fVerbose, &nBufs, &nInvs );
-    printf( "Can resubstitute %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d)  ", 
-        nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    Gia_SimRsbFree( p );
-    return nCount;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////