/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Soonho Kong
*/
#include "util/test.h"
#include "util/numerics/double.h"
#include "util/interval/interval.h"
#include "tests/util/interval/check.h"
#include "util/init_module.h"

using namespace lean;

using std::cout;
using std::endl;

typedef interval<double> di;

static void double_interval_arith() {
    di i1(1.0, 2.0);
    di i2(3.0, 4.0);
    di i3(-10.0, -5.0);
    di i4(-3.0, +4.0);
    di i5(5.0, 8.0);

    double c1 = 0.6;
    double c2 = 3.0;
    double c3 = 0.0;
    double c4 = -4.5;
    double c5 = -0.3;

    cout << "=====================" << endl;
    print_result(i1, "+", c1, i1 + c1);
    print_result(i2, "+", c2, i2 + c2);
    print_result(i3, "+", c3, i3 + c3);
    print_result(i4, "+", c4, i4 + c4);
    print_result(i5, "+", c5, i5 + c5);
    print_result(i5, "+", c1, i5 + c1);
    print_result(i4, "+", c2, i4 + c2);
    print_result(i2, "+", c4, i2 + c4);
    print_result(i1, "+", c5, i1 + c5);

    cout << "=====================" << endl;
    print_result(c1, "+", i1, c1 + i1);
    print_result(c2, "+", i2, c2 + i2);
    print_result(c3, "+", i3, c3 + i3);
    print_result(c4, "+", i4, c4 + i4);
    print_result(c5, "+", i5, c5 + i5);
    print_result(c5, "+", i1, c5 + i1);
    print_result(c4, "+", i2, c4 + i2);
    print_result(c2, "+", i4, c2 + i4);
    print_result(c1, "+", i5, c1 + i5);

    cout << "=====================" << endl;
    print_result(i1, "-", c1, i1 - c1);
    print_result(i2, "-", c2, i2 - c2);
    print_result(i3, "-", c3, i3 - c3);
    print_result(i4, "-", c4, i4 - c4);
    print_result(i5, "-", c5, i5 - c5);
    print_result(i5, "-", c1, i5 - c1);
    print_result(i4, "-", c2, i4 - c2);
    print_result(i2, "-", c4, i2 - c4);
    print_result(i1, "-", c5, i1 - c5);

    cout << "=====================" << endl;
    print_result(c1, "-", i1, c1 - i1);
    print_result(c2, "-", i2, c2 - i2);
    print_result(c3, "-", i3, c3 - i3);
    print_result(c4, "-", i4, c4 - i4);
    print_result(c5, "-", i5, c5 - i5);
    print_result(c5, "-", i1, c5 - i1);
    print_result(c4, "-", i2, c4 - i2);
    print_result(c2, "-", i4, c2 - i4);
    print_result(c1, "-", i5, c1 - i5);

    cout << "=====================" << endl;
    print_result(i1, "*", c1, i1 * c1);
    print_result(i2, "*", c2, i2 * c2);
    print_result(i3, "*", c3, i3 * c3);
    print_result(i4, "*", c4, i4 * c4);
    print_result(i5, "*", c5, i5 * c5);
    print_result(i5, "*", c1, i5 * c1);
    print_result(i4, "*", c2, i4 * c2);
    print_result(i2, "*", c4, i2 * c4);
    print_result(i1, "*", c5, i1 * c5);

    cout << "=====================" << endl;
    print_result(c1, "*", i1, c1 * i1);
    print_result(c2, "*", i2, c2 * i2);
    print_result(c3, "*", i3, c3 * i3);
    print_result(c4, "*", i4, c4 * i4);
    print_result(c5, "*", i5, c5 * i5);
    print_result(c5, "*", i1, c5 * i1);
    print_result(c4, "*", i2, c4 * i2);
    print_result(c2, "*", i4, c2 * i4);
    print_result(c1, "*", i5, c1 * i5);

    cout << "=====================" << endl;
    print_result(i1, "/", c1, i1 / c1);
    print_result(i2, "/", c2, i2 / c2);
    print_result(i3, "/", c3, i3 / c3);
    print_result(i4, "/", c4, i4 / c4);
    print_result(i5, "/", c5, i5 / c5);
    print_result(i5, "/", c1, i5 / c1);
    print_result(i4, "/", c2, i4 / c2);
    print_result(i2, "/", c4, i2 / c4);
    print_result(i1, "/", c5, i1 / c5);

    cout << "=====================" << endl;
    print_result(c1, "/", i1, c1 / i1);
    print_result(c2, "/", i2, c2 / i2);
    print_result(c3, "/", i3, c3 / i3);
    print_result(c5, "/", i5, c5 / i5);
    print_result(c5, "/", i1, c5 / i1);
    print_result(c4, "/", i2, c4 / i2);
    print_result(c1, "/", i5, c1 / i5);
}

