#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 r52197 = x;
        float r52198 = r52197 * r52197;
        float r52199 = 2.0;
        float r52200 = r52197 * r52199;
        float r52201 = y;
        float r52202 = r52200 * r52201;
        float r52203 = r52198 + r52202;
        float r52204 = r52201 * r52201;
        float r52205 = r52203 + r52204;
        return r52205;
}

double f_id(double x, double y) {
        double r52206 = x;
        double r52207 = r52206 * r52206;
        double r52208 = 2.0;
        double r52209 = r52206 * r52208;
        double r52210 = y;
        double r52211 = r52209 * r52210;
        double r52212 = r52207 + r52211;
        double r52213 = r52210 * r52210;
        double r52214 = r52212 + r52213;
        return r52214;
}


double f_of(float x, float y) {
        float r52215 = x;
        float r52216 = r52215 * r52215;
        float r52217 = 2.0;
        float r52218 = r52215 * r52217;
        float r52219 = y;
        float r52220 = r52218 * r52219;
        float r52221 = r52216 + r52220;
        float r52222 = r52219 * r52219;
        float r52223 = r52221 + r52222;
        return r52223;
}

double f_od(double x, double y) {
        double r52224 = x;
        double r52225 = r52224 * r52224;
        double r52226 = 2.0;
        double r52227 = r52224 * r52226;
        double r52228 = y;
        double r52229 = r52227 * r52228;
        double r52230 = r52225 + r52229;
        double r52231 = r52228 * r52228;
        double r52232 = r52230 + r52231;
        return r52232;
}

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 r52233, r52234, r52235, r52236, r52237, r52238, r52239, r52240, r52241;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r52233);
        mpfr_init(r52234);
        mpfr_init_set_str(r52235, "2.0", 10, MPFR_RNDN);
        mpfr_init(r52236);
        mpfr_init(r52237);
        mpfr_init(r52238);
        mpfr_init(r52239);
        mpfr_init(r52240);
        mpfr_init(r52241);
}

double f_im(double x, double y) {
        mpfr_set_d(r52233, x, MPFR_RNDN);
        mpfr_mul(r52234, r52233, r52233, MPFR_RNDN);
        ;
        mpfr_mul(r52236, r52233, r52235, MPFR_RNDN);
        mpfr_set_d(r52237, y, MPFR_RNDN);
        mpfr_mul(r52238, r52236, r52237, MPFR_RNDN);
        mpfr_add(r52239, r52234, r52238, MPFR_RNDN);
        mpfr_mul(r52240, r52237, r52237, MPFR_RNDN);
        mpfr_add(r52241, r52239, r52240, MPFR_RNDN);
        return mpfr_get_d(r52241, MPFR_RNDN);
}

static mpfr_t r52242, r52243, r52244, r52245, r52246, r52247, r52248, r52249, r52250;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52242);
        mpfr_init(r52243);
        mpfr_init_set_str(r52244, "2.0", 10, MPFR_RNDN);
        mpfr_init(r52245);
        mpfr_init(r52246);
        mpfr_init(r52247);
        mpfr_init(r52248);
        mpfr_init(r52249);
        mpfr_init(r52250);
}

double f_fm(double x, double y) {
        mpfr_set_d(r52242, x, MPFR_RNDN);
        mpfr_mul(r52243, r52242, r52242, MPFR_RNDN);
        ;
        mpfr_mul(r52245, r52242, r52244, MPFR_RNDN);
        mpfr_set_d(r52246, y, MPFR_RNDN);
        mpfr_mul(r52247, r52245, r52246, MPFR_RNDN);
        mpfr_add(r52248, r52243, r52247, MPFR_RNDN);
        mpfr_mul(r52249, r52246, r52246, MPFR_RNDN);
        mpfr_add(r52250, r52248, r52249, MPFR_RNDN);
        return mpfr_get_d(r52250, MPFR_RNDN);
}

static mpfr_t r52251, r52252, r52253, r52254, r52255, r52256, r52257, r52258, r52259;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r52251);
        mpfr_init(r52252);
        mpfr_init_set_str(r52253, "2.0", 10, MPFR_RNDN);
        mpfr_init(r52254);
        mpfr_init(r52255);
        mpfr_init(r52256);
        mpfr_init(r52257);
        mpfr_init(r52258);
        mpfr_init(r52259);
}

double f_dm(double x, double y) {
        mpfr_set_d(r52251, x, MPFR_RNDN);
        mpfr_mul(r52252, r52251, r52251, MPFR_RNDN);
        ;
        mpfr_mul(r52254, r52251, r52253, MPFR_RNDN);
        mpfr_set_d(r52255, y, MPFR_RNDN);
        mpfr_mul(r52256, r52254, r52255, MPFR_RNDN);
        mpfr_add(r52257, r52252, r52256, MPFR_RNDN);
        mpfr_mul(r52258, r52255, r52255, MPFR_RNDN);
        mpfr_add(r52259, r52257, r52258, MPFR_RNDN);
        return mpfr_get_d(r52259, MPFR_RNDN);
}