#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 r52288 = x;
        float r52289 = r52288 * r52288;
        float r52290 = y;
        float r52291 = r52290 * r52290;
        float r52292 = r52289 - r52291;
        return r52292;
}

double f_id(double x, double y) {
        double r52293 = x;
        double r52294 = r52293 * r52293;
        double r52295 = y;
        double r52296 = r52295 * r52295;
        double r52297 = r52294 - r52296;
        return r52297;
}


double f_of(float x, float y) {
        float r52298 = x;
        float r52299 = r52298 * r52298;
        float r52300 = y;
        float r52301 = r52300 * r52300;
        float r52302 = r52299 - r52301;
        return r52302;
}

double f_od(double x, double y) {
        double r52303 = x;
        double r52304 = r52303 * r52303;
        double r52305 = y;
        double r52306 = r52305 * r52305;
        double r52307 = r52304 - r52306;
        return r52307;
}

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 r52308, r52309, r52310, r52311, r52312;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r52308);
        mpfr_init(r52309);
        mpfr_init(r52310);
        mpfr_init(r52311);
        mpfr_init(r52312);
}

double f_im(double x, double y) {
        mpfr_set_d(r52308, x, MPFR_RNDN);
        mpfr_mul(r52309, r52308, r52308, MPFR_RNDN);
        mpfr_set_d(r52310, y, MPFR_RNDN);
        mpfr_mul(r52311, r52310, r52310, MPFR_RNDN);
        mpfr_sub(r52312, r52309, r52311, MPFR_RNDN);
        return mpfr_get_d(r52312, MPFR_RNDN);
}

static mpfr_t r52313, r52314, r52315, r52316, r52317;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52313);
        mpfr_init(r52314);
        mpfr_init(r52315);
        mpfr_init(r52316);
        mpfr_init(r52317);
}

double f_fm(double x, double y) {
        mpfr_set_d(r52313, x, MPFR_RNDN);
        mpfr_mul(r52314, r52313, r52313, MPFR_RNDN);
        mpfr_set_d(r52315, y, MPFR_RNDN);
        mpfr_mul(r52316, r52315, r52315, MPFR_RNDN);
        mpfr_sub(r52317, r52314, r52316, MPFR_RNDN);
        return mpfr_get_d(r52317, MPFR_RNDN);
}

static mpfr_t r52318, r52319, r52320, r52321, r52322;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52318);
        mpfr_init(r52319);
        mpfr_init(r52320);
        mpfr_init(r52321);
        mpfr_init(r52322);
}

double f_dm(double x, double y) {
        mpfr_set_d(r52318, x, MPFR_RNDN);
        mpfr_mul(r52319, r52318, r52318, MPFR_RNDN);
        mpfr_set_d(r52320, y, MPFR_RNDN);
        mpfr_mul(r52321, r52320, r52320, MPFR_RNDN);
        mpfr_sub(r52322, r52319, r52321, MPFR_RNDN);
        return mpfr_get_d(r52322, MPFR_RNDN);
}