diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-28 09:56:14 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-04-28 09:56:14 -0400 |
| commit | e4d0f4715a4dce9eb14a0380a669a67a2c0a6616 (patch) | |
| tree | bfe7dd5c04a96150b153a1a71540710aa7e5103e /src/aig/gia | |
| parent | 631b50aa591f47a48cc91813a975effddd3a1f76 (diff) | |
| download | abc-e4d0f4715a4dce9eb14a0380a669a67a2c0a6616.tar.gz abc-e4d0f4715a4dce9eb14a0380a669a67a2c0a6616.tar.bz2 abc-e4d0f4715a4dce9eb14a0380a669a67a2c0a6616.zip | |
Added new options to testcex.
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index d0bd454f..efe4d1d3 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -803,7 +803,7 @@ extern int Gia_ManHasDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); -extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ); +extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 2794956a..125f3592 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1187,7 +1187,7 @@ int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) SeeAlso [] ***********************************************************************/ -int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ) +int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; @@ -1209,12 +1209,14 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p ) assert( iBit == p->nBits ); // remember the number of failed output RetValue = -1; - Gia_ManForEachPo( pAig, pObj, i ) + for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- ) + { if ( Gia_ManPo(pAig, i)->fMark0 ) { RetValue = i; break; } + } Gia_ManCleanMark0(pAig); return RetValue; } |