diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bmc/bmcGen.c | 18 | ||||
-rw-r--r-- | src/sat/satoko/cdb.h | 6 | ||||
-rw-r--r-- | src/sat/satoko/cnf_reader.c | 2 | ||||
-rw-r--r-- | src/sat/satoko/satoko.h | 8 | ||||
-rw-r--r-- | src/sat/satoko/solver.c | 10 | ||||
-rw-r--r-- | src/sat/satoko/solver.h | 6 | ||||
-rw-r--r-- | src/sat/satoko/solver_api.c | 65 | ||||
-rw-r--r-- | src/sat/satoko/types.h | 1 | ||||
-rw-r--r-- | src/sat/satoko/utils/heap.h | 5 | ||||
-rw-r--r-- | src/sat/satoko/watch_list.h | 12 |
10 files changed, 106 insertions, 27 deletions
diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c index 5d84ce87..460c9fec 100644 --- a/src/sat/bmc/bmcGen.c +++ b/src/sat/bmc/bmcGen.c @@ -46,13 +46,13 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj ) { - return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi ); + return Vec_WrdEntryP( p->vSims, iObj * p->nSimWords ); } static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj ) { int w; word * pSims = Gia_ManMoObj( p, iObj ); - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = Gia_ManRandomW( 0 ); } static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj ) @@ -65,19 +65,19 @@ static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj ) if ( Gia_ObjFaninC0(pObj) ) { if ( Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = ~(pSims0[w] | pSims1[w]); else - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = ~pSims0[w] & pSims1[w]; } else { if ( Gia_ObjFaninC1(pObj) ) - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = pSims0[w] & ~pSims1[w]; else - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = pSims0[w] & pSims1[w]; } } @@ -89,12 +89,12 @@ static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj ) word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) ); if ( Gia_ObjFaninC0(pObj) ) { - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = ~pSims0[w]; } else { - for ( w = 0; w < p->iPatsPi; w++ ) + for ( w = 0; w < p->nSimWords; w++ ) pSims[w] = pSims0[w]; } } @@ -102,7 +102,7 @@ void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords ) { int i, iObj; Gia_ManRandomW( 1 ); - p->iPatsPi = nWords; + p->nSimWords = nWords; if ( p->vSims ) Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 ); else diff --git a/src/sat/satoko/cdb.h b/src/sat/satoko/cdb.h index 28686ff2..32b0bf93 100644 --- a/src/sat/satoko/cdb.h +++ b/src/sat/satoko/cdb.h @@ -81,6 +81,12 @@ static inline void cdb_remove(struct cdb *p, struct clause *clause) p->wasted += clause->size; } +static inline void cdb_clear(struct cdb *p) +{ + p->wasted = 0; + p->size = 0; +} + static inline unsigned cdb_capacity(struct cdb *p) { return p->cap; diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c index 9fbbda65..adb9a47b 100644 --- a/src/sat/satoko/cnf_reader.c +++ b/src/sat/satoko/cnf_reader.c @@ -141,7 +141,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver) return -1; } read_clause(&token, lits); - if (!satoko_add_clause(p, vec_uint_data(lits), vec_uint_size(lits))) { + if (!satoko_add_clause(p, (int*)vec_uint_data(lits), vec_uint_size(lits))) { vec_uint_print(lits); return 0; } diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 88070eac..a0c4d216 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -80,12 +80,14 @@ struct satoko_stats { //===------------------------------------------------------------------------=== extern satoko_t *satoko_create(void); extern void satoko_destroy(satoko_t *); +extern void satoko_reset(satoko_t *); + extern void satoko_default_opts(satoko_opts_t *); extern void satoko_configure(satoko_t *, satoko_opts_t *); extern int satoko_parse_dimacs(char *, satoko_t **); -extern void satoko_add_variable(satoko_t *, char); -extern int satoko_add_clause(satoko_t *, unsigned *, unsigned); -extern void satoko_assump_push(satoko_t *s, unsigned); +extern int satoko_add_variable(satoko_t *, char); +extern int satoko_add_clause(satoko_t *, int *, int); +extern void satoko_assump_push(satoko_t *s, int); extern void satoko_assump_pop(satoko_t *s); extern int satoko_simplify(satoko_t *); extern int satoko_solve(satoko_t *); diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 21a4860d..af3dcffb 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -195,7 +195,7 @@ static inline unsigned solver_decide(solver_t *s) if (solver_has_marks(s) && !var_mark(s, next_var)) next_var = UNDEF; } - return var2lit(next_var, vec_char_at(s->polarity, next_var)); + return var2lit(next_var, var_polarity(s, next_var)); } static inline void solver_new_decision(solver_t *s, unsigned lit) @@ -362,13 +362,14 @@ static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref) static inline void solver_analyze_final(solver_t *s, unsigned lit) { - unsigned i; + int i; + vec_uint_clear(s->final_conflict); vec_uint_push_back(s->final_conflict, lit); if (solver_dlevel(s) == 0) return; vec_char_assign(s->seen, lit2var(lit), 1); - for (i = vec_uint_size(s->trail) - 1; i <= vec_uint_at(s->trail_lim, 0); i--) { + for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, 0); i--) { unsigned var = lit2var(vec_uint_at(s->trail, i)); if (vec_char_at(s->seen, var)) { @@ -396,6 +397,9 @@ static inline void solver_garbage_collect(solver_t *s) unsigned *array; struct cdb *new_cdb = cdb_alloc(cdb_capacity(s->all_clauses) - cdb_wasted(s->all_clauses)); + if (s->book_cdb) + s->book_cdb = 0; + for (i = 0; i < 2 * vec_char_size(s->assigns); i++) { struct watcher *w; watch_list_foreach(s->watches, w, i) diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 68cc97dc..33f8ce88 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -95,6 +95,7 @@ struct solver_t_ { /* Bookmark */ unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */ unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */ + unsigned book_cdb; /* Bookmark clause database size */ unsigned book_vars; /* Bookmark number of variables */ unsigned book_trail; /* Bookmark trail size */ @@ -132,6 +133,11 @@ static inline char var_value(solver_t *s, unsigned var) return vec_char_at(s->assigns, var); } +static inline char var_polarity(solver_t *s, unsigned var) +{ + return vec_char_at(s->polarity, var); +} + static inline unsigned var_dlevel(solver_t *s, unsigned var) { return vec_uint_at(s->levels, var); diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 9cad0a14..3cb9f3d3 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -216,7 +216,7 @@ int satoko_simplify(solver_t * s) return SATOKO_OK; } -void satoko_add_variable(solver_t *s, char sign) +int satoko_add_variable(solver_t *s, char sign) { unsigned var = vec_act_size(s->activity); vec_wl_push(s->watches); @@ -231,9 +231,10 @@ void satoko_add_variable(solver_t *s, char sign) heap_insert(s->var_order, var); if (s->marks) vec_char_push_back(s->marks, 0); + return var; } -int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) +int satoko_add_clause(solver_t *s, int *lits, int size) { unsigned i, j; unsigned prev_lit; @@ -248,10 +249,10 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) vec_uint_clear(s->temp_lits); j = 0; prev_lit = UNDEF; - for (i = 0; i < size; i++) { - if (lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE) + for (i = 0; i < (unsigned)size; i++) { + if ((unsigned)lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE) return SATOKO_OK; - else if (lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) { + else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) { prev_lit = lits[i]; vec_uint_push_back(s->temp_lits, lits[i]); } @@ -269,7 +270,7 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) return SATOKO_OK; } -void satoko_assump_push(solver_t *s, unsigned lit) +void satoko_assump_push(solver_t *s, int lit) { vec_uint_push_back(s->assumptions, lit); } @@ -329,6 +330,43 @@ void satoko_unbookmark(satoko_t *s) { s->book_cl_orig = 0; s->book_cl_lrnt = 0; + s->book_cdb = 0; + s->book_vars = 0; + s->book_trail = 0; +} + +void satoko_reset(satoko_t *s) +{ + vec_uint_clear(s->assumptions); + vec_uint_clear(s->final_conflict); + cdb_clear(s->all_clauses); + vec_uint_clear(s->originals); + vec_uint_clear(s->learnts); + vec_wl_clean(s->watches); + vec_act_clear(s->activity); + heap_clear(s->var_order); + vec_uint_clear(s->levels); + vec_uint_clear(s->reasons); + vec_char_clear(s->assigns); + vec_char_clear(s->polarity); + vec_uint_clear(s->trail); + vec_uint_clear(s->trail_lim); + b_queue_clean(s->bq_lbd); + b_queue_clean(s->bq_trail); + vec_uint_clear(s->temp_lits); + vec_char_clear(s->seen); + vec_uint_clear(s->tagged); + vec_uint_clear(s->stack); + vec_uint_clear(s->last_dlevel); + vec_uint_clear(s->stamps); + s->var_act_inc = VAR_ACT_INIT_INC; + s->clause_act_inc = CLAUSE_ACT_INIT_INC; + s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce; + s->RC1 = 1; + s->RC2 = s->opts.n_conf_fst_reduce; + s->book_cl_orig = 0; + s->book_cl_lrnt = 0; + s->book_cdb = 0; s->book_vars = 0; s->book_trail = 0; } @@ -341,6 +379,11 @@ void satoko_rollback(satoko_t *s) struct clause **cl_to_remove; assert(solver_dlevel(s) == 0); + if (!s->book_vars) { + satoko_reset(s); + return; + } + cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts); /* Mark clauses */ vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig) @@ -351,18 +394,28 @@ void satoko_rollback(satoko_t *s) clause_unwatch(s, cdb_cref(s->all_clauses, (unsigned *)cl_to_remove[i])); cl_to_remove[i]->f_mark = 1; } + satoko_free(cl_to_remove); vec_uint_shrink(s->originals, s->book_cl_orig); vec_uint_shrink(s->learnts, s->book_cl_lrnt); /* Shrink variable related vectors */ + for (i = s->book_vars; i < 2 * vec_char_size(s->assigns); i++) { + vec_wl_at(s->watches, i)->size = 0; + vec_wl_at(s->watches, i)->n_bin = 0; + } + s->watches->size = s->book_vars; vec_act_shrink(s->activity, s->book_vars); vec_uint_shrink(s->levels, s->book_vars); vec_uint_shrink(s->reasons, s->book_vars); + vec_uint_shrink(s->stamps, s->book_vars); vec_char_shrink(s->assigns, s->book_vars); + vec_char_shrink(s->seen, s->book_vars); vec_char_shrink(s->polarity, s->book_vars); solver_rebuild_order(s); /* Rewind solver and cancel level 0 assignments to the trail */ solver_cancel_until(s, 0); vec_uint_shrink(s->trail, s->book_trail); + if (s->book_cdb) + s->all_clauses->size = s->book_cdb; s->book_cl_orig = 0; s->book_cl_lrnt = 0; s->book_vars = 0; diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h index 9c47ca7c..06c190ab 100644 --- a/src/sat/satoko/types.h +++ b/src/sat/satoko/types.h @@ -26,6 +26,7 @@ typedef vec_sdbl_t vec_act_t ; #define vec_act_free(vec) vec_sdbl_free(vec) #define vec_act_size(vec) vec_sdbl_size(vec) #define vec_act_data(vec) vec_sdbl_data(vec) +#define vec_act_clear(vec) vec_sdbl_clear(vec) #define vec_act_shrink(vec, size) vec_sdbl_shrink(vec, size) #define vec_act_at(vec, idx) vec_sdbl_at(vec, idx) #define vec_act_push_back(vec, value) vec_sdbl_push_back(vec, value) diff --git a/src/sat/satoko/utils/heap.h b/src/sat/satoko/utils/heap.h index 8b1d8f4b..391b8a7e 100644 --- a/src/sat/satoko/utils/heap.h +++ b/src/sat/satoko/utils/heap.h @@ -158,10 +158,7 @@ static inline void heap_build(heap_t *p, vec_uint_t *entries) static inline void heap_clear(heap_t *p) { - unsigned i; - int entry; - vec_int_foreach(p->indices, entry, i) - vec_int_assign(p->indices, i, -1); + vec_int_clear(p->indices); vec_uint_clear(p->data); } diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h index 49f419f2..1bcbf3b4 100644 --- a/src/sat/satoko/watch_list.h +++ b/src/sat/satoko/watch_list.h @@ -154,12 +154,22 @@ static inline vec_wl_t *vec_wl_alloc(unsigned cap) static inline void vec_wl_free(vec_wl_t *vec_wl) { unsigned i; - for (i = 0; i < vec_wl->size; i++) + for (i = 0; i < vec_wl->cap; i++) watch_list_free(vec_wl->watch_lists + i); satoko_free(vec_wl->watch_lists); satoko_free(vec_wl); } +static inline void vec_wl_clean(vec_wl_t *vec_wl) +{ + unsigned i; + for (i = 0; i < vec_wl->size; i++) { + vec_wl->watch_lists[i].size = 0; + vec_wl->watch_lists[i].n_bin = 0; + } + vec_wl->size = 0; +} + static inline void vec_wl_push(vec_wl_t *vec_wl) { if (vec_wl->size == vec_wl->cap) { |