giaGiarf.c

Go to the documentation of this file.

 
#include "gia.h"
 
ABC_NAMESPACE_IMPL_START

 
// combinational simulation manager
typedef struct Hcd_Man_t_ Hcd_Man_t;
struct Hcd_Man_t_
{
    // parameters
    Gia_Man_t *      pGia;           // the AIG to be used for simulation
    int              nBTLimit;       // internal backtrack limit 
    int              fVerbose;       // internal verbose flag 
    // internal variables
    unsigned *       pSimInfo;       // simulation info for each object
    Vec_Ptr_t *      vSimInfo;       // pointers to the CI simulation info
    Vec_Ptr_t *      vSimPres;       // pointers to the presense of simulation info
    // temporaries
    Vec_Int_t *      vClassOld;      // old class numbers
    Vec_Int_t *      vClassNew;      // new class numbers
    Vec_Int_t *      vClassTemp;     // temporary storage
    Vec_Int_t *      vRefinedC;      // refined const reprs
};
 
static inline unsigned   Hcd_ObjSim( Hcd_Man_t * p, int Id )                  { return p->pSimInfo[Id];      }
static inline unsigned * Hcd_ObjSimP( Hcd_Man_t * p, int Id )                 { return p->pSimInfo + Id;     }
static inline unsigned   Hcd_ObjSetSim( Hcd_Man_t * p, int Id, unsigned n )   { return p->pSimInfo[Id] = n;  }


Hcd_Man_t * Gia_ManEquivStart( Gia_Man_t * pGia, int nBTLimit, int fVerbose )
{
    Hcd_Man_t * p;
    Gia_Obj_t * pObj;
    int i;
    p = ABC_CALLOC( Hcd_Man_t, 1 );
    p->pGia       = pGia;
    p->nBTLimit   = nBTLimit;
    p->fVerbose   = fVerbose;
    p->pSimInfo   = ABC_ALLOC( unsigned, Gia_ManObjNum(pGia) );
    p->vClassOld  = Vec_IntAlloc( 100 );
    p->vClassNew  = Vec_IntAlloc( 100 );
    p->vClassTemp = Vec_IntAlloc( 100 );
    p->vRefinedC  = Vec_IntAlloc( 100 );
    // collect simulation info
    p->vSimInfo = Vec_PtrAlloc( 1000 );
    Gia_ManForEachCi( pGia, pObj, i )
        Vec_PtrPush( p->vSimInfo, Hcd_ObjSimP(p, Gia_ObjId(pGia,pObj)) );
    p->vSimPres = Vec_PtrAllocSimInfo( Gia_ManCiNum(pGia), 1 );
    return p;
}

void Gia_ManEquivStop( Hcd_Man_t * p )
{
    Vec_PtrFree( p->vSimInfo );
    Vec_PtrFree( p->vSimPres );
    Vec_IntFree( p->vClassOld );
    Vec_IntFree( p->vClassNew );
    Vec_IntFree( p->vClassTemp );
    Vec_IntFree( p->vRefinedC );
    ABC_FREE( p->pSimInfo );
    ABC_FREE( p );
}
 

static inline int Hcd_ManCompareEqual( unsigned s0, unsigned s1 )
{
    if ( (s0 & 1) == (s1 & 1) )
        return s0 == s1;
    else
        return s0 ==~s1;
}

static inline int Hcd_ManCompareConst( unsigned s )
{
    if ( s & 1 )
        return s ==~0;
    else
        return s == 0;
}

void Hcd_ManClassCreate( Gia_Man_t * pGia, 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;
            Gia_ObjSetRepr( pGia, Ent, -1 );
            EntPrev = Ent;
        }
        else
        {
            Gia_ObjSetRepr( pGia, Ent, Repr );
            Gia_ObjSetNext( pGia, EntPrev, Ent );
            EntPrev = Ent;
        }
    }
    Gia_ObjSetNext( pGia, EntPrev, 0 );
}

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

int Hcd_ManClassRefineOne( Hcd_Man_t * p, int i )
{
    unsigned Sim0, Sim1;
    int Ent;
    Vec_IntClear( p->vClassOld );
    Vec_IntClear( p->vClassNew );
    Vec_IntPush( p->vClassOld, i );
    Sim0 = Hcd_ObjSim(p, i);
    Gia_ClassForEachObj1( p->pGia, i, Ent )
    {
        Sim1 = Hcd_ObjSim(p, Ent);
        if ( Hcd_ManCompareEqual( Sim0, Sim1 ) )
            Vec_IntPush( p->vClassOld, Ent );
        else
            Vec_IntPush( p->vClassNew, Ent );
    }
    if ( Vec_IntSize( p->vClassNew ) == 0 )
        return 0;
    Hcd_ManClassCreate( p->pGia, p->vClassOld );
    Hcd_ManClassCreate( p->pGia, p->vClassNew );
    if ( Vec_IntSize(p->vClassNew) > 1 )
        return 1 + Hcd_ManClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
    return 1;
}

