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

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

double f_if(float x, float y) {
        float r52156 = x;
        float r52157 = r52156 * r52156;
        float r52158 = y;
        float r52159 = r52158 * r52158;
        float r52160 = r52157 - r52159;
        return r52160;
}

double f_id(double x, double y) {
        double r52161 = x;
        double r52162 = r52161 * r52161;
        double r52163 = y;
        double r52164 = r52163 * r52163;
        double r52165 = r52162 - r52164;
        return r52165;
}


double f_of(float x, float y) {
        float r52166 = x;
        float r52167 = r52166 * r52166;
        float r52168 = y;
        float r52169 = r52168 * r52168;
        float r52170 = r52167 - r52169;
        return r52170;
}

double f_od(double x, double y) {
        double r52171 = x;
        double r52172 = r52171 * r52171;
        double r52173 = y;
        double r52174 = r52173 * r52173;
        double r52175 = r52172 - r52174;
        return r52175;
}

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 r52176, r52177, r52178, r52179, r52180;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r52176);
        mpfr_init(r52177);
        mpfr_init(r52178);
        mpfr_init(r52179);
        mpfr_init(r52180);
}

double f_im(double x, double y) {
        mpfr_set_d(r52176, x, MPFR_RNDN);
        mpfr_mul(r52177, r52176, r52176, MPFR_RNDN);
        mpfr_set_d(r52178, y, MPFR_RNDN);
        mpfr_mul(r52179, r52178, r52178, MPFR_RNDN);
        mpfr_sub(r52180, r52177, r52179, MPFR_RNDN);
        return mpfr_get_d(r52180, MPFR_RNDN);
}

static mpfr_t r52181, r52182, r52183, r52184, r52185;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52181);
        mpfr_init(r52182);
        mpfr_init(r52183);
        mpfr_init(r52184);
        mpfr_init(r52185);
}

double f_fm(double x, double y) {
        mpfr_set_d(r52181, x, MPFR_RNDN);
        mpfr_mul(r52182, r52181, r52181, MPFR_RNDN);
        mpfr_set_d(r52183, y, MPFR_RNDN);
        mpfr_mul(r52184, r52183, r52183, MPFR_RNDN);
        mpfr_sub(r52185, r52182, r52184, MPFR_RNDN);
        return mpfr_get_d(r52185, MPFR_RNDN);
}

static mpfr_t r52186, r52187, r52188, r52189, r52190;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52186);
        mpfr_init(r52187);
        mpfr_init(r52188);
        mpfr_init(r52189);
        mpfr_init(r52190);
}

double f_dm(double x, double y) {
        mpfr_set_d(r52186, x, MPFR_RNDN);
        mpfr_mul(r52187, r52186, r52186, MPFR_RNDN);
        mpfr_set_d(r52188, y, MPFR_RNDN);
        mpfr_mul(r52189, r52188, r52188, MPFR_RNDN);
        mpfr_sub(r52190, r52187, r52189, MPFR_RNDN);
        return mpfr_get_d(r52190, MPFR_RNDN);
}