?

Average Accuracy: 99.9% → 100.0%
Time: 5.0s
Precision: binary64
Cost: 6720

?

\[x + \frac{x - y}{2} \]
\[\mathsf{fma}\left(x, 1.5, -0.5 \cdot y\right) \]
(FPCore (x y) :precision binary64 (+ x (/ (- x y) 2.0)))
(FPCore (x y) :precision binary64 (fma x 1.5 (* -0.5 y)))
double code(double x, double y) {
	return x + ((x - y) / 2.0);
}
double code(double x, double y) {
	return fma(x, 1.5, (-0.5 * y));
}
function code(x, y)
	return Float64(x + Float64(Float64(x - y) / 2.0))
end
function code(x, y)
	return fma(x, 1.5, Float64(-0.5 * y))
end
code[x_, y_] := N[(x + N[(N[(x - y), $MachinePrecision] / 2.0), $MachinePrecision]), $MachinePrecision]
code[x_, y_] := N[(x * 1.5 + N[(-0.5 * y), $MachinePrecision]), $MachinePrecision]
x + \frac{x - y}{2}
\mathsf{fma}\left(x, 1.5, -0.5 \cdot y\right)

Error?

Target

Original99.9%
Target99.9%
Herbie100.0%
\[1.5 \cdot x - 0.5 \cdot y \]

Derivation?

  1. Initial program 99.9%

    \[x + \frac{x - y}{2} \]
  2. Simplified99.9%

    \[\leadsto \color{blue}{\mathsf{fma}\left(y, -0.5, x \cdot 1.5\right)} \]
    Proof

    [Start]99.9

    \[ x + \frac{x - y}{2} \]

    div-sub [=>]99.9

    \[ x + \color{blue}{\left(\frac{x}{2} - \frac{y}{2}\right)} \]

    associate-+r- [=>]99.9

    \[ \color{blue}{\left(x + \frac{x}{2}\right) - \frac{y}{2}} \]

    sub-neg [=>]99.9

    \[ \color{blue}{\left(x + \frac{x}{2}\right) + \left(-\frac{y}{2}\right)} \]

    +-commutative [=>]99.9

    \[ \color{blue}{\left(-\frac{y}{2}\right) + \left(x + \frac{x}{2}\right)} \]

    distribute-neg-frac [=>]99.9

    \[ \color{blue}{\frac{-y}{2}} + \left(x + \frac{x}{2}\right) \]

    neg-mul-1 [=>]99.9

    \[ \frac{\color{blue}{-1 \cdot y}}{2} + \left(x + \frac{x}{2}\right) \]

    associate-/l* [=>]99.7

    \[ \color{blue}{\frac{-1}{\frac{2}{y}}} + \left(x + \frac{x}{2}\right) \]

    associate-/r/ [=>]99.9

    \[ \color{blue}{\frac{-1}{2} \cdot y} + \left(x + \frac{x}{2}\right) \]

    *-commutative [=>]99.9

    \[ \color{blue}{y \cdot \frac{-1}{2}} + \left(x + \frac{x}{2}\right) \]

    fma-def [=>]99.9

    \[ \color{blue}{\mathsf{fma}\left(y, \frac{-1}{2}, x + \frac{x}{2}\right)} \]

    metadata-eval [=>]99.9

    \[ \mathsf{fma}\left(y, \color{blue}{-0.5}, x + \frac{x}{2}\right) \]

    remove-double-neg [<=]99.9

    \[ \mathsf{fma}\left(y, -0.5, \color{blue}{\left(-\left(-x\right)\right)} + \frac{x}{2}\right) \]

    neg-mul-1 [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, \color{blue}{-1 \cdot \left(-x\right)} + \frac{x}{2}\right) \]

    remove-double-neg [<=]99.9

    \[ \mathsf{fma}\left(y, -0.5, -1 \cdot \left(-x\right) + \frac{\color{blue}{-\left(-x\right)}}{2}\right) \]

    neg-mul-1 [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, -1 \cdot \left(-x\right) + \frac{\color{blue}{-1 \cdot \left(-x\right)}}{2}\right) \]

    associate-/l* [=>]99.8

    \[ \mathsf{fma}\left(y, -0.5, -1 \cdot \left(-x\right) + \color{blue}{\frac{-1}{\frac{2}{-x}}}\right) \]

    associate-/r/ [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, -1 \cdot \left(-x\right) + \color{blue}{\frac{-1}{2} \cdot \left(-x\right)}\right) \]

    distribute-rgt-out [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, \color{blue}{\left(-x\right) \cdot \left(-1 + \frac{-1}{2}\right)}\right) \]

    distribute-lft-neg-in [<=]99.9

    \[ \mathsf{fma}\left(y, -0.5, \color{blue}{-x \cdot \left(-1 + \frac{-1}{2}\right)}\right) \]

    distribute-rgt-neg-in [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, \color{blue}{x \cdot \left(-\left(-1 + \frac{-1}{2}\right)\right)}\right) \]

    metadata-eval [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, x \cdot \left(-\left(-1 + \color{blue}{-0.5}\right)\right)\right) \]

    metadata-eval [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, x \cdot \left(-\color{blue}{-1.5}\right)\right) \]

    metadata-eval [=>]99.9

    \[ \mathsf{fma}\left(y, -0.5, x \cdot \color{blue}{1.5}\right) \]
  3. Taylor expanded in y around 0 99.9%

    \[\leadsto \color{blue}{-0.5 \cdot y + 1.5 \cdot x} \]
  4. Simplified100.0%

    \[\leadsto \color{blue}{\mathsf{fma}\left(x, 1.5, -0.5 \cdot y\right)} \]
    Proof

    [Start]99.9

    \[ -0.5 \cdot y + 1.5 \cdot x \]

    +-commutative [=>]99.9

    \[ \color{blue}{1.5 \cdot x + -0.5 \cdot y} \]

    *-commutative [=>]99.9

    \[ \color{blue}{x \cdot 1.5} + -0.5 \cdot y \]

    *-commutative [=>]99.9

    \[ x \cdot 1.5 + \color{blue}{y \cdot -0.5} \]

    fma-def [=>]100.0

    \[ \color{blue}{\mathsf{fma}\left(x, 1.5, y \cdot -0.5\right)} \]

    *-commutative [<=]100.0

    \[ \mathsf{fma}\left(x, 1.5, \color{blue}{-0.5 \cdot y}\right) \]
  5. Final simplification100.0%

    \[\leadsto \mathsf{fma}\left(x, 1.5, -0.5 \cdot y\right) \]

Alternatives

Alternative 1
Accuracy75.7%
Cost456
\[\begin{array}{l} \mathbf{if}\;y \leq -1.7 \cdot 10^{+46}:\\ \;\;\;\;-0.5 \cdot y\\ \mathbf{elif}\;y \leq 3.1 \cdot 10^{+43}:\\ \;\;\;\;x \cdot 1.5\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot y\\ \end{array} \]
Alternative 2
Accuracy99.9%
Cost448
\[x + \frac{x - y}{2} \]
Alternative 3
Accuracy51.1%
Cost192
\[-0.5 \cdot y \]

Error

Reproduce?

herbie shell --seed 2023151 
(FPCore (x y)
  :name "Graphics.Rendering.Chart.Axis.Types:hBufferRect from Chart-1.5.3"
  :precision binary64

  :herbie-target
  (- (* 1.5 x) (* 0.5 y))

  (+ x (/ (- x y) 2.0)))