Herbie run

Date:Wednesday, December 4th, 2024
Commit:4b098aa3 on main
Hostname:nightly with Racket 8.10
Seed:2024339
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:1 774 652.9 MB

Time bar (total: 30.7min)

sample6.8min (22.3%)

Memory
3 334.2MiB live, 423 517.7MiB allocated
Samples
4.1min2 146 538×0valid
25.8s67 974×1valid
11.2s63 953×0invalid
1.7s5 727×2valid
1.0s1 175×5exit
747.0ms1 791×1invalid
359.0ms390×4exit
199.0ms622×3valid
3.0ms25×1exit
1.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 2.9min
ival-mult: 57.5s (32.9% of total)
ival-sub: 23.7s (13.6% of total)
ival-add: 23.3s (13.3% of total)
ival-div: 23.0s (13.1% of total)
ival-log: 11.8s (6.8% of total)
const: 7.3s (4.2% of total)
ival-sqrt: 5.7s (3.3% of total)
ival-sin: 5.1s (2.9% of total)
ival-cos: 3.9s (2.2% of total)
adjust: 3.8s (2.2% of total)
ival-exp: 2.5s (1.4% of total)
ival-true: 1.8s (1% of total)
ival-fabs: 1.7s (1% of total)
exact: 1.1s (0.6% of total)
ival-assert: 935.0ms (0.5% of total)
ival-cosh: 676.0ms (0.4% of total)
ival-tan: 429.0ms (0.2% of total)
ival-hypot: 198.0ms (0.1% of total)
ival-sinh: 179.0ms (0.1% of total)
ival-acos: 175.0ms (0.1% of total)
ival-tanh: 81.0ms (0% of total)
Bogosity

simplify5.4min (17.6%)

Memory
2 857.6MiB live, 292 114.3MiB allocated
Algorithm
2 181×egg-herbie
Stop Event
2 862×iter limit
1 465×node limit
728×saturated
unsound
Counts
74 091 → 72 914

soundness4.8min (15.5%)

Memory
746.3MiB live, 175 767.7MiB allocated
Stop Event
1 445×iter limit
985×node limit
164×fuel
105×done
21×saturated
unsound
Compiler

Compiled 224 520 to 88 711 computations (60.5% saved)

rewrite4.1min (13.3%)

Memory
1 309.8MiB live, 239 042.2MiB allocated
Stop Event
1 993×iter limit
911×node limit
35×unsound
17×saturated
Counts
11 905 → 373 787

localize2.0min (6.5%)

Memory
-442.8MiB live, 127 912.5MiB allocated
Samples
1.1min220 541×0valid
10.7s11 025×1valid
6.5s2 744×2valid
3.9s8 308×0invalid
2.2s789×5exit
606.0ms251×3valid
428.0ms1 006×0exit
60.0ms40×1exit
24.0ms15×2exit
12.0ms13×4valid
7.0ms4exit
Compiler

