Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 02536d53 authored by François Bobot's avatar François Bobot
Browse files

why3stats : go under the transformations

parent a7e2329b
No related branches found
No related tags found
No related merge requests found
...@@ -126,10 +126,9 @@ let update_perf_stats stats prover_and_time = ...@@ -126,10 +126,9 @@ let update_perf_stats stats prover_and_time =
update_avg_time stats.prover_avg_time prover_and_time; update_avg_time stats.prover_avg_time prover_and_time;
update_count stats.prover_num_proofs prover_and_time update_count stats.prover_num_proofs prover_and_time
let stats_of_goal file theory stats goal = let rec stats_of_goal prefix_name stats goal =
let ext_proofs = goal.external_proofs in let ext_proofs = goal.external_proofs in
let proof_id = file.file_name ^ " / " ^ theory.theory_name let proof_id = prefix_name ^ goal.goal_name in
^ " / " ^ goal.goal_name in
let proof_list = let proof_list =
Mstr.fold Mstr.fold
(fun prover proof_attempt acc -> (fun prover proof_attempt acc ->
...@@ -145,19 +144,27 @@ let stats_of_goal file theory stats goal = ...@@ -145,19 +144,27 @@ let stats_of_goal file theory stats goal =
| _ -> acc) | _ -> acc)
ext_proofs ext_proofs
[] in [] in
match proof_list with let no_transf = Mstr.is_empty goal.transformations in
| [] -> begin match proof_list with
| [] when no_transf ->
stats.no_proof <- Sstr.add proof_id stats.no_proof stats.no_proof <- Sstr.add proof_id stats.no_proof
| [ (prover, time) ] -> | [ (prover, time) ] when no_transf ->
stats.only_one_proof <- stats.only_one_proof <-
Sstr.add (proof_id ^ " : " ^ prover) stats.only_one_proof; Sstr.add (proof_id ^ " : " ^ prover) stats.only_one_proof;
update_perf_stats stats (prover, time) update_perf_stats stats (prover, time)
| _ :: _ -> | _ ->
List.iter (update_perf_stats stats) proof_list List.iter (update_perf_stats stats) proof_list end;
Mstr.iter (stats_of_transf prefix_name stats) goal.transformations
and stats_of_transf prefix_name stats _ transf =
let prefix_name = prefix_name ^ transf.transf_name ^ " / " in
List.iter (stats_of_goal prefix_name stats) transf.subgoals
let stats_of_theory file stats theory = let stats_of_theory file stats theory =
let goals = theory.goals in let goals = theory.goals in
List.iter (stats_of_goal file theory stats) goals let prefix_name = file.file_name ^ " / " ^ theory.theory_name
^ " / " in
List.iter (stats_of_goal prefix_name stats) goals
let stats_of_file stats file = let stats_of_file stats file =
let theories = file.theories in let theories = file.theories in
...@@ -172,10 +179,9 @@ let fill_prover_data stats = ...@@ -172,10 +179,9 @@ let fill_prover_data stats =
provers provers
let extract_stats_from_file stats fname = let extract_stats_from_file stats fname =
let env = read_config ~includes:!includes None in
let project_dir = get_project_dir fname in let project_dir = get_project_dir fname in
try try
let file_list = read_project_dir ~allow_obsolete:true ~env project_dir in let file_list = read_project_dir ~allow_obsolete ~env project_dir in
fill_prover_data stats; fill_prover_data stats;
List.iter (stats_of_file stats) file_list List.iter (stats_of_file stats) file_list
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment