From 255f171f632610eead441e62c7fe4cd4148bb207 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 23 Sep 2012 23:53:12 -0700 Subject: Improving computation of choices from equivalence classes. --- src/aig/gia/gia.h | 12 +- src/aig/gia/giaAig.c | 35 ++-- src/aig/gia/giaAig.h | 1 + src/aig/gia/giaChoice.c | 498 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaEquiv.c | 83 -------- src/aig/gia/giaUtil.c | 49 ----- src/aig/gia/module.make | 1 + 7 files changed, 529 insertions(+), 150 deletions(-) create mode 100644 src/aig/gia/giaChoice.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index ef87c5d5..e9e714ad 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -271,6 +271,7 @@ static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); } +static inline char * Gia_ManName( Gia_Man_t * p ) { return p->pName; } static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); } static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); } static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; } @@ -356,9 +357,10 @@ static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } -static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntGetEntry(p->vLevels, Gia_ObjId(p,pObj)); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } -static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Vec_IntSetEntry(p->vLevels, Gia_ObjId(p,pObj), l); } +static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); } +static inline void Gia_ObjSetLevelId( Gia_Man_t * p, int Id, int l ) { Vec_IntSetEntry(p->vLevels, Id, l); } +static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Gia_ObjSetLevelId( p, Gia_ObjId(p,pObj), l ); } static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); } static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); } @@ -596,7 +598,6 @@ static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { r static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; } static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } -static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } @@ -699,6 +700,9 @@ extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ); extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia ); extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame ); +/*=== giaChoice.c ============================================================*/ +extern void Gia_ManVerifyChoices( Gia_Man_t * p ); +extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ); /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ @@ -760,7 +764,6 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p ); extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); -extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ); extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); @@ -912,7 +915,6 @@ extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_ManHasChoices( Gia_Man_t * p ); -extern void Gia_ManVerifyChoices( Gia_Man_t * p ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index d9a1693c..224d3bda 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -419,18 +419,6 @@ void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) ); } } - -/**Function************************************************************* - - Synopsis [Transfers representatives from pGia to pAig.] - - Description [Assumes that pAig was created from pGia.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ) { Gia_Obj_t * pGiaObj, * pGiaRepr; @@ -470,9 +458,9 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) ); for ( i = 0; i < Gia_ManObjNum(pGia); i++ ) Gia_ObjSetRepr( pGia, i, GIA_VOID ); + // move pointers from GIA to AIG Gia_ManForEachObj( pGia, pObjGia, i ) { -// Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 ); if ( Gia_ObjIsCo(pObjGia) ) continue; assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) ); @@ -490,6 +478,27 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) } pGia->pNexts = Gia_ManDeriveNexts( pGia ); } +void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ) +{ + Aig_Obj_t * pObjAig, * pReprAig; + int i; + assert( pAig->pReprs != NULL ); + assert( pGia->pReprs == NULL ); + assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) ); + pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) ); + for ( i = 0; i < Gia_ManObjNum(pGia); i++ ) + Gia_ObjSetRepr( pGia, i, GIA_VOID ); + Aig_ManForEachObj( pAig, pObjAig, i ) + { + if ( Aig_ObjIsCo(pObjAig) ) + continue; + if ( pAig->pReprs[i] == NULL ) + continue; + pReprAig = pAig->pReprs[i]; + Gia_ObjSetRepr( pGia, Abc_Lit2Var(pObjAig->iData), Abc_Lit2Var(pReprAig->iData) ); + } + pGia->pNexts = Gia_ManDeriveNexts( pGia ); +} /**Function************************************************************* diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index adcf9097..b72f6415 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -59,6 +59,7 @@ extern Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ); extern void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ); extern void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ); extern void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ); +extern void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ); extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ); extern Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars ); extern Gia_Man_t * Gia_ManAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops ); diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c new file mode 100644 index 00000000..373f9104 --- /dev/null +++ b/src/aig/gia/giaChoice.c @@ -0,0 +1,498 @@ +/**CFile**************************************************************** + + FileName [giaChoice.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Normalization of structural choices.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reverse the order of nodes in equiv classes.] + + Description [If the flag is 1, assumed current increasing order ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) +{ + Vec_Int_t * vCollected; + Vec_Int_t * vClass; + int i, k, iRepr, iNode, iPrev; + // collect classes + vCollected = Vec_IntAlloc( 100 ); + Gia_ManForEachClass( p, iRepr ) + { + Vec_IntPush( vCollected, iRepr ); +/* + // check classes + if ( !fNowIncreasing ) + { + iPrev = iRepr; + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + if ( iPrev < iNode ) + { + printf( "Class %d : ", iRepr ); + Gia_ClassForEachObj( p, iRepr, iNode ) + printf( " %d", iNode ); + printf( "\n" ); + break; + } + iPrev = iNode; + } + } +*/ + } + // correct each class + vClass = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vCollected, iRepr, i ) + { + Vec_IntClear( vClass ); + Vec_IntPush( vClass, iRepr ); + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + if ( fNowIncreasing ) + assert( iRepr < iNode ); +// else +// assert( iRepr > iNode ); + Vec_IntPush( vClass, iNode ); + } + if ( !fNowIncreasing ) + Vec_IntSort( vClass, 1 ); +// if ( iRepr == 129720 || iRepr == 129737 ) +// Vec_IntPrint( vClass ); + // reverse the class + iPrev = 0; + iRepr = Vec_IntEntryLast( vClass ); + Vec_IntForEachEntry( vClass, iNode, k ) + { + if ( fNowIncreasing ) + Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr ); + else + Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr ); + Gia_ObjSetNext( p, iNode, iPrev ); + iPrev = iNode; + } + } + Vec_IntFree( vCollected ); + Vec_IntFree( vClass ); + // verify + Gia_ManForEachClass( p, iRepr ) + Gia_ClassForEachObj1( p, iRepr, iNode ) + if ( fNowIncreasing ) + assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode ); + else + assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManVerifyChoices( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, iRepr, iNode, fProb = 0; + assert( p->pReprs ); + + // mark nodes + Gia_ManCleanMark0(p); + Gia_ManForEachClass( p, iRepr ) + Gia_ClassForEachObj1( p, iRepr, iNode ) + { + if ( Gia_ObjIsHead(p, iNode) ) + printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1; + if ( Gia_ManObj( p, iNode )->fMark0 == 1 ) + printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1; + Gia_ManObj( p, iNode )->fMark0 = 1; + } + Gia_ManCleanMark0(p); + + Gia_ManForEachObj( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) ) + printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1; + if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) ) + printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1; + } + else if ( Gia_ObjIsCo(pObj) ) + { + if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) ) + printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1; + } + } + if ( !fProb ) + printf( "GIA with choices is correct.\n" ); +} + +/**Function************************************************************* + + Synopsis [Make sure reprsentative nodes do not have representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCheckReprs( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, fProb = 0; + Gia_ManForEachObj( p, pObj, i ) + { + if ( !Gia_ObjHasRepr(p, i) ) + continue; + if ( !Gia_ObjIsAnd(pObj) ) + printf( "Obj %d is not an AND but it has a repr %d.\n", i, Gia_ObjRepr(p, i) ), fProb = 1; + else if ( Gia_ObjHasRepr( p, Gia_ObjRepr(p, i) ) ) + printf( "Obj %d has repr %d with a repr %d.\n", i, Gia_ObjRepr(p, i), Gia_ObjRepr(p, Gia_ObjRepr(p, i)) ), fProb = 1; + } + if ( !fProb ) + printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) ); +} + +/**Function************************************************************* + + Synopsis [Find minimum level of each node using representatives.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManMinLevelRepr_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + int levMin, levCur, objId, reprId; + // skip visited nodes + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return Gia_ObjLevel(p, pObj); + Gia_ObjSetTravIdCurrent(p, pObj); + // skip CI nodes + if ( Gia_ObjIsCi(pObj) ) + return Gia_ObjLevel(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + objId = Gia_ObjId(p, pObj); + if ( Gia_ObjIsNone(p, objId) ) + { + // not part of the equivalence class + Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin1(pObj) ); + Gia_ObjSetAndLevel( p, pObj ); + return Gia_ObjLevel(p, pObj); + } + // has equivalences defined + assert( Gia_ObjHasRepr(p, objId) || Gia_ObjIsHead(p, objId) ); + reprId = Gia_ObjHasRepr(p, objId) ? Gia_ObjRepr(p, objId) : objId; + // iterate through objects + levMin = ABC_INFINITY; + Gia_ClassForEachObj( p, reprId, objId ) + { + levCur = Gia_ManMinLevelRepr_rec( p, Gia_ManObj(p, objId) ); + levMin = Abc_MinInt( levMin, levCur ); + } + assert( levMin < ABC_INFINITY ); + // assign minimum level to all + Gia_ClassForEachObj( p, reprId, objId ) + Gia_ObjSetLevelId( p, objId, levMin ); + return levMin; +} +int Gia_ManMinLevelRepr( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, LevelCur, LevelMax = 0; + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); + Gia_ManIncrementTravId( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + assert( !Gia_ObjIsConst(p, i) ); + LevelCur = Gia_ManMinLevelRepr_rec( p, pObj ); + LevelMax = Abc_MaxInt( LevelMax, LevelCur ); + } + printf( "Max level %d\n", LevelMax ); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Returns mapping of each old repr into new repr.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Gia_ManFindMinLevelMap( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int reprId, objId, levFan0, levFan1; + int levMin, levMinOld, levMax, reprBest; + int * pReprMap, * pMinLevels, iFanin; + int i, fChange = 1; + + Gia_ManLevelNum( p ); + pMinLevels = ABC_ALLOC( int, Gia_ManObjNum(p) ); + while ( fChange ) + { + fChange = 0; + // clean min-levels + memset( pMinLevels, 0xFF, sizeof(int) * Gia_ManObjNum(p) ); + // for each class find min level + Gia_ManForEachClass( p, reprId ) + { + levMin = ABC_INFINITY; + Gia_ClassForEachObj( p, reprId, objId ) + levMin = Abc_MinInt( levMin, Gia_ObjLevelId(p, objId) ); + assert( levMin >= 0 && levMin < ABC_INFINITY ); + Gia_ClassForEachObj( p, reprId, objId ) + { + assert( pMinLevels[objId] == -1 ); + pMinLevels[objId] = levMin; + } + } + // recompute levels + levMax = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + iFanin = Gia_ObjFaninId0(pObj, i); + if ( Gia_ObjIsNone(p, iFanin) ) + levFan0 = Gia_ObjLevelId(p, iFanin); + else if ( Gia_ObjIsConst(p, iFanin) ) + levFan0 = 0; + else + { + assert( Gia_ObjIsClass( p, iFanin ) ); + assert( pMinLevels[iFanin] >= 0 ); + levFan0 = pMinLevels[iFanin]; + } + + iFanin = Gia_ObjFaninId1(pObj, i); + if ( Gia_ObjIsNone(p, iFanin) ) + levFan1 = Gia_ObjLevelId(p, iFanin); + else if ( Gia_ObjIsConst(p, iFanin) ) + levFan1 = 0; + else + { + assert( Gia_ObjIsClass( p, iFanin ) ); + assert( pMinLevels[iFanin] >= 0 ); + levFan1 = pMinLevels[iFanin]; + } + levMinOld = Gia_ObjLevelId(p, i); + levMin = 1 + Abc_MaxInt( levFan0, levFan1 ); + Gia_ObjSetLevelId( p, i, levMin ); + assert( levMin <= levMinOld ); + if ( levMin < levMinOld ) + fChange = 1; + levMax = Abc_MaxInt( levMax, levMin ); + } + printf( "%d ", levMax ); + } + ABC_FREE( pMinLevels ); + printf( "\n" ); + + // create repr map + pReprMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjIsConst(p, i) ) + pReprMap[i] = 0; + Gia_ManForEachClass( p, reprId ) + { + // find min-level repr + reprBest = -1; + levMin = ABC_INFINITY; + Gia_ClassForEachObj( p, reprId, objId ) + if ( levMin > Gia_ObjLevelId(p, objId) ) + { + levMin = Gia_ObjLevelId(p, objId); + reprBest = objId; + } + assert( reprBest > 0 ); + Gia_ClassForEachObj( p, reprId, objId ) + pReprMap[objId] = reprBest; + } + return pReprMap; +} + + + +/**Function************************************************************* + + Synopsis [Find terminal AND nodes] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManDanglingAndNodes( Gia_Man_t * p ) +{ + Vec_Int_t * vTerms; + Gia_Obj_t * pObj; + int i; + Gia_ManCleanMark0( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + Gia_ObjFanin0(pObj)->fMark0 = 1; + Gia_ObjFanin1(pObj)->fMark1 = 1; + } + vTerms = Vec_IntAlloc( 1000 ); + Gia_ManForEachAnd( p, pObj, i ) + if ( !pObj->fMark0 ) + Vec_IntPush( vTerms, i ); + Gia_ManCleanMark0( p ); + return vTerms; +} + +/**Function************************************************************* + + Synopsis [Reconstruct AIG starting with terminals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManRebuidRepr_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprMap ) +{ + int objId, reprLit = -1; + if ( ~pObj->Value ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + objId = Gia_ObjId( p, pObj ); + if ( Gia_ObjIsClass(p, objId) ) + { + assert( pReprMap[objId] > 0 ); + reprLit = Gia_ManRebuidRepr_rec( pNew, p, Gia_ManObj(p, pReprMap[objId]), pReprMap ); + assert( reprLit > 1 ); + } + else + assert( Gia_ObjIsNone(p, objId) ); + Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin0(pObj), pReprMap ); + Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin1(pObj), pReprMap ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + assert( reprLit != (int)pObj->Value ); + if ( reprLit > 1 ) + pNew->pReprs[ Abc_Lit2Var(pObj->Value) ].iRepr = Abc_Lit2Var(reprLit); + return pObj->Value; +} +Gia_Man_t * Gia_ManRebuidRepr( Gia_Man_t * p, int * pReprMap ) +{ + Vec_Int_t * vTerms; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + vTerms = Gia_ManDanglingAndNodes( p ); + Gia_ManForEachObjVec( vTerms, p, pObj, i ) + Gia_ManRebuidRepr_rec( pNew, p, pObj, pReprMap ); + Vec_IntFree( vTerms ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Gia_ManNormalizeChoices( Aig_Man_t * pAig ) +{ + int * pReprMap; + Aig_Man_t * pNew; + Gia_Man_t * pGia, * pTemp; + // create GIA with representatives + assert( Aig_ManRegNum(pAig) == 0 ); + assert( pAig->pReprs != NULL ); + pGia = Gia_ManFromAigSimple( pAig ); + Gia_ManReprFromAigRepr2( pAig, pGia ); + // verify that representatives are correct + Gia_ManCheckReprs( pGia ); + // find min-level repr for each class + pReprMap = Gia_ManFindMinLevelMap( pGia ); + // reconstruct using correct order + pGia = Gia_ManRebuidRepr( pTemp = pGia, pReprMap ); + Gia_ManStop( pTemp ); + ABC_FREE( pReprMap ); + // create choices + + // verify that choices are correct +// Gia_ManVerifyChoices( pGia ); + // copy the result back into AIG + pNew = Gia_ManToAigSimple( pGia ); + Gia_ManReprToAigRepr( pNew, pGia ); + return pNew; +} +void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig ) +{ + Aig_Man_t * pNew = Gia_ManNormalizeChoices( pAig ); + Aig_ManStop( pNew ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index b9557600..2cbdb75f 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -345,89 +345,6 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) } } -/**Function************************************************************* - - Synopsis [Reverse the order of nodes in equiv classes.] - - Description [If the flag is 1, assumed current increasing order ] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) -{ - Vec_Int_t * vCollected; - Vec_Int_t * vClass; - int i, k, iRepr, iNode, iPrev; - // collect classes - vCollected = Vec_IntAlloc( 100 ); - Gia_ManForEachClass( p, iRepr ) - { - Vec_IntPush( vCollected, iRepr ); -/* - // check classes - if ( !fNowIncreasing ) - { - iPrev = iRepr; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - if ( iPrev < iNode ) - { - printf( "Class %d : ", iRepr ); - Gia_ClassForEachObj( p, iRepr, iNode ) - printf( " %d", iNode ); - printf( "\n" ); - break; - } - iPrev = iNode; - } - } -*/ - } - // correct each class - vClass = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vCollected, iRepr, i ) - { - Vec_IntClear( vClass ); - Vec_IntPush( vClass, iRepr ); - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - if ( fNowIncreasing ) - assert( iRepr < iNode ); -// else -// assert( iRepr > iNode ); - Vec_IntPush( vClass, iNode ); - } - if ( !fNowIncreasing ) - Vec_IntSort( vClass, 1 ); -// if ( iRepr == 129720 || iRepr == 129737 ) -// Vec_IntPrint( vClass ); - // reverse the class - iPrev = 0; - iRepr = Vec_IntEntryLast( vClass ); - Vec_IntForEachEntry( vClass, iNode, k ) - { - if ( fNowIncreasing ) - Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr ); - else - Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr ); - Gia_ObjSetNext( p, iNode, iPrev ); - iPrev = iNode; - } - } - Vec_IntFree( vCollected ); - Vec_IntFree( vClass ); - // verify - Gia_ManForEachClass( p, iRepr ) - Gia_ClassForEachObj1( p, iRepr, iNode ) - if ( fNowIncreasing ) - assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode ); - else - assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode ); -} - /**Function************************************************************* Synopsis [Returns representative node.] diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 499f9293..5f443dc8 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -979,55 +979,6 @@ int Gia_ManHasChoices( Gia_Man_t * p ) return 1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManVerifyChoices( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int i, iRepr, iNode, fProb = 0; - assert( p->pReprs ); - - // mark nodes - Gia_ManCleanMark0(p); - Gia_ManForEachClass( p, iRepr ) - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - if ( Gia_ObjIsHead(p, iNode) ) - printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1; - if ( Gia_ManObj( p, iNode )->fMark0 == 1 ) - printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1; - Gia_ManObj( p, iNode )->fMark0 = 1; - } - Gia_ManCleanMark0(p); - - Gia_ManForEachObj( p, pObj, i ) - { - if ( Gia_ObjIsAnd(pObj) ) - { - if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) ) - printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1; - if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) ) - printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1; - } - else if ( Gia_ObjIsCo(pObj) ) - { - if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) ) - printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1; - } - } - if ( !fProb ) - printf( "GIA with choices is correct.\n" ); -} - /**Function************************************************************* Synopsis [Returns 1 if AIG has dangling nodes.] diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 89af261a..d35dcde2 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -5,6 +5,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaCCof.c \ src/aig/gia/giaCex.c \ src/aig/gia/giaCexMin.c \ + src/aig/gia/giaChoice.c \ src/aig/gia/giaCof.c \ src/aig/gia/giaCSatOld.c \ src/aig/gia/giaCSat.c \ -- cgit v1.2.3