Average Error: 0.8 → 0.7
Time: 1.8m
Precision: 64
Internal precision: 384
\[\left(\left(\left(\left(\left(\left(x1 \cdot x4\right) \cdot \left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x2 \cdot \left(\left(\left(x1 - x2\right) + x3\right) + x4\right)\right) + x3 \cdot \left(\left(\left(x1 + x2\right) - x3\right) + x4\right)\right) - \left(x2 \cdot x3\right) \cdot x4\right) - x1 \cdot x3\right) - x1 \cdot x2\right) - x4\]
⬇
\[\log \left(\left(e^{\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right)} \cdot e^{\left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3}\right) \cdot \frac{e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}}{e^{\left(x2 + x3\right) \cdot x1}}\right) - x4\]

Error

Bits error versus x1

Bits error versus x2

Bits error versus x3

Bits error versus x4

Derivation

  1. Initial program 0.8

    \[\left(\left(\left(\left(\left(\left(x1 \cdot x4\right) \cdot \left(\left(\left(\left(-x1\right) + x2\right) + x3\right) - x4\right) + x2 \cdot \left(\left(\left(x1 - x2\right) + x3\right) + x4\right)\right) + x3 \cdot \left(\left(\left(x1 + x2\right) - x3\right) + x4\right)\right) - \left(x2 \cdot x3\right) \cdot x4\right) - x1 \cdot x3\right) - x1 \cdot x2\right) - x4\]

  2. Applied simplify 0.8

    \[\leadsto \color{blue}{\left(\left(\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right) + \left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3\right) + \left(x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right) - \left(x2 + x3\right) \cdot x1\right)\right) - x4}\]
  3. Using strategy rm

  4. Applied add-log-exp 0.8

    \[\leadsto \left(\left(\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right) + \left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3\right) + \left(x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right) - \color{blue}{\log \left(e^{\left(x2 + x3\right) \cdot x1}\right)}\right)\right) - x4\]

  5. Applied add-log-exp 0.8

    \[\leadsto \left(\left(\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right) + \left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3\right) + \left(\color{blue}{\log \left(e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}\right)} - \log \left(e^{\left(x2 + x3\right) \cdot x1}\right)\right)\right) - x4\]

  6. Applied diff-log 0.8

    \[\leadsto \left(\left(\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right) + \left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3\right) + \color{blue}{\log \left(\frac{e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}}{e^{\left(x2 + x3\right) \cdot x1}}\right)}\right) - x4\]

  7. Applied add-log-exp 0.8

    \[\leadsto \left(\left(\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right) + \color{blue}{\log \left(e^{\left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3}\right)}\right) + \log \left(\frac{e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}}{e^{\left(x2 + x3\right) \cdot x1}}\right)\right) - x4\]

  8. Applied add-log-exp 0.8

    \[\leadsto \left(\left(\color{blue}{\log \left(e^{\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right)}\right)} + \log \left(e^{\left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3}\right)\right) + \log \left(\frac{e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}}{e^{\left(x2 + x3\right) \cdot x1}}\right)\right) - x4\]

  9. Applied sum-log 0.8

    \[\leadsto \left(\color{blue}{\log \left(e^{\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right)} \cdot e^{\left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3}\right)} + \log \left(\frac{e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}}{e^{\left(x2 + x3\right) \cdot x1}}\right)\right) - x4\]

  10. Applied sum-log 0.7

    \[\leadsto \color{blue}{\log \left(\left(e^{\left(x2 + \left(\left(-x1\right) + \left(x3 - x4\right)\right)\right) \cdot \left(x4 \cdot x1\right)} \cdot e^{\left(\left(x2 + x1\right) - \left(x3 - x4\right)\right) \cdot x3}\right) \cdot \frac{e^{x2 \cdot \left(\left(x1 - x2\right) + \left(\left(x3 + x4\right) - x3 \cdot x4\right)\right)}}{e^{\left(x2 + x3\right) \cdot x1}}\right)} - x4\]
  11. Removed slow pow expressions

Runtime

Time bar (total: 1.8m) Debug log

Please include this information when filing a bug report:

herbie shell --seed '#(3052192724 3812927732 3686175817 630908657 2373248591 511094450)'
(FPCore (x1 x2 x3 x4)
  :name "kepler1"
  :pre (and (<= 4 x1 6.36) (<= 4 x2 6.36) (<= 4 x3 6.36) (<= 4 x4 6.36))
  (- (- (- (- (+ (+ (* (* x1 x4) (- (+ (+ (- x1) x2) x3) x4)) (* x2 (+ (+ (- x1 x2) x3) x4))) (* x3 (+ (- (+ x1 x2) x3) x4))) (* (* x2 x3) x4)) (* x1 x3)) (* x1 x2)) x4))