dchClass.c File Reference

#include "dchInt.h"

Go to the source code of this file.

Data Structures
struct	Dch_Cla_t_

Macros
#define	Dch_ManForEachClass(p, ppClass, i)
#define	Dch_ClassForEachNode(p, pRepr, pNode, i)

Functions
static Aig_Obj_t *	Dch_ObjNext (Aig_Obj_t **ppNexts, Aig_Obj_t *pObj)
	DECLARATIONS ///. More...
static void	Dch_ObjSetNext (Aig_Obj_t **ppNexts, Aig_Obj_t *pObj, Aig_Obj_t *pNext)
static void	Dch_ObjAddClass (Dch_Cla_t *p, Aig_Obj_t *pRepr, Aig_Obj_t **pClass, int nSize)
	FUNCTION DEFINITIONS ///. More...
static Aig_Obj_t **	Dch_ObjRemoveClass (Dch_Cla_t *p, Aig_Obj_t *pRepr)
Dch_Cla_t *	Dch_ClassesStart (Aig_Man_t *pAig)
void	Dch_ClassesSetData (Dch_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
void	Dch_ClassesStop (Dch_Cla_t *p)
int	Dch_ClassesLitNum (Dch_Cla_t *p)
Aig_Obj_t **	Dch_ClassesReadClass (Dch_Cla_t *p, Aig_Obj_t *pRepr, int *pnSize)
void	Dch_ClassesCheck (Dch_Cla_t *p)
void	Dch_ClassesPrintOne (Dch_Cla_t *p, Aig_Obj_t *pRepr)
void	Dch_ClassesPrint (Dch_Cla_t *p, int fVeryVerbose)
void	Dch_ClassesPrepare (Dch_Cla_t *p, int fLatchCorr, int nMaxLevs)
int	Dch_ClassesRefineOneClass (Dch_Cla_t *p, Aig_Obj_t *pReprOld, int fRecursive)
int	Dch_ClassesRefine (Dch_Cla_t *p)
void	Dch_ClassesCollectOneClass (Dch_Cla_t *p, Aig_Obj_t *pRepr, Vec_Ptr_t *vRoots)
void	Dch_ClassesCollectConst1Group (Dch_Cla_t *p, Aig_Obj_t *pObj, int nNodes, Vec_Ptr_t *vRoots)
int	Dch_ClassesRefineConst1Group (Dch_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)

Macro Definition Documentation

#define Dch_ClassForEachNode	(		p,
			pRepr,
			pNode,
			i
	)

Value:

for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ )        \
        if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else

Definition at line 71 of file dchClass.c.

#define Dch_ManForEachClass	(		p,
			ppClass,
			i
	)

Value:

for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )        \
        if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else

Definition at line 67 of file dchClass.c.

Function Documentation

void Dch_ClassesCheck

(

Dch_Cla_t *

p

)

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

Synopsis [Checks candidate equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file dchClass.c.

{
    Aig_Obj_t * pObj, * pPrev, ** ppClass;
    int i, k, nLits, nClasses, nCands1;
    nClasses = nLits = 0;
    Dch_ManForEachClass( p, ppClass, k )
    {
        pPrev = NULL;
        Dch_ClassForEachNode( p, ppClass[0], pObj, i )
        {
            if ( i == 0 )
                assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
            else
            {
                assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
                assert( pPrev->Id < pObj->Id );
                nLits++;
            }
            pPrev = pObj;
        }
        nClasses++;
    }
    nCands1 = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
        nCands1 += Dch_ObjIsConst1Cand( p->pAig, pObj );
    assert( p->nLits == nLits );
    assert( p->nCands1 == nCands1 );
    assert( p->nClasses == nClasses );
}

void Dch_ClassesCollectConst1Group	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pObj,
		int	nNodes,
		Vec_Ptr_t *	vRoots
	)

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

