Commit 77e7f380 by Heiko Becker

parent 8b9d6c33
 Variables real s1 in [0.0, 1.0], real s2 in [-0.5, 0.5], real s3 in [0, 0.5], real s4 in [0, 0.5]; Definitions r1 rnd64= (-1828.6) * s1 + (-1028.6) * s2 + (-2008.0) * s3 + (-104.0) * s4 ; Expressions ballbeam = r1 ;
 Variables real s1 in [-10.0, 10.0], real s2 in [-10.0, 10.0], real s3 in [-10.0, 10.0], real s4 in [-10.0, 10.0], real y1 in [-10.0, 10.0], real y2 in [-10.0, 10.0]; Expressions out1 rnd64= (-0.0429) * s1 + (-0.9170) * s2 + (-0.3299) * s3 + (-0.8206) * s4, out2 rnd64= 2.4908 * s1 + 0.0751 * s2 + 1.7481 * s3 + (-1.1433) * s4, state1 rnd64= 0.9670 * s1 + (-0.0019) * s2 + 0.0187 * s3 + (-0.0088) * s4 + 0.0447 * y1, state2 rnd64= (-0.0078) * s1 + 0.9052 * s2 + (-0.0181) * s3 + (-0.0392) * s4 + (-0.0003) * y1 + 0.0020 * y2, state3 rnd64= (-0.0830) * s1 + 0.0222 * s2 + 0.8620 * s3 + 0.0978 * s4 + 0.0170 * y1 + 0.0058 * y2, state4 rnd64= (-0.0133) * s1 + 0.0243 * s2 + (-0.0043) * s3 + 0.9824 * s4 + 0.0127 * y1 + 0.0059 * y2 ;
 Variables real s1 in [-1.0, 1.0], real s2 in [-1.0, 1.0], real s3 in [-1.0, 1.0], real s4 in [-1.0, 1.0], real y1 in [-1.0, 1.0], real y2 in [-1.0, 1.0]; Expressions out1 rnd64= (-0.058300) * s1 + (-0.908300) * s2 + (-0.325800) * s3 + (-0.872100) * s4, out2 rnd64= (2.463800) * s1 + (0.050400) * s2 + (1.709900) * s3 + (-1.165300) * s4, state1 rnd64= (0.934292) * s1 + (0.008415) * s2 + (-0.014106) * s3 + (0.023954) * s4 + (0.077400) * y1 + (-0.010300) * y2, state2 rnd64= (-0.006769) * s1 + (0.884924) * s2 + (-0.016066) * s3 + (-0.044019) * s4 + (-0.002200) * y1 + (0.022700) * y2, state3 rnd64= (-0.092148) * s1 + (-0.011039) * s2 + (0.853511) * s3 + (0.107537) * s4 + (0.026700) * y1 + (0.039800) * y2, state4 rnd64= (-0.036410) * s1 + (0.030194) * s2 + (-0.027155) * s3 + (1.004619) * s4 + (0.035600) * y1 + (0.000100) * y2 ;
 Variables real s1 in [-1.0, 1.0], real s2 in [-1.0, 1.0], real y1 in [-1.0, 1.0]; Expressions out1 rnd64= (-3.025300) * s1 + (-12.608900) * s2, state1 rnd64= (0.961270) * s1 + (-0.095962) * s2 + (0.013200) * y1, state2 rnd64= (-0.058217) * s1 + (0.727430) * s2 + (0.102100) * y1 ;
 Variables real u in [0.0, 1.0]; Definitions r1 rnd64= (1 - u) * (1 - u) * (1 - u) / 6.0, r2 rnd64= (3 * u*u*u - 6 * u*u + 4) / 6.0, r3 rnd64= (-3 * u*u*u + 3*u*u + 3*u + 1) / 6.0, r4 rnd64= -u*u*u / 6.0 ; Expressions bspline0 = r1, bspline1 = r2, bspline2 = r3, bspline3 = r4 ;
 Variables real k in [1.3806503e-23, 1.3806503e-23]; real T in [300.0, 300.0]; real a in [0.401, 0.401]; real b in [42.7e-6, 42.7e-6]; real N in [1000, 1000]; real p in [3.5e7, 3.5e7]; real V in [0.1, 0.5]; Definitions res rnd64= (p + a * (N / V) * (N / V)) * (V - N * b) - k * N * T; Expressions carbon_gas = res;
 Variables real s1 in [-1.0, 1.0], real s2 in [-1.0, 1.0], real s3 in [-1.0, 1.0], real y1 in [-1.0, 1.0]; Expressions out1 rnd64= (-0.112900) * s1 + (-0.021100) * s2 + (-0.009300) * s3, state1 rnd64= (0.960883) * s1 + (0.000949) * s2 + (-0.000004) * s3 + (0.039000) * y1, state2 rnd64= (-0.602449) * s1 + (0.899089) * s2 + (-0.013648) * s3 + (0.370000) * y1, state3 rnd64= (-0.009134) * s1 + (-0.011434) * s2 + (-0.002232) * s3 + (-0.017500) * y1 ;
 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(331.4) + rnd64(rnd64(0.6) * T))), r rnd64= rnd64(rnd64(-t1) * v) / ((t1 + u) * (t1 + u)) ; Expressions doppler1 = r ;
 Variables real x1 in [0, 6], real x2 in [0, 6], real x3 in [1, 5], real x4 in [0, 6], real x5 in [1, 5], real x6 in [0, 10]; Expressions floudas1 rnd64= -25 * ((x1 - 2) * (x1 - 2)) - ((x2 - 2) * (x2 - 2)) - ((x3 - 1) * (x3 - 1)) - ((x4 - 4) * (x4 - 4)) - ((x5 - 1) * (x5 - 1)) - ((x6 - 4) * (x6 - 4));
 Variables real x1 in [0, 3], real x2 in [0, 4]; Expressions floudas2 rnd64= -x1 - x2;
 Variables real x1 in [0, 1], real x2 in [0, 1], real x3 in [0, 1], real x4 in [0, 1], real x5 in [0, 1], real x6 in [0, 1], real x7 in [0, 1], real x8 in [0, 1], real x9 in [0, 1], real x10 in [0, 1]; Expressions floudas26 rnd64= 48*x1 + 42*x2 + 48*x3 + 45*x4 + 44*x5 + 41*x6 + 47*x7 + 42*x8 + 45*x9 + 46*x10 - 50*(x1*x1 + x2*x2 + x3*x3 + x4*x4 + x5*x5 + x6*x6 + x7*x7 + x8*x8 + x9*x9 + x10*x10);
 Variables real x1 in [0, 6], real x2 in [0, 6], real x3 in [1, 5], real x4 in [0, 6], real x5 in [1, 5], real x6 in [0, 10]; Expressions floudas33 rnd64= (-1) * (25 * (x1 - 2)*(x1 - 2)) - (x2 - 2)* (x2 - 2) - (x3 - 1)*(x3 - 1) - (x4 - 4)*(x4 - 4) - (x5 - 1)*(x5 - 1) - (x6 - 4)* (x6 - 4);
 Variables real x1 in [0, 2], real x2 in [0, 2], real x3 in [0, 3]; Expressions floudas34 rnd64= -2 * x1 + x2 - x3;
 Variables real x1 in [0, 3], real x2 in [0, 4]; Expressions floudas46 rnd64= (-1 * x1) - x2;
 Variables real x1 in [0, 2], real x2 in [0, 3]; Expressions floudas47 rnd64= -12 * x1 - 7 * x2 + x2 * x2;
 Variables real x1_0 in [-5, 5], real x2_0 in [-5, 5]; Definitions x1 rnd64= x1_0, x2 rnd64= x2_0, t1 rnd64= x1*x1 + x2, t2 = rnd64(rnd64(x1 + rnd64(x2*x2))), r rnd64= (t1 - 11)*(t1 - 11) + rnd64(rnd64(t2 - 7)*rnd64(t2 - 7)) ; Expressions himmilbeauLet = r ;
 Variables real s1 in [-50, 50], real s2 in [-10, 10], real s3 in [-0.785, 0.785], real s4 in [-0.785, 0.785]; Definitions r rnd64= 1.0000 * s1 + 1.6567 * s2 + (-18.6854) * s3 + (-3.4594) * s4 ; Expressions invertedPendulum = r ;
 Variables real x1_0 in [4, 6.36], real x2_0 in [4, 6.36], real x3_0 in [4, 6.36], real x4_0 in [4, 6.36], real x5_0 in [4, 6.36], real x6_0 in [4, 6.36]; Definitions x1 rnd64= x1_0, x2 rnd64= x2_0, x3 rnd64= x3_0, x4 rnd64= x4_0, x5 rnd64= x5_0, x6 rnd64= x6_0, t0 = rnd64(rnd64(rnd64(rnd64(rnd64(rnd64(-1 * x1) + x2) + x3) - x4) + x5) + x6), r0 rnd64= (((((x2 * x5) + (x3 * x6)) - (x2 * x3)) - (x5 * x6)) + rnd64(x1 * t0)), t1 = rnd64(rnd64(rnd64(rnd64(-1 * x1) + x2) + x3) - x4), r1 rnd64= ((((((((x1 * x4) * t1) + (x2 * ((rnd64(x1 - x2) + x3) + x4))) + (x3 * ((rnd64(x1 + x2) - x3) + x4))) - ((x2 * x3) * x4)) - (x1 * x3)) - rnd64(x1 * x2)) - x4), t2 = rnd64(rnd64(rnd64(rnd64(rnd64(rnd64(-1 * x1) + x2) + x3) - x4) + x5) + x6), t3 = rnd64(rnd64(rnd64(rnd64(rnd64(x1 - x2) + x3) + x4) - x5) + x6), r2 rnd64= ((((((((x1 * x4) * t2) + ((x2 * x5) * t3)) + ((x3 * x6) * ((((rnd64(x1 + x2) - x3) + x4) + x5) - x6))) - ((x2 * x3) * x4)) - ((x1 * x3) * x5)) - (rnd64(x1 * x2) * x6)) - ((x4 * x5) * x6)) ; Expressions kepler0 = r0, kepler1 = r1, kepler2 = r2;
 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)))