saigIsoSlow.c File Reference

#include "saig.h"

Go to the source code of this file.

Data Structures
struct	Iso_Obj_t_
struct	Iso_Man_t_

Macros
#define	ISO_MASK   0x3FF
#define	ISO_NUM_INTS   3
	DECLARATIONS ///. More...
#define	Iso_ManForEachObj(p, pObj, i)   for ( i = 1; (i < p->nObjs) && ((pObj) = Iso_ManObj(p, i)); i++ ) if ( pIso->Level == -1 ) {} else

Typedefs
typedef struct Iso_Obj_t_	Iso_Obj_t
typedef struct Iso_Man_t_	Iso_Man_t

Functions
static Iso_Obj_t *	Iso_ManObj (Iso_Man_t *p, int i)
static int	Iso_ObjId (Iso_Man_t *p, Iso_Obj_t *pObj)
static Aig_Obj_t *	Iso_AigObj (Iso_Man_t *p, Iso_Obj_t *q)
void	Iso_ReadPrimes (char *pFileName)
	FUNCTION DEFINITIONS ///. More...
void	Iso_FindNumbers ()
void	Iso_ManObjCount_rec (Aig_Man_t *p, Aig_Obj_t *pObj, int *pnNodes, int *pnEdges)
void	Iso_ManObjCount (Aig_Man_t *p, Aig_Obj_t *pObj, int *pnNodes, int *pnEdges)
Iso_Man_t *	Iso_ManStart (Aig_Man_t *pAig)
void	Iso_ManStop (Iso_Man_t *p, int fVerbose)
int	Iso_ObjCompare (Iso_Obj_t **pp1, Iso_Obj_t **pp2)
int	Iso_ObjCompareByData (Aig_Obj_t **pp1, Aig_Obj_t **pp2)
static int	Iso_ObjHash (Iso_Obj_t *pIso, int nBins)
static int	Iso_ObjHashAdd (Iso_Man_t *p, Iso_Obj_t *pIso)
void	Iso_ManCollectClasses (Iso_Man_t *p)
Iso_Man_t *	Iso_ManCreate (Aig_Man_t *pAig)
void	Iso_ManAssignAdjacency (Iso_Man_t *p)
void	Iso_ManPrintClasseSizes (Iso_Man_t *p)
void	Iso_ManPrintClasses (Iso_Man_t *p, int fVerbose, int fVeryVerbose)
void	Iso_ManRehashClassNodes (Iso_Man_t *p)
Iso_Obj_t *	Iso_ManFindBestObj (Iso_Man_t *p, Iso_Obj_t *pIso)
void	Iso_ManBreakTies (Iso_Man_t *p, int fVerbose)
Vec_Int_t *	Iso_ManFinalize (Iso_Man_t *p)
void	Iso_ManDumpOneClass (Iso_Man_t *p)
Vec_Int_t *	Saig_ManFindIsoPerm (Aig_Man_t *pAig, int fVerbose)

Variables
static int	s_1kPrimes [ISO_MASK+1]

Macro Definition Documentation

#define Iso_ManForEachObj	(		p,
			pObj,
			i
	)		for ( i = 1; (i < p->nObjs) && ((pObj) = Iso_ManObj(p, i)); i++ ) if ( pIso->Level == -1 ) {} else

Definition at line 304 of file saigIsoSlow.c.

#define ISO_MASK   0x3FF

CFile****************************************************************

