Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, K

Average Error: 20.7 → 17.9

Time: 21.6s

Precision: 64

Math

\[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]

↓

\[\begin{array}{l} \mathbf{if}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 8.139896335094742174168253426990729793648 \cdot 10^{149}:\\ \;\;\;\;\frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right)}^{3} - {\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)}^{3}\right)}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{6004799503160661}{18014398509481984} \cdot \left(t \cdot z\right)\right)\right) + \left(\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) + \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)\right)} - \frac{\frac{a}{b}}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r620994 = 2.0;
        double r620995 = x;
        double r620996 = sqrt(r620995);
        double r620997 = r620994 * r620996;
        double r620998 = y;
        double r620999 = z;
        double r621000 = t;
        double r621001 = r620999 * r621000;
        double r621002 = 3.0;
        double r621003 = r621001 / r621002;
        double r621004 = r620998 - r621003;
        double r621005 = cos(r621004);
        double r621006 = r620997 * r621005;
        double r621007 = a;
        double r621008 = b;
        double r621009 = r621008 * r621002;
        double r621010 = r621007 / r621009;
        double r621011 = r621006 - r621010;
        return r621011;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r621012 = 2.0;
        double r621013 = x;
        double r621014 = sqrt(r621013);
        double r621015 = r621012 * r621014;
        double r621016 = y;
        double r621017 = z;
        double r621018 = t;
        double r621019 = r621017 * r621018;
        double r621020 = 3.0;
        double r621021 = r621019 / r621020;
        double r621022 = r621016 - r621021;
        double r621023 = cos(r621022);
        double r621024 = r621015 * r621023;
        double r621025 = 8.139896335094742e+149;
        bool r621026 = r621024 <= r621025;
        double r621027 = cos(r621016);
        double r621028 = cos(r621021);
        double r621029 = r621027 * r621028;
        double r621030 = 3.0;
        double r621031 = pow(r621029, r621030);
        double r621032 = sin(r621016);
        double r621033 = -r621021;
        double r621034 = sin(r621033);
        double r621035 = r621032 * r621034;
        double r621036 = pow(r621035, r621030);
        double r621037 = r621031 - r621036;
        double r621038 = r621015 * r621037;
        double r621039 = 6004799503160661.0;
        double r621040 = 18014398509481984.0;
        double r621041 = r621039 / r621040;
        double r621042 = r621018 * r621017;
        double r621043 = r621041 * r621042;
        double r621044 = cos(r621043);
        double r621045 = r621027 * r621044;
        double r621046 = r621029 * r621045;
        double r621047 = r621035 * r621035;
        double r621048 = r621029 * r621035;
        double r621049 = r621047 + r621048;
        double r621050 = r621046 + r621049;
        double r621051 = r621038 / r621050;
        double r621052 = a;
        double r621053 = b;
        double r621054 = r621052 / r621053;
        double r621055 = r621054 / r621020;
        double r621056 = r621051 - r621055;
        double r621057 = 1.0;
        double r621058 = 2.0;
        double r621059 = r621057 / r621058;
        double r621060 = pow(r621016, r621058);
        double r621061 = r621059 * r621060;
        double r621062 = r621057 - r621061;
        double r621063 = r621015 * r621062;
        double r621064 = r621053 * r621020;
        double r621065 = r621052 / r621064;
        double r621066 = r621063 - r621065;
        double r621067 = r621026 ? r621056 : r621066;
        return r621067;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Target

Original	20.7
Target	18.7
Herbie	17.9

\[\begin{array}{l} \mathbf{if}\;z \lt -1.379333748723514136852843173740882251575 \cdot 10^{129}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{elif}\;z \lt 3.516290613555987147199887107423758623887 \cdot 10^{106}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2\right) \cdot \cos \left(y - \frac{t}{3} \cdot z\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(y - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) \cdot \left(2 \cdot \sqrt{x}\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) < 8.139896335094742e+149

   1. Initial program 14.6

      \[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]
   2. Using strategy rm

   3. Applied sub-neg 14.6

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \cos \color{blue}{\left(y + \left(-\frac{z \cdot t}{3}\right)\right)} - \frac{a}{b \cdot 3}\]

   4. Applied cos-sum 14.0

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\cos y \cdot \cos \left(-\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)} - \frac{a}{b \cdot 3}\]

   5. Simplified 14.0

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\color{blue}{\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)} - \sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) - \frac{a}{b \cdot 3}\]
   6. Using strategy rm

   7. Applied associate-/r* 14.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right) - \sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) - \color{blue}{\frac{\frac{a}{b}}{3}}\]
   8. Using strategy rm

   9. Applied flip3-- 14.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\frac{{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right)}^{3} - {\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)}^{3}}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) + \left(\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) + \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)\right)}} - \frac{\frac{a}{b}}{3}\]

   10. Applied associate-*r/ 14.1

       \[\leadsto \color{blue}{\frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right)}^{3} - {\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)}^{3}\right)}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) + \left(\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) + \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)\right)}} - \frac{\frac{a}{b}}{3}\]

   11. Taylor expanded around inf 14.2

       \[\leadsto \frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right)}^{3} - {\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)}^{3}\right)}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\cos y \cdot \color{blue}{\cos \left(0.3333333333333333148296162562473909929395 \cdot \left(t \cdot z\right)\right)}\right) + \left(\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) + \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)\right)} - \frac{\frac{a}{b}}{3}\]

   12. Simplified 14.2

       \[\leadsto \frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right)}^{3} - {\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)}^{3}\right)}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\cos y \cdot \color{blue}{\cos \left(\frac{6004799503160661}{18014398509481984} \cdot \left(t \cdot z\right)\right)}\right) + \left(\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) + \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)\right)} - \frac{\frac{a}{b}}{3}\]

   if 8.139896335094742e+149 < (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0))))

   1. Initial program 60.9

      \[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]

   2. Taylor expanded around 0 42.3

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(1 - \frac{1}{2} \cdot {y}^{2}\right)} - \frac{a}{b \cdot 3}\]

   3. Simplified 42.3

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(1 - \frac{1}{2} \cdot {y}^{2}\right)} - \frac{a}{b \cdot 3}\]
3. Recombined 2 regimes into one program.

4. Final simplification 17.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) \le 8.139896335094742174168253426990729793648 \cdot 10^{149}:\\ \;\;\;\;\frac{\left(2 \cdot \sqrt{x}\right) \cdot \left({\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right)}^{3} - {\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)}^{3}\right)}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{6004799503160661}{18014398509481984} \cdot \left(t \cdot z\right)\right)\right) + \left(\left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right) + \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3}\right)\right) \cdot \left(\sin y \cdot \sin \left(-\frac{z \cdot t}{3}\right)\right)\right)} - \frac{\frac{a}{b}}{3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \left(1 - \frac{1}{2} \cdot {y}^{2}\right) - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019303 
(FPCore (x y z t a b)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, K"
  :precision binary64

  :herbie-target
  (if (< z -1.379333748723514e129) (- (* (* 2 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.333333333333333315 z) t)))) (/ (/ a 3) b)) (if (< z 3.51629061355598715e106) (- (* (* (sqrt x) 2) (cos (- y (* (/ t 3) z)))) (/ (/ a 3) b)) (- (* (cos (- y (/ (/ 0.333333333333333315 z) t))) (* 2 (sqrt x))) (/ (/ a b) 3))))

  (- (* (* 2 (sqrt x)) (cos (- y (/ (* z t) 3)))) (/ a (* b 3))))