static void double_interval_inf1() {
    di i1(1.0, 2.0);
    di inf;
    di ozero_pinf;
    di ozero_ninf;
    ozero_pinf.set_is_lower_inf(false);
    ozero_ninf.set_is_upper_inf(false);
    di czero_pinf;
    di czero_ninf;
    czero_pinf.set_is_lower_inf(false);
    czero_pinf.set_is_lower_open(false);
    czero_ninf.set_is_upper_inf(false);
    czero_ninf.set_is_upper_open(false);

    cout << i1 << " * " << ozero_ninf << " = " << i1 * ozero_ninf << endl;
    cout << i1 << " * " << ozero_pinf << " = " << i1 * ozero_pinf << endl;
    cout << i1 << " * " << czero_ninf << " = " << i1 * czero_ninf << endl;
    cout << i1 << " * " << czero_pinf << " = " << i1 * czero_pinf << endl;
    lean_assert(i1 * ozero_ninf == ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
    lean_assert(i1 * ozero_pinf == ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
    lean_assert(i1 * czero_ninf == czero_ninf); lean_assert(czero_ninf * i1 == czero_ninf);
    lean_assert(i1 * czero_pinf == czero_pinf); lean_assert(czero_pinf * i1 == czero_pinf);

    cout << "=== Addition between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
    cout << ozero_ninf << " + " << ozero_ninf << " = " << ozero_ninf + ozero_ninf << endl;
    cout << ozero_ninf << " + " << ozero_pinf << " = " << ozero_ninf + ozero_pinf << endl;
    cout << ozero_ninf << " + " << czero_ninf << " = " << ozero_ninf + czero_ninf << endl;
    cout << ozero_ninf << " + " << czero_pinf << " = " << ozero_ninf + czero_pinf << endl;
    cout << ozero_pinf << " + " << ozero_ninf << " = " << ozero_pinf + ozero_ninf << endl;
    cout << ozero_pinf << " + " << ozero_pinf << " = " << ozero_pinf + ozero_pinf << endl;
    cout << ozero_pinf << " + " << czero_ninf << " = " << ozero_pinf + czero_ninf << endl;
    cout << ozero_pinf << " + " << czero_pinf << " = " << ozero_pinf + czero_pinf << endl;
    cout << czero_ninf << " + " << ozero_ninf << " = " << czero_ninf + ozero_ninf << endl;
    cout << czero_ninf << " + " << ozero_pinf << " = " << czero_ninf + ozero_pinf << endl;
    cout << czero_ninf << " + " << czero_ninf << " = " << czero_ninf + czero_ninf << endl;
    cout << czero_ninf << " + " << czero_pinf << " = " << czero_ninf + czero_pinf << endl;
    cout << czero_pinf << " + " << ozero_ninf << " = " << czero_pinf + ozero_ninf << endl;
    cout << czero_pinf << " + " << ozero_pinf << " = " << czero_pinf + ozero_pinf << endl;
    cout << czero_pinf << " + " << czero_ninf << " = " << czero_pinf + czero_ninf << endl;
    cout << czero_pinf << " + " << czero_pinf << " = " << czero_pinf + czero_pinf << endl;

    lean_assert(ozero_ninf + ozero_ninf == ozero_ninf);
    lean_assert(ozero_ninf + ozero_pinf == inf);
    lean_assert(ozero_ninf + czero_ninf == ozero_ninf);
    lean_assert(ozero_ninf + czero_pinf == inf);
    lean_assert(ozero_pinf + ozero_ninf == inf);
    lean_assert(ozero_pinf + ozero_pinf == ozero_pinf);
    lean_assert(ozero_pinf + czero_ninf == inf);
    lean_assert(ozero_pinf + czero_pinf == ozero_pinf);
    lean_assert(czero_ninf + ozero_ninf == ozero_ninf);
    lean_assert(czero_ninf + ozero_pinf == inf);
    lean_assert(czero_ninf + czero_ninf == czero_ninf);
    lean_assert(czero_ninf + czero_pinf == inf);
    lean_assert(czero_pinf + ozero_ninf == inf);
    lean_assert(czero_pinf + ozero_pinf == ozero_pinf);
    lean_assert(czero_pinf + czero_ninf == inf);
    lean_assert(czero_pinf + czero_pinf == czero_pinf);

    cout << "=== Subtraction between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
    cout << ozero_ninf << " - " << ozero_ninf << " = " << ozero_ninf - ozero_ninf << endl;
    cout << ozero_ninf << " - " << ozero_pinf << " = " << ozero_ninf - ozero_pinf << endl;
    cout << ozero_ninf << " - " << czero_ninf << " = " << ozero_ninf - czero_ninf << endl;
    cout << ozero_ninf << " - " << czero_pinf << " = " << ozero_ninf - czero_pinf << endl;
    cout << ozero_pinf << " - " << ozero_ninf << " = " << ozero_pinf - ozero_ninf << endl;
    cout << ozero_pinf << " - " << ozero_pinf << " = " << ozero_pinf - ozero_pinf << endl;
    cout << ozero_pinf << " - " << czero_ninf << " = " << ozero_pinf - czero_ninf << endl;
    cout << ozero_pinf << " - " << czero_pinf << " = " << ozero_pinf - czero_pinf << endl;
    cout << czero_ninf << " - " << ozero_ninf << " = " << czero_ninf - ozero_ninf << endl;
    cout << czero_ninf << " - " << ozero_pinf << " = " << czero_ninf - ozero_pinf << endl;
    cout << czero_ninf << " - " << czero_ninf << " = " << czero_ninf - czero_ninf << endl;
    cout << czero_ninf << " - " << czero_pinf << " = " << czero_ninf - czero_pinf << endl;
    cout << czero_pinf << " - " << ozero_ninf << " = " << czero_pinf - ozero_ninf << endl;
    cout << czero_pinf << " - " << ozero_pinf << " = " << czero_pinf - ozero_pinf << endl;
    cout << czero_pinf << " - " << czero_ninf << " = " << czero_pinf - czero_ninf << endl;
    cout << czero_pinf << " - " << czero_pinf << " = " << czero_pinf - czero_pinf << endl;

    lean_assert(ozero_ninf - ozero_ninf == inf);
    lean_assert(ozero_ninf - ozero_pinf == ozero_ninf);
    lean_assert(ozero_ninf - czero_ninf == inf);
    lean_assert(ozero_ninf - czero_pinf == ozero_ninf);
    lean_assert(ozero_pinf - ozero_ninf == ozero_pinf);
    lean_assert(ozero_pinf - ozero_pinf == inf);
    lean_assert(ozero_pinf - czero_ninf == ozero_pinf);
    lean_assert(ozero_pinf - czero_pinf == inf);
    lean_assert(czero_ninf - ozero_ninf == inf);
    lean_assert(czero_ninf - ozero_pinf == ozero_ninf);
    lean_assert(czero_ninf - czero_ninf == inf);
    lean_assert(czero_ninf - czero_pinf == czero_ninf);
    lean_assert(czero_pinf - ozero_ninf == ozero_pinf);
    lean_assert(czero_pinf - ozero_pinf == inf);
    lean_assert(czero_pinf - czero_ninf == czero_pinf);
    lean_assert(czero_pinf - czero_pinf == inf);

    cout << "=== Multiplication between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
    cout << ozero_ninf << " * " << ozero_ninf << " = " << ozero_ninf * ozero_ninf << endl;
    cout << ozero_ninf << " * " << ozero_pinf << " = " << ozero_ninf * ozero_pinf << endl;
    cout << ozero_ninf << " * " << czero_ninf << " = " << ozero_ninf * czero_ninf << endl;
    cout << ozero_ninf << " * " << czero_pinf << " = " << ozero_ninf * czero_pinf << endl;
    cout << ozero_pinf << " * " << ozero_ninf << " = " << ozero_pinf * ozero_ninf << endl;
    cout << ozero_pinf << " * " << ozero_pinf << " = " << ozero_pinf * ozero_pinf << endl;
    cout << ozero_pinf << " * " << czero_ninf << " = " << ozero_pinf * czero_ninf << endl;
    cout << ozero_pinf << " * " << czero_pinf << " = " << ozero_pinf * czero_pinf << endl;
    cout << czero_ninf << " * " << ozero_ninf << " = " << czero_ninf * ozero_ninf << endl;
    cout << czero_ninf << " * " << ozero_pinf << " = " << czero_ninf * ozero_pinf << endl;
    cout << czero_ninf << " * " << czero_ninf << " = " << czero_ninf * czero_ninf << endl;
    cout << czero_ninf << " * " << czero_pinf << " = " << czero_ninf * czero_pinf << endl;
    cout << czero_pinf << " * " << ozero_ninf << " = " << czero_pinf * ozero_ninf << endl;
    cout << czero_pinf << " * " << ozero_pinf << " = " << czero_pinf * ozero_pinf << endl;
    cout << czero_pinf << " * " << czero_ninf << " = " << czero_pinf * czero_ninf << endl;
    cout << czero_pinf << " * " << czero_pinf << " = " << czero_pinf * czero_pinf << endl;

    lean_assert(ozero_ninf * ozero_ninf == ozero_pinf);
    lean_assert(ozero_ninf * ozero_pinf == ozero_ninf);
    lean_assert(ozero_ninf * czero_ninf == czero_pinf);
    lean_assert(ozero_ninf * czero_pinf == czero_ninf);
    lean_assert(ozero_pinf * ozero_ninf == ozero_ninf);
    lean_assert(ozero_pinf * ozero_pinf == ozero_pinf);
    lean_assert(ozero_pinf * czero_ninf == czero_ninf);
    lean_assert(ozero_pinf * czero_pinf == czero_pinf);
    lean_assert(czero_ninf * ozero_ninf == czero_pinf);
    lean_assert(czero_ninf * ozero_pinf == czero_ninf);
    lean_assert(czero_ninf * czero_ninf == czero_pinf);
    lean_assert(czero_ninf * czero_pinf == czero_ninf);
    lean_assert(czero_pinf * ozero_ninf == czero_ninf);
    lean_assert(czero_pinf * ozero_pinf == czero_pinf);
    lean_assert(czero_pinf * czero_ninf == czero_ninf);
    lean_assert(czero_pinf * czero_pinf == czero_pinf);

    cout << "=== Division between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
    cout << ozero_ninf << " / " << ozero_ninf << " = " << ozero_ninf / ozero_ninf << endl;
    cout << ozero_ninf << " / " << ozero_pinf << " = " << ozero_ninf / ozero_pinf << endl;
    cout << ozero_pinf << " / " << ozero_ninf << " = " << ozero_pinf / ozero_ninf << endl;
    cout << ozero_pinf << " / " << ozero_pinf << " = " << ozero_pinf / ozero_pinf << endl;
    cout << czero_ninf << " / " << ozero_ninf << " = " << czero_ninf / ozero_ninf << endl;
    cout << czero_ninf << " / " << ozero_pinf << " = " << czero_ninf / ozero_pinf << endl;
    cout << czero_pinf << " / " << ozero_ninf << " = " << czero_pinf / ozero_ninf << endl;
    cout << czero_pinf << " / " << ozero_pinf << " = " << czero_pinf / ozero_pinf << endl;

    lean_assert(ozero_ninf / ozero_ninf == ozero_pinf);
    lean_assert(ozero_ninf / ozero_pinf == ozero_ninf);
    lean_assert(ozero_pinf / ozero_ninf == ozero_ninf);
    lean_assert(ozero_pinf / ozero_pinf == ozero_pinf);
    lean_assert(czero_ninf / ozero_ninf == czero_pinf);
    lean_assert(czero_ninf / ozero_pinf == czero_ninf);
    lean_assert(czero_pinf / ozero_ninf == czero_ninf);
    lean_assert(czero_pinf / ozero_pinf == czero_pinf);
}

static void double_interval_inf2() {
    di i1(1.0, 2.0);
    di i2(3.0, 4.0);
    di i3(-10.0, -5.0);
    di i4(-3.0, +4.0);
    di i5(5.0, 8.0);
    di inf;

    double c1 = 0.6;
    double c2 = 3.0;
    double c3 = -0.3;
    double c4 = -4.5;
    double zero = 0.0;

    lean_assert(i1 + inf == inf);   lean_assert(inf + i1 == inf);
    lean_assert(i2 + inf == inf);   lean_assert(inf + i2 == inf);
    lean_assert(i3 + inf == inf);   lean_assert(inf + i3 == inf);
    lean_assert(i4 + inf == inf);   lean_assert(inf + i4 == inf);
    lean_assert(i5 + inf == inf);   lean_assert(inf + i5 == inf);
    lean_assert(c1 + inf == inf);   lean_assert(inf + c1 == inf);
    lean_assert(c2 + inf == inf);   lean_assert(inf + c2 == inf);
    lean_assert(c3 + inf == inf);   lean_assert(inf + c3 == inf);
    lean_assert(c4 + inf == inf);   lean_assert(inf + c4 == inf);
    lean_assert(zero + inf == inf); lean_assert(inf + zero == inf);

    lean_assert(i1 - inf == inf);   lean_assert(inf - i1 == inf);
    lean_assert(i2 - inf == inf);   lean_assert(inf - i2 == inf);
    lean_assert(i3 - inf == inf);   lean_assert(inf - i3 == inf);
    lean_assert(i4 - inf == inf);   lean_assert(inf - i4 == inf);
    lean_assert(i5 - inf == inf);   lean_assert(inf - i5 == inf);
    lean_assert(c1 - inf == inf);   lean_assert(inf - c1 == inf);
    lean_assert(c2 - inf == inf);   lean_assert(inf - c2 == inf);
    lean_assert(c3 - inf == inf);   lean_assert(inf - c3 == inf);
    lean_assert(c4 - inf == inf);   lean_assert(inf - c4 == inf);
    lean_assert(zero - inf == inf); lean_assert(inf - zero == inf);

    lean_assert(i1 * inf == inf);    lean_assert(inf * i1 == inf);
    lean_assert(i2 * inf == inf);    lean_assert(inf * i2 == inf);
    lean_assert(i3 * inf == inf);    lean_assert(inf * i3 == inf);
    lean_assert(i4 * inf == inf);    lean_assert(inf * i4 == inf);
    lean_assert(i5 * inf == inf);    lean_assert(inf * i5 == inf);
    lean_assert(c1 * inf == inf);    lean_assert(inf * c1 == inf);
    lean_assert(c2 * inf == inf);    lean_assert(inf * c2 == inf);
    lean_assert(c3 * inf == inf);    lean_assert(inf * c3 == inf);
    lean_assert(c4 * inf == inf);    lean_assert(inf * c4 == inf);
    lean_assert(zero * inf == zero); lean_assert(inf * zero == zero);
}

static void double_interval_trans() {
    di i1(1.0, 2.0);
    di i2(3.0, 4.0);
    di i3(-10.0, -5.0);
    di i4(-3.0, +4.0);
    di i5(5.0, 8.0);
    di i6(0.3, 1.67);
    di i7(1.8, 3.5);
    di i8(3.5, 4.9);
    di i9(-3.15, -2.0);
    di i10(-0.99, 0.5);
    di i11(-0.8, -0.5);
    di i12(-0.3, 0.2);
    di i13(0.5, 0.9);
    di i14(-0.1, 0.8);
    di i15(-0.4, -0.3);

    di oi1(1.0, 2.0);
    di oi2(3.0, 4.0);
    di oi3(-10.0, -5.0);
    di oi4(-3.0, +4.0);
    di oi5(5.0, 8.0);
    di oi6(0.3, 1.67);
    di oi7(1.8, 3.5);
    di oi8(3.5, 4.9);
    di oi9(-3.15, -2.0);
    di oi10(-3.19, -1.0);
    di oi11(-0.8, -0.5);
    di oi12(-0.3, 0.2);
    di oi13(0.5, 0.9);
    di oi14(-0.1, 0.8);
    di oi15(-0.4, -0.3);

    oi1.set_is_lower_open(true);  oi1.set_is_upper_open(true);
    oi2.set_is_lower_open(true);  oi2.set_is_upper_open(true);
    oi3.set_is_lower_open(true);  oi3.set_is_upper_open(true);
    oi4.set_is_lower_open(true);  oi4.set_is_upper_open(true);
    oi5.set_is_lower_open(true);  oi5.set_is_upper_open(true);
    oi6.set_is_lower_open(true);  oi6.set_is_upper_open(true);
    oi7.set_is_lower_open(true);  oi7.set_is_upper_open(true);
    oi8.set_is_lower_open(true);  oi8.set_is_upper_open(true);
    oi9.set_is_lower_open(true);  oi9.set_is_upper_open(true);
    oi10.set_is_lower_open(true); oi10.set_is_upper_open(true);
    oi11.set_is_lower_open(true); oi11.set_is_upper_open(true);
    oi12.set_is_lower_open(true); oi12.set_is_upper_open(true);
    oi13.set_is_lower_open(true); oi13.set_is_upper_open(true);
    oi14.set_is_lower_open(true); oi14.set_is_upper_open(true);
    oi15.set_is_lower_open(true); oi15.set_is_upper_open(true);

    di inf;
    di ozero_pinf;
    di ozero_ninf;
    ozero_pinf.set_is_lower_inf(false);
    ozero_ninf.set_is_upper_inf(false);
    di czero_pinf;
    di czero_ninf;
    czero_pinf.set_is_lower_inf(false);
    czero_pinf.set_is_lower_open(false);
    czero_ninf.set_is_upper_inf(false);
    czero_ninf.set_is_upper_open(false);

    // double c1 = 0.6;
    // double c2 = 3.0;
    // double c3 = 0.0;
    // double c4 = -4.5;
    // double c5 = -0.3;

    cout << "=====================" << endl;
    check_bop(double, power, i1, 3u);
    check_bop(double, power, i2, 3u);
    check_bop(double, power, i3, 3u);
    check_bop(double, power, i4, 3u);
    check_bop(double, power, i5, 3u);
    check_bop(double, power, i6, 3u);
    check_bop(double, power, i7, 3u);
    check_bop(double, power, i8, 3u);
    check_bop(double, power, i9, 3u);
    check_bop(double, power, i10, 3u);
    check_bop(double, power, i11, 3u);
    check_bop(double, power, i12, 3u);
    check_bop(double, power, i13, 3u);
    check_bop(double, power, i14, 3u);
    check_bop(double, power, i15, 3u);
    check_bop(double, power, oi1, 3u);
    check_bop(double, power, oi2, 3u);
    check_bop(double, power, oi3, 3u);
    check_bop(double, power, oi4, 3u);
    check_bop(double, power, oi5, 3u);
    check_bop(double, power, oi6, 3u);
    check_bop(double, power, oi7, 3u);
    check_bop(double, power, oi8, 3u);
    check_bop(double, power, oi9, 3u);
    check_bop(double, power, oi10, 3u);
    check_bop(double, power, oi11, 3u);
    check_bop(double, power, oi12, 3u);
    check_bop(double, power, oi13, 3u);
    check_bop(double, power, oi14, 3u);
    check_bop(double, power, oi15, 3u);
    check_bop(double, power, inf, 3u);
    check_bop(double, power, ozero_ninf, 3u);
    check_bop(double, power, ozero_pinf, 3u);
    check_bop(double, power, czero_ninf, 3u);
    check_bop(double, power, czero_pinf, 3u);

    cout << "=====================" << endl;
    check_uop(double, exp, i1);
    check_uop(double, exp, i2);
    check_uop(double, exp, i3);
    check_uop(double, exp, i4);
    check_uop(double, exp, i5);
    check_uop(double, exp, i6);
    check_uop(double, exp, i7);
    check_uop(double, exp, i8);
    check_uop(double, exp, i9);
    check_uop(double, exp, i10);
    check_uop(double, exp, i11);
    check_uop(double, exp, i12);
    check_uop(double, exp, i13);
    check_uop(double, exp, i14);
    check_uop(double, exp, i15);
    check_uop(double, exp, oi1);
    check_uop(double, exp, oi2);
    check_uop(double, exp, oi3);
    check_uop(double, exp, oi4);
    check_uop(double, exp, oi5);
    check_uop(double, exp, oi6);
    check_uop(double, exp, oi7);
    check_uop(double, exp, oi8);
    check_uop(double, exp, oi9);
    check_uop(double, exp, oi10);
    check_uop(double, exp, oi11);
    check_uop(double, exp, oi12);
    check_uop(double, exp, oi13);
    check_uop(double, exp, oi14);
    check_uop(double, exp, oi15);
    check_uop(double, exp, inf);
    check_uop(double, exp, ozero_pinf);
    check_uop(double, exp, ozero_ninf);
    check_uop(double, exp, czero_pinf);
    check_uop(double, exp, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, exp2, i1);
    check_uop(double, exp2, i2);
    check_uop(double, exp2, i3);
    check_uop(double, exp2, i4);
    check_uop(double, exp2, i5);
    check_uop(double, exp2, i6);
    check_uop(double, exp2, i7);
    check_uop(double, exp2, i8);
    check_uop(double, exp2, i9);
    check_uop(double, exp2, i10);
    check_uop(double, exp2, i11);
    check_uop(double, exp2, i12);
    check_uop(double, exp2, i13);
    check_uop(double, exp2, i14);
    check_uop(double, exp2, i15);
    check_uop(double, exp2, oi1);
    check_uop(double, exp2, oi2);
    check_uop(double, exp2, oi3);
    check_uop(double, exp2, oi4);
    check_uop(double, exp2, oi5);
    check_uop(double, exp2, oi6);
    check_uop(double, exp2, oi7);
    check_uop(double, exp2, oi8);
    check_uop(double, exp2, oi9);
    check_uop(double, exp2, oi10);
    check_uop(double, exp2, oi11);
    check_uop(double, exp2, oi12);
    check_uop(double, exp2, oi13);
    check_uop(double, exp2, oi14);
    check_uop(double, exp2, oi15);
    check_uop(double, exp2, inf);
    check_uop(double, exp2, ozero_pinf);
    check_uop(double, exp2, ozero_ninf);
    check_uop(double, exp2, czero_pinf);
    check_uop(double, exp2, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, exp10, i1);
    check_uop(double, exp10, i2);
    check_uop(double, exp10, i3);
    check_uop(double, exp10, i4);
    check_uop(double, exp10, i5);
    check_uop(double, exp10, i6);
    check_uop(double, exp10, i7);
    check_uop(double, exp10, i8);
    check_uop(double, exp10, i9);
    check_uop(double, exp10, i10);
    check_uop(double, exp10, i11);
    check_uop(double, exp10, i12);
    check_uop(double, exp10, i13);
    check_uop(double, exp10, i14);
    check_uop(double, exp10, i15);
    check_uop(double, exp10, oi1);
    check_uop(double, exp10, oi2);
    check_uop(double, exp10, oi3);
    check_uop(double, exp10, oi4);
    check_uop(double, exp10, oi5);
    check_uop(double, exp10, oi6);
    check_uop(double, exp10, oi7);
    check_uop(double, exp10, oi8);
    check_uop(double, exp10, oi9);
    check_uop(double, exp10, oi10);
    check_uop(double, exp10, oi11);
    check_uop(double, exp10, oi12);
    check_uop(double, exp10, oi13);
    check_uop(double, exp10, oi14);
    check_uop(double, exp10, oi15);
    check_uop(double, exp10, inf);
    check_uop(double, exp10, ozero_pinf);
    check_uop(double, exp10, ozero_ninf);
    check_uop(double, exp10, czero_pinf);
    check_uop(double, exp10, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, log, i1);
    check_uop(double, log, i2);
    check_uop(double, log, i5);
    check_uop(double, log, i6);
    check_uop(double, log, i7);
    check_uop(double, log, i8);
    check_uop(double, log, oi1);
    check_uop(double, log, oi2);
    check_uop(double, log, oi5);
    check_uop(double, log, oi6);
    check_uop(double, log, oi7);
    check_uop(double, log, oi8);
    check_uop(double, log, ozero_pinf);

    cout << "=====================" << endl;
    check_uop(double, log2, i1);
    check_uop(double, log2, i2);
    check_uop(double, log2, i5);
    check_uop(double, log2, i6);
    check_uop(double, log2, i7);
    check_uop(double, log2, i8);
    check_uop(double, log2, oi1);
    check_uop(double, log2, oi2);
    check_uop(double, log2, oi5);
    check_uop(double, log2, oi6);
    check_uop(double, log2, oi7);
    check_uop(double, log2, oi8);
    check_uop(double, log2, ozero_pinf);

    cout << "=====================" << endl;
    check_uop(double, log10, i1);
    check_uop(double, log10, i2);
    check_uop(double, log10, i5);
    check_uop(double, log10, i6);
    check_uop(double, log10, i7);
    check_uop(double, log10, i8);
    check_uop(double, log10, oi1);
    check_uop(double, log10, oi2);
    check_uop(double, log10, oi5);
    check_uop(double, log10, oi6);
    check_uop(double, log10, oi7);
    check_uop(double, log10, oi8);
    check_uop(double, log10, ozero_pinf);

    cout << "=====================" << endl;
    check_uop(double, sin, i1);
    check_uop(double, sin, i2);
    check_uop(double, sin, i3);
    check_uop(double, sin, i4);
    check_uop(double, sin, i5);
    check_uop(double, sin, i6);
    check_uop(double, sin, i7);
    check_uop(double, sin, i8);
    check_uop(double, sin, i9);
    check_uop(double, sin, i10);
    check_uop(double, sin, i11);
    check_uop(double, sin, i12);
    check_uop(double, sin, i13);
    check_uop(double, sin, i14);
    check_uop(double, sin, i15);
    check_uop(double, sin, oi1);
    check_uop(double, sin, oi2);
    check_uop(double, sin, oi3);
    check_uop(double, sin, oi4);
    check_uop(double, sin, oi5);
    check_uop(double, sin, oi6);
    check_uop(double, sin, oi7);
    check_uop(double, sin, oi8);
    check_uop(double, sin, oi9);
    check_uop(double, sin, oi10);
    check_uop(double, sin, oi11);
    check_uop(double, sin, oi12);
    check_uop(double, sin, oi13);
    check_uop(double, sin, oi14);
    check_uop(double, sin, oi15);
    check_uop(double, sin, inf);
    check_uop(double, sin, ozero_pinf);
    check_uop(double, sin, ozero_ninf);
    check_uop(double, sin, czero_pinf);
    check_uop(double, sin, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, cos, i1);
    check_uop(double, cos, i2);
    check_uop(double, cos, i3);
    check_uop(double, cos, i4);
    check_uop(double, cos, i5);
    check_uop(double, cos, i6);
    check_uop(double, cos, i7);
    check_uop(double, cos, i8);
    check_uop(double, cos, i9);
    check_uop(double, cos, i10);
    check_uop(double, cos, i11);
    check_uop(double, cos, i12);
    check_uop(double, cos, i13);
    check_uop(double, cos, i14);
    check_uop(double, cos, i15);
    check_uop(double, cos, oi1);
    check_uop(double, cos, oi2);
    check_uop(double, cos, oi3);
    check_uop(double, cos, oi4);
    check_uop(double, cos, oi5);
    check_uop(double, cos, oi6);
    check_uop(double, cos, oi7);
    check_uop(double, cos, oi8);
    check_uop(double, cos, oi9);
    check_uop(double, cos, oi10);
    check_uop(double, cos, oi11);
    check_uop(double, cos, oi12);
    check_uop(double, cos, oi13);
    check_uop(double, cos, oi14);
    check_uop(double, cos, oi15);
    check_uop(double, cos, inf);
    check_uop(double, cos, ozero_pinf);
    check_uop(double, cos, ozero_ninf);
    check_uop(double, cos, czero_pinf);
    check_uop(double, cos, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, tan, i1);
    check_uop(double, tan, i2);
    check_uop(double, tan, i3);
    check_uop(double, tan, i4);
    check_uop(double, tan, i5);
    check_uop(double, tan, i6);
    check_uop(double, tan, i7);
    check_uop(double, tan, i8);
    check_uop(double, tan, i9);
    check_uop(double, tan, i10);
    check_uop(double, tan, i11);
    check_uop(double, tan, i12);
    check_uop(double, tan, i13);
    check_uop(double, tan, i14);
    check_uop(double, tan, i15);
    check_uop(double, tan, oi1);
    check_uop(double, tan, oi2);
    check_uop(double, tan, oi3);
    check_uop(double, tan, oi4);
    check_uop(double, tan, oi5);
    check_uop(double, tan, oi6);
    check_uop(double, tan, oi7);
    check_uop(double, tan, oi8);
    check_uop(double, tan, oi9);
    check_uop(double, tan, oi10);
    check_uop(double, tan, oi11);
    check_uop(double, tan, oi12);
    check_uop(double, tan, oi13);
    check_uop(double, tan, oi14);
    check_uop(double, tan, oi15);
    check_uop(double, tan, inf);
    check_uop(double, tan, ozero_pinf);
    check_uop(double, tan, ozero_ninf);
    check_uop(double, tan, czero_pinf);
    check_uop(double, tan, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, asin, i11);
    check_uop(double, asin, i12);
    check_uop(double, asin, i13);
    check_uop(double, asin, i14);
    check_uop(double, asin, i15);
    check_uop(double, asin, oi11);
    check_uop(double, asin, oi12);
    check_uop(double, asin, oi13);
    check_uop(double, asin, oi14);
    check_uop(double, asin, oi15);

    cout << "=====================" << endl;
    check_uop(double, acos, i11);
    check_uop(double, acos, i12);
    check_uop(double, acos, i13);
    check_uop(double, acos, i14);
    check_uop(double, acos, i15);
    check_uop(double, acos, oi11);
    check_uop(double, acos, oi12);
    check_uop(double, acos, oi13);
    check_uop(double, acos, oi14);
    check_uop(double, acos, oi15);

    cout << "=====================" << endl;
    check_uop(double, atan, i1);
    check_uop(double, atan, i2);
    check_uop(double, atan, i3);
    check_uop(double, atan, i4);
    check_uop(double, atan, i5);
    check_uop(double, atan, i6);
    check_uop(double, atan, i7);
    check_uop(double, atan, i8);
    check_uop(double, atan, i9);
    check_uop(double, atan, i10);
    check_uop(double, atan, i11);
    check_uop(double, atan, i12);
    check_uop(double, atan, i13);
    check_uop(double, atan, i14);
    check_uop(double, atan, i15);
    check_uop(double, atan, oi1);
    check_uop(double, atan, oi2);
    check_uop(double, atan, oi3);
    check_uop(double, atan, oi4);
    check_uop(double, atan, oi5);
    check_uop(double, atan, oi6);
    check_uop(double, atan, oi7);
    check_uop(double, atan, oi8);
    check_uop(double, atan, oi9);
    check_uop(double, atan, oi10);
    check_uop(double, atan, oi11);
    check_uop(double, atan, oi12);
    check_uop(double, atan, oi13);
    check_uop(double, atan, oi14);
    check_uop(double, atan, oi15);
    check_uop(double, atan, inf);
    check_uop(double, atan, ozero_pinf);
    check_uop(double, atan, ozero_ninf);
    check_uop(double, atan, czero_pinf);
    check_uop(double, atan, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, sinh, i1);
    check_uop(double, sinh, i2);
    check_uop(double, sinh, i3);
    check_uop(double, sinh, i4);
    check_uop(double, sinh, i5);
    check_uop(double, sinh, i6);
    check_uop(double, sinh, i7);
    check_uop(double, sinh, i8);
    check_uop(double, sinh, i9);
    check_uop(double, sinh, i10);
    check_uop(double, sinh, i11);
    check_uop(double, sinh, i12);
    check_uop(double, sinh, i13);
    check_uop(double, sinh, i14);
    check_uop(double, sinh, i15);
    check_uop(double, sinh, oi1);
    check_uop(double, sinh, oi2);
    check_uop(double, sinh, oi3);
    check_uop(double, sinh, oi4);
    check_uop(double, sinh, oi5);
    check_uop(double, sinh, oi6);
    check_uop(double, sinh, oi7);
    check_uop(double, sinh, oi8);
    check_uop(double, sinh, oi9);
    check_uop(double, sinh, oi10);
    check_uop(double, sinh, oi11);
    check_uop(double, sinh, oi12);
    check_uop(double, sinh, oi13);
    check_uop(double, sinh, oi14);
    check_uop(double, sinh, oi15);
    check_uop(double, sinh, inf);
    check_uop(double, sinh, ozero_pinf);
    check_uop(double, sinh, ozero_ninf);
    check_uop(double, sinh, czero_pinf);
    check_uop(double, sinh, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, cosh, i1);
    check_uop(double, cosh, i2);
    check_uop(double, cosh, i3);
    check_uop(double, cosh, i4);
    check_uop(double, cosh, i5);
    check_uop(double, cosh, i6);
    check_uop(double, cosh, i7);
    check_uop(double, cosh, i8);
    check_uop(double, cosh, i9);
    check_uop(double, cosh, i10);
    check_uop(double, cosh, i11);
    check_uop(double, cosh, i12);
    check_uop(double, cosh, i13);
    check_uop(double, cosh, i14);
    check_uop(double, cosh, i15);
    check_uop(double, cosh, oi1);
    check_uop(double, cosh, oi2);
    check_uop(double, cosh, oi3);
    check_uop(double, cosh, oi4);
    check_uop(double, cosh, oi5);
    check_uop(double, cosh, oi6);
    check_uop(double, cosh, oi7);
    check_uop(double, cosh, oi8);
    check_uop(double, cosh, oi9);
    check_uop(double, cosh, oi10);
    check_uop(double, cosh, oi11);
    check_uop(double, cosh, oi12);
    check_uop(double, cosh, oi13);
    check_uop(double, cosh, oi14);
    check_uop(double, cosh, oi15);
    check_uop(double, cosh, inf);
    check_uop(double, cosh, ozero_pinf);
    check_uop(double, cosh, ozero_ninf);
    check_uop(double, cosh, czero_pinf);
    check_uop(double, cosh, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, tanh, i1);
    check_uop(double, tanh, i2);
    check_uop(double, tanh, i3);
    check_uop(double, tanh, i4);
    check_uop(double, tanh, i5);
    check_uop(double, tanh, i6);
    check_uop(double, tanh, i7);
    check_uop(double, tanh, i8);
    check_uop(double, tanh, i9);
    check_uop(double, tanh, i10);
    check_uop(double, tanh, i11);
    check_uop(double, tanh, i12);
    check_uop(double, tanh, i13);
    check_uop(double, tanh, i14);
    check_uop(double, tanh, i15);
    check_uop(double, tanh, oi1);
    check_uop(double, tanh, oi2);
    check_uop(double, tanh, oi3);
    check_uop(double, tanh, oi4);
    check_uop(double, tanh, oi5);
    check_uop(double, tanh, oi6);
    check_uop(double, tanh, oi7);
    check_uop(double, tanh, oi8);
    check_uop(double, tanh, oi9);
    check_uop(double, tanh, oi10);
    check_uop(double, tanh, oi11);
    check_uop(double, tanh, oi12);
    check_uop(double, tanh, oi13);
    check_uop(double, tanh, oi14);
    check_uop(double, tanh, oi15);
    check_uop(double, tanh, inf);
    check_uop(double, tanh, ozero_pinf);
    check_uop(double, tanh, ozero_ninf);
    check_uop(double, tanh, czero_pinf);
    check_uop(double, tanh, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, csc, i1);
    check_uop(double, csc, i2);
    check_uop(double, csc, i3);
    check_uop(double, csc, i4);
    check_uop(double, csc, i5);
    check_uop(double, csc, i6);
    check_uop(double, csc, i7);
    check_uop(double, csc, i8);
    check_uop(double, csc, i9);
    check_uop(double, csc, i10);
    check_uop(double, csc, i11);
    check_uop(double, csc, i12);
    check_uop(double, csc, i13);
    check_uop(double, csc, i14);
    check_uop(double, csc, i15);
    check_uop(double, csc, oi1);
    check_uop(double, csc, oi2);
    check_uop(double, csc, oi3);
    check_uop(double, csc, oi4);
    check_uop(double, csc, oi5);
    check_uop(double, csc, oi6);
    check_uop(double, csc, oi7);
    check_uop(double, csc, oi8);
    check_uop(double, csc, oi9);
    check_uop(double, csc, oi10);
    check_uop(double, csc, oi11);
    check_uop(double, csc, oi12);
    check_uop(double, csc, oi13);
    check_uop(double, csc, oi14);
    check_uop(double, csc, oi15);
    check_uop(double, csc, inf);
    check_uop(double, csc, ozero_pinf);
    check_uop(double, csc, ozero_ninf);
    check_uop(double, csc, czero_pinf);
    check_uop(double, csc, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, sec, i1);
    check_uop(double, sec, i2);
    check_uop(double, sec, i3);
    check_uop(double, sec, i4);
    check_uop(double, sec, i5);
    check_uop(double, sec, i6);
    check_uop(double, sec, i7);
    check_uop(double, sec, i8);
    check_uop(double, sec, i9);
    check_uop(double, sec, i10);
    check_uop(double, sec, i11);
    check_uop(double, sec, i12);
    check_uop(double, sec, i13);
    check_uop(double, sec, i14);
    check_uop(double, sec, i15);
    check_uop(double, sec, oi1);
    check_uop(double, sec, oi2);
    check_uop(double, sec, oi3);
    check_uop(double, sec, oi4);
    check_uop(double, sec, oi5);
    check_uop(double, sec, oi6);
    check_uop(double, sec, oi7);
    check_uop(double, sec, oi8);
    check_uop(double, sec, oi9);
    check_uop(double, sec, oi10);
    check_uop(double, sec, oi11);
    check_uop(double, sec, oi12);
    check_uop(double, sec, oi13);
    check_uop(double, sec, oi14);
    check_uop(double, sec, oi15);
    check_uop(double, sec, inf);
    check_uop(double, sec, ozero_pinf);
    check_uop(double, sec, ozero_ninf);
    check_uop(double, sec, czero_pinf);
    check_uop(double, sec, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, cot, i1);
    check_uop(double, cot, i2);
    check_uop(double, cot, i3);
    check_uop(double, cot, i4);
    check_uop(double, cot, i5);
    check_uop(double, cot, i6);
    check_uop(double, cot, i7);
    check_uop(double, cot, i8);
    check_uop(double, cot, i9);
    check_uop(double, cot, i10);
    check_uop(double, cot, i11);
    check_uop(double, cot, i12);
    check_uop(double, cot, i13);
    check_uop(double, cot, i14);
    check_uop(double, cot, i15);
    check_uop(double, cot, oi1);
    check_uop(double, cot, oi2);
    check_uop(double, cot, oi3);
    check_uop(double, cot, oi4);
    check_uop(double, cot, oi5);
    check_uop(double, cot, oi6);
    check_uop(double, cot, oi7);
    check_uop(double, cot, oi8);
    check_uop(double, cot, oi9);
    check_uop(double, cot, oi10);
    check_uop(double, cot, oi11);
    check_uop(double, cot, oi12);
    check_uop(double, cot, oi13);
    check_uop(double, cot, oi14);
    check_uop(double, cot, oi15);
    check_uop(double, cot, inf);
    check_uop(double, cot, ozero_pinf);
    check_uop(double, cot, ozero_ninf);
    check_uop(double, cot, czero_pinf);
    check_uop(double, cot, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, asinh, i1);
    check_uop(double, asinh, i2);
    check_uop(double, asinh, i3);
    check_uop(double, asinh, i4);
    check_uop(double, asinh, i5);
    check_uop(double, asinh, i6);
    check_uop(double, asinh, i7);
    check_uop(double, asinh, i8);
    check_uop(double, asinh, i9);
    check_uop(double, asinh, i10);
    check_uop(double, asinh, i11);
    check_uop(double, asinh, i12);
    check_uop(double, asinh, i13);
    check_uop(double, asinh, i14);
    check_uop(double, asinh, i15);
    check_uop(double, asinh, oi1);
    check_uop(double, asinh, oi2);
    check_uop(double, asinh, oi3);
    check_uop(double, asinh, oi4);
    check_uop(double, asinh, oi5);
    check_uop(double, asinh, oi6);
    check_uop(double, asinh, oi7);
    check_uop(double, asinh, oi8);
    check_uop(double, asinh, oi9);
    check_uop(double, asinh, oi10);
    check_uop(double, asinh, oi11);
    check_uop(double, asinh, oi12);
    check_uop(double, asinh, oi13);
    check_uop(double, asinh, oi14);
    check_uop(double, asinh, oi15);
    check_uop(double, asinh, inf);
    check_uop(double, asinh, ozero_pinf);
    check_uop(double, asinh, ozero_ninf);
    check_uop(double, asinh, czero_pinf);
    check_uop(double, asinh, czero_ninf);

    cout << "=====================" << endl;
    check_uop(double, acosh, i1);
    check_uop(double, acosh, i2);
    check_uop(double, acosh, i5);
    check_uop(double, acosh, i7);
    check_uop(double, acosh, i8);
    check_uop(double, acosh, oi1);
    check_uop(double, acosh, oi2);
    check_uop(double, acosh, oi5);
    check_uop(double, acosh, oi7);
    check_uop(double, acosh, oi8);

    cout << "=====================" << endl;
    check_uop(double, atanh, i10);
    check_uop(double, atanh, i11);
    check_uop(double, atanh, i12);
    check_uop(double, atanh, i13);
    check_uop(double, atanh, i14);
    check_uop(double, atanh, i15);
    check_uop(double, atanh, oi11);
    check_uop(double, atanh, oi12);
    check_uop(double, atanh, oi13);
    check_uop(double, atanh, oi14);
    check_uop(double, atanh, oi15);
}

int main() {
    initialize_util_module();
    double_interval_arith();
    double_interval_inf1();
    double_interval_inf2();
    double_interval_trans();
    finalize_util_module();
    return has_violations() ? 1 : 0;
}