diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-11 20:48:23 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-11 20:48:23 -0800 |
| commit | 309ab1c12b262229d6d12071b3bee8d4ffc8b56f (patch) | |
| tree | 0e85a5a7739d83096e1565b41953bd15db030f06 /src/aig | |
| parent | d81aa6d697a8fd2128acef9cf7b2be24a4066f63 (diff) | |
| download | abc-309ab1c12b262229d6d12071b3bee8d4ffc8b56f.tar.gz abc-309ab1c12b262229d6d12071b3bee8d4ffc8b56f.tar.bz2 abc-309ab1c12b262229d6d12071b3bee8d4ffc8b56f.zip | |
Variable timeframe abstraction.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index fe5a8c36..21e31cd2 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -654,7 +654,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) Gia_Obj_t * pObj; int i, Counter; -// Vta_ManSatVerify( p ); + Vta_ManSatVerify( p ); // collect nodes in a topological order vOrder = Vta_ManCollectNodes( p, f ); @@ -664,7 +664,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0; pThis->fVisit = 0; } -/* + // verify Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i ) { @@ -691,7 +691,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) else assert( 0 ); } } -*/ + // compute distance in reverse order pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) ); pThis->Prio = 1; @@ -883,7 +883,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) assert( 0 ); } -/* + // verify Vta_ManForEachObjVec( vOrder, p, pThis, i ) pThis->Value = VTA_VARX; @@ -948,7 +948,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" ); // else // printf( "Verification OK.\n" ); -*/ + // produce true counter-example if ( pTop->Prio == 0 ) |