Herbie run

Date:Wednesday, January 15th, 2025
Commit:d270acbc on main
Seed:2025015
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:115 468.0 MB

Time bar (total: 2.0min)

sample51.8s (42.6%)

Memory
586.1MiB live, 49 770.2MiB allocated; 16.0s collecting garbage
Samples
15.3s16 461×5exit
11.5s40 135×1valid
9.1s108 684×0valid
5.7s16 301×2valid
377.0ms3 875×0invalid
160.0ms1 395×0exit
Precisions
Click to see histograms. Total time spent on operations: 33.6s
ival-exp: 4.3s (12.8% of total)
ival-pow: 3.9s (11.6% of total)
adjust: 3.8s (11.4% of total)
ival-log: 2.6s (7.8% of total)
const: 2.6s (7.8% of total)
ival-cos: 2.2s (6.5% of total)
ival-mult: 1.8s (5.3% of total)
ival-tan: 1.7s (5.1% of total)
ival-sin: 1.4s (4.1% of total)
ival-fmod: 1.3s (3.9% of total)
ival-sqrt: 1.2s (3.6% of total)
ival-div: 1.1s (3.4% of total)
ival-sinh: 1.1s (3.4% of total)
ival-sub: 748.0ms (2.2% of total)
ival-add: 747.0ms (2.2% of total)
ival-acos: 608.0ms (1.8% of total)
ival-<=: 521.0ms (1.5% of total)
ival-pow2: 471.0ms (1.4% of total)
ival-neg: 353.0ms (1% of total)
ival-hypot: 219.0ms (0.7% of total)
ival-==: 167.0ms (0.5% of total)
ival-and: 129.0ms (0.4% of total)
ival-true: 120.0ms (0.4% of total)
ival-assert: 95.0ms (0.3% of total)
exact: 87.0ms (0.3% of total)
ival-atan: 84.0ms (0.2% of total)
ival-<: 67.0ms (0.2% of total)
ival-or: 42.0ms (0.1% of total)
ival->=: 27.0ms (0.1% of total)
ival->: 19.0ms (0.1% of total)
Bogosity

simplify22.2s (18.3%)

Memory
40.8MiB live, 18 667.4MiB allocated; 4.0s collecting garbage
Stop Event
217×iter limit
134×node limit
22×saturated
6×unsound
Counts
3 793 → 3 726

localize12.1s (9.9%)

Memory
125.6MiB live, 12 283.9MiB allocated; 1.8s collecting garbage
Samples
4.4s5 313×1valid
2.2s10 221×0valid
1.7s187×5exit
1.6s1 628×2valid
47.0ms264×0invalid
14.0ms1×1exit
12.0ms50×0exit
Compiler