FileName [aigIso.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Graph isomorphism package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

aigIso.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

Definition at line 122 of file saigIsoSlow.c.

#define ISO_NUM_INTS   3

DECLARATIONS ///.

Definition at line 261 of file saigIsoSlow.c.

Typedef Documentation

typedef struct Iso_Man_t_ Iso_Man_t

Definition at line 277 of file saigIsoSlow.c.

typedef struct Iso_Obj_t_ Iso_Obj_t

Definition at line 263 of file saigIsoSlow.c.

Function Documentation

static Aig_Obj_t* Iso_AigObj ( Iso_Man_t *  p, Iso_Obj_t *  q  )

inlinestatic

Definition at line 302 of file saigIsoSlow.c.

{ return Aig_ManObj( p->pAig, Iso_ObjId(p, q) );                                   }

void Iso_FindNumbers

(

)

Function*************************************************************

Synopsis [Read primes from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file saigIsoSlow.c.

{
    unsigned Nums[1024];
    unsigned char * pNums = (unsigned char *)Nums;
    int i, j;
    srand( 111 );
    for ( i = 0; i < 1024 * 4; i++ )
        pNums[i] = (unsigned char)rand();
    // write out
    for ( i = 0; i < 128; i++ )
    {
        printf( "    " );
        for ( j = 0; j < 8; j++ )
            printf( "0x%08x,", Nums[i*8+j] );
        printf( "\n" );
    }
}

void Iso_ManAssignAdjacency

(

Iso_Man_t *

p

)

Function*************************************************************

Synopsis [Creates adjacency lists.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file saigIsoSlow.c.

{
    int fUseXor = 0;
    Iso_Obj_t * pIso, * pIsoF;
    Aig_Obj_t * pObj, * pObjLi;
    int i;

    // create TFI signatures
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        pIso = p->pObjs + i;
        pIso->FaninSig = 0;
        pIso->FanoutSig = 0;

        if ( Aig_ObjIsCo(pObj) )
            continue;
        if ( fUseXor )
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIso->FaninSig ^= pIsoF->FaninSig;
                if ( pIsoF->Id )
                    pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIso->FaninSig ^= pIsoF->FaninSig;
                if ( pIsoF->Id )
                    pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
        }
        else
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIso->FaninSig += pIsoF->FaninSig;
                if ( pIsoF->Id )
                    pIso->FaninSig += pIsoF->Id * s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIso->FaninSig += pIsoF->FaninSig;
                if ( pIsoF->Id )
                    pIso->FaninSig += pIsoF->Id * s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
        }
    }
    // create TFO signatures
    Aig_ManForEachObjReverse( p->pAig, pObj, i )
    {
        if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
            continue;
        pIso = p->pObjs + i;
        assert( !Aig_ObjIsCo(pObj) || pIso->Id == 0 );
        if ( fUseXor )
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig ^= pIso->FanoutSig;
                if ( pIso->Id )
                    pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIsoF->FanoutSig ^= pIso->FanoutSig;
                if ( pIso->Id )
                    pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
            else if ( Aig_ObjIsCo(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig ^= pIso->FanoutSig;
                if ( pIso->Id )
                    pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
            }
        }
        else
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig += pIso->FanoutSig;
                if ( pIso->Id )
                    pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIsoF->FanoutSig += pIso->FanoutSig;
                if ( pIso->Id )
                    pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
            else if ( Aig_ObjIsCo(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig += pIso->FanoutSig;
                if ( pIso->Id )
                    pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObj)) & ISO_MASK];
            }
        }
    }

    // consider flops
    Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i )
    {
        if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant!
            continue;
        pIso  = Iso_ManObj( p, Aig_ObjId(pObj) );
        pIsoF = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) );
        assert( pIso->FaninSig == 0 );
//        assert( pIsoF->FanoutSig == 0 );

        if ( fUseXor )
        {
            pIso->FaninSig = pIsoF->FaninSig;
            if ( pIsoF->Id )
                pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];

            pIsoF->FanoutSig += pIso->FanoutSig;
            if ( pIso->Id )
                pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];
        }
        else
        {
            pIso->FaninSig = pIsoF->FaninSig;
            if ( pIsoF->Id )
                pIso->FaninSig += pIsoF->Id * s_1kPrimes[Abc_Var2Lit(pIsoF->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];

            pIsoF->FanoutSig += pIso->FanoutSig;
            if ( pIso->Id )
                pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC0(pObjLi)) & ISO_MASK];
        }
    }
}

