Metrics for Midpoint on a great circle

analyze1.5s (2.2%)

Algorithm

1×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	99.8%	0.2%	0%	0%	0%	0
0%	0%	99.8%	0.2%	0%	0%	0%	1
0%	0%	99.8%	0.2%	0%	0%	0%	2
0%	0%	99.8%	0.2%	0%	0%	0%	3
0%	0%	99.8%	0.2%	0%	0%	0%	4
0%	0%	99.8%	0.2%	0%	0%	0%	5
0%	0%	99.8%	0.2%	0%	0%	0%	6
0%	0%	99.8%	0.2%	0%	0%	0%	7
0%	0%	99.8%	0.2%	0%	0%	0%	8
9.4%	9.4%	90.4%	0.2%	0%	0%	0%	9
9.4%	9.4%	90.4%	0.2%	0%	0%	0%	10
10.9%	10.9%	88.9%	0.2%	0%	0%	0%	11
10.9%	10.9%	88.9%	0.2%	0%	0%	0%	12

Compiler

Compiled 25 to 15 computations (40% saved)

sample1.1min (96.9%)

Results

6.3s	4301×	1	valid-rival
2.7s	4238×	1	valid-sollya
2.3s	3950×	0	valid-rival
1.3s	3928×	0	valid-sollya
315.0ms	63×	1	exit-sollya
110.0ms	22×	0	exit-sollya
6.0ms	5×	2	valid-rival
1.0ms	5×	2	valid-sollya

Bogosity

preprocess532.0ms (0.8%)

Algorithm

1×	egg-herbie

Rules

823×	`fma-neg`
781×	`fma-define`
250×	`unsub-neg`
209×	`distribute-lft-neg-in`
184×	`sub-neg`

Iterations

Useful iterations: 2 (0.0ms)

Iter	Nodes	Cost
0	103	1448
1	179	1356
2	294	1348
3	584	1348
4	991	1348
5	1349	1348
6	1744	1348
7	2122	1348
8	2584	1348
9	3151	1348
10	3884	1348
11	4232	1348
12	4410	1348
13	4499	1348
14	4523	1348
15	4527	1348
16	4527	1348
17	4592	1348

Stop Event

1×

saturated

Calls

Call 1

Inputs
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 (neg.f64 lambda1) (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 (neg.f64 lambda2)))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2)))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 (neg.f64 phi1)) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 (neg.f64 phi2)) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 (neg.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))))
(neg.f64 (+.f64 (neg.f64 lambda1) (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)))))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 (neg.f64 lambda2)))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2))))))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 (neg.f64 phi1)) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 (neg.f64 phi2)) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 (neg.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2)))))))
(+.f64 lambda2 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda2 lambda1))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))))))
(+.f64 phi1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 phi1 lambda2))) (+.f64 (cos.f64 lambda1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 phi1 lambda2))))))
(+.f64 phi2 (atan2.f64 (.f64 (cos.f64 lambda1) (sin.f64 (-.f64 phi2 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 lambda1) (cos.f64 (-.f64 phi2 lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 phi1))) (+.f64 (cos.f64 lambda2) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 phi1))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 lambda2) (sin.f64 (-.f64 lambda1 phi2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 lambda2) (cos.f64 (-.f64 lambda1 phi2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi1) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi2) (.f64 (cos.f64 phi1) (cos.f64 (-.f64 lambda1 lambda2))))))

