From c7e855619a1ea5997b68a235c27187a1b43252dc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 24 Jan 2012 14:39:49 -0800 Subject: Variable timeframe abstraction. --- src/aig/gia/giaAbsVta.c | 5 +++-- src/sat/bsat/satSolver2.c | 55 ++++++++++++++++++++++++++++++++++------------- src/sat/bsat/satSolver2.h | 10 ++------- 3 files changed, 45 insertions(+), 25 deletions(-) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index e3baeb7b..4af2b7e7 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -939,8 +939,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) // check the output if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) ) printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" ); - else - printf( "Verification OK.\n" ); +// else +// printf( "Verification OK.\n" ); // produce true counter-example if ( pTop->Prio == 0 ) @@ -1285,6 +1285,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift ) int i, Entry; Vec_IntForEachEntry( vOne, Entry, i ) Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift ); + sat_solver2_simplify( p->pSat ); printf( "\n\n" ); } diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 1cc56fa9..37ae7354 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -469,6 +469,17 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from) s->reasons[v] = from; // = from << 1; s->trail[s->qtail++] = l; order_assigned(s, v); +/* + if ( solver2_dlevel(s) == 0 ) + { + satset * c = from ? clause_read( s, from ) : NULL; + printf( "Enqueing var %d on level %d with reason clause ", v, solver2_dlevel(s) ); + if ( c ) + satset_print( c ); + else + printf( "\n" ); + } +*/ return true; } } @@ -490,6 +501,11 @@ static void solver2_canceluntil(sat_solver2* s, int level) { int bound; int lastLev; int c, x; + + if ( level == 0 ) + { + int ss = 0; + } if (solver2_dlevel(s) <= level) return; @@ -501,12 +517,9 @@ static void solver2_canceluntil(sat_solver2* s, int level) { for (c = s->qtail-1; c >= bound; c--) { x = lit_var(trail[c]); + var_set_value(s, x, varX); s->reasons[x] = 0; -// if ( s->units[x] == 0 || var_level(s, x) > 0 ) - { - var_set_value(s, x, varX); - s->units[x] = 0; // temporary? - } + s->units[x] = 0; // temporary? if ( c < lastLev ) var_set_polar(s, x, !lit_sign(trail[c])); } @@ -519,7 +532,7 @@ static void solver2_canceluntil(sat_solver2* s, int level) { } -static void solver2_record(sat_solver2* s, veci* cls, int proof_id) +static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUnit) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); @@ -527,7 +540,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id) assert(veci_size(cls) > 0); if ( veci_size(cls) == 1 ) { - if ( s->fProofLogging ) + if ( s->fProofLogging && !fSkipUnit) var_set_unit_clause(s, lit_var(begin[0]), Cid); Cid = 0; } @@ -1009,11 +1022,16 @@ static lbool clause_simplify(sat_solver2* s, satset* c) int sat_solver2_simplify(sat_solver2* s) { + int TailOld = s->qtail; // int type; int Counter = 0; assert(solver2_dlevel(s) == 0); + // reset the head + s->qhead = 0; if (solver2_propagate(s) != 0) return false; +// printf( "Tail moved from %d to %d.\n", TailOld, s->qtail ); + if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) return true; /* @@ -1108,8 +1126,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) #ifdef SAT_USE_ANALYZE_FINAL proof_id = solver2_analyze_final(s, confl, 0); assert( proof_id > 0 ); -// if ( proof_id > 0 ) - solver2_record(s,&s->conf_final, proof_id); + solver2_record(s,&s->conf_final, proof_id, 0); #endif veci_delete(&learnt_clause); return l_False; @@ -1120,7 +1137,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level; blevel = s->root_level > blevel ? s->root_level : blevel; solver2_canceluntil(s,blevel); - solver2_record(s,&learnt_clause, proof_id); + solver2_record(s,&learnt_clause, proof_id, 0); #ifdef SAT_USE_ANALYZE_FINAL // if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) @@ -1584,13 +1601,20 @@ void sat_solver2_rollback( sat_solver2* s ) if ( s->units[i] && !clause_is_used(s, s->units[i]) ) s->units[i] = 0; } - // reset + // reset implication queue + assert( (&s->trail_lim)->ptr[0] == s->simpdb_assigns ); + assert( s->simpdb_assigns >= s->iSimpPivot ); + (&s->trail_lim)->ptr[0] = s->iSimpPivot; + s->simpdb_assigns = s->iSimpPivot; + solver2_canceluntil( s, 0 ); + // reset problem clauses if ( s->hClausePivot < veci_size(&s->clauses) ) { satset* first = satset_read(&s->clauses, s->hClausePivot); s->stats.clauses = first->Id; veci_resize(&s->clauses, s->hClausePivot); } + // resetn learned clauses if ( s->hLearntPivot < veci_size(&s->learnts) ) { satset* first = satset_read(&s->learnts, s->hLearntPivot); @@ -1602,6 +1626,7 @@ void sat_solver2_rollback( sat_solver2* s ) s->stats.learnts = first->Id; veci_resize(&s->learnts, s->hLearntPivot); } + // reset watcher lists for ( i = 2*s->iVarPivot; i < 2*s->size; i++ ) s->wlists[i].size = 0; s->size = s->iVarPivot; @@ -1804,7 +1829,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (var_level(s, lit_var(p)) > 0) veci_push(&s->conf_final, p); } - solver2_record(s, &s->conf_final, proof_id); + solver2_record(s, &s->conf_final, proof_id, 1); solver2_canceluntil(s, 0); return l_False; } @@ -1815,7 +1840,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim proof_id = solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); solver2_canceluntil(s, 0); - solver2_record(s,&s->conf_final, proof_id); + solver2_record(s,&s->conf_final, proof_id, 1); return l_False; } } @@ -1866,8 +1891,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim printf("==============================================================================\n"); solver2_canceluntil(s,0); - if ( status == l_True ) - sat_solver2_verify( s ); +// if ( status == l_True ) +// sat_solver2_verify( s ); return status; } diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 221ba3e8..2c5f8bf4 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -115,6 +115,7 @@ struct sat_solver2_t int hLearntPivot; // the pivot among learned clause int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) int iVarPivot; // the pivot among the variables + int iSimpPivot; // marker of unit-clauses veci claActs; // clause activities veci claProofs; // clause proofs @@ -223,14 +224,6 @@ static inline void sat_solver2_act_var_clear(sat_solver2* s) s->activity[i] = 0;//.0; s->var_inc = 1.0; } -static inline void sat_solver2_compress(sat_solver2* s) -{ - if ( s->qtail != s->qhead ) - { - int RetValue = sat_solver2_simplify(s); - assert( RetValue != 0 ); - } -} static inline int sat_solver2_final(sat_solver2* s, int ** ppArray) { @@ -257,6 +250,7 @@ static inline void sat_solver2_bookmark(sat_solver2* s) s->hLearntPivot = veci_size(&s->learnts); s->hClausePivot = veci_size(&s->clauses); s->iVarPivot = s->size; + s->iSimpPivot = s->simpdb_assigns; } static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) -- cgit v1.2.3