fabs fraction 1

Average Accuracy: 97.6% → 99.5%

Time: 11.4s

Precision: binary64

Cost: 7752

Math

\[\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right) \]

↓

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{+.f64}\left(x, 4\right), -500000000000000028883304949057948351218633563548032068549020931617356167008462307328\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{+.f64}\left(x, 4\right), 5\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, \mathsf{+.f64}\left(-1, z\right)\right), y\right), \mathsf{*.f64}\left(4, \mathsf{/.f64}\left(-1, y\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right)\\ \end{array} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (fabs.f64 (-.f64 (/.f64 (+.f64 x 4) y) (*.f64 (/.f64 x y) z))))

↓

(FPCore (x y z)
 :precision binary64
 (if (<=.f64
      (+.f64 x 4)
      -500000000000000028883304949057948351218633563548032068549020931617356167008462307328)
   (fabs.f64 (*.f64 (/.f64 x y) (+.f64 -1 z)))
   (if (<=.f64 (+.f64 x 4) 5)
     (fabs.f64 (+.f64 (/.f64 (*.f64 x (+.f64 -1 z)) y) (*.f64 4 (/.f64 -1 y))))
     (fabs.f64 (-.f64 (/.f64 (+.f64 x 4) y) (*.f64 (/.f64 x y) z))))))

Derivation

1. Split input into 3 regimes

