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

char *name = "Examples.Basics.ProofTests:f4 from sbv-4.4";

double f_if(float x, float y) {
        float r51130 = x;
        float r51131 = r51130 * r51130;
        float r51132 = 2.0;
        float r51133 = r51130 * r51132;
        float r51134 = y;
        float r51135 = r51133 * r51134;
        float r51136 = r51131 + r51135;
        float r51137 = r51134 * r51134;
        float r51138 = r51136 + r51137;
        return r51138;
}

double f_id(double x, double y) {
        double r51139 = x;
        double r51140 = r51139 * r51139;
        double r51141 = 2.0;
        double r51142 = r51139 * r51141;
        double r51143 = y;
        double r51144 = r51142 * r51143;
        double r51145 = r51140 + r51144;
        double r51146 = r51143 * r51143;
        double r51147 = r51145 + r51146;
        return r51147;
}


double f_of(float x, float y) {
        float r51148 = x;
        float r51149 = r51148 * r51148;
        float r51150 = 2.0;
        float r51151 = r51148 * r51150;
        float r51152 = y;
        float r51153 = r51151 * r51152;
        float r51154 = r51149 + r51153;
        float r51155 = r51152 * r51152;
        float r51156 = r51154 + r51155;
        return r51156;
}

double f_od(double x, double y) {
        double r51157 = x;
        double r51158 = r51157 * r51157;
        double r51159 = 2.0;
        double r51160 = r51157 * r51159;
        double r51161 = y;
        double r51162 = r51160 * r51161;
        double r51163 = r51158 + r51162;
        double r51164 = r51161 * r51161;
        double r51165 = r51163 + r51164;
        return r51165;
}

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 r51166, r51167, r51168, r51169, r51170, r51171, r51172, r51173, r51174;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51166);
        mpfr_init(r51167);
        mpfr_init_set_str(r51168, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51169);
        mpfr_init(r51170);
        mpfr_init(r51171);
        mpfr_init(r51172);
        mpfr_init(r51173);
        mpfr_init(r51174);
}

double f_im(double x, double y) {
        mpfr_set_d(r51166, x, MPFR_RNDN);
        mpfr_mul(r51167, r51166, r51166, MPFR_RNDN);
        ;
        mpfr_mul(r51169, r51166, r51168, MPFR_RNDN);
        mpfr_set_d(r51170, y, MPFR_RNDN);
        mpfr_mul(r51171, r51169, r51170, MPFR_RNDN);
        mpfr_add(r51172, r51167, r51171, MPFR_RNDN);
        mpfr_mul(r51173, r51170, r51170, MPFR_RNDN);
        mpfr_add(r51174, r51172, r51173, MPFR_RNDN);
        return mpfr_get_d(r51174, MPFR_RNDN);
}

static mpfr_t r51175, r51176, r51177, r51178, r51179, r51180, r51181, r51182, r51183;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51175);
        mpfr_init(r51176);
        mpfr_init_set_str(r51177, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51178);
        mpfr_init(r51179);
        mpfr_init(r51180);
        mpfr_init(r51181);
        mpfr_init(r51182);
        mpfr_init(r51183);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51175, x, MPFR_RNDN);
        mpfr_mul(r51176, r51175, r51175, MPFR_RNDN);
        ;
        mpfr_mul(r51178, r51175, r51177, MPFR_RNDN);
        mpfr_set_d(r51179, y, MPFR_RNDN);
        mpfr_mul(r51180, r51178, r51179, MPFR_RNDN);
        mpfr_add(r51181, r51176, r51180, MPFR_RNDN);
        mpfr_mul(r51182, r51179, r51179, MPFR_RNDN);
        mpfr_add(r51183, r51181, r51182, MPFR_RNDN);
        return mpfr_get_d(r51183, MPFR_RNDN);
}

static mpfr_t r51184, r51185, r51186, r51187, r51188, r51189, r51190, r51191, r51192;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51184);
        mpfr_init(r51185);
        mpfr_init_set_str(r51186, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51187);
        mpfr_init(r51188);
        mpfr_init(r51189);
        mpfr_init(r51190);
        mpfr_init(r51191);
        mpfr_init(r51192);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51184, x, MPFR_RNDN);
        mpfr_mul(r51185, r51184, r51184, MPFR_RNDN);
        ;
        mpfr_mul(r51187, r51184, r51186, MPFR_RNDN);
        mpfr_set_d(r51188, y, MPFR_RNDN);
        mpfr_mul(r51189, r51187, r51188, MPFR_RNDN);
        mpfr_add(r51190, r51185, r51189, MPFR_RNDN);
        mpfr_mul(r51191, r51188, r51188, MPFR_RNDN);
        mpfr_add(r51192, r51190, r51191, MPFR_RNDN);
        return mpfr_get_d(r51192, MPFR_RNDN);
}