Skip to content

N
naps
Commit 7d9365c7 authored by Masahiko Sakai's avatar Masahiko Sakai
Browse files
Options

Merge branch 'cpp11' into 'master' 

compiler error related c++11

See merge request !2
parents 6d9191a6 7f592eee
Hide whitespace changes
Inline Side-by-side
Showing with 38 additions and 38 deletions
ccminisat/core/Main.cc
View file @ 7d9365c7
......@@ -38,11 +38,11 @@ void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
printf("restarts : %" PRIu64"\n", solver.starts);
printf("conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
......
ccminisat/simp/Main.cc
View file @ 7d9365c7
......@@ -39,11 +39,11 @@ void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
printf("restarts : %" PRIu64"\n", solver.starts);
printf("conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
......
ccminisat/utils/Options.h
View file @ 7d9365c7
......@@ -282,15 +282,15 @@ class Int64Option : public Option
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
fprintf(stderr, "%4"PRIi64, range.begin);
fprintf(stderr, "%4" PRIi64, range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
fprintf(stderr, "%4"PRIi64, range.end);
fprintf(stderr, "%4" PRIi64, range.end);
fprintf(stderr, "] (default: %"PRIi64")\n", value);
fprintf(stderr, "] (default: %" PRIi64")\n", value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
......
es1sat/core/Main.cc
View file @ 7d9365c7
......@@ -38,11 +38,11 @@ void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
printf("restarts : %" PRIu64"\n", solver.starts);
printf("conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
......
es1sat/simp/Main.cc
View file @ 7d9365c7
......@@ -39,11 +39,11 @@ void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
printf("restarts : %" PRIu64"\n", solver.starts);
printf("conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
......
es1sat/utils/Options.h
View file @ 7d9365c7
......@@ -282,15 +282,15 @@ class Int64Option : public Option
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
fprintf(stderr, "%4"PRIi64, range.begin);
fprintf(stderr, "%4" PRIi64, range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
fprintf(stderr, "%4"PRIi64, range.end);
fprintf(stderr, "%4" PRIi64, range.end);
fprintf(stderr, "] (default: %"PRIi64")\n", value);
fprintf(stderr, "] (default: %" PRIi64")\n", value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
......
glueminisat/core/Solver.cc
View file @ 7d9365c7
......@@ -653,7 +653,7 @@ int Solver::permutatedTrail()
removed_propagations += trail_lim[restart_lv] - trail_lim[0];
}
// if (restart_lv > 0)
// printf("lw-restart Level: %4d/%4d (%5.1f%%, %-6"PRIu64")\n", restart_lv, decisionLevel(), (float)restart_lv * 100 / decisionLevel(), starts);
// printf("lw-restart Level: %4d/%4d (%5.1f%%, %-6" PRIu64")\n", restart_lv, decisionLevel(), (float)restart_lv * 100 / decisionLevel(), starts);
if (lw_restart == LW_USE)
return restart_lv;
......@@ -1284,7 +1284,7 @@ void Solver::reduceDB()
// added by nabesima
if (verbosity >= 1) {
printf("c < RDB %-5d(%6"PRIu64"res,%5.0fcnfs/res,%5.1f%%, %6db %7dg %7dg3) >\n",
printf("c < RDB %-5d(%6" PRIu64"res,%5.0fcnfs/res,%5.1f%%, %6db %7dg %7dg3) >\n",
reduce_dbs, starts, (double)conflicts / starts, (double)nLearnts() / org_learnts * 100.0,
num_bin, num_glue, num_glue3);
printLog();
......@@ -1735,7 +1735,7 @@ lbool Solver::solve_()
break;
case VD_SIGMOID:
var_decay = init_var_decay + (max_var_decay - init_var_decay) / (1 + exp(-((double)10 * starts / var_decay_period - 10)));
//printf("%"PRIu64" restarts, var_decay = %f\n", starts, var_decay);
//printf("%" PRIu64" restarts, var_decay = %f\n", starts, var_decay);
break;
default:
assert(false);
......
glueminisat/utils/Options.h
View file @ 7d9365c7
......@@ -282,15 +282,15 @@ class Int64Option : public Option
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
fprintf(stderr, "%4"PRIi64, range.begin);
fprintf(stderr, "%4" PRIi64, range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
fprintf(stderr, "%4"PRIi64, range.end);
fprintf(stderr, "%4" PRIi64, range.end);
fprintf(stderr, "] (default: %"PRIi64")\n", value);
fprintf(stderr, "] (default: %" PRIi64")\n", value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
......
glueminisat/utils/Stat.cc
View file @ 7d9365c7
......@@ -14,15 +14,15 @@ void GlueMiniSat::printStats(Solver& s)
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
// modified by nabesima
//printf("restarts : %"PRIu64"\n", solver.starts);
//printf("restarts : %" PRIu64"\n", solver.starts);
// added by nabesima
printf("variables : %-12d (init %d, after simp %d)\n", s.nFreeVars(), s.init_vars, s.simp_vars);
printf("clauses : %-12d (init %d, after simp %d)\n", s.nClauses(), s.init_clauses, s.simp_clauses);
printf("restarts : %-12"PRIu64" (%.2f /sec, %.2f confs/res, min %"PRIu64" confs, max %"PRIu64" confs, same %"PRIu64")\n", s.starts, s.starts / cpu_time, (double)s.conflicts / s.starts, s.min_confs, s.max_confs, s.same_restarts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s.conflicts, s.conflicts / cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random, %.0f /sec, %4.2f %% deleted)\n", s.decisions, (float)s.rnd_decisions*100 / (float)s.decisions, s.decisions / cpu_time, (double)s.removed_decisions*100 / (s.decisions + s.removed_decisions));
printf("propagations : %-12"PRIu64" (%.0f /sec, %4.2f %% deleted)\n", s.propagations, s.propagations/cpu_time, (double)s.removed_propagations*100 / (s.propagations + s.removed_propagations));
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s.tot_literals, (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
printf("restarts : %-12" PRIu64" (%.2f /sec, %.2f confs/res, min %" PRIu64" confs, max %" PRIu64" confs, same %" PRIu64")\n", s.starts, s.starts / cpu_time, (double)s.conflicts / s.starts, s.min_confs, s.max_confs, s.same_restarts);
printf("conflicts : %-12" PRIu64" (%.0f /sec)\n", s.conflicts, s.conflicts / cpu_time);
printf("decisions : %-12" PRIu64" (%4.2f %% random, %.0f /sec, %4.2f %% deleted)\n", s.decisions, (float)s.rnd_decisions*100 / (float)s.decisions, s.decisions / cpu_time, (double)s.removed_decisions*100 / (s.decisions + s.removed_decisions));
printf("propagations : %-12" PRIu64" (%.0f /sec, %4.2f %% deleted)\n", s.propagations, s.propagations/cpu_time, (double)s.removed_propagations*100 / (s.propagations + s.removed_propagations));
printf("conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", s.tot_literals, (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
// added by nabesima
printf("glue clauses : %-12d (%4.2f %%)\n", s.glue_clauses, (double)s.glue_clauses * 100 / s.conflicts);
printf("avg lbd / avg len : %4.2f / %4.2f\n", (double)s.tot_lbds / s.conflicts, (double)s.tot_literals / s.conflicts);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment