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

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

double f_if(float x, float y) {
        float r49543 = x;
        float r49544 = y;
        float r49545 = r49543 + r49544;
        float r49546 = r49543 - r49544;
        float r49547 = r49545 * r49546;
        return r49547;
}

double f_id(double x, double y) {
        double r49548 = x;
        double r49549 = y;
        double r49550 = r49548 + r49549;
        double r49551 = r49548 - r49549;
        double r49552 = r49550 * r49551;
        return r49552;
}


double f_of(float x, float y) {
        float r49553 = x;
        float r49554 = y;
        float r49555 = r49553 + r49554;
        float r49556 = r49553 - r49554;
        float r49557 = r49555 * r49556;
        return r49557;
}

double f_od(double x, double y) {
        double r49558 = x;
        double r49559 = y;
        double r49560 = r49558 + r49559;
        double r49561 = r49558 - r49559;
        double r49562 = r49560 * r49561;
        return r49562;
}

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 r49563, r49564, r49565, r49566, r49567;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(144);
        mpfr_init(r49563);
        mpfr_init(r49564);
        mpfr_init(r49565);
        mpfr_init(r49566);
        mpfr_init(r49567);
}

double f_im(double x, double y) {
        mpfr_set_d(r49563, x, MPFR_RNDN);
        mpfr_set_d(r49564, y, MPFR_RNDN);
        mpfr_add(r49565, r49563, r49564, MPFR_RNDN);
        mpfr_sub(r49566, r49563, r49564, MPFR_RNDN);
        mpfr_mul(r49567, r49565, r49566, MPFR_RNDN);
        return mpfr_get_d(r49567, MPFR_RNDN);
}

static mpfr_t r49568, r49569, r49570, r49571, r49572;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(144);
        mpfr_init(r49568);
        mpfr_init(r49569);
        mpfr_init(r49570);
        mpfr_init(r49571);
        mpfr_init(r49572);
}

double f_fm(double x, double y) {
        mpfr_set_d(r49568, x, MPFR_RNDN);
        mpfr_set_d(r49569, y, MPFR_RNDN);
        mpfr_add(r49570, r49568, r49569, MPFR_RNDN);
        mpfr_sub(r49571, r49568, r49569, MPFR_RNDN);
        mpfr_mul(r49572, r49570, r49571, MPFR_RNDN);
        return mpfr_get_d(r49572, MPFR_RNDN);
}

static mpfr_t r49573, r49574, r49575, r49576, r49577;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(144);
        mpfr_init(r49573);
        mpfr_init(r49574);
        mpfr_init(r49575);
        mpfr_init(r49576);
        mpfr_init(r49577);
}

double f_dm(double x, double y) {
        mpfr_set_d(r49573, x, MPFR_RNDN);
        mpfr_set_d(r49574, y, MPFR_RNDN);
        mpfr_add(r49575, r49573, r49574, MPFR_RNDN);
        mpfr_sub(r49576, r49573, r49574, MPFR_RNDN);
        mpfr_mul(r49577, r49575, r49576, MPFR_RNDN);
        return mpfr_get_d(r49577, MPFR_RNDN);
}