benchmarks.jsonp

load_benchmarks([{"body":"(sqrt (+ (* x x) (* y y)))","arguments":["x","y"],"operators":["sqrt","+","*"],":spec":"(hypot x y)",":pre":"(and (<= 1 x 100) (<= 1 y 100))",":name":"carthesianToPolar, radius","core_fptaylor":"{\nVariables\n\treal x in [1, 100];\n\treal y in [1, 100];\n\nExpressions\n\tcarthesianToPolar$44$$32$radius rnd64= sqrt(((x * x) + (y * y)));\n}\n","core":"(FPCore\n (x y)\n :name\n \"carthesianToPolar, radius\"\n :pre\n (and (<= 1 x 100) (<= 1 y 100))\n :spec\n (hypot x y)\n (sqrt (+ (* x x) (* y y))))"},{"body":"(let ((pi 314159265359/100000000000) (radiant (atan (/ y x))))\n  (* radiant (/ 180 pi)))","arguments":["x","y"],"operators":["let","atan","/","*"],":spec":"(* (atan2 y x) (/ 180 PI))",":pre":"(and (<= 1 x 100) (<= 1 y 100))",":name":"carthesianToPolar, theta","core_fptaylor":"{\nVariables\n\treal x in [1, 100];\n\treal y in [1, 100];\n\nDefinitions\n\tpi rnd64= 314159265359e-11;\n\tradiant rnd64= atan((y / x));\n\nExpressions\n\tcarthesianToPolar$44$$32$theta rnd64= (radiant * (180 / pi));\n}\n","core":"(FPCore\n (x y)\n :name\n \"carthesianToPolar, theta\"\n :pre\n (and (<= 1 x 100) (<= 1 y 100))\n :spec\n (* (atan2 y x) (/ 180 PI))\n (let ((pi 314159265359/100000000000) (radiant (atan (/ y x))))\n   (* radiant (/ 180 pi))))"},{"body":"(let* ((pi 314159265359/100000000000) (radiant (* theta (/ pi 180))))\n  (* radius (cos radiant)))","arguments":["radius","theta"],"operators":["let*","*","/","cos"],":spec":"(* radius (cos (* theta (/ 180 PI))))",":pre":"(and (<= 1 radius 10) (<= 0 theta 360))",":name":"polarToCarthesian, x","core_fptaylor":false,"core":"(FPCore\n (radius theta)\n :name\n \"polarToCarthesian, x\"\n :pre\n (and (<= 1 radius 10) (<= 0 theta 360))\n :spec\n (* radius (cos (* theta (/ 180 PI))))\n (let* ((pi 314159265359/100000000000) (radiant (* theta (/ pi 180))))\n   (* radius (cos radiant))))"},{"body":"(let* ((pi 314159265359/100000000000) (radiant (* theta (/ pi 180))))\n  (* radius (sin radiant)))","arguments":["radius","theta"],"operators":["let*","*","/","sin"],":spec":"(* radius (sin (* theta (/ 180 PI))))",":pre":"(and (<= 1 radius 10) (<= 0 theta 360))",":name":"polarToCarthesian, y","core_fptaylor":false,"core":"(FPCore\n (radius theta)\n :name\n \"polarToCarthesian, y\"\n :pre\n (and (<= 1 radius 10) (<= 0 theta 360))\n :spec\n (* radius (sin (* theta (/ 180 PI))))\n (let* ((pi 314159265359/100000000000) (radiant (* theta (/ pi 180))))\n   (* radius (sin radiant))))"},{"body":"(let* ((pi 314159265359/100000000000)\n       (impedance_re resistance)\n       (impedance_im (* (* (* 2 pi) frequency) inductance))\n       (denom (+ (* impedance_re impedance_re) (* impedance_im impedance_im)))\n       (current_re (/ (* maxVoltage impedance_re) denom))\n       (current_im (/ (- (* maxVoltage impedance_im)) denom))\n       (maxCurrent\n        (sqrt (+ (* current_re current_re) (* current_im current_im))))\n       (theta (atan (/ current_im current_re))))\n  (* maxCurrent (cos (+ (* (* (* 2 pi) frequency) t) theta))))","arguments":["t","resistance","frequency","inductance","maxVoltage"],"operators":["let*","*","+","/","-","sqrt","atan","cos"],":pre":"(and (<= 0 t 300)\n     (<= 1 resistance 50)\n     (<= 1 frequency 100)\n     (<= 1/1000 inductance 1/250)\n     (<= 1 maxVoltage 12))",":name":"instantaneousCurrent","core_fptaylor":false,"core":"(FPCore\n (t resistance frequency inductance maxVoltage)\n :name\n \"instantaneousCurrent\"\n :pre\n (and (<= 0 t 300)\n      (<= 1 resistance 50)\n      (<= 1 frequency 100)\n      (<= 1/1000 inductance 1/250)\n      (<= 1 maxVoltage 12))\n (let* ((pi 314159265359/100000000000)\n        (impedance_re resistance)\n        (impedance_im (* (* (* 2 pi) frequency) inductance))\n        (denom (+ (* impedance_re impedance_re) (* impedance_im impedance_im)))\n        (current_re (/ (* maxVoltage impedance_re) denom))\n        (current_im (/ (- (* maxVoltage impedance_im)) denom))\n        (maxCurrent\n         (sqrt (+ (* current_re current_re) (* current_im current_im))))\n        (theta (atan (/ current_im current_re))))\n   (* maxCurrent (cos (+ (* (* (* 2 pi) frequency) t) theta)))))"},{"body":"(-\n (+ (+ (* (* a e) i) (* (* b f) g)) (* (* c d) h))\n (+ (+ (* (* c e) g) (* (* b d) i)) (* (* a f) h)))","arguments":["a","b","c","d","e","f","g","h","i"],"operators":["-","+","*"],":pre":"(and (<= -10 a 10)\n     (<= -10 b 10)\n     (<= -10 c 10)\n     (<= -10 d 10)\n     (<= -10 e 10)\n     (<= -10 f 10)\n     (<= -10 g 10)\n     (<= -10 h 10)\n     (<= -10 i 10))",":name":"matrixDeterminant","core_fptaylor":"{\nVariables\n\treal a in [-10, 10];\n\treal b in [-10, 10];\n\treal c in [-10, 10];\n\treal d in [-10, 10];\n\treal e in [-10, 10];\n\treal f in [-10, 10];\n\treal g in [-10, 10];\n\treal h in [-10, 10];\n\treal i in [-10, 10];\n\nExpressions\n\tmatrixDeterminant rnd64= (((((a * e) * i) + ((b * f) * g)) + ((c * d) * h)) - ((((c * e) * g) + ((b * d) * i)) + ((a * f) * h)));\n}\n","core":"(FPCore\n (a b c d e f g h i)\n :name\n \"matrixDeterminant\"\n :pre\n (and (<= -10 a 10)\n      (<= -10 b 10)\n      (<= -10 c 10)\n      (<= -10 d 10)\n      (<= -10 e 10)\n      (<= -10 f 10)\n      (<= -10 g 10)\n      (<= -10 h 10)\n      (<= -10 i 10))\n (-\n  (+ (+ (* (* a e) i) (* (* b f) g)) (* (* c d) h))\n  (+ (+ (* (* c e) g) (* (* b d) i)) (* (* a f) h))))"},{"body":"(-\n (+ (* a (* e i)) (+ (* g (* b f)) (* c (* d h))))\n (+ (* e (* c g)) (+ (* i (* b d)) (* a (* f h)))))","arguments":["a","b","c","d","e","f","g","h","i"],"operators":["-","+","*"],":pre":"(and (<= -10 a 10)\n     (<= -10 b 10)\n     (<= -10 c 10)\n     (<= -10 d 10)\n     (<= -10 e 10)\n     (<= -10 f 10)\n     (<= -10 g 10)\n     (<= -10 h 10)\n     (<= -10 i 10))",":name":"matrixDeterminant2","core_fptaylor":"{\nVariables\n\treal a in [-10, 10];\n\treal b in [-10, 10];\n\treal c in [-10, 10];\n\treal d in [-10, 10];\n\treal e in [-10, 10];\n\treal f in [-10, 10];\n\treal g in [-10, 10];\n\treal h in [-10, 10];\n\treal i in [-10, 10];\n\nExpressions\n\tmatrixDeterminant2 rnd64= (((a * (e * i)) + ((g * (b * f)) + (c * (d * h)))) - ((e * (c * g)) + ((i * (b * d)) + (a * (f * h)))));\n}\n","core":"(FPCore\n (a b c d e f g h i)\n :name\n \"matrixDeterminant2\"\n :pre\n (and (<= -10 a 10)\n      (<= -10 b 10)\n      (<= -10 c 10)\n      (<= -10 d 10)\n      (<= -10 e 10)\n      (<= -10 f 10)\n      (<= -10 g 10)\n      (<= -10 h 10)\n      (<= -10 i 10))\n (-\n  (+ (* a (* e i)) (+ (* g (* b f)) (* c (* d h))))\n  (+ (* e (* c g)) (+ (* i (* b d)) (* a (* f h))))))"},{"body":"(cast (! :precision binary64 (/ t (! :precision binary32 (+ t 1)))))","arguments":["t"],"operators":["cast","!","/","+"],":precision":"binary32",":pre":"(<= 1 t 999)",":name":"intro-example-mixed","core_fptaylor":"{\nVariables\n\treal t in [1, 999];\n\nExpressions\n\tintro$45$example$45$mixed rnd32= (t / (t + 1));\n}\n","core":"(FPCore\n (t)\n :name\n \"intro-example-mixed\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary32\n :pre\n (<= 1 t 999)\n (cast (! :precision binary64 (/ t (! :precision binary32 (+ t 1))))))",":description":"Generated by FPTaylor"},{"body":"(+\n (- (+ (+ (- (* (- x2) x3) (* x1 x4)) (* x2 x5)) (* x3 x6)) (* x5 x6))\n (* x1 (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6)))","arguments":["x1","x2","x3","x4","x5","x6"],"operators":["+","-","*"],":precision":"binary64",":pre":"(and (<= 4 x1 3969/625)\n     (<= 4 x2 3969/625)\n     (<= 4 x3 3969/625)\n     (<= 4 x4 3969/625)\n     (<= 4 x5 3969/625)\n     (<= 4 x6 3969/625))",":name":"delta4","core_fptaylor":"{\nVariables\n\treal x1 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x2 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x3 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x4 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x5 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x6 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\nExpressions\n\tdelta4 rnd64= ((((((-x2 * x3) - (x1 * x4)) + (x2 * x5)) + (x3 * x6)) - (x5 * x6)) + (x1 * (((((-x1 + x2) + x3) - x4) + x5) + x6)));\n}\n","core":"(FPCore\n (x1 x2 x3 x4 x5 x6)\n :name\n \"delta4\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= 4 x1 3969/625)\n      (<= 4 x2 3969/625)\n      (<= 4 x3 3969/625)\n      (<= 4 x4 3969/625)\n      (<= 4 x5 3969/625)\n      (<= 4 x6 3969/625))\n (+\n  (- (+ (+ (- (* (- x2) x3) (* x1 x4)) (* x2 x5)) (* x3 x6)) (* x5 x6))\n  (* x1 (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))))",":description":"Generated by FPTaylor"},{"body":"(+\n (+\n  (+\n   (+\n    (+\n     (+\n      (* (* x1 x4) (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))\n      (* (* x2 x5) (+ (- (+ (+ (- x1 x2) x3) x4) x5) x6)))\n     (* (* x3 x6) (- (+ (+ (- (+ x1 x2) x3) x4) x5) x6)))\n    (* (* (- x2) x3) x4))\n   (* (* (- x1) x3) x5))\n  (* (* (- x1) x2) x6))\n (* (* (- x4) x5) x6))","arguments":["x1","x2","x3","x4","x5","x6"],"operators":["+","*","-"],":precision":"binary64",":pre":"(and (<= 4 x1 3969/625)\n     (<= 4 x2 3969/625)\n     (<= 4 x3 3969/625)\n     (<= 4 x4 3969/625)\n     (<= 4 x5 3969/625)\n     (<= 4 x6 3969/625))",":name":"delta","core_fptaylor":"{\nVariables\n\treal x1 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x2 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x3 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x4 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x5 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\treal x6 in [4, 635039999999999960067498250282369554042816162109375e-50];\n\nExpressions\n\tdelta rnd64= ((((((((x1 * x4) * (((((-x1 + x2) + x3) - x4) + x5) + x6)) + ((x2 * x5) * (((((x1 - x2) + x3) + x4) - x5) + x6))) + ((x3 * x6) * (((((x1 + x2) - x3) + x4) + x5) - x6))) + ((-x2 * x3) * x4)) + ((-x1 * x3) * x5)) + ((-x1 * x2) * x6)) + ((-x4 * x5) * x6));\n}\n","core":"(FPCore\n (x1 x2 x3 x4 x5 x6)\n :name\n \"delta\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= 4 x1 3969/625)\n      (<= 4 x2 3969/625)\n      (<= 4 x3 3969/625)\n      (<= 4 x4 3969/625)\n      (<= 4 x5 3969/625)\n      (<= 4 x6 3969/625))\n (+\n  (+\n   (+\n    (+\n     (+\n      (+\n       (* (* x1 x4) (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))\n       (* (* x2 x5) (+ (- (+ (+ (- x1 x2) x3) x4) x5) x6)))\n      (* (* x3 x6) (- (+ (+ (- (+ x1 x2) x3) x4) x5) x6)))\n     (* (* (- x2) x3) x4))\n    (* (* (- x1) x3) x5))\n   (* (* (- x1) x2) x6))\n  (* (* (- x4) x5) x6)))",":description":"Generated by FPTaylor"},{"body":"(/ 1 (+ (sqrt (+ x 1)) (sqrt x)))","arguments":["x"],"operators":["/","+","sqrt"],":precision":"binary64",":pre":"(<= 1 x 1000)",":name":"sqrt_add","core_fptaylor":"{\nVariables\n\treal x in [1, 1000];\n\nExpressions\n\tsqrt_add rnd64= (1 / (sqrt((x + 1)) + sqrt(x)));\n}\n","core":"(FPCore\n (x)\n :name\n \"sqrt_add\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (<= 1 x 1000)\n (/ 1 (+ (sqrt (+ x 1)) (sqrt x))))",":description":"Generated by FPTaylor"},{"body":"(/ (- (exp x) 1) x)","arguments":["x"],"operators":["/","-","exp"],":precision":"binary64",":pre":"(<= 1/100 x 1/2)",":name":"exp1x","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000020816681711721685132943093776702880859375e-59, 5e-1];\n\nExpressions\n\texp1x rnd64= ((exp(x) - 1) / x);\n}\n","core":"(FPCore\n (x)\n :name\n \"exp1x\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (<= 1/100 x 1/2)\n (/ (- (exp x) 1) x))",":description":"Generated by FPTaylor"},{"body":"(/ (- (exp x) 1) x)","arguments":["x"],"operators":["/","-","exp"],":precision":"binary32",":pre":"(<= 1/100 x 1/2)",":name":"exp1x_32","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000020816681711721685132943093776702880859375e-59, 5e-1];\n\nExpressions\n\texp1x_32 rnd32= ((exp(x) - 1) / x);\n}\n","core":"(FPCore\n (x)\n :name\n \"exp1x_32\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary32\n :pre\n (<= 1/100 x 1/2)\n (/ (- (exp x) 1) x))",":description":"Generated by FPTaylor"},{"body":"(+ x1 x2)","arguments":["x1","x2"],"operators":["+"],":precision":"binary64",":pre":"(and (<= 0 x1 2) (<= 0 x2 3) (<= (+ x1 x2) 2))",":name":"floudas","core_fptaylor":"{\nVariables\n\treal x1 in [0, 2];\n\treal x2 in [0, 3];\n\nConstraints\n\tconstraint0: ((x1 + x2) <= 2);\n\nExpressions\n\tfloudas rnd64= (x1 + x2);\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"floudas\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= 0 x1 2) (<= 0 x2 3) (<= (+ x1 x2) 2))\n (+ x1 x2))",":description":"Generated by FPTaylor"},{"body":"(/ (- (exp x) 1) (log (exp x)))","arguments":["x"],"operators":["/","-","exp","log"],":precision":"binary64",":pre":"(<= 1/100 x 1/2)",":name":"exp1x_log","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000020816681711721685132943093776702880859375e-59, 5e-1];\n\nExpressions\n\texp1x_log rnd64= ((exp(x) - 1) / log(exp(x)));\n}\n","core":"(FPCore\n (x)\n :name\n \"exp1x_log\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (<= 1/100 x 1/2)\n (/ (- (exp x) 1) (log (exp x))))",":description":"Generated by FPTaylor"},{"body":"(/ x (+ x y))","arguments":["x","y"],"operators":["/","+"],":precision":"binary32",":pre":"(and (<= 1 x 4) (<= 1 y 4))",":name":"x_by_xy","core_fptaylor":"{\nVariables\n\treal x in [1, 4];\n\treal y in [1, 4];\n\nExpressions\n\tx_by_xy rnd32= (x / (x + y));\n}\n","core":"(FPCore\n (x y)\n :name\n \"x_by_xy\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary32\n :pre\n (and (<= 1 x 4) (<= 1 y 4))\n (/ x (+ x y)))",":description":"Generated by FPTaylor"},{"body":"(sqrt (+ (* x1 x1) (* x2 x2)))","arguments":["x1","x2"],"operators":["sqrt","+","*"],":precision":"binary64",":pre":"(and (<= 1 x1 100) (<= 1 x2 100))",":name":"hypot","core_fptaylor":"{\nVariables\n\treal x1 in [1, 100];\n\treal x2 in [1, 100];\n\nExpressions\n\thypot rnd64= sqrt(((x1 * x1) + (x2 * x2)));\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"hypot\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= 1 x1 100) (<= 1 x2 100))\n (sqrt (+ (* x1 x1) (* x2 x2))))",":description":"Generated by FPTaylor"},{"body":"(sqrt (+ (* x1 x1) (* x2 x2)))","arguments":["x1","x2"],"operators":["sqrt","+","*"],":precision":"binary32",":pre":"(and (<= 1 x1 100) (<= 1 x2 100))",":name":"hypot32","core_fptaylor":"{\nVariables\n\treal x1 in [1, 100];\n\treal x2 in [1, 100];\n\nExpressions\n\thypot32 rnd32= sqrt(((x1 * x1) + (x2 * x2)));\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"hypot32\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary32\n :pre\n (and (<= 1 x1 100) (<= 1 x2 100))\n (sqrt (+ (* x1 x1) (* x2 x2))))",":description":"Generated by FPTaylor"},{"body":"(log (+ 1 (exp x)))","arguments":["x"],"operators":["log","+","exp"],":precision":"binary64",":pre":"(<= -8 x 8)",":name":"logexp","core_fptaylor":"{\nVariables\n\treal x in [-8, 8];\n\nExpressions\n\tlogexp rnd64= log((1 + exp(x)));\n}\n","core":"(FPCore\n (x)\n :name\n \"logexp\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (<= -8 x 8)\n (log (+ 1 (exp x))))",":description":"Generated by FPTaylor"},{"body":"(let ((p0 (- (+ x0 x1) x2)) (p1 (- (+ x1 x2) x0)) (p2 (- (+ x2 x0) x1)))\n  (+ (+ p0 p1) p2))","arguments":["x0","x1","x2"],"operators":["let","-","+"],":precision":"binary64",":pre":"(and (<= 1 x0 2) (<= 1 x1 2) (<= 1 x2 2))",":name":"sum","core_fptaylor":"{\nVariables\n\treal x0 in [1, 2];\n\treal x1 in [1, 2];\n\treal x2 in [1, 2];\n\nDefinitions\n\tp0 rnd64= ((x0 + x1) - x2);\n\tp1 rnd64= ((x1 + x2) - x0);\n\tp2 rnd64= ((x2 + x0) - x1);\n\nExpressions\n\tsum rnd64= ((p0 + p1) + p2);\n}\n","core":"(FPCore\n (x0 x1 x2)\n :name\n \"sum\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= 1 x0 2) (<= 1 x1 2) (<= 1 x2 2))\n (let ((p0 (- (+ x0 x1) x2)) (p1 (- (+ x1 x2) x0)) (p2 (- (+ x2 x0) x1)))\n   (+ (+ p0 p1) p2)))",":description":"Generated by FPTaylor"},{"body":"(/ z (+ z 1))","arguments":["z"],"operators":["/","+"],":precision":"binary64",":pre":"(<= 0 z 999)",":name":"nonlin1","core_fptaylor":"{\nVariables\n\treal z in [0, 999];\n\nExpressions\n\tnonlin1 rnd64= (z / (z + 1));\n}\n","core":"(FPCore\n (z)\n :name\n \"nonlin1\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (<= 0 z 999)\n (/ z (+ z 1)))",":description":"Generated by FPTaylor"},{"body":"(let ((t (* x y))) (/ (- t 1) (- (* t t) 1)))","arguments":["x","y"],"operators":["let","*","/","-"],":precision":"binary64",":pre":"(and (<= 1001/1000 x 2) (<= 1001/1000 y 2))",":name":"nonlin2","core_fptaylor":"{\nVariables\n\treal x in [1000999999999999889865875957184471189975738525390625e-51, 2];\n\treal y in [1000999999999999889865875957184471189975738525390625e-51, 2];\n\nDefinitions\n\tt rnd64= (x * y);\n\nExpressions\n\tnonlin2 rnd64= ((t - 1) / ((t * t) - 1));\n}\n","core":"(FPCore\n (x y)\n :name\n \"nonlin2\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= 1001/1000 x 2) (<= 1001/1000 y 2))\n (let ((t (* x y))) (/ (- t 1) (- (* t t) 1))))",":description":"Generated by FPTaylor"},{"body":"(sqrt (+ x (* y y)))","arguments":["x","y"],"operators":["sqrt","+","*"],":precision":"binary32",":pre":"(and (<= 1/10 x 10) (<= -5 y 5))",":name":"i4","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000055511151231257827021181583404541015625e-55, 10];\n\treal y in [-5, 5];\n\nExpressions\n\ti4 rnd32= sqrt((x + (y * y)));\n}\n","core":"(FPCore\n (x y)\n :name\n \"i4\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary32\n :pre\n (and (<= 1/10 x 10) (<= -5 y 5))\n (sqrt (+ x (* y y))))",":description":"Generated by FPTaylor"},{"body":"(sin (* x y))","arguments":["x","y"],"operators":["sin","*"],":precision":"binary32",":pre":"(and (<= 1/10 x 10) (<= -5 y 5))",":name":"i6","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000055511151231257827021181583404541015625e-55, 10];\n\treal y in [-5, 5];\n\nExpressions\n\ti6 rnd32= sin((x * y));\n}\n","core":"(FPCore\n (x y)\n :name\n \"i6\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary32\n :pre\n (and (<= 1/10 x 10) (<= -5 y 5))\n (sin (* x y)))",":description":"Generated by FPTaylor"},{"body":"(let ((a (- (+ (* x1 x1) x2) 11)) (b (- (+ x1 (* x2 x2)) 7)))\n  (+ (* a a) (* b b)))","arguments":["x1","x2"],"operators":["let","-","+","*"],":precision":"binary64",":pre":"(and (<= -5 x1 5) (<= -5 x2 5))",":name":"himmilbeau","core_fptaylor":"{\nVariables\n\treal x1 in [-5, 5];\n\treal x2 in [-5, 5];\n\nDefinitions\n\ta rnd64= (((x1 * x1) + x2) - 11);\n\tb rnd64= ((x1 + (x2 * x2)) - 7);\n\nExpressions\n\thimmilbeau rnd64= ((a * a) + (b * b));\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"himmilbeau\"\n :description\n \"Generated by FPTaylor\"\n :precision\n binary64\n :pre\n (and (<= -5 x1 5) (<= -5 x2 5))\n (let ((a (- (+ (* x1 x1) x2) 11)) (b (- (+ x1 (* x2 x2)) 7)))\n   (+ (* a a) (* b b))))",":description":"Generated by FPTaylor"},{"body":"(let ((e (exp x))) (log (+ 1 e)))","arguments":["x"],"operators":["let","exp","log","+"],":cite":["solovyev-et-al-2015"],":precision":"binary64",":pre":"(<= -8 x 8)",":name":"logexp","core_fptaylor":"{\nVariables\n\treal x in [-8, 8];\n\nDefinitions\n\te rnd64= exp(x);\n\nExpressions\n\tlogexp rnd64= log((1 + e));\n}\n","core":"(FPCore\n (x)\n :name\n \"logexp\"\n :cite\n (solovyev-et-al-2015)\n :precision\n binary64\n :pre\n (<= -8 x 8)\n (let ((e (exp x))) (log (+ 1 e))))"},{"body":"(let ((sinLat (sin lat)) (cosLon (cos lon))) (+ x (* (* r sinLat) cosLon)))","arguments":["x","r","lat","lon"],"operators":["let","sin","cos","+","*"],":cite":["solovyev-et-al-2015"],":precision":"binary64",":pre":"(and (<= -10 x 10)\n     (<= 0 r 10)\n     (<= -392699/250000 lat 392699/250000)\n     (<= -62831853/20000000 lon 62831853/20000000))",":name":"sphere","core_fptaylor":"{\nVariables\n\treal x in [-10, 10];\n\treal r in [0, 10];\n\treal lat in [-1570796000000000081087137004942633211612701416015625e-51, 1570796000000000081087137004942633211612701416015625e-51];\n\treal lon in [-3141592650000000208621031561051495373249053955078125e-51, 3141592650000000208621031561051495373249053955078125e-51];\n\nDefinitions\n\tsinLat rnd64= sin(lat);\n\tcosLon rnd64= cos(lon);\n\nExpressions\n\tsphere rnd64= (x + ((r * sinLat) * cosLon));\n}\n","core":"(FPCore\n (x r lat lon)\n :name\n \"sphere\"\n :cite\n (solovyev-et-al-2015)\n :precision\n binary64\n :pre\n (and (<= -10 x 10)\n      (<= 0 r 10)\n      (<= -392699/250000 lat 392699/250000)\n      (<= -62831853/20000000 lon 62831853/20000000))\n (let ((sinLat (sin lat)) (cosLon (cos lon))) (+ x (* (* r sinLat) cosLon))))"},{"body":"(let ((dLon (- lon2 lon1)))\n  (let ((s_lat1 (sin lat1))\n        (c_lat1 (cos lat1))\n        (s_lat2 (sin lat2))\n        (c_lat2 (cos lat2))\n        (s_dLon (sin dLon))\n        (c_dLon (cos dLon)))\n    (atan\n     (/\n      (* c_lat2 s_dLon)\n      (- (* c_lat1 s_lat2) (* (* s_lat1 c_lat2) c_dLon))))))","arguments":["lat1","lat2","lon1","lon2"],"operators":["let","-","sin","cos","atan","/","*"],":cite":["solovyev-et-al-2015"],":precision":"binary64",":pre":"(and (<= 0 lat1 2/5)\n     (<= 1/2 lat2 1)\n     (<= 0 lon1 62831853/20000000)\n     (<= -62831853/20000000 lon2 -1/2))",":name":"azimuth","core_fptaylor":"{\nVariables\n\treal lat1 in [0, 40000000000000002220446049250313080847263336181640625e-53];\n\treal lat2 in [5e-1, 1];\n\treal lon1 in [0, 3141592650000000208621031561051495373249053955078125e-51];\n\treal lon2 in [-3141592650000000208621031561051495373249053955078125e-51, -5e-1];\n\nDefinitions\n\tdLon rnd64= (lon2 - lon1);\n\ts_lat1 rnd64= sin(lat1);\n\tc_lat1 rnd64= cos(lat1);\n\ts_lat2 rnd64= sin(lat2);\n\tc_lat2 rnd64= cos(lat2);\n\ts_dLon rnd64= sin(dLon);\n\tc_dLon rnd64= cos(dLon);\n\nExpressions\n\tazimuth rnd64= atan(((c_lat2 * s_dLon) / ((c_lat1 * s_lat2) - ((s_lat1 * c_lat2) * c_dLon))));\n}\n","core":"(FPCore\n (lat1 lat2 lon1 lon2)\n :name\n \"azimuth\"\n :cite\n (solovyev-et-al-2015)\n :precision\n binary64\n :pre\n (and (<= 0 lat1 2/5)\n      (<= 1/2 lat2 1)\n      (<= 0 lon1 62831853/20000000)\n      (<= -62831853/20000000 lon2 -1/2))\n (let ((dLon (- lon2 lon1)))\n   (let ((s_lat1 (sin lat1))\n         (c_lat1 (cos lat1))\n         (s_lat2 (sin lat2))\n         (c_lat2 (cos lat2))\n         (s_dLon (sin dLon))\n         (c_dLon (cos dLon)))\n     (atan\n      (/\n       (* c_lat2 s_dLon)\n       (- (* c_lat1 s_lat2) (* (* s_lat1 c_lat2) c_dLon)))))))"},{"body":"(-\n (-\n  (-\n   (-\n    (- (* -25 (* (- x1 2) (- x1 2))) (* (- x2 2) (- x2 2)))\n    (* (- x3 1) (- x3 1)))\n   (* (- x4 4) (- x4 4)))\n  (* (- x5 1) (- x5 1)))\n (* (- x6 4) (- x6 4)))","arguments":["x1","x2","x3","x4","x5","x6"],"operators":["-","*"],":precision":"binary64",":pre":"(and (<= 0 x1 6)\n     (<= 0 x2 6)\n     (<= 1 x3 5)\n     (<= 0 x4 6)\n     (<= 0 x5 6)\n     (<= 0 x6 10)\n     (>= (- (+ (* (- x3 3) (- x3 3)) x4) 4) 0)\n     (>= (- (+ (* (- x5 3) (- x5 3)) x6) 4) 0)\n     (>= (+ (- 2 x1) (* 3 x2)) 0)\n     (>= (- (+ 2 x1) x2) 0)\n     (>= (- (- 6 x1) x2) 0)\n     (>= (- (+ x1 x2) 2) 0))",":name":"floudas1","core_fptaylor":"{\nVariables\n\treal x1 in [0, 6];\n\treal x2 in [0, 6];\n\treal x3 in [1, 5];\n\treal x4 in [0, 6];\n\treal x5 in [0, 6];\n\treal x6 in [0, 10];\n\nConstraints\n\tconstraint0: (((((x3 - 3) * (x3 - 3)) + x4) - 4) >= 0);\n\tconstraint1: (((((x5 - 3) * (x5 - 3)) + x6) - 4) >= 0);\n\tconstraint2: (((2 - x1) + (3 * x2)) >= 0);\n\tconstraint3: (((2 + x1) - x2) >= 0);\n\tconstraint4: (((6 - x1) - x2) >= 0);\n\tconstraint5: (((x1 + x2) - 2) >= 0);\n\nExpressions\n\tfloudas1 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)));\n}\n","core":"(FPCore\n (x1 x2 x3 x4 x5 x6)\n :name\n \"floudas1\"\n :precision\n binary64\n :pre\n (and (<= 0 x1 6)\n      (<= 0 x2 6)\n      (<= 1 x3 5)\n      (<= 0 x4 6)\n      (<= 0 x5 6)\n      (<= 0 x6 10)\n      (>= (- (+ (* (- x3 3) (- x3 3)) x4) 4) 0)\n      (>= (- (+ (* (- x5 3) (- x5 3)) x6) 4) 0)\n      (>= (+ (- 2 x1) (* 3 x2)) 0)\n      (>= (- (+ 2 x1) x2) 0)\n      (>= (- (- 6 x1) x2) 0)\n      (>= (- (+ x1 x2) 2) 0))\n (-\n  (-\n   (-\n    (-\n     (- (* -25 (* (- x1 2) (- x1 2))) (* (- x2 2) (- x2 2)))\n     (* (- x3 1) (- x3 1)))\n    (* (- x4 4) (- x4 4)))\n   (* (- x5 1) (- x5 1)))\n  (* (- x6 4) (- x6 4))))"},{"body":"(- (- x1) x2)","arguments":["x1","x2"],"operators":["-"],":precision":"binary64",":pre":"(and (<= 0 x1 3)\n     (<= 0 x2 4)\n     (>=\n      (-\n       (+\n        (- (* 2 (* (* x1 x1) (* x1 x1))) (* (* 8 (* x1 x1)) x1))\n        (* (* 8 x1) x1))\n       x2)\n      0)\n     (>=\n      (-\n       (+\n        (-\n         (+\n          (- (* 4 (* (* x1 x1) (* x1 x1))) (* (* 32 (* x1 x1)) x1))\n          (* (* 88 x1) x1))\n         (* 96 x1))\n        36)\n       x2)\n      0))",":name":"floudas2","core_fptaylor":"{\nVariables\n\treal x1 in [0, 3];\n\treal x2 in [0, 4];\n\nConstraints\n\tconstraint0: (((((2 * ((x1 * x1) * (x1 * x1))) - ((8 * (x1 * x1)) * x1)) + ((8 * x1) * x1)) - x2) >= 0);\n\tconstraint1: (((((((4 * ((x1 * x1) * (x1 * x1))) - ((32 * (x1 * x1)) * x1)) + ((88 * x1) * x1)) - (96 * x1)) + 36) - x2) >= 0);\n\nExpressions\n\tfloudas2 rnd64= (-x1 - x2);\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"floudas2\"\n :precision\n binary64\n :pre\n (and (<= 0 x1 3)\n      (<= 0 x2 4)\n      (>=\n       (-\n        (+\n         (- (* 2 (* (* x1 x1) (* x1 x1))) (* (* 8 (* x1 x1)) x1))\n         (* (* 8 x1) x1))\n        x2)\n       0)\n      (>=\n       (-\n        (+\n         (-\n          (+\n           (- (* 4 (* (* x1 x1) (* x1 x1))) (* (* 32 (* x1 x1)) x1))\n           (* (* 88 x1) x1))\n          (* 96 x1))\n         36)\n        x2)\n       0))\n (- (- x1) x2))"},{"body":"(+ (- (* -12 x1) (* 7 x2)) (* x2 x2))","arguments":["x1","x2"],"operators":["+","-","*"],":precision":"binary64",":pre":"(and (<= 0 x1 2) (<= 0 x2 3) (>= (+ (* -2 (* (* x1 x1) (* x1 x1))) 2) x2))",":name":"floudas3","core_fptaylor":"{\nVariables\n\treal x1 in [0, 2];\n\treal x2 in [0, 3];\n\nConstraints\n\tconstraint0: (((-2 * ((x1 * x1) * (x1 * x1))) + 2) >= x2);\n\nExpressions\n\tfloudas3 rnd64= (((-12 * x1) - (7 * x2)) + (x2 * x2));\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"floudas3\"\n :precision\n binary64\n :pre\n (and (<= 0 x1 2) (<= 0 x2 3) (>= (+ (* -2 (* (* x1 x1) (* x1 x1))) 2) x2))\n (+ (- (* -12 x1) (* 7 x2)) (* x2 x2)))"},{"body":"(let ((e1\n       (+\n        (+\n         (* 3 (* (- x1 3689/10000) (- x1 3689/10000)))\n         (* 10 (* (- x2 117/1000) (- x2 117/1000))))\n        (* 30 (* (- x3 2673/10000) (- x3 2673/10000)))))\n      (e2\n       (+\n        (+\n         (* 1/10 (* (- x1 4699/10000) (- x1 4699/10000)))\n         (* 10 (* (- x2 4387/10000) (- x2 4387/10000))))\n        (* 35 (* (- x3 747/1000) (- x3 747/1000)))))\n      (e3\n       (+\n        (+\n         (* 3 (* (- x1 1091/10000) (- x1 1091/10000)))\n         (* 10 (* (- x2 2183/2500) (- x2 2183/2500))))\n        (* 30 (* (- x3 5547/10000) (- x3 5547/10000)))))\n      (e4\n       (+\n        (+\n         (* 1/10 (* (- x1 763/20000) (- x1 763/20000)))\n         (* 10 (* (- x2 5743/10000) (- x2 5743/10000))))\n        (* 35 (* (- x3 2207/2500) (- x3 2207/2500))))))\n  (let ((exp1 (exp (- e1)))\n        (exp2 (exp (- e2)))\n        (exp3 (exp (- e3)))\n        (exp4 (exp (- e4))))\n    (- (+ (+ (+ (* 1 exp1) (* 6/5 exp2)) (* 3 exp3)) (* 16/5 exp4)))))","arguments":["x1","x2","x3"],"operators":["let","+","*","-","exp"],":precision":"binary64",":pre":"(and (<= 0 x1 1) (<= 0 x2 1) (<= 0 x3 1))",":name":"hartman3","core_fptaylor":"{\nVariables\n\treal x1 in [0, 1];\n\treal x2 in [0, 1];\n\treal x3 in [0, 1];\n\nDefinitions\n\te1 rnd64= (((3 * ((x1 - 3689e-4) * (x1 - 3689e-4))) + (10 * ((x2 - 117e-3) * (x2 - 117e-3)))) + (30 * ((x3 - 2673e-4) * (x3 - 2673e-4))));\n\te2 rnd64= (((1e-1 * ((x1 - 4699e-4) * (x1 - 4699e-4))) + (10 * ((x2 - 4387e-4) * (x2 - 4387e-4)))) + (35 * ((x3 - 747e-3) * (x3 - 747e-3))));\n\te3 rnd64= (((3 * ((x1 - 1091e-4) * (x1 - 1091e-4))) + (10 * ((x2 - 8732e-4) * (x2 - 8732e-4)))) + (30 * ((x3 - 5547e-4) * (x3 - 5547e-4))));\n\te4 rnd64= (((1e-1 * ((x1 - 3815e-5) * (x1 - 3815e-5))) + (10 * ((x2 - 5743e-4) * (x2 - 5743e-4)))) + (35 * ((x3 - 8828e-4) * (x3 - 8828e-4))));\n\texp1 rnd64= exp(-e1);\n\texp2 rnd64= exp(-e2);\n\texp3 rnd64= exp(-e3);\n\texp4 rnd64= exp(-e4);\n\nExpressions\n\thartman3 rnd64= -((((1 * exp1) + (12e-1 * exp2)) + (3 * exp3)) + (32e-1 * exp4));\n}\n","core":"(FPCore\n (x1 x2 x3)\n :name\n \"hartman3\"\n :precision\n binary64\n :pre\n (and (<= 0 x1 1) (<= 0 x2 1) (<= 0 x3 1))\n (let ((e1\n        (+\n         (+\n          (* 3 (* (- x1 3689/10000) (- x1 3689/10000)))\n          (* 10 (* (- x2 117/1000) (- x2 117/1000))))\n         (* 30 (* (- x3 2673/10000) (- x3 2673/10000)))))\n       (e2\n        (+\n         (+\n          (* 1/10 (* (- x1 4699/10000) (- x1 4699/10000)))\n          (* 10 (* (- x2 4387/10000) (- x2 4387/10000))))\n         (* 35 (* (- x3 747/1000) (- x3 747/1000)))))\n       (e3\n        (+\n         (+\n          (* 3 (* (- x1 1091/10000) (- x1 1091/10000)))\n          (* 10 (* (- x2 2183/2500) (- x2 2183/2500))))\n         (* 30 (* (- x3 5547/10000) (- x3 5547/10000)))))\n       (e4\n        (+\n         (+\n          (* 1/10 (* (- x1 763/20000) (- x1 763/20000)))\n          (* 10 (* (- x2 5743/10000) (- x2 5743/10000))))\n         (* 35 (* (- x3 2207/2500) (- x3 2207/2500))))))\n   (let ((exp1 (exp (- e1)))\n         (exp2 (exp (- e2)))\n         (exp3 (exp (- e3)))\n         (exp4 (exp (- e4))))\n     (- (+ (+ (+ (* 1 exp1) (* 6/5 exp2)) (* 3 exp3)) (* 16/5 exp4))))))"},{"body":"(let ((e1\n       (+\n        (+\n         (+\n          (+\n           (+\n            (* 10 (* (- x1 82/625) (- x1 82/625)))\n            (* 3 (* (- x2 106/625) (- x2 106/625))))\n           (* 17 (* (- x3 5569/10000) (- x3 5569/10000))))\n          (* 7/2 (* (- x4 31/2500) (- x4 31/2500))))\n         (* 17/10 (* (- x5 8283/10000) (- x5 8283/10000))))\n        (* 8 (* (- x6 2943/5000) (- x6 2943/5000)))))\n      (e2\n       (+\n        (+\n         (+\n          (+\n           (+\n            (* 1/20 (* (- x1 2329/10000) (- x1 2329/10000)))\n            (* 10 (* (- x2 827/2000) (- x2 827/2000))))\n           (* 17 (* (- x3 8307/10000) (- x3 8307/10000))))\n          (* 1/10 (* (- x4 467/1250) (- x4 467/1250))))\n         (* 8 (* (- x5 251/2500) (- x5 251/2500))))\n        (* 14 (* (- x6 9991/10000) (- x6 9991/10000)))))\n      (e3\n       (+\n        (+\n         (+\n          (+\n           (+\n            (* 3 (* (- x1 587/2500) (- x1 587/2500)))\n            (* 7/2 (* (- x2 1451/10000) (- x2 1451/10000))))\n           (* 17/10 (* (- x3 1761/5000) (- x3 1761/5000))))\n          (* 10 (* (- x4 2883/10000) (- x4 2883/10000))))\n         (* 17 (* (- x5 3047/10000) (- x5 3047/10000))))\n        (* 8 (* (- x6 133/200) (- x6 133/200)))))\n      (e4\n       (+\n        (+\n         (+\n          (+\n           (+\n            (* 17 (* (- x1 4047/10000) (- x1 4047/10000)))\n            (* 8 (* (- x2 2207/2500) (- x2 2207/2500))))\n           (* 1/20 (* (- x3 2183/2500) (- x3 2183/2500))))\n          (* 10 (* (- x4 5743/10000) (- x4 5743/10000))))\n         (* 1/10 (* (- x5 1091/10000) (- x5 1091/10000))))\n        (* 14 (* (- x6 381/10000) (- x6 381/10000))))))\n  (let ((exp1 (exp (- e1)))\n        (exp2 (exp (- e2)))\n        (exp3 (exp (- e3)))\n        (exp4 (exp (- e4))))\n    (- (+ (+ (+ (* 1 exp1) (* 6/5 exp2)) (* 3 exp3)) (* 16/5 exp4)))))","arguments":["x1","x2","x3","x4","x5","x6"],"operators":["let","+","*","-","exp"],":precision":"binary64",":pre":"(and (<= 0 x1 1) (<= 0 x2 1) (<= 0 x3 1) (<= 0 x4 1) (<= 0 x5 1) (<= 0 x6 1))",":name":"hartman6","core_fptaylor":"{\nVariables\n\treal x1 in [0, 1];\n\treal x2 in [0, 1];\n\treal x3 in [0, 1];\n\treal x4 in [0, 1];\n\treal x5 in [0, 1];\n\treal x6 in [0, 1];\n\nDefinitions\n\te1 rnd64= ((((((10 * ((x1 - 1312e-4) * (x1 - 1312e-4))) + (3 * ((x2 - 1696e-4) * (x2 - 1696e-4)))) + (17 * ((x3 - 5569e-4) * (x3 - 5569e-4)))) + (35e-1 * ((x4 - 124e-4) * (x4 - 124e-4)))) + (17e-1 * ((x5 - 8283e-4) * (x5 - 8283e-4)))) + (8 * ((x6 - 5886e-4) * (x6 - 5886e-4))));\n\te2 rnd64= ((((((5e-2 * ((x1 - 2329e-4) * (x1 - 2329e-4))) + (10 * ((x2 - 4135e-4) * (x2 - 4135e-4)))) + (17 * ((x3 - 8307e-4) * (x3 - 8307e-4)))) + (1e-1 * ((x4 - 3736e-4) * (x4 - 3736e-4)))) + (8 * ((x5 - 1004e-4) * (x5 - 1004e-4)))) + (14 * ((x6 - 9991e-4) * (x6 - 9991e-4))));\n\te3 rnd64= ((((((3 * ((x1 - 2348e-4) * (x1 - 2348e-4))) + (35e-1 * ((x2 - 1451e-4) * (x2 - 1451e-4)))) + (17e-1 * ((x3 - 3522e-4) * (x3 - 3522e-4)))) + (10 * ((x4 - 2883e-4) * (x4 - 2883e-4)))) + (17 * ((x5 - 3047e-4) * (x5 - 3047e-4)))) + (8 * ((x6 - 665e-3) * (x6 - 665e-3))));\n\te4 rnd64= ((((((17 * ((x1 - 4047e-4) * (x1 - 4047e-4))) + (8 * ((x2 - 8828e-4) * (x2 - 8828e-4)))) + (5e-2 * ((x3 - 8732e-4) * (x3 - 8732e-4)))) + (10 * ((x4 - 5743e-4) * (x4 - 5743e-4)))) + (1e-1 * ((x5 - 1091e-4) * (x5 - 1091e-4)))) + (14 * ((x6 - 381e-4) * (x6 - 381e-4))));\n\texp1 rnd64= exp(-e1);\n\texp2 rnd64= exp(-e2);\n\texp3 rnd64= exp(-e3);\n\texp4 rnd64= exp(-e4);\n\nExpressions\n\thartman6 rnd64= -((((1 * exp1) + (12e-1 * exp2)) + (3 * exp3)) + (32e-1 * exp4));\n}\n","core":"(FPCore\n (x1 x2 x3 x4 x5 x6)\n :name\n \"hartman6\"\n :precision\n binary64\n :pre\n (and (<= 0 x1 1) (<= 0 x2 1) (<= 0 x3 1) (<= 0 x4 1) (<= 0 x5 1) (<= 0 x6 1))\n (let ((e1\n        (+\n         (+\n          (+\n           (+\n            (+\n             (* 10 (* (- x1 82/625) (- x1 82/625)))\n             (* 3 (* (- x2 106/625) (- x2 106/625))))\n            (* 17 (* (- x3 5569/10000) (- x3 5569/10000))))\n           (* 7/2 (* (- x4 31/2500) (- x4 31/2500))))\n          (* 17/10 (* (- x5 8283/10000) (- x5 8283/10000))))\n         (* 8 (* (- x6 2943/5000) (- x6 2943/5000)))))\n       (e2\n        (+\n         (+\n          (+\n           (+\n            (+\n             (* 1/20 (* (- x1 2329/10000) (- x1 2329/10000)))\n             (* 10 (* (- x2 827/2000) (- x2 827/2000))))\n            (* 17 (* (- x3 8307/10000) (- x3 8307/10000))))\n           (* 1/10 (* (- x4 467/1250) (- x4 467/1250))))\n          (* 8 (* (- x5 251/2500) (- x5 251/2500))))\n         (* 14 (* (- x6 9991/10000) (- x6 9991/10000)))))\n       (e3\n        (+\n         (+\n          (+\n           (+\n            (+\n             (* 3 (* (- x1 587/2500) (- x1 587/2500)))\n             (* 7/2 (* (- x2 1451/10000) (- x2 1451/10000))))\n            (* 17/10 (* (- x3 1761/5000) (- x3 1761/5000))))\n           (* 10 (* (- x4 2883/10000) (- x4 2883/10000))))\n          (* 17 (* (- x5 3047/10000) (- x5 3047/10000))))\n         (* 8 (* (- x6 133/200) (- x6 133/200)))))\n       (e4\n        (+\n         (+\n          (+\n           (+\n            (+\n             (* 17 (* (- x1 4047/10000) (- x1 4047/10000)))\n             (* 8 (* (- x2 2207/2500) (- x2 2207/2500))))\n            (* 1/20 (* (- x3 2183/2500) (- x3 2183/2500))))\n           (* 10 (* (- x4 5743/10000) (- x4 5743/10000))))\n          (* 1/10 (* (- x5 1091/10000) (- x5 1091/10000))))\n         (* 14 (* (- x6 381/10000) (- x6 381/10000))))))\n   (let ((exp1 (exp (- e1)))\n         (exp2 (exp (- e2)))\n         (exp3 (exp (- e3)))\n         (exp4 (exp (- e4))))\n     (- (+ (+ (+ (* 1 exp1) (* 6/5 exp2)) (* 3 exp3)) (* 16/5 exp4))))))"},{"body":"(+\n (- (- (+ (* x2 x5) (* x3 x6)) (* x2 x3)) (* x5 x6))\n (* x1 (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6)))","arguments":["x1","x2","x3","x4","x5","x6"],"operators":["+","-","*"],":precision":"binary64",":pre":"(and (<= 4 x1 159/25)\n     (<= 4 x2 159/25)\n     (<= 4 x3 159/25)\n     (<= 4 x4 159/25)\n     (<= 4 x5 159/25)\n     (<= 4 x6 159/25))",":name":"kepler0","core_fptaylor":"{\nVariables\n\treal x1 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x2 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x3 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x4 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x5 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x6 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\nExpressions\n\tkepler0 rnd64= (((((x2 * x5) + (x3 * x6)) - (x2 * x3)) - (x5 * x6)) + (x1 * (((((-x1 + x2) + x3) - x4) + x5) + x6)));\n}\n","core":"(FPCore\n (x1 x2 x3 x4 x5 x6)\n :name\n \"kepler0\"\n :precision\n binary64\n :pre\n (and (<= 4 x1 159/25)\n      (<= 4 x2 159/25)\n      (<= 4 x3 159/25)\n      (<= 4 x4 159/25)\n      (<= 4 x5 159/25)\n      (<= 4 x6 159/25))\n (+\n  (- (- (+ (* x2 x5) (* x3 x6)) (* x2 x3)) (* x5 x6))\n  (* x1 (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))))"},{"body":"(-\n (-\n  (-\n   (-\n    (+\n     (+\n      (* (* x1 x4) (- (+ (+ (- x1) x2) x3) x4))\n      (* x2 (+ (+ (- x1 x2) x3) x4)))\n     (* x3 (+ (- (+ x1 x2) x3) x4)))\n    (* (* x2 x3) x4))\n   (* x1 x3))\n  (* x1 x2))\n x4)","arguments":["x1","x2","x3","x4"],"operators":["-","+","*"],":precision":"binary64",":pre":"(and (<= 4 x1 159/25) (<= 4 x2 159/25) (<= 4 x3 159/25) (<= 4 x4 159/25))",":name":"kepler1","core_fptaylor":"{\nVariables\n\treal x1 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x2 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x3 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x4 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\nExpressions\n\tkepler1 rnd64= ((((((((x1 * x4) * (((-x1 + x2) + x3) - x4)) + (x2 * (((x1 - x2) + x3) + x4))) + (x3 * (((x1 + x2) - x3) + x4))) - ((x2 * x3) * x4)) - (x1 * x3)) - (x1 * x2)) - x4);\n}\n","core":"(FPCore\n (x1 x2 x3 x4)\n :name\n \"kepler1\"\n :precision\n binary64\n :pre\n (and (<= 4 x1 159/25) (<= 4 x2 159/25) (<= 4 x3 159/25) (<= 4 x4 159/25))\n (-\n  (-\n   (-\n    (-\n     (+\n      (+\n       (* (* x1 x4) (- (+ (+ (- x1) x2) x3) x4))\n       (* x2 (+ (+ (- x1 x2) x3) x4)))\n      (* x3 (+ (- (+ x1 x2) x3) x4)))\n     (* (* x2 x3) x4))\n    (* x1 x3))\n   (* x1 x2))\n  x4))"},{"body":"(-\n (-\n  (-\n   (-\n    (+\n     (+\n      (* (* x1 x4) (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))\n      (* (* x2 x5) (+ (- (+ (+ (- x1 x2) x3) x4) x5) x6)))\n     (* (* x3 x6) (- (+ (+ (- (+ x1 x2) x3) x4) x5) x6)))\n    (* (* x2 x3) x4))\n   (* (* x1 x3) x5))\n  (* (* x1 x2) x6))\n (* (* x4 x5) x6))","arguments":["x1","x2","x3","x4","x5","x6"],"operators":["-","+","*"],":precision":"binary64",":pre":"(and (<= 4 x1 159/25)\n     (<= 4 x2 159/25)\n     (<= 4 x3 159/25)\n     (<= 4 x4 159/25)\n     (<= 4 x5 159/25)\n     (<= 4 x6 159/25))",":name":"kepler2","core_fptaylor":"{\nVariables\n\treal x1 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x2 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x3 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x4 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x5 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\treal x6 in [4, 636000000000000031974423109204508364200592041015625e-50];\n\nExpressions\n\tkepler2 rnd64= ((((((((x1 * x4) * (((((-x1 + x2) + x3) - x4) + x5) + x6)) + ((x2 * x5) * (((((x1 - x2) + x3) + x4) - x5) + x6))) + ((x3 * x6) * (((((x1 + x2) - x3) + x4) + x5) - x6))) - ((x2 * x3) * x4)) - ((x1 * x3) * x5)) - ((x1 * x2) * x6)) - ((x4 * x5) * x6));\n}\n","core":"(FPCore\n (x1 x2 x3 x4 x5 x6)\n :name\n \"kepler2\"\n :precision\n binary64\n :pre\n (and (<= 4 x1 159/25)\n      (<= 4 x2 159/25)\n      (<= 4 x3 159/25)\n      (<= 4 x4 159/25)\n      (<= 4 x5 159/25)\n      (<= 4 x6 159/25))\n (-\n  (-\n   (-\n    (-\n     (+\n      (+\n       (* (* x1 x4) (+ (+ (- (+ (+ (- x1) x2) x3) x4) x5) x6))\n       (* (* x2 x5) (+ (- (+ (+ (- x1 x2) x3) x4) x5) x6)))\n      (* (* x3 x6) (- (+ (+ (- (+ x1 x2) x3) x4) x5) x6)))\n     (* (* x2 x3) x4))\n    (* (* x1 x3) x5))\n   (* (* x1 x2) x6))\n  (* (* x4 x5) x6)))"},{"body":"(/ t (+ t 1))","arguments":["t"],"operators":["/","+"],":cite":["solovyev-et-al-2015"],":pre":"(<= 0 t 999)",":name":"intro-example","core_fptaylor":"{\nVariables\n\treal t in [0, 999];\n\nExpressions\n\tintro$45$example rnd64= (t / (t + 1));\n}\n","core":"(FPCore\n (t)\n :name\n \"intro-example\"\n :cite\n (solovyev-et-al-2015)\n :pre\n (<= 0 t 999)\n (/ t (+ t 1)))"},{"body":"(let ((t (* x y))) (/ (- t 1) (- (* t t) 1)))","arguments":["x","y"],"operators":["let","*","/","-"],":cite":["solovyev-et-al-2015"],":precision":"binary64",":pre":"(and (<= 1001/1000 x 2) (<= 1001/1000 y 2))",":name":"sec4-example","core_fptaylor":"{\nVariables\n\treal x in [1000999999999999889865875957184471189975738525390625e-51, 2];\n\treal y in [1000999999999999889865875957184471189975738525390625e-51, 2];\n\nDefinitions\n\tt rnd64= (x * y);\n\nExpressions\n\tsec4$45$example rnd64= ((t - 1) / ((t * t) - 1));\n}\n","core":"(FPCore\n (x y)\n :name\n \"sec4-example\"\n :cite\n (solovyev-et-al-2015)\n :precision\n binary64\n :pre\n (and (<= 1001/1000 x 2) (<= 1001/1000 y 2))\n (let ((t (* x y))) (/ (- t 1) (- (* t t) 1))))"},{"body":"(let ((p0 (- (+ x0 x1) x2)) (p1 (- (+ x1 x2) x0)) (p2 (- (+ x2 x0) x1)))\n  (+ (+ p0 p1) p2))","arguments":["x0","x1","x2"],"operators":["let","-","+"],":precision":"binary32",":pre":"(and (< 1 x0 2) (< 1 x1 2) (< 1 x2 2))",":name":"test01_sum3","core_fptaylor":"{\nVariables\n\treal x0 in [1, 2];\n\treal x1 in [1, 2];\n\treal x2 in [1, 2];\n\nDefinitions\n\tp0 rnd32= ((x0 + x1) - x2);\n\tp1 rnd32= ((x1 + x2) - x0);\n\tp2 rnd32= ((x2 + x0) - x1);\n\nExpressions\n\ttest01_sum3 rnd32= ((p0 + p1) + p2);\n}\n","core":"(FPCore\n (x0 x1 x2)\n :name\n \"test01_sum3\"\n :precision\n binary32\n :pre\n (and (< 1 x0 2) (< 1 x1 2) (< 1 x2 2))\n (let ((p0 (- (+ x0 x1) x2)) (p1 (- (+ x1 x2) x0)) (p2 (- (+ x2 x0) x1)))\n   (+ (+ p0 p1) p2)))"},{"body":"(+ (+ (+ (+ (+ (+ (+ x0 x1) x2) x3) x4) x5) x6) x7)","arguments":["x0","x1","x2","x3","x4","x5","x6","x7"],"operators":["+"],":precision":"binary64",":pre":"(and (< 1 x0 2)\n     (< 1 x1 2)\n     (< 1 x2 2)\n     (< 1 x3 2)\n     (< 1 x4 2)\n     (< 1 x5 2)\n     (< 1 x6 2)\n     (< 1 x7 2))",":name":"test02_sum8","core_fptaylor":"{\nVariables\n\treal x0 in [1, 2];\n\treal x1 in [1, 2];\n\treal x2 in [1, 2];\n\treal x3 in [1, 2];\n\treal x4 in [1, 2];\n\treal x5 in [1, 2];\n\treal x6 in [1, 2];\n\treal x7 in [1, 2];\n\nExpressions\n\ttest02_sum8 rnd64= (((((((x0 + x1) + x2) + x3) + x4) + x5) + x6) + x7);\n}\n","core":"(FPCore\n (x0 x1 x2 x3 x4 x5 x6 x7)\n :name\n \"test02_sum8\"\n :precision\n binary64\n :pre\n (and (< 1 x0 2)\n      (< 1 x1 2)\n      (< 1 x2 2)\n      (< 1 x3 2)\n      (< 1 x4 2)\n      (< 1 x5 2)\n      (< 1 x6 2)\n      (< 1 x7 2))\n (+ (+ (+ (+ (+ (+ (+ x0 x1) x2) x3) x4) x5) x6) x7))"},{"body":"(/ (+ x y) (- x y))","arguments":["x","y"],"operators":["/","+","-"],":precision":"binary64",":pre":"(and (< 0 x 1) (< -1 y -1/10))",":name":"test03_nonlin2","core_fptaylor":"{\nVariables\n\treal x in [0, 1];\n\treal y in [-1, -1000000000000000055511151231257827021181583404541015625e-55];\n\nExpressions\n\ttest03_nonlin2 rnd64= ((x + y) / (x - y));\n}\n","core":"(FPCore\n (x y)\n :name\n \"test03_nonlin2\"\n :precision\n binary64\n :pre\n (and (< 0 x 1) (< -1 y -1/10))\n (/ (+ x y) (- x y)))"},{"body":"(let ((v2 (* (* w2 (- 0 m2)) (* -3 (* (* 1 (/ a2 w2)) (/ a2 w2)))))\n      (v1 (* (* w1 (- 0 m1)) (* -3 (* (* 1 (/ a1 w1)) (/ a1 w1)))))\n      (v0 (* (* w0 (- 0 m0)) (* -3 (* (* 1 (/ a0 w0)) (/ a0 w0))))))\n  (+ 0 (+ (* v0 1) (+ (* v1 1) (+ (* v2 1) 0)))))","arguments":["m0","m1","m2","w0","w1","w2","a0","a1","a2"],"operators":["let","*","-","/","+"],":precision":"binary64",":pre":"(and (< -1 m0 1)\n     (< -1 m1 1)\n     (< -1 m2 1)\n     (< 1/100000 w0 1)\n     (< 1/100000 w1 1)\n     (< 1/100000 w2 1)\n     (< 1/100000 a0 1)\n     (< 1/100000 a1 1)\n     (< 1/100000 a2 1))",":name":"test04_dqmom9","core_fptaylor":"{\nVariables\n\treal m0 in [-1, 1];\n\treal m1 in [-1, 1];\n\treal m2 in [-1, 1];\n\treal w0 in [10000000000000000818030539140313095458623138256371021270751953125e-69, 1];\n\treal w1 in [10000000000000000818030539140313095458623138256371021270751953125e-69, 1];\n\treal w2 in [10000000000000000818030539140313095458623138256371021270751953125e-69, 1];\n\treal a0 in [10000000000000000818030539140313095458623138256371021270751953125e-69, 1];\n\treal a1 in [10000000000000000818030539140313095458623138256371021270751953125e-69, 1];\n\treal a2 in [10000000000000000818030539140313095458623138256371021270751953125e-69, 1];\n\nDefinitions\n\tv2 rnd64= ((w2 * (0 - m2)) * (-3 * ((1 * (a2 / w2)) * (a2 / w2))));\n\tv1 rnd64= ((w1 * (0 - m1)) * (-3 * ((1 * (a1 / w1)) * (a1 / w1))));\n\tv0 rnd64= ((w0 * (0 - m0)) * (-3 * ((1 * (a0 / w0)) * (a0 / w0))));\n\nExpressions\n\ttest04_dqmom9 rnd64= (0 + ((v0 * 1) + ((v1 * 1) + ((v2 * 1) + 0))));\n}\n","core":"(FPCore\n (m0 m1 m2 w0 w1 w2 a0 a1 a2)\n :name\n \"test04_dqmom9\"\n :precision\n binary64\n :pre\n (and (< -1 m0 1)\n      (< -1 m1 1)\n      (< -1 m2 1)\n      (< 1/100000 w0 1)\n      (< 1/100000 w1 1)\n      (< 1/100000 w2 1)\n      (< 1/100000 a0 1)\n      (< 1/100000 a1 1)\n      (< 1/100000 a2 1))\n (let ((v2 (* (* w2 (- 0 m2)) (* -3 (* (* 1 (/ a2 w2)) (/ a2 w2)))))\n       (v1 (* (* w1 (- 0 m1)) (* -3 (* (* 1 (/ a1 w1)) (/ a1 w1)))))\n       (v0 (* (* w0 (- 0 m0)) (* -3 (* (* 1 (/ a0 w0)) (/ a0 w0))))))\n   (+ 0 (+ (* v0 1) (+ (* v1 1) (+ (* v2 1) 0))))))"},{"body":"(let ((r1 (- x 1)) (r2 (* x x))) (/ r1 (- r2 1)))","arguments":["x"],"operators":["let","-","*","/"],":precision":"binary64",":pre":"(< 100001/100000 x 2)",":name":"test05_nonlin1, r4","core_fptaylor":"{\nVariables\n\treal x in [1000010000000000065512040237081237137317657470703125e-51, 2];\n\nDefinitions\n\tr1 rnd64= (x - 1);\n\tr2 rnd64= (x * x);\n\nExpressions\n\ttest05_nonlin1$44$$32$r4 rnd64= (r1 / (r2 - 1));\n}\n","core":"(FPCore\n (x)\n :name\n \"test05_nonlin1, r4\"\n :precision\n binary64\n :pre\n (< 100001/100000 x 2)\n (let ((r1 (- x 1)) (r2 (* x x))) (/ r1 (- r2 1))))"},{"body":"(/ 1 (+ x 1))","arguments":["x"],"operators":["/","+"],":precision":"binary64",":pre":"(< 100001/100000 x 2)",":name":"test05_nonlin1, test2","core_fptaylor":"{\nVariables\n\treal x in [1000010000000000065512040237081237137317657470703125e-51, 2];\n\nExpressions\n\ttest05_nonlin1$44$$32$test2 rnd64= (1 / (x + 1));\n}\n","core":"(FPCore\n (x)\n :name\n \"test05_nonlin1, test2\"\n :precision\n binary64\n :pre\n (< 100001/100000 x 2)\n (/ 1 (+ x 1)))"},{"body":"(+ (+ (+ x0 x1) x2) x3)","arguments":["x0","x1","x2","x3"],"operators":["+"],":precision":"binary32",":pre":"(and (< -1/100000 x0 100001/100000) (< 0 x1 1) (< 0 x2 1) (< 0 x3 1))",":name":"test06_sums4, sum1","core_fptaylor":"{\nVariables\n\treal x0 in [-10000000000000000818030539140313095458623138256371021270751953125e-69, 1000010000000000065512040237081237137317657470703125e-51];\n\treal x1 in [0, 1];\n\treal x2 in [0, 1];\n\treal x3 in [0, 1];\n\nExpressions\n\ttest06_sums4$44$$32$sum1 rnd32= (((x0 + x1) + x2) + x3);\n}\n","core":"(FPCore\n (x0 x1 x2 x3)\n :name\n \"test06_sums4, sum1\"\n :precision\n binary32\n :pre\n (and (< -1/100000 x0 100001/100000) (< 0 x1 1) (< 0 x2 1) (< 0 x3 1))\n (+ (+ (+ x0 x1) x2) x3))"},{"body":"(+ (+ x0 x1) (+ x2 x3))","arguments":["x0","x1","x2","x3"],"operators":["+"],":precision":"binary32",":pre":"(and (< -1/100000 x0 100001/100000) (< 0 x1 1) (< 0 x2 1) (< 0 x3 1))",":name":"test06_sums4, sum2","core_fptaylor":"{\nVariables\n\treal x0 in [-10000000000000000818030539140313095458623138256371021270751953125e-69, 1000010000000000065512040237081237137317657470703125e-51];\n\treal x1 in [0, 1];\n\treal x2 in [0, 1];\n\treal x3 in [0, 1];\n\nExpressions\n\ttest06_sums4$44$$32$sum2 rnd32= ((x0 + x1) + (x2 + x3));\n}\n","core":"(FPCore\n (x0 x1 x2 x3)\n :name\n \"test06_sums4, sum2\"\n :precision\n binary32\n :pre\n (and (< -1/100000 x0 100001/100000) (< 0 x1 1) (< 0 x2 1) (< 0 x3 1))\n (+ (+ x0 x1) (+ x2 x3)))"},{"body":"(let* ((q\n        (- (fabs (- x (sqrt (+ (* x x) 1)))) (/ 1 (+ x (sqrt (+ (* x x) 1))))))\n       (y (* q q)))\n  (if (== y 0) 1 (/ (- (exp y) 1) x)))","arguments":["x"],"operators":["let*","-","fabs","sqrt","+","*","/","if","==","exp"],":cite":["end-of-error"],":spec":"1.0",":name":"Gustafson's example","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"Gustafson's example\"\n :cite\n (end-of-error)\n :spec\n 1\n (let* ((q\n         (-\n          (fabs (- x (sqrt (+ (* x x) 1))))\n          (/ 1 (+ x (sqrt (+ (* x x) 1))))))\n        (y (* q q)))\n   (if (== y 0) 1 (/ (- (exp y) 1) x))))"},{"body":"(- (sqrt (+ x 1)) (sqrt x))","arguments":["x"],"operators":["-","sqrt","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(>= x 0)",":name":"NMSE example 3.1","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE example 3.1\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (>= x 0)\n (- (sqrt (+ x 1)) (sqrt x)))"},{"body":"(- (sin (+ x eps)) (sin x))","arguments":["x","eps"],"operators":["-","sin","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE example 3.3","core_fptaylor":false,"core":"(FPCore\n (x eps)\n :name\n \"NMSE example 3.3\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (- (sin (+ x eps)) (sin x)))"},{"body":"(/ (- 1 (cos x)) (sin x))","arguments":["x"],"operators":["/","-","cos","sin"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE example 3.4","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE example 3.4\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (/ (- 1 (cos x)) (sin x)))"},{"body":"(- (atan (+ N 1)) (atan N))","arguments":["N"],"operators":["-","atan","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE example 3.5","core_fptaylor":false,"core":"(FPCore\n (N)\n :name\n \"NMSE example 3.5\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (- (atan (+ N 1)) (atan N)))"},{"body":"(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))","arguments":["x"],"operators":["-","/","sqrt","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(>= x 0)",":name":"NMSE example 3.6","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE example 3.6\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (>= x 0)\n (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))"},{"body":"(- (/ 1 (+ x 1)) (/ 1 x))","arguments":["x"],"operators":["-","/","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE problem 3.3.1","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.3.1\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (- (/ 1 (+ x 1)) (/ 1 x)))"},{"body":"(- (tan (+ x eps)) (tan x))","arguments":["x","eps"],"operators":["-","tan","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE problem 3.3.2","core_fptaylor":false,"core":"(FPCore\n (x eps)\n :name\n \"NMSE problem 3.3.2\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (- (tan (+ x eps)) (tan x)))"},{"body":"(+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1)))","arguments":["x"],"operators":["+","-","/"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0 1 -1)",":name":"NMSE problem 3.3.3","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.3.3\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0 1 -1)\n (+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1))))"},{"body":"(- (pow (+ x 1) (/ 1 3)) (pow x (/ 1 3)))","arguments":["x"],"operators":["-","pow","+","/"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(>= x 0)",":name":"NMSE problem 3.3.4","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.3.4\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (>= x 0)\n (- (pow (+ x 1) (/ 1 3)) (pow x (/ 1 3))))"},{"body":"(- (cos (+ x eps)) (cos x))","arguments":["x","eps"],"operators":["-","cos","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE problem 3.3.5","core_fptaylor":false,"core":"(FPCore\n (x eps)\n :name\n \"NMSE problem 3.3.5\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (- (cos (+ x eps)) (cos x)))"},{"body":"(- (log (+ N 1)) (log N))","arguments":["N"],"operators":["-","log","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(> N 0)",":name":"NMSE problem 3.3.6","core_fptaylor":false,"core":"(FPCore\n (N)\n :name\n \"NMSE problem 3.3.6\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (> N 0)\n (- (log (+ N 1)) (log N)))"},{"body":"(+ (- (exp x) 2) (exp (- x)))","arguments":["x"],"operators":["+","-","exp"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE problem 3.3.7","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.3.7\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (+ (- (exp x) 2) (exp (- x))))"},{"body":"(/ (+ (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a))","arguments":["a","b","c"],"operators":["/","+","-","sqrt","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(and (>= (* b b) (* 4 (* a c))) (!= a 0))",":name":"NMSE p42, positive","core_fptaylor":false,"core":"(FPCore\n (a b c)\n :name\n \"NMSE p42, positive\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (and (>= (* b b) (* 4 (* a c))) (!= a 0))\n (/ (+ (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))"},{"body":"(/ (- (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a))","arguments":["a","b","c"],"operators":["/","-","sqrt","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(and (>= (* b b) (* 4 (* a c))) (!= a 0))",":name":"NMSE p42, negative","core_fptaylor":false,"core":"(FPCore\n (a b c)\n :name\n \"NMSE p42, negative\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (and (>= (* b b) (* 4 (* a c))) (!= a 0))\n (/ (- (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))"},{"body":"(/ (+ (- b2) (sqrt (- (* b2 b2) (* a c)))) a)","arguments":["a","b2","c"],"operators":["/","+","-","sqrt","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(and (>= (* b2 b2) (* a c)) (!= a 0))",":name":"NMSE problem 3.2.1, positive","core_fptaylor":false,"core":"(FPCore\n (a b2 c)\n :name\n \"NMSE problem 3.2.1, positive\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (and (>= (* b2 b2) (* a c)) (!= a 0))\n (/ (+ (- b2) (sqrt (- (* b2 b2) (* a c)))) a))"},{"body":"(/ (- (- b2) (sqrt (- (* b2 b2) (* a c)))) a)","arguments":["a","b2","c"],"operators":["/","-","sqrt","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(and (>= (* b2 b2) (* a c)) (!= a 0))",":name":"NMSE problem 3.2.1, negative","core_fptaylor":false,"core":"(FPCore\n (a b2 c)\n :name\n \"NMSE problem 3.2.1, negative\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (and (>= (* b2 b2) (* a c)) (!= a 0))\n (/ (- (- b2) (sqrt (- (* b2 b2) (* a c)))) a))"},{"body":"(- (exp x) 1)","arguments":["x"],"operators":["-","exp"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE example 3.7","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE example 3.7\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (- (exp x) 1))"},{"body":"(- (- (* (+ N 1) (log (+ N 1))) (* N (log N))) 1)","arguments":["N"],"operators":["-","*","+","log"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(> N 0)",":name":"NMSE example 3.8","core_fptaylor":false,"core":"(FPCore\n (N)\n :name\n \"NMSE example 3.8\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (> N 0)\n (- (- (* (+ N 1) (log (+ N 1))) (* N (log N))) 1))"},{"body":"(- (/ 1 x) (/ 1 (tan x)))","arguments":["x"],"operators":["-","/","tan"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE example 3.9","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE example 3.9\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (- (/ 1 x) (/ 1 (tan x))))"},{"body":"(/ (log (- 1 x)) (log (+ 1 x)))","arguments":["x"],"operators":["/","log","-","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(< -1 x 1)",":name":"NMSE example 3.10","core_fptaylor":"{\nVariables\n\treal x in [-1, 1];\n\nExpressions\n\tNMSE$32$example$32$3$46$10 rnd64= (log((1 - x)) / log((1 + x)));\n}\n","core":"(FPCore\n (x)\n :name\n \"NMSE example 3.10\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (< -1 x 1)\n (/ (log (- 1 x)) (log (+ 1 x))))"},{"body":"(/ (- 1 (cos x)) (* x x))","arguments":["x"],"operators":["/","-","cos","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE problem 3.4.1","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.4.1\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (/ (- 1 (cos x)) (* x x)))"},{"body":"(/\n (* eps (- (exp (* (+ a b) eps)) 1))\n (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)))","arguments":["a","b","eps"],"operators":["/","*","-","exp","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= eps 0)",":name":"NMSE problem 3.4.2","core_fptaylor":false,"core":"(FPCore\n (a b eps)\n :name\n \"NMSE problem 3.4.2\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= eps 0)\n (/\n  (* eps (- (exp (* (+ a b) eps)) 1))\n  (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))))"},{"body":"(log (/ (- 1 eps) (+ 1 eps)))","arguments":["eps"],"operators":["log","/","-","+"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(< -1 eps 1)",":name":"NMSE problem 3.4.3","core_fptaylor":"{\nVariables\n\treal eps in [-1, 1];\n\nExpressions\n\tNMSE$32$problem$32$3$46$4$46$3 rnd64= log(((1 - eps) / (1 + eps)));\n}\n","core":"(FPCore\n (eps)\n :name\n \"NMSE problem 3.4.3\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (< -1 eps 1)\n (log (/ (- 1 eps) (+ 1 eps))))"},{"body":"(sqrt (/ (- (exp (* 2 x)) 1) (- (exp x) 1)))","arguments":["x"],"operators":["sqrt","/","-","exp","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE problem 3.4.4","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.4.4\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (sqrt (/ (- (exp (* 2 x)) 1) (- (exp x) 1))))"},{"body":"(/ (- x (sin x)) (- x (tan x)))","arguments":["x"],"operators":["/","-","sin","tan"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE problem 3.4.5","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE problem 3.4.5\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (/ (- x (sin x)) (- x (tan x))))"},{"body":"(- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)))","arguments":["x","n"],"operators":["-","pow","+","/"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(>= x 0)",":name":"NMSE problem 3.4.6","core_fptaylor":false,"core":"(FPCore\n (x n)\n :name\n \"NMSE problem 3.4.6\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (>= x 0)\n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))))"},{"body":"(- (exp (* a x)) 1)","arguments":["a","x"],"operators":["-","exp","*"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":name":"NMSE section 3.5","core_fptaylor":false,"core":"(FPCore\n (a x)\n :name\n \"NMSE section 3.5\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n (- (exp (* a x)) 1))"},{"body":"(/ (exp x) (- (exp x) 1))","arguments":["x"],"operators":["/","exp","-"],":cite":["hamming-1987","herbie-2015"],":fpbench-domain":"textbook",":pre":"(!= x 0)",":name":"NMSE section 3.11","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"NMSE section 3.11\"\n :cite\n (hamming-1987 herbie-2015)\n :fpbench-domain\n textbook\n :pre\n (!= x 0)\n (/ (exp x) (- (exp x) 1)))"},{"body":"(* 1/2 (sqrt (* 2 (+ (sqrt (+ (* re re) (* im im))) re))))","arguments":["re","im"],"operators":["*","sqrt","+"],":cite":["herbie-2015"],":name":"Complex square root","core_fptaylor":false,"core":"(FPCore\n (re im)\n :name\n \"Complex square root\"\n :cite\n (herbie-2015)\n (* 1/2 (sqrt (* 2 (+ (sqrt (+ (* re re) (* im im))) re)))))"},{"body":"(* (* 1/2 (sin re)) (- (exp (- im)) (exp im)))","arguments":["re","im"],"operators":["*","sin","-","exp"],":cite":["herbie-2015"],":name":"Complex sine and cosine","core_fptaylor":false,"core":"(FPCore\n (re im)\n :name\n \"Complex sine and cosine\"\n :cite\n (herbie-2015)\n (* (* 1/2 (sin re)) (- (exp (- im)) (exp im))))"},{"body":"(/\n (* (pow (/ 1 (+ 1 (exp (- s)))) cp) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) cn))\n (* (pow (/ 1 (+ 1 (exp (- t)))) cp) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) cn)))","arguments":["cp","cn","t","s"],"operators":["/","*","pow","+","exp","-"],":cite":["herbie-2015"],":pre":"(and (< 0 cp) (< 0 cn))",":name":"Probabilities in a clustering algorithm","core_fptaylor":false,"core":"(FPCore\n (cp cn t s)\n :name\n \"Probabilities in a clustering algorithm\"\n :cite\n (herbie-2015)\n :pre\n (and (< 0 cp) (< 0 cn))\n (/\n  (* (pow (/ 1 (+ 1 (exp (- s)))) cp) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) cn))\n  (* (pow (/ 1 (+ 1 (exp (- t)))) cp) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) cn))))"},{"body":"(- (tan x) x)","arguments":["x"],"operators":["-","tan"],":precision":"(decimal 25)",":pre":"(== x 1428599129020608582548671)","core_fptaylor":false,"core":"(FPCore\n (x)\n :pre\n (== x 1428599129020608582548671)\n :precision\n (decimal 25)\n :description\n \"Introduced in 'arbitrary-precision'\"\n (- (tan x) x))",":description":"Introduced in 'arbitrary-precision'"},{"body":"(let ((s1 (- (* x1 y2) (* y1 x2)))\n      (s2 (- (* x2 y3) (* y2 x3)))\n      (s3 (- (* x3 y1) (* y3 x1))))\n  (* 1/2 (+ (+ s1 s2) s3)))","arguments":["x1","y1","x2","y2","x3","y3"],"operators":["let","-","*","+"],":precision":"binary64",":name":"Shoelace formula","core_fptaylor":false,"core":"(FPCore\n (x1 y1 x2 y2 x3 y3)\n :name\n \"Shoelace formula\"\n :description\n \"Introduced in 'polygon-area'\"\n :precision\n binary64\n (let ((s1 (- (* x1 y2) (* y1 x2)))\n       (s2 (- (* x2 y3) (* y2 x3)))\n       (s3 (- (* x3 y1) (* y3 x1))))\n   (* 1/2 (+ (+ s1 s2) s3))))",":description":"Introduced in 'polygon-area'"},{"body":"(let* ((dppi PI) (h (/ dppi n)) (t1 0))\n  (while*\n   (<= i n)\n   ((t2\n     0\n     (let ((x (* i h)))\n       (while*\n        (<= k 5)\n        ((d1 (! :precision binary32 1) (! :precision binary32 (* d1 2)))\n         (t1 x (+ t1 (/ (sin (* d1 x)) d1)))\n         (k (! :precision integer 1) (! :precision integer (+ k 1))))\n        t1)))\n    (s1\n     0\n     (let ((s0 (sqrt (+ (* h h) (* (- t2 t1) (- t2 t1))))))\n       (! :precision binary80 (+ s1 s0))))\n    (t1 t1 t2)\n    (i (! :precision integer 1) (! :precision integer (+ i 1))))\n   s1))","arguments":["(! :precision integer n)"],"operators":["let*","/","while*","<=","!","let","*","+","sin","sqrt","-"],":cite":["precimonious-2013"],":precision":"binary64",":pre":"(>= n 0)",":name":"arclength of a wiggly function",":fpbench-pre-override":"(<= 50 x 60)","core_fptaylor":false,"core":"(FPCore\n ((! :precision integer n))\n :name\n \"arclength of a wiggly function\"\n :cite\n (precimonious-2013)\n :precision\n binary64\n :pre\n (>= n 0)\n :fpbench-allowed-ulps\n 10\n :fpbench-pre-override\n (<= 50 x 60)\n (let* ((dppi PI) (h (/ dppi n)) (t1 0))\n   (while*\n    (<= i n)\n    ((t2\n      0\n      (let ((x (* i h)))\n        (while*\n         (<= k 5)\n         ((d1 (! :precision binary32 1) (! :precision binary32 (* d1 2)))\n          (t1 x (+ t1 (/ (sin (* d1 x)) d1)))\n          (k (! :precision integer 1) (! :precision integer (+ k 1))))\n         t1)))\n     (s1\n      0\n      (let ((s0 (sqrt (+ (* h h) (* (- t2 t1) (- t2 t1))))))\n        (! :precision binary80 (+ s1 s0))))\n     (t1 t1 t2)\n     (i (! :precision integer 1) (! :precision integer (+ i 1))))\n    s1)))",":fpbench-allowed-ulps":"10.0"},{"body":"(let ((dppi (acos -1)))\n  (let ((h (/ dppi n)))\n    (while\n     (<= i n)\n     ((s1\n       0\n       (let ((t2\n              (let ((x (* i h)))\n                (while\n                 (<= k 5)\n                 ((d0\n                   (! :precision binary32 2)\n                   (! :precision binary32 (* 2 d0)))\n                  (t0 x (+ t0 (/ (sin (* d0 x)) d0)))\n                  (k 1 (+ k 1)))\n                 t0))))\n         (let ((s0 (sqrt (+ (* h h) (* (- t2 t1) (- t2 t1))))))\n           (! :precision binary80 (+ s1 s0)))))\n      (t1\n       0\n       (let ((t2\n              (let ((x (* i h)))\n                (while\n                 (<= k 5)\n                 ((d0\n                   (! :precision binary32 2)\n                   (! :precision binary32 (* 2 d0)))\n                  (t0 x (+ t0 (/ (sin (* d0 x)) d0)))\n                  (k 1 (+ k 1)))\n                 t0))))\n         t2))\n      (i 1 (+ i 1)))\n     s1)))","arguments":["n"],"operators":["let","acos","/","while","<=","*","!","+","sin","sqrt","-"],":cite":["precimonious-2013"],":precision":"binary64",":pre":"(>= n 0)",":name":"arclength of a wiggly function (old version)",":fpbench-pre-override":"(<= 50 x 60)","core_fptaylor":false,"core":"(FPCore\n (n)\n :name\n \"arclength of a wiggly function (old version)\"\n :cite\n (precimonious-2013)\n :precision\n binary64\n :pre\n (>= n 0)\n :fpbench-pre-override\n (<= 50 x 60)\n (let ((dppi (acos -1)))\n   (let ((h (/ dppi n)))\n     (while\n      (<= i n)\n      ((s1\n        0\n        (let ((t2\n               (let ((x (* i h)))\n                 (while\n                  (<= k 5)\n                  ((d0\n                    (! :precision binary32 2)\n                    (! :precision binary32 (* 2 d0)))\n                   (t0 x (+ t0 (/ (sin (* d0 x)) d0)))\n                   (k 1 (+ k 1)))\n                  t0))))\n          (let ((s0 (sqrt (+ (* h h) (* (- t2 t1) (- t2 t1))))))\n            (! :precision binary80 (+ s1 s0)))))\n       (t1\n        0\n        (let ((t2\n               (let ((x (* i h)))\n                 (while\n                  (<= k 5)\n                  ((d0\n                    (! :precision binary32 2)\n                    (! :precision binary32 (* 2 d0)))\n                   (t0 x (+ t0 (/ (sin (* d0 x)) d0)))\n                   (k 1 (+ k 1)))\n                  t0))))\n          t2))\n       (i 1 (+ i 1)))\n      s1))))"},{"body":"(let ((t1 (+ 1657/5 (* 3/5 T)))) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))","arguments":["u","v","T"],"operators":["let","+","*","/","-"],":cite":["darulova-kuncak-2014"],":fpbench-domain":"science",":precision":"binary64",":pre":"(and (<= -100 u 100) (<= 20 v 20000) (<= -30 T 50))",":name":"doppler1",":rosa-ensuring":"1e-12","core_fptaylor":"{\nVariables\n\treal u in [-100, 100];\n\treal v in [20, 2e4];\n\treal T in [-30, 50];\n\nDefinitions\n\tt1 rnd64= (3314e-1 + (6e-1 * T));\n\nExpressions\n\tdoppler1 rnd64= ((-t1 * v) / ((t1 + u) * (t1 + u)));\n}\n","core":"(FPCore\n (u v T)\n :name\n \"doppler1\"\n :cite\n (darulova-kuncak-2014)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (and (<= -100 u 100) (<= 20 v 20000) (<= -30 T 50))\n :rosa-ensuring\n 1/1000000000000\n (let ((t1 (+ 1657/5 (* 3/5 T)))) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u)))))"},{"body":"(let ((t1 (+ 1657/5 (* 3/5 T)))) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))","arguments":["u","v","T"],"operators":["let","+","*","/","-"],":cite":["darulova-kuncak-2014"],":fpbench-domain":"science",":precision":"binary64",":pre":"(and (<= -125 u 125) (<= 15 v 25000) (<= -40 T 60))",":name":"doppler2","core_fptaylor":"{\nVariables\n\treal u in [-125, 125];\n\treal v in [15, 25000];\n\treal T in [-40, 60];\n\nDefinitions\n\tt1 rnd64= (3314e-1 + (6e-1 * T));\n\nExpressions\n\tdoppler2 rnd64= ((-t1 * v) / ((t1 + u) * (t1 + u)));\n}\n","core":"(FPCore\n (u v T)\n :name\n \"doppler2\"\n :cite\n (darulova-kuncak-2014)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (and (<= -125 u 125) (<= 15 v 25000) (<= -40 T 60))\n (let ((t1 (+ 1657/5 (* 3/5 T)))) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u)))))"},{"body":"(let ((t1 (+ 1657/5 (* 3/5 T)))) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))","arguments":["u","v","T"],"operators":["let","+","*","/","-"],":cite":["darulova-kuncak-2014"],":fpbench-domain":"science",":precision":"binary64",":pre":"(and (<= -30 u 120) (<= 320 v 20300) (<= -50 T 30))",":name":"doppler3","core_fptaylor":"{\nVariables\n\treal u in [-30, 120];\n\treal v in [320, 20300];\n\treal T in [-50, 30];\n\nDefinitions\n\tt1 rnd64= (3314e-1 + (6e-1 * T));\n\nExpressions\n\tdoppler3 rnd64= ((-t1 * v) / ((t1 + u) * (t1 + u)));\n}\n","core":"(FPCore\n (u v T)\n :name\n \"doppler3\"\n :cite\n (darulova-kuncak-2014)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (and (<= -30 u 120) (<= 320 v 20300) (<= -50 T 30))\n (let ((t1 (+ 1657/5 (* 3/5 T)))) (/ (* (- t1) v) (* (+ t1 u) (+ t1 u)))))"},{"body":"(- (- (- (- (* x1 x2)) (* (* 2 x2) x3)) x1) x3)","arguments":["x1","x2","x3"],"operators":["-","*"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"science",":precision":"binary64",":pre":"(and (<= -15 x1 15) (<= -15 x2 15) (<= -15 x3 15))",":name":"rigidBody1","core_fptaylor":"{\nVariables\n\treal x1 in [-15, 15];\n\treal x2 in [-15, 15];\n\treal x3 in [-15, 15];\n\nExpressions\n\trigidBody1 rnd64= (((-(x1 * x2) - ((2 * x2) * x3)) - x1) - x3);\n}\n","core":"(FPCore\n (x1 x2 x3)\n :name\n \"rigidBody1\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (and (<= -15 x1 15) (<= -15 x2 15) (<= -15 x3 15))\n (- (- (- (- (* x1 x2)) (* (* 2 x2) x3)) x1) x3))"},{"body":"(-\n (+\n  (- (+ (* (* (* 2 x1) x2) x3) (* (* 3 x3) x3)) (* (* (* x2 x1) x2) x3))\n  (* (* 3 x3) x3))\n x2)","arguments":["x1","x2","x3"],"operators":["-","+","*"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"science",":precision":"binary64",":pre":"(and (<= -15 x1 15) (<= -15 x2 15) (<= -15 x3 15))",":name":"rigidBody2","core_fptaylor":"{\nVariables\n\treal x1 in [-15, 15];\n\treal x2 in [-15, 15];\n\treal x3 in [-15, 15];\n\nExpressions\n\trigidBody2 rnd64= (((((((2 * x1) * x2) * x3) + ((3 * x3) * x3)) - (((x2 * x1) * x2) * x3)) + ((3 * x3) * x3)) - x2);\n}\n","core":"(FPCore\n (x1 x2 x3)\n :name\n \"rigidBody2\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (and (<= -15 x1 15) (<= -15 x2 15) (<= -15 x3 15))\n (-\n  (+\n   (- (+ (* (* (* 2 x1) x2) x3) (* (* 3 x3) x3)) (* (* (* x2 x1) x2) x3))\n   (* (* 3 x3) x3))\n  x2))"},{"body":"(let ((t (- (+ (* (* 3 x1) x1) (* 2 x2)) x1))\n      (t* (- (- (* (* 3 x1) x1) (* 2 x2)) x1))\n      (d (+ (* x1 x1) 1)))\n  (let ((s (/ t d)) (s* (/ t* d)))\n    (+\n     x1\n     (+\n      (+\n       (+\n        (+\n         (* (+ (* (* (* 2 x1) s) (- s 3)) (* (* x1 x1) (- (* 4 s) 6))) d)\n         (* (* (* 3 x1) x1) s))\n        (* (* x1 x1) x1))\n       x1)\n      (* 3 s*)))))","arguments":["x1","x2"],"operators":["let","-","+","*","/"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"controls",":precision":"binary64",":pre":"(and (<= -5 x1 5) (<= -20 x2 5))",":name":"jetEngine","core_fptaylor":"{\nVariables\n\treal x1 in [-5, 5];\n\treal x2 in [-20, 5];\n\nDefinitions\n\tt rnd64= ((((3 * x1) * x1) + (2 * x2)) - x1);\n\tt$42$ rnd64= ((((3 * x1) * x1) - (2 * x2)) - x1);\n\td rnd64= ((x1 * x1) + 1);\n\ts rnd64= (t / d);\n\ts$42$ rnd64= (t$42$ / d);\n\nExpressions\n\tjetEngine rnd64= (x1 + (((((((((2 * x1) * s) * (s - 3)) + ((x1 * x1) * ((4 * s) - 6))) * d) + (((3 * x1) * x1) * s)) + ((x1 * x1) * x1)) + x1) + (3 * s$42$)));\n}\n","core":"(FPCore\n (x1 x2)\n :name\n \"jetEngine\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n controls\n :precision\n binary64\n :pre\n (and (<= -5 x1 5) (<= -20 x2 5))\n (let ((t (- (+ (* (* 3 x1) x1) (* 2 x2)) x1))\n       (t* (- (- (* (* 3 x1) x1) (* 2 x2)) x1))\n       (d (+ (* x1 x1) 1)))\n   (let ((s (/ t d)) (s* (/ t* d)))\n     (+\n      x1\n      (+\n       (+\n        (+\n         (+\n          (* (+ (* (* (* 2 x1) s) (- s 3)) (* (* x1 x1) (- (* 4 s) 6))) d)\n          (* (* (* 3 x1) x1) s))\n         (* (* x1 x1) x1))\n        x1)\n       (* 3 s*))))))"},{"body":"(-\n (-\n  (+ 3 (/ 2 (* r r)))\n  (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)))\n 9/2)","arguments":["v","w","r"],"operators":["-","+","/","*"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"controls",":precision":"binary64",":pre":"(and (<= -9/2 v -3/10) (<= 2/5 w 9/10) (<= 19/5 r 39/5))",":name":"turbine1","core_fptaylor":"{\nVariables\n\treal v in [-45e-1, -299999999999999988897769753748434595763683319091796875e-54];\n\treal w in [40000000000000002220446049250313080847263336181640625e-53, 90000000000000002220446049250313080847263336181640625e-53];\n\treal r in [379999999999999982236431605997495353221893310546875e-50, 779999999999999982236431605997495353221893310546875e-50];\n\nExpressions\n\tturbine1 rnd64= (((3 + (2 / (r * r))) - (((125e-3 * (3 - (2 * v))) * (((w * w) * r) * r)) / (1 - v))) - 45e-1);\n}\n","core":"(FPCore\n (v w r)\n :name\n \"turbine1\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n controls\n :precision\n binary64\n :pre\n (and (<= -9/2 v -3/10) (<= 2/5 w 9/10) (<= 19/5 r 39/5))\n (-\n  (-\n   (+ 3 (/ 2 (* r r)))\n   (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)))\n  9/2))"},{"body":"(- (- (* 6 v) (/ (* (* 1/2 v) (* (* (* w w) r) r)) (- 1 v))) 5/2)","arguments":["v","w","r"],"operators":["-","*","/"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"controls",":precision":"binary64",":pre":"(and (<= -9/2 v -3/10) (<= 2/5 w 9/10) (<= 19/5 r 39/5))",":name":"turbine2","core_fptaylor":"{\nVariables\n\treal v in [-45e-1, -299999999999999988897769753748434595763683319091796875e-54];\n\treal w in [40000000000000002220446049250313080847263336181640625e-53, 90000000000000002220446049250313080847263336181640625e-53];\n\treal r in [379999999999999982236431605997495353221893310546875e-50, 779999999999999982236431605997495353221893310546875e-50];\n\nExpressions\n\tturbine2 rnd64= (((6 * v) - (((5e-1 * v) * (((w * w) * r) * r)) / (1 - v))) - 25e-1);\n}\n","core":"(FPCore\n (v w r)\n :name\n \"turbine2\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n controls\n :precision\n binary64\n :pre\n (and (<= -9/2 v -3/10) (<= 2/5 w 9/10) (<= 19/5 r 39/5))\n (- (- (* 6 v) (/ (* (* 1/2 v) (* (* (* w w) r) r)) (- 1 v))) 5/2))"},{"body":"(-\n (-\n  (- 3 (/ 2 (* r r)))\n  (/ (* (* 1/8 (+ 1 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)))\n 1/2)","arguments":["v","w","r"],"operators":["-","/","*","+"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"controls",":precision":"binary64",":pre":"(and (<= -9/2 v -3/10) (<= 2/5 w 9/10) (<= 19/5 r 39/5))",":name":"turbine3","core_fptaylor":"{\nVariables\n\treal v in [-45e-1, -299999999999999988897769753748434595763683319091796875e-54];\n\treal w in [40000000000000002220446049250313080847263336181640625e-53, 90000000000000002220446049250313080847263336181640625e-53];\n\treal r in [379999999999999982236431605997495353221893310546875e-50, 779999999999999982236431605997495353221893310546875e-50];\n\nExpressions\n\tturbine3 rnd64= (((3 - (2 / (r * r))) - (((125e-3 * (1 + (2 * v))) * (((w * w) * r) * r)) / (1 - v))) - 5e-1);\n}\n","core":"(FPCore\n (v w r)\n :name\n \"turbine3\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n controls\n :precision\n binary64\n :pre\n (and (<= -9/2 v -3/10) (<= 2/5 w 9/10) (<= 19/5 r 39/5))\n (-\n  (-\n   (- 3 (/ 2 (* r r)))\n   (/ (* (* 1/8 (+ 1 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)))\n  1/2))"},{"body":"(let ((r 4) (K 111/100)) (/ (* r x) (+ 1 (/ x K))))","arguments":["x"],"operators":["let","/","*","+"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"science",":precision":"binary64",":pre":"(<= 1/10 x 3/10)",":name":"verhulst","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000055511151231257827021181583404541015625e-55, 299999999999999988897769753748434595763683319091796875e-54];\n\nDefinitions\n\tr rnd64= 4;\n\tK rnd64= 111e-2;\n\nExpressions\n\tverhulst rnd64= ((r * x) / (1 + (x / K)));\n}\n","core":"(FPCore\n (x)\n :name\n \"verhulst\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (<= 1/10 x 3/10)\n (let ((r 4) (K 111/100)) (/ (* r x) (+ 1 (/ x K)))))"},{"body":"(let ((r 4) (K 111/100)) (/ (* (* r x) x) (+ 1 (* (/ x K) (/ x K)))))","arguments":["x"],"operators":["let","/","*","+"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"science",":precision":"binary64",":pre":"(<= 1/10 x 3/10)",":name":"predatorPrey","core_fptaylor":"{\nVariables\n\treal x in [1000000000000000055511151231257827021181583404541015625e-55, 299999999999999988897769753748434595763683319091796875e-54];\n\nDefinitions\n\tr rnd64= 4;\n\tK rnd64= 111e-2;\n\nExpressions\n\tpredatorPrey rnd64= (((r * x) * x) / (1 + ((x / K) * (x / K))));\n}\n","core":"(FPCore\n (x)\n :name\n \"predatorPrey\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (<= 1/10 x 3/10)\n (let ((r 4) (K 111/100)) (/ (* (* r x) x) (+ 1 (* (/ x K) (/ x K))))))"},{"body":"(let ((p 35000000)\n      (a 401/1000)\n      (b 427/10000000)\n      (t 300)\n      (n 1000)\n      (k 13806503/1000000000000000000000000000000))\n  (- (* (+ p (* (* a (/ n v)) (/ n v))) (- v (* n b))) (* (* k n) t)))","arguments":["v"],"operators":["let","-","*","+","/"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"science",":precision":"binary64",":pre":"(<= 1/10 v 1/2)",":name":"carbonGas","core_fptaylor":"{\nVariables\n\treal v in [1000000000000000055511151231257827021181583404541015625e-55, 5e-1];\n\nDefinitions\n\tp rnd64= 35e6;\n\ta rnd64= 401e-3;\n\tb rnd64= 427e-7;\n\tt rnd64= 300;\n\tn rnd64= 1000;\n\tk rnd64= 13806503e-30;\n\nExpressions\n\tcarbonGas rnd64= (((p + ((a * (n / v)) * (n / v))) * (v - (n * b))) - ((k * n) * t));\n}\n","core":"(FPCore\n (v)\n :name\n \"carbonGas\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n science\n :precision\n binary64\n :pre\n (<= 1/10 v 1/2)\n (let ((p 35000000)\n       (a 401/1000)\n       (b 427/10000000)\n       (t 300)\n       (n 1000)\n       (k 13806503/1000000000000000000000000000000))\n   (- (* (+ p (* (* a (/ n v)) (/ n v))) (- v (* n b))) (* (* k n) t))))"},{":rosa-post":"(=> res (< -1 res 1))","body":"(-\n (+ (- x (/ (* (* x x) x) 6)) (/ (* (* (* (* x x) x) x) x) 120))\n (/ (* (* (* (* (* (* x x) x) x) x) x) x) 5040))","arguments":["x"],"operators":["-","+","/","*"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"mathematics",":precision":"binary64",":pre":"(< -157079632679/100000000000 x 157079632679/100000000000)",":name":"sine",":rosa-ensuring":"1e-14","core_fptaylor":"{\nVariables\n\treal x in [-157079632679000003037117494386620819568634033203125e-50, 157079632679000003037117494386620819568634033203125e-50];\n\nExpressions\n\tsine rnd64= (((x - (((x * x) * x) / 6)) + (((((x * x) * x) * x) * x) / 120)) - (((((((x * x) * x) * x) * x) * x) * x) / 5040));\n}\n","core":"(FPCore\n (x)\n :name\n \"sine\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n mathematics\n :precision\n binary64\n :rosa-post\n (=> res (< -1 res 1))\n :rosa-ensuring\n 1/100000000000000\n :pre\n (< -157079632679/100000000000 x 157079632679/100000000000)\n (-\n  (+ (- x (/ (* (* x x) x) 6)) (/ (* (* (* (* x x) x) x) x) 120))\n  (/ (* (* (* (* (* (* x x) x) x) x) x) x) 5040)))"},{"body":"(-\n (+ (- (+ 1 (* 1/2 x)) (* (* 1/8 x) x)) (* (* (* 1/16 x) x) x))\n (* (* (* (* 5/128 x) x) x) x))","arguments":["x"],"operators":["-","+","*"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"mathematics",":pre":"(<= 0 x 1)",":name":"sqroot","core_fptaylor":"{\nVariables\n\treal x in [0, 1];\n\nExpressions\n\tsqroot rnd64= ((((1 + (5e-1 * x)) - ((125e-3 * x) * x)) + (((625e-4 * x) * x) * x)) - ((((390625e-7 * x) * x) * x) * x));\n}\n","core":"(FPCore\n (x)\n :name\n \"sqroot\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n mathematics\n :pre\n (<= 0 x 1)\n (-\n  (+ (- (+ 1 (* 1/2 x)) (* (* 1/8 x) x)) (* (* (* 1/16 x) x) x))\n  (* (* (* (* 5/128 x) x) x) x)))"},{":rosa-post":"(=> res (< -1 res 1))","body":"(-\n (* 238732414637843/250000000000000 x)\n (* 6450306886639899/50000000000000000 (* (* x x) x)))","arguments":["x"],"operators":["-","*"],":cite":["darulova-kuncak-2014","solovyev-et-al-2015"],":fpbench-domain":"mathematics",":precision":"binary64",":pre":"(< -2 x 2)",":name":"sineOrder3",":rosa-ensuring":"1e-14","core_fptaylor":"{\nVariables\n\treal x in [-2, 2];\n\nExpressions\n\tsineOrder3 rnd64= ((954929658551372e-15 * x) - (12900613773279798e-17 * ((x * x) * x)));\n}\n","core":"(FPCore\n (x)\n :name\n \"sineOrder3\"\n :cite\n (darulova-kuncak-2014 solovyev-et-al-2015)\n :fpbench-domain\n mathematics\n :precision\n binary64\n :pre\n (< -2 x 2)\n :rosa-post\n (=> res (< -1 res 1))\n :rosa-ensuring\n 1/100000000000000\n (-\n  (* 238732414637843/250000000000000 x)\n  (* 6450306886639899/50000000000000000 (* (* x x) x))))"},{"body":"(let ((a 3) (b 7/2))\n  (let ((discr (- (* b b) (* (* a c) 4))))\n    (if (> (- (* b b) (* a c)) 10)\n      (if (> b 0)\n        (/ (* c 2) (- (- b) (sqrt discr)))\n        (if (< b 0)\n          (/ (+ (- b) (sqrt discr)) (* a 2))\n          (/ (+ (- b) (sqrt discr)) (* a 2))))\n      (/ (+ (- b) (sqrt discr)) (* a 2)))))","arguments":["c"],"operators":["let","-","*","if",">","/","sqrt","<","+"],":cite":["darulova-kuncak-2014"],":fpbench-domain":"mathematics",":pre":"(let ((a 3) (b 7/2)) (and (<= -2 c 2) (> (- (* b b) (* (* a c) 4)) 1/10)))",":name":"smartRoot",":rosa-ensuring":"6e-15","core_fptaylor":false,"core":"(FPCore\n (c)\n :name\n \"smartRoot\"\n :cite\n (darulova-kuncak-2014)\n :fpbench-domain\n mathematics\n :pre\n (let ((a 3) (b 7/2)) (and (<= -2 c 2) (> (- (* b b) (* (* a c) 4)) 1/10)))\n :rosa-ensuring\n 3/500000000000000\n (let ((a 3) (b 7/2))\n   (let ((discr (- (* b b) (* (* a c) 4))))\n     (if (> (- (* b b) (* a c)) 10)\n       (if (> b 0)\n         (/ (* c 2) (- (- b) (sqrt discr)))\n         (if (< b 0)\n           (/ (+ (- b) (sqrt discr)) (* a 2))\n           (/ (+ (- b) (sqrt discr)) (* a 2))))\n       (/ (+ (- b) (sqrt discr)) (* a 2))))))"},{":rosa-post":"(=> res (<= 0 res 3))","body":"(if (>= (- (* x x) x) 0) (/ x 10) (+ (* x x) 2))","arguments":["x"],"operators":["if",">=","-","*","/","+"],":cite":["darulova-kuncak-2014"],":pre":"(< 0 x 10)",":name":"cav10",":rosa-ensuring":"3.0","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"cav10\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (< 0 x 10)\n :rosa-post\n (=> res (<= 0 res 3))\n :rosa-ensuring\n 3\n (if (>= (- (* x x) x) 0) (/ x 10) (+ (* x x) 2)))"},{"body":"(if (< x 1/100000) (+ 1 (* 1/2 x)) (sqrt (+ 1 x)))","arguments":["x"],"operators":["if","<","+","*","sqrt"],":cite":["darulova-kuncak-2014"],":pre":"(< 0 x 10)",":name":"squareRoot3",":rosa-ensuring":"1e-10","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"squareRoot3\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (< 0 x 10)\n :rosa-ensuring\n 1/10000000000\n (if (< x 1/100000) (+ 1 (* 1/2 x)) (sqrt (+ 1 x))))"},{"body":"(if (< x 1/10000) (+ 1 (* 1/2 x)) (sqrt (+ 1 x)))","arguments":["x"],"operators":["if","<","+","*","sqrt"],":cite":["darulova-kuncak-2014"],":pre":"(< 0 x 10)",":name":"squareRoot3Invalid",":rosa-ensuring":"1e-10","core_fptaylor":false,"core":"(FPCore\n (x)\n :name\n \"squareRoot3Invalid\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (< 0 x 10)\n :rosa-ensuring\n 1/10000000000\n (if (< x 1/10000) (+ 1 (* 1/2 x)) (sqrt (+ 1 x))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 9 a 9) (<= 471/100 b 489/100) (<= 471/100 c 489/100))",":name":"triangle","core_fptaylor":"{\nVariables\n\treal a in [9, 9];\n\treal b in [470999999999999996447286321199499070644378662109375e-50, 488999999999999968025576890795491635799407958984375e-50];\n\treal c in [470999999999999996447286321199499070644378662109375e-50, 488999999999999968025576890795491635799407958984375e-50];\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 9 a 9) (<= 471/100 b 489/100) (<= 471/100 c 489/100))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{":rosa-post":"(=> res (<= 29/100 res 351/10))","body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/10))\n     (> (+ a c) (+ b 1/10))\n     (> (+ b c) (+ a 1/10)))",":name":"triangle1",":rosa-ensuring":"2.7e-11","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-1));\n\tconstraint1: ((a + c) > (b + 1e-1));\n\tconstraint2: ((b + c) > (a + 1e-1));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle1 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle1\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/10))\n      (> (+ a c) (+ b 1/10))\n      (> (+ b c) (+ a 1/10)))\n :rosa-post\n (=> res (<= 29/100 res 351/10))\n :rosa-ensuring\n 27/1000000000000\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/100))\n     (> (+ a c) (+ b 1/100))\n     (> (+ b c) (+ a 1/100)))",":name":"triangle2","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-2));\n\tconstraint1: ((a + c) > (b + 1e-2));\n\tconstraint2: ((b + c) > (a + 1e-2));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle2 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle2\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/100))\n      (> (+ a c) (+ b 1/100))\n      (> (+ b c) (+ a 1/100)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/1000))\n     (> (+ a c) (+ b 1/1000))\n     (> (+ b c) (+ a 1/1000)))",":name":"triangle3","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-3));\n\tconstraint1: ((a + c) > (b + 1e-3));\n\tconstraint2: ((b + c) > (a + 1e-3));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle3 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle3\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/1000))\n      (> (+ a c) (+ b 1/1000))\n      (> (+ b c) (+ a 1/1000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/10000))\n     (> (+ a c) (+ b 1/10000))\n     (> (+ b c) (+ a 1/10000)))",":name":"triangle4","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-4));\n\tconstraint1: ((a + c) > (b + 1e-4));\n\tconstraint2: ((b + c) > (a + 1e-4));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle4 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle4\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/10000))\n      (> (+ a c) (+ b 1/10000))\n      (> (+ b c) (+ a 1/10000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/100000))\n     (> (+ a c) (+ b 1/100000))\n     (> (+ b c) (+ a 1/100000)))",":name":"triangle5","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-5));\n\tconstraint1: ((a + c) > (b + 1e-5));\n\tconstraint2: ((b + c) > (a + 1e-5));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle5 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle5\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/100000))\n      (> (+ a c) (+ b 1/100000))\n      (> (+ b c) (+ a 1/100000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/1000000))\n     (> (+ a c) (+ b 1/1000000))\n     (> (+ b c) (+ a 1/1000000)))",":name":"triangle6","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-6));\n\tconstraint1: ((a + c) > (b + 1e-6));\n\tconstraint2: ((b + c) > (a + 1e-6));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle6 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle6\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/1000000))\n      (> (+ a c) (+ b 1/1000000))\n      (> (+ b c) (+ a 1/1000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/10000000))\n     (> (+ a c) (+ b 1/10000000))\n     (> (+ b c) (+ a 1/10000000)))",":name":"triangle7","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-7));\n\tconstraint1: ((a + c) > (b + 1e-7));\n\tconstraint2: ((b + c) > (a + 1e-7));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle7 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle7\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/10000000))\n      (> (+ a c) (+ b 1/10000000))\n      (> (+ b c) (+ a 1/10000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/100000000))\n     (> (+ a c) (+ b 1/100000000))\n     (> (+ b c) (+ a 1/100000000)))",":name":"triangle8","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-8));\n\tconstraint1: ((a + c) > (b + 1e-8));\n\tconstraint2: ((b + c) > (a + 1e-8));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle8 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle8\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/100000000))\n      (> (+ a c) (+ b 1/100000000))\n      (> (+ b c) (+ a 1/100000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/1000000000))\n     (> (+ a c) (+ b 1/1000000000))\n     (> (+ b c) (+ a 1/1000000000)))",":name":"triangle9","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-9));\n\tconstraint1: ((a + c) > (b + 1e-9));\n\tconstraint2: ((b + c) > (a + 1e-9));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle9 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle9\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/1000000000))\n      (> (+ a c) (+ b 1/1000000000))\n      (> (+ b c) (+ a 1/1000000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/10000000000))\n     (> (+ a c) (+ b 1/10000000000))\n     (> (+ b c) (+ a 1/10000000000)))",":name":"triangle10","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-10));\n\tconstraint1: ((a + c) > (b + 1e-10));\n\tconstraint2: ((b + c) > (a + 1e-10));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle10 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle10\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/10000000000))\n      (> (+ a c) (+ b 1/10000000000))\n      (> (+ b c) (+ a 1/10000000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/100000000000))\n     (> (+ a c) (+ b 1/100000000000))\n     (> (+ b c) (+ a 1/100000000000)))",":name":"triangle11","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-11));\n\tconstraint1: ((a + c) > (b + 1e-11));\n\tconstraint2: ((b + c) > (a + 1e-11));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle11 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle11\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/100000000000))\n      (> (+ a c) (+ b 1/100000000000))\n      (> (+ b c) (+ a 1/100000000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{"body":"(let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c))))","arguments":["a","b","c"],"operators":["let","/","+","sqrt","*","-"],":cite":["darulova-kuncak-2014"],":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/1000000000000))\n     (> (+ a c) (+ b 1/1000000000000))\n     (> (+ b c) (+ a 1/1000000000000)))",":name":"triangle12","core_fptaylor":"{\nVariables\n\treal a in [1, 9];\n\treal b in [1, 9];\n\treal c in [1, 9];\n\nConstraints\n\tconstraint0: ((a + b) > (c + 1e-12));\n\tconstraint1: ((a + c) > (b + 1e-12));\n\tconstraint2: ((b + c) > (a + 1e-12));\n\nDefinitions\n\ts rnd64= (((a + b) + c) / 2);\n\nExpressions\n\ttriangle12 rnd64= sqrt((((s * (s - a)) * (s - b)) * (s - c)));\n}\n","core":"(FPCore\n (a b c)\n :name\n \"triangle12\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/1000000000000))\n      (> (+ a c) (+ b 1/1000000000000))\n      (> (+ b c) (+ a 1/1000000000000)))\n (let ((s (/ (+ (+ a b) c) 2))) (sqrt (* (* (* s (- s a)) (- s b)) (- s c)))))"},{":rosa-post":"(=> res (<= -17/100 res 1/20))","body":"(/ (- (* (* u u) u)) 6)","arguments":["u"],"operators":["/","-","*"],":cite":["darulova-kuncak-2014"],":pre":"(<= 0 u 1)",":name":"bspline3",":rosa-ensuring":"1e-11","core_fptaylor":"{\nVariables\n\treal u in [0, 1];\n\nExpressions\n\tbspline3 rnd64= (-((u * u) * u) / 6);\n}\n","core":"(FPCore\n (u)\n :name\n \"bspline3\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (<= 0 u 1)\n :rosa-post\n (=> res (<= -17/100 res 1/20))\n :rosa-ensuring\n 1/100000000000\n (/ (- (* (* u u) u)) 6))"},{":rosa-post":"(=> res (>= res 0))","body":"(if (< a b)\n  (/\n   (sqrt (* (* (* (+ c (+ b a)) (- a (- c b))) (+ a (- c b))) (+ c (- b a))))\n   4)\n  (/\n   (sqrt (* (* (* (+ c (+ a b)) (- b (- c a))) (+ b (- c a))) (+ c (- a b))))\n   4))","arguments":["a","b","c"],"operators":["if","<","/","sqrt","*","+","-"],":cite":["darulova-kuncak-2014"],":example":{"c":"8.5","b":"4.0"},":pre":"(and (<= 1 a 9)\n     (<= 1 b 9)\n     (<= 1 c 9)\n     (> (+ a b) (+ c 1/1000000))\n     (> (+ a c) (+ b 1/1000000))\n     (> (+ b c) (+ a 1/1000000))\n     (< a c)\n     (< b c))",":name":"triangleSorted",":rosa-ensuring":"2e-09","core_fptaylor":false,"core":"(FPCore\n (a b c)\n :name\n \"triangleSorted\"\n :cite\n (darulova-kuncak-2014)\n :pre\n (and (<= 1 a 9)\n      (<= 1 b 9)\n      (<= 1 c 9)\n      (> (+ a b) (+ c 1/1000000))\n      (> (+ a c) (+ b 1/1000000))\n      (> (+ b c) (+ a 1/1000000))\n      (< a c)\n      (< b c))\n :rosa-post\n (=> res (>= res 0))\n :rosa-ensuring\n 1/500000000\n :example\n ((b 4) (c 17/2))\n (if (< a b)\n   (/\n    (sqrt (* (* (* (+ c (+ b a)) (- a (- c b))) (+ a (- c b))) (+ c (- b a))))\n    4)\n   (/\n    (sqrt (* (* (* (+ c (+ a b)) (- b (- c a))) (+ b (- c a))) (+ c (- a b))))\n    4)))"},{"body":"(let ((dt 1/10) (solarMass 3947841760435743/100000000000000))\n  (while\n   (< i 100)\n   ((x\n     x0\n     (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n       (let ((mag (/ dt (* (* distance distance) distance))))\n         (let ((vxNew (- vx (* (* x solarMass) mag)))) (+ x (* dt vxNew))))))\n    (y\n     y0\n     (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n       (let ((mag (/ dt (* (* distance distance) distance))))\n         (let ((vyNew (- vy (* (* y solarMass) mag)))) (+ y (* dt vyNew))))))\n    (z\n     z0\n     (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n       (let ((mag (/ dt (* (* distance distance) distance))))\n         (let ((vzNew (- vz (* (* z solarMass) mag)))) (+ z (* dt vzNew))))))\n    (vx\n     vx0\n     (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n       (let ((mag (/ dt (* (* distance distance) distance))))\n         (- vx (* (* x solarMass) mag)))))\n    (vy\n     vy0\n     (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n       (let ((mag (/ dt (* (* distance distance) distance))))\n         (- vy (* (* y solarMass) mag)))))\n    (vz\n     vz0\n     (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n       (let ((mag (/ dt (* (* distance distance) distance))))\n         (- vz (* (* z solarMass) mag)))))\n    (i 0 (+ i 1)))\n   x))","arguments":["x0","y0","z0","vx0","vy0","vz0"],"operators":["let","while","<","sqrt","+","*","/","-"],":fpbench-domain":"science",":pre":"(and (< -6 x0 6)\n     (< -6 y0 6)\n     (< -1/5 z0 1/5)\n     (< -3 vx0 3)\n     (< -3 vy0 3)\n     (< -1/10 vz0 1/10))",":name":"N Body Simulation","core_fptaylor":false,"core":"(FPCore\n (x0 y0 z0 vx0 vy0 vz0)\n :name\n \"N Body Simulation\"\n :fpbench-domain\n science\n :pre\n (and (< -6 x0 6)\n      (< -6 y0 6)\n      (< -1/5 z0 1/5)\n      (< -3 vx0 3)\n      (< -3 vy0 3)\n      (< -1/10 vz0 1/10))\n (let ((dt 1/10) (solarMass 3947841760435743/100000000000000))\n   (while\n    (< i 100)\n    ((x\n      x0\n      (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n        (let ((mag (/ dt (* (* distance distance) distance))))\n          (let ((vxNew (- vx (* (* x solarMass) mag)))) (+ x (* dt vxNew))))))\n     (y\n      y0\n      (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n        (let ((mag (/ dt (* (* distance distance) distance))))\n          (let ((vyNew (- vy (* (* y solarMass) mag)))) (+ y (* dt vyNew))))))\n     (z\n      z0\n      (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n        (let ((mag (/ dt (* (* distance distance) distance))))\n          (let ((vzNew (- vz (* (* z solarMass) mag)))) (+ z (* dt vzNew))))))\n     (vx\n      vx0\n      (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n        (let ((mag (/ dt (* (* distance distance) distance))))\n          (- vx (* (* x solarMass) mag)))))\n     (vy\n      vy0\n      (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n        (let ((mag (/ dt (* (* distance distance) distance))))\n          (- vy (* (* y solarMass) mag)))))\n     (vz\n      vz0\n      (let ((distance (sqrt (+ (+ (* x x) (* y y)) (* z z)))))\n        (let ((mag (/ dt (* (* distance distance) distance))))\n          (- vz (* (* z solarMass) mag)))))\n     (i 0 (+ i 1)))\n    x)))"},{"body":"(let ((h 1/100) (L 2) (m 3/2) (g 196133/20000))\n  (while\n   (< n N)\n   ((t\n     t0\n     (let ((k1w (* (/ (- g) L) (sin t))))\n       (let ((k2t (+ w (* (/ h 2) k1w)))) (+ t (* h k2t)))))\n    (w\n     w0\n     (let ((k2w (* (/ (- g) L) (sin (+ t (* (/ h 2) w)))))) (+ w (* h k2w))))\n    (n 0 (+ n 1)))\n   t))","arguments":["t0","w0","N"],"operators":["let","while","<","*","/","-","sin","+"],":fpbench-domain":"science",":example":{"N":"1000.0"},":pre":"(and (< -2 t0 2) (< -5 w0 5))",":name":"Pendulum","core_fptaylor":false,"core":"(FPCore\n (t0 w0 N)\n :name\n \"Pendulum\"\n :fpbench-domain\n science\n :pre\n (and (< -2 t0 2) (< -5 w0 5))\n :example\n ((N 1000))\n (let ((h 1/100) (L 2) (m 3/2) (g 196133/20000))\n   (while\n    (< n N)\n    ((t\n      t0\n      (let ((k1w (* (/ (- g) L) (sin t))))\n        (let ((k2t (+ w (* (/ h 2) k1w)))) (+ t (* h k2t)))))\n     (w\n      w0\n      (let ((k2w (* (/ (- g) L) (sin (+ t (* (/ h 2) w)))))) (+ w (* h k2w))))\n     (n 0 (+ n 1)))\n    t)))"},{"body":"(while\n (< i 10)\n ((x\n   x0\n   (-\n    x\n    (/\n     (+ (+ (- x (/ (pow x 3) 6)) (/ (pow x 5) 120)) (/ (pow x 7) 5040))\n     (+ (+ (- 1 (/ (* x x) 2)) (/ (pow x 4) 24)) (/ (pow x 6) 720)))))\n  (i 0 (+ i 1)))\n x)","arguments":["x0"],"operators":["while","<","-","/","+","pow","*"],":fpbench-domain":"mathematics",":pre":"(< -1 x0 1)",":name":"Sine Newton","core_fptaylor":false,"core":"(FPCore\n (x0)\n :name\n \"Sine Newton\"\n :fpbench-domain\n mathematics\n :pre\n (< -1 x0 1)\n (while\n  (< i 10)\n  ((x\n    x0\n    (-\n     x\n     (/\n      (+ (+ (- x (/ (pow x 3) 6)) (/ (pow x 5) 120)) (/ (pow x 7) 5040))\n      (+ (+ (- 1 (/ (* x x) 2)) (/ (pow x 4) 24)) (/ (pow x 6) 720)))))\n   (i 0 (+ i 1)))\n  x))"},{"body":"(+\n (+\n  (+\n   (* 1335/4 (pow b 6))\n   (*\n    (pow a 2)\n    (- (- (- (* (* 11 (pow a 2)) (pow b 2)) (pow b 6)) (* 121 (pow b 4))) 2)))\n  (* 11/2 (pow b 8)))\n (/ a (* 2 b)))","arguments":["a","b"],"operators":["+","*","pow","-","/"],":example":{"a":"77617.0","b":"33096.0"},":name":"Rump's example, with pow","core_fptaylor":false,"core":"(FPCore\n (a b)\n :name\n \"Rump's example, with pow\"\n :example\n ((a 77617) (b 33096))\n (+\n  (+\n   (+\n    (* 1335/4 (pow b 6))\n    (*\n     (pow a 2)\n     (- (- (- (* (* 11 (pow a 2)) (pow b 2)) (pow b 6)) (* 121 (pow b 4))) 2)))\n   (* 11/2 (pow b 8)))\n  (/ a (* 2 b))))"},{"body":"(let ((b2 (* b b)))\n  (let ((b4 (* b2 b2)))\n    (let ((b6 (* b4 b2)) (b8 (* b4 b4)) (a2 (* a a)))\n      (let ((firstexpr (- (- (- (* (* 11 a2) b2) b6) (* 121 b4)) 2)))\n        (+\n         (+ (+ (* 1335/4 b6) (* a2 firstexpr)) (* 11/2 b8))\n         (/ a (* 2 b)))))))","arguments":["a","b"],"operators":["let","*","-","+","/"],":example":{"a":"77617.0","b":"33096.0"},":name":"Rump's example, from C program","core_fptaylor":false,"core":"(FPCore\n (a b)\n :name\n \"Rump's example, from C program\"\n :example\n ((a 77617) (b 33096))\n (let ((b2 (* b b)))\n   (let ((b4 (* b2 b2)))\n     (let ((b6 (* b4 b2)) (b8 (* b4 b4)) (a2 (* a a)))\n       (let ((firstexpr (- (- (- (* (* 11 a2) b2) b6) (* 121 b4)) 2)))\n         (+\n          (+ (+ (* 1335/4 b6) (* a2 firstexpr)) (* 11/2 b8))\n          (/ a (* 2 b))))))))"},{"body":"(let ((b2 (* b b)))\n  (let ((b4 (* b2 b2)))\n    (let ((b6 (* b4 b2)) (b8 (* b4 b4)) (a2 (* a a)))\n      (let ((firstexpr (- (- (* (* 11 a2) b2) (* 121 b4)) 2)))\n        (+\n         (+ (+ (* (- 1335/4 a2) b6) (* a2 firstexpr)) (* 11/2 b8))\n         (/ a (* 2 b)))))))","arguments":["a","b"],"operators":["let","*","-","+","/"],":cite":["rump-revisited-2002"],":example":{"a":"77617.0","b":"33096.0"},":name":"Rump's example revisited for floating point","core_fptaylor":false,"core":"(FPCore\n (a b)\n :name\n \"Rump's example revisited for floating point\"\n :example\n ((a 77617) (b 33096))\n :cite\n (rump-revisited-2002)\n (let ((b2 (* b b)))\n   (let ((b4 (* b2 b2)))\n     (let ((b6 (* b4 b2)) (b8 (* b4 b4)) (a2 (* a a)))\n       (let ((firstexpr (- (- (* (* 11 a2) b2) (* 121 b4)) 2)))\n         (+\n          (+ (+ (* (- 1335/4 a2) b6) (* a2 firstexpr)) (* 11/2 b8))\n          (/ a (* 2 b))))))))"},{"body":"(let ((inv_l 1/10) (c 617/50))\n  (while*\n   (< t 1000)\n   ((delta_dl 0 (* c sl))\n    (delta_dr 0 (* c sr))\n    (delta_d 0 (* (+ delta_dl delta_dr) 1/2))\n    (delta_theta 0 (* (- delta_dr delta_dl) inv_l))\n    (arg 0 (+ theta (* delta_theta 1/2)))\n    (cosi\n     0\n     (+\n      (- 1 (* (* arg arg) 1/2))\n      (* (* (* (* arg arg) arg) arg) 208333333/5000000000)))\n    (x 0 (+ x (* delta_d cosi)))\n    (sini\n     0\n     (+\n      (- arg (* (* (* arg arg) arg) 833333333/5000000000))\n      (* (* (* (* (* arg arg) arg) arg) arg) 8333333/1000000000)))\n    (y 0 (+ y (* delta_d sini)))\n    (theta -197/200 (+ theta delta_theta))\n    (t 0 (+ t 1))\n    (tmp sl* sl)\n    (sl sl* (if (== j 50) sr sl))\n    (sr sr* (if (== j 50) tmp sr))\n    (j 0 (if (== j 50) 0 (+ j 1))))\n   x))","arguments":["sr*","sl*"],"operators":["let","while*","<","*","+","-","if","=="],":cite":["damouche-martel-chapoutot-fmics15"],":fpbench-domain":"controls",":precision":"binary32",":example":{"sl*":"0.0525398163397","sr*":"0.0785398163397"},":pre":"(and (< 1/20 sl* (* 2 PI)) (< 1/20 sr* (* 2 PI)))",":name":"Odometry","core_fptaylor":false,"core":"(FPCore\n (sr* sl*)\n :name\n \"Odometry\"\n :description\n \"Compute the position of a robot from the speed of the wheels.\\nInputs: Speed `sl`, `sr` of the left and right wheel, in rad/s.\"\n :cite\n (damouche-martel-chapoutot-fmics15)\n :fpbench-domain\n controls\n :precision\n binary32\n :pre\n (and (< 1/20 sl* (* 2 PI)) (< 1/20 sr* (* 2 PI)))\n :example\n ((sr* 785398163397/10000000000000) (sl* 525398163397/10000000000000))\n (let ((inv_l 1/10) (c 617/50))\n   (while*\n    (< t 1000)\n    ((delta_dl 0 (* c sl))\n     (delta_dr 0 (* c sr))\n     (delta_d 0 (* (+ delta_dl delta_dr) 1/2))\n     (delta_theta 0 (* (- delta_dr delta_dl) inv_l))\n     (arg 0 (+ theta (* delta_theta 1/2)))\n     (cosi\n      0\n      (+\n       (- 1 (* (* arg arg) 1/2))\n       (* (* (* (* arg arg) arg) arg) 208333333/5000000000)))\n     (x 0 (+ x (* delta_d cosi)))\n     (sini\n      0\n      (+\n       (- arg (* (* (* arg arg) arg) 833333333/5000000000))\n       (* (* (* (* (* arg arg) arg) arg) arg) 8333333/1000000000)))\n     (y 0 (+ y (* delta_d sini)))\n     (theta -197/200 (+ theta delta_theta))\n     (t 0 (+ t 1))\n     (tmp sl* sl)\n     (sl sl* (if (== j 50) sr sl))\n     (sr sr* (if (== j 50) tmp sr))\n     (j 0 (if (== j 50) 0 (+ j 1))))\n    x)))",":description":"Compute the position of a robot from the speed of the wheels.\nInputs: Speed `sl`, `sr` of the left and right wheel, in rad/s."},{"body":"(let* ((dt 1/2) (invdt (/ 1 dt)))\n  (while*\n   (< t 100)\n   ((e 0 (- c m))\n    (p 0 (* kp e))\n    (i 0 (+ i (* (* ki dt) e)))\n    (d 0 (* (* kd invdt) (- e eold)))\n    (r 0 (+ (+ p i) d))\n    (m m (+ m (* 1/100 r)))\n    (eold 0 e)\n    (t 0 (+ t dt)))\n   m))","arguments":["m","kp","ki","kd","c"],"operators":["let*","/","while*","<","-","*","+"],":cite":["damouche-martel-chapoutot-nsv14","damouche-martel-chapoutot-fmics15"],":fpbench-domain":"controls",":precision":"binary64",":example":{"ki":"0.69006","kd":"2.8454","kp":"9.4514","m":"-5.0"},":pre":"(and (< -10 m 10) (< -10 c 10))",":name":"PID","core_fptaylor":false,"core":"(FPCore\n (m kp ki kd c)\n :name\n \"PID\"\n :description\n \"Keep a measure at its setpoint using a PID controller.\\nInputs: Measure `m`; gains `kp`, `ki`, `kd`; setpoint `c`\"\n :cite\n (damouche-martel-chapoutot-nsv14 damouche-martel-chapoutot-fmics15)\n :fpbench-domain\n controls\n :precision\n binary64\n :pre\n (and (< -10 m 10) (< -10 c 10))\n :example\n ((m -5) (kp 47257/5000) (ki 34503/50000) (kd 14227/5000))\n (let* ((dt 1/2) (invdt (/ 1 dt)))\n   (while*\n    (< t 100)\n    ((e 0 (- c m))\n     (p 0 (* kp e))\n     (i 0 (+ i (* (* ki dt) e)))\n     (d 0 (* (* kd invdt) (- e eold)))\n     (r 0 (+ (+ p i) d))\n     (m m (+ m (* 1/100 r)))\n     (eold 0 e)\n     (t 0 (+ t dt)))\n    m)))",":description":"Keep a measure at its setpoint using a PID controller.\nInputs: Measure `m`; gains `kp`, `ki`, `kd`; setpoint `c`"},{"body":"(let ((sixieme (/ 1 6)) (eps 1/200) (k 6/5))\n  (while\n   (> e eps)\n   ((y_n\n     y_n*\n     (let* ((k1 (let ((v (- c y_n))) (* (* k v) v)))\n            (k2 (let ((v (- c (+ y_n (* (* 1/2 h) k1))))) (* (* k v) v)))\n            (k3 (let ((v (- c (+ y_n (* (* 1/2 h) k2))))) (* (* k v) v)))\n            (k4 (let ((v (- c (+ y_n (* h k3))))) (* (* k v) v))))\n       (+ y_n (* (* sixieme h) (+ (+ (+ k1 (* 2 k2)) (* 2 k3)) k4)))))\n    (i 0 (+ i 1))\n    (e 1 (- e eps)))\n   (fabs e)))","arguments":["h","y_n*","c"],"operators":["let","/","while",">","let*","-","*","+","fabs"],":cite":["damouche-martel-chapoutot-fmics15"],":fpbench-domain":"mathematics",":precision":"binary32",":example":{"y_n*":"10.1","h":"0.1","c":"100.1"},":pre":"(and (< 0 y_n* 100) (< 1/100000 h 1/10) (< 50 c 200))",":name":"Runge-Kutta 4","core_fptaylor":false,"core":"(FPCore\n (h y_n* c)\n :name\n \"Runge-Kutta 4\"\n :description\n \"Solve the differential equation `y' = (c - y)^2\\nInputs: Step size `h`; initial condition `y_n*`; paramter `c`\"\n :cite\n (damouche-martel-chapoutot-fmics15)\n :fpbench-domain\n mathematics\n :precision\n binary32\n :pre\n (and (< 0 y_n* 100) (< 1/100000 h 1/10) (< 50 c 200))\n :example\n ((h 1/10) (y_n* 101/10) (c 1001/10))\n (let ((sixieme (/ 1 6)) (eps 1/200) (k 6/5))\n   (while\n    (> e eps)\n    ((y_n\n      y_n*\n      (let* ((k1 (let ((v (- c y_n))) (* (* k v) v)))\n             (k2 (let ((v (- c (+ y_n (* (* 1/2 h) k1))))) (* (* k v) v)))\n             (k3 (let ((v (- c (+ y_n (* (* 1/2 h) k2))))) (* (* k v) v)))\n             (k4 (let ((v (- c (+ y_n (* h k3))))) (* (* k v) v))))\n        (+ y_n (* (* sixieme h) (+ (+ (+ k1 (* 2 k2)) (* 2 k3)) k4)))))\n     (i 0 (+ i 1))\n     (e 1 (- e eps)))\n    (fabs e))))",":description":"Solve the differential equation `y' = (c - y)^2\nInputs: Step size `h`; initial condition `y_n*`; paramter `c`"},{"body":"(let ((eps 1/100)\n      (Dc -1280)\n      (Ac00 499/1000)\n      (Ac01 -1/20)\n      (Ac10 1/100)\n      (Ac11 1)\n      (Bc0 1)\n      (Bc1 0)\n      (Cc0 14112/25)\n      (Cc1 0))\n  (while*\n   (> e eps)\n   ((yc 0 (let ((v (- y yd))) (if (< v -1) -1 (if (< 1 v) 1 v))))\n    (u 0 (+ (* Cc0 xc0) (+ (* Cc1 xc1) (* Dc yc))))\n    (xc0 0 (+ (* Ac00 xc0) (+ (* Ac01 xc1) (* Bc0 yc))))\n    (xc1 0 (+ (* Ac10 xc0) (+ (* Ac11 xc1) (* Bc1 yc))))\n    (i 0 (+ i 1))\n    (e 1 (fabs (- yc xc1))))\n   xc1))","arguments":["y","yd"],"operators":["let","while*",">","-","if","<","+","*","fabs"],":cite":["feron-ieee10","damouche-martel-chapoutot-fmics15"],":fpbench-domain":"controls",":precision":"binary32",":example":{"yd":"5.0","y":"2.5"},":pre":"(and (< 0 yd 50) (< 0 y 50))",":name":"Lead-lag System","core_fptaylor":false,"core":"(FPCore\n (y yd)\n :name\n \"Lead-lag System\"\n :description\n \"Move a mass from an initial position to a desired position.\\nInputs: Initial position `y`; desired position `yd`\"\n :cite\n (feron-ieee10 damouche-martel-chapoutot-fmics15)\n :fpbench-domain\n controls\n :precision\n binary32\n :pre\n (and (< 0 yd 50) (< 0 y 50))\n :example\n ((y 5/2) (yd 5))\n (let ((eps 1/100)\n       (Dc -1280)\n       (Ac00 499/1000)\n       (Ac01 -1/20)\n       (Ac10 1/100)\n       (Ac11 1)\n       (Bc0 1)\n       (Bc1 0)\n       (Cc0 14112/25)\n       (Cc1 0))\n   (while*\n    (> e eps)\n    ((yc 0 (let ((v (- y yd))) (if (< v -1) -1 (if (< 1 v) 1 v))))\n     (u 0 (+ (* Cc0 xc0) (+ (* Cc1 xc1) (* Dc yc))))\n     (xc0 0 (+ (* Ac00 xc0) (+ (* Ac01 xc1) (* Bc0 yc))))\n     (xc1 0 (+ (* Ac10 xc0) (+ (* Ac11 xc1) (* Bc1 yc))))\n     (i 0 (+ i 1))\n     (e 1 (fabs (- yc xc1))))\n    xc1)))",":description":"Move a mass from an initial position to a desired position.\nInputs: Initial position `y`; desired position `yd`"},{"body":"(let* ((a 1/4) (b 5000) (n 25) (h (/ (- b a) n)))\n  (while*\n   (< xa 5000)\n   ((xb 0 (let ((v (+ xa h))) (if (> v 5000) 5000 v)))\n    (r\n     0\n     (let ((gxa\n            (/\n             u\n             (-\n              (+ (- (* (* (* 7/10 xa) xa) xa) (* (* 3/5 xa) xa)) (* 9/10 xa))\n              1/5)))\n           (gxb\n            (/\n             u\n             (-\n              (+ (- (* (* (* 7/10 xb) xb) xb) (* (* 3/5 xb) xb)) (* 9/10 xb))\n              1/5))))\n       (+ r (* (* (+ gxa gxb) 1/2) h))))\n    (xa 1/4 (+ xa h)))\n   r))","arguments":["u"],"operators":["let*","/","-","while*","<","let","+","if",">","*"],":cite":["damouche-martel-chapoutot-fmics15"],":fpbench-domain":"mathematics",":pre":"(<= 111/100 u 111/50)",":name":"Trapeze","core_fptaylor":false,"core":"(FPCore\n (u)\n :name\n \"Trapeze\"\n :cite\n (damouche-martel-chapoutot-fmics15)\n :fpbench-domain\n mathematics\n :pre\n (<= 111/100 u 111/50)\n (let* ((a 1/4) (b 5000) (n 25) (h (/ (- b a) n)))\n   (while*\n    (< xa 5000)\n    ((xb 0 (let ((v (+ xa h))) (if (> v 5000) 5000 v)))\n     (r\n      0\n      (let ((gxa\n             (/\n              u\n              (-\n               (+ (- (* (* (* 7/10 xa) xa) xa) (* (* 3/5 xa) xa)) (* 9/10 xa))\n               1/5)))\n            (gxb\n             (/\n              u\n              (-\n               (+ (- (* (* (* 7/10 xb) xb) xb) (* (* 3/5 xb) xb)) (* 9/10 xb))\n               1/5))))\n        (+ r (* (* (+ gxa gxb) 1/2) h))))\n     (xa 1/4 (+ xa h)))\n    r)))"},{"body":"(let* ((R 6400000)\n       (G 166857/2500000000000000)\n       (Mt 5973600000000000000000000)\n       (dt 1/10)\n       (T (* 24 3600))\n       (nombrepas (/ T dt))\n       (r0 (+ (* 400 10000) R))\n       (vr0 0)\n       (teta0 0)\n       (viss (sqrt (/ (* G Mt) r0)))\n       (vteta0 (/ viss r0))\n       (rf R)\n       (vrf 0)\n       (tetaf 0)\n       (vl (sqrt (/ (* G Mt) R)))\n       (vlrad (/ vl r0))\n       (vtetaf (* 11/10 vlrad)))\n  (while*\n   (< i 2000000)\n   ((t_i 0 (+ t_im1 dt))\n    (mf_i 0 (- mf_im1 (* A t_im1)))\n    (u1_i 0 (+ (* u2_im1 dt) u1_im1))\n    (u3_i 0 (+ (* u4_im1 dt) u3_im1))\n    (w1_i 0 (+ (* w2_im1 dt) w1_im1))\n    (w3_i 0 (+ (* w4_im1 dt) w3_im1))\n    (u2_i\n     0\n     (+\n      (* (* (- G) (/ Mt (* u1_im1 u1_im1))) dt)\n      (* (* u1_im1 u4_im1) (* u4_im1 dt))))\n    (u4_i 0 (+ (* (* -2 (* u2_im1 (/ u4_im1 u1_im1))) dt) u4_im1))\n    (w2_i\n     0\n     (+\n      (+\n       (* (* (- G) (/ Mt (* w1_im1 w1_im1))) dt)\n       (* (* w1_im1 w4_im1) (* w4_im1 dt)))\n      (+\n       (if (> mf_im1 0) (* (/ (* A w2_im1) (- Mf (* A t_im1))) dt) 0)\n       w2_im1)))\n    (w4_i\n     0\n     (+\n      (* (* -2 (* w2_im1 (/ w4_im1 w1_im1))) dt)\n      (+\n       (if (> mf_im1 0) (* A (* (/ w4_im1 (- Mf (* A t_im1))) dt)) 0)\n       w4_im1)))\n    (x 0 (* u1_i (cos u3_i)))\n    (y 0 (* u1_i (sin u3_i)))\n    (i 1 (+ i 1))\n    (u1_im1 r0 u1_i)\n    (u2_im1 vr0 u2_i)\n    (u3_im1 teta0 u3_i)\n    (u4_im1 vteta0 u4_i)\n    (w1_im1 rf w1_i)\n    (w2_im1 vrf w2_i)\n    (w3_im1 tetaf w3_i)\n    (w4_im1 vtetaf w4_i)\n    (t_im1 0 t_i)\n    (mf_im1 Mf mf_i))\n   x))","arguments":["Mf","A"],"operators":["let*","*","/","+","sqrt","while*","<","-","if",">","cos","sin"],":cite":["damouche-martel-chapoutot-cf15"],":fpbench-domain":"controls",":precision":"binary32",":example":{"A":"140.0","Mf":"150000.0"},":name":"Rocket Trajectory","core_fptaylor":false,"core":"(FPCore\n (Mf A)\n :name\n \"Rocket Trajectory\"\n :description\n \"Compute the trajectory of a rocket around the earth.\\nInputs: Mass `Mf`; acceleration `A`\"\n :cite\n (damouche-martel-chapoutot-cf15)\n :fpbench-domain\n controls\n :precision\n binary32\n :example\n ((Mf 150000) (A 140))\n (let* ((R 6400000)\n        (G 166857/2500000000000000)\n        (Mt 5973600000000000000000000)\n        (dt 1/10)\n        (T (* 24 3600))\n        (nombrepas (/ T dt))\n        (r0 (+ (* 400 10000) R))\n        (vr0 0)\n        (teta0 0)\n        (viss (sqrt (/ (* G Mt) r0)))\n        (vteta0 (/ viss r0))\n        (rf R)\n        (vrf 0)\n        (tetaf 0)\n        (vl (sqrt (/ (* G Mt) R)))\n        (vlrad (/ vl r0))\n        (vtetaf (* 11/10 vlrad)))\n   (while*\n    (< i 2000000)\n    ((t_i 0 (+ t_im1 dt))\n     (mf_i 0 (- mf_im1 (* A t_im1)))\n     (u1_i 0 (+ (* u2_im1 dt) u1_im1))\n     (u3_i 0 (+ (* u4_im1 dt) u3_im1))\n     (w1_i 0 (+ (* w2_im1 dt) w1_im1))\n     (w3_i 0 (+ (* w4_im1 dt) w3_im1))\n     (u2_i\n      0\n      (+\n       (* (* (- G) (/ Mt (* u1_im1 u1_im1))) dt)\n       (* (* u1_im1 u4_im1) (* u4_im1 dt))))\n     (u4_i 0 (+ (* (* -2 (* u2_im1 (/ u4_im1 u1_im1))) dt) u4_im1))\n     (w2_i\n      0\n      (+\n       (+\n        (* (* (- G) (/ Mt (* w1_im1 w1_im1))) dt)\n        (* (* w1_im1 w4_im1) (* w4_im1 dt)))\n       (+\n        (if (> mf_im1 0) (* (/ (* A w2_im1) (- Mf (* A t_im1))) dt) 0)\n        w2_im1)))\n     (w4_i\n      0\n      (+\n       (* (* -2 (* w2_im1 (/ w4_im1 w1_im1))) dt)\n       (+\n        (if (> mf_im1 0) (* A (* (/ w4_im1 (- Mf (* A t_im1))) dt)) 0)\n        w4_im1)))\n     (x 0 (* u1_i (cos u3_i)))\n     (y 0 (* u1_i (sin u3_i)))\n     (i 1 (+ i 1))\n     (u1_im1 r0 u1_i)\n     (u2_im1 vr0 u2_i)\n     (u3_im1 teta0 u3_i)\n     (u4_im1 vteta0 u4_i)\n     (w1_im1 rf w1_i)\n     (w2_im1 vrf w2_i)\n     (w3_im1 tetaf w3_i)\n     (w4_im1 vtetaf w4_i)\n     (t_im1 0 t_i)\n     (mf_im1 Mf mf_i))\n    x)))",":description":"Compute the trajectory of a rocket around the earth.\nInputs: Mass `Mf`; acceleration `A`"},{"body":"(let ((eps 1/100000000000000000))\n  (while*\n   (> e eps)\n   ((x_n1\n     0\n     (+\n      (- (- (/ b1 a11) (* (/ 1/10 a11) x2)) (* (/ 1/5 a11) x3))\n      (* (/ 3/10 a11) x4)))\n    (x_n2\n     0\n     (-\n      (+ (- (/ b2 a22) (* (/ 3/10 a22) x1)) (* (/ 1/10 a22) x3))\n      (* (/ 1/5 a22) x4)))\n    (x_n3\n     0\n     (-\n      (+ (- (/ b3 a33) (* (/ 1/5 a33) x1)) (* (/ 3/10 a33) x2))\n      (* (/ 1/10 a33) x4)))\n    (x_n4\n     0\n     (-\n      (- (+ (/ b4 a44) (* (/ 1/10 a44) x1)) (* (/ 1/5 a44) x2))\n      (* (/ 3/10 a44) x3)))\n    (i 0 (+ i 1))\n    (e 1 (fabs (- x_n4 x4)))\n    (x1 0 x_n1)\n    (x2 0 x_n2)\n    (x3 0 x_n3)\n    (x4 0 x_n4))\n   x2))","arguments":["a11","a22","a33","a44","b1","b2","b3","b4"],"operators":["let","while*",">","+","-","/","*","fabs"],":cite":["atkinson-1989"],":fpbench-domain":"mathematics",":precision":"binary32",":example":{"a11":"0.61","b4":"(/ 1 5)","b3":"0.25","b1":"0.5","a22":"0.62","a33":"0.6006","a44":"0.601","b2":"(/ 1 3)"},":name":"Jacobi's Method","core_fptaylor":false,"core":"(FPCore\n (a11 a22 a33 a44 b1 b2 b3 b4)\n :name\n \"Jacobi's Method\"\n :description\n \"Solve a linear system `Ax = b`.\\nInputs: Array entries `aij`; vector entries `bi`\"\n :cite\n (atkinson-1989)\n :fpbench-domain\n mathematics\n :precision\n binary32\n :example\n ((a11 61/100)\n  (a22 31/50)\n  (a33 3003/5000)\n  (a44 601/1000)\n  (b1 1/2)\n  (b2 (/ 1 3))\n  (b3 1/4)\n  (b4 (/ 1 5)))\n (let ((eps 1/100000000000000000))\n   (while*\n    (> e eps)\n    ((x_n1\n      0\n      (+\n       (- (- (/ b1 a11) (* (/ 1/10 a11) x2)) (* (/ 1/5 a11) x3))\n       (* (/ 3/10 a11) x4)))\n     (x_n2\n      0\n      (-\n       (+ (- (/ b2 a22) (* (/ 3/10 a22) x1)) (* (/ 1/10 a22) x3))\n       (* (/ 1/5 a22) x4)))\n     (x_n3\n      0\n      (-\n       (+ (- (/ b3 a33) (* (/ 1/5 a33) x1)) (* (/ 3/10 a33) x2))\n       (* (/ 1/10 a33) x4)))\n     (x_n4\n      0\n      (-\n       (- (+ (/ b4 a44) (* (/ 1/10 a44) x1)) (* (/ 1/5 a44) x2))\n       (* (/ 3/10 a44) x3)))\n     (i 0 (+ i 1))\n     (e 1 (fabs (- x_n4 x4)))\n     (x1 0 x_n1)\n     (x2 0 x_n2)\n     (x3 0 x_n3)\n     (x4 0 x_n4))\n    x2)))",":description":"Solve a linear system `Ax = b`.\nInputs: Array entries `aij`; vector entries `bi`"},{"body":"(let ((eps 1/2000))\n  (while*\n   (and (> e eps) (< i 100000))\n   ((x_n\n     0\n     (let ((f\n            (-\n             (+\n              (-\n               (+\n                (- (* (* x x) (* (* x x) x)) (* (* 10 x) (* (* x x) x)))\n                (* (* 40 x) (* x x)))\n               (* (* 80 x) x))\n              (* 80 x))\n             32))\n           (ff\n            (+\n             (-\n              (+\n               (- (* (* 5 x) (* (* x x) x)) (* (* 40 x) (* x x)))\n               (* (* 120 x) x))\n              (* 160 x))\n             80)))\n       (- x (/ f ff))))\n    (e 1 (fabs (- x x_n)))\n    (x 0 x_n)\n    (i 0 (+ i 1)))\n   x))","arguments":["x0"],"operators":["let","while*","and",">","<","-","+","*","/","fabs"],":cite":["atkinson-1989"],":fpbench-domain":"mathematics",":precision":"binary32",":example":{"x0":"0.0"},":pre":"(< 0 x0 3)",":name":"Newton-Raphson's Method","core_fptaylor":false,"core":"(FPCore\n (x0)\n :name\n \"Newton-Raphson's Method\"\n :description\n \"Find the zeros of a function `f = (x - 2)**5`.\\nInputs: Initial guess `x0`\"\n :cite\n (atkinson-1989)\n :fpbench-domain\n mathematics\n :precision\n binary32\n :pre\n (< 0 x0 3)\n :example\n ((x0 0))\n (let ((eps 1/2000))\n   (while*\n    (and (> e eps) (< i 100000))\n    ((x_n\n      0\n      (let ((f\n             (-\n              (+\n               (-\n                (+\n                 (- (* (* x x) (* (* x x) x)) (* (* 10 x) (* (* x x) x)))\n                 (* (* 40 x) (* x x)))\n                (* (* 80 x) x))\n               (* 80 x))\n              32))\n            (ff\n             (+\n              (-\n               (+\n                (- (* (* 5 x) (* (* x x) x)) (* (* 40 x) (* x x)))\n                (* (* 120 x) x))\n               (* 160 x))\n              80)))\n        (- x (/ f ff))))\n     (e 1 (fabs (- x x_n)))\n     (x 0 x_n)\n     (i 0 (+ i 1)))\n    x)))",":description":"Find the zeros of a function `f = (x - 2)**5`.\nInputs: Initial guess `x0`"},{"body":"(let ((eps 1/2000))\n  (while*\n   (> e eps)\n   ((vx 0 (+ (+ (* a11 v1) (* a12 v2)) (+ (* a13 v3) (* a14 v4))))\n    (vy 0 (+ (+ (* a21 v1) (* a22 v2)) (+ (* a23 v3) (* a24 v4))))\n    (vz 0 (+ (+ (* a31 v1) (* a32 v2)) (+ (* a33 v3) (* a34 v4))))\n    (vw 0 (+ (+ (* a41 v1) (* a42 v2)) (+ (* a43 v3) (* a44 v4))))\n    (i 0 (+ i 1))\n    (v1 v1 (/ vx vw))\n    (v2 v2 (/ vy vw))\n    (v3 v3 (/ vz vw))\n    (v4 v4 1)\n    (e 1 (fabs (- 1 v1))))\n   v1))","arguments":["a11","a12","a13","a14","a21","a22","a23","a24","a31","a32","a33","a34","a41","a42","a43","a44","v1","v2","v3","v4"],"operators":["let","while*",">","+","*","/","fabs","-"],":cite":["golub-vanloan-1996"],":fpbench-domain":"mathematics",":precision":"binary32",":example":{"a31":"0.01","v2":"0.0","a11":"150.0","a14":"0.01","a13":"0.01","a23":"0.01","v4":"1.0","a12":"0.01","v3":"0.0","a24":"0.01","a32":"0.01","a41":"0.01","a42":"0.01","a21":"0.01","a22":"150.0","v1":"0.0","a34":"0.01","a33":"150.0","a43":"0.01","a44":"150.0"},":pre":"(<\n 150\n (-\n  (+\n   (+\n    (+\n     (+\n      (+\n       (+\n        (+\n         (+\n          (+\n           (+\n            (+ (* (* (* a11 a22) a33) a44) (* (* (* a12 a23) a34) a41))\n            (* (* (* a13 a24) a31) a42))\n           (* (* (* a14 a21) a32) a43))\n          (* (* (* a11 a23) a34) a42))\n         (* (* (* a12 a21) a33) a44))\n        (* (* (* a13 a21) a32) a44))\n       (* (* (* a14 a22) a33) a41))\n      (* (* (* a11 a24) a32) a43))\n     (* (* (* a12 a24) a31) a43))\n    (* (* (* a13 a22) a34) a41))\n   (* (* (* a14 a23) a31) a42))\n  (+\n   (+\n    (+\n     (+\n      (+\n       (+\n        (+\n         (+\n          (+\n           (+\n            (+ (* (* (* a11 a22) a34) a43) (* (* (* a12 a23) a31) a44))\n            (* (* (* a13 a24) a32) a41))\n           (* (* (* a14 a21) a33) a42))\n          (* (* (* a11 a23) a32) a44))\n         (* (* (* a12 a21) a34) a43))\n        (* (* (* a13 a21) a34) a42))\n       (* (* (* a14 a22) a31) a43))\n      (* (* (* a11 a24) a33) a42))\n     (* (* (* a12 a24) a33) a41))\n    (* (* (* a13 a22) a31) a44))\n   (* (* (* a14 a23) a32) a41)))\n 200)",":name":"Eigenvalue Computation","core_fptaylor":false,"core":"(FPCore\n (a11 a12 a13 a14 a21 a22 a23 a24 a31 a32 a33 a34 a41 a42 a43 a44 v1 v2 v3 v4)\n :name\n \"Eigenvalue Computation\"\n :description\n \"Compute the largest eigenvalue of a matrix and return its vector.\\nInputs: Matrix `aij`; initial guess `vi` with one nonzero element\"\n :cite\n (golub-vanloan-1996)\n :fpbench-domain\n mathematics\n :precision\n binary32\n :pre\n (<\n  150\n  (-\n   (+\n    (+\n     (+\n      (+\n       (+\n        (+\n         (+\n          (+\n           (+\n            (+\n             (+ (* (* (* a11 a22) a33) a44) (* (* (* a12 a23) a34) a41))\n             (* (* (* a13 a24) a31) a42))\n            (* (* (* a14 a21) a32) a43))\n           (* (* (* a11 a23) a34) a42))\n          (* (* (* a12 a21) a33) a44))\n         (* (* (* a13 a21) a32) a44))\n        (* (* (* a14 a22) a33) a41))\n       (* (* (* a11 a24) a32) a43))\n      (* (* (* a12 a24) a31) a43))\n     (* (* (* a13 a22) a34) a41))\n    (* (* (* a14 a23) a31) a42))\n   (+\n    (+\n     (+\n      (+\n       (+\n        (+\n         (+\n          (+\n           (+\n            (+\n             (+ (* (* (* a11 a22) a34) a43) (* (* (* a12 a23) a31) a44))\n             (* (* (* a13 a24) a32) a41))\n            (* (* (* a14 a21) a33) a42))\n           (* (* (* a11 a23) a32) a44))\n          (* (* (* a12 a21) a34) a43))\n         (* (* (* a13 a21) a34) a42))\n        (* (* (* a14 a22) a31) a43))\n       (* (* (* a11 a24) a33) a42))\n      (* (* (* a12 a24) a33) a41))\n     (* (* (* a13 a22) a31) a44))\n    (* (* (* a14 a23) a32) a41)))\n  200)\n :example\n ((a11 150)\n  (a12 1/100)\n  (a13 1/100)\n  (a14 1/100)\n  (a21 1/100)\n  (a22 150)\n  (a23 1/100)\n  (a24 1/100)\n  (a31 1/100)\n  (a32 1/100)\n  (a33 150)\n  (a34 1/100)\n  (a41 1/100)\n  (a42 1/100)\n  (a43 1/100)\n  (a44 150)\n  (v1 0)\n  (v2 0)\n  (v3 0)\n  (v4 1))\n (let ((eps 1/2000))\n   (while*\n    (> e eps)\n    ((vx 0 (+ (+ (* a11 v1) (* a12 v2)) (+ (* a13 v3) (* a14 v4))))\n     (vy 0 (+ (+ (* a21 v1) (* a22 v2)) (+ (* a23 v3) (* a24 v4))))\n     (vz 0 (+ (+ (* a31 v1) (* a32 v2)) (+ (* a33 v3) (* a34 v4))))\n     (vw 0 (+ (+ (* a41 v1) (* a42 v2)) (+ (* a43 v3) (* a44 v4))))\n     (i 0 (+ i 1))\n     (v1 v1 (/ vx vw))\n     (v2 v2 (/ vy vw))\n     (v3 v3 (/ vz vw))\n     (v4 v4 1)\n     (e 1 (fabs (- 1 v1))))\n    v1)))",":description":"Compute the largest eigenvalue of a matrix and return its vector.\nInputs: Matrix `aij`; initial guess `vi` with one nonzero element"},{"body":"(let ((eps 1/200000))\n  (while*\n   (> e eps)\n   ((h1 0 (+ (+ (* Q11 qj1) (* Q21 qj2)) (* Q31 qj3)))\n    (h2 0 (+ (+ (* Q12 qj1) (* Q22 qj2)) (* Q32 qj3)))\n    (h3 0 (+ (+ (* Q13 qj1) (* Q23 qj2)) (* Q33 qj3)))\n    (qj1 Q31 (- qj1 (+ (+ (* Q11 h1) (* Q12 h2)) (* Q13 h3))))\n    (qj2 Q32 (- qj2 (+ (+ (* Q21 h1) (* Q22 h2)) (* Q23 h3))))\n    (qj3 Q33 (- qj3 (+ (+ (* Q31 h1) (* Q32 h2)) (* Q33 h3))))\n    (r1 0 (+ r1 h1))\n    (r2 0 (+ r2 h2))\n    (r3 0 (+ r3 h3))\n    (r\n     (+ (+ (* qj1 qj1) (* qj2 qj2)) (* qj3 qj3))\n     (+ (+ (* qj1 qj1) (* qj2 qj2)) (* qj3 qj3)))\n    (rjj 0 (sqrt r))\n    (e 10 (fabs (- 1 (/ rjj rold))))\n    (i 1 (+ i 1))\n    (rold (sqrt r) rjj))\n   qj1))","arguments":["Q11","Q12","Q13","Q21","Q22","Q23","Q31","Q32","Q33"],"operators":["let","while*",">","+","*","sqrt","-","fabs","/"],":cite":["abdelmalek-bit71","golub-vanloan-1996","hernandez-roman-tomas-vidal-tr07"],":fpbench-domain":"mathematics",":precision":"binary32",":example":{"Q13":"0.0","Q33":"(/ 1 2583)","Q11":"(/ 1 63)","Q23":"0.0","Q12":"0.0","Q22":"(/ 1 225)","Q21":"0.0","Q31":"(/ 1 2592)","Q32":"(/ 1 2601)"},":pre":"(and (< 1 Q11 (/ 1 7)) (< 1 Q22 (/ 1 25)))",":name":"Iterative Gram-Schmidt Method","core_fptaylor":false,"core":"(FPCore\n (Q11 Q12 Q13 Q21 Q22 Q23 Q31 Q32 Q33)\n :name\n \"Iterative Gram-Schmidt Method\"\n :description\n \"Orthogonalize a set of non-zero vectors in a Euclidian or Hermitian space.\\nInputs: Vectors `Qij`\"\n :cite\n (abdelmalek-bit71 golub-vanloan-1996 hernandez-roman-tomas-vidal-tr07)\n :fpbench-domain\n mathematics\n :precision\n binary32\n :pre\n (and (< 1 Q11 (/ 1 7)) (< 1 Q22 (/ 1 25)))\n :example\n ((Q11 (/ 1 63))\n  (Q12 0)\n  (Q13 0)\n  (Q21 0)\n  (Q22 (/ 1 225))\n  (Q23 0)\n  (Q31 (/ 1 2592))\n  (Q32 (/ 1 2601))\n  (Q33 (/ 1 2583)))\n (let ((eps 1/200000))\n   (while*\n    (> e eps)\n    ((h1 0 (+ (+ (* Q11 qj1) (* Q21 qj2)) (* Q31 qj3)))\n     (h2 0 (+ (+ (* Q12 qj1) (* Q22 qj2)) (* Q32 qj3)))\n     (h3 0 (+ (+ (* Q13 qj1) (* Q23 qj2)) (* Q33 qj3)))\n     (qj1 Q31 (- qj1 (+ (+ (* Q11 h1) (* Q12 h2)) (* Q13 h3))))\n     (qj2 Q32 (- qj2 (+ (+ (* Q21 h1) (* Q22 h2)) (* Q23 h3))))\n     (qj3 Q33 (- qj3 (+ (+ (* Q31 h1) (* Q32 h2)) (* Q33 h3))))\n     (r1 0 (+ r1 h1))\n     (r2 0 (+ r2 h2))\n     (r3 0 (+ r3 h3))\n     (r\n      (+ (+ (* qj1 qj1) (* qj2 qj2)) (* qj3 qj3))\n      (+ (+ (* qj1 qj1) (* qj2 qj2)) (* qj3 qj3)))\n     (rjj 0 (sqrt r))\n     (e 10 (fabs (- 1 (/ rjj rold))))\n     (i 1 (+ i 1))\n     (rold (sqrt r) rjj))\n    qj1)))",":description":"Orthogonalize a set of non-zero vectors in a Euclidian or Hermitian space.\nInputs: Vectors `Qij`"}]);