Herbie run

Date:Thursday, October 31st, 2024
Commit:946043fe on Original-Inv-Same-cost-model
Hostname:nightly with Racket 8.10
Seed:2024305
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

Time bar (total: 5.0min)

sample1.2min (23.8%)

Memory
442.8MiB live, 72 068.8MiB allocated
Samples
31.5s285 583×0valid
12.6s43 975×1valid
7.3s16 760×2valid
523.0ms4 221×0invalid
228.0ms434×3valid
194.0ms101×3exit
141.0ms952×0exit
100.0ms101×4exit
5.0ms32×1exit
Precisions
Click to see histograms. Total time spent on operations: 39.9s
ival-mult: 8.1s (20.4% of total)
ival-add: 4.7s (11.7% of total)
const: 3.5s (8.7% of total)
ival-sub: 3.4s (8.5% of total)
ival-div: 3.1s (7.8% of total)
ival-pow: 3.0s (7.6% of total)
ival-<=: 2.9s (7.2% of total)
adjust: 2.7s (6.7% of total)
ival-sin: 2.0s (5% of total)
ival-neg: 1.5s (3.7% of total)
ival-cos: 1.5s (3.7% of total)
ival-exp: 635.0ms (1.6% of total)
ival-sqrt: 567.0ms (1.4% of total)
exact: 454.0ms (1.1% of total)
ival-atan: 416.0ms (1% of total)
ival-and: 371.0ms (0.9% of total)
ival-==: 239.0ms (0.6% of total)
ival-pow2: 215.0ms (0.5% of total)
ival-true: 155.0ms (0.4% of total)
ival-assert: 147.0ms (0.4% of total)
ival-tan: 106.0ms (0.3% of total)
ival-expm1: 99.0ms (0.2% of total)
ival-<: 99.0ms (0.2% of total)
ival-log1p: 84.0ms (0.2% of total)
ival-pi: 43.0ms (0.1% of total)
ival-hypot: 17.0ms (0% of total)
ival-if: 4.0ms (0% of total)
ival-fabs: 4.0ms (0% of total)
Bogosity

simplify53.4s (17.7%)

Memory
580.1MiB live, 45 679.9MiB allocated
Algorithm
344×egg-herbie
Stop Event
471×iter limit
306×node limit
39×saturated
11×unsound
Counts
11 132 → 10 988

soundness41.1s (13.6%)

Memory
-272.3MiB live, 23 380.1MiB allocated
Stop Event
306×iter limit
181×node limit
28×fuel
14×done
saturated
unsound
Compiler

Compiled 43 661 to 13 861 computations (68.3% saved)

rewrite36.4s (12.1%)

Memory
-397.4MiB live, 34 211.5MiB allocated
Stop Event
306×iter limit
145×node limit
11×saturated
unsound
Counts
2 005 → 98 899

eval23.2s (7.7%)

Memory
465.8MiB live, 27 275.3MiB allocated
Compiler

Compiled 4 614 593 to 406 553 computations (91.2% saved)

localize22.9s (7.6%)

Memory
-59.9MiB live, 22 687.6MiB allocated
Samples
9.1s29 836×0valid
4.3s5 644×1valid
3.7s2 403×2valid
508.0ms198×3valid
157.0ms259×0exit
81.0ms12×5exit
57.0ms295×0invalid
46.0ms4valid
Compiler

