summaryrefslogtreecommitdiffstats
path: root/src/sat/satoko
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-08-28 11:15:00 +0200
committerBruno Schmitt <bruno@oschmitt.com>2017-08-28 11:15:00 +0200
commitd0f81fcf2952b8a46548c0dd74f95fa1cd0a504f (patch)
treef963459de39b36d8ca71166e9afc5761b3cdafe0 /src/sat/satoko
parent3df049f37df1f02feaf7585a04f2e07e5fd33fbc (diff)
downloadabc-d0f81fcf2952b8a46548c0dd74f95fa1cd0a504f.tar.gz
abc-d0f81fcf2952b8a46548c0dd74f95fa1cd0a504f.tar.bz2
abc-d0f81fcf2952b8a46548c0dd74f95fa1cd0a504f.zip
[Satoko] Small fix.
Diffstat (limited to 'src/sat/satoko')
-rw-r--r--src/sat/satoko/solver_api.c12
1 files changed, 8 insertions, 4 deletions
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index d404992e..0d073ec7 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -531,10 +531,14 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
return;
}
fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
- for (i = 0; i < vec_char_size(s->assigns); i++)
- if ( var_value(s, i) != VAR_UNASSING )
- fprintf(file, "%d %d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var, zero_var ? : 0);
-
+ for (i = 0; i < vec_char_size(s->assigns); i++) {
+ if ( var_value(s, i) != VAR_UNASSING ) {
+ if (zero_var)
+ fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i) : i);
+ else
+ fprintf(file, "%d 0\n", var_value(s, i) == LIT_FALSE ? -(int)(i + 1) : i + 1);
+ }
+ }
array = vec_uint_data(s->originals);
for (i = 0; i < vec_uint_size(s->originals); i++)
clause_dump(file, clause_fetch(s, array[i]), !zero_var);