diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-06 20:54:41 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-06 20:54:41 -0800 |
commit | 542f84d2fb059a0779ee1878ee3c1cc2fdbad2df (patch) | |
tree | 41f3c34302e9c021d61d156ce69ba7163d02a14f /src/sat/satoko | |
parent | 6ae1f35fae4eb7a8d569f88fe143faad8239c26c (diff) | |
download | abc-542f84d2fb059a0779ee1878ee3c1cc2fdbad2df.tar.gz abc-542f84d2fb059a0779ee1878ee3c1cc2fdbad2df.tar.bz2 abc-542f84d2fb059a0779ee1878ee3c1cc2fdbad2df.zip |
Small changes to compile satoko on Windows.
Diffstat (limited to 'src/sat/satoko')
-rw-r--r-- | src/sat/satoko/act_clause.h | 4 | ||||
-rw-r--r-- | src/sat/satoko/cnf_reader.c | 2 | ||||
-rw-r--r-- | src/sat/satoko/solver.c | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h index 5a2fda2b..2e80a1e6 100644 --- a/src/sat/satoko/act_clause.h +++ b/src/sat/satoko/act_clause.h @@ -26,9 +26,9 @@ static inline void clause_act_rescale(solver_t *s) vec_uint_foreach(s->learnts, cref, i) { clause = clause_read(s, cref); - clause->data[clause->size].act *= 1e-20; + clause->data[clause->size].act *= (float)1e-20; } - s->clause_act_inc *= 1e-20; + s->clause_act_inc *= (float)1e-20; } /** Increment the activity value of one clause ('clause') diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c index 5e4b92f9..9fbbda65 100644 --- a/src/sat/satoko/cnf_reader.c +++ b/src/sat/satoko/cnf_reader.c @@ -97,7 +97,7 @@ static void read_clause(char **token, vec_uint_t *lits) break; sign = (var > 0); var = abs(var) - 1; - vec_uint_push_back(lits, var2lit((unsigned) var, !sign)); + vec_uint_push_back(lits, var2lit((unsigned) var, (char)!sign)); } } diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 8c06bbe8..a4114e54 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -330,7 +330,7 @@ static inline int solver_rst(solver_t *s) static inline int solver_block_rst(solver_t *s) { - return s->stats.n_conflicts > s->opts.fst_block_rst && + return s->stats.n_conflicts > (int)s->opts.fst_block_rst && b_queue_is_valid(s->bq_lbd) && ((long)vec_uint_size(s->trail) > (s->opts.b_rst * (long)b_queue_avg(s->bq_trail))); } |