Compiled 77 173 to 9 009 computations (88.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.3s
ival-mult: 3.3s (24.6% of total)
ival-add: 1.9s (14.3% of total)
ival-div: 1.8s (13.5% of total)
adjust: 1.3s (9.5% of total)
ival-sub: 1.2s (9% of total)
ival-pow: 847.0ms (6.4% of total)
const: 734.0ms (5.5% of total)
ival-tan: 580.0ms (4.4% of total)
ival-sin: 440.0ms (3.3% of total)
ival-neg: 377.0ms (2.8% of total)
ival-sqrt: 186.0ms (1.4% of total)
ival-exp: 148.0ms (1.1% of total)
ival-cos: 134.0ms (1% of total)
ival-pow2: 123.0ms (0.9% of total)
ival-pi: 101.0ms (0.8% of total)
exact: 62.0ms (0.5% of total)
ival-log1p: 54.0ms (0.4% of total)
ival-true: 35.0ms (0.3% of total)
ival-expm1: 30.0ms (0.2% of total)
ival-assert: 18.0ms (0.1% of total)
ival-atan: 7.0ms (0.1% of total)
ival-log: 3.0ms (0% of total)

preprocess14.7s (4.9%)

Memory
166.5MiB live, 10 870.6MiB allocated
Algorithm
42×egg-herbie
Stop Event
82×iter limit
65×node limit
21×saturated
Compiler

Compiled 59 787 to 9 290 computations (84.5% saved)

explain10.2s (3.4%)

Memory
-408.6MiB live, 11 370.8MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation13170
+.f64#fcancellation38391
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2140
sqrt.f64#foflow-rescue1940
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1840
/.f64#fo/o1630
/.f64#fn/o1580
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1130
-.f64#fnan-rescue1060
/.f64#fu/n700
/.f64#fn/u630
/.f64#fo/n510
*.f64#fn*u450
/.f64#fu/u430
+.f64#fnan-rescue390
*.f64#fn*o290
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue180
(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow32
(/.f64 i n)overflow18
(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow18
sqrt.f64#fuflow-rescue80
Confusion
Predicted +Predicted -
+3889210
-1086545
Precision
0.9729797348011008
Recall
0.9487679921932178
Confusion?
Predicted +Predicted MaybePredicted -
+388916149
-1081866359
Precision?
0.9323204419889503
Recall?
0.9880458648450842
Freqs
test
numberfreq
06755
13566
2386
345
Total Confusion?
Predicted +Predicted MaybePredicted -
+3010
-209
Precision?
0.9393939393939394
Recall?
1.0
Samples
1.5s16 420×0valid
1.4s3 748×1valid
490.0ms1 288×2valid
29.0ms46×3valid
5.0ms4valid
Compiler

Compiled 10 840 to 1 926 computations (82.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.4s
ival-mult: 597.0ms (25.1% of total)
ival-sub: 374.0ms (15.8% of total)
ival-pow: 257.0ms (10.8% of total)
ival-add: 244.0ms (10.3% of total)
adjust: 211.0ms (8.9% of total)
ival-div: 204.0ms (8.6% of total)
ival-sin: 136.0ms (5.7% of total)
ival-cos: 112.0ms (4.7% of total)
const: 53.0ms (2.2% of total)
ival-exp: 36.0ms (1.5% of total)
ival-sqrt: 36.0ms (1.5% of total)
ival-pow2: 30.0ms (1.3% of total)
ival-true: 21.0ms (0.9% of total)
exact: 19.0ms (0.8% of total)
ival-neg: 15.0ms (0.6% of total)
ival-assert: 10.0ms (0.4% of total)
ival-log1p: 5.0ms (0.2% of total)
ival-expm1: 5.0ms (0.2% of total)
ival-tan: 4.0ms (0.2% of total)
ival-atan: 4.0ms (0.2% of total)
ival-pi: 2.0ms (0.1% of total)

regimes7.9s (2.6%)

Memory
123.1MiB live, 9 252.0MiB allocated
Counts
6 097 → 630
Calls

96 calls:

870.0ms
x
362.0ms
b
349.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
298.0ms
c
291.0ms
n
Compiler

Compiled 9 366 to 6 053 computations (35.4% saved)

prune7.3s (2.4%)

Memory
-666.5MiB live, 10 125.4MiB allocated
Counts
110 920 → 2 281
Compiler

Compiled 168 185 to 73 199 computations (56.5% saved)

analyze4.6s (1.5%)

Memory
-70.3MiB live, 4 458.2MiB allocated
Algorithm
43×search
random
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%54.5%45.5%0%0%0%0
21.4%11.7%42.9%45.5%0%0%0%1
37.4%20.4%34.1%45.5%0%0%0%2
48.7%26.2%27.7%45.5%0%0.6%0%3
57.7%30.7%22.6%45.5%0%1.2%0%4
71.2%37.7%15.3%45.5%0%1.6%0%5
72.9%38.4%14.3%45.5%0%1.8%0%6
77.9%40.7%11.6%45.5%0%2.2%0%7
81.5%42.6%9.7%45.5%0%2.3%0%8
84.1%43.8%8.3%45.5%0%2.5%0%9
86.2%44.6%7.2%45.5%0%2.7%0%10
88.2%45.6%6.1%45.5%0%2.8%0%11
89.1%45.9%5.6%45.5%0%2.9%0%12
Compiler

Compiled 1 402 to 721 computations (48.6% saved)

series4.5s (1.5%)

Memory
86.7MiB live, 4 660.9MiB allocated
Counts
2 005 → 11 132
Calls

876 calls:

TimeVariablePointExpression
111.0ms
r
@inf
((- (- (+ 3 (/ 2 (* r r))) (/ (* 1/8 (+ (* -2 v) 3)) (* (- 1 v) (pow (* r w) -2)))) 9/2) (* 1/8 (+ (* -2 v) 3)) (* (* w r) (* w r)) (- (+ 3 (/ 2 (* r r))) (/ (* 1/8 (+ (* -2 v) 3)) (* (- 1 v) (pow (* r w) -2)))) (* (* (* (* w w) r) -1/4) r) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (/ 2 (* r r)) (+ (* (* (* 1/4 (* r r)) w) w) 3/2)) (* (* (* w w) r) -1/4) (+ (* (* -3/8 (* r r)) (* w w)) 3) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) (+ (* (* -3/8 (* w w)) (* r r)) (+ 3 (/ (/ 2 r) r))) (+ (* (* -1/4 (* w w)) (* r r)) -3/2) (+ (/ 2 (* r r)) (- 3 (+ (* (/ (pow (* w r) 2) (- 1 v)) (* (+ (* -2 v) 3) 1/8)) 9/2))) (/ 2 (* r r)) (* r r) (- (- (+ 3 (/ 2 (* r r))) (* (* (* (* (+ (* -2 v) 3) 1/8) w) (* w r)) (/ r (- 1 v)))) 9/2) (- (+ 3 (/ 2 (* r r))) (* (* (* (* (+ (* -2 v) 3) 1/8) w) (* w r)) (/ r (- 1 v)))) (+ 3 (/ 2 (* r r))) (/ (* 1/8 (+ (* -2 v) 3)) (* (- 1 v) (pow (* r w) -2))) (/ (- 1 v) (* (* w r) (* w r))) (* (* w w) r) (* -3/8 (* r r)) (- 3 (+ (* (/ (pow (* w r) 2) (- 1 v)) (* (+ (* -2 v) 3) 1/8)) 9/2)) (* -1/4 (* w w)) (* (* (* (+ (* -2 v) 3) 1/8) w) (* w r)) (* (* (* (* (+ (* -2 v) 3) 1/8) w) (* w r)) (/ r (- 1 v))))
93.0ms
c
@-inf
((/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (- (* b b) (* 4 (* a c))) (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (neg b) (sqrt (- (* b b) (* 4 (* a c)))))
77.0ms
x
@0
((/ x (/ 1 (+ (* (* -6450306886639899/50000000000000000 x) x) 238732414637843/250000000000000))) (/ 1 (+ (* (* -6450306886639899/50000000000000000 x) x) 238732414637843/250000000000000)) (+ (* (* -6450306886639899/50000000000000000 x) x) 238732414637843/250000000000000) (* -6450306886639899/50000000000000000 x) (* (* x x) x) (- (* 238732414637843/250000000000000 x) (* (* (* -6450306886639899/50000000000000000 (* x x)) -1) x)) (* -6450306886639899/50000000000000000 (* (* x x) x)) (* x x) (* (* (* -6450306886639899/50000000000000000 x) x) x) (- (* 238732414637843/250000000000000 x) (* (* (* -6450306886639899/50000000000000000 (* x x)) -1) x)) (* (* -6450306886639899/50000000000000000 x) x) (- (* 238732414637843/250000000000000 x) (* 6450306886639899/50000000000000000 (* (* x x) x))) (* (sqrt (* (* 238732414637843/250000000000000 x) (sqrt x))) (sqrt (* (sqrt x) 238732414637843/250000000000000))) (sqrt (* (* 238732414637843/250000000000000 x) (sqrt x))) (* (* 238732414637843/250000000000000 x) (sqrt x)) (sqrt (pow x 4)) (* (+ (* -6450306886639899/50000000000000000 (sqrt (pow x 4))) 238732414637843/250000000000000) x) (+ (* -6450306886639899/50000000000000000 (sqrt (pow x 4))) 238732414637843/250000000000000) (pow x 4) (* (sqrt x) 238732414637843/250000000000000))
76.0ms
x
@-inf
((/ x (/ 1 (+ (* (* -6450306886639899/50000000000000000 x) x) 238732414637843/250000000000000))) (/ 1 (+ (* (* -6450306886639899/50000000000000000 x) x) 238732414637843/250000000000000)) (+ (* (* -6450306886639899/50000000000000000 x) x) 238732414637843/250000000000000) (* -6450306886639899/50000000000000000 x) (* (* x x) x) (- (* 238732414637843/250000000000000 x) (* (* (* -6450306886639899/50000000000000000 (* x x)) -1) x)) (* -6450306886639899/50000000000000000 (* (* x x) x)) (* x x) (* (* (* -6450306886639899/50000000000000000 x) x) x) (- (* 238732414637843/250000000000000 x) (* (* (* -6450306886639899/50000000000000000 (* x x)) -1) x)) (* (* -6450306886639899/50000000000000000 x) x) (- (* 238732414637843/250000000000000 x) (* 6450306886639899/50000000000000000 (* (* x x) x))) (* (sqrt (* (* 238732414637843/250000000000000 x) (sqrt x))) (sqrt (* (sqrt x) 238732414637843/250000000000000))) (sqrt (* (* 238732414637843/250000000000000 x) (sqrt x))) (* (* 238732414637843/250000000000000 x) (sqrt x)) (sqrt (pow x 4)) (* (+ (* -6450306886639899/50000000000000000 (sqrt (pow x 4))) 238732414637843/250000000000000) x) (+ (* -6450306886639899/50000000000000000 (sqrt (pow x 4))) 238732414637843/250000000000000) (pow x 4) (* (sqrt x) 238732414637843/250000000000000))
73.0ms
y
@0
((exp (* (log (* y 1/2)) -1)) (* (log (* y 1/2)) -1) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (+ (* (exp (* (log (* y 1/2)) -1)) (* x (/ x y))) -1) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (/ (* (- x y) (+ x y)) (+ (* y y) (* x x))) (* (- x y) (+ x y)) (* x x) (+ (* y y) (* x x)) (* (+ y x) (/ (- x y) (+ (* y y) (* x x)))) (+ y x) (/ (- x y) (+ (* y y) (* x x))) (- x y) (/ (- (* (* 4 (pow (/ (* (/ y x) y) x) 2)) (+ (* (* (/ y x) y) (/ -2 x)) -1)) (* (+ (* (* (/ y x) y) (/ -2 x)) -1) 1)) (* (+ (* (* (/ y x) y) (/ -2 x)) -1) (+ (* (* (/ y x) y) (/ -2 x)) -1))) (- (* (* 4 (pow (/ (* (/ y x) y) x) 2)) (+ (* (* (/ y x) y) (/ -2 x)) -1)) (* (+ (* (* (/ y x) y) (/ -2 x)) -1) 1)) (pow (/ (* (/ y x) y) x) 2) (* (+ (* (* (/ y x) y) (/ -2 x)) -1) 1) (* x (/ x y)) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (/ (* (/ y x) y) x))

bsearch3.2s (1.1%)

Memory
3.1MiB live, 3 570.1MiB allocated
Algorithm
207×binary-search
102×left-value
Stop Event
191×narrow-enough
15×predicate-same
predicate-failed
Samples
1.3s11 730×0valid
241.0ms1 048×1valid
107.0ms362×2valid
76.0ms1 112×0invalid
8.0ms12×3valid
5.0ms33×1exit
Compiler

Compiled 132 731 to 72 892 computations (45.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.3s
ival-mult: 538.0ms (41.3% of total)
ival-div: 189.0ms (14.5% of total)
ival-sub: 146.0ms (11.2% of total)
ival-add: 136.0ms (10.4% of total)
ival-pow: 122.0ms (9.4% of total)
ival-exp: 47.0ms (3.6% of total)
adjust: 41.0ms (3.1% of total)
ival-neg: 28.0ms (2.1% of total)
ival-sqrt: 20.0ms (1.5% of total)
ival-true: 11.0ms (0.8% of total)
exact: 11.0ms (0.8% of total)
ival-assert: 6.0ms (0.5% of total)
const: 3.0ms (0.2% of total)
ival-pi: 3.0ms (0.2% of total)

start2.0ms (0%)

Memory
3.7MiB live, 3.7MiB allocated

end0.0ms (0%)

Memory
0.5MiB live, 0.5MiB allocated

Profiling

Loading profile data...