void Iso_ManBreakTies	(	Iso_Man_t *	p,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Find nodes with the min number of edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 1043 of file saigIsoSlow.c.

{
    int fUseOneBest = 0;
    Iso_Obj_t * pIso, * pTemp;
    int i, LevelStart = 0;
    pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
    LevelStart = pIso->Level;
    if ( fVerbose )
        printf( "Best level %d\n", LevelStart ); 
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
    {
        if ( (int)pIso->Level < LevelStart )
            break;
        if ( !fUseOneBest )
        {
            for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
            {
                assert( pTemp->Id ==  0 );
                pTemp->Id = p->nObjIds++;
            }
            continue;
        }
        if ( pIso->Level == 0 )//&& pIso->nFoutPos + pIso->nFoutNeg == 0 )
        {
            for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
                pTemp->Id = p->nObjIds++;
            continue;
        }
        pIso = Iso_ManFindBestObj( p, pIso );
        pIso->Id = p->nObjIds++;
    }
}

void Iso_ManCollectClasses

(

Iso_Man_t *

p

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 556 of file saigIsoSlow.c.

{
    Iso_Obj_t * pIso;
    int i;
    abctime clk = Abc_Clock();
    Vec_PtrClear( p->vSingles );
    Vec_PtrClear( p->vClasses );
    for ( i = 0; i < p->nBins; i++ )
    {
        for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) )
        {
            assert( pIso->Id == 0 );
            if ( pIso->iClass )
                Vec_PtrPush( p->vClasses, pIso );
            else 
                Vec_PtrPush( p->vSingles, pIso );
        }
    }
    clk = Abc_Clock();
    Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
    Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
    p->timeSort += Abc_Clock() - clk;
    assert( Vec_PtrSize(p->vSingles) == p->nSingles );
    assert( Vec_PtrSize(p->vClasses) == p->nClasses );
    // assign IDs to singletons
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
        if ( pIso->Id == 0 )
            pIso->Id = p->nObjIds++;
}

Iso_Man_t* Iso_ManCreate

(

Aig_Man_t *

pAig

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 597 of file saigIsoSlow.c.

{
    int fUseXor = 0;
    Iso_Man_t * p;
    Iso_Obj_t * pIso, * pIsoF;
    Aig_Obj_t * pObj, * pObjLi;
    int i;
    p = Iso_ManStart( pAig );

    // create TFI signatures
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( Aig_ObjIsCo(pObj) )
            continue;
        pIso = p->pObjs + i;
        pIso->Level = pObj->Level;
//        pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);

        assert( pIso->FaninSig == 0 );
        assert( pIso->FanoutSig == 0 );
        if ( fUseXor )
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIso->FaninSig ^= pIsoF->FaninSig;
                pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIso->FaninSig ^= pIsoF->FaninSig;
                pIso->FaninSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
        }
        else
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIso->FaninSig += pIsoF->FaninSig;
                pIso->FaninSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIso->FaninSig += pIsoF->FaninSig;
                pIso->FaninSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
        }
    }

    // create TFO signatures
    Aig_ManForEachObjReverse( pAig, pObj, i )
    {
        if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
            continue;
        pIso = p->pObjs + i;
        if ( fUseXor )
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig ^= pIso->FanoutSig;
                pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIsoF->FanoutSig ^= pIso->FanoutSig;
                pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
            else if ( Aig_ObjIsCo(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig ^= pIso->FanoutSig;
                pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
            }
        }
        else
        {
            if ( Aig_ObjIsNode(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig += pIso->FanoutSig;
                pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];

                pIsoF = p->pObjs + Aig_ObjFaninId1(pObj);
                pIsoF->FanoutSig += pIso->FanoutSig;
                pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK];
            }
            else if ( Aig_ObjIsCo(pObj) )
            {
                pIsoF = p->pObjs + Aig_ObjFaninId0(pObj);
                pIsoF->FanoutSig += pIso->FanoutSig;
                pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC0(pObj)) & ISO_MASK];
            }
        }
    }

    // consider flops
    Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i )
    {
        if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant!
            continue;
        pIso  = Iso_ManObj( p, Aig_ObjId(pObj) );
        pIsoF = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) );

        assert( pIso->FaninSig == 0 );
        pIso->FaninSig = pIsoF->FaninSig;

