(FPCore (x y z t a) :precision binary64 (+ x (/ (* (- y x) (- z t)) (- a t))))
↓
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (+ x (* (- z t) (* (- y x) (/ 1.0 (- a t))))))
(t_2 (+ x (/ (* (- y x) (- z t)) (- a t)))))
(if (<= t_2 (- INFINITY))
t_1
(if (<= t_2 -1e-300)
t_2
(if (<= t_2 0.0)
(- y (* x (/ (- a z) t)))
(if (<= t_2 2e+290) t_2 t_1))))))
double code(double x, double y, double z, double t, double a) {
return x + (((y - x) * (z - t)) / (a - t));
}
↓
double code(double x, double y, double z, double t, double a) {
double t_1 = x + ((z - t) * ((y - x) * (1.0 / (a - t))));
double t_2 = x + (((y - x) * (z - t)) / (a - t));
double tmp;
if (t_2 <= -((double) INFINITY)) {
tmp = t_1;
} else if (t_2 <= -1e-300) {
tmp = t_2;
} else if (t_2 <= 0.0) {
tmp = y - (x * ((a - z) / t));
} else if (t_2 <= 2e+290) {
tmp = t_2;
} else {
tmp = t_1;
}
return tmp;
}
public static double code(double x, double y, double z, double t, double a) {
return x + (((y - x) * (z - t)) / (a - t));
}
↓
public static double code(double x, double y, double z, double t, double a) {
double t_1 = x + ((z - t) * ((y - x) * (1.0 / (a - t))));
double t_2 = x + (((y - x) * (z - t)) / (a - t));
double tmp;
if (t_2 <= -Double.POSITIVE_INFINITY) {
tmp = t_1;
} else if (t_2 <= -1e-300) {
tmp = t_2;
} else if (t_2 <= 0.0) {
tmp = y - (x * ((a - z) / t));
} else if (t_2 <= 2e+290) {
tmp = t_2;
} else {
tmp = t_1;
}
return tmp;
}
def code(x, y, z, t, a):
return x + (((y - x) * (z - t)) / (a - t))
if (+.f64 x (/.f64 (*.f64 (-.f64 y x) (-.f64 z t)) (-.f64 a t))) < -inf.0 or 2.00000000000000012e290 < (+.f64 x (/.f64 (*.f64 (-.f64 y x) (-.f64 z t)) (-.f64 a t)))
if -inf.0 < (+.f64 x (/.f64 (*.f64 (-.f64 y x) (-.f64 z t)) (-.f64 a t))) < -1.00000000000000003e-300 or 0.0 < (+.f64 x (/.f64 (*.f64 (-.f64 y x) (-.f64 z t)) (-.f64 a t))) < 2.00000000000000012e290
(-.f64 y (*.f64 (/.f64 (-.f64 y x) t) (-.f64 z a))): 0 points increase in error, 0 points decrease in error
(-.f64 y (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 y x) (/.f64 t (-.f64 z a))))): 31 points increase in error, 26 points decrease in error
(-.f64 y (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 y x) (-.f64 z a)) t))): 45 points increase in error, 33 points decrease in error
(-.f64 y (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 z (-.f64 y x)) (*.f64 a (-.f64 y x)))) t)): 0 points increase in error, 1 points decrease in error
(-.f64 y (/.f64 (-.f64 (Rewrite=> *-commutative_binary64 (*.f64 (-.f64 y x) z)) (*.f64 a (-.f64 y x))) t)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 y (neg.f64 (/.f64 (-.f64 (*.f64 (-.f64 y x) z) (*.f64 a (-.f64 y x))) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 (-.f64 y x) z) (*.f64 a (-.f64 y x))) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 (-.f64 y x) z) t) (/.f64 (*.f64 a (-.f64 y x)) t))))): 0 points increase in error, 0 points decrease in error
(+.f64 y (*.f64 -1 (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 z (-.f64 y x))) t) (/.f64 (*.f64 a (-.f64 y x)) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 y (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t)) (*.f64 -1 (/.f64 (*.f64 a (-.f64 y x)) t))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 y (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t))) (*.f64 -1 (/.f64 (*.f64 a (-.f64 y x)) t)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 z (-.f64 y x)) t)) y)) (*.f64 -1 (/.f64 (*.f64 a (-.f64 y x)) t))): 0 points increase in error, 0 points decrease in error
\[\leadsto y - \color{blue}{x \cdot \frac{a - z}{t}}
\]
Proof
(*.f64 x (/.f64 (-.f64 a z) t)): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite=> div-sub_binary64 (-.f64 (/.f64 a t) (/.f64 z t)))): 1 points increase in error, 3 points decrease in error
(*.f64 x (Rewrite=> sub-neg_binary64 (+.f64 (/.f64 a t) (neg.f64 (/.f64 z t))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 a t)))) (neg.f64 (/.f64 z t)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 (/.f64 a t)) (/.f64 z t))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 z t) (neg.f64 (/.f64 a t)))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 z t) (/.f64 a t))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (neg.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 z a) t)))): 3 points increase in error, 1 points decrease in error
(*.f64 x (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 z a) t)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 z a) t) -1))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 z a) (/.f64 t -1)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 x (-.f64 z a)) (/.f64 t -1))): 46 points increase in error, 38 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 z a) x)) (/.f64 t -1)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (*.f64 (-.f64 z a) x) t) -1)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 z a) x) t))): 0 points increase in error, 0 points decrease in error
herbie shell --seed 2022300
(FPCore (x y z t a)
:name "Graphics.Rendering.Chart.Axis.Types:linMap from Chart-1.5.3"
:precision binary64
:herbie-target
(if (< a -1.6153062845442575e-142) (+ x (* (/ (- y x) 1.0) (/ (- z t) (- a t)))) (if (< a 3.774403170083174e-182) (- y (* (/ z t) (- y x))) (+ x (* (/ (- y x) 1.0) (/ (- z t) (- a t))))))
(+ x (/ (* (- y x) (- z t)) (- a t))))