Herbie run

Date:Thursday, October 24th, 2024
Commit:8924ce3e on Original-Inv
Hostname:nightly with Racket 8.10
Seed:2024298
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:avg-errorreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default

Time bar (total: 30.3min)

sample5.8min (19.1%)

Memory
1 316.0MiB live, 355 431.5MiB allocated
Samples
3.4min2 146 940×0valid
23.6s67 689×1valid
10.4s63 830×0invalid
1.6s5 655×2valid
1.3s1 202×5exit
387.0ms1 757×1invalid
309.0ms579×3valid
291.0ms379×4exit
4.0ms32×1exit
0.0ms1×4valid
Precisions
Click to see histograms. Total time spent on operations: 2.5min
ival-mult: 48.7s (32.7% of total)
ival-sub: 21.5s (14.4% of total)
ival-add: 20.7s (13.9% of total)
ival-div: 17.5s (11.8% of total)
ival-log: 10.4s (7% of total)
ival-sqrt: 5.7s (3.8% of total)
const: 5.6s (3.8% of total)
ival-sin: 4.4s (2.9% of total)
ival-cos: 3.3s (2.2% of total)
adjust: 3.3s (2.2% of total)
ival-exp: 2.5s (1.7% of total)
ival-true: 1.8s (1.2% of total)
exact: 1.1s (0.7% of total)
ival-assert: 952.0ms (0.6% of total)
ival-fabs: 459.0ms (0.3% of total)
ival-cosh: 252.0ms (0.2% of total)
ival-acos: 226.0ms (0.2% of total)
ival-tan: 206.0ms (0.1% of total)
ival-hypot: 159.0ms (0.1% of total)
ival-sinh: 125.0ms (0.1% of total)
ival-tanh: 85.0ms (0.1% of total)
Bogosity

simplify5.7min (18.6%)

Memory
1 044.2MiB live, 282 607.0MiB allocated
Algorithm
2 227×egg-herbie
Stop Event
3 140×iter limit
1 493×node limit
653×saturated
101×unsound
Counts
75 846 → 74 650

soundness4.5min (14.8%)

Memory
1 361.3MiB live, 163 697.6MiB allocated
Stop Event
1 646×iter limit
1 024×node limit
160×fuel
109×done
39×unsound
16×saturated
Compiler

Compiled 269 286 to 104 152 computations (61.3% saved)

rewrite4.0min (13.2%)

Memory
-2 329.1MiB live, 222 451.7MiB allocated
Stop Event
2 043×iter limit
950×node limit
24×unsound
17×saturated
Counts
11 995 → 577 791

eval2.2min (7.4%)

Memory
1 745.0MiB live, 150 589.3MiB allocated
Compiler

Compiled 19 988 593 to 2 064 516 computations (89.7% saved)

localize1.9min (6.1%)

Memory
-1 342.0MiB live, 124 182.4MiB allocated
Samples
1.0min226 243×0valid
12.3s11 029×1valid
5.1s3 111×2valid
3.0s7 402×0invalid
1.7s796×5exit
459.0ms986×0exit
443.0ms492×2exit
345.0ms259×3valid
238.0ms121×4exit
179.0ms124×1exit
54.0ms56×1invalid
5.0ms5×4valid
Compiler

