llb1Man.c File Reference

#include "llbInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Llb_ManPrepareVarMap (Llb_Man_t *p)
	DECLARATIONS ///. More...
void	Llb_ManPrepareVarLimits (Llb_Man_t *p)
void	Llb_ManStop (Llb_Man_t *p)
Llb_Man_t *	Llb_ManStart (Aig_Man_t *pAigGlo, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)

Function Documentation

void Llb_ManPrepareVarLimits

(

Llb_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file llb1Man.c.

{
    Llb_Grp_t * pGroup;
    Aig_Obj_t * pVar;
    int i, k;
    assert( p->vVarBegs == NULL );
    assert( p->vVarEnds == NULL );
    p->vVarEnds = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); 
    p->vVarBegs = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); 
    Vec_IntFill( p->vVarBegs, Aig_ManObjNumMax(p->pAig), p->pMatrix->nCols );

    for ( i = 0; i < p->pMatrix->nCols; i++ )
    {
        pGroup = p->pMatrix->pColGrps[i];

        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
                Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
                Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );

        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
                Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
                Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
    }
}

ABC_NAMESPACE_IMPL_START void Llb_ManPrepareVarMap

(

Llb_Man_t *

p

)

DECLARATIONS ///.

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

FileName [llb1Man.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Reachability manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

llb1Man.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file llb1Man.c.

{
    Aig_Obj_t * pObjLi, * pObjLo;
    int i, iVarLi, iVarLo;
    assert( p->vNs2Glo == NULL );
    assert( p->vCs2Glo == NULL );
    assert( p->vGlo2Cs == NULL );
    assert( p->vGlo2Ns == NULL );
    p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
    p->vCs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
    p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
    p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
    {
        iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi));
        iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
        assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) );
        assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) );
        Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
        Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
        Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
        Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
    }
    // add mapping of the PIs
    Saig_ManForEachPi( p->pAig, pObjLo, i )
    {
        iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
        Vec_IntWriteEntry( p->vCs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
        Vec_IntWriteEntry( p->vNs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
    }
}

Llb_Man_t* Llb_ManStart	(	Aig_Man_t *	pAigGlo,
		Aig_Man_t *	pAig,
		Gia_ParLlb_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file llb1Man.c.

{
    Llb_Man_t * p;
    Aig_ManCleanMarkA( pAig );
    p = ABC_CALLOC( Llb_Man_t, 1 );
    p->pAigGlo  = pAigGlo;
    p->pPars    = pPars;
    p->pAig     = pAig;
    p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots );
    p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
    p->vRings   = Vec_PtrAlloc( 100 );
    Llb_ManPrepareVarMap( p );
    Llb_ManPrepareGroups( p );
    Aig_ManCleanMarkA( pAig );
    p->pMatrix = Llb_MtrCreate( p );
    p->pMatrix->pMan = p;
    return p;
}

void Llb_ManStop

(

Llb_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file llb1Man.c.

{
    Llb_Grp_t * pGrp;
    DdNode * bTemp;
    int i;

//    Vec_IntFreeP( &p->vMem );
//    Vec_PtrFreeP( &p->vTops );
//    Vec_PtrFreeP( &p->vBots );
//    Vec_VecFreeP( (Vec_Vec_t **)&p->vCuts );

    if ( p->pMatrix )
        Llb_MtrFree( p->pMatrix );
    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i )
        Llb_ManGroupStop( pGrp );
    if ( p->dd )
    {
//        printf( "Manager dd\n" );
        Extra_StopManager( p->dd );
    }
    if ( p->ddG )
    {
//        printf( "Manager ddG\n" );
        if ( p->ddG->bFunc )
            Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc ); 
        Extra_StopManager( p->ddG );
    }
    if ( p->ddR )
    {
//        printf( "Manager ddR\n" );
        if ( p->ddR->bFunc )
            Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc ); 
        Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
            Cudd_RecursiveDeref( p->ddR, bTemp );
        Extra_StopManager( p->ddR );
    }
    Aig_ManStop( p->pAig );
    Vec_PtrFreeP( &p->vGroups );
    Vec_IntFreeP( &p->vVar2Obj );
    Vec_IntFreeP( &p->vObj2Var );
    Vec_IntFreeP( &p->vVarBegs );
    Vec_IntFreeP( &p->vVarEnds );
    Vec_PtrFreeP( &p->vRings  );
    Vec_IntFreeP( &p->vNs2Glo );
    Vec_IntFreeP( &p->vCs2Glo );
    Vec_IntFreeP( &p->vGlo2Cs );
    Vec_IntFreeP( &p->vGlo2Ns );
//    Vec_IntFreeP( &p->vHints );
    ABC_FREE( p );
}