#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 r51962 = x;
        float r51963 = r51962 * r51962;
        float r51964 = y;
        float r51965 = r51964 * r51964;
        float r51966 = r51963 - r51965;
        return r51966;
}

double f_id(double x, double y) {
        double r51967 = x;
        double r51968 = r51967 * r51967;
        double r51969 = y;
        double r51970 = r51969 * r51969;
        double r51971 = r51968 - r51970;
        return r51971;
}


double f_of(float x, float y) {
        float r51972 = x;
        float r51973 = r51972 * r51972;
        float r51974 = y;
        float r51975 = r51974 * r51974;
        float r51976 = r51973 - r51975;
        return r51976;
}

double f_od(double x, double y) {
        double r51977 = x;
        double r51978 = r51977 * r51977;
        double r51979 = y;
        double r51980 = r51979 * r51979;
        double r51981 = r51978 - r51980;
        return r51981;
}

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 r51982, r51983, r51984, r51985, r51986;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51982);
        mpfr_init(r51983);
        mpfr_init(r51984);
        mpfr_init(r51985);
        mpfr_init(r51986);
}

double f_im(double x, double y) {
        mpfr_set_d(r51982, x, MPFR_RNDN);
        mpfr_mul(r51983, r51982, r51982, MPFR_RNDN);
        mpfr_set_d(r51984, y, MPFR_RNDN);
        mpfr_mul(r51985, r51984, r51984, MPFR_RNDN);
        mpfr_sub(r51986, r51983, r51985, MPFR_RNDN);
        return mpfr_get_d(r51986, MPFR_RNDN);
}

static mpfr_t r51987, r51988, r51989, r51990, r51991;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51987);
        mpfr_init(r51988);
        mpfr_init(r51989);
        mpfr_init(r51990);
        mpfr_init(r51991);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51987, x, MPFR_RNDN);
        mpfr_mul(r51988, r51987, r51987, MPFR_RNDN);
        mpfr_set_d(r51989, y, MPFR_RNDN);
        mpfr_mul(r51990, r51989, r51989, MPFR_RNDN);
        mpfr_sub(r51991, r51988, r51990, MPFR_RNDN);
        return mpfr_get_d(r51991, MPFR_RNDN);
}

static mpfr_t r51992, r51993, r51994, r51995, r51996;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51992);
        mpfr_init(r51993);
        mpfr_init(r51994);
        mpfr_init(r51995);
        mpfr_init(r51996);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51992, x, MPFR_RNDN);
        mpfr_mul(r51993, r51992, r51992, MPFR_RNDN);
        mpfr_set_d(r51994, y, MPFR_RNDN);
        mpfr_mul(r51995, r51994, r51994, MPFR_RNDN);
        mpfr_sub(r51996, r51993, r51995, MPFR_RNDN);
        return mpfr_get_d(r51996, MPFR_RNDN);
}