Compiled 10 936 to 1 728 computations (84.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.1s
ival-mult: 1.3s (15.4% of total)
adjust: 1.2s (14.5% of total)
ival-sin: 1.1s (13.3% of total)
ival-cos: 1.0s (12.3% of total)
ival-div: 615.0ms (7.6% of total)
ival-add: 572.0ms (7% of total)
const: 322.0ms (4% of total)
ival-tan: 288.0ms (3.5% of total)
ival-sub: 283.0ms (3.5% of total)
ival-log: 260.0ms (3.2% of total)
ival-sqrt: 226.0ms (2.8% of total)
ival-pow: 206.0ms (2.5% of total)
ival-exp: 153.0ms (1.9% of total)
ival-pow2: 147.0ms (1.8% of total)
ival-fmod: 132.0ms (1.6% of total)
ival-sinh: 90.0ms (1.1% of total)
ival-neg: 77.0ms (0.9% of total)
ival-hypot: 71.0ms (0.9% of total)
ival-asin: 52.0ms (0.6% of total)
ival-acos: 44.0ms (0.5% of total)
ival-pi: 22.0ms (0.3% of total)
exact: 20.0ms (0.2% of total)
ival-true: 15.0ms (0.2% of total)
ival-cbrt: 12.0ms (0.1% of total)
ival-cosh: 8.0ms (0.1% of total)
ival-assert: 8.0ms (0.1% of total)
ival-atan: 1.0ms (0% of total)

rewrite6.9s (5.6%)

Memory
-107.9MiB live, 6 008.3MiB allocated; 1.7s collecting garbage
Stop Event
211×iter limit
47×node limit
20×unsound
4×saturated
Counts
925 → 14 179

analyze4.2s (3.5%)

Memory
120.4MiB live, 3 990.1MiB allocated; 1.6s collecting garbage
Algorithm
20×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%73.7%26.3%0%0%0%0
28.8%21.3%52.5%26.3%0%0%0%1
44.1%32.5%41.2%26.3%0%0%0%2
52.6%38.7%35%26.3%0%0%0%3
61.9%45.6%28.1%26.3%0%0%0%4
65.2%47.5%25.3%26.3%0%0.9%0%5
66.8%48.4%24%26.3%0%1.2%0%6
71.1%51.1%20.8%26.3%0%1.9%0%7
72.1%51.6%20%26.3%0%2.1%0%8
74.4%53%18.2%26.3%0%2.5%0%9
75.8%53.9%17.2%26.3%0%2.6%0%10
76.6%54.3%16.6%26.3%0%2.8%0%11
77.3%54.8%16.1%26.3%0%2.9%0%12
Compiler

Compiled 279 to 216 computations (22.6% saved)

preprocess4.2s (3.4%)

Memory
133.6MiB live, 3 344.0MiB allocated; 733ms collecting garbage
Stop Event
38×iter limit
29×node limit
13×saturated
Compiler

Compiled 7 537 to 2 896 computations (61.6% saved)

regimes4.1s (3.4%)

Memory
56.1MiB live, 5 060.4MiB allocated; 798ms collecting garbage
Counts
2 600 → 146
Calls

53 calls:

545.0ms
x
488.0ms
a
335.0ms
b
318.0ms
r
184.0ms
(/.f64 (sin.f64 b) (cos.f64 (+.f64 a b)))
Compiler

Compiled 1 640 to 1 879 computations (-14.6% saved)

derivations4.0s (3.3%)

Memory
11.3MiB live, 2 355.2MiB allocated; 432ms collecting garbage
Stop Event
12×fuel
8×done
Compiler

Compiled 2 891 to 853 computations (70.5% saved)

explain3.4s (2.8%)

Memory
-87.2MiB live, 3 746.0MiB allocated; 733ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5630
cos.f64#fsensitivity5060
-.f64#fcancellation3450
sqrt.f64#fuflow-rescue2950
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2560
/.f64(/.f64 (-.f64 x lo) (-.f64 hi lo))n/o2540
↳(-.f64 hi lo)overflow256
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2480
tan.f64(tan.f64 (+.f64 y z))sensitivity1850
pow.f64(pow.f64 l (exp.f64 w))sensitivity11917
*.f64#fn*o400
*.f64#fn*u390
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u230
↳(pow.f64 c #s(literal 2 binary64))overflow71
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow75
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow58
↳(pow.f64 s #s(literal 2 binary64))underflow57
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue190
↳(*.f64 a a)overflow118
↳(*.f64 b b)overflow19
*.f64#fu*o180
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue30
↳(sinh.f64 x)overflow3
↳(/.f64 (sinh.f64 x) x)overflow3
/.f64(/.f64 (-.f64 x lo) (-.f64 hi lo))o/o20
↳(-.f64 x lo)overflow2
↳(-.f64 hi lo)overflow256
Confusion
Predicted +Predicted -
+2171268
-6722009
Precision
0.7636299683432993
Recall
0.8901189011890119
Confusion?
Predicted +Predicted MaybePredicted -
+21710268
-672171992
Precision?
0.759090909090909
Recall?
0.8901189011890119
Freqs
test
numberfreq
02277
12772
270
31
Total Confusion?
Predicted +Predicted MaybePredicted -
+1800
-002
Precision?
1.0
Recall?
1.0
Samples
615.0ms102×5exit
540.0ms6 632×0valid
512.0ms2 450×1valid
389.0ms1 056×2valid
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.5s
ival-cos: 618.0ms (40.1% of total)
adjust: 136.0ms (8.8% of total)
ival-log: 108.0ms (7% of total)
ival-mult: 106.0ms (6.9% of total)
ival-tan: 97.0ms (6.3% of total)
ival-exp: 58.0ms (3.8% of total)
ival-sqrt: 56.0ms (3.6% of total)
ival-acos: 56.0ms (3.6% of total)
ival-add: 49.0ms (3.2% of total)
ival-sub: 44.0ms (2.9% of total)
ival-fmod: 43.0ms (2.8% of total)
ival-sinh: 37.0ms (2.4% of total)
ival-sin: 37.0ms (2.4% of total)
ival-div: 32.0ms (2.1% of total)
ival-pow2: 22.0ms (1.4% of total)
ival-true: 9.0ms (0.6% of total)
ival-hypot: 9.0ms (0.6% of total)
ival-pow: 8.0ms (0.5% of total)
ival-neg: 7.0ms (0.5% of total)
ival-assert: 5.0ms (0.3% of total)
ival-atan: 3.0ms (0.2% of total)
exact: 2.0ms (0.1% of total)

eval3.0s (2.5%)

Memory
100.8MiB live, 3 909.3MiB allocated; 565ms collecting garbage
Compiler

Compiled 686 753 to 77 167 computations (88.8% saved)

series2.7s (2.2%)

Memory
225.3MiB live, 2 856.8MiB allocated; 565ms collecting garbage
Counts
925 → 3 793
Calls

387 calls:

TimeVariablePointExpression
97.0ms
x
@-inf
((log (/ (sinh x) x)) (* (* (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) x) (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) (log (/ (sinh x) x)) (* (* x x) 1/6) (* x x) (log (/ (sinh x) x)) (* (* (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) x) (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) (- (log (sinh x)) (log x)) (log (sinh x)) (sinh x) (log x) (+ (* 1/2835 (* x x)) -1/180))
82.0ms
x
@-inf
((/ (- x lo) (- hi lo)) (+ (* (+ (/ hi lo) 1) (/ (- hi x) lo)) 1) (* (/ hi lo) (/ hi lo)) (/ hi lo) (/ (- x lo) (- hi lo)) (/ (- x lo) hi) (- x lo) (+ (* (/ (- x hi) lo) hi) (- x hi)) (/ (- x lo) (- hi lo)) (- 1 (/ (+ (* (/ (- x hi) lo) hi) (- x hi)) lo)) (/ (+ (* (/ (- x hi) lo) hi) (- x hi)) lo) (+ (* (+ (* (/ lo hi) lo) lo) (/ (/ (- x lo) hi) hi)) (/ (- x lo) hi)) (/ (- x lo) (- hi lo)) (+ (* (/ lo hi) lo) lo) (/ lo hi) (+ (* lo (/ (/ (- x lo) hi) hi)) (/ (+ (- x lo) (* (/ (* (/ (- x lo) hi) lo) hi) lo)) hi)) (+ (- x lo) (* (/ (* (/ (- x lo) hi) lo) hi) lo)) (/ (- x lo) (- hi lo)) (/ (/ (- x lo) hi) hi) (/ (+ (- x lo) (* (/ (* (/ (- x lo) hi) lo) hi) lo)) hi) (/ (* (/ (- x lo) hi) lo) hi))
78.0ms
x
@inf
((/ (- x lo) (- hi lo)) (+ (* (+ (/ hi lo) 1) (/ (- hi x) lo)) 1) (+ (/ hi lo) 1) (/ hi lo) (/ (- x lo) (- hi lo)) (/ (- x lo) (- hi lo)) (- 1 (/ x lo)) (/ x lo) (/ (- x lo) (- hi lo)) (- (/ (- hi x) lo) -1) (/ (- hi x) lo) (- hi x) (+ (* (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo)) (- x lo)) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo)) (- x lo)) hi) (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo))
75.0ms
a
@0
((+ x (- (/ (+ (tan z) (tan y)) (- 1 (/ (* (tan y) (sin z)) (cos z)))) (tan a))) (- (/ (+ (tan z) (tan y)) (- 1 (/ (* (tan y) (sin z)) (cos z)))) (tan a)) (/ (+ (tan z) (tan y)) (- 1 (/ (* (tan y) (sin z)) (cos z)))) (+ (tan z) (tan y)) (+ x (- (tan (+ y z)) (tan a))) (- (+ (/ (sin z) (cos z)) x) (/ (sin a) (cos a))) (- x (/ (sin a) (cos a))) (- x a) (- (+ (tan (+ z y)) x) (tan a)) (+ (tan (+ z y)) x) (tan (+ z y)) (+ z y) (+ x (/ (sin (- (+ z y) a)) (* (cos (+ z y)) (cos a)))) (/ (sin (- (+ z y) a)) (* (cos (+ z y)) (cos a))) (sin (- (+ z y) a)) (- (+ z y) a) (/ (- (pow (+ (tan z) x) 2) (pow (tan a) 2)) (+ (+ (tan z) x) (tan a))) (+ x (- (tan (+ y z)) (tan a))) (- (pow (+ (tan z) x) 2) (pow (tan a) 2)) (pow (+ (tan z) x) 2) (* (tan y) (sin z)) (/ (* (tan y) (sin z)) (cos z)) (tan a) (cos (+ z y)) (* (cos (+ z y)) (cos a)) (pow (tan a) 2))
73.0ms
lo
@0
((/ (- x lo) (- hi lo)) (+ (* (+ (/ hi lo) 1) (/ (- hi x) lo)) 1) (* hi (/ (/ hi lo) lo)) (/ (/ hi lo) lo) (/ (- x lo) (- hi lo)) (/ x hi) (+ (* (/ (- x lo) hi) lo) (- x lo)) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) lo) (- x lo)) hi) (/ (- x lo) hi) (- (/ (+ (* (+ (* (/ lo hi) lo) lo) (/ (- x lo) hi)) x) hi) (/ lo hi)) (/ (- x lo) (- hi lo)) (/ (+ (* (+ (* (/ lo hi) lo) lo) (/ (- x lo) hi)) x) hi) (+ (* (+ (* (/ lo hi) lo) lo) (/ (- x lo) hi)) x) (+ (* (* (/ (- x lo) hi) lo) (/ lo hi)) (+ (* (/ (- x lo) hi) lo) (- x lo))) (/ (+ (* (* (/ (- x lo) hi) lo) (/ lo hi)) (+ (* (/ (- x lo) hi) lo) (- x lo))) hi) (/ (- x lo) (- hi lo)) (+ (* (/ lo hi) lo) lo))

