diff options
| -rw-r--r-- | src/aig/gia/giaUtil.c | 2 | ||||
| -rw-r--r-- | src/sat/satoko/satoko.h | 4 | ||||
| -rw-r--r-- | src/sat/satoko/solver_api.c | 10 |
3 files changed, 8 insertions, 8 deletions
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index d64c53fa..d100b6c1 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -2063,7 +2063,7 @@ void Gia_AigerWriteLut( Gia_Man_t * p, char * pFileName ) ***********************************************************************/ void Gia_ManDetectMuxes( Gia_Man_t * p ) { - Gia_Obj_t * pObj, * pNodeT, * pNodeE; int i; + Gia_Obj_t * pObj = NULL, * pNodeT, * pNodeE; int i; Gia_ManForEachObj( p, pObj, i ); if ( Gia_ObjIsAnd(pObj) && Gia_ObjRecognizeMux(pObj, &pNodeT, &pNodeE) ) pObj->fMark0 = 1; diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 7c2f3720..2d3e056e 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -84,8 +84,8 @@ extern void satoko_default_opts(satoko_opts_t *); extern void satoko_configure(satoko_t *, satoko_opts_t *); extern int satoko_parse_dimacs(char *, satoko_t **); extern int satoko_add_variable(satoko_t *, char); -extern int satoko_add_clause(satoko_t *, unsigned *, unsigned); -extern void satoko_assump_push(satoko_t *s, unsigned); +extern int satoko_add_clause(satoko_t *, int *, int); +extern void satoko_assump_push(satoko_t *s, int); extern void satoko_assump_pop(satoko_t *s); extern int satoko_simplify(satoko_t *); extern int satoko_solve(satoko_t *); diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index e03cc084..e4fd88b7 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -234,7 +234,7 @@ int satoko_add_variable(solver_t *s, char sign) return var; } -int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) +int satoko_add_clause(solver_t *s, int *lits, int size) { unsigned i, j; unsigned prev_lit; @@ -249,10 +249,10 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) vec_uint_clear(s->temp_lits); j = 0; prev_lit = UNDEF; - for (i = 0; i < size; i++) { - if (lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE) + for (i = 0; i < (unsigned)size; i++) { + if ((unsigned)lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE) return SATOKO_OK; - else if (lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) { + else if ((unsigned)lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) { prev_lit = lits[i]; vec_uint_push_back(s->temp_lits, lits[i]); } @@ -270,7 +270,7 @@ int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size) return SATOKO_OK; } -void satoko_assump_push(solver_t *s, unsigned lit) +void satoko_assump_push(solver_t *s, int lit) { vec_uint_push_back(s->assumptions, lit); } |