Commit eb497c00 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Updating script

parent 0edd19ed
......@@ -63,11 +63,13 @@
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.57,
"steps": 504993 } ],
"time": 13.0899,
"steps": 762 } ],
"Else":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.4768,
"time": 1.3846,
"steps": 988 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.7078,
"time": 3.5036,
"steps": 1254 } ] } } ] } } ] } } ] } } ]
......@@ -58,7 +58,7 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.0464,
"time": 2.6657,
"steps": 1013 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F13_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F13_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_1[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_1[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_1[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_1[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_1[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_1[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_1[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_1[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F13_RealRMat_s_a00 = r_0 ;\n F13_RealRMat_s_a01 = r_1 ;\n F13_RealRMat_s_a02 = r_2 ;\n F13_RealRMat_s_a10 = r_3 ;\n F13_RealRMat_s_a11 = r_4 ;\n F13_RealRMat_s_a12 = r_5 ;\n F13_RealRMat_s_a20 = r_6 ;\n F13_RealRMat_s_a21 = r_7 ;\n F13_RealRMat_s_a22 = r_8\n }\n {\n F13_RealRMat_s_a00 = r_0 ;\n F13_RealRMat_s_a01 = r_3 ;\n F13_RealRMat_s_a02 = r_6 ;\n F13_RealRMat_s_a10 = r_1 ;\n F13_RealRMat_s_a11 = r_4 ;\n F13_RealRMat_s_a12 = r_7 ;\n F13_RealRMat_s_a20 = r_2 ;\n F13_RealRMat_s_a21 = r_5 ;\n F13_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 8,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.33,
"steps": 440606 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 10,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 4)]<Mf32_1[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 12,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.45,
"steps": 404798 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 16,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.1,
"steps": 276811 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.39,
"steps": 404043 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 13,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.35,
"steps": 404774 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.51,
"steps": 401541 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "script", "verdict": "valid", "time": 3.0907, "steps": 1331 },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 8, "kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children": { "Then": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 0.8195, "steps": 721 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 3.0907, "steps": 1331 } ] } } ]
......@@ -3,5 +3,5 @@
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 5.6003,
"verdict": "valid", "time": 5.9597,
"steps": 1628 } ] } } ]
......@@ -70,7 +70,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.4829,
"time": 3.6229,
"steps": 809 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 20. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 20. },
{ "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 8.49 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 13.72 } ],
"OnRight": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 15.68 } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 20. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 20. },
{ "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.82 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.37 } ],
"OnRight": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.47 } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 2.05 } ],
"verdict": "valid", "time": 2.41 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.22 } ],
"verdict": "valid", "time": 5. } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.31 } ],
"verdict": "valid", "time": 4.84 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 20. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 20. },
{ "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 14.1908,
"steps": 136 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 20.95 },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 20. } ],
"OnRight": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 20. },
{ "header": "Range",
"tactic": "Wp.range",
"params":
{ "inf": 0,
"sup": 0 },
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(offset rm_0)",
"pattern": "offset$rm" },
"children":
{ "Lower 0":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.04,
"steps": 247903 },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" } ],
"Value 0":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.05,
"steps": 248289 },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" } ],
"Upper 0":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 18.2 } ] } } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -31,5 +31,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.03,
"steps": 149234 } ] } } ] } } ] } } ] } } ]
"time": 0.04,
"steps": 144528 } ] } } ] } } ] } } ] } } ]
......@@ -63,5 +63,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 8.7116,
"time": 8.5669,
"steps": 144 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -33,5 +33,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.7335,
"time": 3.4379,
"steps": 28 } ] } } ] } } ] } } ] } } ]
......@@ -31,7 +31,7 @@
{ "Unfold 'EqS12_RealVect3_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0037,
"time": 0.0186,
"steps": 8 },
{ "header": "Split",
"tactic": "Wp.split",
......
......@@ -61,7 +61,6 @@
"pattern": "EqS13_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS13_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.04,
"steps": 51791 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.63 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -193,5 +193,5 @@
{ "Unfold 'L_add_RealVect3'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.4797,
"time": 4.1286,
"steps": 142 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
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