prune2.0s (1.7%)

Memory
-162.5MiB live, 2 918.0MiB allocated; 449ms collecting garbage
Counts
20 234 → 1 513
Compiler

Compiled 81 013 to 42 821 computations (47.1% saved)

bsearch835.0ms (0.7%)

Memory
92.9MiB live, 556.7MiB allocated; 43ms collecting garbage
Algorithm
30×binary-search
9×left-value
Stop Event
29×narrow-enough
1×predicate-same
Samples
380.0ms1 292×1valid
105.0ms1 636×0valid
Compiler

Compiled 8 864 to 7 303 computations (17.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 399.0ms
ival-fmod: 123.0ms (30.8% of total)
ival-tan: 68.0ms (17% of total)
adjust: 45.0ms (11.3% of total)
ival-cos: 40.0ms (10% of total)
ival-add: 28.0ms (7% of total)
ival-sin: 26.0ms (6.5% of total)
ival-mult: 16.0ms (4% of total)
ival-exp: 13.0ms (3.3% of total)
ival-div: 10.0ms (2.5% of total)
ival-pow2: 8.0ms (2% of total)
ival-sqrt: 7.0ms (1.8% of total)
ival-sub: 5.0ms (1.3% of total)
ival-pow: 2.0ms (0.5% of total)
ival-true: 2.0ms (0.5% of total)
ival-neg: 2.0ms (0.5% of total)
ival-assert: 1.0ms (0.3% of total)
ival-log: 1.0ms (0.3% of total)
ival-sinh: 1.0ms (0.3% of total)
exact: 0.0ms (0% of total)

start1.0ms (0%)

Memory
1.5MiB live, 1.5MiB allocated; 0ms collecting garbage

end0.0ms (0%)

Memory
0.3MiB live, 0.2MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...