//        assert( pIsoF->FanoutSig == 0 );
        pIsoF->FanoutSig += pIso->FanoutSig;
    }
/*
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pIso = p->pObjs + i;
        Aig_ObjPrint( pAig, pObj );
        printf( "Lev = %4d.  Pos = %4d.  FaninSig = %10d.  FanoutSig = %10d.\n", 
            pIso->Level, pIso->nFinNeg, pIso->FaninSig, pIso->FanoutSig );
    }
*/
    // add to the hash table
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
            continue;
        pIso = p->pObjs + i;
        Iso_ObjHashAdd( p, pIso );
    }
    // derive classes for the first time
    Iso_ManCollectClasses( p );
    return p;
}

void Iso_ManDumpOneClass

(

Iso_Man_t *

p

)

Function*************************************************************

Synopsis [Find nodes with the min number of edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 1140 of file saigIsoSlow.c.

{
    Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
    Iso_Obj_t * pIso, * pTemp;
    Aig_Man_t * pNew = NULL;
    assert( p->nClasses > 0 );
    pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
    assert( pIso->Id == 0 );
    for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
    {
        assert( pTemp->Id == 0 );
        Vec_PtrPush( vNodes, Iso_AigObj(p, pTemp) );
    }
    pNew = Aig_ManDupNodes( p->pAig, vNodes );
    Vec_PtrFree( vNodes );
    Aig_ManShow( pNew, 0, NULL ); 
    Aig_ManStopP( &pNew );
}

Vec_Int_t* Iso_ManFinalize

(

Iso_Man_t *

p

)

Function*************************************************************

Synopsis [Finalizes unification of combinational outputs.]

Description [Assigns IDs to the unclassified CIs in the order of obj IDs.]

SideEffects []

SeeAlso []

Definition at line 1087 of file saigIsoSlow.c.

{
    Vec_Int_t * vRes;
    Aig_Obj_t * pObj;
    int i;
    assert( p->nClasses == 0 );
    assert( Vec_PtrSize(p->vClasses) == 0 );
    // set canonical numbers
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
        {
            pObj->iData = -1;
            continue;
        }
        pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id;
        assert( pObj->iData > 0 );
    }
    Aig_ManConst1(p->pAig)->iData = 0;
    // assign unique IDs to the CIs
    Vec_PtrClear( p->vTemp1 );
    Vec_PtrClear( p->vTemp2 );
    Aig_ManForEachCi( p->pAig, pObj, i )
    {
        assert( pObj->iData > 0 );
        if ( Aig_ObjCioId(pObj) >= Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop
            Vec_PtrPush( p->vTemp2, pObj );
        else // PI
            Vec_PtrPush( p->vTemp1, pObj );
    }
    // sort CIs by their IDs
    Vec_PtrSort( p->vTemp1, (int (*)(void))Iso_ObjCompareByData );
    Vec_PtrSort( p->vTemp2, (int (*)(void))Iso_ObjCompareByData );
    // create the result
    vRes = Vec_IntAlloc( Aig_ManCiNum(p->pAig) );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i )
        Vec_IntPush( vRes, Aig_ObjCioId(pObj) );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i )
        Vec_IntPush( vRes, Aig_ObjCioId(pObj) );
    return vRes;
}

Iso_Obj_t* Iso_ManFindBestObj	(	Iso_Man_t *	p,
		Iso_Obj_t *	pIso
	)

Function*************************************************************

