From ecd14d4daf479f2cd2f630095b7370a48465dac1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 15 Feb 2012 18:40:05 -0800 Subject: Isomorphism checking code. --- src/aig/gia/giaIso.c | 665 ++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 579 insertions(+), 86 deletions(-) (limited to 'src/aig/gia/giaIso.c') diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index aca4ba99..c0feb735 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -27,56 +27,47 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Gia_IsoLnk_t_ Gia_IsoLnk_t; -struct Gia_IsoLnk_t_ -{ - int iBeg; - int nSize; - int iPrev; - int iNext; -}; - -typedef struct Gia_IsoLst_t_ Gia_IsoLst_t; -struct Gia_IsoLst_t_ -{ - int iHead; - int iTail; -}; - typedef struct Gia_IsoMan_t_ Gia_IsoMan_t; struct Gia_IsoMan_t_ { Gia_Man_t * pGia; int nObjs; + int nUniques; // collected info Vec_Int_t * vLevels; Vec_Int_t * vFin0Levs; Vec_Int_t * vFin1Levs; + Vec_Int_t * vFinSig; Vec_Int_t * vFoutPos; Vec_Int_t * vFoutNeg; - Vec_Int_t * vFinSig; // sorting structures Vec_Int_t * vMap; Vec_Int_t * vSeens; Vec_Int_t * vCounts; Vec_Int_t * vResult; // fanout representation - Vec_Int_t * vFanouts; + Vec_Int_t * vFanout; + Vec_Int_t * vFanout2; // class representation Vec_Int_t * vItems; - Gia_IsoLst_t List; - Gia_IsoLnk_t * pLinks; - Gia_IsoLnk_t * pLinksFree; - int nLinksUsed; - int nLinksAlloc; + Vec_Int_t * vUniques; + Vec_Int_t * vClass; + Vec_Int_t * vClass2; + Vec_Int_t * vClassNew; + Vec_Int_t * vLevelLim; // temporary storage Vec_Ptr_t * vRoots; Vec_Int_t * vUsed; Vec_Int_t * vRefs; // results Vec_Ptr_t * vResults; + Vec_Int_t * vPermCis; + Vec_Int_t * vPermCos; }; +static inline int * Gia_IsoFanoutVec( Vec_Int_t * p, int Id ) { return Vec_IntEntryP( p, Vec_IntEntry(p, Id) ); } + + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -102,9 +93,9 @@ Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia ) p->vLevels = Vec_IntAlloc( p->nObjs ); p->vFin0Levs = Vec_IntAlloc( p->nObjs ); p->vFin1Levs = Vec_IntAlloc( p->nObjs ); + p->vFinSig = Vec_IntAlloc( p->nObjs ); p->vFoutPos = Vec_IntAlloc( p->nObjs ); p->vFoutNeg = Vec_IntAlloc( p->nObjs ); - p->vFinSig = Vec_IntAlloc( p->nObjs ); // sorting structures p->vMap = Vec_IntStartFull( 2*p->nObjs ); p->vSeens = Vec_IntAlloc( p->nObjs ); @@ -112,14 +103,22 @@ Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia ) p->vResult = Vec_IntAlloc( p->nObjs ); // class representation p->vItems = Vec_IntAlloc( p->nObjs ); + p->vUniques = Vec_IntAlloc( p->nObjs ); + p->vClass = Vec_IntAlloc( p->nObjs/2 ); + p->vClass2 = Vec_IntAlloc( p->nObjs/2 ); + p->vClassNew = Vec_IntAlloc( p->nObjs/2 ); + p->vLevelLim = Vec_IntAlloc( 1000 ); // fanout representation - p->vFanouts = Vec_IntAlloc( 6 * p->nObjs ); + p->vFanout = Vec_IntAlloc( 6 * p->nObjs ); + p->vFanout2 = Vec_IntAlloc( 0 ); // temporary storage p->vRoots = Vec_PtrAlloc( 1000 ); p->vUsed = Vec_IntAlloc( p->nObjs ); p->vRefs = Vec_IntAlloc( p->nObjs ); // results p->vResults = Vec_PtrAlloc( Gia_ManPoNum(pGia) ); + p->vPermCis = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vPermCos = Vec_IntAlloc( Gia_ManCoNum(pGia) ); return p; } void Gia_IsoManStop( Gia_IsoMan_t * p ) @@ -128,9 +127,9 @@ void Gia_IsoManStop( Gia_IsoMan_t * p ) Vec_IntFree( p->vLevels ); Vec_IntFree( p->vFin0Levs ); Vec_IntFree( p->vFin1Levs ); + Vec_IntFree( p->vFinSig ); Vec_IntFree( p->vFoutPos ); Vec_IntFree( p->vFoutNeg ); - Vec_IntFree( p->vFinSig ); // sorting structures Vec_IntFree( p->vMap ); Vec_IntFree( p->vSeens ); @@ -138,13 +137,22 @@ void Gia_IsoManStop( Gia_IsoMan_t * p ) Vec_IntFree( p->vResult ); // class representation Vec_IntFree( p->vItems ); + Vec_IntFree( p->vUniques ); + Vec_IntFree( p->vClass ); + Vec_IntFree( p->vClass2 ); + Vec_IntFree( p->vClassNew ); + Vec_IntFree( p->vLevelLim ); // fanout representation - Vec_IntFree( p->vFanouts ); + Vec_IntFree( p->vFanout ); + Vec_IntFree( p->vFanout2 ); // temporary storage Vec_IntFree( p->vRefs ); Vec_IntFree( p->vUsed ); Vec_PtrFree( p->vRoots ); + // results // Vec_PtrFree( p->vResults ); + Vec_IntFree( p->vPermCis ); + Vec_IntFree( p->vPermCos ); ABC_FREE( p ); } @@ -259,8 +267,8 @@ void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, V pOff = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, pObj->Value) ); if ( Gia_ObjIsAnd(pObj) ) { - pOff0 = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, Gia_ObjFanin0(pObj)->Value) ); - pOff1 = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, Gia_ObjFanin1(pObj)->Value) ); + pOff0 = Gia_IsoFanoutVec( vFanout, Gia_ObjFanin0(pObj)->Value ); + pOff1 = Gia_IsoFanoutVec( vFanout, Gia_ObjFanin1(pObj)->Value ); pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); pOff0[1+(*pOff0)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC0(pObj) ); @@ -270,15 +278,15 @@ void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, V else if ( Gia_ObjIsRo(p, pObj) ) { pObjRi = Gia_ObjRoToRi(p, pObj); - pOff0 = Vec_IntEntryP( vFanout, Vec_IntEntry(vFanout, Gia_ObjFanin0(pObjRi)->Value) ); - pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); - pOff0[1+(*pOff0)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC0(pObj) ); + pOff0 = Gia_IsoFanoutVec( vFanout, Gia_ObjFanin0(pObjRi)->Value ); + pOff[1+(*pOff)++] = Abc_Var2Lit( Gia_ObjFanin0(pObjRi)->Value, Gia_ObjFaninC0(pObjRi) ); + pOff0[1+(*pOff0)++] = Abc_Var2Lit( pObj->Value, Gia_ObjFaninC0(pObjRi) ); } } // verify Gia_ManForEachObjVec( vUsed, p, pObj, i ) { - nOffset = Vec_IntEntry( vFanout, Vec_IntEntry(vFanout, pObj->Value) ); + nOffset = *Gia_IsoFanoutVec( vFanout, pObj->Value ); if ( Gia_ObjIsAnd(pObj) ) nOffset -= 2; else if ( Gia_ObjIsRo(p, pObj) ) @@ -287,6 +295,75 @@ void Gia_IsoCreateFanout( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vRefs, V } } +/**Function************************************************************* + + Synopsis [Add fanouts of a new singleton object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_IsoAddSingletonFanouts( Gia_IsoMan_t * p, int Item, int Unique ) +{ + int i, * pFan, * pFan2; + pFan = Gia_IsoFanoutVec( p->vFanout, Item ); + for ( i = 0; i < pFan[0]; i++ ) + { + if ( Vec_IntEntry( p->vUniques, Abc_Lit2Var(pFan[1+i]) ) >= 0 ) + continue; + pFan2 = Gia_IsoFanoutVec( p->vFanout2, Abc_Lit2Var(pFan[1+i]) ); + pFan2[1+(*pFan2)++] = Abc_Var2Lit( Unique, Abc_LitIsCompl(pFan[1+i]) ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_IsoCreateFanout2( Gia_IsoMan_t * p ) +{ + int i, Entry, nOffset, nFanouts = 0, nLeftover = 0; + assert( Vec_IntSize(p->vFanout2) == 0 ); + // count the number of fanouts and objects remaining + Vec_IntForEachEntry( p->vUniques, Entry, i ) + { + if ( Entry >= 0 ) + continue; + nLeftover++; + nFanouts += *Gia_IsoFanoutVec(p->vFanout, i); + } + assert( nLeftover + p->nUniques == Vec_IntSize(p->vUsed) ); + // assign the fanouts + nOffset = Vec_IntSize(p->vUsed); + Vec_IntGrowResize( p->vFanout2, Vec_IntSize(p->vUsed) + 2 * nLeftover + nFanouts ); + Vec_IntForEachEntry( p->vUniques, Entry, i ) + { + if ( Entry >= 0 ) + continue; + Vec_IntWriteEntry( p->vFanout2, i, nOffset ); + Vec_IntWriteEntry( p->vFanout2, nOffset, 0 ); + nOffset += 2 + *Gia_IsoFanoutVec(p->vFanout, i); + } + assert( nOffset == Vec_IntSize(p->vUsed) + 2 * nLeftover + nFanouts ); + // add currently available items + Vec_IntForEachEntry( p->vUniques, Entry, i ) + { + if ( Entry == -1 ) + continue; + Gia_IsoAddSingletonFanouts( p, i, Entry ); + } +} + /**Function************************************************************* Synopsis [] @@ -306,8 +383,8 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p ) Vec_IntClear( p->vFin0Levs ); Vec_IntClear( p->vFin1Levs ); Vec_IntClear( p->vFinSig ); - Vec_IntFill( p->vFoutPos, p->nObjs, 0 ); - Vec_IntFill( p->vFoutNeg, p->nObjs, 0 ); + Vec_IntFill( p->vFoutPos, Vec_IntSize(p->vUsed), 0 ); + Vec_IntFill( p->vFoutNeg, Vec_IntSize(p->vUsed), 0 ); Gia_ManForEachObjVec( p->vUsed, p->pGia, pObj, i ) { if ( Gia_ObjIsAnd(pObj) ) @@ -338,7 +415,7 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p ) { pObjRi = Gia_ObjRoToRi(p->pGia, pObj); Vec_IntPush( p->vLevels, 0 ); - Vec_IntPush( p->vFin0Levs, 1 ); + Vec_IntPush( p->vFin0Levs, 1 ); // not ready yet! Vec_IntPush( p->vFin1Levs, 0 ); Vec_IntPush( p->vFinSig, Gia_ObjFaninC0(pObjRi) ); Vec_IntAddToEntry( Gia_ObjFaninC0(pObjRi) ? p->vFoutNeg : p->vFoutPos, Gia_ObjFanin0(pObjRi)->Value, 1 ); @@ -359,7 +436,11 @@ void Gia_IsoCreateSigs( Gia_IsoMan_t * p ) } else assert( 0 ); } - // create items + assert( Vec_IntSize( p->vLevels ) == Vec_IntSize(p->vUsed) ); + assert( Vec_IntSize( p->vFin0Levs ) == Vec_IntSize(p->vUsed) ); + assert( Vec_IntSize( p->vFin1Levs ) == Vec_IntSize(p->vUsed) ); + assert( Vec_IntSize( p->vFinSig ) == Vec_IntSize(p->vUsed) ); + // prepare items Vec_IntClear( p->vItems ); for ( i = 0; i < Vec_IntSize(p->vUsed); i++ ) Vec_IntPush( p->vItems, i ); @@ -393,8 +474,9 @@ void Gia_IsoSortStats( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, // collect places Vec_IntClear( vSeens ); Vec_IntClear( vCounts ); - Vec_IntForEachEntry( vCosts, Entry, i ) + Vec_IntForEachEntry( vItems, Entry, i ) { + Entry = Vec_IntEntry(vCosts, Entry); Place = Vec_IntEntry(vMap, Entry); if ( Place == -1 ) { @@ -444,25 +526,56 @@ void Gia_IsoSortStats( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, SeeAlso [] ***********************************************************************/ -void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, Vec_Int_t * vSeens, Vec_Int_t * vCounts, Vec_Int_t * vResult ) +Vec_Int_t * Gia_IsoCreateStats( Gia_IsoMan_t * p, int iPo ) +{ + Vec_Int_t * vStats = Vec_IntAlloc( 1000 ); + Gia_IsoCollectUsed( p->pGia, iPo, p->vUsed, p->vRoots ); + Gia_IsoSortStats( p->vItems, p->vLevels, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); + Gia_IsoSortStats( p->vItems, p->vFin0Levs, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); + Gia_IsoSortStats( p->vItems, p->vFin1Levs, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); + Gia_IsoSortStats( p->vItems, p->vFoutPos, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); + Gia_IsoSortStats( p->vItems, p->vFoutNeg, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); + Gia_IsoSortStats( p->vItems, p->vFinSig, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vStats, p->vResult ); + Gia_IsoCleanUsed( p->pGia, p->vUsed ); + return vStats; +} + + + + +/**Function************************************************************* + + Synopsis [Sorting an array of entries.] + + Description [This procedure can have the following outcomes: + - There is no refinement (the class remains unchanged). + - There is complete refinement (all elements became singletons) + - There is partial refinement (some new classes and some singletons) + The permutes set of items if returned in vItems.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, + Vec_Int_t * vSeens, Vec_Int_t * vCounts, Vec_Int_t * vResult, + Vec_Int_t * vClassNew ) { - int i, Entry, Place, Counter; + int i, Entry, Entry0, Place, Counter; // assumes vCosts are between 0 and Vec_IntSize(vMap) // assumes vMap is clean and leaves it clean assert( Vec_IntSize(vItems) > 1 ); - if ( Vec_IntSize(vItems) < 15 ) - { - Vec_IntGrowResize( vResult, Vec_IntSize(vItems) ); - memmove( Vec_IntArray(vResult), Vec_IntArray(vItems), sizeof(int) * Vec_IntSize(vItems) ); - Vec_IntSelectSortCost( Vec_IntArray(vResult), Vec_IntSize(vItems), vCosts ); - return; - } + + // prepare return values + Vec_IntClear( vClassNew ); // collect places Vec_IntClear( vSeens ); Vec_IntClear( vCounts ); - Vec_IntForEachEntry( vCosts, Entry, i ) + Vec_IntForEachEntry( vItems, Entry0, i ) { + Entry = Vec_IntEntry(vCosts, Entry0); Place = Vec_IntEntry(vMap, Entry); if ( Place == -1 ) { @@ -474,35 +587,159 @@ void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, V Vec_IntAddToEntry( vCounts, Place, 1 ); } - // sort places - Vec_IntSort( vSeens, 0 ); - - // set the map to point to the place in the final array - Counter = 0; - Vec_IntForEachEntry( vSeens, Entry, i ) + // check if refinement is happening + if ( Vec_IntSize(vSeens) == 1 ) // there is no refinement { - Place = Vec_IntEntry( vMap, Entry ); - Vec_IntWriteEntry( vMap, Entry, Counter ); - Counter += Vec_IntEntry( vCounts, Place ); + Vec_IntPush( vClassNew, 0 ); + Vec_IntPush( vClassNew, Vec_IntSize(vItems) ); + // no need to change vItems } - assert( Counter == Vec_IntSize(vItems) ); - - // fill the result - Vec_IntGrowResize( vResult, Vec_IntSize(vItems) ); - Vec_IntFill( vResult, Vec_IntSize(vItems), -1 ); // verify - Vec_IntForEachEntry( vItems, Entry, i ) + else // complete or partial refinement { - Place = Vec_IntAddToEntry( vMap, Entry, 1 ) - 1; - Vec_IntWriteEntry( vResult, Place, Entry ); + // sort places + Vec_IntSort( vSeens, 0 ); + + // set the map to point to the place in the final array + Counter = 0; + Vec_IntForEachEntry( vSeens, Entry, i ) + { + Place = Vec_IntEntry( vMap, Entry ); + Vec_IntWriteEntry( vMap, Entry, Counter ); + Vec_IntPush( vClassNew, Counter ); + Vec_IntPush( vClassNew, Vec_IntEntry( vCounts, Place ) ); + assert( Vec_IntEntry( vCounts, Place ) > 0 ); + Counter += Vec_IntEntry( vCounts, Place ); + } + assert( Counter == Vec_IntSize(vItems) ); + + // fill the result + Vec_IntGrowResize( vResult, Vec_IntSize(vItems) ); + Vec_IntFill( vResult, Vec_IntSize(vItems), -1 ); // verify + Vec_IntForEachEntry( vItems, Entry0, i ) + { + Entry = Vec_IntEntry(vCosts, Entry0); + Place = Vec_IntAddToEntry( vMap, Entry, 1 ) - 1; + Vec_IntWriteEntry( vResult, Place, Entry0 ); + } + Vec_IntForEachEntry( vResult, Entry, i ) // verify + assert( Entry >= 0 ); + assert( Vec_IntSize(vItems) == Vec_IntSize(vResult) ); + memmove( Vec_IntArray(vItems), Vec_IntArray(vResult), sizeof(int) * Vec_IntSize(vResult) ); } - Vec_IntForEachEntry( vResult, Entry, i ) // verify - assert( Entry >= 0 ); // clean map Vec_IntForEachEntry( vSeens, Entry, i ) Vec_IntWriteEntry( vMap, Entry, -1 ); } +/**Function************************************************************* + + Synopsis [Introduces a new singleton object.] + + Description [Updates current equivalence classes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_IsoAddSingleton( Gia_IsoMan_t * p, int Item ) +{ + // assign unique number + assert( Vec_IntEntry( p->vUniques, Item ) == -1 ); + Vec_IntWriteEntry( p->vUniques, Item, p->nUniques++ ); + if ( Vec_IntSize(p->vFanout2) == 0 ) + return; + // create fanouts + Gia_IsoAddSingletonFanouts( p, Item, p->nUniques-1 ); +} + +/**Function************************************************************* + + Synopsis [Updates current equivalence classes.]] + + Description [ + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_IsoRefine( Gia_IsoMan_t * p, Vec_Int_t * vParam ) +{ + Vec_Int_t vThis, * pTemp; + int i, k, Begin, nSize, Begin2, nSize2, Counter = 0; + assert( Vec_IntSize(p->vClass) > 0 ); + assert( Vec_IntSize(p->vClass) % 2 == 0 ); + Vec_IntClear( p->vClass2 ); + Vec_IntForEachEntryDouble( p->vClass, Begin, nSize, i ) + { + vThis.nSize = vThis.nCap = nSize; + vThis.pArray = Vec_IntArray(p->vItems) + Begin; + Gia_IsoSortVec( &vThis, vParam, p->vMap, p->vSeens, p->vCounts, p->vResult, p->vClassNew ); + Vec_IntForEachEntryDouble( p->vClassNew, Begin2, nSize2, k ) + { + if ( nSize2 == 1 ) + { + Gia_IsoAddSingleton( p, Vec_IntEntry(p->vItems, Begin+Begin2) ); + Counter++; + continue; + } + Vec_IntPush( p->vClass2, Begin+Begin2 ); + Vec_IntPush( p->vClass2, nSize2 ); + } + } + // update classes + pTemp = p->vClass2; p->vClass2 = p->vClass; p->vClass = pTemp; + // remember beginning of each level + if ( vParam == p->vLevels ) + { + Vec_IntClear( p->vLevelLim ); + Vec_IntForEachEntryDouble( p->vClass, Begin, nSize, i ) + { + assert( nSize > 0 ); + assert( Vec_IntEntry(p->vLevels, Vec_IntEntry(p->vItems, Begin)) == i ); + Vec_IntPush( p->vLevelLim, Begin ); + } + Vec_IntPush( p->vLevelLim, Vec_IntSize(p->vItems) ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_IsoAssignUniqueToLastLevel( Gia_IsoMan_t * p ) +{ + int i, Begin, End, Item, Level, Counter = 0; + assert( Vec_IntSize( p->vClass ) > 0 ); + // get the last unrefined class + Begin = Vec_IntEntry( p->vClass, Vec_IntSize(p->vClass)-2 ); + // get the last unrefined class + Item = Vec_IntEntry( p->vItems, Begin ); + // get the level of this class + Level = Vec_IntEntry( p->vLevels, Item ); + // get the first entry on this level + Begin = Vec_IntEntry( p->vLevelLim, Level ); + End = Vec_IntEntry( p->vLevelLim, Level+1 ); + // assign all unassigned items on this level + Vec_IntForEachEntryStartStop( p->vItems, Item, i, Begin, End ) + if ( Vec_IntEntry( p->vUniques, Item ) == -1 ) + { + Gia_IsoAddSingleton( p, Item ); + Counter++; + } + return Counter; +} + /**Function************************************************************* Synopsis [] @@ -514,17 +751,32 @@ void Gia_IsoSortVec( Vec_Int_t * vItems, Vec_Int_t * vCosts, Vec_Int_t * vMap, V SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_IsoCreateStats( Gia_IsoMan_t * p ) +void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, int nSingles, int Time ) { - Vec_Int_t * vRes; - vRes = Vec_IntAlloc( 1000 ); - Gia_IsoSortStats( p->vItems, p->vLevels, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vRes, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFin0Levs, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vRes, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFin1Levs, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vRes, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFoutPos, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vRes, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFoutNeg, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vRes, p->vResult ); - Gia_IsoSortStats( p->vItems, p->vFinSig, p->vMap, p->vSeens, p->vCounts, p->vResult ); Vec_IntAppend( vRes, p->vResult ); - return vRes; + printf( "Iter %3d : ", Iter ); + printf( "Classes =%7d. ", Vec_IntSize(p->vClass)/2 ); + printf( "Uniques =%7d. ", p->nUniques ); + printf( "Singles =%7d. ", nSingles ); + Abc_PrintTime( 1, "Time", Time ); +} + +/**Function************************************************************* + + Synopsis [Compares two objects by their ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjCompareByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 ) +{ + Gia_Obj_t * pObj1 = *pp1; + Gia_Obj_t * pObj2 = *pp2; + assert( Gia_ObjIsTerm(pObj1) && Gia_ObjIsTerm(pObj2) ); + return pObj1->Value - pObj2->Value; } /**Function************************************************************* @@ -538,17 +790,149 @@ Vec_Int_t * Gia_IsoCreateStats( Gia_IsoMan_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_IsoOne( Gia_IsoMan_t * p, int iPo ) +void Gia_IsoCreateUniques( Gia_IsoMan_t * p, int iPo ) { - Vec_Int_t * vStats = NULL; + Vec_Int_t * vArray[6] = { p->vLevels, p->vFin0Levs, p->vFin1Levs, p->vFoutPos, p->vFoutNeg, p->vFinSig }; + int i, nSingles, clk = clock(); Gia_IsoCollectUsed( p->pGia, iPo, p->vUsed, p->vRoots ); -// Gia_IsoCreateFanout( p->pGia, p->vUsed, p->vRefs, p->vFanouts ); - Gia_IsoCreateSigs( p ); - vStats = Gia_IsoCreateStats( p ); + Vec_IntClear( p->vFanout2 ); + // prepare uniques + p->nUniques = 0; + Vec_IntFill( p->vUniques, Vec_IntSize(p->vUsed), -1 ); + Gia_IsoAddSingleton( p, 0 ); + // prepare classes + Vec_IntClear( p->vClass ); + Vec_IntPush( p->vClass, 1 ); + Vec_IntPush( p->vClass, Vec_IntSize(p->vUsed) ); + // perform refinement + Gia_IsoPrint( p, 0, 0, clock() - clk ); + for ( i = 0; i < 6; i++ ) + { + nSingles = Gia_IsoRefine( p, vArray[i] ); + Gia_IsoPrint( p, i+1, nSingles, clock() - clk ); + } + // derive fanouts + Gia_IsoCreateFanout( p->pGia, p->vUsed, p->vRefs, p->vFanout ); + Gia_IsoCreateFanout2( p ); + // perform refinement + for ( i = 6; p->nUniques < Vec_IntSize(p->vUsed); i++ ) + { + nSingles = Gia_IsoRefine( p, NULL ); + Gia_IsoPrint( p, i+1, nSingles, clock() - clk ); + if ( nSingles == 0 ) + { + nSingles = Gia_IsoAssignUniqueToLastLevel( p ); + Gia_IsoPrint( p, i+1, nSingles, clock() - clk ); + } + } + // finished refinement Gia_IsoCleanUsed( p->pGia, p->vUsed ); - return vStats; +} + +/**Function************************************************************* + + Synopsis [Returns canonical permutation of the inputs.] + + Description [Assumes that each CI/AND object has its unique number set.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManFindIsoPermCis( Gia_Man_t * p, Vec_Ptr_t * vTemp, Vec_Int_t * vRes ) +{ + Gia_Obj_t * pObj; + int i; + Vec_IntClear( vRes ); + // assign unique IDs to PIs + Vec_PtrClear( vTemp ); + Gia_ManForEachPi( p, pObj, i ) + Vec_PtrPush( vTemp, pObj ); + Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); + // create the result + Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) + Vec_IntPush( vRes, Gia_ObjCioId(pObj) ); + // assign unique IDs to ROs + Vec_PtrClear( vTemp ); + Gia_ManForEachRo( p, pObj, i ) + Vec_PtrPush( vTemp, pObj ); + Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); + // create the result + Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) + Vec_IntPush( vRes, Gia_ObjCioId(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Find the canonical permutation of the COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManFindIsoPermCos( Gia_Man_t * p, Vec_Int_t * vPermCis, Vec_Ptr_t * vTemp, Vec_Int_t * vRes ) +{ + Gia_Obj_t * pObj; + int i, Entry, Diff; + assert( Vec_IntSize(vPermCis) == Gia_ManCiNum(p) ); + Vec_IntClear( vRes ); + if ( Gia_ManPoNum(p) == 1 ) + Vec_IntPush( vRes, 0 ); + else + { + Vec_PtrClear( vTemp ); + Gia_ManForEachPo( p, pObj, i ) + { + pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + Vec_PtrPush( vTemp, pObj ); + } + Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue ); + Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) + Vec_IntPush( vRes, Gia_ObjCioId(pObj) ); + } + // add flop outputs + Diff = Gia_ManPoNum(p) - Gia_ManPiNum(p); + Vec_IntForEachEntryStart( vPermCis, Entry, i, Gia_ManPiNum(p) ) + Vec_IntPush( vRes, Entry + Diff ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupCanonical( Gia_Man_t * p, Vec_Int_t * vUsed, Vec_Int_t * vUniques ) +{ + return NULL; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_IsoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 ) +{ + return Vec_StrCompareVec( *p1, *p2 ); +} + + /**Function************************************************************* Synopsis [] @@ -571,16 +955,15 @@ void Gia_IsoTest( Gia_Man_t * pGia ) p = Gia_IsoManStart( pGia ); for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) { - if ( i % 1000 == 0 ) + if ( i % 100 == 0 ) printf( "Finished %5d\r", i ); - vStats = Gia_IsoOne( p, i ); + vStats = Gia_IsoCreateStats( p, i ); Vec_PtrPush( p->vResults, vStats ); if ( fVerbose ) printf( "%d ", Vec_IntSize(vStats)/2 ); } if ( fVerbose ) printf( " \n" ); - vResults = p->vResults; p->vResults = NULL; Gia_IsoManStop( p ); @@ -590,6 +973,116 @@ void Gia_IsoTest( Gia_Man_t * pGia ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_IsoFilterPos( Gia_Man_t * pGia, int fVerbose ) +{ + int fVeryVerbose = 0; + Gia_IsoMan_t * p; + Gia_Man_t * pTemp; + Vec_Ptr_t * vBuffers, * vClasses; + Vec_Int_t * vLevel, * vRemain; + Vec_Str_t * vStr, * vPrev; + int i, nUnique = 0, clk = clock(); + int clkAig = 0, clkIso = 0, clk2; + + // start the manager + Gia_ManCleanValue( pGia ); + p = Gia_IsoManStart( pGia ); + // derive AIG for each PO + vBuffers = Vec_PtrAlloc( Gia_ManPoNum(pGia) ); + for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) + { + if ( i % 100 == 0 ) + printf( "%6d finished...\r", i ); + + clk2 = clock(); + pTemp = Gia_ManDupCanonical( pGia, p->vUsed, p->vUniques ); + clkIso += clock() - clk2; + + clk2 = clock(); + vStr = Gia_WriteAigerIntoMemoryStr( pTemp ); + clkAig += clock() - clk2; + + Vec_PtrPush( vBuffers, vStr ); + Gia_ManStop( pTemp ); + // remember the output number in nCap (attention: hack!) + vStr->nCap = i; + } + // stop the manager + Gia_IsoManStop( p ); + +// s_Counter = 0; + if ( fVerbose ) + { + Abc_PrintTime( 1, "Isomorph time", clkIso ); + Abc_PrintTime( 1, "AIGER time", clkAig ); + } + + // sort the infos + clk = clock(); + Vec_PtrSort( vBuffers, (int (*)(void))Gia_IsoCompareVecStr ); + + // create classes + clk = clock(); + vClasses = Vec_PtrAlloc( Gia_ManPoNum(pGia) ); + // start the first class + Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) ); + vPrev = (Vec_Str_t *)Vec_PtrEntry( vBuffers, 0 ); + Vec_IntPush( vLevel, vPrev->nCap ); + // consider other classes + Vec_PtrForEachEntryStart( Vec_Str_t *, vBuffers, vStr, i, 1 ) + { + if ( Vec_StrCompareVec(vPrev, vStr) ) + Vec_PtrPush( vClasses, Vec_IntAlloc(4) ); + vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses ); + Vec_IntPush( vLevel, vStr->nCap ); + vPrev = vStr; + } + Vec_VecFree( (Vec_Vec_t *)vBuffers ); + + if ( fVerbose ) + Abc_PrintTime( 1, "Sorting time", clock() - clk ); +// Abc_PrintTime( 1, "Traversal time", time_Trav ); + + // report the results +// Vec_VecPrintInt( (Vec_Vec_t *)vClasses ); +// printf( "Devided %d outputs into %d cand equiv classes.\n", Gia_ManPoNum(pGia), Vec_PtrSize(vClasses) ); + if ( fVerbose ) + { + Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) + if ( Vec_IntSize(vLevel) > 1 ) + printf( "%d ", Vec_IntSize(vLevel) ); + else + nUnique++; + printf( " Unique = %d\n", nUnique ); + } + + // collect the first ones + vRemain = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i ) + Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) ); + + // derive the resulting AIG + pTemp = Gia_ManDupCones( pGia, Vec_IntArray(vRemain), Vec_IntSize(vRemain) ); + Vec_IntFree( vRemain ); + +// return (Vec_Vec_t *)vClasses; + Vec_VecFree( (Vec_Vec_t *)vClasses ); + +// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); + return pTemp; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3