diff options
| -rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 4 | ||||
| -rw-r--r-- | src/sat/glucose/Options.h | 8 | ||||
| -rw-r--r-- | src/sat/glucose/Vec.h | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 026a792e..8e82e654 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -121,8 +121,8 @@ void glucose_print_stats(Solver& s, abctime clk) { double cpu_time = (double)(unsigned)clk / CLOCKS_PER_SEC; double mem_used = memUsed(); - printf("c restarts : %d (%d conflicts on average)\n", (int)s.starts, s.starts > 0 ? s.conflicts/s.starts : 0); - printf("c blocked restarts : %d (multiple: %d) \n", (int)s.nbstopsrestarts,s.nbstopsrestartssame); + printf("c restarts : %d (%d conflicts on average)\n", (int)s.starts, s.starts > 0 ? (int)(s.conflicts/s.starts) : 0); + printf("c blocked restarts : %d (multiple: %d) \n", (int)s.nbstopsrestarts, (int)s.nbstopsrestartssame); printf("c last block at restart : %d\n", (int)s.lastblockatrestart); printf("c nb ReduceDB : %-12d\n", (int)s.nbReduceDB); printf("c nb removed Clauses : %-12d\n", (int)s.nbRemovedClauses); diff --git a/src/sat/glucose/Options.h b/src/sat/glucose/Options.h index 08e9543e..598d66d6 100644 --- a/src/sat/glucose/Options.h +++ b/src/sat/glucose/Options.h @@ -62,7 +62,7 @@ class Option struct OptionLt { bool operator()(const Option* x, const Option* y) { int test1 = strcmp(x->category, y->category); - return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; + return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0); } }; @@ -284,15 +284,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4d", range.begin); + fprintf(stderr, "%4d", (int)range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4d", range.end); + fprintf(stderr, "%4d", (int)range.end); - fprintf(stderr, "] (default: %d)\n", value); + fprintf(stderr, "] (default: %d)\n", (int)value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h index 8db84a03..f44c65f0 100644 --- a/src/sat/glucose/Vec.h +++ b/src/sat/glucose/Vec.h @@ -96,7 +96,7 @@ template<class T> void vec<T>::capacity(int min_cap) { if (cap >= min_cap) return; int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 - if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) + if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) throw OutOfMemoryException(); } |