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 | |
parent | d81aa6d697a8fd2128acef9cf7b2be24a4066f63 (diff) | |
download | abc-309ab1c12b262229d6d12071b3bee8d4ffc8b56f.tar.gz abc-309ab1c12b262229d6d12071b3bee8d4ffc8b56f.tar.bz2 abc-309ab1c12b262229d6d12071b3bee8d4ffc8b56f.zip |
Variable timeframe abstraction.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 10 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 37 |
2 files changed, 33 insertions, 14 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 ) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 48c68154..50a46050 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -498,35 +498,55 @@ static inline int solver2_assume(sat_solver2* s, lit l) } static void solver2_canceluntil(sat_solver2* s, int level) { - lit* trail; int bound; int lastLev; int c, x; - if (solver2_dlevel(s) < level) + if (solver2_dlevel(s) <= level) return; + assert( solver2_dlevel(s) > 0 ); - trail = s->trail; bound = (veci_begin(&s->trail_lim))[level]; lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; for (c = s->qtail-1; c >= bound; c--) { - x = lit_var(trail[c]); + x = lit_var(s->trail[c]); var_set_value(s, x, varX); s->reasons[x] = 0; s->units[x] = 0; // temporary? if ( c < lastLev ) - var_set_polar(s, x, !lit_sign(trail[c])); + var_set_polar(s, x, !lit_sign(s->trail[c])); } for (c = s->qhead-1; c >= bound; c--) - order_unassigned(s,lit_var(trail[c])); + order_unassigned(s,lit_var(s->trail[c])); s->qhead = s->qtail = bound; veci_resize(&s->trail_lim,level); } +static void solver2_canceluntil_rollback(sat_solver2* s, int NewBound) { + int c, x; + + assert( solver2_dlevel(s) == 0 ); + assert( s->qtail == s->qhead ); + assert( s->qtail >= NewBound ); + + for (c = s->qtail-1; c >= NewBound; c--) + { + x = lit_var(s->trail[c]); + var_set_value(s, x, varX); + s->reasons[x] = 0; + s->units[x] = 0; // temporary? + } + + for (c = s->qhead-1; c >= NewBound; c--) + order_unassigned(s,lit_var(s->trail[c])); + + s->qhead = s->qtail = NewBound; +} + static void solver2_record(sat_solver2* s, veci* cls, int proof_id) { @@ -1513,9 +1533,8 @@ void sat_solver2_rollback( sat_solver2* s ) } } // reset implication queue - assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot ); - (&s->trail_lim)->ptr[0] = s->iSimpPivot; - solver2_canceluntil( s, 0 ); + assert( solver2_dlevel(s) == 0 ); + solver2_canceluntil_rollback( s, s->iSimpPivot ); // reset problem clauses if ( s->hClausePivot < veci_size(&s->clauses) ) { |