diff options
Diffstat (limited to 'src/aig/saig/saigInd.c')
| -rw-r--r-- | src/aig/saig/saigInd.c | 43 |
1 files changed, 41 insertions, 2 deletions
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; } |