int Hcd_ManHashKey( 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);
 
}

void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined )
{
    int * pTable, nTableSize, Key, i, k;
    nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
    pTable = ABC_CALLOC( int, nTableSize );
    Vec_IntForEachEntry( vRefined, i, k )
    {
        assert( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) );
        Key = Hcd_ManHashKey( Hcd_ObjSimP(p, i), 1, nTableSize );
        if ( pTable[Key] == 0 )
            Gia_ObjSetRepr( p->pGia, i, GIA_VOID );
        else
        {
            Gia_ObjSetNext( p->pGia, pTable[Key], i );
            Gia_ObjSetRepr( p->pGia, i, Gia_ObjRepr(p->pGia, pTable[Key]) );
            if ( Gia_ObjRepr(p->pGia, i) == GIA_VOID )
                Gia_ObjSetRepr( p->pGia, i, pTable[Key] );
        }
        pTable[Key] = i;
    }
    ABC_FREE( pTable );
//    Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 );
    // refine classes in the table
    Vec_IntForEachEntry( vRefined, i, k )
    {
        if ( Gia_ObjIsHead( p->pGia, i ) )
            Hcd_ManClassRefineOne( p, i );
    }
    Gia_ManEquivPrintClasses( p->pGia, 0, 0.0 );
}

void Hcd_ManClassesRefine( Hcd_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    Vec_IntClear( p->vRefinedC );
    Gia_ManForEachAnd( p->pGia, pObj, i )
    {
        if ( Gia_ObjIsTail(p->pGia, i) ) // add check for the class level
        {
            Hcd_ManClassRefineOne( p, Gia_ObjRepr(p->pGia, i) );
        }
        else if ( Gia_ObjIsConst(p->pGia, i) )
        {
            if ( !Hcd_ManCompareConst( Hcd_ObjSim(p, i) ) )
                Vec_IntPush( p->vRefinedC, i );
        }
    }
    Hcd_ManClassesRehash( p, p->vRefinedC );
}

void Hcd_ManClassesCreate( Hcd_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    assert( p->pGia->pReprs == NULL );
    p->pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pGia) );
    p->pGia->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pGia) );
    Gia_ManForEachObj( p->pGia, pObj, i )
        Gia_ObjSetRepr( p->pGia, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
}

void Hcd_ManSimulationInit( Hcd_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachCi( p->pGia, pObj, i )
        Hcd_ObjSetSim( p, i, (Gia_ManRandom(0) << 1) );
}

