summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcGen.c18
-rw-r--r--src/sat/satoko/cdb.h6
-rw-r--r--src/sat/satoko/cnf_reader.c2
-rw-r--r--src/sat/satoko/satoko.h8
-rw-r--r--src/sat/satoko/solver.c10
-rw-r--r--src/sat/satoko/solver.h6
-rw-r--r--src/sat/satoko/solver_api.c65
-rw-r--r--src/sat/satoko/types.h1
-rw-r--r--src/sat/satoko/utils/heap.h5
-rw-r--r--src/sat/satoko/watch_list.h12
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) {
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-24 23:12:04 +0000