(- (- (* (/ vz vx) (- ax dx))) (- (- az dz) (* (/ vz vx) (- ax dx))))

Average Error: 30.5 → 0

Time: 1.9s

Precision: binary64

• could not determine a ground truth for program body

  1. vz = 2.0752281133453581e+170
  2. vx = 1.9022557314603913e+44
  3. ax = 8.835495262651818e-07
  4. dx = 2.4597770320850772e+213
  5. az = -2.6084825868293674e-43
  6. dz = 1.9244547571378957e-41

Math

\[\left(-\frac{vz}{vx} \cdot \left(ax - dx\right)\right) - \left(\left(az - dz\right) - \frac{vz}{vx} \cdot \left(ax - dx\right)\right)\]

↓

\[dz - az\]

Error

Bits error versus vz

Bits error versus vx

Bits error versus ax

Bits error versus dx

Bits error versus az

Bits error versus dz

Derivation

1. Initial program 30.5

   \[\left(-\frac{vz}{vx} \cdot \left(ax - dx\right)\right) - \left(\left(az - dz\right) - \frac{vz}{vx} \cdot \left(ax - dx\right)\right)\]

2. Simplified 0

   \[\leadsto \color{blue}{dz - az}\]

3. Final simplification 0

   \[\leadsto dz - az\]

Reproduce

herbie shell --seed 2020153 
(FPCore (vz vx ax dx az dz)
  :name "(- (- (* (/ vz vx) (- ax dx))) (- (- az dz) (* (/ vz vx) (- ax dx))))"
  :precision binary64
  (- (neg (* (/ vz vx) (- ax dx))) (- (- az dz) (* (/ vz vx) (- ax dx)))))