Average Error: 25.7 → 1.7
Time: 44.6s
Precision: 64
Internal Precision: 384
\[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
↓
\[\begin{array}{l} \mathbf{if}\;\frac{1}{\sqrt{c^2 + d^2}^*} \cdot \left(\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} - \frac{a}{\sqrt{\sqrt{c^2 + d^2}^*}} \cdot \frac{d}{\sqrt{\sqrt{c^2 + d^2}^*}}\right) \le -4.057114789023461 \cdot 10^{-127}:\\ \;\;\;\;\frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}} + \frac{\frac{-a}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{d}}\\ \mathbf{if}\;\frac{1}{\sqrt{c^2 + d^2}^*} \cdot \left(\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} - \frac{a}{\sqrt{\sqrt{c^2 + d^2}^*}} \cdot \frac{d}{\sqrt{\sqrt{c^2 + d^2}^*}}\right) \le 1.3673325635416466 \cdot 10^{+297}:\\ \;\;\;\;\frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}} + \frac{\frac{-a}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{d}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}} + \frac{\frac{-a}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{d}}\\ \end{array}\]

Error

Bits error versus a

Bits error versus b

Bits error versus c

Bits error versus d

Target

Original25.7
Target0.5
Herbie1.7
\[\begin{array}{l} \mathbf{if}\;\left|d\right| \lt \left|c\right|:\\ \;\;\;\;\frac{b - a \cdot \frac{d}{c}}{c + d \cdot \frac{d}{c}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(-a\right) + b \cdot \frac{c}{d}}{d + c \cdot \frac{c}{d}}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if (* (/ 1 (hypot c d)) (- (/ (* c b) (hypot c d)) (* (/ a (sqrt (hypot c d))) (/ d (sqrt (hypot c d)))))) < -4.057114789023461e-127 or 1.3673325635416466e+297 < (* (/ 1 (hypot c d)) (- (/ (* c b) (hypot c d)) (* (/ a (sqrt (hypot c d))) (/ d (sqrt (hypot c d))))))

    1. Initial program 34.6

      \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt34.6

      \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}}\]

    4. Applied *-un-lft-identity34.6

      \[\leadsto \frac{\color{blue}{1 \cdot \left(b \cdot c - a \cdot d\right)}}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}\]

    5. Applied times-frac34.6

      \[\leadsto \color{blue}{\frac{1}{\sqrt{c \cdot c + d \cdot d}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}\]

    6. Applied simplify34.6

      \[\leadsto \color{blue}{\frac{1}{\sqrt{c^2 + d^2}^*}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}\]

    7. Applied simplify31.0

      \[\leadsto \frac{1}{\sqrt{c^2 + d^2}^*} \cdot \color{blue}{\frac{c \cdot b - a \cdot d}{\sqrt{c^2 + d^2}^*}}\]
    8. Using strategy rm

    9. Applied div-sub31.0

      \[\leadsto \frac{1}{\sqrt{c^2 + d^2}^*} \cdot \color{blue}{\left(\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} - \frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right)}\]
    10. Using strategy rm

    11. Applied sub-neg31.0

      \[\leadsto \frac{1}{\sqrt{c^2 + d^2}^*} \cdot \color{blue}{\left(\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} + \left(-\frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right)\right)}\]

    12. Applied distribute-rgt-in31.0

      \[\leadsto \color{blue}{\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} \cdot \frac{1}{\sqrt{c^2 + d^2}^*} + \left(-\frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right) \cdot \frac{1}{\sqrt{c^2 + d^2}^*}}\]

    13. Applied simplify11.6

      \[\leadsto \color{blue}{\frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}}} + \left(-\frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right) \cdot \frac{1}{\sqrt{c^2 + d^2}^*}\]

    14. Applied simplify1.7

      \[\leadsto \frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}} + \color{blue}{\frac{\frac{-a}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{d}}}\]

    if -4.057114789023461e-127 < (* (/ 1 (hypot c d)) (- (/ (* c b) (hypot c d)) (* (/ a (sqrt (hypot c d))) (/ d (sqrt (hypot c d)))))) < 1.3673325635416466e+297

    1. Initial program 20.4

      \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt20.4

      \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}}\]

    4. Applied *-un-lft-identity20.4

      \[\leadsto \frac{\color{blue}{1 \cdot \left(b \cdot c - a \cdot d\right)}}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}\]

    5. Applied times-frac20.4

      \[\leadsto \color{blue}{\frac{1}{\sqrt{c \cdot c + d \cdot d}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}\]

    6. Applied simplify20.4

      \[\leadsto \color{blue}{\frac{1}{\sqrt{c^2 + d^2}^*}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}\]

    7. Applied simplify8.0

      \[\leadsto \frac{1}{\sqrt{c^2 + d^2}^*} \cdot \color{blue}{\frac{c \cdot b - a \cdot d}{\sqrt{c^2 + d^2}^*}}\]
    8. Using strategy rm

    9. Applied div-sub8.0

      \[\leadsto \frac{1}{\sqrt{c^2 + d^2}^*} \cdot \color{blue}{\left(\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} - \frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right)}\]
    10. Using strategy rm

    11. Applied sub-neg8.0

      \[\leadsto \frac{1}{\sqrt{c^2 + d^2}^*} \cdot \color{blue}{\left(\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} + \left(-\frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right)\right)}\]

    12. Applied distribute-rgt-in8.0

      \[\leadsto \color{blue}{\frac{c \cdot b}{\sqrt{c^2 + d^2}^*} \cdot \frac{1}{\sqrt{c^2 + d^2}^*} + \left(-\frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right) \cdot \frac{1}{\sqrt{c^2 + d^2}^*}}\]

    13. Applied simplify8.5

      \[\leadsto \color{blue}{\frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}}} + \left(-\frac{a \cdot d}{\sqrt{c^2 + d^2}^*}\right) \cdot \frac{1}{\sqrt{c^2 + d^2}^*}\]

    14. Applied simplify1.6

      \[\leadsto \frac{\frac{c}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{b}} + \color{blue}{\frac{\frac{-a}{\sqrt{c^2 + d^2}^*}}{\frac{\sqrt{c^2 + d^2}^*}{d}}}\]
  3. Recombined 2 regimes into one program.

Runtime

Time bar (total: 44.6s)Debug logProfile

herbie shell --seed '#(1064173506 2580572819 2847706409 4129882574 1125180799 1845288547)' +o rules:numerics
(FPCore (a b c d)
  :name "Complex division, imag part"

  :herbie-target
  (if (< (fabs d) (fabs c)) (/ (- b (* a (/ d c))) (+ c (* d (/ d c)))) (/ (+ (- a) (* b (/ c d))) (+ d (* c (/ c d)))))

  (/ (- (* b c) (* a d)) (+ (* c c) (* d d))))