From 7d29663720b02b02ceaae5b75fb8fe05ba4aae73 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2012 18:25:41 -0700 Subject: Fixed several important problems in choice computation (command 'dch'). --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaChoice.c | 362 +++++++++--------------------------------------- src/aig/gia/giaUtil.c | 91 ------------ 3 files changed, 68 insertions(+), 387 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e9e714ad..0c98e94d 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -703,6 +703,7 @@ extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, i /*=== giaChoice.c ============================================================*/ extern void Gia_ManVerifyChoices( Gia_Man_t * p ); extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ); +extern int Gia_ManHasChoices( Gia_Man_t * p ); /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ @@ -914,7 +915,6 @@ extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); 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 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/giaChoice.c b/src/aig/gia/giaChoice.c index 373f9104..a1d9e325 100644 --- a/src/aig/gia/giaChoice.c +++ b/src/aig/gia/giaChoice.c @@ -51,28 +51,7 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) // 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 ) @@ -83,14 +62,12 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) { if ( fNowIncreasing ) assert( iRepr < iNode ); -// else -// 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 ); +// if ( !fNowIncreasing ) +// Vec_IntSort( vClass, 1 ); // reverse the class iPrev = 0; iRepr = Vec_IntEntryLast( vClass ); @@ -192,9 +169,10 @@ void Gia_ManCheckReprs( Gia_Man_t * p ) printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) ); } + /**Function************************************************************* - Synopsis [Find minimum level of each node using representatives.] + Synopsis [Returns 1 if AIG has choices.] Description [] @@ -203,290 +181,84 @@ void Gia_ManCheckReprs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_ManMinLevelRepr_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +int Gia_ManHasChoices( Gia_Man_t * p ) { - 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) ) + Gia_Obj_t * pObj; + int i, Counter1 = 0, Counter2 = 0; + int nFailNoRepr = 0; + int nFailHaveRepr = 0; + int nChoiceNodes = 0; + int nChoices = 0; + if ( p->pReprs == NULL || p->pNexts == NULL ) + return 0; + // check if there are any representatives + Gia_ManForEachObj( p, pObj, i ) { - // 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); + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) + { +// printf( "%d ", i ); + Counter1++; + } +// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) +// Counter2++; } - // 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 ) +// printf( "\n" ); + Gia_ManForEachObj( p, pObj, i ) { - levCur = Gia_ManMinLevelRepr_rec( p, Gia_ManObj(p, objId) ); - levMin = Abc_MinInt( levMin, levCur ); +// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) +// Counter1++; + if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) + { +// printf( "%d ", i ); + Counter2++; + } } - 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 ) +// printf( "\n" ); + if ( Counter1 == 0 ) { - assert( !Gia_ObjIsConst(p, i) ); - LevelCur = Gia_ManMinLevelRepr_rec( p, pObj ); - LevelMax = Abc_MaxInt( LevelMax, LevelCur ); + printf( "Warning: AIG has repr data-strucure but not reprs.\n" ); + return 0; } - 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 ) + printf( "%d nodes have reprs.\n", Counter1 ); + printf( "%d nodes have nexts.\n", Counter2 ); + // check if there are any internal nodes without fanout + // make sure all nodes without fanout have representatives + // make sure all nodes with fanout have no representatives + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) { - fChange = 0; - // clean min-levels - memset( pMinLevels, 0xFF, sizeof(int) * Gia_ManObjNum(p) ); - // for each class find min level - Gia_ManForEachClass( p, reprId ) + if ( Gia_ObjRefs(p, pObj) == 0 ) { - 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; - } + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL ) + nFailNoRepr++; + else + nChoices++; } - // recompute levels - levMax = 0; - Gia_ManForEachAnd( p, pObj, i ) + else { - 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 ); + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL ) + nFailHaveRepr++; + if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL ) + nChoiceNodes++; } - 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; + if ( Gia_ObjReprObj( p, i ) ) + assert( Gia_ObjRepr(p, i) < i ); } - 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 ) + if ( nChoices == 0 ) + return 0; + if ( nFailNoRepr ) { - Gia_ObjFanin0(pObj)->fMark0 = 1; - Gia_ObjFanin1(pObj)->fMark1 = 1; + printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr ); +// return 0; } - 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) ) + if ( nFailHaveRepr ) { - assert( pReprMap[objId] > 0 ); - reprLit = Gia_ManRebuidRepr_rec( pNew, p, Gia_ManObj(p, pReprMap[objId]), pReprMap ); - assert( reprLit > 1 ); + printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr ); +// return 0; } - 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 ); +// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices ); + return 1; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5f443dc8..e4a4dd09 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -888,97 +888,6 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ) return ConeSize1; } -/**Function************************************************************* - - Synopsis [Returns 1 if AIG has choices.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManHasChoices( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int i, Counter1 = 0, Counter2 = 0; - int nFailNoRepr = 0; - int nFailHaveRepr = 0; - int nChoiceNodes = 0; - int nChoices = 0; - if ( p->pReprs == NULL || p->pNexts == NULL ) - return 0; - // check if there are any representatives - Gia_ManForEachObj( p, pObj, i ) - { - if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) - { -// printf( "%d ", i ); - Counter1++; - } -// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) -// Counter2++; - } -// printf( "\n" ); - Gia_ManForEachObj( p, pObj, i ) - { -// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) -// Counter1++; - if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) - { -// printf( "%d ", i ); - Counter2++; - } - } -// printf( "\n" ); - if ( Counter1 == 0 ) - { - printf( "Warning: AIG has repr data-strucure but not reprs.\n" ); - return 0; - } - printf( "%d nodes have reprs.\n", Counter1 ); - printf( "%d nodes have nexts.\n", Counter2 ); - // check if there are any internal nodes without fanout - // make sure all nodes without fanout have representatives - // make sure all nodes with fanout have no representatives - ABC_FREE( p->pRefs ); - Gia_ManCreateRefs( p ); - Gia_ManForEachAnd( p, pObj, i ) - { - if ( Gia_ObjRefs(p, pObj) == 0 ) - { - if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL ) - nFailNoRepr++; - else - nChoices++; - } - else - { - if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL ) - nFailHaveRepr++; - if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL ) - nChoiceNodes++; - } - if ( Gia_ObjReprObj( p, i ) ) - assert( Gia_ObjRepr(p, i) < i ); - } - if ( nChoices == 0 ) - return 0; - if ( nFailNoRepr ) - { - printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr ); -// return 0; - } - if ( nFailHaveRepr ) - { - printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr ); -// return 0; - } -// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices ); - return 1; -} - /**Function************************************************************* Synopsis [Returns 1 if AIG has dangling nodes.] -- cgit v1.2.3