Synopsis [Returns equivalence class of the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 546 of file dchClass.c.

{
    int i, Limit;
    Vec_PtrClear( vRoots );
    Limit = Abc_MinInt( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
    for ( i = pObj->Id; i < Limit; i++ )
    {
        pObj = Aig_ManObj( p->pAig, i );
        if ( pObj && Dch_ObjIsConst1Cand( p->pAig, pObj ) )
            Vec_PtrPush( vRoots, pObj );
    }
}

void Dch_ClassesCollectOneClass	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pRepr,
		Vec_Ptr_t *	vRoots
	)

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

Synopsis [Returns equivalence class of the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 525 of file dchClass.c.

{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrClear( vRoots );
    Dch_ClassForEachNode( p, pRepr, pObj, i )
        Vec_PtrPush( vRoots, pObj );
    assert( Vec_PtrSize(vRoots) > 1 ); 
}

int Dch_ClassesLitNum

(

Dch_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file dchClass.c.

{
    return p->nLits;
}

void Dch_ClassesPrepare	(	Dch_Cla_t *	p,
		int	fLatchCorr,
		int	nMaxLevs
	)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 336 of file dchClass.c.

{
    Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
    Aig_Obj_t * pObj, * pTemp, * pRepr;
    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;

    // allocate the hash table hashing simulation info into nodes
    nTableSize = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); 
    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 

    // add all the nodes to the hash table
    nEntries = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Aig_ObjIsCi(pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
                continue;
        }
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
        {
            Dch_ObjSetConst1Cand( p->pAig, pObj );
            p->nCands1++;
            continue;
        }
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
            ppTable[iEntry] = pObj;
        else
        {
            // set the representative of this node
            pRepr = ppTable[iEntry];
            Aig_ObjSetRepr( p->pAig, pObj, pRepr );
            // add node to the table
            if ( Dch_ObjNext( ppNexts, pRepr ) == NULL )
            { // this will be the second entry
                p->pClassSizes[pRepr->Id]++;
                nEntries++;
            }
            // add the entry to the list
            Dch_ObjSetNext( ppNexts, pObj, Dch_ObjNext( ppNexts, pRepr ) );
            Dch_ObjSetNext( ppNexts, pRepr, pObj );
            p->pClassSizes[pRepr->Id]++;
            nEntries++;
        }
    }

    // allocate room for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
    p->pMemClassesFree = p->pMemClasses + nEntries;
 
    // copy the entries into storage in the topological order
    nEntries2 = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
            continue;
        nNodes = p->pClassSizes[pObj->Id];
        // skip the nodes that are not representatives of non-trivial classes
        if ( nNodes == 0 )
            continue;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
        ppClassNew = p->pMemClasses + nEntries2;
        ppClassNew[0] = pObj;
        for ( pTemp = Dch_ObjNext(ppNexts, pObj), k = 1; pTemp; 
              pTemp = Dch_ObjNext(ppNexts, pTemp), k++ )
        {
            ppClassNew[nNodes-k] = pTemp;
        }
        // add the class of nodes
        p->pClassSizes[pObj->Id] = 0;
        Dch_ObjAddClass( p, pObj, ppClassNew, nNodes );
        // increment the number of entries
        nEntries2 += nNodes;
    }
    assert( nEntries == nEntries2 );
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
    // now it is time to refine the classes
    Dch_ClassesRefine( p );
    Dch_ClassesCheck( p );
}

void Dch_ClassesPrint	(	Dch_Cla_t *	p,
		int	fVeryVerbose
	)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 303 of file dchClass.c.

{
    Aig_Obj_t ** ppClass;
    Aig_Obj_t * pObj;
    int i;
    Abc_Print( 1, "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", 
        p->nCands1, p->nClasses, p->nLits );
    if ( !fVeryVerbose )
        return;
    Abc_Print( 1, "Constants { " );
    Aig_ManForEachObj( p->pAig, pObj, i )
        if ( Dch_ObjIsConst1Cand( p->pAig, pObj ) )
            Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
    Abc_Print( 1, "}\n" );
    Dch_ManForEachClass( p, ppClass, i )
    {
        Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
        Dch_ClassesPrintOne( p, ppClass[0] );
    }
    Abc_Print( 1, "\n" );
}

void Dch_ClassesPrintOne	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pRepr
	)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file dchClass.c.

{
    Aig_Obj_t * pObj;
    int i;
    Abc_Print( 1, "{ " );
    Dch_ClassForEachNode( p, pRepr, pObj, i )
        Abc_Print( 1, "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
    Abc_Print( 1, "}\n" );
}

Aig_Obj_t** Dch_ClassesReadClass	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pRepr,
		int *	pnSize
	)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file dchClass.c.

{
    assert( p->pId2Class[pRepr->Id] != NULL );
    assert( p->pClassSizes[pRepr->Id] > 1 );
    *pnSize = p->pClassSizes[pRepr->Id];
    return p->pId2Class[pRepr->Id];
}

int Dch_ClassesRefine

(

Dch_Cla_t *

p

)

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 504 of file dchClass.c.

{
    Aig_Obj_t ** ppClass;
    int i, nRefis = 0;
    Dch_ManForEachClass( p, ppClass, i )
        nRefis += Dch_ClassesRefineOneClass( p, ppClass[0], 0 );
    return nRefis;
}

int Dch_ClassesRefineConst1Group	(	Dch_Cla_t *	p,
		Vec_Ptr_t *	vRoots,
		int	fRecursive
	)

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 570 of file dchClass.c.

