


Bits error versus R



Bits error versus lambda1



Bits error versus lambda2



Bits error versus phi1



Bits error versus phi2
Results
Initial program 17.0
rmApplied cos-diff3.6
rmApplied acos-asin3.7
Final simplification3.7
herbie shell --seed 2019016 +o rules:numerics
(FPCore (R lambda1 lambda2 phi1 phi2)
:name "Spherical law of cosines"
(* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R))
Time bar (total: 42.3s)Debug log
| 256× | (pre true 80) |
| 153× | (body real 1280) |
| 64× | (body real 640) |
| 23× | (body real 320) |
| 12× | (body real 160) |
| 4× | (body real 80) |
| 79.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 16.5b
Found 4 expressions with local error:
| 4.0b | (cos (- lambda1 lambda2)) |
| 1.3b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 0.2b | (* (sin phi1) (sin phi2)) |
| 0.2b | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 7× | add-cube-cbrt |
| 7× | *-un-lft-identity |
| 7× | add-sqr-sqrt |
| 6× | add-exp-log |
| 6× | associate-*l* |
| 6× | add-cbrt-cube |
| 6× | pow1 |
| 4× | add-log-exp |
| 4× | log1p-expm1-u |
| 4× | expm1-log1p-u |
| 3× | associate-*r* |
| 2× | *-commutative |
| 2× | cos-sum |
| 1× | sin-mult |
| 1× | cbrt-unprod |
| 1× | prod-exp |
| 1× | pow-prod-down |
| 1× | sub-neg |
| 1× | cos-diff |
| 1× | acos-asin |
| 8.0ms | (* (sin phi1) (sin phi2)) |
| 5.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 4.0ms | (cos (- lambda1 lambda2)) |
| 2.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 59.0ms | (* (sin phi1) (sin phi2)) |
| 53.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 28.0ms | (cos (- lambda1 lambda2)) |
| 11.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 61.0ms | (- (+ 1 (* lambda2 lambda1)) (* 1/2 (pow lambda1 2))) |
| 51.0ms | (* (* (* (sin phi1) (sin phi1)) (sin phi1)) (* (* (sin phi2) (sin phi2)) (sin phi2))) |
| 33.0ms | (* (acos (+ (* (cos phi1) (* (cos (- lambda1 lambda2)) (cos phi2))) (* (sin phi1) (sin phi2)))) R) |
| 33.0ms | (* (acos (+ (* (cos phi1) (* (cos (- lambda1 lambda2)) (cos phi2))) (* (sin phi1) (sin phi2)))) R) |
| 32.0ms | (acos (+ (* (cos phi1) (* (cos (- lambda1 lambda2)) (cos phi2))) (* (sin phi1) (sin phi2)))) |
10 alts after pruning (10 fresh and 0 done)
Merged error: 2.9b
Found 4 expressions with local error:
| 1.2b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 0.2b | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 0.2b | (* (sin phi1) (sin phi2)) |
| 0.2b | (* (sin lambda1) (sin lambda2)) |
| 9× | add-cube-cbrt |
| 9× | associate-*l* |
| 9× | *-un-lft-identity |
| 9× | add-sqr-sqrt |
| 8× | add-exp-log |
| 8× | add-cbrt-cube |
| 8× | pow1 |
| 6× | associate-*r* |
| 4× | add-log-exp |
| 4× | log1p-expm1-u |
| 4× | expm1-log1p-u |
| 3× | *-commutative |
| 2× | sin-mult |
| 2× | cbrt-unprod |
| 2× | prod-exp |
| 2× | pow-prod-down |
| 1× | acos-asin |
| 7.0ms | (* (sin phi1) (sin phi2)) |
| 5.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 4.0ms | (* (sin lambda1) (sin lambda2)) |
| 3.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 79.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 68.0ms | (* (sin phi1) (sin phi2)) |
| 60.0ms | (* (sin lambda1) (sin lambda2)) |
| 16.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 277.0ms | (* (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))) (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))))) |
| 269.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))) |
| 249.0ms | (* (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) R) |
| 241.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))) |
| 236.0ms | (* R (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2)))))) |
13 alts after pruning (13 fresh and 0 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 2.7b | (log (exp (* (sin lambda1) (sin lambda2)))) |
| 1.2b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) |
| 0.2b | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) R) |
| 0.2b | (* (sin lambda1) (sin lambda2)) |
| 8× | add-cube-cbrt |
| 8× | *-un-lft-identity |
| 8× | add-sqr-sqrt |
| 7× | pow1 |
| 6× | add-exp-log |
| 6× | associate-*l* |
| 6× | add-cbrt-cube |
| 5× | add-log-exp |
| 4× | log1p-expm1-u |
| 4× | expm1-log1p-u |
| 3× | log-pow |
| 3× | associate-*r* |
| 3× | log-prod |
| 2× | *-commutative |
| 1× | sin-mult |
| 1× | cbrt-unprod |
| 1× | prod-exp |
| 1× | pow-prod-down |
| 1× | rem-log-exp |
| 1× | exp-to-pow |
| 1× | exp-prod |
| 1× | acos-asin |
| 8.0ms | (* (sin lambda1) (sin lambda2)) |
| 5.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) R) |
| 5.0ms | (log (exp (* (sin lambda1) (sin lambda2)))) |
| 2.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) |
| 95.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) R) |
| 77.0ms | (log (exp (* (sin lambda1) (sin lambda2)))) |
| 54.0ms | (* (sin lambda1) (sin lambda2)) |
| 29.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) |
| 307.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2))))))))) |
| 272.0ms | (* (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2))))))))) (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))))) |
| 270.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) |
| 239.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))) |
| 230.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))) |
12 alts after pruning (12 fresh and 0 done)
Merged error: 2.8b
Found 4 expressions with local error:
| 3.2b | (log (exp (sin lambda1))) |
| 1.2b | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) |
| 0.2b | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) R) |
| 0.2b | (* (sin phi1) (sin phi2)) |
| 9× | add-cube-cbrt |
| 9× | *-un-lft-identity |
| 9× | add-sqr-sqrt |
| 7× | pow1 |
| 6× | add-exp-log |
| 6× | associate-*l* |
| 6× | add-cbrt-cube |
| 4× | add-log-exp |
| 4× | log1p-expm1-u |
| 4× | log-pow |
| 4× | expm1-log1p-u |
| 3× | associate-*r* |
| 3× | exp-prod |
| 3× | log-prod |
| 2× | *-commutative |
| 1× | sin-mult |
| 1× | cbrt-unprod |
| 1× | prod-exp |
| 1× | pow-prod-down |
| 1× | rem-log-exp |
| 1× | acos-asin |
| 8.0ms | (* (sin phi1) (sin phi2)) |
| 5.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) R) |
| 4.0ms | (log (exp (sin lambda1))) |
| 2.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) |
| 113.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) R) |
| 73.0ms | (* (sin phi1) (sin phi2)) |
| 31.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) |
| 22.0ms | (log (exp (sin lambda1))) |
| 300.0ms | (* (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1))))))))) (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))))) |
| 262.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1))))))))) |
| 219.0ms | (* (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) R) |
| 209.0ms | (* R (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2)))))) |
| 200.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) |
12 alts after pruning (12 fresh and 0 done)
Merged error: 2.7b
0% (0.4b remaining)
Error of 3.7b against oracle of 3.3b and baseline of 3.7b
| 8004× | (pre true 80) |
| 4769× | (body real 1280) |
| 2126× | (body real 640) |
| 703× | (body real 320) |
| 263× | (body real 160) |
| 127× | (body real 80) |
| 16× | (body real 2560) |