Added minimal utility for getting bench stats

Makefile

@@ -5,7 +5,7 @@ COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display
 FLAGS=
 DIRS=-Is sat,smt,util,util/smtlib
 DOC=msat.docdir/index.html
-TEST=sat_solve.native
+TEST=sat_solve.native bench_stats.native
 
 NAME=msat
 
@@ -28,6 +28,9 @@ $(TEST): $(LIB)
 bench: $(TEST)
 	cd bench && $(MAKE)
 
+stats:
+	./bench_stats.native `git rev-parse HEAD`
+
 log:
 	cat _build/$(LOG) || true
 

_tags

@@ -1,3 +1,5 @@
+<util/*.cmx>: package(unix)
+<util/*.native>: package(unix)
 <smt/*.cmx>: for-pack(Msat), package(zarith)
 <sat/*.cmx>: for-pack(Msat)
 

sat/solver.ml

@@ -698,9 +698,7 @@ module Make (F : Formula_intf.S)
     let nbv = St.nb_vars () in
     let nbc = env.nb_init_clauses + List.length cnf in
     Iheap.grow_to_by_double env.order nbv;
-    (*
+    (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
-    List.iter (List.iter (fun a -> insert_var_order a.var)) cnf;
-    *)
     St.iter_vars insert_var_order;
     Vec.grow_to_by_double env.model nbv;
     Vec.grow_to_by_double env.clauses nbc;

util/bench_stats.ml

@@ -0,0 +1,86 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+exception Commit_not_found
+exception Commit_ambiguous
+
+let get_commit s =
+    let d = Filename.concat (Filename.dirname Sys.argv.(0)) "bench" in
+    match Parselog.complete (Filename.concat d "logs") s with
+    | [c] -> Filename.basename c, Parselog.parse_commit c
+    | [] -> raise Commit_not_found
+    | _ -> raise Commit_ambiguous
+
+type commit_stats = {
+    nb_sat : int;
+    nb_unsat : int;
+    nb_timeout : int;
+    nb_spaceout : int;
+    avg_time : float
+}
+
+let get_stats h =
+    let avg = ref 0. in
+    let sat = ref 0 in
+    let unsat = ref 0 in
+    let timeout = ref 0 in
+    let spaceout = ref 0 in
+    let nb_success () =
+        float (!sat + !unsat)
+    in
+    let update_avg t =
+        let n = nb_success () in
+        avg := (!avg *. n +. t) /. (n +. 1.)
+    in
+    let aux f pb = Parselog.(
+        match pb.pb_st with
+        | Sat ->
+                update_avg pb.pb_time;
+                incr sat
+        | Unsat ->
+                update_avg pb.pb_time;
+                incr unsat
+        | Timeout ->
+                incr timeout
+        | Spaceout ->
+                incr spaceout
+    ) in
+    Hashtbl.iter aux h;
+    {
+        nb_sat = !sat;
+        nb_unsat = !unsat;
+        nb_timeout = !timeout;
+        nb_spaceout = !spaceout;
+        avg_time = !avg;
+    }
+
+let print_stats s =
+    let sha, h = get_commit s in
+    let st = get_stats h in
+    Format.printf "Average time : %f (%d / %d)@\nTimeouts : %d@\nSpaceouts : %d@."
+    st.avg_time (st.nb_sat + st.nb_unsat)
+    (st.nb_sat + st.nb_unsat + st.nb_timeout + st.nb_spaceout) st.nb_timeout st.nb_spaceout
+
+let print_diff _ _ = ()
+
+let main () =
+    if Array.length Sys.argv = 2 then
+        print_stats Sys.argv.(1)
+    else if Array.length Sys.argv = 3 then
+        print_diff Sys.argv.(1) Sys.argv.(2)
+    else
+        Format.fprintf Format.std_formatter "Don't know what to do !@."
+;;
+
+try
+    main ()
+with
+| Commit_not_found ->
+        Format.printf "No such commit found@.";
+        exit 2
+| Commit_ambiguous ->
+        Format.printf "Too many commits fit this prefix@.";
+        exit 2

util/parselog.ml

@@ -0,0 +1,93 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(* Misc directory/files manipulation *)
+let list_dir s =
+    let d = Unix.opendir s in
+    let l = ref [] in
+    try
+        while true do
+            l := (Filename.concat s (Unix.readdir d)) :: !l
+        done;
+        assert false
+    with End_of_file ->
+        !l
+
+let list_dir_files_rec s =
+    let rec aux acc = function
+        | [] -> acc
+        | f :: r ->
+                let f' = Filename.basename f in
+                if f' = Filename.current_dir_name || f' = Filename.parent_dir_name then
+                    aux acc r
+                else begin match Unix.((stat f).st_kind) with
+                | Unix.S_REG -> aux (f :: acc) r
+                | Unix.S_DIR -> aux acc (List.rev_append (list_dir f) r)
+                | _ -> aux acc r
+                end
+    in
+    aux [] [s]
+
+(* Commit sha completion *)
+let complete root sha =
+    let l = list_dir root in
+    let aux s = try String.sub s 0 (String.length sha) with Invalid_argument _ -> "" in
+    let test s = sha = aux (Filename.basename s) in
+    List.filter test l
+
+let commit_info sha =
+    let cmd = "git show "^ sha in
+    let ch = Unix.open_process_in cmd in
+    let l = (input_line ch :: input_line ch :: input_line ch :: input_line ch :: input_line ch :: input_line ch :: []) in
+    ignore (Unix.close_process_in ch);
+    String.concat "\n" (List.rev l)
+
+(* Raw log file parsing *)
+exception Empty_raw of string
+exception Unknown_status of string list
+
+type status =
+    | Sat
+    | Unsat
+    | Timeout
+    | Spaceout
+
+type pb = {
+    pb_name : string;
+    pb_st : status;
+    pb_time : float;
+}
+
+let status_of_lines = function
+    | ["Sat"] -> Sat
+    | ["Unsat"] -> Unsat
+    | ["Time limit exceeded"; _] -> Timeout
+    | ["Size limit exceeded"; _] -> Spaceout
+    | l -> raise (Unknown_status l)
+
+let parse_raw f =
+    let f_in = open_in f in
+    let f_lines = ref [] in
+    begin try
+        while true do
+            f_lines := input_line f_in :: !f_lines
+        done;
+        assert false
+    with End_of_file ->
+        close_in f_in;
+    end;
+    match !f_lines with
+    | [] -> raise (Empty_raw f)
+    | s :: r ->
+            let st = status_of_lines (List.rev r) in
+            { pb_name = f; pb_st = st; pb_time = float_of_string s }
+
+let parse_commit root =
+    let l = list_dir_files_rec (Filename.concat root "raw") in
+    let res = Hashtbl.create (List.length l) in
+    List.iter (fun f -> Hashtbl.add res f (parse_raw f)) l;
+    res
+

util/parselog.mli

@@ -0,0 +1,17 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+exception Empty_raw of string
+exception Unknown_status of string list
+
+val complete : string -> string -> string list
+val commit_info : string -> string
+
+type status = Sat | Unsat | Timeout | Spaceout
+type pb = { pb_name : string; pb_st : status; pb_time : float; }
+
+val parse_raw : string -> pb
+val parse_commit : string -> (string, pb) Hashtbl.t