void Hcd_ManSimulateSimple( Hcd_Man_t * p )
{
    Gia_Obj_t * pObj;
    unsigned Res0, Res1;
    int i;
    Gia_ManForEachAnd( p->pGia, pObj, i )
    {
        Res0 = Hcd_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
        Res1 = Hcd_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
        Hcd_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
                             (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
    }
}
 

unsigned Gia_Resimulate_rec( Hcd_Man_t * p, int iObj )
{
    Gia_Obj_t * pObj;
    unsigned Res0, Res1;
    if ( Gia_ObjIsTravIdCurrentId( p->pGia, iObj ) )
        return Hcd_ObjSim( p, iObj );
    Gia_ObjSetTravIdCurrentId( p->pGia, iObj );
    pObj = Gia_ManObj(p->pGia, iObj);
    if ( Gia_ObjIsCi(pObj) )
        return Hcd_ObjSim( p, iObj );
    assert( Gia_ObjIsAnd(pObj) );
    Res0 = Gia_Resimulate_rec( p, Gia_ObjFaninId0(pObj, iObj) );
    Res1 = Gia_Resimulate_rec( p, Gia_ObjFaninId1(pObj, iObj) );
    return Hcd_ObjSetSim( p, iObj, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
                                   (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
}

void Gia_ResimulateAndRefine( Hcd_Man_t * p, int i )
{
    int RetValue, iObj;
    Gia_ManIncrementTravId( p->pGia );
    Gia_ClassForEachObj( p->pGia, i, iObj )
        Gia_Resimulate_rec( p, iObj );
    RetValue = Hcd_ManClassRefineOne( p, i );
    if ( RetValue == 0 )
        printf( "!!! no refinement !!!\n" );
//    assert( RetValue );
}

static inline Gia_Obj_t * Gia_ObjTempRepr( Gia_Man_t * p, int i, int Level )
{
    int iRepr, iMember;
    iRepr = Gia_ObjRepr( p, i ); 
    if ( !Gia_ObjProved(p, i) )
        return NULL;
    if ( Gia_ObjFailed(p, i) )
        return NULL;
    if ( iRepr == GIA_VOID )
        return NULL;
    if ( iRepr == 0 )
        return Gia_ManConst0( p );
//    if ( p->pLevels[iRepr] < Level )
//        return Gia_ManObj( p, iRepr );
    Gia_ClassForEachObj( p, iRepr, iMember )
    {
        if ( Gia_ObjFailed(p, iMember) )
            continue;
        if ( iMember >= i )
            return NULL;
        if ( Gia_ObjLevelId(p, iMember) < Level )
            return Gia_ManObj( p, iMember );
    }
    assert( 0 );
    return NULL;
}

Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvRoots )
{
    Gia_Man_t * pNew;
    Gia_Obj_t * pObj, * pRepr;
    Vec_Ptr_t * vRoots;
    int i;
    vRoots = Vec_PtrAlloc( 100 );
    // copy unmarked nodes
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    Gia_ManHashAlloc( pNew );
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( Gia_ObjLevelId(p, i) > Level )
            continue;
        if ( Gia_ObjLevelId(p, i) == Level )
            Vec_PtrPush( vRoots, pObj );
        if ( Gia_ObjLevelId(p, i) < Level && (pRepr = Gia_ObjTempRepr(p, i, Level)) )
        {
//            printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) ); 
            assert( pRepr < pObj );
            pObj->Value  = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
            continue;
        }
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    }
    *pvRoots = vRoots;
    // required by SAT solving
    Gia_ManCreateRefs( pNew );
    Gia_ManFillValue( pNew );
    Gia_ManIncrementTravId( pNew ); // needed for MiniSat to record cexes
//    Gia_ManSetPhase( pNew ); // needed if MiniSat is using polarity -- should not be enabled for TAS because fPhase is used to label
    return pNew;
}

Vec_Ptr_t * Gia_CollectRelatedClasses( Gia_Man_t * pGia, Vec_Ptr_t * vRoots )
{
    Vec_Ptr_t * vClasses;
    Gia_Obj_t * pRoot, * pRepr;
    int i;
    vClasses = Vec_PtrAlloc( 100 );
    Gia_ManConst0( pGia )->fMark0 = 1;
    Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pRoot, i )
    {
        pRepr = Gia_ObjReprObj( pGia, Gia_ObjId(pGia, pRoot) );
        if ( pRepr == NULL || pRepr->fMark0 )
            continue;
        pRepr->fMark0 = 1;
        Vec_PtrPush( vClasses, pRepr );
    }
    Gia_ManConst0( pGia )->fMark0 = 0;
    Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i )
        pRepr->fMark0 = 0;
    return vClasses;
}

Gia_Obj_t * Gia_CollectClassMembers( Gia_Man_t * p, Gia_Obj_t * pRepr, Vec_Ptr_t * vMembers, int Level )
{
    Gia_Obj_t * pTempRepr = NULL;
    int iRepr, iMember;
    iRepr = Gia_ObjId( p, pRepr );
    Vec_PtrClear( vMembers );
    Gia_ClassForEachObj( p, iRepr, iMember )
    {
        if ( Gia_ObjLevelId(p, iMember) == Level )
            Vec_PtrPush( vMembers, Gia_ManObj( p, iMember ) );
        if ( pTempRepr == NULL && Gia_ObjLevelId(p, iMember) < Level )
            pTempRepr = Gia_ManObj( p, iMember );
    }
    return pTempRepr;
}
 