2. if (+.f64 x 4) < -5.00000000000000029e83

   1. Initial program 99.8%

      \[\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right) \]

   2. Simplified 99.8%

      \[\leadsto \color{blue}{\mathsf{fabs.f64}\left(\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(-4, x\right), y\right)\right)\right)} \]
      Proof

      [Start] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right) \]
      fabs-sub [=>] 99.8	\[ \color{blue}{\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right)} \]
      associate-*l/ [=>] 81.4	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, z\right), y\right)}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right) \]
      *-commutative [=>] 81.4	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(z, x\right)}, y\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right) \]
      associate-*l/ [<=] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right) \]
      *-commutative [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(z, y\right)\right)}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right) \]
      fma-neg [=>] 99.8	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right)}\right) \]
      distribute-neg-frac [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(x, 4\right)\right), y\right)}\right)\right) \]
      +-commutative [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(\color{blue}{\mathsf{+.f64}\left(4, x\right)}\right), y\right)\right)\right) \]
      distribute-neg-in [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(4\right), \mathsf{neg.f64}\left(x\right)\right)}, y\right)\right)\right) \]
      unsub-neg [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(4\right), x\right)}, y\right)\right)\right) \]
      metadata-eval [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{fma.f64}\left(x, \mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{-4}, x\right), y\right)\right)\right) \]

   3. Taylor expanded in x around inf 99.6%

      \[\leadsto \mathsf{fabs.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(1, y\right)\right), x\right)}\right) \]

   4. Simplified 99.8%

      \[\leadsto \mathsf{fabs.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)}\right) \]
      Proof

      [Start] 99.6	\[ \mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(1, y\right)\right), x\right)\right) \]
      *-commutative [=>] 99.6	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{*.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{/.f64}\left(z, y\right), \mathsf{/.f64}\left(1, y\right)\right)\right)}\right) \]
      sub-neg [=>] 99.6	\[ \mathsf{fabs.f64}\left(\mathsf{*.f64}\left(x, \color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(z, y\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(1, y\right)\right)\right)}\right)\right) \]
      +-commutative [=>] 99.6	\[ \mathsf{fabs.f64}\left(\mathsf{*.f64}\left(x, \color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(1, y\right)\right), \mathsf{/.f64}\left(z, y\right)\right)}\right)\right) \]
      distribute-rgt-out [<=] 99.6	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(1, y\right)\right), x\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)\right)}\right) \]
      distribute-neg-frac [=>] 99.6	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(1\right), y\right)}, x\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)\right)\right) \]
      metadata-eval [=>] 99.6	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\color{blue}{-1}, y\right), x\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)\right)\right) \]
      associate-*l/ [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, x\right), y\right)}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)\right)\right) \]
      associate-*r/ [<=] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(x, y\right)\right)}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)\right)\right) \]
      *-commutative [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), -1\right)}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(z, y\right), x\right)\right)\right) \]
      *-commutative [<=] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), -1\right), \color{blue}{\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(z, y\right)\right)}\right)\right) \]
      associate-*r/ [=>] 81.4	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), -1\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, z\right), y\right)}\right)\right) \]
      associate-/l* [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), -1\right), \color{blue}{\mathsf{/.f64}\left(x, \mathsf{/.f64}\left(y, z\right)\right)}\right)\right) \]
      associate-/r/ [=>] 99.8	\[ \mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), -1\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)}\right)\right) \]
      distribute-lft-out [=>] 99.8	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)}\right) \]

   if -5.00000000000000029e83 < (+.f64 x 4) < 5

   1. Initial program 96.6%

      \[\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right) \]

   2. Simplified 99.4%

      \[\leadsto \color{blue}{\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, y\right), \mathsf{fma.f64}\left(x, z, \mathsf{\_.f64}\left(-4, x\right)\right)\right)\right)} \]
      Proof

      [Start] 96.6	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right) \]
      *-rgt-identity [<=] 96.6	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right), 1\right)} \]
      fabs-sub [=>] 96.6	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right)}, 1\right) \]
      metadata-eval [<=] 96.6	\[ \mathsf{*.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right), \color{blue}{\mathsf{fabs.f64}\left(1\right)}\right) \]
      metadata-eval [<=] 96.6	\[ \mathsf{*.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right), \mathsf{fabs.f64}\left(\color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      fabs-mul [<=] 96.6	\[ \color{blue}{\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right), \mathsf{neg.f64}\left(-1\right)\right)\right)} \]
      metadata-eval [=>] 96.6	\[ \mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right), \color{blue}{1}\right)\right) \]
      *-rgt-identity [=>] 96.6	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)}\right) \]
      associate-*l/ [=>] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, z\right), y\right)}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\right)\right) \]
      div-sub [<=] 99.4	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(x, z\right), \mathsf{+.f64}\left(x, 4\right)\right), y\right)}\right) \]
      sub-neg [=>] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(x, z\right), \mathsf{neg.f64}\left(\mathsf{+.f64}\left(x, 4\right)\right)\right)}, y\right)\right) \]
      +-commutative [<=] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(x, 4\right)\right), \mathsf{*.f64}\left(x, z\right)\right)}, y\right)\right) \]
      remove-double-neg [<=] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(x, 4\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, z\right)\right)\right)}\right), y\right)\right) \]
      distribute-neg-in [<=] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, z\right)\right)\right)\right)}, y\right)\right) \]
      sub-neg [<=] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right)}\right), y\right)\right) \]
      neg-mul-1 [=>] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right)\right)}, y\right)\right) \]
      associate-*l/ [<=] 99.4	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(-1, y\right), \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right)\right)}\right) \]
      remove-double-neg [<=] 99.4	\[ \mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(-1, y\right)\right)\right)}, \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right)\right)\right) \]
      distribute-lft-neg-in [<=] 99.4	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(-1, y\right)\right), \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right)\right)\right)}\right) \]
      distribute-rgt-neg-in [=>] 99.4	\[ \mathsf{fabs.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(-1, y\right)\right), \mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right)\right)\right)}\right) \]

   3. Taylor expanded in x around inf 99.4%

      \[\leadsto \mathsf{fabs.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{\_.f64}\left(z, 1\right), x\right), y\right), \mathsf{*.f64}\left(4, \mathsf{/.f64}\left(1, y\right)\right)\right)}\right) \]

   if 5 < (+.f64 x 4)

   1. Initial program 99.8%

      \[\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right) \]
3. Recombined 3 regimes into one program.

