Commit 32db4336 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update WP script for loat_rmat_of_quat function

parent b4501f19
......@@ -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": 0.89 } ],
"verdict": "valid", "time": 0.78 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.23 } ],
"verdict": "valid", "time": 4.14 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.18 } ],
"verdict": "valid", "time": 3.91 } ],
"OverLap": [ { "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": 3.64 } ],
"verdict": "valid", "time": 3.49 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.3 } ],
"verdict": "valid", "time": 4.86 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.38 } ],
"verdict": "valid", "time": 4.86 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 10. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children": { "Unfold 'P_unary_quaternion_1_'": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 10. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Separated",
"tactic": "Wp.separated",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.26 } ],
"OnLeft":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.48 } ],
"OnRight":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.5 } ],
"OverLap":
[ { "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": 5.8 } ],
"verdict": "valid", "time": 5.47 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 8.96 } ],
"verdict": "valid", "time": 9.26 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 8.91 } ],
"verdict": "valid", "time": 9.52 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -12,4 +12,4 @@
"children": { "Unfold 'L_l_RMat_of_FloatQuat_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.24 } ] } } ] } } ]
"time": 3.4 } ] } } ] } } ]
......@@ -72,7 +72,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.48 } ] } } ],
"time": 1.58 } ] } } ],
"Goal 2/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -88,7 +88,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.7839,
"time": 1.7821,
"steps": 28 } ] } } ],
"Goal 3/6":
[ { "header": "Definition",
......@@ -105,7 +105,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.07 } ] } } ],
"time": 1.01 } ] } } ],
"Goal 4/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -121,7 +121,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.85 } ] } } ],
"time": 1.5 } ] } } ],
"Goal 5/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -137,7 +137,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.18 } ] } } ],
"time": 1.83 } ] } } ],
"Goal 6/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -153,7 +153,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5372,
"time": 2.2867,
"steps": 28 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
......@@ -33,5 +33,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.0835,
"time": 3.0657,
"steps": 28 } ] } } ] } } ] } } ] } } ]
......@@ -63,5 +63,5 @@
{ "Unfold 'EqS12_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.02,
"time": 0.03,
"steps": 45566 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
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