abcDetect.c

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

  FileName    [abcDetect.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Detect conditions.]

  Author      [Alan Mishchenko, Dao Ai Quoc]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 7, 2016.]

  Revision    [$Id: abcDetect.c,v 1.00 2016/06/07 00:00:00 alanmi Exp $]

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

#include "base/abc/abc.h"
#include "misc/vec/vecHsh.h"
#include "misc/util/utilNam.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "map/mio/mio.h"
#include "map/mio/exp.h"

ABC_NAMESPACE_IMPL_START

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

typedef enum { 
    ABC_FIN_NONE = -100,   //  0:  unknown
    ABC_FIN_SA0,           //  1:
    ABC_FIN_SA1,           //  2:
    ABC_FIN_NEG,           //  3:
    ABC_FIN_RDOB_AND,      //  4:
    ABC_FIN_RDOB_NAND,     //  5:
    ABC_FIN_RDOB_OR,       //  6:
    ABC_FIN_RDOB_NOR,      //  7:
    ABC_FIN_RDOB_XOR,      //  8:
    ABC_FIN_RDOB_NXOR,     //  9:
    ABC_FIN_RDOB_NOT,      // 10:
    ABC_FIN_RDOB_BUFF,     // 11:
    ABC_FIN_RDOB_LAST      // 12:
} Abc_FinType_t;

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

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

  Synopsis    [Generates fault list for the given mapped network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt )
{
    Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
    Mio_Gate_t * pGate;
    Abc_Obj_t * pObj;
    int i, Count = 1;
    FILE * pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
        return;
    }
    assert( Abc_NtkIsMappedLogic(pNtk) );
    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        Mio_Gate_t * pGateObj = (Mio_Gate_t *)pObj->pData;
        int nInputs = Mio_GateReadPinNum(pGateObj);
        // add basic faults (SA0, SA1, NEG)
        fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA0" ), Count++;
        fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA1" ), Count++;
        fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "NEG" ), Count++;
        if ( fStuckAt )
            continue;
        // add other faults, which correspond to changing the given gate
        // by another gate with the same support-size from the same library
        Mio_LibraryForEachGate( pLib, pGate )
            if ( pGate != pGateObj && Mio_GateReadPinNum(pGate) == nInputs )
                fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), Mio_GateReadName(pGate) ), Count++;
    }
    printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d %sfaults.\n", 
        pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1, fStuckAt ? "stuck-at ":"" );
    fclose( pFile );
}

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

  Synopsis    [Recognize type.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Io_ReadFinTypeMapped( Mio_Library_t * pLib, char * pThis )
{
    Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pThis, NULL );
    if ( pGate == NULL )
    {
        printf( "Cannot find gate \"%s\" in the current library.\n", pThis );
        return ABC_FIN_NONE;
    }
    return Mio_GateReadCell( pGate );
}
int Io_ReadFinType( char * pThis )
{
    if ( !strcmp(pThis, "SA0") )        return ABC_FIN_SA0;
    if ( !strcmp(pThis, "SA1") )        return ABC_FIN_SA1;
    if ( !strcmp(pThis, "NEG") )        return ABC_FIN_NEG;
    if ( !strcmp(pThis, "RDOB_AND") )   return ABC_FIN_RDOB_AND;
    if ( !strcmp(pThis, "RDOB_NAND") )  return ABC_FIN_RDOB_NAND;
    if ( !strcmp(pThis, "RDOB_OR") )    return ABC_FIN_RDOB_OR;
    if ( !strcmp(pThis, "RDOB_NOR") )   return ABC_FIN_RDOB_NOR;
    if ( !strcmp(pThis, "RDOB_XOR") )   return ABC_FIN_RDOB_XOR;
    if ( !strcmp(pThis, "RDOB_NXOR") )  return ABC_FIN_RDOB_NXOR;
    if ( !strcmp(pThis, "RDOB_NOT") )   return ABC_FIN_RDOB_NOT;
    if ( !strcmp(pThis, "RDOB_BUFF") )  return ABC_FIN_RDOB_BUFF;
    return ABC_FIN_NONE;
}
char * Io_WriteFinType( int Type )
{
    if ( Type == ABC_FIN_SA0 )          return "SA0";
    if ( Type == ABC_FIN_SA1 )          return "SA1";
    if ( Type == ABC_FIN_NEG )          return "NEG";
    if ( Type == ABC_FIN_RDOB_AND  )    return "RDOB_AND" ;
    if ( Type == ABC_FIN_RDOB_NAND )    return "RDOB_NAND";
    if ( Type == ABC_FIN_RDOB_OR   )    return "RDOB_OR"  ;
    if ( Type == ABC_FIN_RDOB_NOR  )    return "RDOB_NOR" ;
    if ( Type == ABC_FIN_RDOB_XOR  )    return "RDOB_XOR" ;
    if ( Type == ABC_FIN_RDOB_NXOR )    return "RDOB_NXOR";
    if ( Type == ABC_FIN_RDOB_NOT  )    return "RDOB_NOT" ;
    if ( Type == ABC_FIN_RDOB_BUFF )    return "RDOB_BUFF";
    return "Unknown";
}

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

  Synopsis    [Read information from file.]

  Description [Returns information as a set of pairs: (ObjId, TypeId).
  Uses the current network to map ObjName given in the file into ObjId.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
{
    Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
    char Buffer[1000];
    Abc_Obj_t * pObj;
    Abc_Nam_t * pNam;
    Vec_Int_t * vMap; 
    Vec_Int_t * vPairs = NULL;
    int i, Type, iObj, fFound, nLines = 1;
    FILE * pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Cannot open input file \"%s\" for reading.\n", pFileName );
        return NULL;
    }
    // map CI/node names into their IDs
    pNam = Abc_NamStart( 1000, 10 );
    vMap = Vec_IntAlloc( 1000 );
    Vec_IntPush( vMap, -1 );
    Abc_NtkForEachObj( pNtk, pObj, i )
    {
        if ( !Abc_ObjIsCi(pObj) && !Abc_ObjIsNode(pObj) )
            continue;
        Abc_NamStrFindOrAdd( pNam, Abc_ObjName(pObj), &fFound );
        if ( fFound )
        {
            printf( "The same name \"%s\" appears twice among CIs and internal nodes.\n", Abc_ObjName(pObj) );
            goto finish;
        }
        Vec_IntPush( vMap, Abc_ObjId(pObj) );
    }
    assert( Vec_IntSize(vMap) == Abc_NamObjNumMax(pNam) );
    // read file lines
    vPairs = Vec_IntAlloc( 1000 );
    Vec_IntPushTwo( vPairs, -1, -1 );
    while ( fgets(Buffer, 1000, pFile) != NULL )
    {
        // read line number
        char * pToken = strtok( Buffer, " \n\r\t" );
        if ( pToken == NULL )
            break;
        if ( nLines++ != atoi(pToken) )
        {
            printf( "Line numbers are not consecutive. Quitting.\n" );
            Vec_IntFreeP( &vPairs );
            goto finish;
        }
        // read object name and find its ID
        pToken = strtok( NULL, " \n\r\t" );
        iObj = Abc_NamStrFind( pNam, pToken );
        if ( !iObj )
        {
            printf( "Cannot find object with name \"%s\".\n", pToken );
            continue;
        }
        // read type
        pToken = strtok( NULL, " \n\r\t" );
        if ( Abc_NtkIsMappedLogic(pNtk) )
        {
            if ( !strcmp(pToken, "SA0") || !strcmp(pToken, "SA1") || !strcmp(pToken, "NEG") )
                Type = Io_ReadFinType( pToken );
            else
                Type = Io_ReadFinTypeMapped( pLib, pToken );
        }
        else
            Type = Io_ReadFinType( pToken );
        if ( Type == ABC_FIN_NONE )
        {
            printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
            continue;
        }
        Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
    }
    assert( Vec_IntSize(vPairs) == 2 * nLines );
    printf( "Finished reading %d lines from the fault list file \"%s\".\n", nLines - 1, pFileName );

    // verify the reader by printing the results
    if ( fVerbose )
        Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
            printf( "%-10d%-10s%-10s\n", i/2, Abc_ObjName(Abc_NtkObj(pNtk, iObj)), Io_WriteFinType(Type) );

