Commit 354803d2 authored by François Bobot's avatar François Bobot

- Try to not keep foolishly a task and so all is transform.

- treat all the prover for one gone, and not anymore conversely
parent d51f735c
...@@ -50,7 +50,7 @@ type why_result = ...@@ -50,7 +50,7 @@ type why_result =
type ('a,'b) result = {tool : 'a; type ('a,'b) result = {tool : 'a;
prob : 'b; prob : 'b;
task : task; task : Decl.prsymbol;
idtask : int; idtask : int;
result : why_result} result : why_result}
...@@ -104,7 +104,8 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add = ...@@ -104,7 +104,8 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
callback tool.tval pval task i res; callback tool.tval pval task i res;
match res with match res with
| Scheduler.InternalFailure _ | Scheduler.Done _ -> | Scheduler.InternalFailure _ | Scheduler.Done _ ->
add v {tool = tool.tval; prob = pval; task = task; add v {tool = tool.tval; prob = pval;
task = Task.task_goal task;
idtask = i; idtask = i;
result = match res with result = match res with
| Scheduler.InternalFailure exn -> InternalFailure exn | Scheduler.InternalFailure exn -> InternalFailure exn
...@@ -125,13 +126,20 @@ let any ?callback toolprob = ...@@ -125,13 +126,20 @@ let any ?callback toolprob =
!l !l
let all_list ?callback tools probs = let all_list_tp ?callback tools probs =
let l = ref [] in let l = ref [] in
general ?callback (fun f -> general ?callback (fun f ->
List.iter (fun t -> List.iter (fun p -> f () t p) probs) tools) List.iter (fun t -> List.iter (fun p -> f () t p) probs) tools)
(fun () r -> l:=r::!l); (fun () r -> l:=r::!l);
!l !l
let all_list_pt ?callback tools probs =
let l = ref [] in
general ?callback (fun f ->
List.iter (fun p -> List.iter (fun t -> f () t p) tools) probs)
(fun () r -> l:=r::!l);
!l
let all_array ?callback tools probs = let all_array ?callback tools probs =
let m = Array.make_matrix (Array.length tools) (Array.length probs) let m = Array.make_matrix (Array.length tools) (Array.length probs)
[] in [] in
...@@ -164,7 +172,7 @@ type ('a,'b) bench = ...@@ -164,7 +172,7 @@ type ('a,'b) bench =
} }
let run_bench ?callback bench = let run_bench ?callback bench =
all_list ?callback bench.btools bench.bprobs all_list_pt ?callback bench.btools bench.bprobs
let run_benchs ?callback benchs = let run_benchs ?callback benchs =
let benchs = List.map (fun b -> (b,ref [])) benchs in let benchs = List.map (fun b -> (b,ref [])) benchs in
...@@ -180,12 +188,13 @@ let run_benchs_tools ?callback benchs = ...@@ -180,12 +188,13 @@ let run_benchs_tools ?callback benchs =
b, List.map (fun t -> t,ref []) b.btools) benchs in b, List.map (fun t -> t,ref []) b.btools) benchs in
general ?callback (fun f -> general ?callback (fun f ->
List.iter (fun (b,l) -> List.iter (fun (b,l) ->
List.iter (fun (t,l) -> List.iter (fun p -> f l t p) b.bprobs) List.iter (fun p -> List.iter (fun (t,l) -> f l t p) l)
l) benchs) b.bprobs) benchs)
(fun l r -> l:=r::!l); (fun l r -> l:=r::!l);
List.map (fun (b,l) -> b,List.map (fun (t,l) -> t.tval,!l) l) benchs List.map (fun (b,l) -> b,List.map (fun (t,l) -> t.tval,!l) l) benchs
(** average *) (** average *)
(** valid * timeout * unknown * invalid *) (** valid * timeout * unknown * invalid *)
...@@ -294,7 +303,7 @@ answer output time ...@@ -294,7 +303,7 @@ answer output time
let cmp x y = let cmp x y =
let c = cmp x.prob y.prob in let c = cmp x.prob y.prob in
if c <> 0 then c else if c <> 0 then c else
let id x = (Task.task_goal x.task).Decl.pr_name.Ident.id_string in let id x = x.task.Decl.pr_name.Ident.id_string in
let c = String.compare (id x) (id y) in let c = String.compare (id x) (id y) in
if c <> 0 then c else compare x.idtask y.idtask in if c <> 0 then c else compare x.idtask y.idtask in
let l = List.map (fun (p,l) -> p,List.fast_sort cmp l) l in let l = List.map (fun (p,l) -> p,List.fast_sort cmp l) l in
...@@ -315,7 +324,7 @@ in ...@@ -315,7 +324,7 @@ in
(* No printer for task since we want the same name evenif its (* No printer for task since we want the same name evenif its
the same file with different environnement (loaded two times) *) the same file with different environnement (loaded two times) *)
fprintf fmt "%a|%s|%i ," print_prob b fprintf fmt "%a|%s|%i ," print_prob b
(Task.task_goal t).Decl.pr_name.Ident.id_string t.Decl.pr_name.Ident.id_string
id; id;
Pp.print_list Pp.comma print_cell fmt l in Pp.print_list Pp.comma print_cell fmt l in
Pp.print_list print_newline print_line fmt l Pp.print_list print_newline print_line fmt l
......
...@@ -50,13 +50,17 @@ type why_result = ...@@ -50,13 +50,17 @@ type why_result =
type ('a,'b) result = {tool : 'a; type ('a,'b) result = {tool : 'a;
prob : 'b; prob : 'b;
task : task; task : Decl.prsymbol;
idtask : int; idtask : int;
result : why_result} result : why_result}
type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit
val all_list : val all_list_tp :
?callback:('a,'b) callback ->
'a tool list -> 'b prob list -> ('a,'b) result list
val all_list_pt :
?callback:('a,'b) callback -> ?callback:('a,'b) callback ->
'a tool list -> 'b prob list -> ('a,'b) result list 'a tool list -> 'b prob list -> ('a,'b) result list
......
...@@ -345,9 +345,6 @@ let () = ...@@ -345,9 +345,6 @@ let () =
let fold acc (n,l) = let fold acc (n,l) =
List.rev_append (List.map (fun v -> (("cmdline","",n),v)) l) acc in List.rev_append (List.map (fun v -> (("cmdline","",n),v)) l) acc in
th |> List.map map |> List.fold_left fold [] in th |> List.map map |> List.fold_left fold [] in
let gen = Env.Wenv.memoize 3 (fun env ->
let memo = Trans.store (fun task -> gen env task) in
Trans.apply memo) in
{ B.ptask = gen; { B.ptask = gen;
ptrans = fun _ -> transl; ptrans = fun _ -> transl;
}::acc in }::acc in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment