Herbie run

Date:Saturday, October 5th, 2024
Commit:3ce6ba2b on main
Hostname:nightly with Racket 8.10
Seed:2024279
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: 34.0min)

sample6.3min (18.6%)

Memory
1 021.8MiB live, 380 946.9MiB allocated
Samples
3.8min2 147 412×0valid
24.1s67 259×1valid
10.7s64 056×0invalid
2.1s5 613×2valid
1.1s1 110×5exit
569.0ms1 748×1invalid
495.0ms580×3valid
302.0ms340×4exit
2.0ms21×1exit
Precisions
Click to see histograms. Total time spent on operations: 2.7min
ival-mult: 58.2s (35.5% of total)
ival-add: 23.3s (14.2% of total)
ival-sub: 21.0s (12.8% of total)
ival-div: 19.5s (11.9% of total)
ival-log: 9.4s (5.8% of total)
const: 6.0s (3.7% of total)
ival-sqrt: 6.0s (3.6% of total)
ival-sin: 4.6s (2.8% of total)
ival-exp: 3.2s (2% of total)
adjust: 3.2s (1.9% of total)
ival-cos: 2.9s (1.7% of total)
ival-true: 1.6s (1% of total)
ival-fabs: 1.2s (0.7% of total)
exact: 1.1s (0.7% of total)
ival-assert: 959.0ms (0.6% of total)
ival-cosh: 512.0ms (0.3% of total)
ival-tan: 310.0ms (0.2% of total)
ival-acos: 288.0ms (0.2% of total)
ival-sinh: 190.0ms (0.1% of total)
ival-tanh: 183.0ms (0.1% of total)
ival-hypot: 160.0ms (0.1% of total)
Bogosity

simplify6.3min (18.5%)

Memory
2 277.0MiB live, 294 212.8MiB allocated
Algorithm
2 129×egg-herbie
Stop Event
2 777×iter limit
1 238×node limit
904×saturated
Counts
351 636 → 343 415

soundness5.3min (15.6%)

Memory
1 038.1MiB live, 160 624.4MiB allocated
Stop Event
1 414×iter limit
958×node limit
147×fuel
122×done
21×saturated
unsound
Compiler

Compiled 135 570 to 79 360 computations (41.5% saved)

rewrite3.6min (10.6%)

Memory
1 141.1MiB live, 219 270.4MiB allocated
Stop Event
1 907×iter limit
901×node limit
20×unsound
16×saturated
Counts
11 470 → 478 119

eval3.2min (9.5%)

Memory
1 375.0MiB live, 238 527.0MiB allocated
Compiler

Compiled 21 039 488 to 1 911 867 computations (90.9% saved)

localize2.0min (6%)

Memory
-1 766.7MiB live, 123 068.7MiB allocated
Samples
1.2min218 349×0valid
10.1s10 706×1valid
5.3s3 266×2valid
1.5s3 315×0invalid
995.0ms437×5exit
632.0ms1 229×0exit
405.0ms280×3valid
356.0ms354×2exit
140.0ms139×1exit
6.0ms4valid
Compiler