finish:
    Vec_IntFree( vMap );
    Abc_NamDeref( pNam );
    fclose( pFile );
    return vPairs;
}


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

  Synopsis    [Extend the network by adding second timeframe.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFrameExtend( Abc_Ntk_t * pNtk )
{
    Vec_Ptr_t * vFanins, * vNodes;
    Abc_Obj_t * pObj, * pFanin, * pReset, * pEnable, * pSignal;
    Abc_Obj_t * pResetN, * pEnableN, * pAnd0, * pAnd1, * pMux;
    int i, k, iStartPo, nPisOld = Abc_NtkPiNum(pNtk), nPosOld = Abc_NtkPoNum(pNtk);
    // skip if there are no flops
    if ( pNtk->nConstrs == 0 )
        return;
    assert( Abc_NtkPiNum(pNtk) >= pNtk->nConstrs );
    assert( Abc_NtkPoNum(pNtk) >= pNtk->nConstrs * 4 );
    // collect nodes
    vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
    Abc_NtkForEachNode( pNtk, pObj, i )
        Vec_PtrPush( vNodes, pObj );
    // duplicate PIs
    vFanins = Vec_PtrAlloc( 2 );
    Abc_NtkForEachPi( pNtk, pObj, i )
    {
        if ( i == nPisOld )
            break;
        if ( i < nPisOld - pNtk->nConstrs )
        {
            Abc_NtkDupObj( pNtk, pObj, 0 );
            Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" );
            continue;
        }
        // create flop input
        iStartPo = nPosOld + 4 * (i - nPisOld);
        pReset   = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 1 ) );
        pEnable  = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 2 ) );
        pSignal  = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 3 ) );
        pResetN  = Abc_NtkCreateNodeInv( pNtk, pReset );
        pEnableN = Abc_NtkCreateNodeInv( pNtk, pEnable );
        Vec_PtrFillTwo( vFanins, 2, pEnableN, pObj );
        pAnd0    = Abc_NtkCreateNodeAnd( pNtk, vFanins );
        Vec_PtrFillTwo( vFanins, 2, pEnable, pSignal );
        pAnd1    = Abc_NtkCreateNodeAnd( pNtk, vFanins );
        Vec_PtrFillTwo( vFanins, 2, pAnd0, pAnd1 );
        pMux     = Abc_NtkCreateNodeOr( pNtk, vFanins );
        Vec_PtrFillTwo( vFanins, 2, pResetN, pMux );
        pObj->pCopy = Abc_NtkCreateNodeAnd( pNtk, vFanins );
    }
    // duplicate internal nodes
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        Abc_NtkDupObj( pNtk, pObj, 0 );
    // connect objects
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        Abc_ObjForEachFanin( pObj, pFanin, k )
            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
    // create new POs and reconnect flop inputs
    Abc_NtkForEachPo( pNtk, pObj, i )
    {
        if ( i == nPosOld )
            break;
        if ( i < nPosOld - 4 * pNtk->nConstrs )
        {
            Abc_NtkDupObj( pNtk, pObj, 0 );
            Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" );
            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
            continue;
        }
        Abc_ObjPatchFanin( pObj, Abc_ObjFanin0(pObj), Abc_ObjFanin0(pObj)->pCopy );
    }
    Vec_PtrFree( vFanins );
    Vec_PtrFree( vNodes );
}

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

  Synopsis    [Detect equivalence classes of nodes in terms of their TFO.]

  Description [Given is the logic network (pNtk) and the set of objects
  (primary inputs or internal nodes) to be considered (vObjs), this function
  returns a set of equivalence classes of these objects in terms of their 
  transitive fanout (TFO). Two objects belong to the same class if the set 
  of COs they feed into are the same.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_NtkDetectObjClasses_rec( Abc_Obj_t * pObj, Vec_Int_t * vMap, Hsh_VecMan_t * pHash, Vec_Int_t * vTemp )
{
    Vec_Int_t * vArray, * vSet;
    Abc_Obj_t * pNext; int i;
    // get the CO set for this object
    int Entry = Vec_IntEntry(vMap, Abc_ObjId(pObj));
    if ( Entry != -1 ) // the set is already computed
        return Entry;
    // compute a new CO set
    assert( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) );
    // if there is no fanouts, the set of COs is empty
    if ( Abc_ObjFanoutNum(pObj) == 0 )
    {
        Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), 0 );
        return 0;
    }
    // compute the set for the first fanout
    Entry = Abc_NtkDetectObjClasses_rec( Abc_ObjFanout0(pObj), vMap, pHash, vTemp );
    if ( Abc_ObjFanoutNum(pObj) == 1 )
    {
        Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry );
        return Entry;
    }
    vSet = Vec_IntAlloc( 16 );
    // initialize the set with that of first fanout
    vArray = Hsh_VecReadEntry( pHash, Entry );
    Vec_IntClear( vSet );
    Vec_IntAppend( vSet, vArray );
    // iteratively add sets of other fanouts
    Abc_ObjForEachFanout( pObj, pNext, i )
    {
        if ( i == 0 ) 
            continue;
        Entry = Abc_NtkDetectObjClasses_rec( pNext, vMap, pHash, vTemp );
        vArray = Hsh_VecReadEntry( pHash, Entry );
        Vec_IntTwoMerge2( vSet, vArray, vTemp );
        ABC_SWAP( Vec_Int_t, *vSet, *vTemp );
    }
    // create or find new set and map the object into it
    Entry = Hsh_VecManAdd( pHash, vSet );
    Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry );
    Vec_IntFree( vSet );
    return Entry;
}
Vec_Wec_t * Abc_NtkDetectObjClasses( Abc_Ntk_t * pNtk, Vec_Int_t * vObjs, Vec_Wec_t ** pvCos )
{
    Vec_Wec_t * vClasses;   // classes of equivalence objects from vObjs
    Vec_Int_t * vClassMap;  // mapping of each CO set into its class in vClasses
    Vec_Int_t * vClass;     // one equivalence class     
    Abc_Obj_t * pObj; 
    int i, iObj, SetId, ClassId;
    // create hash table to hash sets of CO indexes
    Hsh_VecMan_t * pHash = Hsh_VecManStart( 1000 );
    // create elementary sets (each composed of one CO) and map COs into them
    Vec_Int_t * vMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
    Vec_Int_t * vSet = Vec_IntAlloc( 16 );
    assert( Abc_NtkIsLogic(pNtk) );
    // compute empty set
    SetId = Hsh_VecManAdd( pHash, vSet );
    assert( SetId == 0 );
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        Vec_IntFill( vSet, 1, Abc_ObjId(pObj) );
        SetId = Hsh_VecManAdd( pHash, vSet );
        Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), SetId );
    }
    // make sure the array of objects is sorted
    Vec_IntSort( vObjs, 0 );
    // begin from the objects and map their IDs into sets of COs
    Abc_NtkForEachObjVec( vObjs, pNtk, pObj, i )
        Abc_NtkDetectObjClasses_rec( pObj, vMap, pHash, vSet );
    Vec_IntFree( vSet );
    // create map for mapping CO set its their classes
    vClassMap = Vec_IntStartFull( Hsh_VecSize(pHash) + 1 );
    // collect classes of objects
    vClasses = Vec_WecAlloc( 1000 );
    Vec_IntForEachEntry( vObjs, iObj, i )
    {
        //char * pName = Abc_ObjName( Abc_NtkObj(pNtk, iObj) );
        // for a given object (iObj), find the ID of its COs set
        SetId = Vec_IntEntry( vMap, iObj );
        assert( SetId >= 0 );
        // for the given CO set, finds its equivalence class
        ClassId = Vec_IntEntry( vClassMap, SetId );
        if ( ClassId == -1 )  // there is no equivalence class
        {
            // map this CO set into a new equivalence class
            Vec_IntWriteEntry( vClassMap, SetId, Vec_WecSize(vClasses) );
            vClass = Vec_WecPushLevel( vClasses );
        }
        else // get hold of the equivalence class
            vClass = Vec_WecEntry( vClasses, ClassId );
        // add objects to the class
        Vec_IntPush( vClass, iObj );
        // print the set for this object
        //printf( "Object %5d : ", iObj );
        //Vec_IntPrint( Hsh_VecReadEntry(pHash, SetId) );
    }
    // collect arrays of COs for each class
    *pvCos = Vec_WecStart( Vec_WecSize(vClasses) );
    Vec_WecForEachLevel( vClasses, vClass, i )
    {
        iObj = Vec_IntEntry( vClass, 0 );
        // for a given object (iObj), find the ID of its COs set
        SetId = Vec_IntEntry( vMap, iObj );
        assert( SetId >= 0 );
        // for the given CO set ID, find the set
        vSet = Hsh_VecReadEntry( pHash, SetId );
        Vec_IntAppend( Vec_WecEntry(*pvCos, i), vSet );
    }
    Hsh_VecManStop( pHash );
    Vec_IntFree( vClassMap );
    Vec_IntFree( vMap );
    return vClasses;
}
void Abc_NtkDetectClassesTest2( Abc_Ntk_t * pNtk, int fVerbose, int fVeryVerbose )
{
    Vec_Int_t * vObjs;
    Vec_Wec_t * vRes, * vCos;
    // for testing, create the set of object IDs for all combinational inputs (CIs)
    Abc_Obj_t * pObj; int i;
    vObjs = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Vec_IntPush( vObjs, Abc_ObjId(pObj) );
    // compute equivalence classes of CIs and print them
    vRes = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCos );
    Vec_WecPrint( vRes, 0 );
    Vec_WecPrint( vCos, 0 );
    // clean up
    Vec_IntFree( vObjs );
    Vec_WecFree( vRes );
    Vec_WecFree( vCos );
}

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

  Synopsis    [Collecting objects.]

  Description [Collects combinational inputs (vCIs) and internal nodes (vNodes)
  reachable from the given set of combinational outputs (vCOs).]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFinMiterCollect_rec( Abc_Obj_t * pObj, Vec_Int_t * vCis, Vec_Int_t * vNodes )
{
    if ( Abc_NodeIsTravIdCurrent(pObj) )
        return;
    Abc_NodeSetTravIdCurrent(pObj);
    if ( Abc_ObjIsCi(pObj) )
        Vec_IntPush( vCis, Abc_ObjId(pObj) );
    else
    {
        Abc_Obj_t * pFanin; int i;
        assert( Abc_ObjIsNode( pObj ) );
        Abc_ObjForEachFanin( pObj, pFanin, i )
            Abc_NtkFinMiterCollect_rec( pFanin, vCis, vNodes );
        Vec_IntPush( vNodes, Abc_ObjId(pObj) );
    }
}
void Abc_NtkFinMiterCollect( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes )
{
    Abc_Obj_t * pObj; int i;
    Vec_IntClear( vCis );
    Vec_IntClear( vNodes );
    Abc_NtkIncrementTravId( pNtk );
    Abc_NtkForEachObjVec( vCos, pNtk, pObj, i )
        Abc_NtkFinMiterCollect_rec( Abc_ObjFanin0(pObj), vCis, vNodes );
}

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

  Synopsis    [Simulates expression using given simulation info.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim )
{
    int i, w, nVars = Mio_GateReadPinNum(pGate);
    Vec_Int_t * vExpr = Mio_GateReadExpr( pGate );
    assert( nVars <= 6 );
    for ( w = 0; w < nWords; w++ )
    {
        word uFanins[6];
        for ( i = 0; i < nVars; i++ )
            uFanins[i] = ppFaninSims[i][w];
        pObjSim[w] = Exp_Truth6( nVars, vExpr, uFanins );
    }
}

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

  Synopsis    [Simulates expression for one simulation pattern.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] )
{
    int nVars = Mio_GateReadPinNum(pGate);
    int i, iMint = 0;
    for ( i = 0; i < nVars; i++ )
        if ( iBits[i] )
            iMint |= (1 << i);
    return Abc_InfoHasBit( (unsigned *)Mio_GateReadTruthP(pGate), iMint );
}

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

  Synopsis    [Simulated expression with one bit.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits )
{
    int i, nVars = Mio_GateReadPinNum(pGate);
    Vec_Int_t * vExpr = Mio_GateReadExpr( pGate );
    if ( Exp_IsConst0(vExpr) )
        return 0;
    if ( Exp_IsConst1(vExpr) )
        return 1;
    if ( Exp_IsLit(vExpr) )
    {
        int Index0  = Vec_IntEntry(vExpr,0) >> 1;
        int fCompl0 = Vec_IntEntry(vExpr,0) & 1;
        assert( Index0 < nVars );
        return Abc_LitNotCond( iLits[Index0], fCompl0 );
    }
    Vec_IntClear( vLits );
    for ( i = 0; i < nVars; i++ )
        Vec_IntPush( vLits, iLits[i] );
    for ( i = 0; i < Exp_NodeNum(vExpr); i++ )
    {
        int Index0  = Vec_IntEntry( vExpr, 2*i+0 ) >> 1;
        int Index1  = Vec_IntEntry( vExpr, 2*i+1 ) >> 1;
        int fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1;
        int fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1;
        Vec_IntPush( vLits, Gia_ManHashAnd( pGia, Abc_LitNotCond(Vec_IntEntry(vLits, Index0), fCompl0), Abc_LitNotCond(Vec_IntEntry(vLits, Index1), fCompl1) ) );
    }
    return Abc_LitNotCond( Vec_IntEntryLast(vLits), Vec_IntEntryLast(vExpr) & 1 );
}

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

  Synopsis    [AIG construction and simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Abc_NtkFinSimOneLit( Gia_Man_t * pNew, Abc_Obj_t * pObj, int Type, Vec_Int_t * vMap, int n, Vec_Int_t * vTemp )
{
    if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 )
    {
        extern int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits );
        Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc;
        int i, Lits[6];
        for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )
            Lits[i] = Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId(pObj, i), n) );
        return Mio_LibGateSimulateGia( pNew, Mio_LibraryReadGateById(pLib, Type), Lits, vTemp );
    }
    else
    {
        int iLit0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId0(pObj), n) ) : -1;
        int iLit1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId1(pObj), n) ) : -1;
        assert( Type != ABC_FIN_NEG );
        if ( Type == ABC_FIN_SA0 )            return 0;
        if ( Type == ABC_FIN_SA1 )            return 1;
        if ( Type == ABC_FIN_RDOB_BUFF )      return iLit0;
        if ( Type == ABC_FIN_RDOB_NOT )       return Abc_LitNot( iLit0 );
        if ( Type == ABC_FIN_RDOB_AND )       return Gia_ManHashAnd( pNew, iLit0, iLit1 );
        if ( Type == ABC_FIN_RDOB_OR )        return Gia_ManHashOr( pNew, iLit0, iLit1 );
        if ( Type == ABC_FIN_RDOB_XOR )       return Gia_ManHashXor( pNew, iLit0, iLit1 );
        if ( Type == ABC_FIN_RDOB_NAND )      return Abc_LitNot(Gia_ManHashAnd( pNew, iLit0, iLit1 ));
        if ( Type == ABC_FIN_RDOB_NOR )       return Abc_LitNot(Gia_ManHashOr( pNew, iLit0, iLit1 ));
        if ( Type == ABC_FIN_RDOB_NXOR )      return Abc_LitNot(Gia_ManHashXor( pNew, iLit0, iLit1 ));
        assert( 0 );
        return -1;
    }
}
static inline int Abc_NtkFinSimOneBit( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords, int iBit )
{
    if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 )
    {
        extern int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] );
        Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc;
        int i, iBits[6];
        for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )
        {
            word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) );
            iBits[i] = Abc_InfoHasBit( (unsigned*)pSim0, iBit );
        }
        return Mio_LibGateSimulateOne( Mio_LibraryReadGateById(pLib, Type), iBits );
    }
    else
    {
        word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL;
        word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL;
        int iBit0 = Abc_ObjFaninNum(pObj) > 0 ? Abc_InfoHasBit( (unsigned*)pSim0, iBit ) : -1;
        int iBit1 = Abc_ObjFaninNum(pObj) > 1 ? Abc_InfoHasBit( (unsigned*)pSim1, iBit ) : -1;
        assert( Type != ABC_FIN_NEG );
        if ( Type == ABC_FIN_SA0 )            return 0;
        if ( Type == ABC_FIN_SA1 )            return 1;
        if ( Type == ABC_FIN_RDOB_BUFF )      return iBit0;
        if ( Type == ABC_FIN_RDOB_NOT )       return !iBit0;
        if ( Type == ABC_FIN_RDOB_AND )       return iBit0 & iBit1;
        if ( Type == ABC_FIN_RDOB_OR )        return iBit0 | iBit1;
        if ( Type == ABC_FIN_RDOB_XOR )       return iBit0 ^ iBit1;
        if ( Type == ABC_FIN_RDOB_NAND )      return !(iBit0 & iBit1);
        if ( Type == ABC_FIN_RDOB_NOR )       return !(iBit0 | iBit1);
        if ( Type == ABC_FIN_RDOB_NXOR )      return !(iBit0 ^ iBit1);
        assert( 0 );
        return -1;
    }
}
static inline void Abc_NtkFinSimOneWord( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords )
{
    if ( Abc_NtkIsMappedLogic(pObj->pNtk) )
    {
        extern void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim );
        word * ppSims[6]; int i;
        word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );
        assert( Type == -1 );
        for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )
            ppSims[i] = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) );
        Mio_LibGateSimulate( (Mio_Gate_t *)pObj->pData, ppSims, nWords, pSim );
    }
    else
    {
        word * pSim  = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );  int w;
        word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL;
        word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL;
        assert( Type != ABC_FIN_NEG );
        if ( Type == ABC_FIN_SA0 )            for ( w = 0; w < nWords; w++ ) pSim[w] = 0;
        else if ( Type == ABC_FIN_SA1 )       for ( w = 0; w < nWords; w++ ) pSim[w] = ~((word)0);
        else if ( Type == ABC_FIN_RDOB_BUFF ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w];
        else if ( Type == ABC_FIN_RDOB_NOT )  for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w];
        else if ( Type == ABC_FIN_RDOB_AND )  for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] & pSim1[w];
        else if ( Type == ABC_FIN_RDOB_OR )   for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] | pSim1[w];
        else if ( Type == ABC_FIN_RDOB_XOR )  for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] ^ pSim1[w];
        else if ( Type == ABC_FIN_RDOB_NAND ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] & pSim1[w]);
        else if ( Type == ABC_FIN_RDOB_NOR )  for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] | pSim1[w]);
        else if ( Type == ABC_FIN_RDOB_NXOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] ^ pSim1[w]);
        else assert( 0 );
    }
}


