


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
(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: 39.2s)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) |
| 40.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 |
| 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 |
| 7.0ms | (* (sin phi1) (sin phi2)) |
| 6.0ms | (cos (- lambda1 lambda2)) |
| 5.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 2.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 67.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) R) |
| 65.0ms | (* (sin phi1) (sin phi2)) |
| 36.0ms | (cos (- lambda1 lambda2)) |
| 14.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))) |
| 70.0ms | (* (* (* (sin phi1) (sin phi1)) (sin phi1)) (* (* (sin phi2) (sin phi2)) (sin phi2))) |
| 51.0ms | (- (+ 1 (* lambda2 lambda1)) (* 1/2 (pow lambda1 2))) |
| 31.0ms | (* (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))))) (cbrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2))))))) |
| 31.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (cos (- lambda1 lambda2)))))) |
| 29.0ms | (* (acos (+ (* (cos phi1) (* (cos (- lambda1 lambda2)) (cos phi2))) (* (sin phi1) (sin phi2)))) R) |
9 alts after pruning (9 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 |
| 3× | *-commutative |
| 2× | sin-mult |
| 2× | cbrt-unprod |
| 2× | prod-exp |
| 2× | pow-prod-down |
| 1× | acos-asin |
| 3.0ms | (* (sin phi1) (sin phi2)) |
| 3.0ms | (* (sin lambda1) (sin lambda2)) |
| 2.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 1.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 96.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) R) |
| 61.0ms | (* (sin lambda1) (sin lambda2)) |
| 59.0ms | (* (sin phi1) (sin phi2)) |
| 21.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2)))))) |
| 195.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)))))))) |
| 178.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda1) (sin lambda2))))))) |
| 145.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) |
| 145.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))) |
| 143.0ms | (* R (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:
| 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 |
| 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 |
| 7.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) |
| 4.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)))))))) |
| 80.0ms | (* (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) R) |
| 73.0ms | (log (exp (* (sin lambda1) (sin lambda2)))) |
| 65.0ms | (* (sin lambda1) (sin lambda2)) |
| 34.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2)))))))) |
| 268.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)))))))))) |
| 226.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (log (exp (* (sin lambda1) (sin lambda2))))))))) |
| 164.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))) |
| 160.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) |
| 137.0ms | (* R (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2)))))) |
11 alts after pruning (11 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× | log-pow |
| 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 |
| 7.0ms | (* (sin phi1) (sin phi2)) |
| 4.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)))))))) |
| 107.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)) |
| 30.0ms | (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1)))))))) |
| 16.0ms | (log (exp (sin lambda1))) |
| 182.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)))))))))) |
| 166.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (sin lambda1) (sin lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (* (sin phi1) (sin phi2))))) |
| 165.0ms | (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) |
| 160.0ms | (sqrt (acos (+ (* (sin phi1) (sin phi2)) (* (* (cos phi1) (cos phi2)) (+ (* (cos lambda1) (cos lambda2)) (* (sin lambda2) (log (exp (sin lambda1))))))))) |
| 146.0ms | (* (acos (+ (* (cos phi1) (* (cos phi2) (* (cos lambda1) (cos lambda2)))) (+ (* (cos phi1) (* (cos phi2) (* (sin lambda2) (sin lambda1)))) (* (sin phi1) (sin phi2))))) R) |
11 alts after pruning (11 fresh and 0 done)
Merged error: 2.8b
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) |