Small changes to support old compilers.

src/base/abci/abc.c

@@ -23357,7 +23357,7 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
         int status;
 
         satoko_parse_dimacs( pFileName, &p );
-    satoko_configure(p, &opts);
+        satoko_configure(p, &opts);
 
         clk = Abc_Clock();
         status = satoko_solve( p );

src/sat/satoko/satoko.h

@@ -30,8 +30,8 @@ typedef struct solver_t_ satoko_t;
 typedef struct satoko_opts satoko_opts_t;
 struct satoko_opts {
     /* Limits */
-    long long conf_limit;  /* Limit on the n.of conflicts */
-    long long prop_limit;  /* Limit on the n.of implications */
+    long conf_limit;  /* Limit on the n.of conflicts */
+    long prop_limit;  /* Limit on the n.of implications */
 
     /* Constants used for restart heuristic */
     double f_rst;          /* Used to force a restart */

src/sat/satoko/solver.c

@@ -325,14 +325,14 @@ static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt
 static inline int solver_rst(solver_t *s)
 {
     return b_queue_is_valid(s->bq_lbd) &&
-           (((long long)b_queue_avg(s->bq_lbd) * s->opts.f_rst) > (s->sum_lbd / s->stats.n_conflicts));
+           (((long)b_queue_avg(s->bq_lbd) * s->opts.f_rst) > (s->sum_lbd / s->stats.n_conflicts));
 }
 
 static inline int solver_block_rst(solver_t *s)
 {
     return s->stats.n_conflicts > s->opts.fst_block_rst &&
            b_queue_is_valid(s->bq_lbd) &&
-           (vec_uint_size(s->trail) > (s->opts.b_rst * (long long)b_queue_avg(s->bq_trail)));
+           ((long)vec_uint_size(s->trail) > (s->opts.b_rst * (long)b_queue_avg(s->bq_trail)));
 }
 
 static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref)

src/sat/satoko/solver.h

@@ -42,13 +42,13 @@ struct satoko_stats {
     unsigned n_starts;
     unsigned n_reduce_db;
 
-    long long n_decisions;
-    long long n_propagations;
-    long long n_inspects;
-    long long n_conflicts;
+    long n_decisions;
+    long n_propagations;
+    long n_inspects;
+    long n_conflicts;
 
-    long long n_original_lits;
-    long long n_learnt_lits;
+    long n_original_lits;
+    long n_learnt_lits;
 };
 
 typedef struct solver_t_ solver_t;
@@ -82,17 +82,9 @@ struct solver_t_ {
     unsigned i_qhead; /* Head of propagation queue (as index into the trail). */
     unsigned n_assigns_simplify; /* Number of top-level assignments since
                     last execution of 'simplify()'. */
-    long long n_props_simplify;  /* Remaining number of propagations that
-                    must be made before next execution of
-                    'simplify()'. */
-
-    /* Temporary data used by Search method */
-    b_queue_t *bq_trail;
-    b_queue_t *bq_lbd;
-    long RC1;
-    long RC2;
-    unsigned n_confl_bfr_reduce;
-    float sum_lbd;
+    long n_props_simplify;  /* Remaining number of propagations that
+                   must be made before next execution of
+                   'simplify()'. */
 
     /* Temporary data used by Analyze */
     vec_uint_t *temp_lits;
@@ -101,10 +93,18 @@ struct solver_t_ {
     vec_uint_t *stack;
     vec_uint_t *last_dlevel;
 
+    /* Temporary data used by Search method */
+    b_queue_t *bq_trail;
+    b_queue_t *bq_lbd;
+    long RC1;
+    long RC2;
+    long n_confl_bfr_reduce;
+    float sum_lbd;
+
     /* Misc temporary */
+    unsigned cur_stamp; /* Used for marking literals and levels of interest */
     vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
                  * clauses minimization with binary resolution */
-    unsigned cur_stamp; /* Used for marking literals and levels of interest */
 
     struct satoko_stats stats;
     struct satoko_opts opts;

src/sat/satoko/solver_api.c

@@ -68,9 +68,9 @@ static inline void print_opts(solver_t *s)
 static inline void print_stats(solver_t *s)
 {
     printf("starts        : %10d\n", s->stats.n_starts);
-    printf("conflicts     : %10lld\n", s->stats.n_conflicts);
-    printf("decisions     : %10lld\n", s->stats.n_decisions);
-    printf("propagations  : %10lld\n", s->stats.n_propagations);
+    printf("conflicts     : %10ld\n", s->stats.n_conflicts);
+    printf("decisions     : %10ld\n", s->stats.n_decisions);
+    printf("propagations  : %10ld\n", s->stats.n_propagations);
 }
 
 //===------------------------------------------------------------------------===
@@ -166,13 +166,13 @@ void satoko_default_opts(satoko_opts_t *opts)
     opts->inc_special_reduce = 1000;
     opts->lbd_freeze_clause = 30;
     /* VSIDS heuristic */
-    opts->var_decay = 0.95;
-    opts->clause_decay = 0.995;
+    opts->var_decay = (act_t) 0.95;
+    opts->clause_decay = (clause_act_t) 0.995;
     /* Binary resolution */
     opts->clause_max_sz_bin_resol = 30;
     opts->clause_min_lbd_bin_resol = 6;
 
-    opts->garbage_max_ratio = 0.3;
+    opts->garbage_max_ratio = (float) 0.3;
 }
 
 /**

src/sat/satoko/utils/b_queue.h

@@ -21,7 +21,7 @@ struct b_queue_t_ {
     unsigned cap;
     unsigned i_first;
     unsigned i_empty;
-    unsigned long long sum;
+    unsigned long sum;
     unsigned *data;
 };
 
@@ -61,7 +61,7 @@ static inline void b_queue_push(b_queue_t *p, unsigned Value)
 
 static inline unsigned b_queue_avg(b_queue_t *p)
 {
-    return (unsigned)(p->sum / ((unsigned long long) p->size));
+    return (unsigned)(p->sum / ((unsigned long) p->size));
 }
 
 static inline unsigned b_queue_is_valid(b_queue_t *p)

src/sat/satoko/utils/misc.h

@@ -9,8 +9,6 @@
 #ifndef satoko__utils__misc_h
 #define satoko__utils__misc_h
 
-#include <stdint.h>
-
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 

src/sat/satoko/utils/vec/vec_char.h

@@ -248,9 +248,10 @@ static inline long vec_char_memory(vec_char_t *p)
 
 static inline void vec_char_print(vec_char_t* p)
 {
+    unsigned i;
     assert(p != NULL);
     fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
-    for (unsigned i = 0; i < p->size; i++)
+    for (i = 0; i < p->size; i++)
         fprintf(stdout, " %d", p->data[i]);
     fprintf(stdout, " }\n");
 }

src/sat/satoko/watch_list.h

@@ -113,7 +113,8 @@ static inline vec_wl_t *vec_wl_alloc(unsigned cap)
 
 static inline void vec_wl_free(vec_wl_t *vec_wl)
 {
-    for (unsigned i = 0; i < vec_wl->size; i++)
+    unsigned i;
+    for (i = 0; i < vec_wl->size; i++)
         watch_list_free(vec_wl->watch_lists + i);
     satoko_free(vec_wl->watch_lists);
     satoko_free(vec_wl);