Average Error: 36.9 → 0.3
Time: 57.7s
Precision: 64
Internal Precision: 128
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -5.956917387507836 \cdot 10^{-06}:\\ \;\;\;\;\frac{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\ \mathbf{elif}\;\varepsilon \le 3.1311107548585422 \cdot 10^{-06}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot (\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \left(\varepsilon + {\varepsilon}^{5} \cdot \frac{2}{15}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_* \cdot \frac{\tan \varepsilon + \tan x}{1 - \frac{{\left(\tan \varepsilon \cdot \sin x\right)}^{3}}{{\left(\cos x\right)}^{3}}} - \tan x\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Target

Original36.9
Target14.9
Herbie0.3
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -5.956917387507836e-06

    1. Initial program 28.4

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Using strategy rm

    3. Applied tan-sum0.4

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm

    5. Applied flip--0.5

      \[\leadsto \color{blue}{\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} + \tan x}}\]

    if -5.956917387507836e-06 < eps < 3.1311107548585422e-06

    1. Initial program 44.8

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Using strategy rm

    3. Applied tan-sum44.2

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm

    5. Applied flip3--44.2

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]

    6. Applied associate-/r/44.2

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]

    7. Simplified44.2

      \[\leadsto \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \color{blue}{(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_*} - \tan x\]
    8. Using strategy rm

    9. Applied fma-udef44.2

      \[\leadsto \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \color{blue}{\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot (\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_* + 1\right)} - \tan x\]

    10. Applied distribute-rgt-in44.2

      \[\leadsto \color{blue}{\left(\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot (\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} + 1 \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}\right)} - \tan x\]

    11. Applied associate--l+39.7

      \[\leadsto \color{blue}{\left(\left(\tan \varepsilon \cdot \tan x\right) \cdot (\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} + \left(1 \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} - \tan x\right)}\]

    12. Taylor expanded around 0 0.2

      \[\leadsto \left(\left(\tan \varepsilon \cdot \tan x\right) \cdot (\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) \cdot \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} + \color{blue}{\left(\frac{1}{3} \cdot {\varepsilon}^{3} + \left(\frac{2}{15} \cdot {\varepsilon}^{5} + \varepsilon\right)\right)}\]

    if 3.1311107548585422e-06 < eps

    1. Initial program 29.9

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Using strategy rm

    3. Applied tan-sum0.4

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm

    5. Applied flip3--0.4

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]

    6. Applied associate-/r/0.4

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]

    7. Simplified0.4

      \[\leadsto \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \color{blue}{(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_*} - \tan x\]
    8. Using strategy rm

    9. Applied tan-quot0.5

      \[\leadsto \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon\right)}^{3}} \cdot (\left(\tan \varepsilon \cdot \tan x\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_* - \tan x\]

    10. Applied associate-*l/0.5

      \[\leadsto \frac{\tan x + \tan \varepsilon}{{1}^{3} - {\color{blue}{\left(\frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)}}^{3}} \cdot (\left(\tan \varepsilon \cdot \tan x\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_* - \tan x\]

    11. Applied cube-div0.5

      \[\leadsto \frac{\tan x + \tan \varepsilon}{{1}^{3} - \color{blue}{\frac{{\left(\sin x \cdot \tan \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3}}}} \cdot (\left(\tan \varepsilon \cdot \tan x\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_* - \tan x\]
  3. Recombined 3 regimes into one program.

  4. Final simplification0.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -5.956917387507836 \cdot 10^{-06}:\\ \;\;\;\;\frac{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\ \mathbf{elif}\;\varepsilon \le 3.1311107548585422 \cdot 10^{-06}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot (\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \left(\varepsilon + {\varepsilon}^{5} \cdot \frac{2}{15}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left((\left(\tan x\right) \cdot \left(\tan \varepsilon\right) + 1)_*\right) + 1)_* \cdot \frac{\tan \varepsilon + \tan x}{1 - \frac{{\left(\tan \varepsilon \cdot \sin x\right)}^{3}}{{\left(\cos x\right)}^{3}}} - \tan x\\ \end{array}\]

Reproduce

herbie shell --seed 2019002 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))

Details

Time bar (total: 56.2s)Debug log

sample472.0ms

Algorithm
intervals

simplify4.0ms

Counts
1 → 1
Calls

1 calls. Slowest were:

4.0ms
(- (tan (+ x eps)) (tan x))

prune5.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 35.3b

localize18.0ms

Local error

Found 2 expressions with local error:

3.3b
(tan (+ x eps))
1.1b
(- (tan (+ x eps)) (tan x))

rewrite16.0ms

Algorithm
rewrite-expression-head
Counts
2 → 41
Calls

2 calls. Slowest were:

12.0ms
(- (tan (+ x eps)) (tan x))
3.0ms
(tan (+ x eps))

series187.0ms

Counts
2 → 6
Calls

2 calls. Slowest were:

100.0ms
(- (tan (+ x eps)) (tan x))
87.0ms
(tan (+ x eps))

simplify1.2s

Counts
35 → 47
Calls

35 calls. Slowest were:

286.0ms
(+ (* x (pow eps 2)) (+ eps (* (pow x 2) eps)))
192.0ms
(- (* (+ (tan x) (tan eps)) (cos x)) (* (- 1 (* (tan x) (tan eps))) (sin x)))
179.0ms
(* (- 1 (* (tan x) (tan eps))) (cos x))

prune535.0ms

Pruning

8 alts after pruning (8 fresh and 0 done)

Merged error: 14.0b

localize33.0ms

Local error

Found 4 expressions with local error:

2.6b
(- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))
0.2b
(* (tan x) (tan eps))
0.1b
(/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))
0.1b
(+ (tan x) (tan eps))

rewrite85.0ms

Algorithm
rewrite-expression-head
Counts
4 → 168
Calls

4 calls. Slowest were:

39.0ms
(- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))
25.0ms
(/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))
8.0ms
(* (tan x) (tan eps))

series913.0ms

Counts
4 → 12
Calls

4 calls. Slowest were:

458.0ms
(- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x))
213.0ms
(/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps))))
126.0ms
(+ (tan x) (tan eps))
115.0ms
(* (tan x) (tan eps))