Synopsis [Find nodes with the min number of edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 1008 of file saigIsoSlow.c.

{
    Iso_Obj_t * pTemp, * pBest = NULL;
    int nNodesBest = -1, nNodes;
    int nEdgesBest = -1, nEdges;
    assert( pIso->Id == 0 );
    if ( pIso->Level == 0 )
        return pIso;
    for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
    {
        assert( pTemp->Id == 0 );
        Iso_ManObjCount( p->pAig, Iso_AigObj(p, pTemp), &nNodes, &nEdges );
//        printf( "%d,%d ", nNodes, nEdges );
        if ( nNodesBest < nNodes || (nNodesBest == nNodes && nEdgesBest < nEdges) )
        {
            nNodesBest = nNodes;
            nEdgesBest = nEdges;
            pBest = pTemp;
        }
    }
//    printf( "\n" );
    return pBest;
}

static Iso_Obj_t* Iso_ManObj ( Iso_Man_t *  p, int  i  )

inlinestatic

Definition at line 300 of file saigIsoSlow.c.

{ assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                }

void Iso_ManObjCount	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int *	pnNodes,
		int *	pnEdges
	)

Definition at line 406 of file saigIsoSlow.c.

{
    assert( Aig_ObjIsNode(pObj) );
    *pnNodes = *pnEdges = 0;
    Aig_ManIncrementTravId( p );
    Iso_ManObjCount_rec( p, pObj, pnNodes, pnEdges );
}

void Iso_ManObjCount_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int *	pnNodes,
		int *	pnEdges
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 394 of file saigIsoSlow.c.

{
    if ( Aig_ObjIsCi(pObj) )
        return;
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    Iso_ManObjCount_rec( p, Aig_ObjFanin0(pObj), pnNodes, pnEdges );
    Iso_ManObjCount_rec( p, Aig_ObjFanin1(pObj), pnNodes, pnEdges );
    (*pnEdges) += Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
    (*pnNodes)++;
}