// returns 1 if the functionality with indexes i1 and i2 is the same
static inline int Abc_NtkFinCompareSimTwo( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Wrd_t * vSims, int nWords, int i1, int i2 )
{
    Abc_Obj_t * pObj; int i;
    assert( i1 != i2 );
    Abc_NtkForEachObjVec( vCos, pNtk, pObj, i )
    {
        word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) );
        if ( Abc_InfoHasBit((unsigned*)pSim0, i1) != Abc_InfoHasBit((unsigned*)pSim0, i2) )
            return 0;
    }
    return 1;
}

Gia_Man_t * Abc_NtkFinMiterToGia( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, 
                                  int iObjs[2], int Types[2], Vec_Int_t * vLits )
{
    Gia_Man_t * pNew = NULL, * pTemp;
    Abc_Obj_t * pObj; 
    Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
    int n, i, Type, iMiter, iLit, * pLits;
    // create AIG manager
    pNew = Gia_ManStart( 1000 );
    pNew->pName = Abc_UtilStrsav( pNtk->pName );
    pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
    Gia_ManHashStart( pNew );
    // create inputs
    Abc_NtkForEachObjVec( vCis, pNtk, pObj, i )
    {
        iLit = Gia_ManAppendCi(pNew);
        for ( n = 0; n < 2; n++ )
        {
            if ( iObjs[n] != (int)Abc_ObjId(pObj) )
                Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), iLit );
            else if ( Types[n] != ABC_FIN_NEG )
                Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) );
            else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG )
                Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(iLit) );
        }
    }
    // create internal nodes
    Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
    {
        Type = Abc_NtkIsMappedLogic(pNtk) ? Mio_GateReadCell((Mio_Gate_t *)pObj->pData) : Vec_IntEntry(vTypes, Abc_ObjId(pObj));
        for ( n = 0; n < 2; n++ )
        {
            if ( iObjs[n] != (int)Abc_ObjId(pObj) )
                Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp) );
            else if ( Types[n] != ABC_FIN_NEG )
                Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) );
            else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG )
                Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp)) );
        }
    }
    // create comparator
    iMiter = 0;
    Abc_NtkForEachObjVec( vCos, pNtk, pObj, i )
    {
        pLits  = Vec_IntEntryP( vLits, Abc_Var2Lit(Abc_ObjFaninId0(pObj), 0) );
        iLit   = Gia_ManHashXor( pNew, pLits[0], pLits[1] );
        iMiter = Gia_ManHashOr( pNew, iMiter, iLit );
    }
    Gia_ManAppendCo( pNew, iMiter );
    // perform cleanup
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    Vec_IntFree( vTemp );
    return pNew;
}
void Abc_NtkFinSimulateOne( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, 
                            Vec_Wec_t * vMap2, Vec_Int_t * vPat, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vPairs, Vec_Wec_t * vRes, int iLevel, int iItem )
{
    Abc_Obj_t * pObj; 
    Vec_Int_t * vClass, * vArray;
    int i, Counter = 0;
    int nItems = Vec_WecSizeSize(vRes);
    assert( nItems == Vec_WecSizeSize(vMap2) );
    assert( nItems <= 128 * nWords );
    // assign inputs
    assert( Vec_IntSize(vPat) == Vec_IntSize(vCis) );
    Abc_NtkForEachObjVec( vCis, pNtk, pObj, i )
    {
        int w, iObj = Abc_ObjId( pObj );
        word Init = Vec_IntEntry(vPat, i) ? ~((word)0) : 0;
        word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );
        for ( w = 0; w < nWords; w++ )
            pSim[w] = Init;
        vArray = Vec_WecEntry(vMap2, iObj);
        if ( Vec_IntSize(vArray) > 0 )
        {
            int k, iFin, Index, iObj, Type;
            Vec_IntForEachEntryDouble( vArray, iFin, Index, k )
            {
                assert( Index < 64 );
                iObj = Vec_IntEntry( vPairs, 2*iFin );
                assert( iObj == (int)Abc_ObjId(pObj) );
                Type = Vec_IntEntry( vPairs, 2*iFin+1 );
                assert( Type == ABC_FIN_NEG || Type == ABC_FIN_SA0 || Type == ABC_FIN_SA1 );
                if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) )
                    Abc_InfoXorBit( (unsigned *)pSim, Index );
                Counter++;
            }
        }
    }
    // simulate internal nodes
    Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
    {
        int iObj = Abc_ObjId( pObj );
        int Type = Abc_NtkIsMappedLogic(pNtk) ? -1 : Vec_IntEntry( vTypes, iObj );
        word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );
        Abc_NtkFinSimOneWord( pObj, Type, vSims, nWords );
        vArray = Vec_WecEntry(vMap2, iObj);
        if ( Vec_IntSize(vArray) > 0 )
        {
            int k, iFin, Index, iObj, Type;
            Vec_IntForEachEntryDouble( vArray, iFin, Index, k )
            {
                assert( Index < 64 * nWords );
                iObj = Vec_IntEntry( vPairs, 2*iFin );
                assert( iObj == (int)Abc_ObjId(pObj) );
                Type = Vec_IntEntry( vPairs, 2*iFin+1 );
                if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) )
                    Abc_InfoXorBit( (unsigned *)pSim, Index );
                Counter++;
            }
        }
    }
    assert( nItems == 2*Counter );

    // confirm no refinement
    Vec_WecForEachLevelStop( vRes, vClass, i, iLevel+1 )
    {
        int k, iFin, Index, Value;
        int Index0 = Vec_IntEntry( vClass, 1 );
        Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 )
        {
            if ( i == iLevel && k/2 >= iItem )
                break;
            //printf( "Double-checking pair %d and %d\n", iFin0, iFin );
            Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index );
            assert( Value ); // the same value
        }
    }

    // check refinement
    Vec_WecForEachLevelStart( vRes, vClass, i, iLevel )
    {
        int k, iFin, Index, Value, Index0 = Vec_IntEntry(vClass, 1);
        int j = (i == iLevel) ? 2*iItem : 2;
        Vec_Int_t * vNewClass = NULL;
        Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, j )
        {
            Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index );
            if ( Value )  // the same value
            {
                Vec_IntWriteEntry( vClass, j++, iFin );
                Vec_IntWriteEntry( vClass, j++, Index );
                continue;
            }
            // create new class
            vNewClass = vNewClass ? vNewClass : Vec_WecPushLevel( vRes );
            Vec_IntPushTwo( vNewClass, iFin, Index );  // index and first entry
            vClass = Vec_WecEntry( vRes, i );
        }
        Vec_IntShrink( vClass, j );
    }
}

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

  Synopsis    [Check equivalence using SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, int iObjs[2], int Types[2], Vec_Int_t * vLits )
{
    Gia_Man_t * pGia = Abc_NtkFinMiterToGia( pNtk, vTypes, vCos, vCis, vNodes, iObjs, Types, vLits );
    if ( Gia_ManAndNum(pGia) == 0 && Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManCo(pGia, 0))) )
    {
        Vec_Int_t * vPat = Gia_ObjFaninC0(Gia_ManCo(pGia, 0)) ? Vec_IntStart(Vec_IntSize(vCis)) : NULL;
        Gia_ManStop( pGia );
        return vPat;
    }
    else
    {
        Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
        sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
        if ( pSat == NULL )
        {
            Gia_ManStop( pGia );
            Cnf_DataFree( pCnf );
            return NULL;
        }
        else
        {
            int i, nConfLimit = 10000;
            Vec_Int_t * vPat = NULL;
            int status, iVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
            //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0 );
            Gia_ManStop( pGia );
            Cnf_DataFree( pCnf );
            status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
            if ( status == l_Undef )
                vPat = Vec_IntAlloc(0);
            else if ( status == l_True )
            {
                vPat = Vec_IntAlloc( Vec_IntSize(vCis) );
                for ( i = 0; i < Vec_IntSize(vCis); i++ )
                    Vec_IntPush( vPat, sat_solver_var_value(pSat, iVarBeg+i) );
            }
            //printf( "%d ", sat_solver_nconflicts(pSat) );
            sat_solver_delete( pSat );
            return vPat;
        }
    }
}


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

  Synopsis    [Refinement of equivalence classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkFinLocalSetup( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Int_t * vResArray )
{
    int i, iFin;
    Vec_IntClear( vResArray );
    Vec_IntForEachEntry( vList, iFin, i )
    {
        int iObj = Vec_IntEntry( vPairs, 2*iFin );
        Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj );
        Vec_IntPushTwo( vArray, iFin, i );
        Vec_IntPushTwo( vResArray, iFin, i );
    }
}
void Abc_NtkFinLocalSetdown( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2 )
{
    int i, iFin;
    Vec_IntForEachEntry( vList, iFin, i )
    {
        int iObj = Vec_IntEntry( vPairs, 2*iFin );
        Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj );
        Vec_IntClear( vArray );
    }
}
int Abc_NtkFinRefinement( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, 
                          Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Wec_t * vResult )
{
    Vec_Wec_t * vRes  = Vec_WecAlloc( 100 );
    int nWords = Abc_Bit6WordNum( Vec_IntSize(vList) );
    Vec_Wrd_t * vSims = Vec_WrdStart( nWords * Abc_NtkObjNumMax(pNtk) );  // simulation info for each object
    Vec_Int_t * vLits = Vec_IntStart( 2*Abc_NtkObjNumMax(pNtk) );         // two literals for each object
    Vec_Int_t * vPat, * vClass, * vArray;  
    int i, k, iFin, Index, nCalls = 0;
    // prepare
    vArray = Vec_WecPushLevel( vRes );
    Abc_NtkFinLocalSetup( vPairs, vList, vMap2, vArray );
    // try all-0/all-1 pattern
    for ( i = 0; i < 2; i++ )
    {
        vPat = Vec_IntAlloc( Vec_IntSize(vCis) );
        Vec_IntFill( vPat, Vec_IntSize(vCis), i );
        Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, 0, 1 );
        Vec_IntFree( vPat );
    }
    // explore the classes
    //Vec_WecPrint( vRes, 0 );
    Vec_WecForEachLevel( vRes, vClass, i )
    {
        int iFin0  = Vec_IntEntry( vClass, 0 );
        Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 )
        {
            int Objs[2]  = { Vec_IntEntry(vPairs, 2*iFin0),   Vec_IntEntry(vPairs, 2*iFin)   }; 
            int Types[2] = { Vec_IntEntry(vPairs, 2*iFin0+1), Vec_IntEntry(vPairs, 2*iFin+1) }; 
            nCalls++;
            //printf( "Checking pair %d and %d.\n", iFin0, iFin );
            vPat = Abc_NtkFinCheckPair( pNtk, vTypes, vCos, vCis, vNodes, Objs, Types, vLits );
            if ( vPat == NULL ) // proved
                continue;
            assert( Vec_IntEntry(vClass, k) == iFin );
            if ( Vec_IntSize(vPat) == 0 )
            {
                Vec_Int_t * vNewClass = Vec_WecPushLevel( vRes );
                Vec_IntPushTwo( vNewClass, iFin, Index );  // index and first entry
                vClass = Vec_WecEntry( vRes, i );
                Vec_IntDrop( vClass, k+1 );
                Vec_IntDrop( vClass, k );
            }
            else // resimulate and refine
                Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, i, k/2 );
            Vec_IntFree( vPat );
            // make sure refinement happened (k'th entry is now absent or different)
            vClass = Vec_WecEntry( vRes, i );
            assert( Vec_IntSize(vClass) <= k || Vec_IntEntry(vClass, k) != iFin );
            k -= 2;
            //Vec_WecPrint( vRes, 0 );
        }
    }
    // unprepare
    Abc_NtkFinLocalSetdown( vPairs, vList, vMap2 );
    // reload proved equivs into the final array
    Vec_WecForEachLevel( vRes, vArray, i )
    {
        assert( Vec_IntSize(vArray) % 2 == 0 );
        if ( Vec_IntSize(vArray) <= 2 )
            continue;
        vClass = Vec_WecPushLevel( vResult );
        Vec_IntForEachEntryDouble( vArray, iFin, Index, k )
            Vec_IntPush( vClass, iFin );
    }
    Vec_WecFree( vRes );
    Vec_WrdFree( vSims );
    Vec_IntFree( vLits );
    return nCalls;
}

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

  Synopsis    [Detecting classes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Abc_ObjFinGateType( Abc_Obj_t * pNode )
{
    char * pSop = (char *)pNode->pData;
    if ( !strcmp(pSop, "1 1\n") )         return ABC_FIN_RDOB_BUFF;
    if ( !strcmp(pSop, "0 1\n") )         return ABC_FIN_RDOB_NOT;
    if ( !strcmp(pSop, "11 1\n") )        return ABC_FIN_RDOB_AND;
    if ( !strcmp(pSop, "11 0\n") )        return ABC_FIN_RDOB_NAND;
    if ( !strcmp(pSop, "00 0\n") )        return ABC_FIN_RDOB_OR;
    if ( !strcmp(pSop, "00 1\n") )        return ABC_FIN_RDOB_NOR;
    if ( !strcmp(pSop, "01 1\n10 1\n") )  return ABC_FIN_RDOB_XOR;
    if ( !strcmp(pSop, "11 1\n00 1\n") )  return ABC_FIN_RDOB_NXOR;
    return ABC_FIN_NONE;
}
int Abc_NtkFinCheckTypesOk( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj; int i;
    Abc_NtkForEachNode( pNtk, pObj, i )
        if ( Abc_ObjFinGateType(pObj) == ABC_FIN_NONE )
            return i;
    return 0;
}
int Abc_NtkFinCheckTypesOk2( Abc_Ntk_t * pNtk )
{
    Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
    int i, iObj, Type;
    Vec_IntForEachEntryDoubleStart( pNtk->vFins, iObj, Type, i, 2 )
    {
        Abc_Obj_t * pObj = Abc_NtkObj( pNtk, iObj );
        Mio_Gate_t * pGateFlt, * pGateObj = (Mio_Gate_t *)pObj->pData;
        if ( Type < 0 ) // SA0, SA1, NEG
            continue;
        pGateFlt = Mio_LibraryReadGateById( pLib, Type );
        if ( Mio_GateReadPinNum(pGateFlt) < 1 )
            continue;
        if ( Mio_GateReadPinNum(pGateObj) != Mio_GateReadPinNum(pGateFlt) )
            return iObj;
    }
    return 0;
}
Vec_Int_t * Abc_NtkFinComputeTypes( Abc_Ntk_t * pNtk )
{
    Abc_Obj_t * pObj; int i;
    Vec_Int_t * vObjs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
    Abc_NtkForEachNode( pNtk, pObj, i )
        Vec_IntWriteEntry( vObjs, Abc_ObjId(pObj), Abc_ObjFinGateType(pObj) );
    return vObjs;
}
Vec_Int_t * Abc_NtkFinComputeObjects( Vec_Int_t * vPairs, Vec_Wec_t ** pvMap, int nObjs )
{
    int i, iObj, Type;
    Vec_Int_t * vObjs = Vec_IntAlloc( 100 );
    *pvMap = Vec_WecStart( nObjs );
    Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
    {
        Vec_IntPush( vObjs, iObj );
        Vec_WecPush( *pvMap, iObj, i/2 );
    }
    Vec_IntUniqify( vObjs );
    return vObjs;
}
Vec_Int_t * Abc_NtkFinCreateList( Vec_Wec_t * vMap, Vec_Int_t * vClass )
{
    int i, iObj;
    Vec_Int_t * vList = Vec_IntAlloc( 100 );
    Vec_IntForEachEntry( vClass, iObj, i )
        Vec_IntAppend( vList, Vec_WecEntry(vMap, iObj) );
    return vList;
}
int Abc_NtkFinCountPairs( Vec_Wec_t * vClasses )
{
    int i, Counter = 0;
    Vec_Int_t * vLevel;
    Vec_WecForEachLevel( vClasses, vLevel, i )
        Counter += Vec_IntSize(vLevel) - 1;
    return Counter;
}
Vec_Wec_t * Abc_NtkDetectFinClasses( Abc_Ntk_t * pNtk, int fVerbose )
{
    Vec_Int_t * vTypes = NULL; // gate types
    Vec_Int_t * vPairs;        // original info as a set of pairs (ObjId, TypeId)
    Vec_Int_t * vObjs;         // all those objects that have some fin 
    Vec_Wec_t * vMap;          // for each object, the set of fins
    Vec_Wec_t * vMap2;         // for each local object, the set of pairs (Info, Index)
    Vec_Wec_t * vClasses;      // classes of objects
    Vec_Wec_t * vCoSets;       // corresponding CO sets
    Vec_Int_t * vClass;        // one class
    Vec_Int_t * vCoSet;        // one set of COs
    Vec_Int_t * vCiSet;        // one set of CIs
    Vec_Int_t * vNodeSet;      // one set of nodes
    Vec_Int_t * vList;         // one info list
    Vec_Wec_t * vResult;       // resulting equivalences
    int i, iObj, nCalls;
    if ( pNtk->vFins == NULL )
    {
        printf( "Current network does not have the required info.\n" );
        return NULL;
    }
    assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsMappedLogic(pNtk) );
    if ( Abc_NtkIsSopLogic(pNtk) )
    {
        iObj = Abc_NtkFinCheckTypesOk(pNtk);
        if ( iObj )
        {
            printf( "Current network contains unsupported gate types (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
            return NULL;
        }
        vTypes   = Abc_NtkFinComputeTypes( pNtk );
    }
    else if ( Abc_NtkIsMappedLogic(pNtk) )
    {
        iObj = Abc_NtkFinCheckTypesOk2(pNtk);
        if ( iObj )
        {
            printf( "Current network has mismatch between mapped gate size and fault gate size (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
            return NULL;
        }
    }
    else assert( 0 );
    //Abc_NtkFrameExtend( pNtk );
    // collect data
    vPairs   = pNtk->vFins;
    vObjs    = Abc_NtkFinComputeObjects( vPairs, &vMap, Abc_NtkObjNumMax(pNtk) );
    vClasses = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCoSets );
    // refine classes
    vCiSet   = Vec_IntAlloc( 1000 );
    vNodeSet = Vec_IntAlloc( 1000 );
    vMap2    = Vec_WecStart( Abc_NtkObjNumMax(pNtk) );
    vResult  = Vec_WecAlloc( 1000 );
    Vec_WecForEachLevel( vClasses, vClass, i )
    {
        // extract one window
        vCoSet = Vec_WecEntry( vCoSets, i );
        Abc_NtkFinMiterCollect( pNtk, vCoSet, vCiSet, vNodeSet );
        // refine one class
        vList = Abc_NtkFinCreateList( vMap, vClass );
        nCalls = Abc_NtkFinRefinement( pNtk, vTypes, vCoSet, vCiSet, vNodeSet, vPairs, vList, vMap2, vResult );
        if ( fVerbose )
            printf( "Group %4d :  Obj =%4d. Fins =%4d.  CI =%5d. CO =%5d. Node =%6d.  SAT calls =%5d.\n", 
                i, Vec_IntSize(vClass), Vec_IntSize(vList), Vec_IntSize(vCiSet), Vec_IntSize(vCoSet), Vec_IntSize(vNodeSet), nCalls );
        Vec_IntFree( vList );
    }
    // sort entries in each array
    Vec_WecForEachLevel( vResult, vClass, i )
        Vec_IntSort( vClass, 0 );
    // sort by the index of the first entry
    Vec_WecSortByFirstInt( vResult, 0 ); 
    // cleanup
    Vec_IntFreeP( & vTypes );
    Vec_IntFree( vObjs );
    Vec_WecFree( vClasses );
    Vec_WecFree( vMap );
    Vec_WecFree( vMap2 );
    Vec_WecFree( vCoSets );
    Vec_IntFree( vCiSet );
    Vec_IntFree( vNodeSet );
    return vResult;
}

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

  Synopsis    [Print results.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkPrintFinResults( Vec_Wec_t * vClasses )
{
    Vec_Int_t * vClass;
    int i, k, Entry;
    Vec_WecForEachLevel( vClasses, vClass, i )
        Vec_IntForEachEntryStart( vClass, Entry, k, 1 )
            printf( "%d %d\n", Vec_IntEntry(vClass, 0), Entry );
}

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

  Synopsis    [Top-level procedure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose )
{
    Vec_Wec_t * vResult;
    abctime clk = Abc_Clock();
    if ( fSeq ) 
        Abc_NtkFrameExtend( pNtk );
    vResult = Abc_NtkDetectFinClasses( pNtk, fVerbose );
    printf( "Computed %d equivalence classes with %d item pairs.  ", Vec_WecSize(vResult), Abc_NtkFinCountPairs(vResult) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( fVeryVerbose )
        Vec_WecPrint( vResult, 1 );
//    if ( fVerbose )
//        Abc_NtkPrintFinResults( vResult );
    Vec_WecFree( vResult );
}


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


ABC_NAMESPACE_IMPL_END