int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
{
    unsigned * pInfo, * pPres;
    int i;
    for ( i = 0; i < nLits; i++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
        if ( Abc_InfoHasBit( pPres, iBit ) && 
             Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
             return 0;
    }
    for ( i = 0; i < nLits; i++ )
    {
        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
        Abc_InfoSetBit( pPres, iBit );
        if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
            Abc_InfoXorBit( pInfo, iBit );
    }
    return 1;
}

int Gia_GiarfStorePattern( Vec_Ptr_t * vSimInfo, Vec_Ptr_t * vPres, Vec_Int_t * vCex )
{
    int k;
    for ( k = 1; k < 32; k++ )
        if ( Gia_GiarfStorePatternTry( vSimInfo, vPres, k, (int *)Vec_IntArray(vCex), Vec_IntSize(vCex) ) )
            break;
    return (int)(k < 32);
}

void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k )
{
    Gia_Obj_t * pObj;
    unsigned * pInfo;
    int Lit, i;
    Vec_IntForEachEntry( vCex, Lit, i )
    {
        pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) );
        pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) );
        if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) )
            Abc_InfoXorBit( pInfo, k );
    }
}

void Gia_GiarfPrintClasses( Gia_Man_t * pGia )
{
    int nFails  = 0;
    int nProves = 0;
    int nTotal  = 0;
    int nBoth   = 0;
    int i;
    for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
    {
        nFails  += Gia_ObjFailed(pGia, i);
        nProves += Gia_ObjProved(pGia, i);
        nTotal  += Gia_ObjReprObj(pGia, i) != NULL;
        nBoth   += Gia_ObjFailed(pGia, i) && Gia_ObjProved(pGia, i);
    }
    printf( "nFails = %7d.  nProves = %7d.  nBoth = %7d.  nTotal = %7d.\n", 
        nFails, nProves, nBoth, nTotal );
}
 
ABC_NAMESPACE_IMPL_END
 
#include "proof/cec/cecInt.h"
 
ABC_NAMESPACE_IMPL_START
 

