#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 r51868 = x;
        float r51869 = r51868 * r51868;
        float r51870 = y;
        float r51871 = r51870 * r51870;
        float r51872 = r51869 - r51871;
        return r51872;
}

double f_id(double x, double y) {
        double r51873 = x;
        double r51874 = r51873 * r51873;
        double r51875 = y;
        double r51876 = r51875 * r51875;
        double r51877 = r51874 - r51876;
        return r51877;
}


double f_of(float x, float y) {
        float r51878 = x;
        float r51879 = r51878 * r51878;
        float r51880 = y;
        float r51881 = r51880 * r51880;
        float r51882 = r51879 - r51881;
        return r51882;
}

double f_od(double x, double y) {
        double r51883 = x;
        double r51884 = r51883 * r51883;
        double r51885 = y;
        double r51886 = r51885 * r51885;
        double r51887 = r51884 - r51886;
        return r51887;
}

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 r51888, r51889, r51890, r51891, r51892;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51888);
        mpfr_init(r51889);
        mpfr_init(r51890);
        mpfr_init(r51891);
        mpfr_init(r51892);
}

double f_im(double x, double y) {
        mpfr_set_d(r51888, x, MPFR_RNDN);
        mpfr_mul(r51889, r51888, r51888, MPFR_RNDN);
        mpfr_set_d(r51890, y, MPFR_RNDN);
        mpfr_mul(r51891, r51890, r51890, MPFR_RNDN);
        mpfr_sub(r51892, r51889, r51891, MPFR_RNDN);
        return mpfr_get_d(r51892, MPFR_RNDN);
}

static mpfr_t r51893, r51894, r51895, r51896, r51897;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51893);
        mpfr_init(r51894);
        mpfr_init(r51895);
        mpfr_init(r51896);
        mpfr_init(r51897);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51893, x, MPFR_RNDN);
        mpfr_mul(r51894, r51893, r51893, MPFR_RNDN);
        mpfr_set_d(r51895, y, MPFR_RNDN);
        mpfr_mul(r51896, r51895, r51895, MPFR_RNDN);
        mpfr_sub(r51897, r51894, r51896, MPFR_RNDN);
        return mpfr_get_d(r51897, MPFR_RNDN);
}

static mpfr_t r51898, r51899, r51900, r51901, r51902;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51898);
        mpfr_init(r51899);
        mpfr_init(r51900);
        mpfr_init(r51901);
        mpfr_init(r51902);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51898, x, MPFR_RNDN);
        mpfr_mul(r51899, r51898, r51898, MPFR_RNDN);
        mpfr_set_d(r51900, y, MPFR_RNDN);
        mpfr_mul(r51901, r51900, r51900, MPFR_RNDN);
        mpfr_sub(r51902, r51899, r51901, MPFR_RNDN);
        return mpfr_get_d(r51902, MPFR_RNDN);
}