simplify15.3s

Counts
199 → 180
Calls

199 calls. Slowest were:

827.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan x) (tan eps)))) (cbrt (- 1 (* (tan x) (tan eps)))))) (/ (+ (tan x) (tan eps)) (cbrt (- 1 (* (tan x) (tan eps))))) (- (* (cbrt (tan x)) (* (cbrt (tan x)) (cbrt (tan x))))))
509.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan x) (tan eps)))) (cbrt (- 1 (* (tan x) (tan eps)))))) (/ (+ (tan x) (tan eps)) (cbrt (- 1 (* (tan x) (tan eps))))) (- (* (sqrt (tan x)) (sqrt (tan x)))))
486.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan x) (tan eps)))) (cbrt (- 1 (* (tan x) (tan eps)))))) (/ (+ (tan x) (tan eps)) (cbrt (- 1 (* (tan x) (tan eps))))) (- (* (sqrt (tan x)) (sqrt (tan x)))))

prune1.9s

Pruning

15 alts after pruning (15 fresh and 0 done)

Merged error: 13.9b

localize56.0ms

Local error

Found 4 expressions with local error:

2.6b
(- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (fma (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1) 1)) (tan x))
0.3b
(pow (* (tan x) (tan eps)) 3)
0.2b
(* (tan x) (tan eps))
0.2b
(* (tan eps) (tan x))

rewrite23.0ms

Algorithm
rewrite-expression-head
Counts
4 → 88
Calls

4 calls. Slowest were:

11.0ms
(- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (fma (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1) 1)) (tan x))
4.0ms
(* (tan x) (tan eps))
4.0ms
(* (tan eps) (tan x))

series1.5s

Counts
4 → 12
Calls

4 calls. Slowest were:

1.2s
(- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (fma (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1) 1)) (tan x))
139.0ms
(pow (* (tan x) (tan eps)) 3)
107.0ms
(* (tan eps) (tan x))
101.0ms
(* (tan x) (tan eps))

simplify4.5s

Counts
59 → 100
Calls

59 calls. Slowest were:

584.0ms
(fma (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (fma (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1) 1) (- (* (sqrt (tan x)) (sqrt (tan x)))))
422.0ms
(fma (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (fma (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1) 1) (- (* (cbrt (tan x)) (* (cbrt (tan x)) (cbrt (tan x))))))
405.0ms
(fma (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (fma (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1) 1) (- (* (tan x) 1)))

prune1.5s

Pruning

11 alts after pruning (11 fresh and 0 done)

Merged error: 12.0b

localize21.0ms

Local error

Found 4 expressions with local error:

2.7b
(- (* 1 (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3)))) (tan x))
0.3b
(* (* (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1)) (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))))
0.3b
(pow (* (tan x) (tan eps)) 3)
0.3b
(pow (* (tan x) (tan eps)) 3)

rewrite66.0ms

Algorithm
rewrite-expression-head
Counts
4 → 133
Calls

4 calls. Slowest were:

40.0ms
(* (* (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1)) (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))))
14.0ms
(- (* 1 (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3)))) (tan x))
6.0ms
(pow (* (tan x) (tan eps)) 3)

series1.1s

Counts
4 → 12
Calls

4 calls. Slowest were:

464.0ms
(- (* 1 (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3)))) (tan x))
436.0ms
(* (* (* (tan eps) (tan x)) (fma (tan x) (tan eps) 1)) (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))))
120.0ms
(pow (* (tan x) (tan eps)) 3)
107.0ms
(pow (* (tan x) (tan eps)) 3)

simplify14.1s

Counts
104 → 145
Calls

104 calls. Slowest were:

664.0ms
(* (* (* (tan eps) (sin x)) (fma (tan x) (tan eps) 1)) (+ (tan x) (tan eps)))
391.0ms
(+ (* (pow 1 3) (pow 1 3)) (+ (* (pow (* (tan x) (tan eps)) 3) (pow (* (tan x) (tan eps)) 3)) (* (pow 1 3) (pow (* (tan x) (tan eps)) 3))))
353.0ms
(* (* (* (sin eps) (sin x)) (fma (tan x) (tan eps) 1)) (+ (tan x) (tan eps)))

prune1.7s

Pruning

10 alts after pruning (10 fresh and 0 done)

Merged error: 0.1b

regimes168.0ms

Accuracy

99.1% (0.2b remaining)

Error of 0.3b against oracle of 0.2b and baseline of 19.7b

bsearch363.0ms

end0.0ms

sample10.5s

Algorithm
intervals