mirror of https://github.com/YosysHQ/abc.git
Deriving CEX after phase/tempor/reparam.
This commit is contained in:
Alan Mishchenko
parent
a68593c4f2
commit
0058cefee3
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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" );
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue