Commit 5cf1554d authored by MARCHE Claude's avatar MARCHE Claude

update example residuals using new transformation induction_arg_pr

parent 4756c1cd
......@@ -7,173 +7,197 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../residual.mlw" expanded="true">
<theory name="Residuals" sum="e0e851172bdfa7d0dd256f092fc4fd98" expanded="true">
<goal name="WP_parameter accepts_epsilon" expl="VC for accepts_epsilon">
<transf name="split_goal_wp">
<goal name="WP_parameter accepts_epsilon.1" expl="postcondition">
<file name="../residual.mlw" proved="true">
<theory name="Residuals" proved="true" sum="751887864908ee3d56cf65a325b5bea0">
<goal name="WP_parameter accepts_epsilon" expl="VC for accepts_epsilon" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter accepts_epsilon.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.2" expl="postcondition">
<goal name="WP_parameter accepts_epsilon.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.3" expl="postcondition">
<goal name="WP_parameter accepts_epsilon.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.4" expl="variant decrease">
<goal name="WP_parameter accepts_epsilon.3" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.5" expl="postcondition">
<goal name="WP_parameter accepts_epsilon.4" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.6" expl="variant decrease">
<goal name="WP_parameter accepts_epsilon.5" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="53"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.7" expl="postcondition">
<goal name="WP_parameter accepts_epsilon.6" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.8" expl="variant decrease">
<goal name="WP_parameter accepts_epsilon.7" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.9" expl="variant decrease">
<goal name="WP_parameter accepts_epsilon.8" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="53"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.10" expl="postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter accepts_epsilon.10.1" expl="VC for accepts_epsilon">
<goal name="WP_parameter accepts_epsilon.9" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter accepts_epsilon.9.0" expl="VC for accepts_epsilon" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.10.2" expl="VC for accepts_epsilon">
<goal name="WP_parameter accepts_epsilon.9.1" expl="VC for accepts_epsilon" proved="true">
<proof prover="0" timelimit="60" memlimit="4000"><result status="valid" time="6.18" steps="10891"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter accepts_epsilon.11" expl="postcondition">
<goal name="WP_parameter accepts_epsilon.10" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="336"/></proof>
</goal>
<goal name="WP_parameter accepts_epsilon.12" expl="postcondition">
<goal name="WP_parameter accepts_epsilon.11" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</transf>
</goal>
<goal name="inversion_mem_star_gen" expl="">
<goal name="inversion_mem_star_gen" proved="true">
<proof prover="3" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.28"/></proof>
<transf name="induction_pr">
<goal name="inversion_mem_star_gen.1" expl="">
<transf name="induction_arg_pr" proved="true" arg1="H2">
<goal name="inversion_mem_star_gen.0" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.1" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.2" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.3" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.4" proved="true">
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inversion_mem_star_gen.5" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.6" proved="true">
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
<transf name="induction_pr" proved="true" >
<goal name="inversion_mem_star_gen.0" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="inversion_mem_star_gen.2" expl="">
<goal name="inversion_mem_star_gen.1" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="inversion_mem_star_gen.3" expl="">
<goal name="inversion_mem_star_gen.2" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="inversion_mem_star_gen.4" expl="">
<goal name="inversion_mem_star_gen.3" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="inversion_mem_star_gen.5" expl="">
<goal name="inversion_mem_star_gen.4" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="inversion_mem_star_gen.6" expl="">
<goal name="inversion_mem_star_gen.5" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="inversion_mem_star_gen.7" expl="">
<goal name="inversion_mem_star_gen.6" proved="true">
<proof prover="6"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
<goal name="inversion_mem_star" expl="">
<goal name="inversion_mem_star" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter residual" expl="VC for residual" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter residual.1" expl="postcondition">
<goal name="WP_parameter residual" expl="VC for residual" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter residual.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="89"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter residual.2" expl="postcondition">
<goal name="WP_parameter residual.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="91"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter residual.3" expl="postcondition">
<goal name="WP_parameter residual.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="535"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter residual.4" expl="variant decrease">
<goal name="WP_parameter residual.3" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="51"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.32"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.5" expl="variant decrease">
<goal name="WP_parameter residual.4" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="52"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter residual.6" expl="postcondition">
<goal name="WP_parameter residual.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="133"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter residual.7" expl="variant decrease">
<goal name="WP_parameter residual.6" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="53"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.8" expl="variant decrease">
<goal name="WP_parameter residual.7" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="54"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter residual.9" expl="postcondition">
<goal name="WP_parameter residual.8" expl="postcondition" proved="true">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="WP_parameter residual.10" expl="variant decrease">
<goal name="WP_parameter residual.9" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.11" expl="postcondition" expanded="true">
<goal name="WP_parameter residual.10" expl="postcondition" proved="true">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter residual.12" expl="variant decrease">
<goal name="WP_parameter residual.11" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="52"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.78"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.13" expl="postcondition" expanded="true">
<goal name="WP_parameter residual.12" expl="postcondition" proved="true">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.34"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter decide_mem" expl="VC for decide_mem">
<transf name="split_goal_wp">
<goal name="WP_parameter decide_mem.1" expl="postcondition">
<goal name="WP_parameter decide_mem" expl="VC for decide_mem" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter decide_mem.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter decide_mem.2" expl="variant decrease">
<goal name="WP_parameter decide_mem.1" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter decide_mem.3" expl="postcondition">
<goal name="WP_parameter decide_mem.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Test" sum="b1a665b01fa289fa209c670a5754de10">
<goal name="WP_parameter test_astar" expl="VC for test_astar">
<transf name="split_goal_wp">
<theory name="Test" proved="true" sum="b1a665b01fa289fa209c670a5754de10">
<goal name="WP_parameter test_astar" expl="VC for test_astar" proved="true">
<transf name="split_goal_wp" proved="true" >
</transf>
</goal>
</theory>
<theory name="DFA" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="DFA" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
......@@ -213,7 +213,6 @@ let induction_l label induct kn t =
let (ctx, (ls, argl, cl), goal) = locate kn label t in
let fold vsi p t = if p then vsi else t_freevars vsi t in
let vsi = List.fold_left2 fold Mvs.empty (parameters ls cl) argl in
(*let vsi = t_vars (t_app_infer ls argl) in*)
let cindep, cdep = partition ctx vsi in
let goal = zip cdep goal in
List.map (fun (_,c) ->
......
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