bench : in one bench one file at a time

src/bench/bench.ml

@@ -39,7 +39,7 @@ type 'a tool = {
 }
 
 type 'a prob = {
-  ptask  : env -> task -> ('a * task) list; (** needed for tenv *)
+  ptask  : (env -> task -> ('a * task) list) list; (** needed for tenv *)
   ptrans : env -> task list trans;
 }
 
@@ -99,19 +99,18 @@ let call s callback tool prob =
       (Trans.singleton tool.ttrans) in
     MainWorker.add_work MainWorker.level2 s
       (fun () ->
+        MainWorker.stop_work MainWorker.level2 s;
         MainWorker.start_work MainWorker.level3 s;
         apply_transformation_l ~callback:(trans_cb pval) trans task) in
   (** Split *)
-  MainWorker.start_work MainWorker.level1 s;
-  MainWorker.add_work MainWorker.level1 s
-    (fun () ->
-      MainWorker.start_work MainWorker.level2 s;
-      let cb ths =
-        List.iter iter_task ths;
-        MainWorker.stop_work MainWorker.level2 s;
-        MainWorker.stop_work MainWorker.level1 s in
-      do_why ~callback:cb (prob.ptask tool.tenv) tool.tuse
-    )
+  List.iter (fun create_task ->
+    MainWorker.start_work MainWorker.level1 s;
+    MainWorker.add_work MainWorker.level1 s
+      (fun () ->
+        let cb ths = List.iter iter_task ths;
+          MainWorker.stop_work MainWorker.level1 s in
+        do_why ~callback:cb (create_task tool.tenv) tool.tuse
+      )) prob.ptask
 
 let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
   Debug.dprintf debug "Start one general@.";
@@ -139,7 +138,8 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
     MainWorker.stop_work MainWorker.level1 t;
   ) () in
   (** Treat the work done and wait *)
-  MainWorker.treat ~maxlevel2:(!Scheduler.maximum_running_proofs * 3)
+  MainWorker.treat
+    ~maxlevel2:(!Scheduler.maximum_running_proofs * 3)
     ~maxlevel3:(!Scheduler.maximum_running_proofs * 3)
     t (fun () f -> f ()) ()
 

src/bench/bench.mli

@@ -39,7 +39,8 @@ type 'a tool = {
 }
 
 type 'a prob = {
-  ptask  : env -> task -> ('a * task) list; (** needed for tenv and tuse *)
+  ptask  : (env -> task -> ('a * task) list) list;
+  (** needed for tenv and tuse *)
   ptrans : env -> task list trans; (** perhaps should be merged in
                                        ptask *)
 }

src/bench/benchrc.ml

@@ -110,7 +110,7 @@ let read_probs absf map (name,section) =
   let format = get_stringo section "format" in
   (* files *)
   let files = get_stringl ~default:[] section "file" in
-  let gen env task =
+  let gen fname env task =
     try
       let read_one fname =
         let cin = open_in (absf fname) in
@@ -122,11 +122,10 @@ let read_probs absf map (name,section) =
       let map (name,th) = name,Task.split_theory th None task in
       let fold acc (n,l) =
         List.rev_append (List.rev_map (fun v -> (n,v)) l) acc in
-      files |> List.map read_one |> list_flatten_rev
-               |> List.rev_map map |> List.fold_left fold []
+      read_one fname |> List.rev_map map |> List.fold_left fold []
     with exn -> eprintf "%a@." Exn_printer.exn_printer exn; exit 1
   in
-  Mstr.add name { ptask   = gen; ptrans   = gen_trans} map
+  Mstr.add name { ptask   = List.map gen files; ptrans   = gen_trans} map
 
 let read_bench absf mtools mprobs map (name,section) =
   let tools = get_stringl section "tools" in

src/bench/whybench.ml

@@ -345,7 +345,7 @@ let () =
         let fold acc (n,l) =
           List.rev_append (List.map (fun v -> (("cmdline","",n),v)) l) acc in
         th |> List.map map |> List.fold_left fold [] in
-      { B.ptask   = gen;
+      { B.ptask   = [gen];
         ptrans   = fun _ -> transl;
       }::acc in
   Debug.dprintf debug "Load problems@.";