Commit 1f448ffb authored by MARCHE Claude's avatar MARCHE Claude

resurrected option -P of why3replay

parent b4c37450
......@@ -954,7 +954,7 @@ let replay_print fmt (lr: (proofNodeID * Whyconf.prover * Call_provers.resource_
in
Format.fprintf fmt "%a@." (Pp.print_list Pp.newline pp_elem) lr
let replay ~valid_only ~obsolete_only ?(use_steps=false)
let replay ~valid_only ~obsolete_only ?(use_steps=false) ?(filter=fun _ -> true)
c ~callback ~notification ~final_callback ~any =
let craft_report count s r id pr limits pa =
......@@ -978,11 +978,12 @@ let replay ~valid_only ~obsolete_only ?(use_steps=false)
in
let need_replay pa =
(pa.proof_obsolete || not obsolete_only) &&
(not valid_only ||
match pa.Session_itp.proof_state with
| None -> false
| Some pr -> Call_provers.(pr.pr_answer = Valid))
filter pa &&
(pa.proof_obsolete || not obsolete_only) &&
(not valid_only ||
match pa.Session_itp.proof_state with
| None -> false
| Some pr -> Call_provers.(pr.pr_answer = Valid))
in
let session = c.controller_session in
......
......@@ -299,6 +299,7 @@ val replay:
valid_only:bool ->
obsolete_only:bool ->
?use_steps:bool ->
?filter:(proof_attempt_node -> bool) ->
controller ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
notification:notifier ->
......@@ -319,11 +320,14 @@ val replay:
When finished, call the callback [final_callback] with the report,
a list of 4-uples [(goalID, prover, limits, report)]
When obsolete_only is set, only obsolete proofs are replayed (default)
When [obsolete_only] is set, only obsolete proofs are replayed (default)
When use_steps is set, replay use the recorded number of proof
When [use_steps] is set, replay use the recorded number of proof
steps (not set by default)
When [filter] is set, only the proof attempts on which the filter
returns true are replayed
*)
......
......@@ -247,19 +247,16 @@ let add_to_check_no_smoke some_merge_miss found_obs cont =
C.register_observer update_monitor;
if !opt_provers = [] then
let () =
C.replay ~valid_only:false ~obsolete_only:false ~use_steps:!opt_use_steps
C.replay ~valid_only:false ~obsolete_only:!opt_obsolete_only ~use_steps:!opt_use_steps
~callback ~notification ~final_callback cont ~any:None
in ()
else
failwith "option -P not yet supported"
(*
let filter a =
List.exists
(fun p -> Whyconf.filter_prover p a.Session.proof_prover)
(fun p -> Whyconf.filter_prover p a.Session_itp.prover)
!opt_provers in
M.check_all ~release:true ~use_steps:!opt_use_steps
~filter ~callback env_session sched
*)
C.replay ~valid_only:false ~obsolete_only:!opt_obsolete_only ~use_steps:!opt_use_steps
~filter ~callback ~notification ~final_callback cont ~any:None
(*
......
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