[llvm-commits] CVS: llvm-test/MultiSource/Benchmarks/minisat/long.cnf.gz short.cnf.gz Main.cpp Makefile

[Owen Anderson]

Changes in directory llvm-test/MultiSource/Benchmarks/minisat:

long.cnf.gz added (r1.1)
short.cnf.gz added (r1.1)
Main.cpp updated: 1.1 -> 1.2
Makefile updated: 1.1 -> 1.2
---
Log message:

Reenable some hacked out output from minisat to better indentify failures.
Also, gzip the input files to save some bandwidth.

NOTE: This currently fails the JIT which can't load zlib symbols for it.



---
Diffs of the changes:  (+21 -11)

 Main.cpp     |   29 +++++++++++++++++++----------
 Makefile     |    3 ++-
 long.cnf.gz  |    0 
 short.cnf.gz |    0 
 4 files changed, 21 insertions(+), 11 deletions(-)


Index: llvm-test/MultiSource/Benchmarks/minisat/long.cnf.gz


Index: llvm-test/MultiSource/Benchmarks/minisat/short.cnf.gz


Index: llvm-test/MultiSource/Benchmarks/minisat/Main.cpp
diff -u llvm-test/MultiSource/Benchmarks/minisat/Main.cpp:1.1 llvm-test/MultiSource/Benchmarks/minisat/Main.cpp:1.2
--- llvm-test/MultiSource/Benchmarks/minisat/Main.cpp:1.1	Thu Feb  8 02:25:16 2007
+++ llvm-test/MultiSource/Benchmarks/minisat/Main.cpp	Thu Feb  8 02:40:59 2007
@@ -23,6 +23,7 @@
 #include <errno.h>
 
 #include <signal.h>
+#include <zlib.h>
 
 #include "Solver.h"
 
@@ -83,7 +84,7 @@
 #define CHUNK_LIMIT 1048576
 
 class StreamBuffer {
-    FILE*  in;
+    gzFile  in;
     char    buf[CHUNK_LIMIT];
     int     pos;
     int     size;
@@ -91,10 +92,10 @@
     void assureLookahead() {
         if (pos >= size) {
             pos  = 0;
-            size = fread(buf, 1, sizeof(buf), in); } }
+            size = gzread(in, buf, sizeof(buf)); } }
 
 public:
-    StreamBuffer(FILE* i) : in(i), pos(0), size(0) {
+    StreamBuffer(gzFile i) : in(i), pos(0), size(0) {
         assureLookahead(); }
 
     int  operator *  () { return (pos >= size) ? EOF : buf[pos]; }
@@ -161,6 +162,8 @@
             if (match(in, "p cnf")){
                 int vars    = parseInt(in);
                 int clauses = parseInt(in);
+                reportf("|  Number of variables:  %-12d                                         |\n", vars);
+                reportf("|  Number of clauses:    %-12d                                         |\n", clauses);
             }else{
                 reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
             }
@@ -174,7 +177,7 @@
 
 // Inserts problem into solver.
 //
-static void parse_DIMACS(FILE* input_stream, Solver& S) {
+static void parse_DIMACS(gzFile input_stream, Solver& S) {
     StreamBuffer in(input_stream);
     parse_DIMACS_main(in, S); }
 
@@ -187,12 +190,11 @@
     double   cpu_time = cpuTime();
     uint64_t mem_used = memUsed();
     reportf("restarts              : %lld\n", solver.starts);
-    reportf("conflicts             : %-12lld   (%.0f /sec)\n", solver.conflicts   , solver.conflicts   /cpu_time);
-    reportf("decisions             : %-12lld   (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions   /cpu_time);
-    reportf("propagations          : %-12lld   (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+    reportf("conflicts             : %-12lld\n", solver.conflicts);
+    reportf("decisions             : %-12lld   (%4.2f %% random)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions);
+    reportf("propagations          : %-12lld\n", solver.propagations);
     reportf("conflict literals     : %-12lld   (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
     if (mem_used != 0) reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
-    reportf("CPU time              : %g s\n", cpu_time);
 }
 
 Solver* solver;
@@ -283,6 +285,7 @@
     argc = j;
 
 
+    reportf("This is MiniSat 2.0 beta\n");
 #if defined(__linux__)
     fpu_control_t oldcw, newcw;
     _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
@@ -297,11 +300,15 @@
     if (argc == 1)
         reportf("Reading from standard input... Use '-h' or '--help' for help.\n");
 
-    FILE* in = fopen(argv[1], "rb");
+    gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
     if (in == NULL)
         reportf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
 
-    parse_DIMACS(in, S);;
+    reportf("============================[ Problem Statistics ]=============================\n");
+    reportf("|                                                                             |\n");
+
+    parse_DIMACS(in, S);
+    gzclose(in);
     FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
 
     if (!S.simplify()){
@@ -312,6 +319,8 @@
     }
 
     bool ret = S.solve();
+    printStats(S);
+    reportf("\n");
     printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n");
     if (res != NULL){
         if (ret){


Index: llvm-test/MultiSource/Benchmarks/minisat/Makefile
diff -u llvm-test/MultiSource/Benchmarks/minisat/Makefile:1.1 llvm-test/MultiSource/Benchmarks/minisat/Makefile:1.2
--- llvm-test/MultiSource/Benchmarks/minisat/Makefile:1.1	Thu Feb  8 02:25:16 2007
+++ llvm-test/MultiSource/Benchmarks/minisat/Makefile	Thu Feb  8 02:40:59 2007
@@ -3,6 +3,7 @@
 LEVEL = ../../..
 PROG = minisat
 CPPFLAGS = -D NDEBUG -Imtl
-RUN_OPTIONS = long.cnf
+LDFLAGS = -lz
+RUN_OPTIONS = -verbosity=0 long.cnf.gz
 
 include ../../Makefile.multisrc