4. Final simplification 99.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{+.f64}\left(x, 4\right), -500000000000000028883304949057948351218633563548032068549020931617356167008462307328\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{+.f64}\left(x, 4\right), 5\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, \mathsf{+.f64}\left(-1, z\right)\right), y\right), \mathsf{*.f64}\left(4, \mathsf{/.f64}\left(-1, y\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	83.9%
Cost	8402

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -100000000000000004337729697461918607329029332495193931179177378933611681288968111094132375552\right) \lor \neg \left(\mathsf{<=.f64}\left(t_0, -99999999999999996863366107917975552\right) \lor \neg \mathsf{<=.f64}\left(t_0, \frac{-944473296573929}{18889465931478580854784}\right) \land \mathsf{<=.f64}\left(t_0, 200000000000000000\right)\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(-4, x\right), y\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	99.4%
Cost	7881

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right)\\ t_1 := \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -100000000000000004337729697461918607329029332495193931179177378933611681288968111094132375552\right) \lor \neg \mathsf{<=.f64}\left(t_1, 20000000000000000292613904613497460619400859757293101185572215743395927285022964318208\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(t_0, t_1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(t_0, \mathsf{/.f64}\left(\mathsf{*.f64}\left(x, z\right), y\right)\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	99.5%
Cost	7497

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{+.f64}\left(x, 4\right), -500000000000000028883304949057948351218633563548032068549020931617356167008462307328\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{+.f64}\left(x, 4\right), 1000000000000000\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, 4\right), \mathsf{*.f64}\left(x, z\right)\right), y\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	69.2%
Cost	7380

\[\begin{array}{l} t_0 := \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(x, y\right)\right)\\ t_1 := \mathsf{fabs.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(z, y\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(x, -3399999999999999808183241646624835745081690979043936365758462650413778207765556101120\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, -189999999999999991810803399150023465781378521542043050268688384\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, \frac{-21}{2}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, \frac{7737125245533627}{2417851639229258349412352}\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(4, y\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, 13000000000000000545814985068482673153932600755199359587174942412051311805237030304947234573091544492450193241712064887320070451338303251369030072140480643072\right):\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 5
Accuracy	69.2%
Cost	7380

\[\begin{array}{l} t_0 := \mathsf{fabs.f64}\left(\mathsf{/.f64}\left(x, y\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(x, -2700000000000000177537804058633432932314233312775077709074428568766181286728584658944\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, -64999999999999999832268122104098466167637483886642265587712\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(z, y\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, \frac{-2871044762448691}{281474976710656}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, \frac{6189700196426901}{9671406556917033397649408}\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(4, y\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, 14000000000000001291319807458664685733140734210189072737945793450577002600461909955516734622831824083885537823291772513829726814498631617936474019837048258560\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 6
Accuracy	99.7%
Cost	7369

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-578960446186581}{115792089237316195423570985008687907853269984665640564039457584007913129639936}\right) \lor \neg \mathsf{<=.f64}\left(x, \frac{1684996666696915}{1684996666696914987166688442938726917102321526408785780068975640576}\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 4\right), y\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(4, \mathsf{*.f64}\left(x, z\right)\right)\right)\right)\right)\\ \end{array} \]

Alternative 7
Accuracy	98.5%
Cost	7241

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, -80\right) \lor \neg \mathsf{<=.f64}\left(x, 4\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, z\right), y\right), \mathsf{/.f64}\left(4, y\right)\right)\right)\\ \end{array} \]

Alternative 8
Accuracy	98.5%
Cost	7113

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, -80\right) \lor \neg \mathsf{<=.f64}\left(x, \frac{4728779608739021}{1125899906842624}\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(x, y\right), \mathsf{+.f64}\left(-1, z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(4, \mathsf{*.f64}\left(x, z\right)\right), y\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	81.8%
Cost	6984

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(z, -110000000000000011507058562473419478732976770901436004752438097511792917535279055179127954487954226462107988599498470682665928285010969485275828793945096192\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(x, \mathsf{/.f64}\left(y, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(z, 1349999999999999866755350528\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(-4, x\right), y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(z, y\right)\right)\right)\\ \end{array} \]

Alternative 10
Accuracy	70.8%
Cost	6857

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-21}{2}\right) \lor \neg \mathsf{<=.f64}\left(x, 4\right):\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(x, y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(4, y\right)\right)\\ \end{array} \]

Alternative 11
Accuracy	49.4%
Cost	6592

\[\mathsf{fabs.f64}\left(\mathsf{/.f64}\left(4, y\right)\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (x y z)
  :name "fabs fraction 1"
  :precision binary64
  (fabs (- (/ (+ x 4.0) y) (* (/ x y) z))))