diff options
Diffstat (limited to 'src/aig/gia/giaIso.c')
-rw-r--r-- | src/aig/gia/giaIso.c | 91 |
1 files changed, 87 insertions, 4 deletions
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index 57e90067..3b391529 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -821,10 +821,12 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); } + if ( Gia_ManPoNum(p->pGia) > 1 ) vEquivs = Gia_IsoCollectCosClasses( p, fVerbose ); Gia_IsoManTransferUnique( p ); Gia_IsoManStop( p ); + return vEquivs; } @@ -897,8 +899,11 @@ void Gia_ManFindCaninicalOrder( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAn Vec_IntPush( vCis, Gia_ObjId(p, pObj) ); // remember PI permutation if ( pvPiPerm ) + { + *pvPiPerm = Vec_IntAlloc( Gia_ManPiNum(p) ); Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i ) Vec_IntPush( *pvPiPerm, Gia_ObjCioId(pObj) ); + } // assign unique IDs to POs if ( Gia_ManPoNum(p) == 1 ) @@ -986,7 +991,7 @@ Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAn ***********************************************************************/ Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose ) { - Gia_Man_t * vResult = NULL; + Gia_Man_t * pRes = NULL; Vec_Int_t * vCis, * vAnds, * vCos; Vec_Ptr_t * vEquiv; if ( Gia_ManCiNum(p) == 0 ) // const AIG @@ -1005,12 +1010,12 @@ Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose ) vCos = Vec_IntAlloc( Gia_ManCoNum(p) ); Gia_ManFindCaninicalOrder( p, vCis, vAnds, vCos, NULL ); // derive the new AIG - vResult = Gia_ManDupFromVecs( p, vCis, vAnds, vCos, Gia_ManRegNum(p) ); + pRes = Gia_ManDupFromVecs( p, vCis, vAnds, vCos, Gia_ManRegNum(p) ); // cleanup Vec_IntFree( vCis ); Vec_IntFree( vAnds ); Vec_IntFree( vCos ); - return vResult; + return pRes; } /**Function************************************************************* @@ -1032,6 +1037,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_ Vec_Str_t * vStr; // duplicate pPart = Gia_ManDupCones( p, &iPo, 1, 1 ); +//Gia_ManPrint( pPart ); assert( Gia_ManPoNum(pPart) == 1 ); if ( Gia_ManCiNum(pPart) == 0 ) // const AIG { @@ -1039,6 +1045,8 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_ assert( Gia_ManObjNum(pPart) == 2 ); vStr = Gia_WriteAigerIntoMemoryStr( pPart ); Gia_ManStop( pPart ); + if ( pvPiPerm ) + *pvPiPerm = Vec_IntAlloc( 0 ); return vStr; } // derive canonical values @@ -1049,6 +1057,8 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_ vAnds = Vec_IntAlloc( Gia_ManAndNum(pPart) ); vCos = Vec_IntAlloc( Gia_ManCoNum(pPart) ); Gia_ManFindCaninicalOrder( pPart, vCis, vAnds, vCos, pvPiPerm ); +//printf( "Internal: " ); +//Vec_IntPrint( vCis ); // derive the AIGER string vStr = Gia_WriteAigerIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) ); // cleanup @@ -1132,6 +1142,10 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P printf( "%6d finished...\r", Counter ); assert( pvPiPerms == NULL || Vec_PtrArray(*pvPiPerms)[iPo] == NULL ); vStr = Gia_ManIsoFindString( p, iPo, 0, pvPiPerms ? (Vec_Int_t **)Vec_PtrArray(*pvPiPerms) + iPo : NULL ); + +// printf( "Output %2d : ", iPo ); +// Vec_IntPrint( Vec_PtrArray(*pvPiPerms)[iPo] ); + // check if this string already exists Vec_PtrForEachEntry( Vec_Str_t *, vStrings, vStr2, s ) if ( Vec_StrCompareVec(vStr, vStr2) == 0 ) @@ -1211,7 +1225,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P SeeAlso [] ***********************************************************************/ -void Gia_IsoTest( Gia_Man_t * p, int fVerbose ) +void Gia_IsoTestOld( Gia_Man_t * p, int fVerbose ) { Vec_Ptr_t * vEquivs; clock_t clk = clock(); @@ -1226,6 +1240,75 @@ void Gia_IsoTest( Gia_Man_t * p, int fVerbose ) Vec_VecFreeP( (Vec_Vec_t **)&vEquivs ); } +/**Function************************************************************* + + Synopsis [Test remapping of CEXes for isomorphic POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_IsoTestGenPerm( int nPis ) +{ + Vec_Int_t * vPerm; + int i, * pArray; + vPerm = Vec_IntStartNatural( nPis ); + pArray = Vec_IntArray( vPerm ); + for ( i = 0; i < nPis; i++ ) + { + int iNew = rand() % nPis; + ABC_SWAP( int, pArray[i], pArray[iNew] ); + } + return vPerm; +} +void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ) +{ + Abc_Cex_t * pCexNew; + Vec_Int_t * vPiPerm; + Vec_Ptr_t * vPosEquivs, * vPisPerm; + Vec_Int_t * vPerm0, * vPerm1; + Gia_Man_t * pPerm, * pDouble, * pAig; + assert( Gia_ManPoNum(p) == 1 ); + assert( Gia_ManRegNum(p) > 0 ); + // generate random permutation of PIs + vPiPerm = Gia_IsoTestGenPerm( Gia_ManPiNum(p) ); + printf( "Considering random permutation of the AIG:\n" ); + Vec_IntPrint( vPiPerm ); + // create AIG with two primary outputs (original and permuted) + pPerm = Gia_ManDupPerm( p, vPiPerm ); + pDouble = Gia_ManDupAppendNew( p, pPerm ); +//Gia_WriteAiger( pDouble, "test.aig", 0, 0 ); + + // analyze the two-output miter + pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0 ); + Vec_VecFree( (Vec_Vec_t *)vPosEquivs ); + + // given CEX for output 0, derive CEX for output 1 + vPerm0 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 0 ); + vPerm1 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 1 ); + pCexNew = Abc_CexPermuteTwo( pCex, vPerm0, vPerm1 ); + Vec_VecFree( (Vec_Vec_t *)vPisPerm ); + + // check that original CEX and the resulting CEX is valid + if ( Gia_ManVerifyCex(p, pCex, 0) ) + printf( "CEX for the init AIG is valid.\n" ); + else + printf( "CEX for the init AIG is not valid.\n" ); + if ( Gia_ManVerifyCex(pPerm, pCexNew, 0) ) + printf( "CEX for the perm AIG is valid.\n" ); + else + printf( "CEX for the perm AIG is not valid.\n" ); + // delete + Gia_ManStop( pAig ); + Gia_ManStop( pDouble ); + Gia_ManStop( pPerm ); + Vec_IntFree( vPiPerm ); + Abc_CexFree( pCexNew ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |