Commit 647571c5 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add missing FPTaylor benchmarks

parent 19c59e6b
Variables
real u0 in [-100, 100],
real v0 in [20, 20000],
real T0 in [-30, 50];
Definitions
u rnd64= u0,
v rnd64= v0,
T rnd64= T0,
t1 = rnd64(rnd64((rnd64(0.6) * T) + rnd64(331.4))),
r rnd64= ((-t1) * v) / ((t1 + u) * (t1 + u))
;
Expressions
doppler1 = r
;
Variables
real x01 in [-5,5],
real x02 in [-20,20];
Definitions
x1 rnd64= x01,
x2 rnd64= x02,
t rnd64 = (3*x1*x1 + 2*x2 - x1),
r rnd64 = x1 + ((2*x1*(t/(x1*x1 + 1)) * (t/(x1*x1 + 1) - 3) + x1*x1*(4*(t/(x1*x1 + 1))-6)) *
(x1*x1 + 1) + 3*x1*x1*(t/(x1*x1 + 1)) + x1*x1*x1 + x1 +
3 * ((3*x1*x1 + 2*x2 -x1)/(x1*x1 + 1)))
;
Expressions
jetengine = r
;
Base path: /home/hbecker/Git_Repos/FPTaylor
Config file: /home/hbecker/Git_Repos/FPTaylor/default.cfg
default-rnd = rnd64
nlopt-cc = gcc -std=c99 -O3
opt-exact = true
develop = false
log-append-date = start
uncertainty = false
rel-error = false
opt-approx = false
proof-record = false
find-bounds = true
proof-dir = proofs
opt-f-abs-tol = 0.01
fail-on-exception = true
print-opt-lower-bounds = true
bb-compile = {base}/b_and_b/compile.sh {base} {input} {out}
z3-python-lib =
opt-x-abs-tol = 0.01
export-error-bounds =
opt-f-rel-tol = 0.01
opt-x-rel-tol = 0.0
rel-error-threshold = 0.0001
bb-alg = opt0
log-base-dir = log
intermediate-opt = false
z3-interval-bounds = true
opt-max-iters = 1000000
abs-error = true
z3-bin =
maxima-simplification = false
debug = true
export-error-bounds-data =
fp-power2-model = true
opt = bb
default-var-type = float64
verbosity = 2
ulp-error = false
opt-timeout = 10000
nlopt-lib = -lnlopt -lm
tmp-base-dir = tmp
unique-indices = false
z3-seed = 0
tmp-date = false
z3-python-cmd = python
const-approx-real-vars = false
eval_const_expr: (-(100))
result: -100
eval_const_expr: 100
result: 100
eval_const_expr: 0
result: 0
eval_const_expr: 100
result: 100
eval_const_expr: (-(100))
result: -100
eval_const_expr: 20
result: 20
eval_const_expr: 20000
result: 20000
eval_const_expr: 0
result: 0
eval_const_expr: 20000
result: 20000
eval_const_expr: 20
result: 20
eval_const_expr: (-(30))
result: -30
eval_const_expr: 50
result: 50
eval_const_expr: 0
result: 0
eval_const_expr: 50
result: 50
eval_const_expr: (-(30))
result: -30
|tasks| = 1
Processing: doppler1
*************************************
Taylor form for: rnd64((rnd64((rnd64((-(rnd64(rnd64((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))))))) * rnd64(v0))) / rnd64((rnd64((rnd64(rnd64(rnd64((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))))) + rnd64(rnd64(u0)))) * rnd64((rnd64(rnd64(rnd64((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))))) + rnd64(rnd64(u0))))))))
Conservative bound: [-158.719144, -0.029442]
Simplified rounding: rnd64((rnd64(((-(rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))))) * rnd64(v0))) / rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0))) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0)))))))
Building Taylor forms...
const_rnd_form
precise_const_rnd_form
Inexact constant: (1657/5); err = (1024/5)
const_rnd_form
precise_const_rnd_form
Inexact constant: (3/5); err = (1/5)
var_rnd_form
mul_form
rounded_form
add_form
rounded_form
neg_form
var_rnd_form
mul_form
rounded_form
const_rnd_form
precise_const_rnd_form
Inexact constant: (1657/5); err = (1024/5)
const_rnd_form
precise_const_rnd_form
Inexact constant: (3/5); err = (1/5)
var_rnd_form
mul_form
rounded_form
add_form
rounded_form
var_rnd_form
add_form
rounded_form
const_rnd_form
precise_const_rnd_form
Inexact constant: (1657/5); err = (1024/5)
const_rnd_form
precise_const_rnd_form
Inexact constant: (3/5); err = (1/5)
var_rnd_form
mul_form
rounded_form
add_form
rounded_form
var_rnd_form
add_form
rounded_form
mul_form
rounded_form
div_form
inv_form
mul_form
rounded_form
Simplifying Taylor forms...
success
v0 = (((-(((1657/5) + ((3/5) * T0)))) * v0) * (1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))
-1 (58): exp = -53: (2486717035483741/309485009821345068724781056)
1 (24): exp = -53: ((((((((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * (1024/5)) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * (T0 * (1/5))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * (1024/5)) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * (T0 * (1/5))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))) + ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * (v0 * (-((1024/5)))))) + ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * (v0 * (-((T0 * (1/5)))))))
2 (26): exp = -53: (((((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * ((3/5) * floor_power2(T0))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * ((3/5) * floor_power2(T0))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))) + ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * (v0 * (-(((3/5) * floor_power2(T0)))))))
3 (28): exp = -53: (((((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2((((3/5) * T0) + interval(-3.24185123190545780801e-15, 3.24185123190545780801e-15)))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2((((3/5) * T0) + interval(-3.24185123190545780801e-15, 3.24185123190545780801e-15)))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))) + ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * (v0 * (-(floor_power2((((3/5) * T0) + interval(-3.24185123190545780801e-15, 3.24185123190545780801e-15))))))))
4 (30): exp = -53: (((((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2((((1657/5) + ((3/5) * T0)) + interval(-2.77555756156289166660e-14, 2.77555756156289166660e-14)))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2((((1657/5) + ((3/5) * T0)) + interval(-2.77555756156289166660e-14, 2.77555756156289166660e-14)))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))) + ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * (v0 * (-(floor_power2((((1657/5) + ((3/5) * T0)) + interval(-2.77555756156289166660e-14, 2.77555756156289166660e-14))))))))
5 (9): exp = -53: ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * ((-(((1657/5) + ((3/5) * T0)))) * floor_power2(v0)))
6 (11): exp = -53: ((1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))) * floor_power2((((-(((1657/5) + ((3/5) * T0)))) * v0) + interval(-1.78092847136213132150e-09, 1.78092847136213132150e-09))))
7 (32): exp = -53: ((((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2(u0)) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2(u0)) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))))
8 (33): exp = -53: ((((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2(((((1657/5) + ((3/5) * T0)) + u0) + interval(-6.32827124036339354259e-14, 6.32827124036339354259e-14)))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))) + (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((((((1657/5) + ((3/5) * T0)) + u0) * floor_power2(((((1657/5) + ((3/5) * T0)) + u0) + interval(-6.32827124036339354259e-14, 6.32827124036339354259e-14)))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0))))))))
9 (36): exp = -53: (((-(((1657/5) + ((3/5) * T0)))) * v0) * (-((floor_power2((((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) + interval(-8.46248404684502588932e-11, 8.46248404684502588932e-11))) / (((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)) * ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))))))
10 (40): exp = -53: floor_power2(((((-(((1657/5) + ((3/5) * T0)))) * v0) * (1 / ((((1657/5) + ((3/5) * T0)) + u0) * (((1657/5) + ((3/5) * T0)) + u0)))) + interval(-3.94993705872679559268e-13, 3.94993705872679559268e-13)))
Corresponding original subexpressions:
1: rnd64(0)
2: rnd64(T0)
3: rnd64((rnd64((3/5)) * rnd64(T0)))
4: rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0)))))
5: rnd64(v0)
6: rnd64(((-(rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))))) * rnd64(v0)))
7: rnd64(u0)
8: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0)))
9: rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0))) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0)))))
10: rnd64((rnd64(((-(rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))))) * rnd64(v0))) / rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0))) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((1657/5)) + rnd64((rnd64((3/5)) * rnd64(T0))))) + rnd64(u0)))))))
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 427, max = 23): 427
min = -1.389561e+02 (lower_min = -1.375714e+02)
max = -3.169713e-02 (lower_max = -3.967690e-02)
subopt = 1.384675e+00 (1.0%)
bounds: [-1.389561e+02, -3.169713e-02]
Computing absolute errors
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 0): 0
min = 8.035016e-12 (lower_min = 8.035016e-12)
max = 8.035016e-12 (lower_max = 8.035016e-12)
subopt = 0.000000e+00 (0.0%)
rmin(result = 8.035016e-12, lower = 8.035016e-12), rmax(result = 8.035016e-12, lower = 8.035016e-12)
-1: exp = -53: 8.035016e-12 (low = 8.035016e-12, subopt = 0.0%)
Solving the exact optimization problem
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 7313): 7313
min = 0.000000e+00 (lower_min = 0.000000e+00)
max = 1.096961e+03 (lower_max = 1.088234e+03)
subopt = 8.726599e+00 (0.8%)
exact bound (exp = -53): 1.096961e+03 (low = 1.088234e+03, subopt = 0.8%)
total2: 8.920660e-28 (low = 8.920660e-28, subopt = 0.0%)
exact total: 1.217871e-13 (low = 1.208183e-13, subopt = 0.8%)
Elapsed time: 1.36586
*************************************
-------------------------------------------------------------------------------
Problem: doppler1
Optimization lower bounds for error models:
The absolute error model (exact): 1.208183e-13 (suboptimality = 0.8%)
Bounds (without rounding): [-1.389561e+02, -3.169713e-02]
Bounds (floating-point): [-1.38956107612810029650e+02, -3.16971265341684516059e-02]
Absolute error (exact): 1.217871e-13
Elapsed time: 1.37
Base path: /home/hbecker/Git_Repos/FPTaylor
Config file: /home/hbecker/Git_Repos/FPTaylor/default.cfg
default-rnd = rnd64
nlopt-cc = gcc -std=c99 -O3
opt-exact = true
develop = false
log-append-date = start
uncertainty = false
rel-error = false
opt-approx = false
proof-record = false
find-bounds = true
proof-dir = proofs
opt-f-abs-tol = 0.01
fail-on-exception = true
print-opt-lower-bounds = true
bb-compile = {base}/b_and_b/compile.sh {base} {input} {out}
z3-python-lib =
opt-x-abs-tol = 0.01
export-error-bounds =
opt-f-rel-tol = 0.01
opt-x-rel-tol = 0.0
rel-error-threshold = 0.0001
bb-alg = opt0
log-base-dir = log
intermediate-opt = false
z3-interval-bounds = true
opt-max-iters = 1000000
abs-error = true
z3-bin =
maxima-simplification = false
debug = true
export-error-bounds-data =
fp-power2-model = true
opt = bb
default-var-type = float64
verbosity = 2
ulp-error = false
opt-timeout = 10000
nlopt-lib = -lnlopt -lm
tmp-base-dir = tmp
unique-indices = false
z3-seed = 0
tmp-date = false
z3-python-cmd = python
const-approx-real-vars = false
eval_const_expr: (-(5))
result: -5
eval_const_expr: 5
result: 5
eval_const_expr: 0
result: 0
eval_const_expr: 5
result: 5
eval_const_expr: (-(5))
result: -5
eval_const_expr: (-(5))
result: -5
eval_const_expr: 5
result: 5
eval_const_expr: 0
result: 0
eval_const_expr: 5
result: 5
eval_const_expr: (-(5))
result: -5
|tasks| = 1
Processing: himmilbeauLet
*************************************
Taylor form for: rnd64((rnd64((rnd64((rnd64(rnd64((rnd64((rnd64(rnd64(x1_0)) * rnd64(rnd64(x1_0)))) + rnd64(rnd64(x2_0))))) - rnd64(11))) * rnd64((rnd64(rnd64((rnd64((rnd64(rnd64(x1_0)) * rnd64(rnd64(x1_0)))) + rnd64(rnd64(x2_0))))) - rnd64(11))))) + rnd64((rnd64((rnd64(rnd64((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0)))))) - 7)) * rnd64((rnd64(rnd64((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0)))))) - 7))))))
Conservative bound: [-0.000000, 890.000000]
Simplified rounding: rnd[64,ne,1.00,-53,0]((rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11)) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11)))) + rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7)) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7))))))
Building Taylor forms...
var_rnd_form
var_rnd_form
mul_form
rounded_form
var_rnd_form
add_form
rounded_form
const_form
sub_form
rounded_form
var_rnd_form
var_rnd_form
mul_form
rounded_form
var_rnd_form
add_form
rounded_form
const_form
sub_form
rounded_form
mul_form
rounded_form
var_rnd_form
var_rnd_form
var_rnd_form
mul_form
rounded_form
add_form
rounded_form
const_form
sub_form
rounded_form
var_rnd_form
var_rnd_form
var_rnd_form
mul_form
rounded_form
add_form
rounded_form
const_form
sub_form
rounded_form
mul_form
rounded_form
add_form
rounded_form
Simplifying Taylor forms...
success
v0 = (((((x1_0 * x1_0) + x2_0) - 11) * (((x1_0 * x1_0) + x2_0) - 11)) + (((x1_0 + (x2_0 * x2_0)) - 7) * ((x1_0 + (x2_0 * x2_0)) - 7)))
-1 (68): exp = -53: (2511284557840387/1237940039285380274899124224)
1 (12): exp = -53: (((((((((x1_0 * x1_0) + x2_0) - 11) * (x1_0 * floor_power2(x1_0))) + ((((x1_0 * x1_0) + x2_0) - 11) * (x1_0 * floor_power2(x1_0)))) + ((((x1_0 * x1_0) + x2_0) - 11) * (x1_0 * floor_power2(x1_0)))) + ((((x1_0 * x1_0) + x2_0) - 11) * (x1_0 * floor_power2(x1_0)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2(x1_0))) + (((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2(x1_0)))
2 (14): exp = -53: (((((x1_0 * x1_0) + x2_0) - 11) * floor_power2(((x1_0 * x1_0) + interval(-4.44089209850062695056e-15, 4.44089209850062695056e-15)))) + ((((x1_0 * x1_0) + x2_0) - 11) * floor_power2(((x1_0 * x1_0) + interval(-4.44089209850062695056e-15, 4.44089209850062695056e-15)))))
3 (16): exp = -53: (((((((((x1_0 * x1_0) + x2_0) - 11) * floor_power2(x2_0)) + ((((x1_0 * x1_0) + x2_0) - 11) * floor_power2(x2_0))) + (((x1_0 + (x2_0 * x2_0)) - 7) * (x2_0 * floor_power2(x2_0)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * (x2_0 * floor_power2(x2_0)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * (x2_0 * floor_power2(x2_0)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * (x2_0 * floor_power2(x2_0))))
4 (17): exp = -53: (((((x1_0 * x1_0) + x2_0) - 11) * floor_power2((((x1_0 * x1_0) + x2_0) + interval(-6.66133814775094003140e-15, 6.66133814775094003140e-15)))) + ((((x1_0 * x1_0) + x2_0) - 11) * floor_power2((((x1_0 * x1_0) + x2_0) + interval(-6.66133814775094003140e-15, 6.66133814775094003140e-15)))))
5 (19): exp = -53: (((((x1_0 * x1_0) + x2_0) - 11) * floor_power2(((((x1_0 * x1_0) + x2_0) - 11) + interval(-8.43769498715119128494e-15, 8.43769498715119128494e-15)))) + ((((x1_0 * x1_0) + x2_0) - 11) * floor_power2(((((x1_0 * x1_0) + x2_0) - 11) + interval(-8.43769498715119128494e-15, 8.43769498715119128494e-15)))))
6 (22): exp = -53: floor_power2((((((x1_0 * x1_0) + x2_0) - 11) * (((x1_0 * x1_0) + x2_0) - 11)) + interval(-3.88133969408954928480e-13, 3.88133969408954928480e-13)))
7 (38): exp = -53: ((((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2(((x2_0 * x2_0) + interval(-4.44089209850062695056e-15, 4.44089209850062695056e-15)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2(((x2_0 * x2_0) + interval(-4.44089209850062695056e-15, 4.44089209850062695056e-15)))))
8 (40): exp = -53: ((((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2(((x1_0 + (x2_0 * x2_0)) + interval(-6.66133814775094003140e-15, 6.66133814775094003140e-15)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2(((x1_0 + (x2_0 * x2_0)) + interval(-6.66133814775094003140e-15, 6.66133814775094003140e-15)))))
9 (42): exp = -53: ((((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2((((x1_0 + (x2_0 * x2_0)) - 7) + interval(-8.43769498715119128494e-15, 8.43769498715119128494e-15)))) + (((x1_0 + (x2_0 * x2_0)) - 7) * floor_power2((((x1_0 + (x2_0 * x2_0)) - 7) + interval(-8.43769498715119128494e-15, 8.43769498715119128494e-15)))))
10 (45): exp = -53: floor_power2(((((x1_0 + (x2_0 * x2_0)) - 7) * ((x1_0 + (x2_0 * x2_0)) - 7)) + interval(-4.69846384021366550830e-13, 4.69846384021366550830e-13)))
11 (47): exp = -53: floor_power2(((((((x1_0 * x1_0) + x2_0) - 11) * (((x1_0 * x1_0) + x2_0) - 11)) + (((x1_0 + (x2_0 * x2_0)) - 7) * ((x1_0 + (x2_0 * x2_0)) - 7))) + interval(-9.43245481721534006486e-13, 9.43245481721534006486e-13)))
Corresponding original subexpressions:
1: rnd64(x1_0)
2: rnd64((rnd64(x1_0) * rnd64(x1_0)))
3: rnd64(x2_0)
4: rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0)))
5: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11))
6: rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11)) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11))))
7: rnd64((rnd64(x2_0) * rnd64(x2_0)))
8: rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0)))))
9: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7))
10: rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7)) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7))))
11: rnd[64,ne,1.00,-53,0]((rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11)) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64((rnd64(x1_0) * rnd64(x1_0))) + rnd64(x2_0))) - 11)))) + rnd64((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7)) * rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(x1_0) + rnd64((rnd64(x2_0) * rnd64(x2_0))))) - 7))))))
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 261, max = 3): 261
min = -8.522868e-03 (lower_min = 8.885356e-05)
max = 8.900000e+02 (lower_max = 8.900000e+02)
subopt = 2.273737e-12 (0.0%)
bounds: [-8.522868e-03, 8.900000e+02]
Computing absolute errors
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 0): 0
min = 2.028600e-12 (lower_min = 2.028600e-12)
max = 2.028600e-12 (lower_max = 2.028600e-12)
subopt = 0.000000e+00 (0.0%)
rmin(result = 2.028600e-12, lower = 2.028600e-12), rmax(result = 2.028600e-12, lower = 2.028600e-12)
-1: exp = -53: 2.028600e-12 (low = 2.028600e-12, subopt = 0.0%)
Solving the exact optimization problem
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 3): 3
min = 0.000000e+00 (lower_min = 0.000000e+00)
max = 9.008000e+03 (lower_max = 9.008000e+03)
subopt = 3.092282e-11 (0.0%)
exact bound (exp = -53): 9.008000e+03 (low = 9.008000e+03, subopt = 0.0%)
total2: 2.252198e-28 (low = 2.252198e-28, subopt = 0.0%)
exact total: 1.000089e-12 (low = 1.000089e-12, subopt = 0.0%)
Elapsed time: 0.51479
*************************************
-------------------------------------------------------------------------------
Problem: himmilbeauLet
Optimization lower bounds for error models:
The absolute error model (exact): 1.000089e-12 (suboptimality = 0.0%)
Bounds (without rounding): [-8.522868e-03, 8.900000e+02]
Bounds (floating-point): [-8.52286815743381019617e-03, 8.90000000000002160050e+02]
Absolute error (exact): 1.000089e-12
Elapsed time: 0.51
Base path: /home/hbecker/Git_Repos/FPTaylor
Config file: /home/hbecker/Git_Repos/FPTaylor/default.cfg
default-rnd = rnd64
nlopt-cc = gcc -std=c99 -O3
opt-exact = true
develop = false
log-append-date = start
uncertainty = false
rel-error = false
opt-approx = false
proof-record = false
find-bounds = true
proof-dir = proofs
opt-f-abs-tol = 0.01
fail-on-exception = true
print-opt-lower-bounds = true
bb-compile = {base}/b_and_b/compile.sh {base} {input} {out}
z3-python-lib =
opt-x-abs-tol = 0.01
export-error-bounds =
opt-f-rel-tol = 0.01
opt-x-rel-tol = 0.0
rel-error-threshold = 0.0001
bb-alg = opt0
log-base-dir = log
intermediate-opt = false
z3-interval-bounds = true
opt-max-iters = 1000000
abs-error = true
z3-bin =
maxima-simplification = false
debug = true
export-error-bounds-data =
fp-power2-model = true
opt = bb
default-var-type = float64
verbosity = 2
ulp-error = false
opt-timeout = 10000
nlopt-lib = -lnlopt -lm
tmp-base-dir = tmp
unique-indices = false
z3-seed = 0
tmp-date = false
z3-python-cmd = python
const-approx-real-vars = false
eval_const_expr: (-(15))
result: -15
eval_const_expr: 15
result: 15
eval_const_expr: 0
result: 0
eval_const_expr: 15
result: 15
eval_const_expr: (-(15))
result: -15
eval_const_expr: (-(15))
result: -15
eval_const_expr: 15
result: 15
eval_const_expr: 0
result: 0
eval_const_expr: 15
result: 15
eval_const_expr: (-(15))
result: -15
eval_const_expr: (-(15))
result: -15
eval_const_expr: 15
result: 15
eval_const_expr: 0
result: 0
eval_const_expr: 15
result: 15
eval_const_expr: (-(15))
result: -15
|tasks| = 2
Processing: rigidBody1
*************************************
Taylor form for: rnd64((rnd64((rnd64((rnd64((rnd64((-(rnd64(rnd64(x1_0))))) * rnd64(rnd64(x2_0)))) - rnd64((rnd64((2 * rnd64(x2_0))) * rnd64(rnd64(x3_0)))))) - rnd64(rnd64(x1_0)))) - rnd64(rnd64(x3_0))))
Conservative bound: [-705.000000, 705.000000]
Simplified rounding: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(((-(rnd64(x1_0))) * rnd64(x2_0))) - rnd64(((2 * rnd64(x2_0)) * rnd64(x3_0))))) - rnd64(x1_0))) - rnd64(x3_0)))
Building Taylor forms...
var_rnd_form
neg_form
var_rnd_form
mul_form
rounded_form
const_form
var_rnd_form
mul_form
var_rnd_form
mul_form
rounded_form
sub_form
rounded_form
var_rnd_form
sub_form
rounded_form
var_rnd_form
sub_form
rounded_form
Simplifying Taylor forms...
success
v0 = (((((-(x1_0)) * x2_0) - ((2 * x2_0) * x3_0)) - x1_0) - x3_0)
-1 (26): exp = -53: (3377699720527873/158456325028528675187087900672)
1 (1): exp = -53: ((x2_0 * (-(floor_power2(x1_0)))) + (-(floor_power2(x1_0))))
2 (2): exp = -53: (((-(x1_0)) * floor_power2(x2_0)) + (-((x3_0 * (2 * floor_power2(x2_0))))))
3 (4): exp = -53: floor_power2((((-(x1_0)) * x2_0) + interval(-2.66453525910037601256e-14, 2.66453525910037601256e-14)))
4 (8): exp = -53: ((-(((2 * x2_0) * floor_power2(x3_0)))) + (-(floor_power2(x3_0))))
5 (10): exp = -53: (-(floor_power2((((2 * x2_0) * x3_0) + interval(-5.32907051820075202512e-14, 5.32907051820075202512e-14)))))
6 (12): exp = -53: floor_power2(((((-(x1_0)) * x2_0) - ((2 * x2_0) * x3_0)) + interval(-1.22568621918617332550e-13, 1.22568621918617332550e-13)))
7 (15): exp = -53: floor_power2((((((-(x1_0)) * x2_0) - ((2 * x2_0) * x3_0)) - x1_0) + interval(-1.80300219199125472652e-13, 1.80300219199125472652e-13)))
8 (18): exp = -53: floor_power2(((((((-(x1_0)) * x2_0) - ((2 * x2_0) * x3_0)) - x1_0) - x3_0) + interval(-2.38031816479633612754e-13, 2.38031816479633612754e-13)))
Corresponding original subexpressions:
1: rnd64(x1_0)
2: rnd64(x2_0)
3: rnd64(((-(rnd64(x1_0))) * rnd64(x2_0)))
4: rnd64(x3_0)
5: rnd64(((2 * rnd64(x2_0)) * rnd64(x3_0)))
6: rnd[64,ne,1.00,-53,0]((rnd64(((-(rnd64(x1_0))) * rnd64(x2_0))) - rnd64(((2 * rnd64(x2_0)) * rnd64(x3_0)))))
7: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(((-(rnd64(x1_0))) * rnd64(x2_0))) - rnd64(((2 * rnd64(x2_0)) * rnd64(x3_0))))) - rnd64(x1_0)))
8: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd64(((-(rnd64(x1_0))) * rnd64(x2_0))) - rnd64(((2 * rnd64(x2_0)) * rnd64(x3_0))))) - rnd64(x1_0))) - rnd64(x3_0)))
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 137): 137
min = -7.050000e+02 (lower_min = -7.050000e+02)
max = 7.050000e+02 (lower_max = 6.994922e+02)
subopt = 5.507813e+00 (0.8%)
bounds: [-7.050000e+02, 7.050000e+02]
Computing absolute errors
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 0): 0
min = 2.131628e-14 (lower_min = 2.131628e-14)
max = 2.131628e-14 (lower_max = 2.131628e-14)
subopt = 0.000000e+00 (0.0%)
rmin(result = 2.131628e-14, lower = 2.131628e-14), rmax(result = 2.131628e-14, lower = 2.131628e-14)
-1: exp = -53: 2.131628e-14 (low = 2.131628e-14, subopt = 0.0%)
Solving the exact optimization problem
bb_opt: x_abs_tol = 1.000000e-02, f_rel_tol = 1.000000e-02, f_abs_tol = 1.000000e-02, iters = 1000000
iterations(min = 0, max = 0): 0
min = 0.000000e+00 (lower_min = 0.000000e+00)
max = 2.656000e+03 (lower_max = 2.656000e+03)
subopt = 4.547474e-12 (0.0%)
exact bound (exp = -53): 2.656000e+03 (low = 2.656000e+03, subopt = 0.0%)
total2: 2.366583e-30 (low = 2.366583e-30, subopt = 0.0%)
exact total: 2.948752e-13 (low = 2.948752e-13, subopt = 0.0%)
Elapsed time: 0.45887
Processing: rigidBody2
*************************************
Taylor form for: rnd64((rnd64((rnd64((rnd64((rnd64((2 * rnd64(rnd64((rnd64((rnd64(x1_0) * rnd64(x2_0))) * rnd64(x3_0)))))) + rnd64((rnd64((rnd64(3) * rnd64(rnd64(x3_0)))) * rnd64(rnd64(x3_0)))))) - rnd64((rnd64(x2_0) * rnd64(rnd64((rnd64((rnd64(x1_0) * rnd64(x2_0))) * rnd64(x3_0)))))))) + rnd64((rnd64((rnd64(3) * rnd64(rnd64(x3_0)))) * rnd64(rnd64(x3_0)))))) - rnd64(rnd64(x2_0))))
Conservative bound: [-58740.000000, 58740.000000]
Simplified rounding: rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0]((rnd[64,ne,1.00,-53,0](((2 * rnd64((rnd64((rnd64(x1_0) * rnd64(x2_0))) * rnd64(x3_0)))) + rnd64((rnd64((3 * rnd64(x3_0))) * rnd64(x3_0))))) - rnd64((rnd64(x2_0) * rnd64((rnd64((rnd64(x1_0) * rnd64(x2_0))) * rnd64(x3_0))))))) + rnd64((rnd64((3 * rnd64(x3_0))) * rnd64(x3_0))))) - rnd64(x2_0)))
Building Taylor forms...
const_form
var_rnd_form
var_rnd_form
mul_form
rounded_form
var_rnd_form
mul_form
rounded_form
mul_form
const_form
var_rnd_form
mul_form
rounded_form
var_rnd_form
mul_form
rounded_form
add_form
rounded_form
var_rnd_form
var_rnd_form
var_rnd_form