Compiled 251 407 to 40 989 computations (83.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 55.5s
ival-mult: 20.4s (36.8% of total)
ival-div: 9.2s (16.6% of total)
ival-add: 7.4s (13.4% of total)
ival-sub: 4.0s (7.2% of total)
ival-log: 2.3s (4.1% of total)
adjust: 2.3s (4.1% of total)
const: 2.2s (3.9% of total)
ival-pow: 1.8s (3.2% of total)
ival-cos: 1.1s (2% of total)
ival-neg: 1.0s (1.9% of total)
ival-sqrt: 808.0ms (1.5% of total)
ival-sin: 736.0ms (1.3% of total)
ival-exp: 518.0ms (0.9% of total)
ival-pow2: 260.0ms (0.5% of total)
exact: 253.0ms (0.5% of total)
ival-hypot: 211.0ms (0.4% of total)
ival-true: 205.0ms (0.4% of total)
ival-expm1: 167.0ms (0.3% of total)
ival-tan: 163.0ms (0.3% of total)
ival-log1p: 130.0ms (0.2% of total)
ival-assert: 117.0ms (0.2% of total)
ival-tanh: 53.0ms (0.1% of total)
ival-cosh: 30.0ms (0.1% of total)
ival-sinh: 28.0ms (0.1% of total)
ival-pi: 27.0ms (0% of total)
ival-fabs: 27.0ms (0% of total)
ival-acos: 20.0ms (0% of total)
ival-asin: 13.0ms (0% of total)
ival-cbrt: 7.0ms (0% of total)

regimes1.6min (4.6%)

Memory
-904.7MiB live, 117 077.2MiB allocated
Counts
39 374 → 5 081
Calls

511 calls:

12.8s
x
12.7s
y
9.6s
z
6.2s
t
3.8s
a
Compiler

Compiled 38 777 to 58 406 computations (-50.6% saved)

series1.5min (4.3%)

Memory
540.3MiB live, 85 996.1MiB allocated
Counts
11 470 → 351 636
Calls

8898 calls:

TimeVariablePointExpression
3.9s
a
@-inf
((+ (* (+ (* z (* y (* 18 x))) (* -4 a)) t) (+ (* c b) (neg (+ (* k (* 27 j)) (* i (* 4 x)))))) (+ (* z (* y (* 18 x))) (* -4 a)) (* y (* 18 x)) (* 18 x) (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (* -27 (* k j)) (* k j) (+ (* (* 27 k) (neg j)) (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i))) (* 27 k) (neg j) (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* i x) -4) (* i x) (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (+ (* c b) (+ (* (* -27 k) j) (* -4 (* a t)))) (+ (* (* -27 k) j) (* -4 (* a t))) (* -27 k) (+ (* c b) (neg (+ (* k (* 27 j)) (* i (* 4 x))))) (* (* j 27) k))
2.3s
x
@inf
((/ (log (/ y x)) (/ -1 x)) (log (/ y x)) (/ y x) (/ -1 x) (/ (* (neg (* x x)) (log (/ y x))) x) (* (neg (* x x)) (log (/ y x))) (neg (* x x)) (* x x) (* x (* 2 (log (/ (sqrt (neg x)) (sqrt (neg y)))))) (* 2 (log (/ (sqrt (neg x)) (sqrt (neg y))))) (log (/ (sqrt (neg x)) (sqrt (neg y)))) (/ (sqrt (neg x)) (sqrt (neg y))) (* x (- (log (neg (pow x 3))) (log (* (neg y) (* x x))))) (- (log (neg (pow x 3))) (log (* (neg y) (* x x)))) (log (neg (pow x 3))) (* (log (neg x)) 3) (* x (- (log (* (* (neg x) x) x)) (log (* (neg y) (* x x))))) (- (log (* (* (neg x) x) x)) (log (* (neg y) (* x x)))) (log (* (* (neg x) x) x)) (* (neg x) x) (neg x) (log (* (neg y) (* x x))) (* (neg y) (* x x)))
1.4s
y
@0
((/ 1 (pow x -1)) (* (/ 1 (pow x -1)) (log (+ 1 (/ (neg y) x)))) (pow x -1) (log (+ 1 (/ (neg y) x))) (* (log (- 1 (/ y x))) x) (log (- 1 (/ y x))) (/ (neg y) x) (neg y) (/ -1 (/ x y)) (* x 1) (* (* x 1) (log (- 1 (/ y x)))) (log (- 1 (/ y x))) (* (/ (* y y) x) (/ -1 y)) (* (* x 1) (log (- 1 (/ y x)))) (log (- 1 (/ y x))) (* x (log (- 1 (/ y x)))) (log (- 1 (/ y x))) (- (log y) (log (neg x))) (log y) (/ (* y y) x))
479.0ms
a
@-inf
((* (+ (* (* z y) -9) (+ (* (/ (* b a) t) 27) (* (/ x t) 2))) t) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* z y) -9) (+ (* (/ (* b a) t) 27) (* (/ x t) 2))) (* z y) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (* (* b a) 27) (* b a) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* 27 b) a) (* x 2)) (* 27 b) (* x 2) (+ (* (* t y) (* -9 z)) (+ (* (* b 27) a) (* 2 x))) (* t y) (* -9 z) (+ (* (* b 27) a) (* 2 x)) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* (* y t) z) -9) (* (* a b) 27)) (* (* y t) z) (* y t) (/ (* b a) t) (+ (* (/ (* b a) t) 27) (* (/ x t) 2)) (* (* a b) 27))
354.0ms
y
@0
((+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (* x (log y)) z) (+ (+ (+ (* x (log y)) z) t) a) (* x (log y)) (* (- b 1/2) (log c)))

preprocess1.3min (3.9%)

Memory
349.1MiB live, 70 629.5MiB allocated
Algorithm
269×egg-herbie
Stop Event
538×iter limit
394×saturated
144×node limit
Compiler

Compiled 175 538 to 57 710 computations (67.1% saved)

prune1.1min (3.3%)

Memory
-3 363.4MiB live, 100 524.1MiB allocated
Counts
905 507 → 14 043
Compiler

Compiled 426 148 to 298 621 computations (29.9% saved)

