From 02711b6392bb12816a9041e5e13e6d0168599085 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 30 Jul 2011 19:18:26 +0700 Subject: Added generation of counter-examples to induction in 'ind'. --- src/aig/cec/cecSeq.c | 7 +++---- src/aig/saig/saig.h | 2 +- src/aig/saig/saigInd.c | 43 +++++++++++++++++++++++++++++++++++++++++-- src/base/abci/abc.c | 19 +++++++++++++++---- src/base/abci/abcDar.c | 14 ++++++++++---- 5 files changed, 70 insertions(+), 15 deletions(-) diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index e9f3df37..7e7549c0 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -49,21 +49,20 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) ); assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) ); nWords = Vec_PtrReadWordsSimInfo( vInfo ); -/* for ( k = 0; k < pCex->nRegs; k++ ) { - pInfo = Vec_PtrEntry( vInfo, k ); + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0; } -*/ +/* for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); for ( w = 0; w < nWords; w++ ) pInfo[w] = 0; } - +*/ for ( i = pCex->nRegs; i < pCex->nBits; i++ ) { pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ ); diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index dd6064ad..9766768d 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -163,7 +163,7 @@ extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * /*=== 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 ==========================================================*/ -extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose ); +extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose ); /*=== saigIoa.c ==========================================================*/ extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index 6bb29488..190d8d25 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -142,12 +142,12 @@ void Saig_ManAddUniqueness( sat_solver * pSat, Vec_Int_t * vState, int nRegs, in SeeAlso [] ***********************************************************************/ -int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose ) +int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose ) { sat_solver * pSat; Aig_Man_t * pAigPart; Cnf_Dat_t * pCnfPart; - Vec_Int_t * vTopVarNums, * vState; + Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL; Vec_Ptr_t * vTop, * vBot; Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo; int i, k, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev; @@ -190,6 +190,24 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, nSatVarNum += pCnfPart->nVars; nClauses += pCnfPart->nClauses; + // remember top frame var IDs + if ( fGetCex && vTopVarIds == NULL ) + { + vTopVarIds = Vec_IntStartFull( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObjPi, i ) + { + if ( pObjPi->pData == NULL ) + continue; + pObjPiCopy = (Aig_Obj_t *)pObjPi->pData; + assert( Aig_ObjIsPi(pObjPiCopy) ); + if ( Saig_ObjIsPi(p, pObjPi) ) + Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); + else if ( Saig_ObjIsLo(p, pObjPi) ) + Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); + else assert( 0 ); + } + } + // stitch variables of top and bot assert( Aig_ManPoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) ); Aig_ManForEachPo( pAigPart, pObjPo, i ) @@ -294,7 +312,27 @@ nextrun: printf( "\n" ); } if ( f == nFramesMax - 1 ) + { + // derive counter-example + assert( status == l_True ); + if ( fGetCex ) + { + int VarNum, iBit = 0; + Abc_Cex_t * pCex = Abc_CexAlloc( Aig_ManRegNum(p)-1, Saig_ManPiNum(p), 1 ); + pCex->iFrame = 0; + pCex->iPo = 0; + Vec_IntForEachEntryStart( vTopVarIds, VarNum, i, 1 ) + { + if ( VarNum >= 0 && sat_solver_var_value( pSat, VarNum ) ) + Aig_InfoSetBit( pCex->pData, iBit ); + iBit++; + } + assert( iBit == pCex->nBits ); + Abc_CexFree( p->pSeqModel ); + p->pSeqModel = pCex; + } break; + } if ( fUnique ) { for ( i = 1; i < iLast; i++ ) @@ -333,6 +371,7 @@ nextrun: Vec_PtrFree( vTop ); Vec_PtrFree( vBot ); Vec_IntFree( vState ); + Vec_IntFreeP( &vTopVarIds ); return RetValue; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ee0c98ff..980ba7ed 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19546,19 +19546,21 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) int nConfMax; int fUnique; int fUniqueAll; + int fGetCex; int fVerbose; int fVeryVerbose; int c; - extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose ); // set defaults nFramesMax = 100; nConfMax = 1000; fUnique = 0; fUniqueAll = 0; + fGetCex = 0; fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCuavwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCuaxvwh" ) ) != EOF ) { switch ( c ) { @@ -19590,6 +19592,9 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': fUniqueAll ^= 1; break; + case 'x': + fGetCex ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -19629,15 +19634,21 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose ); + pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose ); + if ( fGetCex ) + { + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + printf( "The current CEX in ABC is set to be the CEX to induction.\n" ); + } return 0; usage: - Abc_Print( -2, "usage: ind [-FC num] [-uavwh]\n" ); + Abc_Print( -2, "usage: ind [-FC num] [-uaxvwh]\n" ); Abc_Print( -2, "\t runs the inductive case of the K-step induction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); Abc_Print( -2, "\t-u : toggle adding uniqueness constraints on demand [default = %s]\n", fUnique? "yes": "no" ); Abc_Print( -2, "\t-a : toggle adding uniqueness constraints always [default = %s]\n", fUniqueAll? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle returning CEX to induction for the top frame [default = %s]\n", fGetCex? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing additional verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 695ae4ef..c0822ba9 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3151,16 +3151,15 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC SeeAlso [] ***********************************************************************/ -int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose ) { - Aig_Man_t * pMan, * pTemp; + Aig_Man_t * pMan; int clkTotal = clock(); int RetValue; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return -1; - RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose ); - Aig_ManStop( pTemp ); + RetValue = Saig_ManInduction( pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose ); if ( RetValue == 1 ) { printf( "Networks are equivalent. " ); @@ -3176,6 +3175,13 @@ ABC_PRT( "Time", clock() - clkTotal ); printf( "Networks are UNDECIDED. " ); ABC_PRT( "Time", clock() - clkTotal ); } + if ( fGetCex ) + { + ABC_FREE( pNtk->pModel ); + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; + } + Aig_ManStop( pMan ); return RetValue; } -- cgit v1.2.3