Commit 723ee788 authored by MARCHE Claude's avatar MARCHE Claude

method play_all to session for benchmarking

parent 23fc7bee
......@@ -514,6 +514,33 @@ let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
~obsolete_only ~context_unproved_goals_only)
tr.transf_goals
(***********************************)
(* play all *)
(***********************************)
let rec play_on_goal_and_children eS eT ~timelimit l g =
List.iter
(fun p -> prover_on_goal eS eT ~timelimit p g)
l;
PHstr.iter
(fun _ t ->
List.iter
(play_on_goal_and_children eS eT ~timelimit l)
t.transf_goals)
g.goal_transformations
let play_all eS eT ~timelimit l =
PHstr.iter
(fun _ file ->
List.iter
(fun th ->
List.iter
(play_on_goal_and_children eS eT ~timelimit l)
th.theory_goals)
file.file_theories)
eS.session.session_files
(***********************************)
(* method: mark proofs as obsolete *)
(***********************************)
......
......@@ -191,6 +191,13 @@ module Make(O: OBSERVER) : sig
already 'valid'
*)
val play_all :
O.key env_session -> t -> timelimit:int -> Whyconf.prover list -> unit
(** [play_all es sched l] runs every prover of list [l] on all
goals and sub-goals of the session, with the given time limit.
Useful for benchmarking provers
*)
val cancel : O.key any -> unit
(** [cancel a] marks all proofs under [a] as obsolete *)
......
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