From 1efbeceedbb00267f38d0dfc9b24307ad3e1feca Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Mon, 5 Apr 2010 04:01:56 +0000 Subject: STP: Eliminate use of non-standard variadic macro. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100392 91177308-0d34-0410-b5e6-96231b3b80d8 --- stp/sat/Solver.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'stp/sat/Solver.cpp') diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp index 13a9ae08..9761c719 100644 --- a/stp/sat/Solver.cpp +++ b/stp/sat/Solver.cpp @@ -768,24 +768,26 @@ bool Solver::solve(const vec& assumps) assumps.copyTo(assumptions); if (verbosity >= 1){ - reportf("==================================[MINISAT]====================================\n"); - reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); - reportf("===============================================================================\n"); + printf("==================================[MINISAT]====================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); + printf("===============================================================================\n"); } // Search: while (status == l_Undef){ if (verbosity >= 1) - //reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); - reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + //printf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); status = search((int)nof_conflicts, (int)nof_learnts); nof_conflicts *= params.restart_inc; nof_learnts *= params.learntsize_inc; } - if (verbosity >= 1) - reportf("==============================================================================\n"); + if (verbosity >= 1) { + printf("==============================================================================\n"); + fflush(stdout); + } if (status == l_True){ // Copy model: -- cgit 1.4.1