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

char *name = "Examples.Basics.BasicTests:f3 from sbv-4.4";

double f_if(float x, float y) {
        float r51840 = x;
        float r51841 = y;
        float r51842 = r51840 + r51841;
        float r51843 = r51842 * r51842;
        return r51843;
}

double f_id(double x, double y) {
        double r51844 = x;
        double r51845 = y;
        double r51846 = r51844 + r51845;
        double r51847 = r51846 * r51846;
        return r51847;
}


double f_of(float x, float y) {
        float r51848 = x;
        float r51849 = y;
        float r51850 = r51848 + r51849;
        float r51851 = r51850 * r51850;
        return r51851;
}

double f_od(double x, double y) {
        double r51852 = x;
        double r51853 = y;
        double r51854 = r51852 + r51853;
        double r51855 = r51854 * r51854;
        return r51855;
}

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 r51856, r51857, r51858, r51859;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51856);
        mpfr_init(r51857);
        mpfr_init(r51858);
        mpfr_init(r51859);
}

double f_im(double x, double y) {
        mpfr_set_d(r51856, x, MPFR_RNDN);
        mpfr_set_d(r51857, y, MPFR_RNDN);
        mpfr_add(r51858, r51856, r51857, MPFR_RNDN);
        mpfr_mul(r51859, r51858, r51858, MPFR_RNDN);
        return mpfr_get_d(r51859, MPFR_RNDN);
}

static mpfr_t r51860, r51861, r51862, r51863;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51860);
        mpfr_init(r51861);
        mpfr_init(r51862);
        mpfr_init(r51863);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51860, x, MPFR_RNDN);
        mpfr_set_d(r51861, y, MPFR_RNDN);
        mpfr_add(r51862, r51860, r51861, MPFR_RNDN);
        mpfr_mul(r51863, r51862, r51862, MPFR_RNDN);
        return mpfr_get_d(r51863, MPFR_RNDN);
}

static mpfr_t r51864, r51865, r51866, r51867;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51864);
        mpfr_init(r51865);
        mpfr_init(r51866);
        mpfr_init(r51867);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51864, x, MPFR_RNDN);
        mpfr_set_d(r51865, y, MPFR_RNDN);
        mpfr_add(r51866, r51864, r51865, MPFR_RNDN);
        mpfr_mul(r51867, r51866, r51866, MPFR_RNDN);
        return mpfr_get_d(r51867, MPFR_RNDN);
}