mirror of
https://github.com/YosysHQ/abc.git
synced 2026-09-01 18:27:44 +02:00
Small changes to compile satoko on Windows.
This commit is contained in:
@@ -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')
|
||||
|
||||
@@ -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));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -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)));
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user