#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 r52128 = x;
        float r52129 = y;
        float r52130 = r52128 + r52129;
        float r52131 = r52130 * r52130;
        return r52131;
}

double f_id(double x, double y) {
        double r52132 = x;
        double r52133 = y;
        double r52134 = r52132 + r52133;
        double r52135 = r52134 * r52134;
        return r52135;
}


double f_of(float x, float y) {
        float r52136 = x;
        float r52137 = y;
        float r52138 = r52136 + r52137;
        float r52139 = r52138 * r52138;
        return r52139;
}

double f_od(double x, double y) {
        double r52140 = x;
        double r52141 = y;
        double r52142 = r52140 + r52141;
        double r52143 = r52142 * r52142;
        return r52143;
}

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 r52144, r52145, r52146, r52147;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r52144);
        mpfr_init(r52145);
        mpfr_init(r52146);
        mpfr_init(r52147);
}

double f_im(double x, double y) {
        mpfr_set_d(r52144, x, MPFR_RNDN);
        mpfr_set_d(r52145, y, MPFR_RNDN);
        mpfr_add(r52146, r52144, r52145, MPFR_RNDN);
        mpfr_mul(r52147, r52146, r52146, MPFR_RNDN);
        return mpfr_get_d(r52147, MPFR_RNDN);
}

static mpfr_t r52148, r52149, r52150, r52151;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52148);
        mpfr_init(r52149);
        mpfr_init(r52150);
        mpfr_init(r52151);
}

double f_fm(double x, double y) {
        mpfr_set_d(r52148, x, MPFR_RNDN);
        mpfr_set_d(r52149, y, MPFR_RNDN);
        mpfr_add(r52150, r52148, r52149, MPFR_RNDN);
        mpfr_mul(r52151, r52150, r52150, MPFR_RNDN);
        return mpfr_get_d(r52151, MPFR_RNDN);
}

static mpfr_t r52152, r52153, r52154, r52155;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52152);
        mpfr_init(r52153);
        mpfr_init(r52154);
        mpfr_init(r52155);
}

double f_dm(double x, double y) {
        mpfr_set_d(r52152, x, MPFR_RNDN);
        mpfr_set_d(r52153, y, MPFR_RNDN);
        mpfr_add(r52154, r52152, r52153, MPFR_RNDN);
        mpfr_mul(r52155, r52154, r52154, MPFR_RNDN);
        return mpfr_get_d(r52155, MPFR_RNDN);
}