Skip to content
Snippets Groups Projects
Commit c8a80909 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] script updates

parent 6a52d235
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 33 additions and 132 deletions
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
+ 4
− 22
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_P1 i_0) /\\ (P_Q1 i_2) /\\ (P_P2 i_1 i_2)\n/\\ (exists i_3:int.\n (P_Q2 i_0 i_3))",
"pattern": "\\E\\E\\E&P_P1P_Q1P_P2\\E#3#1#2#1P_Q2" },
"children": { "Goal 1/2": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0511159896851 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int. (P_Q1 i_0) /\\ (P_P2 i_1 i_0)",
"pattern": "\\E\\E&P_Q1P_P2#1#0#1" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0514709949493 } ] } } ],
"Goal 2/2": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0521941184998 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0:int. (P_P1 i_0) /\\ (exists i_1:int.\n (P_Q2 i_0 i_1))",
"pattern": "\\E&P_P1\\E#1P_Q2#1#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515058040619 } ] } } ] } } ]
"pattern": "\\E" },
"children": { "Goal 1/2": [], "Goal 2/2": [] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
+ 4
− 32
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2,i_3:int.\n(P_Q1 1) /\\ (P_P2 i_0 i_1) /\\ (P_R2 i_1 i_2)\n/\\ (exists i_4:int.\n (P_Q2 i_3 i_4))",
"pattern": "\\E\\E\\E\\E&P_Q1P_P2P_R2\\E1#4#3#3#2" },
"children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0512578487396 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int. (P_Q2 i_0 i_1)",
"pattern": "\\E\\EP_Q2#1#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515179634094 } ] } } ],
"Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0517938137054 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int. (P_P2 i_2 i_1) /\\ (P_R2 i_1 i_0)",
"pattern": "\\E\\E\\E&P_P2P_R2#0#1#1#2" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515098571777 } ] } } ],
"Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0528788566589 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "(P_Q1 1)",
"pattern": "P_Q11" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515050888062 } ] } } ] } } ]
"pattern": "\\EP_Q11" },
"children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
+ 3
− 13
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_Q1 1) \\/ (P_P1 i_0) \\/ (P_P2 i_1 i_2) \\/ (exists i_3:int.\n (P_Q2 i_0 i_3))",
"pattern": "\\E\\E\\E|P_Q1P_P1P_P2\\E1#3#2#1P_Q2" },
"children": { "Distrib (exists or)": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515348911285 },
{ "header": "NOP",
"tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-goal",
"target": "(P_Q1 1) \\/ (exists i_0:int.\n (P_P1 i_0)) \\/ (exists i_0,i_1:int.\n (P_P2 i_1 i_0))\n\\/ (exists i_0,i_1:int.\n (P_Q2 i_0 i_1))",
"pattern": "|P_Q1\\E\\E\\E1P_P1\\E\\E#0P_P2P_Q2#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0513439178467 } ] } } ] } } ]
"pattern": "\\EP_Q11" },
"children": { "Split": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "unknown" } ] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
+ 4
− 16
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2:int.\n(P_Q1 1) /\\ (P_P1 i_0) /\\ (P_P2 i_1 i_2) /\\ (forall i_3:int.\n (P_Q2 i_0 i_3))",
"pattern": "\\F\\F\\F&P_Q1P_P1P_P2\\F1#3#2#1P_Q2" },
"children": { "Distrib (forall and)": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.051558971405 },
{ "header": "NOP",
"tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0,
"kind": "have",
"target": "(P_Q1 1) /\\ (forall i_0:int.\n (P_P1 i_0)) /\\ (forall i_0,i_1:int.\n (P_P2 i_1 i_0))\n/\\ (forall i_0,i_1:int.\n (P_Q2 i_0 i_1))",
"pattern": "&P_Q1\\F\\F\\F1P_P1\\F\\F#0P_P2P_Q2#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0513830184937 } ] } } ] } } ]
"pattern": "\\FP_Q11" },
"children": { "Split (distrib forall and)": [] } } ]
src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
+ 4
− 35
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
[ { "prover": "script", "verdict": "unknown" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2,i_3:int.\n(P_Q1 1) \\/ (P_P2 i_0 i_1) \\/ (P_R2 i_1 i_2)\n\\/ (forall i_4:int.\n (P_Q2 i_3 i_4))",
"pattern": "\\F\\F\\F\\F|P_Q1P_P2P_R2\\F1#4#3#3#2" },
"children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0511250495911 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "forall i_0,i_1:int. (P_Q2 i_0 i_1)",
"pattern": "\\F\\FP_Q2#1#0" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515208244324 } ] } } ],
"Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0517539978027 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2:int. (P_P2 i_2 i_1) \\/ (P_R2 i_1 i_0)",
"pattern": "\\F\\F\\F|P_P2P_R2#0#1#1#2" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.0515398979187 } ] } } ],
"Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
"time": 0.0528609752655 },
{ "header": "NOP", "tactic": "Wp.Test.NOP",
"params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
"target": "(P_Q1 1)",
"pattern": "P_Q11" },
"children": { "Nop": [ { "prover": "alt-ergo",
"verdict": "unknown",
"time": 0.051561832428 } ] } } ] } } ]
"pattern": "\\FP_Q11" },
"children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+ 2
− 2
View file @ c8a80909
......@@ -17,7 +17,7 @@
predicate R2(integer a1, integer a2) reads \nothing ;
} */
/*@ ensures Goal_Exist_Or:
/*@ ensures Goal_Exist_Or:
(\exists integer a, b, c ;
P1(a) || P2(b, c) || Q1(1) || \exists integer d ; Q2(a,d)) ;
......@@ -29,7 +29,7 @@
(\exists integer a, b, c, d ;
P2(a, b) && R2(b, c) && Q1(1) && \exists integer e ; Q2(d,e)) ;
@ ensures Hyp_Forall_And:
@ ensures Hyp_Forall_And:
(\forall integer a, b, c ;
P1(a) && P2(b, c) && Q1(1) && \forall integer d ; Q2(a,d)
) ==>
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0236,
"steps": 41 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.018,
"steps": 29 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0177,
"steps": 40 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
"pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0154,
"steps": 24 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0167,
"steps": 33 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0167,
"steps": 33 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0196,
"steps": 39 } ],
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+ 1
− 1
View file @ c8a80909
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0152,
"steps": 27 } ],
......
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