Compiled 319 117 to 50 159 computations (84.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 57.7s
ival-mult: 18.8s (32.6% of total)
ival-div: 9.6s (16.6% of total)
ival-add: 8.0s (13.8% of total)
ival-sub: 5.0s (8.6% of total)
const: 2.8s (4.8% of total)
adjust: 2.4s (4.1% of total)
ival-log: 2.1s (3.6% of total)
ival-sin: 2.0s (3.4% of total)
ival-pow: 1.7s (2.9% of total)
ival-cos: 1.1s (1.8% of total)
ival-neg: 1.1s (1.8% of total)
ival-sqrt: 1.0s (1.8% of total)
ival-exp: 635.0ms (1.1% of total)
ival-pow2: 306.0ms (0.5% of total)
exact: 257.0ms (0.4% of total)
ival-true: 220.0ms (0.4% of total)
ival-asinh: 219.0ms (0.4% of total)
ival-tan: 140.0ms (0.2% of total)
ival-cosh: 119.0ms (0.2% of total)
ival-assert: 111.0ms (0.2% of total)
ival-log1p: 64.0ms (0.1% of total)
ival-fabs: 57.0ms (0.1% of total)
ival-hypot: 54.0ms (0.1% of total)
ival-sinh: 49.0ms (0.1% of total)
ival-pi: 42.0ms (0.1% of total)
ival-expm1: 22.0ms (0% of total)
ival-tanh: 16.0ms (0% of total)
ival-asin: 15.0ms (0% of total)
ival-cosu: 12.0ms (0% of total)
ival-acos: 11.0ms (0% of total)

preprocess1.5min (5%)

Memory
635.9MiB live, 81 977.4MiB allocated
Algorithm
269×egg-herbie
Stop Event
538×iter limit
305×node limit
233×saturated
Compiler

Compiled 389 492 to 70 156 computations (82% saved)

regimes1.5min (4.8%)

Memory
-16.8MiB live, 105 883.9MiB allocated
Counts
39 789 → 5 141
Calls

509 calls:

11.9s
x
11.2s
y
9.6s
z
5.6s
t
3.7s
a
Compiler

Compiled 39 334 to 59 312 computations (-50.8% saved)

series53.1s (2.9%)

Memory
-329.7MiB live, 61 259.7MiB allocated
Counts
11 995 → 75 846
Calls

9222 calls:

TimeVariablePointExpression
282.0ms
z
@-inf
((+ (* (/ z (+ (* -2 (* z z)) (* t y))) (+ y y)) x) (/ z (+ (* -2 (* z z)) (* t y))) (/ -1/2 z) (+ y y) (- x (/ (* (* y 2) z) (- (* (* z 2) z) (* y t)))) (+ (* (/ z t) 2) x) (* z (/ 2 t)) (/ 2 t) (fabs (/ y z)) (- x (/ (* (* y 2) z) (- (* (* z 2) z) (* y t)))) (/ (* (* y 2) z) (- (* (* z 2) z) (* y t))) (/ y z) (exp (log (/ y z))) (- x (/ (* (* y 2) z) (- (* (* z 2) z) (* y t)))) (/ (* (* y 2) z) (- (* (* z 2) z) (* y t))) (log (/ y z)) (exp (* (log (* -2 z)) -1)) (+ (* (/ z (+ (* -2 (* z z)) (* t y))) (* 2 y)) x) (/ z (+ (* -2 (* z z)) (* t y))) (log (* -2 z)))
250.0ms
x
@inf
((* (+ (* (/ (log (/ x y)) z) x) -1) z) (- (* x (- (log x) (log y))) z) (+ (* (/ (log (/ x y)) z) x) -1) (/ (log (/ x y)) z) (/ (* z z) z) (- (* x (log (/ x y))) z) (* z z) (neg (+ (* (log (/ y x)) x) z)) (+ (* (log (/ y x)) x) z) (* (log (/ y x)) x) (log (/ y x)) (/ 1 (pow (+ (* (log (/ x y)) x) (neg z)) -1)) (pow (+ (* (log (/ x y)) x) (neg z)) -1) (/ (/ 1 x) (log (/ x y))) (/ 1 x) (- (* x (- (log (neg x)) (log (neg y)))) z) (* x (- (log (neg x)) (log (neg y)))) (- (log (neg x)) (log (neg y))) (log (neg x)) (log (/ x y)) (/ x y) (log (neg y)) (neg x) (neg y))
215.0ms
x
@inf
((+ (* (+ (* z (+ 7936500793651/10000000000000000 y)) -13888888888889/5000000000000000) (/ z x)) (/ 83333333333333/1000000000000000 x)) (+ (+ (- (* (- x 1/2) (log x)) x) 91893853320467/100000000000000) (+ (* (+ (* z (+ 7936500793651/10000000000000000 y)) -13888888888889/5000000000000000) (/ z x)) (/ 83333333333333/1000000000000000 x))) (+ (- (* (- x 1/2) (log x)) x) 91893853320467/100000000000000) (* (- (log x) 1) x) (+ (+ (- (* (- x 1/2) (log x)) x) 91893853320467/100000000000000) (/ (+ (* (- (* (+ y 7936500793651/10000000000000000) z) 13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- (+ (* (- x 1/2) (log x)) (/ (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- x 91893853320467/100000000000000)) (* (/ (* z z) x) 7936500793651/10000000000000000) (/ (* z z) x) (+ (+ (- (* (- x 1/2) (log x)) x) 91893853320467/100000000000000) (/ (+ (* (- (* (+ y 7936500793651/10000000000000000) z) 13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (* (+ (* z (/ z x)) (/ (- (+ (* (- x 1/2) (log x)) (/ (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- x 91893853320467/100000000000000)) y)) y) (+ (* z (/ z x)) (/ (- (+ (* (- x 1/2) (log x)) (/ (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- x 91893853320467/100000000000000)) y)) (/ z x) (/ (+ (* (+ (* (log x) -1/2) 91893853320467/100000000000000) x) (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000)) x) (+ (+ (- (* (- x 1/2) (log x)) x) 91893853320467/100000000000000) (/ (+ (* (- (* (+ y 7936500793651/10000000000000000) z) 13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- (+ (* (- x 1/2) (log x)) (/ (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- x 91893853320467/100000000000000)) (+ (* (+ (* (log x) -1/2) 91893853320467/100000000000000) x) (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000)) (+ (* (+ (* (/ (+ 7936500793651/10000000000000000 y) x) z) (/ -13888888888889/5000000000000000 x)) z) (/ 83333333333333/1000000000000000 x)) (+ (* (/ (+ 7936500793651/10000000000000000 y) x) z) (/ -13888888888889/5000000000000000 x)) (+ (+ (- (* (- x 1/2) (log x)) x) 91893853320467/100000000000000) (+ (* (+ (* z (+ 7936500793651/10000000000000000 y)) -13888888888889/5000000000000000) (/ z x)) (/ 83333333333333/1000000000000000 x))) (- (+ (+ (* (+ (* (/ (+ 7936500793651/10000000000000000 y) x) z) (/ -13888888888889/5000000000000000 x)) z) (/ 83333333333333/1000000000000000 x)) (+ (* (log x) (+ -1/2 x)) 91893853320467/100000000000000)) x) (/ 83333333333333/1000000000000000 x) (/ (- (+ (* (- x 1/2) (log x)) (/ (+ (* (+ (* 7936500793651/10000000000000000 z) -13888888888889/5000000000000000) z) 83333333333333/1000000000000000) x)) (- x 91893853320467/100000000000000)) y) (/ (/ (* z z) x) y) (+ (* (log x) -1/2) 91893853320467/100000000000000) (+ (* (log x) (+ -1/2 x)) 91893853320467/100000000000000))
208.0ms
t
@inf
((+ (* (/ (- y z) (- a z)) (- t x)) x) (/ (- y z) (- a z)) (/ (- y z) a) (- y z) (+ x (* (- y z) (/ (- t x) (- a z)))) (* (- y z) (/ t (- a z))) (* t (/ y a)) (/ y a) (+ x (* (- y z) (/ (- t x) (- a z)))) (* (- y z) (/ t (- a z))) (* t (/ (- y z) a)) (+ x (* (- y z) (/ (- t x) (- a z)))) (- t (* (/ (- t x) z) (- y a))) (+ (* a (/ (- t x) z)) t) (/ (- t x) z) (- t (* (/ (- t x) z) (- y a))) (+ x (* (- y z) (/ (- t x) (- a z)))) (* (/ (- t x) z) (- y a)) (/ (- t x) z) (- t x) (- t x))
205.0ms
x
@inf
((neg (+ (* (log (/ y x)) x) z)) (+ (* (log (/ y x)) x) z) (log (/ y x)) (/ y x) (- (* x (log (/ x y))) z) (- (* x (log (/ x y))) z) (* (log (/ x y)) x) (log (/ x y)) (/ x y) (/ 1 (/ 1 (+ (* (log (/ x y)) x) z))) (/ 1 (+ (* (log (/ x y)) x) z)) (+ (* (log (/ x y)) x) z) (* (+ (* (- (log x) (log y)) (/ x z)) -1) z) (- (* x (- (log x) (log y))) z) (+ (* (- (log x) (log y)) (/ x z)) -1) (- (log x) (log y)))

prune46.6s (2.6%)

Memory
-1 793.5MiB live, 64 645.9MiB allocated
Counts
586 928 → 13 879
Compiler

Compiled 835 855 to 460 133 computations (45% saved)

explain42.8s (2.4%)

Memory
-681.7MiB live, 50 036.2MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15913
/.f64#fo/n11610
sqrt.f64#foflow-rescue7730
-.f64#fcancellation5813
/.f64#fo/o5570
*.f64#fn*o5280
+.f64#fnan-rescue4630
-.f64#fnan-rescue4420
cos.f64#fsensitivity3520
+.f64#fcancellation3240
/.f64#fu/n2880
/.f64#fn/o2860
sin.f64#fsensitivity2090
*.f64#fn*u1940
cos.f64#foflow-rescue1580
/.f64#fn/u1440
/.f64#fu/u940
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity850
log.f64#foflow-rescue840
log.f64#fuflow-rescue740
sqrt.f64#fuflow-rescue450
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue410
↳(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow41
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue410
↳(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow41
exp.f64#fsensitivity324
*.f64#fo*u250
*.f64#fu*o40
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))cancellation10
Confusion
Predicted +Predicted -
+5972207
-169960986
Precision
0.7785164906791814
Recall
0.9664994335653019
Confusion?
Predicted +Predicted MaybePredicted -
+59721206
-1699860978
Precision?
0.777734375
Recall?
0.9666612720504936
Freqs
test
numberfreq
061193
16886
2702
350
429
53
61
Total Confusion?
Predicted +Predicted MaybePredicted -
+13300
-30133
Precision?
0.9779411764705882
Recall?
1.0
Samples
12.8s130 580×0valid
2.2s5 826×1valid
660.0ms1 218×2valid
35.0ms100×3valid
1.0ms4×5exit
Compiler

Compiled 34 663 to 10 844 computations (68.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 9.1s
ival-mult: 2.7s (29.6% of total)
ival-add: 1.5s (16.6% of total)
ival-sub: 1.2s (12.8% of total)
ival-div: 1.1s (12.2% of total)
ival-log: 914.0ms (10.1% of total)
const: 318.0ms (3.5% of total)
ival-sqrt: 304.0ms (3.3% of total)
adjust: 258.0ms (2.8% of total)
ival-sin: 214.0ms (2.4% of total)
ival-cos: 212.0ms (2.3% of total)
ival-true: 126.0ms (1.4% of total)
ival-exp: 83.0ms (0.9% of total)
exact: 65.0ms (0.7% of total)
ival-assert: 61.0ms (0.7% of total)
ival-tan: 13.0ms (0.1% of total)
ival-cosh: 11.0ms (0.1% of total)
ival-fabs: 11.0ms (0.1% of total)
ival-hypot: 9.0ms (0.1% of total)
ival-tanh: 8.0ms (0.1% of total)
ival-sinh: 8.0ms (0.1% of total)
ival-acos: 5.0ms (0.1% of total)

bsearch37.3s (2%)

Memory
462.8MiB live, 39 128.3MiB allocated
Algorithm
1 804×binary-search
1 148×left-value
Stop Event
1 766×narrow-enough
37×predicate-same
1×predicate-failed
Samples
21.2s134 077×0valid
889.0ms3 188×1valid
363.0ms4 161×0invalid
49.0ms184×2valid
5.0ms19×1invalid
1.0ms7×3valid
Compiler

Compiled 1 084 708 to 762 005 computations (29.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 15.2s
ival-mult: 7.7s (50.5% of total)
ival-sub: 2.7s (17.9% of total)
ival-add: 2.0s (12.9% of total)
ival-div: 938.0ms (6.2% of total)
const: 531.0ms (3.5% of total)
ival-log: 424.0ms (2.8% of total)
ival-sin: 210.0ms (1.4% of total)
ival-cos: 150.0ms (1% of total)
ival-sqrt: 124.0ms (0.8% of total)
adjust: 120.0ms (0.8% of total)
ival-true: 112.0ms (0.7% of total)
ival-exp: 66.0ms (0.4% of total)
ival-assert: 58.0ms (0.4% of total)
exact: 52.0ms (0.3% of total)
ival-fabs: 35.0ms (0.2% of total)
ival-cosh: 12.0ms (0.1% of total)
ival-tanh: 6.0ms (0% of total)
ival-sinh: 3.0ms (0% of total)

analyze19.9s (1.1%)

Memory
-45.2MiB live, 21 196.4MiB allocated
Algorithm
269×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
46.8%46.8%53.1%0.1%0%0%0%1
50.5%50.1%49.2%0.1%0%0.6%0%2
58.6%57%40.3%0.1%0%2.6%0%3
65.2%62.7%33.5%0.1%0%3.6%0%4
71.2%68.2%27.5%0.1%0%4.1%0%5
75.9%72.3%23%0.1%0%4.6%0%6
79.8%75.6%19.1%0.1%0%5.1%0%7
81.7%77%17.3%0.1%0%5.6%0%8
84.3%79.3%14.7%0.1%0%5.9%0%9
85.9%80.5%13.2%0.1%0%6.2%0%10
88.5%82.8%10.8%0.1%0%6.2%0%11
89.6%83.6%9.8%0.1%0%6.5%0%12
Compiler

Compiled 3 462 to 2 977 computations (14% saved)

start7.0ms (0%)

Memory
16.0MiB live, 15.4MiB allocated

end2.0ms (0%)

Memory
4.5MiB live, 4.2MiB allocated

Profiling

Loading profile data...