explain46.6s (2.3%)

Memory
-1 048.4MiB live, 55 341.5MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15694
/.f64#fo/n12660
sqrt.f64#foflow-rescue7560
/.f64#fo/o6120
-.f64#fcancellation5747
*.f64#fn*o5000
-.f64#fnan-rescue4990
+.f64#fnan-rescue4550
cos.f64#fsensitivity3590
+.f64#fcancellation3353
/.f64#fn/o3320
/.f64#fu/n3010
sin.f64#fsensitivity2250
*.f64#fn*u1820
/.f64#fn/u1400
cos.f64#foflow-rescue1250
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity1030
/.f64#fu/u860
log.f64#fuflow-rescue830
log.f64#foflow-rescue820
sqrt.f64#fuflow-rescue550
exp.f64#fsensitivity324
*.f64#fo*u270
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue230
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow23
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue230
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow23
*.f64(*.f64 (-.f64 (*.f64 k y2) (*.f64 j y3)) (-.f64 (*.f64 y4 y1) (*.f64 y5 y0)))u*o20
(*.f64 j y3)underflow28
(-.f64 (*.f64 k y2) (*.f64 j y3))underflow8
(*.f64 k y2)underflow31
(*.f64 y4 y1)overflow38
(-.f64 (*.f64 y4 y1) (*.f64 y5 y0))overflow68
(*.f64 y5 y0)overflow38
Confusion
Predicted +Predicted -
+6158222
-169060794
Precision
0.7846585117227319
Recall
0.965203761755486
Confusion?
Predicted +Predicted MaybePredicted -
+61586216
-16901360781
Precision?
0.7835261217745011
Recall?
0.9661442006269593
Freqs
test
numberfreq
061016
17062
2705
355
423
51
62
Total Confusion?
Predicted +Predicted MaybePredicted -
+13800
-21128
Precision?
0.9787234042553191
Recall?
1.0
Samples
14.2s130 540×0valid
2.4s5 896×1valid
636.0ms1 208×2valid
38.0ms84×3valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 9.7s
ival-mult: 3.1s (31.9% of total)
ival-sub: 1.4s (14.6% of total)
ival-div: 1.1s (11.4% of total)
ival-add: 1.1s (11.2% of total)
ival-log: 924.0ms (9.6% of total)
ival-sqrt: 360.0ms (3.7% of total)
const: 353.0ms (3.7% of total)
adjust: 325.0ms (3.4% of total)
ival-sin: 255.0ms (2.6% of total)
ival-cos: 187.0ms (1.9% of total)
ival-exp: 161.0ms (1.7% of total)
ival-true: 116.0ms (1.2% of total)
ival-hypot: 105.0ms (1.1% of total)
exact: 63.0ms (0.7% of total)
ival-assert: 60.0ms (0.6% of total)
ival-tan: 31.0ms (0.3% 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-tanh: 7.0ms (0.1% of total)
ival-acos: 5.0ms (0.1% of total)

bsearch37.3s (1.8%)

Memory
-20.1MiB live, 38 209.4MiB allocated
Algorithm
1 671×binary-search
1 218×left-value
Stop Event
1 652×narrow-enough
19×predicate-same
Samples
19.5s133 953×0valid
1.1s3 304×1valid
277.0ms2 646×0invalid
26.0ms106×2valid
2.0ms13×3valid
Compiler

Compiled 289 627 to 337 332 computations (-16.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 12.8s
ival-mult: 5.5s (42.5% of total)
ival-sub: 2.3s (17.9% of total)
ival-add: 1.4s (10.8% of total)
ival-div: 1.1s (8.9% of total)
const: 599.0ms (4.7% of total)
ival-log: 597.0ms (4.7% of total)
ival-sin: 367.0ms (2.9% of total)
ival-cos: 356.0ms (2.8% of total)
adjust: 148.0ms (1.2% of total)
ival-sqrt: 140.0ms (1.1% of total)
ival-true: 101.0ms (0.8% of total)
ival-exp: 94.0ms (0.7% of total)
ival-assert: 59.0ms (0.5% of total)
exact: 50.0ms (0.4% of total)
ival-tanh: 16.0ms (0.1% of total)
ival-cosh: 8.0ms (0.1% of total)
ival-fabs: 4.0ms (0% of total)
ival-sinh: 4.0ms (0% of total)

analyze20.1s (1%)

Memory
-12.3MiB live, 23 061.8MiB 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)

start8.0ms (0%)

Memory
16.2MiB live, 16.0MiB allocated

end2.0ms (0%)

Memory
4.6MiB live, 4.3MiB allocated

Profiling

Loading profile data...