int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t * vOldRoots, int Level, int fUseMiniSat )
{
    int fUse2Solver = 0;
    Cec_ManSat_t * pSat;
    Cec_ParSat_t Pars;
    Tas_Man_t * pTas;
    Vec_Int_t * vCex;
    Vec_Ptr_t * vClasses, * vMembers, * vOldRootsNew;
    Gia_Obj_t * pRoot, * pMember, * pMemberPrev, * pRepr, * pTempRepr;
    int i, k, nIter, iRoot, iRootNew, iMember, iMemberPrev, status, fOneFailed;//, iRepr;//, fTwoMember;
    int nSaved = 0, nRecords = 0, nUndec = 0, nClassRefs = 0, nTsat = 0, nMiniSat = 0;
    clock_t clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock();
    if ( Vec_PtrSize(vOldRoots) == 0 )
        return 0;
    // start SAT solvers
    Cec_ManSatSetDefaultParams( &Pars );
    Pars.fPolarFlip = 0;
    Pars.nBTLimit   = p->nBTLimit;
    pSat = Cec_ManSatCreate( pGiaLev, &Pars );
    pTas = Tas_ManAlloc( pGiaLev, p->nBTLimit );
    if ( fUseMiniSat )
        vCex = Cec_ManSatReadCex( pSat );
    else
        vCex = Tas_ReadModel( pTas );
    vMembers = Vec_PtrAlloc( 100 );
    Vec_PtrCleanSimInfo( p->vSimPres, 0, 1 );
    // resolve constants
    Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i )
    {
        iRoot = Gia_ObjId( p->pGia, pRoot );
        if ( !Gia_ObjIsConst( p->pGia, iRoot ) )
            continue;
        iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase );
        assert( iRootNew != 1 );
        if ( fUse2Solver )
        {
            nTsat++;
           clk = clock();
            status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
           timeTsat += clock() - clk;
            if ( status == -1 )
            {
                nMiniSat++;
               clk = clock();
                status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) );
               timeMiniSat += clock() - clk;
                if ( status == 0 )
                {
                    Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
                    vCex = Cec_ManSatReadCex( pSat );
                }
            }
            else if ( status == 0 )
                vCex = Tas_ReadModel( pTas );
        }
        else if ( fUseMiniSat )
        {
            nMiniSat++;
           clk = clock();
            status = Cec_ManSatCheckNode( pSat, Gia_ObjFromLit(pGiaLev, iRootNew) );
           timeMiniSat += clock() - clk;
            if ( status == 0 )
                Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
        }
        else
        {
            nTsat++;
           clk = clock();
            status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iRootNew), NULL );
           timeTsat += clock() - clk;
        }
        if ( status == -1 ) // undec
        {
//            Gia_ObjSetFailed( p->pGia, iRoot );
            nUndec++;
//            Hcd_ManClassClassRemoveOne( p, iRoot );
            Gia_ObjSetFailed( p->pGia, iRoot );
        }
        else if ( status == 1 ) // unsat
        {
            Gia_ObjSetProved( p->pGia, iRoot );
//            printf( "proved constant %d\n", iRoot );
        }
        else  // sat
        {
//            printf( "Disproved constant %d\n", iRoot );
            Gia_ObjUnsetRepr( p->pGia, iRoot ); // do we need this?
            nRecords++;
            nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex );
        }
    }
 
    vClasses = Vec_PtrAlloc( 100 );
    vOldRootsNew = Vec_PtrAlloc( 100 );
    for ( nIter = 0; Vec_PtrSize(vOldRoots) > 0; nIter++ )
    {
//        printf( "Iter = %d  (Size = %d)\n", nIter, Vec_PtrSize(vOldRoots) );
        // resolve equivalences 
        Vec_PtrClear( vClasses );
        Vec_PtrClear( vOldRootsNew );
        Gia_ManConst0( p->pGia )->fMark0 = 1;
        Vec_PtrForEachEntry( Gia_Obj_t *, vOldRoots, pRoot, i )
        {
            iRoot = Gia_ObjId( p->pGia, pRoot );
            if ( Gia_ObjIsHead( p->pGia, iRoot ) )
                pRepr = pRoot;
            else if ( Gia_ObjIsClass( p->pGia, iRoot ) )
                pRepr = Gia_ObjReprObj( p->pGia, iRoot );
            else
                continue;
            if ( pRepr->fMark0 )
                continue;
            pRepr->fMark0 = 1;
            Vec_PtrPush( vClasses, pRepr );
//            iRepr = Gia_ObjId( p->pGia, pRepr );
//            fTwoMember = Gia_ClassIsPair(p->pGia, iRepr)
            // derive temp repr and members on this level
            pTempRepr = Gia_CollectClassMembers( p->pGia, pRepr, vMembers, Level );
            if ( pTempRepr )
                Vec_PtrPush( vMembers, pTempRepr );
            if ( Vec_PtrSize(vMembers) < 2 )
                continue;
            // try proving the members
            fOneFailed = 0;
            pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers );
            Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
            {
                iMemberPrev = Abc_LitNotCond( pMemberPrev->Value,  pMemberPrev->fPhase ); 
                iMember     = Abc_LitNotCond( pMember->Value,     !pMember->fPhase ); 
                assert( iMemberPrev != iMember );
                if ( fUse2Solver )
                {
                    nTsat++;
                   clk = clock();
                    status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
                   timeTsat += clock() - clk;
                    if ( status == -1 )
                    {
                        nMiniSat++;
                       clk = clock();
                        status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
                       timeMiniSat += clock() - clk;
                        if ( status == 0 )
                        {
                            Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
                            vCex = Cec_ManSatReadCex( pSat );
                        }
                    }
                    else if ( status == 0 )
                        vCex = Tas_ReadModel( pTas );
                }
                else if ( fUseMiniSat )
                {
                    nMiniSat++;
                   clk = clock();
                    status = Cec_ManSatCheckNodeTwo( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
                   timeMiniSat += clock() - clk;
                    if ( status == 0 )
                        Cec_ManSavePattern( pSat, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
                }
                else
                {
                    nTsat++;
                   clk = clock();
                    status = Tas_ManSolve( pTas, Gia_ObjFromLit(pGiaLev, iMemberPrev), Gia_ObjFromLit(pGiaLev, iMember) );
                   timeTsat += clock() - clk;
                }
                if ( status == -1 ) // undec
                {
//                    Gia_ObjSetFailed( p->pGia, iRoot );
                    nUndec++;
                    if ( Gia_ObjLevel(p->pGia, pMemberPrev) > Gia_ObjLevel(p->pGia, pMember) )
                    {
//                        Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMemberPrev) );
                        Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) );
                        Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) );
                    }
                    else
                    {
//                        Hcd_ManClassClassRemoveOne( p, Gia_ObjId(p->pGia, pMember) );
                        Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMemberPrev) );
                        Gia_ObjSetFailed( p->pGia, Gia_ObjId(p->pGia, pMember) );
                    }
                }
                else if ( status == 1 ) // unsat
                {
//                    Gia_ObjSetProved( p->pGia, iRoot );
                }
                else  // sat
                {
//                    iRepr = Gia_ObjId( p->pGia, pRepr );
//                    if ( Gia_ClassIsPair(p->pGia, iRepr) )
//                        Gia_ClassUndoPair(p->pGia, iRepr);
//                    else
                    {
                        fOneFailed = 1;
                        nRecords++;
                        nSaved += Gia_GiarfStorePattern( p->vSimInfo, p->vSimPres, vCex );
                        Gia_GiarfInsertPattern( p, vCex, (k % 31) + 1 );
                    }
                }
                pMemberPrev = pMember;
