#include <tgmath.h>
#include <gmp.h>
#include <mpfr.h>
#include <stdio.h>
#include <stdbool.h>

char *name = "Examples.Basics.ProofTests:f4 from sbv-4.4";

double f_if(float x, float y) {
        float r51833 = x;
        float r51834 = r51833 * r51833;
        float r51835 = 2.0;
        float r51836 = r51833 * r51835;
        float r51837 = y;
        float r51838 = r51836 * r51837;
        float r51839 = r51834 + r51838;
        float r51840 = r51837 * r51837;
        float r51841 = r51839 + r51840;
        return r51841;
}

double f_id(double x, double y) {
        double r51842 = x;
        double r51843 = r51842 * r51842;
        double r51844 = 2.0;
        double r51845 = r51842 * r51844;
        double r51846 = y;
        double r51847 = r51845 * r51846;
        double r51848 = r51843 + r51847;
        double r51849 = r51846 * r51846;
        double r51850 = r51848 + r51849;
        return r51850;
}


double f_of(float x, float y) {
        float r51851 = x;
        float r51852 = r51851 * r51851;
        float r51853 = 2.0;
        float r51854 = r51851 * r51853;
        float r51855 = y;
        float r51856 = r51854 * r51855;
        float r51857 = r51852 + r51856;
        float r51858 = r51855 * r51855;
        float r51859 = r51857 + r51858;
        return r51859;
}

double f_od(double x, double y) {
        double r51860 = x;
        double r51861 = r51860 * r51860;
        double r51862 = 2.0;
        double r51863 = r51860 * r51862;
        double r51864 = y;
        double r51865 = r51863 * r51864;
        double r51866 = r51861 + r51865;
        double r51867 = r51864 * r51864;
        double r51868 = r51866 + r51867;
        return r51868;
}

void mpfr_fmod2(mpfr_t r, mpfr_t n, mpfr_t d, mpfr_rnd_t rmd) {
        mpfr_fmod(r, n, d, rmd);
        if (mpfr_cmp_ui(r, 0) < 0) mpfr_add(r, r, d, rmd);
}


static mpfr_t r51869, r51870, r51871, r51872, r51873, r51874, r51875, r51876, r51877;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51869);
        mpfr_init(r51870);
        mpfr_init_set_str(r51871, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51872);
        mpfr_init(r51873);
        mpfr_init(r51874);
        mpfr_init(r51875);
        mpfr_init(r51876);
        mpfr_init(r51877);
}

double f_im(double x, double y) {
        mpfr_set_d(r51869, x, MPFR_RNDN);
        mpfr_mul(r51870, r51869, r51869, MPFR_RNDN);
        ;
        mpfr_mul(r51872, r51869, r51871, MPFR_RNDN);
        mpfr_set_d(r51873, y, MPFR_RNDN);
        mpfr_mul(r51874, r51872, r51873, MPFR_RNDN);
        mpfr_add(r51875, r51870, r51874, MPFR_RNDN);
        mpfr_mul(r51876, r51873, r51873, MPFR_RNDN);
        mpfr_add(r51877, r51875, r51876, MPFR_RNDN);
        return mpfr_get_d(r51877, MPFR_RNDN);
}

static mpfr_t r51878, r51879, r51880, r51881, r51882, r51883, r51884, r51885, r51886;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51878);
        mpfr_init(r51879);
        mpfr_init_set_str(r51880, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51881);
        mpfr_init(r51882);
        mpfr_init(r51883);
        mpfr_init(r51884);
        mpfr_init(r51885);
        mpfr_init(r51886);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51878, x, MPFR_RNDN);
        mpfr_mul(r51879, r51878, r51878, MPFR_RNDN);
        ;
        mpfr_mul(r51881, r51878, r51880, MPFR_RNDN);
        mpfr_set_d(r51882, y, MPFR_RNDN);
        mpfr_mul(r51883, r51881, r51882, MPFR_RNDN);
        mpfr_add(r51884, r51879, r51883, MPFR_RNDN);
        mpfr_mul(r51885, r51882, r51882, MPFR_RNDN);
        mpfr_add(r51886, r51884, r51885, MPFR_RNDN);
        return mpfr_get_d(r51886, MPFR_RNDN);
}

static mpfr_t r51887, r51888, r51889, r51890, r51891, r51892, r51893, r51894, r51895;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51887);
        mpfr_init(r51888);
        mpfr_init_set_str(r51889, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51890);
        mpfr_init(r51891);
        mpfr_init(r51892);
        mpfr_init(r51893);
        mpfr_init(r51894);
        mpfr_init(r51895);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51887, x, MPFR_RNDN);
        mpfr_mul(r51888, r51887, r51887, MPFR_RNDN);
        ;
        mpfr_mul(r51890, r51887, r51889, MPFR_RNDN);
        mpfr_set_d(r51891, y, MPFR_RNDN);
        mpfr_mul(r51892, r51890, r51891, MPFR_RNDN);
        mpfr_add(r51893, r51888, r51892, MPFR_RNDN);
        mpfr_mul(r51894, r51891, r51891, MPFR_RNDN);
        mpfr_add(r51895, r51893, r51894, MPFR_RNDN);
        return mpfr_get_d(r51895, MPFR_RNDN);
}