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

3 files changed, 20 insertions, 20 deletions

diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp
index 29635ec5..ed8f1761 100644
--- a/stp/AST/ToSAT.cpp
+++ b/stp/AST/ToSAT.cpp
@@ -121,15 +121,16 @@ namespace BEEV {
       return;
     double  cpu_time = MINISAT::cpuTime();
     MINISAT::int64   mem_used = MINISAT::memUsed();
-    reportf("restarts              : %"I64_fmt"\n", s.starts);
-    reportf("conflicts             : %-12"I64_fmt"   (%.0f /sec)\n", s.conflicts   , s.conflicts   /cpu_time);
-    reportf("decisions             : %-12"I64_fmt"   (%.0f /sec)\n", s.decisions   , s.decisions   /cpu_time);
-    reportf("propagations          : %-12"I64_fmt"   (%.0f /sec)\n", s.propagations, s.propagations/cpu_time);
-    reportf("conflict literals     : %-12"I64_fmt"   (%4.2f %% deleted)\n", 
-	    s.tot_literals, 
-	    (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
-    if (mem_used != 0) reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
-    reportf("CPU time              : %g s\n", cpu_time);
+    printf("restarts              : %"I64_fmt"\n", s.starts);
+    printf("conflicts             : %-12"I64_fmt"   (%.0f /sec)\n", s.conflicts   , s.conflicts   /cpu_time);
+    printf("decisions             : %-12"I64_fmt"   (%.0f /sec)\n", s.decisions   , s.decisions   /cpu_time);
+    printf("propagations          : %-12"I64_fmt"   (%.0f /sec)\n", s.propagations, s.propagations/cpu_time);
+    printf("conflict literals     : %-12"I64_fmt"   (%4.2f %% deleted)\n", 
+           s.tot_literals, 
+           (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
+    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
+    printf("CPU time              : %g s\n", cpu_time);
+    fflush(stdout);
   }
   
   // Prints Satisfying assignment directly, for debugging.
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<Lit>& 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:
diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h
index 8826fac7..0a6dc87e 100644
--- a/stp/sat/Solver.h
+++ b/stp/sat/Solver.h
@@ -24,9 +24,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "VarOrder.h"
 
 namespace MINISAT {
-// Redfine if you want output to go somewhere else:
-#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) )
-
 
 //=================================================================================================
 // Solver -- the main class: