SynthBasics:moogVCF from YampaSynth-0.2

Average Error: 4.8 → 1.1

Time: 1.2m

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) = -\infty \lor \neg \left(x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) \le 2.46077799748154714011751001250268401259 \cdot 10^{294}\right):\\ \;\;\;\;x + \left(t \cdot z - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r554911 = x;
        double r554912 = y;
        double r554913 = z;
        double r554914 = r554912 * r554913;
        double r554915 = t;
        double r554916 = r554915 / r554912;
        double r554917 = tanh(r554916);
        double r554918 = r554911 / r554912;
        double r554919 = tanh(r554918);
        double r554920 = r554917 - r554919;
        double r554921 = r554914 * r554920;
        double r554922 = r554911 + r554921;
        return r554922;
}

↓

double f(double x, double y, double z, double t) {
        double r554923 = x;
        double r554924 = y;
        double r554925 = z;
        double r554926 = r554924 * r554925;
        double r554927 = t;
        double r554928 = r554927 / r554924;
        double r554929 = tanh(r554928);
        double r554930 = r554923 / r554924;
        double r554931 = tanh(r554930);
        double r554932 = r554929 - r554931;
        double r554933 = r554926 * r554932;
        double r554934 = r554923 + r554933;
        double r554935 = -inf.0;
        bool r554936 = r554934 <= r554935;
        double r554937 = 2.460777997481547e+294;
        bool r554938 = r554934 <= r554937;
        double r554939 = !r554938;
        bool r554940 = r554936 || r554939;
        double r554941 = r554927 * r554925;
        double r554942 = r554923 * r554925;
        double r554943 = r554941 - r554942;
        double r554944 = r554923 + r554943;
        double r554945 = r554940 ? r554944 : r554934;
        return r554945;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.8
Target	1.9
Herbie	1.1

\[x + y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)\]

Derivation

1. Split input into 2 regimes

2. if (+ x (* (* y z) (- (tanh (/ t y)) (tanh (/ x y))))) < -inf.0 or 2.460777997481547e+294 < (+ x (* (* y z) (- (tanh (/ t y)) (tanh (/ x y)))))

   1. Initial program 53.8

      \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
   2. Using strategy rm

   3. Applied flip3-- 53.8

      \[\leadsto x + \left(y \cdot z\right) \cdot \color{blue}{\frac{{\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\]

   4. Applied associate-*r/ 53.8

      \[\leadsto x + \color{blue}{\frac{\left(y \cdot z\right) \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\]

   5. Taylor expanded around 0 7.4

      \[\leadsto x + \color{blue}{\left(t \cdot z - x \cdot z\right)}\]

   if -inf.0 < (+ x (* (* y z) (- (tanh (/ t y)) (tanh (/ x y))))) < 2.460777997481547e+294

   1. Initial program 0.5

      \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
3. Recombined 2 regimes into one program.

4. Final simplification 1.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) = -\infty \lor \neg \left(x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) \le 2.46077799748154714011751001250268401259 \cdot 10^{294}\right):\\ \;\;\;\;x + \left(t \cdot z - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019350 +o rules:numerics
(FPCore (x y z t)
  :name "SynthBasics:moogVCF from YampaSynth-0.2"
  :precision binary64

  :herbie-target
  (+ x (* y (* z (- (tanh (/ t y)) (tanh (/ x y))))))

  (+ x (* (* y z) (- (tanh (/ t y)) (tanh (/ x y))))))