diff options
| -rw-r--r-- | src/sat/satoko/clause.h | 14 | ||||
| -rw-r--r-- | src/sat/satoko/cnf_reader.c | 2 | ||||
| -rw-r--r-- | src/sat/satoko/satoko.h | 11 | ||||
| -rw-r--r-- | src/sat/satoko/solver.c | 2 | ||||
| -rw-r--r-- | src/sat/satoko/solver_api.c | 48 |
5 files changed, 74 insertions, 3 deletions
diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h index 2be18cd6..9b05868b 100644 --- a/src/sat/satoko/clause.h +++ b/src/sat/satoko/clause.h @@ -59,5 +59,19 @@ static inline void clause_print(struct clause *clause) printf("}\n"); } +static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var) +{ + unsigned i; + for (i = 0; i < clause->size; i++) { + int var = (clause->data[i].lit >> 1); + char pol = (clause->data[i].lit & 1); + fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var)); + } + if (no_zero_var) + fprintf(file, "0\n"); + else + fprintf(file, "\n"); +} + ABC_NAMESPACE_HEADER_END #endif /* satoko__clause_h */ diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c index adb9a47b..8223affd 100644 --- a/src/sat/satoko/cnf_reader.c +++ b/src/sat/satoko/cnf_reader.c @@ -150,7 +150,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver) vec_uint_free(lits); satoko_free(buffer); *solver = p; - return satoko_simplify(p); + return SATOKO_OK; } ABC_NAMESPACE_IMPL_END diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index a0c4d216..6634e68e 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -60,6 +60,7 @@ struct satoko_opts { unsigned clause_min_lbd_bin_resol; float garbage_max_ratio; char verbose; + char no_simplify; }; typedef struct satoko_stats satoko_stats_t; @@ -108,6 +109,16 @@ extern void satoko_unbookmark(satoko_t *); */ extern int satoko_final_conflict(satoko_t *, unsigned *); +/* Procedure to dump a DIMACS file. + * - It receives as input the solver, a file name string and two integers. + * - If the file name string is NULL the solver will dump in stdout. + * - The first argument can be either 0 or 1 and is an option to dump learnt + * clauses. (value 1 will dump them). + * - The seccond argument can be either 0 or 1 and is an option to use 0 as a + * variable ID or not. Keep in mind that if 0 is used as an ID the generated + * file will not be a DIMACS. (value 1 will use 0 as ID). + */ +extern void satoko_write_dimacs(satoko_t *, char *, int, int); extern satoko_stats_t satoko_stats(satoko_t *); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index af3dcffb..42bc6448 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -644,7 +644,7 @@ char solver_search(solver_t *s) solver_cancel_until(s, 0); return SATOKO_UNDEC; } - if (solver_dlevel(s) == 0) + if (!s->opts.no_simplify && solver_dlevel(s) == 0) satoko_simplify(s); /* Reduce the set of learnt clauses */ diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 3cb9f3d3..dada33cc 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -152,6 +152,7 @@ void satoko_default_opts(satoko_opts_t *opts) { memset(opts, 0, sizeof(satoko_opts_t)); opts->verbose = 0; + opts->no_simplify = 0; /* Limits */ opts->conf_limit = 0; opts->prop_limit = 0; @@ -290,6 +291,10 @@ int satoko_solve(solver_t *s) //if (s->opts.verbose) // print_opts(s); + if (!s->opts.no_simplify) + if (satoko_simplify(s) != SATOKO_OK) + return SATOKO_UNDEC; + while (status == SATOKO_UNDEC) { status = solver_search(s); if (solver_check_limits(s) == 0) @@ -297,6 +302,7 @@ int satoko_solve(solver_t *s) } if (s->opts.verbose) print_stats(s); + solver_cancel_until(s, vec_uint_size(s->assumptions)); return status; } @@ -309,7 +315,6 @@ int satoko_final_conflict(solver_t *s, unsigned *out) memcpy(out, vec_uint_data(s->final_conflict), sizeof(unsigned) * vec_uint_size(s->final_conflict)); return vec_uint_size(s->final_conflict); - } satoko_stats_t satoko_stats(satoko_t *s) @@ -324,6 +329,7 @@ void satoko_bookmark(satoko_t *s) s->book_cl_lrnt = vec_uint_size(s->learnts); s->book_vars = vec_char_size(s->assigns); s->book_trail = vec_uint_size(s->trail); + s->opts.no_simplify = 1; } void satoko_unbookmark(satoko_t *s) @@ -333,6 +339,7 @@ void satoko_unbookmark(satoko_t *s) s->book_cdb = 0; s->book_vars = 0; s->book_trail = 0; + s->opts.no_simplify = 0; } void satoko_reset(satoko_t *s) @@ -442,4 +449,43 @@ void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars) var_clean_mark(s, pvars[i]); } +void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) +{ + FILE *file; + unsigned i; + unsigned n_vars = vec_act_size(s->activity); + unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->assumptions); + unsigned n_lrnts = vec_uint_size(s->learnts); + unsigned *array; + + assert(wrt_lrnt == 0 || wrt_lrnt == 1); + assert(zero_var == 0 || zero_var == 1); + if (fname != NULL) + file = fopen(fname, "w"); + else + file = stdout; + + if (file == NULL) { + printf( "Error: Cannot open output file.\n"); + return; + } + fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig); + array = vec_uint_data(s->assumptions); + for (i = 0; i < vec_uint_size(s->assumptions); i++) + fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var); + + array = vec_uint_data(s->originals); + for (i = 0; i < vec_uint_size(s->originals); i++) + clause_dump(file, clause_read(s, array[i]), !zero_var); + + if (wrt_lrnt) { + printf(" Lertns %u", n_lrnts); + array = vec_uint_data(s->learnts); + for (i = 0; i < n_lrnts; i++) + clause_dump(file, clause_read(s, array[i]), !zero_var); + } + +} + + ABC_NAMESPACE_IMPL_END |