Commit 503e4737 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Code cleaning

parent 7ba71702
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.2306,
"steps": 991 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.5505,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 10.1966,
"steps": 1288 } ] } } ] } } ] } } ] } } ]
"time": 2.7065,
"steps": 1249 } ] } } ] } } ] } } ] } } ]
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 10.5394,
"steps": 1289 },
"time": 2.4316,
"steps": 1008 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_7 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 F12_RealRMat_s_a00 = Mf32_7[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_7[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_7[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_7[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_7[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_7[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_7[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_7[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_7[(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 F12_RealRMat_s_a00 = Mf32_7[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_7[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_7[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_7[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_7[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_7[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_7[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_7[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_7[(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_7[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_7[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_7[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_7[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_7[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_7[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_7[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_7[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_7[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.32 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n } L_id_rmat)",
"pattern": "EqS9_RealRMat_s{RealRMat_s}L_id_rmat" },
"children":
{ "Unfold 'EqS9_RealRMat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"kind": "have",
"occur": 0,
"target": "L_id_rmat",
"pattern": "L_id_rmat" },
"children":
{ "Unfold 'L_id_rmat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.27 } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "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.31,
"steps": 404607 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 3.7782, "steps": 1331 } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_7 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 F12_RealRMat_s_a00 = Mf32_7[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_7[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_7[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_7[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_7[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_7[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_7[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_7[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_7[(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 F12_RealRMat_s_a00 = Mf32_7[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_7[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_7[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_7[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_7[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_7[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_7[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_7[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_7[(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": "L_id_rmat",
"pattern": "L_id_rmat" },
"children":
{ "Unfold 'L_id_rmat'":
[ { "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_7[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_7[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_7[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_7[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_7[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_7[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_7[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_7[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_7[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.49,
"steps": 548633 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n }\n {\n F9_RealRMat_s_a00 = 1 ;\n F9_RealRMat_s_a01 = 0 ;\n F9_RealRMat_s_a02 = 0 ;\n F9_RealRMat_s_a10 = 0 ;\n F9_RealRMat_s_a11 = 1 ;\n F9_RealRMat_s_a12 = 0 ;\n F9_RealRMat_s_a20 = 0 ;\n F9_RealRMat_s_a21 = 0 ;\n F9_RealRMat_s_a22 = 1\n })",
"pattern": "EqS9_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS9_RealRMat_s'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 1.6,
"steps": 3136482 } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "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.7925, "steps": 722 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 4.5395, "steps": 1331 } ] } } ]
[ { "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(L_l_FloatQuat_of_RMat_trace_pos_t Mf32_0 rm_0)",
"pattern": "L_l_FloatQuat_of_RMat_trace_pos_t" },
......@@ -69,25 +68,7 @@
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 15. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout",
"time": 15. },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 15. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 15. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 22.0475,
"steps": 848 },
{ "header": "Definition",
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......@@ -96,9 +77,7 @@
"pattern": "EqS13_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"children":
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 12.127,
"steps": 3775 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 9.5815,
"steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -608,25 +608,6 @@ void float_quat_of_orientation_vect(struct FloatQuat *q, const struct FloatVect3
}
}
/*
lemma test:
\forall real r_5, r_6, r_12, r_13, r_14, r_15, r_16, r_17;
SQR(r_5) / 4
+ SQR((r_14 - r_12) / (2 * r_5)) + SQR((r_13 - r_16) / (2 * r_5)) + SQR((r_17 - r_15) / (2 * r_5)) == 1.0;
*/
/*
lemma test_2:
\forall struct FloatRMat *rm;
\let r_4 = 1.0 + rm->m[0] + rm->m[4] + rm->m[8];
\let r_5 = \sqrt(r_4);
\let r_6 = 2.0 * r_5;
\valid_read(rm) ==>
((1.0/4) * r_5 * r_5
+ SQR((rm->m[5] - rm->m[7]) / (r_6))
+ SQR((rm->m[6] - rm->m[2]) / (r_6))
+ SQR((rm->m[1] - rm->m[3]) / (r_6))) == 1.0;
*/
void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
{
......@@ -638,19 +619,6 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = (RMAT_ELMT(*rm, 1, 2) - RMAT_ELMT(*rm, 2, 1)) / four_qi;
q->qy = (RMAT_ELMT(*rm, 2, 0) - RMAT_ELMT(*rm, 0, 2)) / four_qi;
q->qz = (RMAT_ELMT(*rm, 0, 1) - RMAT_ELMT(*rm, 1, 0)) / four_qi;
//@ assert q->qi * q->qi == 0.5* 0.5 * (1 + tr);
//@ assert \at(rm->m[0], Pre) == rm->m[0];
//@ assert \at(rm->m[1], Pre) == rm->m[1];
//@ assert \at(rm->m[2], Pre) == rm->m[2];
//@ assert \at(rm->m[3], Pre) == rm->m[3];
//@ assert \at(rm->m[4], Pre) == rm->m[4];
//@ assert \at(rm->m[5], Pre) == rm->m[5];
//@ assert \at(rm->m[6], Pre) == rm->m[6];
//@ assert \at(rm->m[7], Pre) == rm->m[7];
//@ assert \at(rm->m[8], Pre) == rm->m[8];
//@ assert SQR(rm->m[0]) + SQR(rm->m[1]) + SQR(rm->m[2]) == 1;
// assert transpose(l_RMat_of_FloatRMat(rm)) == l_RMat_of_FloatQuat(q);
// assert unary_quaternion(q);
/*printf("tr > 0\n");*/
} else {
if (RMAT_ELMT(*rm, 0, 0) > RMAT_ELMT(*rm, 1, 1) &&
......@@ -662,7 +630,6 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = 0.5 * two_qx;
q->qy = (RMAT_ELMT(*rm, 0, 1) + RMAT_ELMT(*rm, 1, 0)) / four_qx;
q->qz = (RMAT_ELMT(*rm, 2, 0) + RMAT_ELMT(*rm, 0, 2)) / four_qx;
// assert unary_quaternion(q);
/*printf("m00 largest\n");*/
} else if (RMAT_ELMT(*rm, 1, 1) > RMAT_ELMT(*rm, 2, 2)) {
const float two_qy =
......@@ -672,7 +639,6 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = (RMAT_ELMT(*rm, 0, 1) + RMAT_ELMT(*rm, 1, 0)) / four_qy;
q->qy = 0.5 * two_qy;
q->qz = (RMAT_ELMT(*rm, 1, 2) + RMAT_ELMT(*rm, 2, 1)) / four_qy;
// assert unary_quaternion(q);
/*printf("m11 largest\n");*/
} else {
const float two_qz =
......@@ -682,7 +648,6 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = (RMAT_ELMT(*rm, 2, 0) + RMAT_ELMT(*rm, 0, 2)) / four_qz;
q->qy = (RMAT_ELMT(*rm, 1, 2) + RMAT_ELMT(*rm, 2, 1)) / four_qz;
q->qz = 0.5 * two_qz;
// assert unary_quaternion(q);
/*printf("m22 largest\n");*/
}
}
......
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