Commit 07638376 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch '266-questions-on-replay-use-steps' into 'master'

Resolve "Questions on `replay --use-steps `"

Closes #266

See merge request !87
parents 8d544dbe 059e39e4
......@@ -3,9 +3,8 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.6.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="11" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
......@@ -13,55 +12,55 @@
<theory name="Square" proved="true">
<goal name="sqr_non_neg" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="sqr_increasing" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sqr_sum" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="Simple" proved="true">
<goal name="VC isqrt" expl="VC for isqrt" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="30"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="101"/></proof>
</goal>
<goal name="VC main" expl="VC for main" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</theory>
<theory name="NewtonMethod" proved="true">
<goal name="VC sqrt" expl="VC for sqrt" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC sqrt.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC sqrt.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
<goal name="VC sqrt.2" expl="check division by zero" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC sqrt.3" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC sqrt.4" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sqrt.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC sqrt.6" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC sqrt.7" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="33"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC sqrt.8" expl="check division by zero" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
<goal name="VC sqrt.9" expl="check division by zero" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
<goal name="VC sqrt.10" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -69,54 +68,54 @@
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sqrt.10.1" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.12" steps="31"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC sqrt.10.2" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.33" steps="72"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="28"/></proof>
</goal>
<goal name="VC sqrt.10.3" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="VC sqrt.10.4" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="28"/></proof>
</goal>
<goal name="VC sqrt.10.5" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="28"/></proof>
</goal>
<goal name="VC sqrt.10.6" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="VC sqrt.10.7" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="30"/></proof>
</goal>
<goal name="VC sqrt.10.8" expl="VC for sqrt" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqrt.11" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="24"/></proof>
</goal>
<goal name="VC sqrt.12" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="34"/></proof>
<proof prover="3"><result status="valid" time="0.10" steps="90"/></proof>
</goal>
<goal name="VC sqrt.13" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="26"/></proof>
</goal>
<goal name="VC sqrt.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="15"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="27"/></proof>
</goal>
<goal name="VC sqrt.15" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="28"/></proof>
</goal>
<goal name="VC sqrt.16" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="17"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="29"/></proof>
</goal>
<goal name="VC sqrt.17" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="VC sqrt.18" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="58"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
......
......@@ -34,6 +34,7 @@ val file_of_theory : driver -> string -> Theory.theory -> string
(** [file_of_theory d f th] produces a filename
for the prover of driver [d], for a theory [th] from filename [f] *)
(* unused outside ?
val call_on_buffer :
command : string ->
limit : Call_provers.resource_limit ->
......@@ -42,7 +43,7 @@ val call_on_buffer :
filename : string ->
printer_mapping : Printer.printer_mapping ->
driver -> Buffer.t -> Call_provers.prover_call
*)
val print_task :
?old : in_channel ->
......
......@@ -1125,16 +1125,16 @@ let replay ~valid_only ~obsolete_only ?(use_steps=false) ?(filter=fun _ -> true)
begin
let parid = pa.parent in
let pr = pa.prover in
(* TODO: if pr is not installed, lookup for a replacement policy
OR: delegate this work to the replay_proof_attempt function *)
(* If use_steps, we give only steps as a limit
TODO: steps should not be used if prover was replaced above *)
let limit =
(* If use_steps, we give only steps as a limit *)
let step_limit = Call_provers.(empty_limit.limit_steps) in
let step_limit =
if use_steps then
Call_provers.{empty_limit with limit_steps = pa.limit.limit_steps}
else
Call_provers.{ pa.limit with limit_steps = empty_limit.limit_steps }
match pa.proof_state with
| None -> step_limit
| Some r -> r.Call_provers.pr_steps
else step_limit
in
let limit = Call_provers.{pa.limit with limit_steps = step_limit } in
replay_proof_attempt c pr limit parid id
~callback:(fun id s ->
craft_report s parid limit pa;
......
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