Commit 48dce311 authored by François Bobot's avatar François Bobot

rc file working add timelimit

parent 22cfca3f
......@@ -455,7 +455,7 @@ endif
# BENCH
###############
BENCH_FILES = bench whybench benchrc
BENCH_FILES = bench benchrc whybench
BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
......
[tools fast]
prover = "alt-ergo"
prover = "cvc3"
timelimit = 5
[tools tptp]
prover = "spass"
[probs funny]
file = "talk290.mlw"
transform = "split_goal"
[bench fast_and_funny]
tools = fast
probs = funny
\ No newline at end of file
......@@ -75,10 +75,12 @@ struct
c = Condition.create ();
nb_task = 0}
let test s = s.nb_task = 0
let start s = Mutex.lock s.m; s.nb_task <- s.nb_task + 1; Mutex.unlock s.m
let stop s = Mutex.lock s.m; s.nb_task <- s.nb_task - 1;
if s.nb_task = 0 then Condition.signal s.c; Mutex.unlock s.m
let wait s = Mutex.lock s.m; Condition.wait s.c s.m
if test s then Condition.signal s.c; Mutex.unlock s.m
let wait s = Mutex.lock s.m;
if not (test s) then Condition.wait s.c s.m
let lock s = Mutex.lock s.m
let unlock s = Mutex.unlock s.m
end
......@@ -124,7 +126,8 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
MTask.unlock s
| _ -> () in
call s cb tool prob);
MTask.wait s
MTask.wait s;
MTask.unlock s
let any ?callback toolprob =
let l = ref [] in
......@@ -147,3 +150,114 @@ let all_array ?callback tools probs =
Array.iteri (fun i t -> Array.iteri (fun j p -> f (i,j) t p) probs) tools)
(fun (i,j) r -> m.(i).(j) <- r::m.(i).(j));
m
let all_list_tools ?callback tools probs =
let tools = List.map (fun t -> (t, ref [])) tools in
general ?callback (fun f ->
List.iter (fun (t,l) -> List.iter (fun p -> f l t p) probs) tools)
(fun l r -> l:=r::!l);
List.map (fun (t,l) -> (t.tval,!l)) tools
type output =
(** on stdout *)
|Average
|Timeline
(** In a file *)
|Csv
type ('a,'b) bench =
{
btools : 'a tool list;
bprobs : 'b prob list;
boutputs : output list;
}
let run_bench ?callback bench =
all_list ?callback bench.btools bench.bprobs
let run_benchs ?callback benchs =
let benchs = List.map (fun b -> (b,ref [])) benchs in
general ?callback (fun f ->
List.iter (fun (b,l) ->
List.iter (fun t -> List.iter (fun p -> f l t p) b.bprobs)
b.btools) benchs)
(fun l r -> l:=r::!l);
List.map (fun (b,l) -> (b,!l)) benchs
let run_benchs_tools ?callback benchs =
let benchs = List.map (fun b ->
b, List.map (fun t -> t,ref []) b.btools) benchs in
general ?callback (fun f ->
List.iter (fun (b,l) ->
List.iter (fun (t,l) -> List.iter (fun p -> f l t p) b.bprobs)
l) benchs)
(fun l r -> l:=r::!l);
List.map (fun (b,l) -> b,List.map (fun (t,l) -> t.tval,!l) l) benchs
(** average *)
(** valid * timeout * unknown * invalid *)
type nb_avg = int * float
let add_nb_avg (nb,avg) time =
(succ nb, ((float nb) *. avg +. time) /. (float (succ nb)))
let empty_nb_avg = (0,0.)
let print_nb_avg fmt (nb,avg) = Format.fprintf fmt "%i : %.2f" nb avg
type tool_res =
{ valid : nb_avg;
timeout : nb_avg;
unknown : nb_avg;
invalid : nb_avg;
failure : nb_avg}
let empty_tool_res =
{ valid = empty_nb_avg;
timeout = empty_nb_avg;
unknown = empty_nb_avg;
invalid = empty_nb_avg;
failure = empty_nb_avg;
}
let print_tool_res fmt tool_res =
Format.fprintf fmt "(%a, %a, %a, %a, %a)"
print_nb_avg tool_res.valid
print_nb_avg tool_res.unknown
print_nb_avg tool_res.timeout
print_nb_avg tool_res.invalid
print_nb_avg tool_res.failure
let compute_average l =
let fold tr res =
let r = res.result in
match r.pr_answer with
| Valid -> {tr with valid = add_nb_avg tr.valid r.pr_time}
| Timeout -> {tr with timeout = add_nb_avg tr.timeout r.pr_time}
| Invalid -> {tr with invalid = add_nb_avg tr.invalid r.pr_time}
| Unknown _ -> {tr with unknown = add_nb_avg tr.unknown r.pr_time}
| Failure _ | HighFailure ->
{tr with failure = add_nb_avg tr.failure r.pr_time} in
List.fold_left fold empty_tool_res l
let filter_timeline l =
let l = List.filter (fun r -> r.result.pr_answer = Valid) l in
let compare_valid x y =
let c = compare x.result.pr_time y.result.pr_time in
if c <> 0 then c else compare x y in
let l = List.fast_sort compare_valid l in
l
let compute_timeline min max step =
let rec aux acc cur next = function
| _ when next > max -> List.rev acc
| [] -> aux (cur::acc) cur (next+.step) []
| {result={pr_time = t}}::_ as l when t >= next ->
aux (cur::acc) cur (next+.step) l
| _::l -> aux acc (cur+1) next l in
aux [] 0 min
let max_time l =
List.fold_left (fun acc {result={pr_time = t}} -> max acc t) 0. l
......@@ -64,3 +64,56 @@ val all_array :
val any :
?callback:('a,'b) callback ->
('a tool * 'b prob) list -> ('a,'b) result list
val all_list_tools :
?callback:('a,'b) callback ->
'a tool list -> 'b prob list -> ('a * ('a,'b) result list) list
type output =
(** on stdout *)
|Average
|Timeline
(** In a file *)
|Csv
type ('a,'b) bench =
{
btools : 'a tool list;
bprobs : 'b prob list;
boutputs : output list;
}
val run_bench :
?callback:('a,'b) callback -> ('a,'b) bench -> ('a,'b) result list
val run_benchs :
?callback:('a,'b) callback -> ('a,'b) bench list ->
(('a,'b) bench * ('a,'b) result list) list
val run_benchs_tools :
?callback:('a,'b) callback -> ('a,'b) bench list ->
(('a,'b) bench * ('a * ('a,'b) result list) list) list
type nb_avg = int * float
val print_nb_avg : Format.formatter -> nb_avg -> unit
type tool_res =
{ valid : nb_avg;
timeout : nb_avg;
unknown : nb_avg;
invalid : nb_avg;
failure : nb_avg}
val print_tool_res : Format.formatter -> tool_res -> unit
val compute_average : ('a,'b) result list -> tool_res
val compute_timeline :
float -> float -> float -> ('a,'b) result list -> int list
val filter_timeline : ('a,'b) result list -> ('a,'b) result list
val max_time : ('a,'b) result list -> float
......@@ -23,31 +23,25 @@ open Why
open Util
open Theory
type output =
(** on stdout *)
|Average
|Timeline
(** In a file *)
|Csv
type bench =
{
(* tool_name, prover_name *)
btools : (string * string) tool list;
(* prob_name, file_name, theory name *)
bprobs : (string * string * string) prob list;
boutputs : output list;
}
type id_tool = (string * string)
type id_prob = (string * string * string)
type benchrc = { tools : (string * string) tool list Mstr.t;
probs : (string * string * string) prob Mstr.t;
benchs : bench Mstr.t;
type benchrc = { tools : id_tool tool list Mstr.t;
probs : id_prob prob Mstr.t;
benchs : (id_tool,id_prob) bench Mstr.t
}
open Whyconf
open Rc
let read_tools wc map (name,section) =
let absolute_filename dirname f =
if Filename.is_relative f then
Filename.concat dirname f
else
f
let read_tools absf wc map (name,section) =
(* loadpath *)
let wc_main = get_main wc in
let loadpath = get_stringl ~default:[] section "loadpath" in
......@@ -84,7 +78,7 @@ let read_tools wc map (name,section) =
try
let driver = get_string section "driver" in
let command = get_string section "command" in
("driver",driver,command) :: provers
("driver",absf driver,command) :: provers
with MissingField _ -> provers in
let load_driver (n,d,c) = n,Driver.load_driver env d,c in
let provers = List.map load_driver provers in
......@@ -100,7 +94,7 @@ let read_tools wc map (name,section) =
} in
Mstr.add name (List.map create_tool provers) map
let read_probs map (name,section) =
let read_probs absf map (name,section) =
(* transformations *)
let transforms = get_stringl ~default:[] section "transform" in
let gen_trans env =
......@@ -117,50 +111,57 @@ let read_probs map (name,section) =
let files = get_stringl ~default:[] section "file" in
let gen env task =
let fwhy () =
let read_one fname =
let cin = open_in fname in
let m = Env.read_channel ?format:format env fname cin in
close_in cin;
let ths = Mnm.bindings m in
List.rev_map (fun (n,th) -> ((name,fname,n),th)) ths
in
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 [] in
try
let read_one fname =
let cin = open_in (absf fname) in
let m = Env.read_channel ?format:format env fname cin in
close_in cin;
let ths = Mnm.bindings m in
List.rev_map (fun (n,th) -> ((name,fname,n),th)) ths
in
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 []
with exn -> eprintf "%a@." Exn_printer.exn_printer exn; exit 1
in
Scheduler.do_why_sync fwhy () in
Mstr.add name { ptask = gen; ptrans = gen_trans} map
let read_bench mtools mprobs map (name,section) =
let tools = get_stringl section "tools" in
let lookup s =
try Mstr.find s mtools with Not_found -> eprintf "Undefined tools %s@." s;
try Mstr.find s mtools
with Not_found -> eprintf "Undefined tools %s@." s;
exit 1 in
let tools = list_flatten_rev (List.map lookup tools) in
let probs = get_stringl section "probs" in
let lookup s =
try Mstr.find s mprobs with Not_found -> eprintf "Undefined probs %s@." s;
try Mstr.find s mprobs
with Not_found -> eprintf "Undefined probs %s@." s;
exit 1 in
let probs = List.map lookup probs in
let outputs = get_stringl ~default:[] section "probs" in
let outputs = get_stringl ~default:[] section "outputs" in
let check = function
| "average" -> Average
| "timeline" -> Timeline
| "csv" -> Csv
| s -> eprintf "Unknown output %s" s; exit 1 in
| s -> eprintf "Unknown output %s@." s; exit 1 in
let outputs = List.map check outputs in
Mstr.add name { btools = tools; bprobs = probs; boutputs = outputs} map
let read_file wc f =
let rc = from_file f in
let absf = absolute_filename (Filename.dirname f) in
let tools = get_family rc "tools" in
let tools = List.fold_left (read_tools wc) Mstr.empty tools in
let tools = List.fold_left (read_tools absf wc) Mstr.empty tools in
let probs = get_family rc "probs" in
let probs = List.fold_left read_probs Mstr.empty probs in
let probs = List.fold_left (read_probs absf) Mstr.empty probs in
let benchs = get_family rc "bench" in
let benchs = List.fold_left (read_bench tools probs) Mstr.empty benchs in
let benchs = List.fold_left (read_bench tools probs)
Mstr.empty benchs in
{tools = tools;
probs = probs;
benchs = benchs}
......@@ -43,26 +43,16 @@ open Bench
open Why
open Util
type output =
(** on stdout *)
|Average
|Timeline
(** In a file *)
|Csv
type bench =
{
(* tool_name, prover_name *)
btools : (string * string) tool list;
(* prob_name, file_name, theory name *)
bprobs : (string * string * string) prob list;
boutputs : output list;
}
type benchrc = { tools : (string * string) tool list Mstr.t;
probs : (string * string * string) prob Mstr.t;
benchs : bench Mstr.t
type id_tool = (string * string)
(* tool_name, prover_name *)
type id_prob = (string * string * string)
(* prob_name, file_name, theory name *)
type benchrc = { tools : id_tool tool list Mstr.t;
probs : id_prob prob Mstr.t;
benchs : (id_tool,id_prob) bench Mstr.t
}
val read_file : Whyconf.config -> string -> benchrc
......@@ -97,6 +97,7 @@ let opt_output = ref None
let opt_timelimit = ref None
let opt_memlimit = ref None
let opt_task = ref None
let opt_benchrc = ref []
let opt_print_theory = ref false
let opt_print_namespace = ref false
......@@ -131,7 +132,9 @@ let option_list = Arg.align [
"-I", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L (obsolete)";
"-P", Arg.String (fun s -> opt_prover := s::!opt_prover),
"Add <prover> in the bench";
"<prover> Add <prover> in the bench";
"-B", Arg.String (fun s -> opt_benchrc := s::!opt_benchrc),
"<bench> Read one bench configuration file from <bench>";
"--prover", Arg.String (fun s -> opt_prover := s::!opt_prover),
" same as -P";
"-F", Arg.String (fun s -> opt_parser := Some s),
......@@ -181,6 +184,7 @@ let option_list = Arg.align [
let tools = ref []
let probs = ref []
let benchs = ref []
let () =
try
......@@ -261,11 +265,6 @@ let () =
end;
if !opt_list then exit 0;
if Queue.is_empty opt_queue then begin
Arg.usage option_list usage_msg;
exit 1
end;
(* Someting else using rc file intead of driver will be added later *)
(* if !opt_prover <> None && !opt_driver <> None then begin *)
(* eprintf "Options '-P'/'--prover' and \ *)
......@@ -273,9 +272,12 @@ let () =
(* exit 1 *)
(* end; *)
if !opt_prover = [] then begin
eprintf "At least one prover is required.@.";
exit 1 end;
if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue) then
begin
eprintf "At least one bench is required or one prover and one file.@.";
Arg.usage option_list usage_msg;
exit 1
end;
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
......@@ -291,7 +293,7 @@ let () =
let prover = try Mstr.find s (get_provers config) with
| Not_found -> eprintf "Prover %s not found.@." s; exit 1
in
{ B.tval = s;
{ B.tval = "cmdline",s;
ttrans = Trans.identity;
tdriver = load_driver env prover.driver;
tcommand = prover.command;
......@@ -309,7 +311,6 @@ let () =
in
List.fold_left lookup Trans.identity_l !opt_trans in
let fold_prob acc = function
| None, _ -> acc
| Some f, _ ->
......@@ -325,7 +326,7 @@ let () =
let th = Mnm.bindings m in
let map (name,th) = name,Task.split_theory th None task in
let fold acc (n,l) =
List.rev_append (List.map (fun v -> (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
(* let gen = Env.Wenv.memoize 3 (fun env -> *)
(* let memo = Trans.store (fun task -> gen env task) in *)
......@@ -334,83 +335,66 @@ let () =
{ B.ptask = gen;
ptrans = fun _ -> transl;
}::acc in
probs := Queue.fold fold_prob [] opt_queue
probs := Queue.fold fold_prob [] opt_queue;
benchs := List.map (Benchrc.read_file config) !opt_benchrc
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(** valid * timeout * unknown * invalid *)
type nb_avg = int * float
let add_nb_avg (nb,avg) time =
(succ nb, ((float nb) *. avg +. time) /. (float (succ nb)))
let empty_nb_avg = (0,0.)
let print_nb_avg fmt (nb,avg) = fprintf fmt "%i : %.2f" nb avg
type tool_res =
{ valid : nb_avg;
timeout : nb_avg;
unknown : nb_avg;
invalid : nb_avg;
failure : nb_avg}
let empty_tool_res =
{ valid = empty_nb_avg;
timeout = empty_nb_avg;
unknown = empty_nb_avg;
invalid = empty_nb_avg;
failure = empty_nb_avg;
}
let count_result =
let m = Mnm.empty in
let fold m res =
let tr = Mnm.find_default res.B.tool empty_tool_res m in
let r = res.B.result in
let tr = match r.C.pr_answer with
| C.Valid -> {tr with valid = add_nb_avg tr.valid r.C.pr_time}
| C.Timeout -> {tr with timeout = add_nb_avg tr.timeout r.C.pr_time}
| C.Invalid -> {tr with invalid = add_nb_avg tr.invalid r.C.pr_time}
| C.Unknown _ -> {tr with unknown = add_nb_avg tr.unknown r.C.pr_time}
| C.Failure _ | C.HighFailure ->
{tr with failure = add_nb_avg tr.failure r.C.pr_time} in
Mnm.add res.B.tool tr m in
List.fold_left fold m
let () = Scheduler.async := (fun f v -> ignore (Thread.create f v))
let print_result l =
let tool_res = List.map (fun (t,l) -> t,B.compute_average l) l in
let print_tool_res ((_,tool_name),tool_res) =
printf "%a - %s@." B.print_tool_res tool_res tool_name in
printf "(v,t,u,f,i) - valid, unknown, timeout, invalid, failure@.";
List.iter print_tool_res tool_res
let print_timeline l =
let l = List.map (fun (t,l) -> t,B.filter_timeline l) l in
let max = List.fold_left (fun acc (_,l) -> max acc (B.max_time l)) 0. l in
let step = max/.10. in
let tl = List.map (fun (t,l) -> t,B.compute_timeline 0. max step l) l in
let print_timeline ((_,tool_name),timeline) =
printf "@[%a - %s@]@."
(Pp.print_list Pp.comma (fun fmt -> fprintf fmt "%.3i"))
timeline tool_name in
printf "@[%a@]@."
(Pp.print_iter1 (fun f -> iterf f 0. max)
Pp.comma (fun fmt -> fprintf fmt "%.3f"))
step;
List.iter print_timeline tl
let () =
let m = Mutex.create () in
let callback tool prob task i res =
let callback (_,tool) (_,_,prob) task i res =
Mutex.lock m;
printf "%s %a %i with %s : %a@."
prob Pretty.print_pr (task_goal task) i tool
Scheduler.print_pas res;
Mutex.unlock m
in
let l = B.all_list ~callback !tools !probs in
(* let print_result fmt res = *)
(* fprintf fmt "%s %a %i with %s : %a@." *)
(* res.B.prob Pretty.print_pr *)
(* (task_goal res.B.task) res.B.idtask res.B.tool *)
(* C.print_prover_result res.B.result in *)
(* eprintf "Done :@.%a@." *)
(* (Pp.print_list Pp.newline print_result) l *)
let tool_res = count_result l in
let print_tool_res tool_name tool_res =
printf "(%a, %a, %a, %a, %a) - %s@."
print_nb_avg tool_res.valid
print_nb_avg tool_res.unknown
print_nb_avg tool_res.timeout
print_nb_avg tool_res.invalid
print_nb_avg tool_res.failure
tool_name in
printf "(v,t,u,f,i) - valid, unknown, timeout, invalid, failure@.";
Mnm.iter print_tool_res tool_res
let l = B.all_list_tools ~callback !tools !probs in
print_result l;
let callback (_,tool) (_,file,prob) task i res =
Mutex.lock m;
printf "%s.%s %a %i with %s : %a@."
file prob Pretty.print_pr (task_goal task) i tool
Scheduler.print_pas res;
Mutex.unlock m
in
let benchs =
List.map (fun b -> List.map snd (Mstr.bindings b.Benchrc.benchs))
!benchs in
let bl = B.run_benchs_tools ~callback (list_flatten_rev benchs) in
List.iter (fun (_,l) -> print_result l) bl;
List.iter (fun (_,l) -> print_timeline l) bl
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/whybench.byte"
compile-command: "unset LANG; make -j -C ../.. bin/whybench.byte"
End:
*)
......@@ -1001,7 +1001,6 @@ let redo_external_proof q g a =
in
Db.set_status a.Model.proof_db db_res time
in
GtkThread.sync (callback Model.Scheduled 0.0) "";
let old = if a.Model.edited_as = "" then None else
begin
eprintf "Info: proving using edited file %s@." a.Model.edited_as;
......
......@@ -183,7 +183,6 @@ let event_handler () =
!scheduled_proofs !maximum_running_proofs;
Mutex.unlock queue_lock;
(* build the prover task from goal in [a] *)
!async (fun () -> callback Scheduled) ();
try
let call_prover : unit -> unit -> Call_provers.prover_result =
(*
......@@ -255,6 +254,7 @@ let (_scheduler_thread : Thread.t) =
let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
~command ~driver ~callback
goal =
!async (fun () -> callback Scheduled) ();
Mutex.lock queue_lock;
Queue.push (debug,timelimit,memlimit,old,command,driver,callback,goal)