Compiled 150 969 to 23 838 computations (84.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.1min
ival-mult: 23.6s (36.9% of total)
ival-add: 9.2s (14.4% of total)
ival-div: 8.1s (12.6% of total)
ival-sub: 4.9s (7.6% of total)
ival-sin: 2.9s (4.6% of total)
const: 2.7s (4.2% of total)
ival-cos: 2.7s (4.2% of total)
ival-pow: 2.1s (3.2% of total)
adjust: 2.0s (3.1% of total)
ival-log: 1.8s (2.8% of total)
ival-neg: 1.0s (1.6% of total)
ival-sqrt: 986.0ms (1.5% of total)
ival-pow2: 478.0ms (0.7% of total)
ival-exp: 450.0ms (0.7% of total)
exact: 272.0ms (0.4% of total)
ival-true: 212.0ms (0.3% of total)
ival-assert: 108.0ms (0.2% of total)
ival-hypot: 92.0ms (0.1% of total)
ival-log1p: 90.0ms (0.1% of total)
ival-pi: 79.0ms (0.1% of total)
ival-tan: 63.0ms (0.1% of total)
ival-asin: 52.0ms (0.1% of total)
ival-fabs: 49.0ms (0.1% of total)
ival-cosh: 43.0ms (0.1% of total)
ival-sinh: 38.0ms (0.1% of total)
ival-tanh: 35.0ms (0.1% of total)
ival-acos: 21.0ms (0% of total)
ival-sinu: 16.0ms (0% of total)
ival-cosu: 9.0ms (0% of total)
ival-expm1: 4.0ms (0% of total)

eval1.7min (5.6%)

Memory
281.9MiB live, 122 233.6MiB allocated
Compiler

Compiled 17 212 761 to 1 610 555 computations (90.6% saved)

regimes1.3min (4.1%)

Memory
482.1MiB live, 88 661.6MiB allocated
Counts
33 285 → 4 796
Calls

511 calls:

11.5s
x
9.8s
y
7.9s
z
4.6s
t
2.9s
a
Compiler

Compiled 37 275 to 56 967 computations (-52.8% saved)

series1.1min (3.4%)

Memory
1 414.0MiB live, 69 427.2MiB allocated
Counts
11 905 → 74 091
Calls

9108 calls:

TimeVariablePointExpression
1.6s
y
@inf
((+ (* (/ x y) (* (/ x y) 1/2)) -1) (/ (- (* x x) (* (* y 4) y)) (+ (* x x) (* (* y 4) y))) (/ x y) (* (/ x y) 1/2) (- (* (pow (/ x y) 12) (pow (/ 1/8 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 2)) (* (/ -1 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) (/ (+ (* 1/8 (pow (/ x y) 6)) 1) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))))) (* (/ -1 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) (/ (+ (* 1/8 (pow (/ x y) 6)) 1) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)))) (- (pow (/ (* (pow (/ x y) 6) 1/8) (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1))) 3) (pow (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1) 3)) (/ (- (* x x) (* (* y 4) y)) (+ (* x x) (* (* y 4) y))) (+ (+ (* (pow (/ x y) 12) (pow (/ 1/8 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 2)) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) -2)) (/ (* 1/8 (pow (/ x y) 6)) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) 2))) (+ (* (pow (/ x y) 12) (pow (/ 1/8 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 2)) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) -2)) (/ (- (* x x) (* (* y 4) y)) (+ (* x x) (* (* y 4) y))) (+ (* (pow (/ x y) 12) (pow (/ 1/8 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 2)) (* (/ (+ (* 1/8 (pow (/ x y) 6)) 1) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) -1))) (* (/ (+ (* 1/8 (pow (/ x y) 6)) 1) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) -1)) (/ (- (* x x) (* (* y 4) y)) (+ (* x x) (* (* y 4) y))) (/ (+ (* 1/262144 (pow (/ (pow (/ x y) 6) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 6)) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) -6)) (* (/ (- (* 1/512 (pow (/ x y) 18)) 1) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) 3)) (+ (* (pow (/ x y) 12) (pow (/ 1/8 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 2)) (* (/ (+ (* 1/8 (pow (/ x y) 6)) 1) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) -1))))) (+ (* (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1) (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1)) (* (pow (/ (* -1/8 (pow (/ x y) 6)) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 1) (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1))) (+ (* (/ (* (pow (/ x y) 6) 1/8) (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1))) (/ (* (pow (/ x y) 6) 1/8) (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)))) (+ (* (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1) (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1)) (* (pow (/ (* -1/8 (pow (/ x y) 6)) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 1) (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1)))) (* (pow (/ (* -1/8 (pow (/ x y) 6)) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 1) (pow (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1)) -1)) (pow (/ (* -1/8 (pow (/ x y) 6)) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 1) (* (pow (/ x y) 12) (pow (/ 1/8 (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))) 2)) (/ (* (pow (/ x y) 6) 1/8) (+ (* (pow (/ x y) 4) 1/4) (+ (* (pow (/ x y) 2) 1/2) 1))) (/ (* 1/8 (pow (/ x y) 6)) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) 2)) (/ (- (* 1/512 (pow (/ x y) 18)) 1) (pow (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1)) 3)) (/ (- (* x x) (* (* y 4) y)) (+ (* x x) (* (* y 4) y))) (/ (* -1/8 (pow (/ x y) 6)) (+ (* 1/4 (pow (/ x y) 4)) (+ (* 1/2 (pow (/ x y) 2)) 1))))
445.0ms
t
@inf
((neg (- t x)) (+ x (/ (* (- y z) (- t x)) (- a z))) (+ (* (/ (neg (- t x)) z) (- y a)) t) (/ (neg (- t x)) z) (+ (* 0 x) (* 1 t)) (* 1 t) (+ x (/ (* (- y z) (- t x)) (- a z))) (+ (* (neg (- t x)) (/ z (- a z))) x) (+ x (/ (* (- y z) (- t x)) (- a z))) (+ (* (/ (- t x) a) y) x) (* (- 1 (/ y a)) x) (- 1 (/ y a)) (+ x (/ (* (- y z) (- t x)) (- a z))) (+ (* (neg (- t x)) (/ z (- a z))) x) (+ (* (/ (- x t) a) z) x) (/ (- x t) a) (+ x (/ (* (- y z) (- t x)) (- a z))) (/ (* (- y z) (- t x)) (- a z)) (* (- y z) (- t x)) (+ (* (neg x) (- y z)) (* t (- y z))) (* (- x t) z))
353.0ms
t
@-inf
((/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) (/ (- t a) (- b y)) (* (- (/ t (* (- b y) a)) (/ 1 (- b y))) a) (- (/ t (* (- b y) a)) (/ 1 (- b y))) (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) (/ x (- 1 z)) (+ (* x z) x) (* z x) (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) (/ (- t a) b) (- t a) (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) (* (/ y (+ (* (- b y) z) y)) x) (/ y (+ (* (- b y) z) y)) (+ (* (- b y) z) y) (- (/ t y) (/ (* (- b y) x) y)) (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) (/ (+ (* t z) (* y x)) (+ (* (- b y) z) y)) (+ (* (- (/ t y) (/ (* (- b y) x) y)) z) x) (/ t (* (- b y) a)) (/ 1 (- b y)) (/ (* (- b y) x) y))
341.0ms
a
@0
((+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (+ (* (+ (* (neg y) i) (* a c)) j) (* (+ (* (neg c) z) (* t i)) b)) (+ (* (neg y) i) (* a c)) (neg y) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (* (+ (* (neg a) x) (* i b)) t) (+ (* (neg a) x) (* i b)) (* i b) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (* (+ (* (neg x) t) (* j c)) a) (+ (* (neg x) t) (* j c)) (* (neg t) x) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (* (+ (* (neg y) i) (* a c)) j) (* (* (- y (/ (* t b) j)) j) (neg i)) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (* (* 1 j) (+ (* c a) (+ (* (neg i) y) (/ (+ (* (neg b) (+ (* (neg i) t) (* c z))) (* (+ (* (neg a) t) (* z y)) x)) j)))) (* (- y (/ (* t b) j)) j) (* (+ (* (neg c) z) (* t i)) b) (+ (* (neg c) z) (* t i)) (neg t) (/ (* t b) j))
322.0ms
y
@0
((* (* (* 3 x) y) x) (* (* 3 x) y) (* 3 x) (* (* x y) (* 3 x)) (* x y) (/ -3 (/ -1 x)) (* (* (/ -3 (/ -1 x)) x) y) (* (/ -3 (/ -1 x)) x) (/ -1 x) (/ (/ (* 3 y) (/ -1 x)) (/ -1 x)) (/ (* 3 y) (/ -1 x)) (* 3 y) (* (pow x 3/8) (* (pow x 3/8) (* (* (pow x 3/4) y) (* (sqrt x) 3)))) (* (pow x 3/8) (* (* (pow x 3/4) y) (* (sqrt x) 3))) (pow x 3/8) (* (* (pow x 3/4) y) (* (sqrt x) 3)) (* (sqrt x) 3))

preprocess1.0min (3.4%)

Memory
754.0MiB live, 62 009.4MiB allocated
Algorithm
269×egg-herbie
Stop Event
536×iter limit
398×saturated
142×node limit
Compiler

Compiled 330 334 to 61 158 computations (81.5% saved)

explain50.7s (2.8%)

Memory
-1 199.0MiB live, 56 972.3MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15433
/.f64#fo/n11230
sqrt.f64#foflow-rescue7770
/.f64#fo/o5790
-.f64#fcancellation55710
*.f64#fn*o5070
+.f64#fnan-rescue4710
-.f64#fnan-rescue4600
cos.f64#fsensitivity3360
/.f64#fn/o3020
+.f64#fcancellation2981
/.f64#fu/n2780
sin.f64#fsensitivity2200
*.f64#fn*u1850
cos.f64#foflow-rescue1440
/.f64#fn/u1150
log.f64#foflow-rescue990
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity930
/.f64#fu/u810
log.f64#fuflow-rescue710
sqrt.f64#fuflow-rescue470
*.f64#fo*u320
exp.f64#fsensitivity294
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue280
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow28
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue280
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow28
+.f64(+.f64 x (*.f64 (*.f64 (-.f64 y x) #s(literal 6 binary64)) (-.f64 (/.f64 #s(literal 2 binary64) #s(literal 3 binary64)) z)))oflow-right10
Confusion
Predicted +Predicted -
+5911212
-164361098
Precision
0.7824993380990204
Recall
0.9653764494528826
Confusion?
Predicted +Predicted MaybePredicted -
+59111211
-16431861080
Precision?
0.780668163211409
Recall?
0.9655397680875388
Freqs
test
numberfreq
061310
16814
2661
355
417
57
Total Confusion?
Predicted +Predicted MaybePredicted -
+14200
-21124
Precision?
0.9793103448275862
Recall?
1.0
Samples
14.5s130 828×0valid
3.1s5 710×1valid
780.0ms1 094×2valid
27.0ms92×3valid
1.0ms4valid
Compiler

Compiled 24 442 to 8 402 computations (65.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 10.5s
ival-mult: 3.3s (31.6% of total)
ival-log: 1.6s (14.9% of total)
ival-sub: 1.4s (12.9% of total)
ival-add: 1.2s (11.2% of total)
ival-div: 944.0ms (9% of total)
const: 392.0ms (3.7% of total)
adjust: 375.0ms (3.6% of total)
ival-exp: 318.0ms (3% of total)
ival-sin: 297.0ms (2.8% of total)
ival-cos: 292.0ms (2.8% of total)
ival-sqrt: 169.0ms (1.6% of total)
ival-true: 123.0ms (1.2% of total)
exact: 67.0ms (0.6% of total)
ival-assert: 58.0ms (0.6% of total)
ival-tan: 11.0ms (0.1% of total)
ival-cosh: 11.0ms (0.1% of total)
ival-fabs: 11.0ms (0.1% of total)
ival-sinh: 9.0ms (0.1% of total)
ival-hypot: 9.0ms (0.1% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-acos: 4.0ms (0% of total)

bsearch40.0s (2.2%)

Memory
374.5MiB live, 40 381.8MiB allocated
Algorithm
1 776×binary-search
951×left-value
Stop Event
1 744×narrow-enough
32×predicate-same
Samples
21.7s137 317×0valid
1.2s3 361×1valid
269.0ms3 180×0invalid
22.0ms117×2valid
12.0ms49×1invalid
1.0ms3valid
Compiler

Compiled 1 104 019 to 777 050 computations (29.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 16.0s
ival-mult: 7.2s (45.2% of total)
ival-sub: 3.1s (19.1% of total)
ival-add: 1.9s (11.7% of total)
ival-div: 1.1s (6.8% of total)
const: 716.0ms (4.5% of total)
ival-log: 454.0ms (2.8% of total)
ival-sin: 417.0ms (2.6% of total)
ival-cos: 391.0ms (2.4% of total)
ival-exp: 208.0ms (1.3% of total)
adjust: 173.0ms (1.1% of total)
ival-sqrt: 116.0ms (0.7% of total)
ival-true: 113.0ms (0.7% of total)
ival-assert: 59.0ms (0.4% of total)
exact: 54.0ms (0.3% of total)
ival-tanh: 17.0ms (0.1% of total)
ival-cosh: 14.0ms (0.1% of total)
ival-sinh: 7.0ms (0% of total)
ival-fabs: 3.0ms (0% of total)

prune38.0s (2.1%)

Memory
-714.8MiB live, 51 147.6MiB allocated
Counts
422 418 → 12 896
Compiler

Compiled 835 911 to 451 136 computations (46% saved)

analyze23.0s (1.3%)

Memory
519.4MiB live, 25 435.1MiB 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)

start10.0ms (0%)

Memory
26.3MiB live, 26.0MiB allocated

end2.0ms (0%)

Memory
4.3MiB live, 4.1MiB allocated

Profiling

Loading profile data...