void Iso_ManPrintClasses	(	Iso_Man_t *	p,
		int	fVerbose,
		int	fVeryVerbose
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 909 of file saigIsoSlow.c.

{
    int fOnlyCis = 0;
    Iso_Obj_t * pIso, * pTemp;
    int i;

    // count unique objects
    if ( fVerbose )
        printf( "Total objects =%7d.  Entries =%7d.  Classes =%7d.  Singles =%7d.\n", 
            p->nObjs, p->nEntries, p->nClasses, p->nSingles );

    if ( !fVeryVerbose )
        return;

    printf( "Non-trivial classes:\n" );
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
    {
        if ( fOnlyCis && pIso->Level > 0 )
            continue;

        printf( "%5d : {", i );
        for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
        {
            if ( fOnlyCis )
                printf( " %d", Aig_ObjCioId( Iso_AigObj(p, pTemp) ) );
            else
            {
                Aig_Obj_t * pObj = Iso_AigObj(p, pTemp);
                if ( Aig_ObjIsNode(pObj) )
                    printf( " %d{%s%d(%d),%s%d(%d)}", Iso_ObjId(p, pTemp), 
                        Aig_ObjFaninC0(pObj)? "-": "+", Aig_ObjFaninId0(pObj), Aig_ObjLevel(Aig_ObjFanin0(pObj)), 
                        Aig_ObjFaninC1(pObj)? "-": "+", Aig_ObjFaninId1(pObj), Aig_ObjLevel(Aig_ObjFanin1(pObj)) );
                else
                    printf( " %d", Iso_ObjId(p, pTemp) );
            }
            printf( "(%d)", pTemp->Level );
        }        
        printf( " }\n" );
    }
}

void Iso_ManPrintClasseSizes

(

Iso_Man_t *

p

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 884 of file saigIsoSlow.c.

{
    Iso_Obj_t * pIso, * pTemp;
    int i, Counter;
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
    {
        Counter = 0;
        for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
            Counter++;
        printf( "%d ", Counter );
    }
    printf( "\n" );
}

void Iso_ManRehashClassNodes

(

Iso_Man_t *

p

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 962 of file saigIsoSlow.c.

{
    Iso_Obj_t * pIso, * pTemp;
    int i;
    // collect nodes
    Vec_PtrClear( p->vTemp1 );
    Vec_PtrClear( p->vTemp2 );
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
    {
        for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
            if ( pTemp->Id == 0 )
                Vec_PtrPush( p->vTemp1, pTemp );
            else
                Vec_PtrPush( p->vTemp2, pTemp );
    }
    // clean and add nodes
    p->nClasses = 0;       // total number of classes
    p->nEntries = 0;       // total number of entries
    p->nSingles = 0;       // total number of singletons
    memset( p->pBins, 0, sizeof(int) * p->nBins );
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp1, pTemp, i )
    {
        assert( pTemp->Id == 0 );
        pTemp->iClass = pTemp->iNext = 0;
        Iso_ObjHashAdd( p, pTemp );
    }
    Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp2, pTemp, i )
    {
        assert( pTemp->Id != 0 );
        pTemp->iClass = pTemp->iNext = 0;
    }
    // collect new classes
    Iso_ManCollectClasses( p );
}

Iso_Man_t* Iso_ManStart

(

Aig_Man_t *

pAig

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file saigIsoSlow.c.

{
    Iso_Man_t * p;
    p = ABC_CALLOC( Iso_Man_t, 1 );
    p->pAig     = pAig;
    p->nObjs    = Aig_ManObjNumMax( pAig );
    p->pObjs    = ABC_CALLOC( Iso_Obj_t, p->nObjs );
    p->nBins    = Abc_PrimeCudd( p->nObjs );
    p->pBins    = ABC_CALLOC( int, p->nBins );    
    p->vSingles = Vec_PtrAlloc( 1000 );
    p->vClasses = Vec_PtrAlloc( 1000 );
    p->vTemp1   = Vec_PtrAlloc( 1000 );
    p->vTemp2   = Vec_PtrAlloc( 1000 );
    p->nObjIds  = 1;
    return p;
}

void Iso_ManStop	(	Iso_Man_t *	p,
		int	fVerbose
	)

Definition at line 441 of file saigIsoSlow.c.

{
    if ( fVerbose )
    {
        p->timeOther = p->timeTotal - p->timeHash - p->timeFout;
        ABC_PRTP( "Building ", p->timeFout,               p->timeTotal );
        ABC_PRTP( "Hashing  ", p->timeHash-p->timeSort,   p->timeTotal );
        ABC_PRTP( "Sorting  ", p->timeSort,               p->timeTotal );
        ABC_PRTP( "Other    ", p->timeOther,              p->timeTotal );
        ABC_PRTP( "TOTAL    ", p->timeTotal,              p->timeTotal );
    }
    Vec_PtrFree( p->vTemp1 );
    Vec_PtrFree( p->vTemp2 );
    Vec_PtrFree( p->vClasses );
    Vec_PtrFree( p->vSingles );
    ABC_FREE( p->pBins );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}

int Iso_ObjCompare	(	Iso_Obj_t **	pp1,
		Iso_Obj_t **	pp2
	)

Function*************************************************************

Synopsis [Compares two objects by their signature.]

Description []

SideEffects []

SeeAlso []

Definition at line 473 of file saigIsoSlow.c.

{
    return -memcmp( *pp1, *pp2, sizeof(int) * ISO_NUM_INTS );
}

int Iso_ObjCompareByData	(	Aig_Obj_t **	pp1,
		Aig_Obj_t **	pp2
	)

Function*************************************************************

Synopsis [Compares two objects by their ID.]

Description []

SideEffects []

SeeAlso []

Definition at line 489 of file saigIsoSlow.c.

{
    Aig_Obj_t * pIso1 = *pp1;
    Aig_Obj_t * pIso2 = *pp2;
    assert( Aig_ObjIsCi(pIso1) || Aig_ObjIsCo(pIso1) );
    assert( Aig_ObjIsCi(pIso2) || Aig_ObjIsCo(pIso2) );
    return pIso1->iData - pIso2->iData;
}

static int Iso_ObjHash ( Iso_Obj_t *  pIso, int  nBins  )

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 509 of file saigIsoSlow.c.

{
    static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
    unsigned * pArray = (unsigned *)pIso;
    unsigned i, Value = 0;
    assert( ISO_NUM_INTS < 8 );
    for ( i = 0; i < ISO_NUM_INTS; i++ )
        Value ^= BigPrimes[i] * pArray[i];
    return Value % nBins;
}

static int Iso_ObjHashAdd ( Iso_Man_t *  p, Iso_Obj_t *  pIso  )

inlinestatic

Definition at line 519 of file saigIsoSlow.c.

{
    Iso_Obj_t * pThis;
    int * pPlace = p->pBins + Iso_ObjHash( pIso, p->nBins );
    p->nEntries++;
    for ( pThis = Iso_ManObj(p, *pPlace); 
          pThis; pPlace = &pThis->iNext, 
          pThis = Iso_ManObj(p, *pPlace) )
        if ( Iso_ObjCompare( &pThis, &pIso ) == 0 ) // equal signatures
        {
            if ( pThis->iClass == 0 )
            {
                p->nClasses++;
                p->nSingles--;
            }
            // add to the list
            pIso->iClass = pThis->iClass;
            pThis->iClass = Iso_ObjId( p, pIso );
            return 1;
        }
    // create new list
    *pPlace = Iso_ObjId( p, pIso );
    p->nSingles++;
    return 0;
}

static int Iso_ObjId ( Iso_Man_t *  p, Iso_Obj_t *  pObj  )

inlinestatic

Definition at line 301 of file saigIsoSlow.c.

{ assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }

void Iso_ReadPrimes

(

char *

pFileName

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Read primes from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 325 of file saigIsoSlow.c.

{
    FILE * pFile;
    int Nums[10000];
    int i, j, Temp, nSize = 0;
    // read the numbers
    pFile = fopen( pFileName, "rb" );
    while ( fscanf( pFile, "%d", Nums + nSize++ ) == 1 );
    fclose( pFile );
    assert( nSize >= (1<<10) );
    // randomly permute
    srand( 111 );
    for ( i = 0; i < nSize; i++ )
    {
        j = rand() % nSize;
        Temp = Nums[i];
        Nums[i] = Nums[j];
        Nums[j] = Temp;
    }
    // write out
    for ( i = 0; i < 64; i++ )
    {
        printf( "    " );
        for ( j = 0; j < 16; j++ )
            printf( "%d,", Nums[i*16+j] );
        printf( "\n" );
    }
}

Vec_Int_t* Saig_ManFindIsoPerm	(	Aig_Man_t *	pAig,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Finds canonical permutation of CIs and assigns unique IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1170 of file saigIsoSlow.c.

{
    int fVeryVerbose = 0;
    Vec_Int_t * vRes;
    Iso_Man_t * p;
    abctime clk = Abc_Clock(), clk2 = Abc_Clock();
    p = Iso_ManCreate( pAig );
    p->timeFout += Abc_Clock() - clk;
    Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
    while ( p->nClasses )
    {
        // assign adjacency to classes
        clk = Abc_Clock();
        Iso_ManAssignAdjacency( p );
        p->timeFout += Abc_Clock() - clk;
        // rehash the class nodes
        clk = Abc_Clock();
        Iso_ManRehashClassNodes( p );
        p->timeHash += Abc_Clock() - clk;
        Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
        // force refinement
        while ( p->nSingles == 0 && p->nClasses )
        {
//            Iso_ManPrintClasseSizes( p );
            // assign IDs to the topmost level of classes
            Iso_ManBreakTies( p, fVerbose );
            // assign adjacency to classes
            clk = Abc_Clock();
            Iso_ManAssignAdjacency( p );
            p->timeFout += Abc_Clock() - clk;
            // rehash the class nodes
            clk = Abc_Clock();
            Iso_ManRehashClassNodes( p );
            p->timeHash += Abc_Clock() - clk;
            Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
        }
    }
    p->timeTotal = Abc_Clock() - clk2;
//    printf( "IDs assigned = %d.  Objects = %d.\n", p->nObjIds, 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
    assert( p->nObjIds == 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
//    if ( p->nClasses )
//        Iso_ManDumpOneClass( p );
    vRes = Iso_ManFinalize( p );
    Iso_ManStop( p, fVerbose );
    return vRes;
}

Variable Documentation

int s_1kPrimes[ISO_MASK+1]

static

Definition at line 123 of file saigIsoSlow.c.