//                if ( fOneFailed )
//                    k += Vec_PtrSize(vMembers) / 4;
            }
            // if fail, quit this class
            if ( fOneFailed )
            {
                nClassRefs++;
                Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
                    if ( pMember != pTempRepr && !Gia_ObjFailed(p->pGia, Gia_ObjId(p->pGia, pMember)) )
                        Vec_PtrPush( vOldRootsNew, pMember );
                clk = clock();
                Gia_ResimulateAndRefine( p, Gia_ObjId(p->pGia, pRepr) );
                timeSim += clock() - clk;
            }
            else
            {
                Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
                    Gia_ObjSetProved( p->pGia, Gia_ObjId(p->pGia, pMember) );
/*
//            }
//            else
//            {
                printf( "Proved equivalent: " );
                Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
                    printf( "%d(L=%d)  ", Gia_ObjId(p->pGia, pMember), p->pGia->pLevels[Gia_ObjId(p->pGia, pMember)] );
                printf( "\n" );
*/
            }
 
        }
        Vec_PtrClear( vOldRoots );
        Vec_PtrForEachEntry( Gia_Obj_t *, vOldRootsNew, pMember, i )
            Vec_PtrPush( vOldRoots, pMember );
        // clean up
        Gia_ManConst0( p->pGia )->fMark0 = 0;
        Vec_PtrForEachEntry( Gia_Obj_t *, vClasses, pRepr, i )
            pRepr->fMark0 = 0;
    }
    Vec_PtrFree( vClasses );
    Vec_PtrFree( vOldRootsNew );
    printf( "nSaved = %d   nRecords = %d   nUndec = %d   nClassRefs = %d   nMiniSat = %d   nTas = %d\n", 
        nSaved, nRecords, nUndec, nClassRefs, nMiniSat, nTsat );
    ABC_PRT( "Tas    ",  timeTsat );
    ABC_PRT( "MiniSat",  timeMiniSat );
    ABC_PRT( "Sim    ",  timeSim );
    ABC_PRT( "Total  ",  clock() - timeTotal );
 
    // resimulate
//    clk = clock();
    Hcd_ManSimulateSimple( p );
    Hcd_ManClassesRefine( p );
//    ABC_PRT( "Simulate/refine", clock() - clk );
 
    // verify the results
    Vec_PtrFree( vMembers );
    Tas_ManStop( pTas );
    Cec_ManSatStop( pSat );
    return nIter;
}

void Gia_ComputeEquivalences( Gia_Man_t * pGia, int nBTLimit, int fUseMiniSat, int fVerbose )
{
    Hcd_Man_t * p;
    Vec_Ptr_t * vRoots;
    Gia_Man_t * pGiaLev;
    int i, Lev, nLevels, nIters;
    clock_t clk;
    Gia_ManRandom( 1 );
    Gia_ManSetPhase( pGia );
    nLevels = Gia_ManLevelNum( pGia );
    Gia_ManIncrementTravId( pGia );
    // start the manager
    p = Gia_ManEquivStart( pGia, nBTLimit, fVerbose );
    // create trivial classes
    Hcd_ManClassesCreate( p );
    // refine
    for ( i = 0; i < 3; i++ )
    {
        clk = clock();       
        Hcd_ManSimulationInit( p );
        Hcd_ManSimulateSimple( p );
        ABC_PRT( "Sim", clock() - clk );
        clk = clock();
        Hcd_ManClassesRefine( p );
        ABC_PRT( "Ref", clock() - clk );
    }
    // process in the levelized order
    for ( Lev = 1; Lev < nLevels; Lev++ )
    {
        clk = clock();
        printf( "LEVEL %3d  (out of %3d)   ", Lev, nLevels );
        pGiaLev = Gia_GenerateReducedLevel( pGia, Lev, &vRoots );
        nIters = Gia_ComputeEquivalencesLevel( p, pGiaLev, vRoots, Lev, fUseMiniSat );
        Gia_ManStop( pGiaLev );
        Vec_PtrFree( vRoots );
        printf( "Iters = %3d   " );
        ABC_PRT( "Time", clock() - clk );
    }
    Gia_GiarfPrintClasses( pGia );
    // clean up
    Gia_ManEquivStop( p );
}

 
 
ABC_NAMESPACE_IMPL_END