diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-20 20:29:11 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-20 20:29:11 +0700 |
| commit | 56035ab9ab1051f87e1186d06bd250375f9d4227 (patch) | |
| tree | a15057b597b4da9fccb58bed3a4e7faad20d8a95 /src/aig/llb/llb4Cex.c | |
| parent | 21dfaedebd842c240e770d3bcfb62e2fb4531b40 (diff) | |
| download | abc-56035ab9ab1051f87e1186d06bd250375f9d4227.tar.gz abc-56035ab9ab1051f87e1186d06bd250375f9d4227.tar.bz2 abc-56035ab9ab1051f87e1186d06bd250375f9d4227.zip | |
Making sure reconcile does not change the PO number.
Diffstat (limited to 'src/aig/llb/llb4Cex.c')
| -rw-r--r-- | src/aig/llb/llb4Cex.c | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/aig/llb/llb4Cex.c b/src/aig/llb/llb4Cex.c index 6c4cedfb..603c6e59 100644 --- a/src/aig/llb/llb4Cex.c +++ b/src/aig/llb/llb4Cex.c @@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int fVerbose ) +Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose ) { Abc_Cex_t * pCex; Cnf_Dat_t * pCnf; @@ -124,8 +124,18 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int // add the last frame when the property fails Vec_IntClear( vAssumps ); - Saig_ManForEachPo( pAig, pObj, k ) - Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) ); + if ( iCexPo >= 0 ) + { + Saig_ManForEachPo( pAig, pObj, k ) + if ( k == iCexPo ) + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) ); + } + else + { + Saig_ManForEachPo( pAig, pObj, k ) + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ) ); + } + // add clause status = sat_solver_addclause( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps) ); if ( status == 0 ) @@ -292,7 +302,7 @@ Abc_Cex_t * Llb4_Nonlin4NormalizeCex( Aig_Man_t * pAigOrg, Aig_Man_t * pAigRpm, return NULL; } // derive updated counter-example - pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, 0 ); + pCexOrg = Llb4_Nonlin4TransformCex( pAigOrg, vStates, pCexRpm->iPo, 0 ); Vec_PtrFree( vStates ); return pCexOrg; } |