#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 r49508 = x;
        float r49509 = r49508 * r49508;
        float r49510 = y;
        float r49511 = r49510 * r49510;
        float r49512 = r49509 - r49511;
        return r49512;
}

double f_id(double x, double y) {
        double r49513 = x;
        double r49514 = r49513 * r49513;
        double r49515 = y;
        double r49516 = r49515 * r49515;
        double r49517 = r49514 - r49516;
        return r49517;
}


double f_of(float x, float y) {
        float r49518 = x;
        float r49519 = y;
        float r49520 = r49518 + r49519;
        float r49521 = r49518 - r49519;
        float r49522 = r49520 * r49521;
        return r49522;
}

double f_od(double x, double y) {
        double r49523 = x;
        double r49524 = y;
        double r49525 = r49523 + r49524;
        double r49526 = r49523 - r49524;
        double r49527 = r49525 * r49526;
        return r49527;
}

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 r49528, r49529, r49530, r49531, r49532;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(144);
        mpfr_init(r49528);
        mpfr_init(r49529);
        mpfr_init(r49530);
        mpfr_init(r49531);
        mpfr_init(r49532);
}

double f_im(double x, double y) {
        mpfr_set_d(r49528, x, MPFR_RNDN);
        mpfr_mul(r49529, r49528, r49528, MPFR_RNDN);
        mpfr_set_d(r49530, y, MPFR_RNDN);
        mpfr_mul(r49531, r49530, r49530, MPFR_RNDN);
        mpfr_sub(r49532, r49529, r49531, MPFR_RNDN);
        return mpfr_get_d(r49532, MPFR_RNDN);
}

static mpfr_t r49533, r49534, r49535, r49536, r49537;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(144);
        mpfr_init(r49533);
        mpfr_init(r49534);
        mpfr_init(r49535);
        mpfr_init(r49536);
        mpfr_init(r49537);
}

double f_fm(double x, double y) {
        mpfr_set_d(r49533, x, MPFR_RNDN);
        mpfr_set_d(r49534, y, MPFR_RNDN);
        mpfr_add(r49535, r49533, r49534, MPFR_RNDN);
        mpfr_sub(r49536, r49533, r49534, MPFR_RNDN);
        mpfr_mul(r49537, r49535, r49536, MPFR_RNDN);
        return mpfr_get_d(r49537, MPFR_RNDN);
}

static mpfr_t r49538, r49539, r49540, r49541, r49542;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(144);
        mpfr_init(r49538);
        mpfr_init(r49539);
        mpfr_init(r49540);
        mpfr_init(r49541);
        mpfr_init(r49542);
}

double f_dm(double x, double y) {
        mpfr_set_d(r49538, x, MPFR_RNDN);
        mpfr_set_d(r49539, y, MPFR_RNDN);
        mpfr_add(r49540, r49538, r49539, MPFR_RNDN);
        mpfr_sub(r49541, r49538, r49539, MPFR_RNDN);
        mpfr_mul(r49542, r49540, r49541, MPFR_RNDN);
        return mpfr_get_d(r49542, MPFR_RNDN);
}