From 0058cefee35e08eaa5740c0febf3829c89781a3c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Dec 2012 00:19:18 -0800 Subject: Deriving CEX after phase/tempor/reparam. --- src/aig/gia/gia.h | 4 ++ src/aig/gia/giaCex.c | 95 +++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaDup.c | 104 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaIso.c | 91 ++++++++++++++++++++++++++++++++++++++++-- src/base/abci/abc.c | 6 ++- src/misc/util/utilCex.c | 11 +++-- 6 files changed, 300 insertions(+), 11 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index d9e86085..52db2cce 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -728,6 +728,8 @@ 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 ); +extern Abc_Cex_t * Gia_ManCexExtendToIncludeCurrentStates( Gia_Man_t * p, Abc_Cex_t * pCex ); +extern Abc_Cex_t * Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, Abc_Cex_t * pCex ); /*=== giaChoice.c ============================================================*/ extern void Gia_ManVerifyChoices( Gia_Man_t * p ); extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ); @@ -760,7 +762,9 @@ extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo ); +extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ); diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c index 58415f73..fdc0c709 100644 --- a/src/aig/gia/giaCex.c +++ b/src/aig/gia/giaCex.c @@ -241,6 +241,101 @@ void Gia_ManCounterExampleValueTest( Gia_Man_t * pGia, Abc_Cex_t * pCex ) } +/**Function************************************************************* + + Synopsis [Returns CEX containing PI+CS values for each timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gia_ManCexExtendToIncludeCurrentStates( Gia_Man_t * p, Abc_Cex_t * pCex ) +{ + Abc_Cex_t * pNew; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int i, k, iBit = 0; + assert( pCex->nRegs > 0 ); + // start the counter-example + pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCex->iFrame + 1 ); + pNew->iFrame = pCex->iFrame; + pNew->iPo = pCex->iPo; + // set const0 + Gia_ManConst0(p)->fMark0 = 0; + // set init state + Gia_ManForEachRi( p, pObjRi, k ) + pObjRi->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + assert( iBit == pCex->nRegs ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + Gia_ManForEachCi( p, pObj, k ) + if ( pObj->fMark0 ) + Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k ); + Gia_ManForEachAnd( p, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( p, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + } + assert( iBit == pCex->nBits ); + assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 ); + Gia_ManCleanMark0(p); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns CEX containing all object valuess for each timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, Abc_Cex_t * pCex ) +{ + Abc_Cex_t * pNew; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int i, k, iBit = 0; + assert( pCex->nRegs > 0 ); + // start the counter-example + pNew = Abc_CexAlloc( 0, Gia_ManObjNum(p), pCex->iFrame + 1 ); + pNew->iFrame = pCex->iFrame; + pNew->iPo = pCex->iPo; + // set const0 + Gia_ManConst0(p)->fMark0 = 0; + // set init state + Gia_ManForEachRi( p, pObjRi, k ) + pObjRi->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + assert( iBit == pCex->nRegs ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + pObjRo->fMark0 = pObjRi->fMark0; + Gia_ManForEachObj( p, pObj, k ) + if ( pObj->fMark0 ) + Abc_InfoSetBit( pNew->pData, pNew->nPis * i + k ); + Gia_ManForEachAnd( p, pObj, k ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachCo( p, pObj, k ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + } + assert( iBit == pCex->nBits ); + assert( Gia_ManPo(p, pCex->iPo)->fMark0 == 1 ); + Gia_ManCleanMark0(p); + return pNew; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 3d0b9bf3..b5fcae45 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -428,6 +428,49 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG without any changes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ) +{ +// Vec_Int_t * vPiPermInv; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + assert( Vec_IntSize(vPiPerm) == Gia_ManPiNum(p) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; +// vPiPermInv = Vec_IntInvert( vPiPerm, -1 ); + Gia_ManForEachPi( p, pObj, i ) +// Gia_ManPi(p, Vec_IntEntry(vPiPermInv,i))->Value = Gia_ManAppendCi( pNew ); + Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi( pNew ); +// Vec_IntFree( vPiPermInv ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + { + if ( Gia_ObjIsRo(p, pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + } + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + /**Function************************************************************* Synopsis [Appends second AIG without any changes.] @@ -459,6 +502,60 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo ) } } + +/**Function************************************************************* + + Synopsis [Append second AIG on top of the first with the permutation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(pOne) + Gia_ManObjNum(pTwo) ); + pNew->pName = Abc_UtilStrsav( pOne->pName ); + pNew->pSpec = Abc_UtilStrsav( pOne->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pOne)->Value = 0; + Gia_ManForEachObj1( pOne, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + } + Gia_ManConst0(pTwo)->Value = 0; + Gia_ManForEachObj1( pTwo, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsPi(pTwo, pObj) ) + pObj->Value = Gia_ManPi(pOne, Gia_ObjCioId(pObj))->Value; + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + } + Gia_ManHashStop( pNew ); + // primary outputs + Gia_ManForEachPo( pOne, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachPo( pTwo, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + // flop inputs + Gia_ManForEachRi( pOne, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachRi( pTwo, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pOne) + Gia_ManRegNum(pTwo) ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates while adding self-loops to the registers.] @@ -1854,6 +1951,12 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ) SeeAlso [] ***********************************************************************/ +int Gia_ObjCompareByCioId( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 ) +{ + Gia_Obj_t * pObj1 = *pp1; + Gia_Obj_t * pObj2 = *pp2; + return Gia_ObjCioId(pObj1) - Gia_ObjCioId(pObj2); +} void Gia_ManDupCones_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) @@ -1892,6 +1995,7 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ) Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i ) Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots ); + Vec_PtrSort( vLeaves, (int (*)(void))Gia_ObjCompareByCioId ); // start the new manager // Gia_ManFillValue( p ); 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e0bcb523..22e018ab 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28953,6 +28953,7 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pAig; Vec_Ptr_t * vPosEquivs; +// Vec_Ptr_t * vPiPerms; int c, fDualOut = 0, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF ) @@ -28982,6 +28983,8 @@ int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, NULL, fDualOut, fVerbose ); +// pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, &vPiPerms, fDualOut, fVerbose ); +// Vec_VecFree( (Vec_Vec_t *)vPiPerms ); if ( pAig == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Iso(): Transformation has failed.\n" ); @@ -30344,7 +30347,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); // extern void Ga2_ManComputeTest( Gia_Man_t * p ); // extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); - + extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30390,6 +30393,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_IsoTest( pAbc->pGia, fVerbose ); // Ga2_ManComputeTest( pAbc->pGia ); // Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose ); + Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index d8ed84b8..2f205d2e 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -452,16 +452,15 @@ Abc_Cex_t * Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New ) ***********************************************************************/ Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew ) { - Vec_Int_t * vPermInv = Vec_IntInvert( vPermNew, -1 ); - Vec_Int_t * vPerm = Vec_IntAlloc( Vec_IntSize(vPermOld) ); Abc_Cex_t * pCex; - int i, Entry; + Vec_Int_t * vPerm; + int i, eOld, eNew; assert( Vec_IntSize(vPermOld) == p->nPis ); assert( Vec_IntSize(vPermNew) == p->nPis ); - Vec_IntForEachEntry( vPerm, Entry, i ) - Vec_IntEntry( vPerm, Vec_IntEntry(vPermInv, Vec_IntEntry(vPermOld, Entry)) ); + vPerm = Vec_IntStartFull( p->nPis ); + Vec_IntForEachEntryTwo( vPermOld, vPermNew, eOld, eNew, i ) + Vec_IntWriteEntry( vPerm, eOld, eNew ); pCex = Abc_CexPermute( p, vPerm ); - Vec_IntFree( vPermInv ); Vec_IntFree( vPerm ); return pCex; } -- cgit v1.2.3