Skip to content

Commit b0fb916

Browse files
Merge pull request #75 from tzik/pri
Specify variable size explicitly in format strings
2 parents 5e7e83d + da371a9 commit b0fb916

File tree

3 files changed

+28
-26
lines changed

3 files changed

+28
-26
lines changed

minisat/core/Solver.cc

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2618,7 +2618,7 @@ lbool Solver::search(int &nof_conflicts)
26182618
// simplify
26192619
//
26202620
if (lcm && conflicts >= curSimplify * nbconfbeforesimplify) {
2621-
TRACE(printf("c ### simplifyAll on conflict : %ld\n", conflicts);)
2621+
TRACE(printf("c ### simplifyAll on conflict : %" PRId64 "\n", conflicts);)
26222622
if (verbosity >= 1)
26232623
printf("c schedule LCM with: nbClauses: %d, nbLearnts_core: %d, nbLearnts_tier2: %d, nbLearnts_local: %d, "
26242624
"nbLearnts: %d\n",
@@ -2659,7 +2659,7 @@ lbool Solver::search(int &nof_conflicts)
26592659

26602660
conflicts++;
26612661
nof_conflicts--;
2662-
TRACE(printf("c hit conflict %ld\n", conflicts);)
2662+
TRACE(printf("c hit conflict %" PRId64 "\n", conflicts);)
26632663
if (conflicts == 100000 && learnts_core.size() < 100) core_lbd_cut = 5;
26642664
ConflictData data = FindConflictLevel(confl);
26652665
if (data.nHighestLevel == 0) return l_False;
@@ -3295,7 +3295,7 @@ bool Solver::inprocessing()
32953295
int Z = 0, i, j, k, l = -1, p;
32963296

32973297
if (verbosity > 0)
3298-
printf("c inprocessing simplify at try %ld, next limit: %ld\n", inprocess_attempts, inprocess_next_lim);
3298+
printf("c inprocessing simplify at try %" PRId64 ", next limit: %" PRId64 "\n", inprocess_attempts, inprocess_next_lim);
32993299
// fill occurrence data structure
33003300
O.resize(2 * nVars());
33013301

@@ -3520,16 +3520,16 @@ void Solver::printStats()
35203520
starts, restart.partialRestarts, restart.savedDecisions, restart.savedPropagations,
35213521
((double)restart.savedPropagations * 100.0) / (double)propagations);
35223522
printf("c polarity : %d pos, %d neg\n", posMissingInSome, negMissingInSome);
3523-
printf("c LCM : %lu runs, %lu Ctried, %lu Cshrinked (%lu known duplicates), %lu Ldeleted, %lu "
3524-
"Lrev-deleted\n",
3523+
printf("c LCM : %" PRIu64 " runs, %" PRIu64 " Ctried, %" PRIu64 " Cshrinked (%" PRIu64
3524+
" known duplicates), %" PRIu64 " Ldeleted, %" PRIu64 " Lrev-deleted\n",
35253525
nbSimplifyAll, LCM_total_tries, LCM_successful_tries, nr_lcm_duplicates, LCM_dropped_lits, LCM_dropped_reverse);
3526-
printf("c Inprocessing : %lu subsumed, %lu dropped lits, %lu attempts, %lu mems\n", inprocessing_C,
3527-
inprocessing_L, inprocessings, inprocess_mems);
3528-
printf("c Stats: : %lf solve, %lu steps, %lf simp, %lu steps, %d var, budget: %d\n", statistics.solveSeconds,
3529-
statistics.solveSteps, statistics.simpSeconds, statistics.simpSteps, nVars(), withinBudget());
3530-
printf("c backup trail: stored: %lu used successfully: %lu\n", backuped_trail_lits, used_backup_lits);
3531-
printf("c accesses: clauses: %lu occurrences: %lu sum: %lu\n", counter_access.clause(),
3532-
counter_access.occurrence(), counter_access.sum());
3526+
printf("c Inprocessing : %" PRIu64 " subsumed, %" PRIu64 " dropped lits, %" PRIu64 " attempts, %" PRIu64 " mems\n",
3527+
inprocessing_C, inprocessing_L, inprocessings, inprocess_mems);
3528+
printf("c Stats: : %lf solve, %" PRIu64 " steps, %lf simp, %" PRIu64 " steps, %d var, budget: %d\n",
3529+
statistics.solveSeconds, statistics.solveSteps, statistics.simpSeconds, statistics.simpSteps, nVars(), withinBudget());
3530+
printf("c backup trail: stored: %" PRIu64 " used successfully: %" PRIu64 "\n", backuped_trail_lits, used_backup_lits);
3531+
printf("c accesses: clauses: %" PRIu64 " occurrences: %" PRIu64 " sum: %" PRIu64 "\n",
3532+
counter_access.clause(), counter_access.occurrence(), counter_access.sum());
35333533
printf("c CPU time : %g s\n", cpu_time);
35343534
}
35353535

minisat/simp/Main.cc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -240,7 +240,7 @@ int main(int argc, char **argv)
240240
double simplified_time = cpuTime();
241241
if (S.verbosity > 0) {
242242
printf("c | Simplification time: %12.2f s |\n", simplified_time - parsed_time);
243-
printf("c | Simplification steps: %12ld |\n", S.counter_sum());
243+
printf("c | Simplification steps: %12" PRId64 " |\n", S.counter_sum());
244244
printf("c | |\n");
245245
}
246246

minisat/utils/Options.h

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -630,10 +630,10 @@ class Int64Option : public Option
630630
void checkValueOrExit(int64_t tmp)
631631
{
632632
if (tmp > range.end) {
633-
fprintf(stderr, "ERROR! value <%ld> is too large for option \"%s\".\n", tmp, name);
633+
fprintf(stderr, "ERROR! value <%" PRId64 "> is too large for option \"%s\".\n", tmp, name);
634634
exit(1);
635635
} else if (tmp < range.begin) {
636-
fprintf(stderr, "ERROR! value <%ld> is too small for option \"%s\".\n", tmp, name);
636+
fprintf(stderr, "ERROR! value <%" PRId64 "> is too small for option \"%s\".\n", tmp, name);
637637
exit(1);
638638
}
639639
}
@@ -734,23 +734,25 @@ class Int64Option : public Option
734734
if (i != 0) {
735735
fprintf(pcsFile, ",");
736736
}
737-
fprintf(pcsFile, "%ld", values[i]);
737+
fprintf(pcsFile, "%" PRId64, values[i]);
738738
}
739-
fprintf(pcsFile, "} [%ld] # %s\n", value, description);
739+
fprintf(pcsFile, "} [%" PRId64 "] # %s\n", value, description);
740740
} else {
741741
if ((range.end - range.begin <= 16 && range.end - range.begin > 0 && range.end != INT32_MAX) ||
742742
(range.begin <= 0 && range.end >= 0)) {
743743
if (range.end - range.begin <= 16 && range.end - range.begin > 0) { // print all values if the difference is really small
744-
fprintf(pcsFile, "%s {%ld", name, range.begin);
744+
fprintf(pcsFile, "%s {%" PRId64, name, range.begin);
745745
for (int64_t i = range.begin + 1; i <= range.end; ++i) {
746-
fprintf(pcsFile, ",%ld", i);
746+
fprintf(pcsFile, ",%" PRId64, i);
747747
}
748-
fprintf(pcsFile, "} [%ld] # %s\n", value, description);
748+
fprintf(pcsFile, "} [%" PRId64 "] # %s\n", value, description);
749749
} else {
750-
fprintf(pcsFile, "%s [%ld,%ld] [%ld]i # %s\n", name, range.begin, range.end, value, description);
750+
fprintf(pcsFile, "%s [%" PRId64 ",%" PRId64 "] [%" PRId64 "]i # %s\n", name, range.begin,
751+
range.end, value, description);
751752
}
752753
} else {
753-
fprintf(pcsFile, "%s [%ld,%ld] [%ld]il # %s\n", name, range.begin, range.end, value, description);
754+
fprintf(pcsFile, "%s [%" PRId64 ",%" PRId64 "] [%" PRId64 "]il # %s\n", name, range.begin, range.end,
755+
value, description);
754756
}
755757
}
756758
}
@@ -768,8 +770,8 @@ class Int64Option : public Option
768770
for (size_t i = 0; i < values.size(); ++i) {
769771
if (values[i] == defaultValue) {
770772
continue;
771-
} // do not print default value
772-
snprintf(buffer, size, "%ld", values[i]); // convert value
773+
} // do not print default value
774+
snprintf(buffer, size, "%" PRId64, values[i]); // convert value
773775
const int sl = strlen(buffer);
774776
size = size - strlen(buffer) - 1; // store new size
775777
if (i + 1 < values.size() && values[i + 1] != defaultValue) {
@@ -782,8 +784,8 @@ class Int64Option : public Option
782784
for (int64_t i = range.begin; i <= range.end; ++i) {
783785
if (i == defaultValue) {
784786
continue;
785-
} // do not print default value
786-
snprintf(buffer, size, "%ld", i); // convert value
787+
} // do not print default value
788+
snprintf(buffer, size, "%" PRId64, i); // convert value
787789
const int sl = strlen(buffer);
788790
size = size - strlen(buffer) - 1; // store new size
789791
if (i != range.end && i + 1 != defaultValue) {

0 commit comments

Comments
 (0)