From 71cbf17e7f0352556af12ccccf9051e02c773e58 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 17:46:48 -0800 Subject: Unified the use of counter-examples in three packages. --- src/aig/saig/saig.h | 2 ++ src/aig/saig/saigAbs.c | 10 +++--- src/aig/saig/saigBmc.c | 3 +- src/aig/saig/saigBmc2.c | 6 ++-- src/aig/saig/saigBmc3.c | 6 ++-- src/aig/saig/saigDup.c | 85 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/saig/saigSimSeq.c | 2 +- 7 files changed, 99 insertions(+), 15 deletions(-) (limited to 'src/aig/saig') diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index b1017bdb..bf5681b9 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -149,6 +149,8 @@ extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ); extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); +extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ); +extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ); /*=== saigHaig.c ==========================================================*/ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); /*=== saigInd.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 938a66e2..471d5d2d 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -101,12 +101,12 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA Abc_Cex_t * pCex; Aig_Obj_t * pObj; int i, f; - if ( !Ssw_SmlRunCounterExample( pAbs, pCexAbs ) ) + if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) ) printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" ); else printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" ); // start the counter-example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); pCex->iFrame = pCexAbs->iFrame; pCex->iPo = pCexAbs->iPo; // copy the bit data @@ -121,10 +121,10 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA } } // verify the counter example - if ( !Ssw_SmlRunCounterExample( p, pCex ) ) + if ( !Saig_ManVerifyCex( p, pCex ) ) { printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" ); - Ssw_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } else @@ -194,7 +194,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo printf( "Running property directed reachability...\n" ); RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex ); if ( pCex ) - pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex ); + pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex ); Aig_ManStop( pAbsOrpos ); pAbs->pSeqModel = pCex; if ( RetValue ) diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 8aa3af80..cb506054 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -301,11 +301,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else if ( status == l_True ) { -// extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); pModel[Aig_ManPiNum(pFrames)] = pObj->Id; - pAig->pSeqModel = (Abc_Cex_t *)Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); + pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); ABC_FREE( pModel ); Vec_IntFree( vCiIds ); diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 3d57ae6e..9c36deb3 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -637,7 +637,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) Aig_Obj_t * pObj, * pObjFrm; int i, f, iVarNum; // start the counter-example - pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 ); pCex->iFrame = p->iFrameFail; pCex->iPo = p->iOutputFail; // copy the bit data @@ -656,10 +656,10 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) } } // verify the counter example - if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) ) + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" ); - Ssw_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index a75297f7..570e8a26 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1108,8 +1108,7 @@ clkOther += clock() - clk2; continue; if ( Lit == 1 ) { - extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); - Abc_Cex_t * pCex = Fra_SmlTrivCounterExample( pAig, f*Saig_ManPoNum(pAig)+i ); + Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); printf( "Output %d is trivially SAT in frame %d.\n", i, f ); if ( !pPars->fSolveAll ) { @@ -1137,9 +1136,8 @@ clkOther += clock() - clk2; } else if ( status == l_True ) { -// extern void * Fra_SmlSimpleCounterExample( Aig_Man_t * p, int * pModel, int iFrame, int iPo ); int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) ); - Abc_Cex_t * pCex = Fra_SmlSimpleCounterExample( pAig, pModel, f, i ); + Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 ); ABC_FREE( pModel ); fFirst = 0; if ( !pPars->fSolveAll ) diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index f4e557f8..b2b33bdb 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -265,6 +265,91 @@ Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) return pNew; } +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB; + Aig_ManCleanMarkB(pAig); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + // remember the number of failed output + RetValue = -1; + Saig_ManForEachPo( pAig, pObj, i ) + if ( pObj->fMarkB ) + { + RetValue = i; + break; + } + Aig_ManCleanMarkB(pAig); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index 37bb12b5..cc5a9e05 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -418,7 +418,7 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int Abc_Cex_t * p; unsigned * pData; int f, i, w, iPioId, Counter; - p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); + p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); p->iFrame = iFrame; p->iPo = iOut; // fill in the binary data -- cgit v1.2.3