{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    if ( Vec_PtrSize(vRoots) == 0 )
        return 0;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
            Vec_PtrPush( p->vClassNew, pObj );
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    p->nCands1 -= Vec_PtrSize(p->vClassNew);
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
    if ( Vec_PtrSize(p->vClassNew) == 1 )
        return 1;
    // create a new class composed of these nodes
    ppClassNew = p->pMemClassesFree;
    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        ppClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
    Dch_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

int Dch_ClassesRefineOneClass	(	Dch_Cla_t *	p,
		Aig_Obj_t *	pReprOld,
		int	fRecursive
	)

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

Synopsis [Iteratively refines the classes after simulation.]

Description [Returns the number of refinements performed.]

SideEffects []

SeeAlso []

Definition at line 443 of file dchClass.c.

{
    Aig_Obj_t ** pClassOld, ** pClassNew;
    Aig_Obj_t * pObj, * pReprNew;
    int i;

    // split the class
    Vec_PtrClear( p->vClassOld );
    Vec_PtrClear( p->vClassNew );
    Dch_ClassForEachNode( p, pReprOld, pObj, i )
        if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
            Vec_PtrPush( p->vClassOld, pObj );
        else
            Vec_PtrPush( p->vClassNew, pObj );
    // check if splitting happened
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;

    // get the new representative
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    assert( Vec_PtrSize(p->vClassOld) > 0 );
    assert( Vec_PtrSize(p->vClassNew) > 0 );

    // create old class
    pClassOld = Dch_ObjRemoveClass( p, pReprOld );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
    {
        pClassOld[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
    }
    // create new class
    pClassNew = pClassOld + i;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        pClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }

    // put classes back
    if ( Vec_PtrSize(p->vClassOld) > 1 )
        Dch_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
    if ( Vec_PtrSize(p->vClassNew) > 1 )
        Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );

    // check if the class should be recursively refined
    if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
        return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

void Dch_ClassesSetData	(	Dch_Cla_t *	p,
		void *	pManData,
		unsigned(*)(void *, Aig_Obj_t *)	pFuncNodeHash,
		int(*)(void *, Aig_Obj_t *)	pFuncNodeIsConst,
		int(*)(void *, Aig_Obj_t *, Aig_Obj_t *)	pFuncNodesAreEqual
	)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file dchClass.c.

{
    p->pManData           = pManData;
    p->pFuncNodeHash      = pFuncNodeHash;
    p->pFuncNodeIsConst   = pFuncNodeIsConst;
    p->pFuncNodesAreEqual = pFuncNodesAreEqual;
}

Dch_Cla_t* Dch_ClassesStart

(

Aig_Man_t *

pAig

)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file dchClass.c.

{
    Dch_Cla_t * p;
    p = ABC_ALLOC( Dch_Cla_t, 1 );
    memset( p, 0, sizeof(Dch_Cla_t) );
    p->pAig         = pAig;
    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
    assert( pAig->pReprs == NULL );
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    return p;
}

void Dch_ClassesStop

(

Dch_Cla_t *

p

)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file dchClass.c.

{
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
    ABC_FREE( p->pId2Class );
    ABC_FREE( p->pClassSizes );
    ABC_FREE( p->pMemClasses );
    ABC_FREE( p );
}

static void Dch_ObjAddClass ( Dch_Cla_t *  p, Aig_Obj_t *  pRepr, Aig_Obj_t **  pClass, int  nSize  )

inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis [Creates one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file dchClass.c.

{
    assert( p->pId2Class[pRepr->Id] == NULL );
    p->pId2Class[pRepr->Id] = pClass; 
    assert( p->pClassSizes[pRepr->Id] == 0 );
    assert( nSize > 1 );
    p->pClassSizes[pRepr->Id] = nSize;
    p->nClasses++;
    p->nLits += nSize - 1;
}

static Aig_Obj_t* Dch_ObjNext ( Aig_Obj_t **  ppNexts, Aig_Obj_t *  pObj  )

inlinestatic

DECLARATIONS ///.

Definition at line 63 of file dchClass.c.

{ return ppNexts[pObj->Id];  }

static Aig_Obj_t** Dch_ObjRemoveClass ( Dch_Cla_t *  p, Aig_Obj_t *  pRepr  )

inlinestatic

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

Synopsis [Removes one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file dchClass.c.

{
    Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
    int nSize;
    assert( pClass != NULL );
    p->pId2Class[pRepr->Id] = NULL; 
    nSize = p->pClassSizes[pRepr->Id];
    assert( nSize > 1 );
    p->nClasses--;
    p->nLits -= nSize - 1;
    p->pClassSizes[pRepr->Id] = 0;
    return pClass;
}

static void Dch_ObjSetNext ( Aig_Obj_t **  ppNexts, Aig_Obj_t *  pObj, Aig_Obj_t *  pNext  )

inlinestatic

Definition at line 64 of file dchClass.c.

{ ppNexts[pObj->Id] = pNext; }