summaryrefslogtreecommitdiffstats
path: root/src/aig/saig/saigInd.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-07-30 19:18:26 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-07-30 19:18:26 +0700
commit02711b6392bb12816a9041e5e13e6d0168599085 (patch)
tree4dc160c3c135a915fb35159f44e7dcf0e69fc403 /src/aig/saig/saigInd.c
parentc60852f4a935f72bb399414853b130eb49b79804 (diff)
downloadabc-02711b6392bb12816a9041e5e13e6d0168599085.tar.gz
abc-02711b6392bb12816a9041e5e13e6d0168599085.tar.bz2
abc-02711b6392bb12816a9041e5e13e6d0168599085.zip
Added generation of counter-examples to induction in 'ind'.
Diffstat (limited to 'src/aig/saig/saigInd.c')
-rw-r--r--src/aig/saig/saigInd.c43
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;
}