Commit 14a1e9e2 authored by MARCHE Claude's avatar MARCHE Claude

heuristic for time limit of proof replay

the time limit for the replay is the max of the time limit
given initially and twice the time taken by the prover
(if the result was "valid")

E.g, if Alt-Ergo said valid in 4.9 seconds, for an initial limit of 5,
then the replay will give 10 seconds
parent 10c3f14f
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="explicit_subst/why3session.xml">
name="examples/explicit_subst/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......
......@@ -388,7 +388,6 @@ module M = Session.Make
goals_model#set ~row:iter ~column:index_column (-1);
goals_model#get_row_reference (goals_model#get_path iter)
let remove row =
let (_:bool) = goals_model#remove row#iter in ()
......@@ -426,7 +425,7 @@ let set_proof_state ~obsolete a =
(image_of_result ~obsolete res);
let t = match res with
| Session.Done { Call_provers.pr_time = time } ->
Format.sprintf "%.2f" time
Format.sprintf "%.2f [%d.0]" time a.M.timelimit
| Session.Unedited -> "not yet edited"
| _ -> ""
in
......
......@@ -218,31 +218,6 @@ let init =
(* eprintf "Item '%s' loaded@." name *)
()
(*
let string_of_result result =
match result with
| Session.Undone -> "undone"
| Session.Scheduled -> "scheduled"
| Session.Running -> "running"
| Session.InternalFailure _ -> "internal failure"
| Session.Done r -> match r.Call_provers.pr_answer with
| Call_provers.Valid -> "valid"
| Call_provers.Invalid -> "invalid"
| Call_provers.Timeout -> "timeout"
| Call_provers.Unknown _ -> "unknown"
| Call_provers.Failure _ -> "failure"
| Call_provers.HighFailure -> "high failure"
let print_result fmt res =
let t = match res with
| Session.Done { Call_provers.pr_time = time } ->
Format.sprintf "(%.1f)" time
| _ -> ""
in
fprintf fmt "%s%s" (string_of_result res) t
*)
let print_result fmt
{Call_provers.pr_answer=ans; Call_provers.pr_output=out;
Call_provers.pr_time=t} =
......
......@@ -1652,7 +1652,15 @@ let rec replay_on_goal_or_children
(fun _ a ->
if not obsolete_only || a.proof_obsolete then
if not context_unproved_goals_only || proof_successful a
then redo_external_proof ~timelimit:a.timelimit g a)
then
let timelimit =
match a.proof_state with
| Done { Call_provers.pr_answer = Call_provers.Valid;
Call_provers.pr_time = t }
-> max a.timelimit (truncate (ceil (t *. 2.0)))
| _ -> a.timelimit
in
redo_external_proof ~timelimit g a)
g.external_proofs;
Hashtbl.iter
(fun _ t ->
......
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