Commit e90e8da8 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Destruct 243

parent 6c796347
......@@ -43,7 +43,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC fast_exp_imperative.5" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.72" steps="64"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="1.07" steps="66"/></proof>
</goal>
<goal name="VC fast_exp_imperative.6" expl="postcondition" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.00" steps="6"/></proof>
......
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.4.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -208,9 +209,9 @@
<goal name="VC tortoise_and_hare.10.0" expl="assertion" proved="true">
<transf name="replace" proved="true" arg1="n" arg2="(k*lambda)">
<goal name="VC tortoise_and_hare.10.0.0" expl="assertion" proved="true">
<transf name="instantiate" proved="true" arg1="H10" arg2="(j+n),j">
<transf name="instantiate" proved="true" arg1="H9" arg2="(j+n),j">
<goal name="VC tortoise_and_hare.10.0.0.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.12"/></proof>
<proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
......@@ -267,7 +268,7 @@
<goal name="VC tortoise_and_hare.19.1.1.0.1.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="((k-1) * lambda &gt;= 0)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="7"><result status="valid" time="9.59"/></proof>
<proof prover="7"><result status="valid" time="1.91"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(i1 &gt;= lambda)">
......@@ -284,7 +285,7 @@
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(lambda &lt; i1)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.80" steps="276"/></proof>
<proof prover="2"><result status="valid" time="0.80" steps="271"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.1" expl="asserted formula" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
......@@ -399,7 +400,7 @@
<goal name="VC tortoise_and_hare.26.0.1.0" expl="true case (assertion)" proved="true">
<transf name="assert" proved="true" arg1="(n = lambda \/ n = 2*lambda)">
<goal name="VC tortoise_and_hare.26.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="36"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
<goal name="VC tortoise_and_hare.26.0.1.0.1" expl="true case (assertion)" proved="true">
<proof prover="6"><result status="valid" time="0.06"/></proof>
......
......@@ -134,7 +134,7 @@ type is_destructed =
| Param of Decl.decl
| Goal_term of term
(* [destruct_term ~original_decl ~decl_name t]: This destroys a headterm and
(* [destruct_term ~decl_name t]: This destroys a headterm and
generate an appropriate lists of goals/declarations that can be used by
decl_goal_l.
......@@ -144,7 +144,6 @@ type is_destructed =
which are eventually converted to disjoint tasks.
*)
let destruct_term ~recursive (t: term) =
let original_decl = t in
(* Standard way to know that a lsymbol is a constructor TODO ? *)
let is_constructor l =
l.ls_constr <> 0
......@@ -192,11 +191,10 @@ let destruct_term ~recursive (t: term) =
(try
let part_t = t_subst_single x tx te in
let new_t = t_quant_close Texists tl tr part_t in
(* TODO remove original_decl here ? *)
(* The recursive call is done after new symbols are introduced so we
readd the new decls to every generated list. *)
let l_t = destruct_term_exception new_t in
List.map (fun x -> Axiom_term original_decl :: Param x_decl :: x) l_t
List.map (fun x -> Param x_decl :: x) l_t
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("destruct_exists", ty1, ty2)))
......@@ -248,7 +246,6 @@ let destruct ~recursive pr : Task.task tlist =
decl_goal_l (fun d ->
match d.d_node with
| Dprop (Paxiom, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
(* TODO solve the problem of original_decl not being a decl anymore ??? *)
let decl_list = destruct_term ~recursive ht in
List.map (fun l -> List.map (fun x ->
match x with
......
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