summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/sat/satoko/clause.h14
-rw-r--r--src/sat/satoko/cnf_reader.c2
-rw-r--r--src/sat/satoko/satoko.h11
-rw-r--r--src/sat/satoko/solver.c2
-rw-r--r--src/sat/satoko/solver_api.c48
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