Outputs
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(+.f64 (neg.f64 lambda1) (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2))))))
(-.f64 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)) (cos.f64 phi1))) lambda1)
(-.f64 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda2) lambda1))) (fma.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2)) (cos.f64 phi1))) lambda1)
(-.f64 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2)) (cos.f64 phi1))) lambda1)
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 (neg.f64 lambda2)))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2)))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (+.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2)) (cos.f64 phi1))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 (neg.f64 phi1)) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 (neg.f64 phi2)) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 (neg.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(neg.f64 (+.f64 (neg.f64 lambda1) (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)))))))
(-.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)) (cos.f64 phi1))))
(-.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda2) lambda1))) (fma.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2)) (cos.f64 phi1))))
(-.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 (neg.f64 lambda1) lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2)) (cos.f64 phi1))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 (neg.f64 lambda2)))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2))))))))
(-.f64 (neg.f64 lambda1) (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (+.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2)) (cos.f64 phi1))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 (neg.f64 phi1)) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))))
(-.f64 (neg.f64 lambda1) (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 (neg.f64 phi2)) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 (neg.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2)))))))
(neg.f64 (+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))))
(-.f64 (neg.f64 lambda1) (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(+.f64 lambda2 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda2 lambda1))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))))))
(+.f64 lambda2 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda2 lambda1))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)) (cos.f64 phi1))))
(+.f64 lambda2 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda2 lambda1))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1))))
(+.f64 phi1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 phi1 lambda2))) (+.f64 (cos.f64 lambda1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 phi1 lambda2))))))
(+.f64 phi1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 phi1 lambda2))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 phi1 lambda2)) (cos.f64 lambda1))))
(+.f64 phi2 (atan2.f64 (.f64 (cos.f64 lambda1) (sin.f64 (-.f64 phi2 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 lambda1) (cos.f64 (-.f64 phi2 lambda2))))))
(+.f64 phi2 (atan2.f64 (*.f64 (cos.f64 lambda1) (sin.f64 (-.f64 phi2 lambda2))) (fma.f64 (cos.f64 lambda1) (cos.f64 (-.f64 phi2 lambda2)) (cos.f64 phi1))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 phi1))) (+.f64 (cos.f64 lambda2) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 phi1))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 phi1))) (fma.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 phi1)) (cos.f64 lambda2))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 lambda2) (sin.f64 (-.f64 lambda1 phi2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 lambda2) (cos.f64 (-.f64 lambda1 phi2))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (cos.f64 lambda2) (sin.f64 (-.f64 lambda1 phi2))) (fma.f64 (cos.f64 lambda2) (cos.f64 (-.f64 lambda1 phi2)) (cos.f64 phi1))))
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi1) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi2) (.f64 (cos.f64 phi1) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (.f64 (sin.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1)) (+.f64 (cos.f64 phi2) (.f64 (cos.f64 phi1) (cos.f64 (-.f64 lambda1 lambda2))))))
(+.f64 lambda1 (atan2.f64 (*.f64 (sin.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi1)) (fma.f64 (cos.f64 phi1) (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi2))))

Symmetry

(abs phi1)

(abs phi2)

Compiler

Compiled 24 to 14 computations (41.7% saved)

eval0.0ms (0%)

Compiler: Compiled 4 to 4 computations (0% saved)

prune2.0ms (0%)

Alt Table

Click to see full alt table

Status	Accuracy	Program
	98.7%	(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))

Compiler

Compiled 48 to 28 computations (41.7% saved)

simplify5.0ms (0%)

Algorithm

1×	egg-herbie

Rules

4×	`+-commutative`
3×	`*-commutative`
2×	`sub-neg`
1×	`neg-sub0`
1×	`neg-mul-1`

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	22	87
1	28	87
2	33	87
3	35	87
4	36	87

Stop Event

1×

saturated

Calls

Call 1

Inputs
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))

Outputs
(+.f64 lambda1 (atan2.f64 (.f64 (cos.f64 phi2) (sin.f64 (-.f64 lambda1 lambda2))) (+.f64 (cos.f64 phi1) (.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))))))

soundness1.0ms (0%)

Stop Event

1×

fuel

Compiler

Compiled 24 to 14 computations (41.7% saved)

preprocess96.0ms (0.1%)

Remove

(abs phi2)

(abs phi1)

Compiler

Compiled 288 to 168 computations (41.7% saved)

Midpoint on a great circle

analyze1.5s (2.2%)

sample1.1min (96.9%)

preprocess532.0ms (0.8%)

eval0.0ms (0%)

prune2.0ms (0%)

simplify5.0ms (0%)

soundness1.0ms (0%)

preprocess96.0ms (0.1%)

end0.0ms (0%)

Profiling