Commit ae9ef936 authored by MARCHE Claude's avatar MARCHE Claude

fix missing cases in shape computation

parent e549f00f
......@@ -153,7 +153,7 @@ lemma many_steps_seq_rec:
many_steps s1 i1 s2 Sskip /\ many_steps s2 i2 s3 Sskip
lemma many_steps_seq:
forall s1 s3:state, i1 i2:stmt [many_steps s1 (Sseq i1 i2) s3 Sskip].
forall s1 s3:state, i1 i2:stmt.
many_steps s1 (Sseq i1 i2) s3 Sskip ->
exists s2:state.
many_steps s1 i1 s2 Sskip /\ many_steps s2 i2 s3 Sskip
......
......@@ -10,6 +10,10 @@
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="coq-realize"
name="Coq Realize"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
......@@ -56,7 +60,7 @@
expanded="true">
<goal
name="ident_eq_dec"
sum="657a0cf836398f0e71a03149e8d3f752"
sum="ca7c4648761db026ea93d61666f0b79a"
proved="true"
expanded="false"
shape="ainfix =V0V1NOainfix =V0V1F">
......@@ -72,7 +76,7 @@
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
......@@ -84,7 +88,7 @@
</goal>
<goal
name="check_skip"
sum="7a80eb56e935bc1dae5a16b66655b71a"
sum="a28ed21b2b531fe3e8a3933e02f27497"
proved="true"
expanded="false"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
......@@ -93,19 +97,19 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Test13"
sum="752a2c5d7bd2066e4a0ea6f8202ff247"
sum="bc53c41524b84304eb79b4e36fef8af8"
proved="true"
expanded="false"
shape="Laconstc0ainfix =aeval_exprV0aEconstc13c13">
......@@ -121,7 +125,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="eprover"
......@@ -135,19 +139,19 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="Test42"
sum="3c9c1d72a759712365d998f7a29886de"
sum="78671d09729d8ffd84136c2dcf7eb74b"
proved="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEvarV0c42">
......@@ -163,7 +167,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="eprover"
......@@ -189,7 +193,7 @@
</goal>
<goal
name="Test55"
sum="ff32d38bb9935b5125f45e8793463171"
sum="9f1ffc89f69ccb03e44edbf6adfebb8d"
proved="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55">
......@@ -210,7 +214,7 @@
</goal>
<goal
name="Ass42"
sum="dcf28f4f2eb16812656ba92851bc662a"
sum="456c846b124e10fccdeb72291a3819b0"
proved="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipF">
......@@ -231,7 +235,7 @@
</goal>
<goal
name="If42"
sum="c31c3a15e03ada451dfc85fff902ad2b"
sum="9c97951c8cf8d86219396907bf0260eb"
proved="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4F">
......@@ -240,19 +244,19 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.47"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.86"/>
<result status="valid" time="0.84"/>
</proof>
</goal>
<goal
name="progress"
sum="de162538bff3e343afe673c48cceac7c"
sum="3e029691d2ae6f6e5afe69a1860de120"
proved="true"
expanded="false"
shape="aone_stepV0V1V2V3EIainfix =V1aSskipNF">
......@@ -261,12 +265,12 @@
timelimit="5"
edited="imp_Imp_progress_1.v"
obsolete="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.68"/>
</proof>
</goal>
<goal
name="many_steps_seq_rec"
sum="d65712d0e695898d17b619c58dfaddc5"
sum="11055dd7c0d1df4d3beead62e71fb0d0"
proved="true"
expanded="false"
shape="amany_stepsV6V5V1aSskipAamany_stepsV0V4V6aSskipEIainfix =V2aSseqV4V5FIainfix =V3aSskipIamany_stepsV0V2V1V3F">
......@@ -275,12 +279,12 @@
timelimit="3"
edited="imp_Imp_many_steps_seq_rec_1.v"
obsolete="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
name="many_steps_seq"
sum="98667096725002aa995a17db1a8945b8"
sum="dd8b486013219116b304a7fa85098017"
proved="true"
expanded="false"
shape="amany_stepsV4V3V1aSskipAamany_stepsV0V2V4aSskipEIamany_stepsV0aSseqV2V3V1aSskipF">
......@@ -296,19 +300,19 @@
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="eval_subst_expr"
sum="43a7f007490895fc85d1a5055de98919"
sum="977774231aa576a9290e4f9016c04ed0"
proved="true"
expanded="false"
shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
......@@ -317,12 +321,12 @@
timelimit="5"
edited="imp_Imp_eval_subst_expr_1.v"
obsolete="false">
<result status="valid" time="0.45"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal
name="eval_subst"
sum="41c9426526820307330065d8ac78c17c"
sum="a104713723b4fa4f3517a9438902ec80"
proved="true"
expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F">
......@@ -331,12 +335,12 @@
timelimit="5"
edited="imp_Imp_eval_subst_2.v"
obsolete="false">
<result status="valid" time="0.53"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="skip_rule"
sum="dfcd50b4105bd2ae7cd329453fdbc909"
sum="e7044c767994d31b5b88e917bfff9ac0"
proved="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
......@@ -345,12 +349,12 @@
timelimit="3"
edited="imp_Imp_skip_rule_1.v"
obsolete="false">
<result status="valid" time="0.67"/>
<result status="valid" time="0.60"/>
</proof>
</goal>
<goal
name="assign_rule"
sum="d492b0a1117c6083520f1a99f602c05b"
sum="0ec8e9f1b70042827e8a4110996d5ce6"
proved="true"
expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
......@@ -359,12 +363,12 @@
timelimit="5"
edited="imp_Imp_assign_rule_1.v"
obsolete="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="seq_rule"
sum="a5e519277ce236964d153818a92437e6"
sum="b0875f2e4e3ff470e938fb16ff79cd67"
proved="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
......@@ -373,7 +377,7 @@
timelimit="3"
edited="imp_Imp_seq_rule_2.v"
obsolete="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.61"/>
</proof>
<proof
prover="z3"
......@@ -385,7 +389,7 @@
</goal>
<goal
name="if_rule"
sum="72ad5869a02dbc44921cf038f2f2959e"
sum="8e1f396662d807419bc751cf7f6d58b9"
proved="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
......@@ -394,12 +398,12 @@
timelimit="3"
edited="imp_Imp_if_rule_1.v"
obsolete="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal
name="while_rule_rec"
sum="a984a32a61ac3a2a4f6bd3514298ecfe"
sum="094bc644f8c198e43d4d30be08dab9f4"
proved="false"
expanded="true"
shape="aeval_fmlaV4aFandaFnotaFtermV0V1Iaeval_fmlaV3V1Iainfix =V6aSskipIainfix =V5aSwhileV0V2Iamany_stepsV3V5V4V6FIavalid_tripleaFandaFtermV0V1V2V1F">
......@@ -407,36 +411,36 @@
prover="coq"
timelimit="5"
edited="imp_Imp_while_rule_rec_1.v"
obsolete="true"><undone/>
obsolete="true">
<result status="unknown" time="0.59"/>
</proof>
</goal>
<goal
name="while_rule"
sum="681ef1ff491ebf2565e3659f675db3fa"
proved="false"
sum="78107beafe1c5ce0bd6dd9b7a96554f4"
proved="true"
expanded="true"
shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
<proof
prover="cvc3"
timelimit="3"
edited=""
obsolete="true">
<result status="valid" time="0.16"/>
obsolete="false">
<result status="valid" time="0.18"/>
</proof>
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="true">
<result status="valid" time="0.41"/>
obsolete="false">
<result status="valid" time="0.35"/>
</proof>
<proof
prover="z3"
timelimit="3"
edited=""
obsolete="true">
<result status="valid" time="0.05"/>
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
</theory>
......
......@@ -123,13 +123,19 @@ let rec t_shape ~(push:string->'a->'a) c m (acc:'a) t : 'a =
let m = vs_rename_alpha c m u in
t_shape ~push c m (push tag_eps acc) f
| Tquant (q,b) ->
let vl,_,f1 = t_open_quant b in
(* TODO: take triggers into account !! *)
let vl,triggers,f1 = t_open_quant b in
let m = vl_rename_alpha c m vl in
let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
push hq (t_shape ~push c m acc f1)
(* argument first, intentionally, to give more weight on A in
forall x,A *)
(* argument first, intentionally, to give more weight on A in
forall x,A *)
let acc = push hq (t_shape ~push c m acc f1) in
List.fold_right
(fun trigger acc ->
List.fold_right
(fun t acc ->
t_shape ~push c m acc t)
trigger acc)
triggers acc
| Tbinop (o,f,g) ->
let tag = match o with
| Tand -> tag_and
......@@ -159,6 +165,22 @@ let pr_shape_list fmt t =
(* shape of a task *)
let logic_decl_shape ~(push:string->'a->'a) (acc:'a) (ls,d) : 'a =
let acc = push (ls.ls_name.Ident.id_string) acc in
match d with
| None -> acc
| Some def ->
let vl,t = Decl.open_ls_defn def in
let c = ref (-1) in
let m = vl_rename_alpha c Mvs.empty vl in
t_shape ~push c m acc t
let logic_ind_decl_shape ~(push:string->'a->'a) (acc:'a) (ls,cl) : 'a =
let acc = push (ls.ls_name.Ident.id_string) acc in
List.fold_right
(fun (_,t) acc -> t_shape ~push (ref (-1)) Mvs.empty acc t)
cl acc
let propdecl_shape ~(push:string->'a->'a) (acc:'a) (k,n,t) : 'a =
let tag = match k with
| Decl.Plemma -> tag_Plemma
......@@ -172,13 +194,21 @@ let propdecl_shape ~(push:string->'a->'a) (acc:'a) (k,n,t) : 'a =
let decl_shape ~(push:string->'a->'a) (acc:'a) d : 'a =
match d.Decl.d_node with
| Decl.Dtype _tyl -> push tag_Dtype acc
| Decl.Dlogic _ldl -> push tag_Dlogic acc
| Decl.Dind _idl -> push tag_Dind acc
| Decl.Dtype tyl ->
List.fold_right
(fun _ty acc -> acc)
tyl (push tag_Dtype acc)
| Decl.Dlogic ldl ->
List.fold_right
(fun d acc -> logic_decl_shape ~push acc d)
ldl (push tag_Dlogic acc)
| Decl.Dind idl ->
List.fold_right
(fun d acc -> logic_ind_decl_shape ~push acc d)
idl (push tag_Dind acc)
| Decl.Dprop pdecl ->
propdecl_shape ~push (push tag_Dprop acc) pdecl
let tdecl_shape ~(push:string->'a->'a) (acc:'a) t : 'a =
match t.Theory.td_node with
| Theory.Decl d -> decl_shape ~push (push tag_tDecl acc) d
......@@ -193,8 +223,6 @@ let rec task_shape ~(push:string->'a->'a) (acc:'a) t : 'a =
task_shape ~push (tdecl_shape ~push acc t.Task.task_decl)
t.Task.task_prev
(* checksum of a task
it is the MD5 digest of the shape
*)
......@@ -208,191 +236,3 @@ let task_checksum t =
(*
shape = list of string, ordered lexicographically
shape (forall x:t, P) = code(forall) :: shape (P)
shape (P -> Q) = code(->) :: shape(P) @ shape(Q)
shape (App(f,[t1,..,tn] ) =
code(app) :: code(f) @ code (t1) ... @ code (tn)
code(f) = user name (not unique but it is not a problem)
code(Var x) = code(Var) :: code(debruijn x)
code(Const n) = n (en tant que string ?)
*)
(*
code of a shape: maps shapes into real numbers in [0..1], such that
compare t1 t2 = code (shape t1) -. code (shape t2)
is a good comparison operator
code(n:int) = 1 / (1+abs(n))
so code(0) = 1, code(1) = 0.5,
code(x:real) = 1 / (1+abs x)
code(ConstInt n) = h (n) / 3
code(ConstReal x) = (2 + h (x)) / 3
more generally, for any type t = C0 x | ... | Cn x
code(Ci x) = (2i + h(x)) / (2n+1)
*)
(* not good ?
for any type t = t0 x ... x tn
hash((x0,..,x_n)) = (2i + h(x)) / (2n+1)
*)
(*
let const_code = function
| ConstInt n -> 1.0 /. (1.0 +. abs (float_of_string n)) /. 3.0
| ConstReal n -> (2.0 + 1.0 /. (1.0 +. abs (float_of_string x)) /. 3.0
let rec t_code c m t =
let fn = t_code c m in
let divide i c = (float(i+i) +. c) /. 23.0 in
(* 12 constructors -> divide by 23 *)
match t.t_node with
| Tconst c -> divide 0 (const_code c)
| Tvar v -> divide 1 (Mvs.find_default v (var_code v) m)
| Tapp (s,l) ->
let acc = Hashcons.combine 2 (ls_hash s) in
Hashcons.combine_list fn acc l
| Tif (f,t1,t2) ->
Hashcons.combine3 3 (fn f) (fn t1) (fn t2)
| Tlet (t1,b) ->
let u,t2 = t_open_bound b in
let m = vs_rename_alpha c m u in
Hashcons.combine2 4 (fn t1) (t_hash_alpha c m t2)
| Tcase (t1,bl) ->
let hash_br b =
let p,t2 = t_open_branch b in
let m = pat_rename_alpha c m p in
t_hash_alpha c m t2
in
let acc = Hashcons.combine 5 (fn t1) in
Hashcons.combine_list hash_br acc bl
| Teps b ->
let u,f = t_open_bound b in
let m = vs_rename_alpha c m u in
Hashcons.combine 6 (t_hash_alpha c m f)
| Tquant (q,b) ->
let vl,_,f1 = t_open_quant b in
let m = vl_rename_alpha c m vl in
let hq = match q with Tforall -> 1 | Texists -> 2 in
Hashcons.combine2 1 hq (t_hash_alpha c m f1)
| Tbinop (o,f,g) ->
let ho = match o with
| Tand -> 3 | Tor -> 4 | Timplies -> 5 | Tiff -> 7
in
Hashcons.combine3 2 ho (fn f) (fn g)
| Tnot f ->
Hashcons.combine 3 (fn f)
| Ttrue -> 4
| Tfalse -> 5
let t_hash_alpha = t_hash_alpha (ref (-1)) Mvs.empty
*)
(* distance of two terms *)
(*
let dist_bool b = if b then 0.0 else 1.0
let average l =
let n,s = List.fold_left (fun (n,s) x -> (n+1,s+.x)) (0,0.0) l in
float n *. s
let rec pat_dist p1 p2 =
if ty_equal p1.pat_ty p2.pat_ty then
match p1.pat_node, p2.pat_node with
| Pwild, Pwild | Pvar _, Pvar _ -> 0.0
| Papp (f1, l1), Papp (f2, l2) ->
if ls_equal f1 f2 then
0.5 *. average (List.map2 pat_dist l1 l2)
else 1.0
| Pas (p1, _), Pas (p2, _) -> pat_dist p1 p2
| Por (p1, q1), Por (p2, q2) ->
0.5 *. average [pat_dist p1 p2 ; pat_dist q1 q2 ]
| _ -> 1.0
else 1.0
let rec t_dist c1 c2 m1 m2 e1 e2 =
let t_d = t_dist c1 c2 m1 m2 in
match e1.t_node, e2.t_node with
| Tvar v1, Tvar v2 ->
begin
try dist_bool (Mvs.find v1 m1 = Mvs.find v2 m2)
with Not_found -> 1.0
end
| Tconst c1, Tconst c2 -> 0.5 *. dist_bool (c1 = c2)
| Tapp(ls1,tl1), Tapp(ls2,tl2) ->
if ls_equal ls1 ls2 then
0.5 *. average (List.map2 t_d tl1 tl2)
else 1.0
| Tif(c1,t1,e1), Tif(c2,t2,e2) ->
0.5 *. average [t_d c1 c2 ; t_d t1 t2 ; t_d e1 e2]
| Tlet(t1,b1), Tlet(t2,b2) ->
let u1,e1 = t_open_bound b1 in
let u2,e2 = t_open_bound b2 in
let m1 = vs_rename_alpha c1 m1 u1 in
let m2 = vs_rename_alpha c2 m2 u2 in
0.5 *. average [t_d t1 t2; t_dist c1 c2 m1 m2 e1 e2]
| Tcase (t1,bl1), Tcase (t2,bl2) ->
if List.length bl1 = List.length bl2 then
let br_dist ((pat1,_,_) as b1) ((pat2,_,_) as b2) =
let p1,e1 = t_open_branch b1 in
let p2,e2 = t_open_branch b2 in
let m1 = pat_rename_alpha c1 m1 p1 in
let m2 = pat_rename_alpha c2 m2 p2 in
average [pat_dist pat1 pat2 ; t_dist c1 c2 m1 m2 e1 e2]
in
0.5 *. average (t_d t1 t2 :: List.map2 br_dist bl1 bl2)
else
1.0
| Teps b1, Teps b2 ->
let u1,e1 = t_open_bound b1 in
let u2,e2 = t_open_bound b2 in
let m1 = vs_rename_alpha c1 m1 u1 in
let m2 = vs_rename_alpha c2 m2 u2 in
0.5 *. t_dist c1 c2 m1 m2 e1 e2
| Tquant (q1,b1), Tquant (q2,b2) ->
if q1 = q2 &&
list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2
then
let vl1,_,e1 = t_open_quant b1 in
let vl2,_,e2 = t_open_quant b2 in
let m1 = vl_rename_alpha c1 m1 vl1 in
let m2 = vl_rename_alpha c2 m2 vl2 in
0.5 *. t_dist c1 c2 m1 m2 e1 e2
else
1.0
| Tbinop (a,f1,g1), Tbinop (b,f2,g2) ->
if a = b then 0.5 *. average [ t_d f1 f2 ; t_d g1 g2]
else 1.0
| Tnot f1, Tnot f2 -> 0.5 *. t_d f1 f2
| Ttrue, Ttrue | Tfalse, Tfalse -> 0.0
| _ -> 1.0
let t_dist t1 t2 = t_dist (ref (-1)) (ref (-1)) Mvs.empty Mvs.empty t1 t2
*)
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