Herbie run

Date:Sunday, March 2nd, 2025
Commit:141e80a8 on main
Seed:2025061
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:86 075.2 MB

Time bar (total: 1.5min)

sample48.3s (54.6%)

Memory
528.4MiB live, 45 766.8MiB allocated; 14.8s collecting garbage
Samples
14.2s16 648×5exit
9.7s39 913×1valid
8.7s108 791×0valid
6.7s16 416×2valid
455.0ms3 852×0invalid
141.0ms1 395×0exit
Precisions
Click to see histograms. Total time spent on operations: 31.4s
adjust: 4.1s (12.9% of total)
ival-exp: 3.8s (12% of total)
ival-pow: 3.7s (11.9% of total)
ival-log: 3.4s (10.9% of total)
ival-cos: 2.4s (7.7% of total)
ival-mult: 1.7s (5.5% of total)
ival-div: 1.7s (5.5% of total)
ival-tan: 1.5s (4.6% of total)
ival-sinh: 1.4s (4.5% of total)
ival-sub: 1.3s (4.1% of total)
ival-sqrt: 1.2s (3.8% of total)
ival-fmod: 1.0s (3.3% of total)
ival-add: 812.0ms (2.6% of total)
ival-sin: 791.0ms (2.5% of total)
ival-hypot: 527.0ms (1.7% of total)
ival-acos: 495.0ms (1.6% of total)
const: 461.0ms (1.5% of total)
ival-pow2: 459.0ms (1.5% of total)
ival-neg: 273.0ms (0.9% of total)
ival-<=: 101.0ms (0.3% of total)
ival-assert: 75.0ms (0.2% of total)
ival-atan: 56.0ms (0.2% of total)
exact: 41.0ms (0.1% of total)
ival-and: 39.0ms (0.1% of total)
ival-or: 19.0ms (0.1% of total)
ival->: 2.0ms (0% of total)
ival-==: 2.0ms (0% of total)
ival-<: 2.0ms (0% of total)
Bogosity

rewrite10.4s (11.8%)

Memory
181.1MiB live, 9 356.1MiB allocated; 1.8s collecting garbage
Stop Event
194×iter limit
51×node limit
16×unsound
4×saturated
Counts
7 618 → 17 981

regimes5.3s (6%)

Memory
151.8MiB live, 6 747.9MiB allocated; 933ms collecting garbage
Counts
3 548 → 177
Calls

53 calls:

620.0ms
a
525.0ms
x
376.0ms
r
355.0ms
b
319.0ms
z
Compiler

Compiled 1 702 to 2 075 computations (-21.9% saved)

preprocess4.4s (5%)

Memory
20.5MiB live, 3 831.7MiB allocated; 875ms collecting garbage
Stop Event
38×iter limit
29×node limit
13×saturated
Compiler

Compiled 8 249 to 2 984 computations (63.8% saved)

eval3.6s (4.1%)

Memory
-184.1MiB live, 3 981.7MiB allocated; 1.3s collecting garbage
Compiler

Compiled 699 155 to 80 609 computations (88.5% saved)

derivations3.3s (3.8%)

Memory
-9.6MiB live, 2 461.3MiB allocated; 949ms collecting garbage
Stop Event
12×fuel
8×done
Compiler

Compiled 3 305 to 911 computations (72.4% saved)

explain3.2s (3.7%)

Memory
227.9MiB live, 3 425.9MiB allocated; 606ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5850
cos.f64#fsensitivity4950
sqrt.f64#fuflow-rescue3330
-.f64#fcancellation3272
/.f64#fn/o2570
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2532
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2520
tan.f64(tan.f64 (+.f64 y z))sensitivity1920
pow.f64(pow.f64 l (exp.f64 w))sensitivity12911
*.f64#fn*u370
*.f64#fn*o310
*.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))overflow76
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow72
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow61
↳(pow.f64 s #s(literal 2 binary64))underflow61
*.f64#fu*o150
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue120
↳(*.f64 a a)overflow129
↳(*.f64 b b)overflow12
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue40
↳(sinh.f64 x)overflow4
↳(/.f64 (sinh.f64 x) x)overflow4
+.f64(+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a)))cancellation11
Confusion
Predicted +Predicted -
+2205272
-6791964
Precision
0.7645631067961165
Recall
0.8901897456600727
Confusion?
Predicted +Predicted MaybePredicted -
+22052270
-679141950
Precision?
0.7610344827586207
Recall?
0.8909971740008075
Freqs
test
numberfreq
02236
12823
260
31
Total Confusion?
Predicted +Predicted MaybePredicted -
+1800
-002
Precision?
1.0
Recall?
1.0
Samples
634.0ms112×5exit
588.0ms2 418×1valid
438.0ms6 672×0valid
356.0ms1 038×2valid
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.6s
ival-cos: 624.0ms (38.8% of total)
adjust: 146.0ms (9.1% of total)
ival-add: 130.0ms (8.1% of total)
ival-sqrt: 88.0ms (5.5% of total)
ival-log: 87.0ms (5.4% of total)
ival-tan: 75.0ms (4.7% of total)
ival-mult: 73.0ms (4.5% of total)
ival-sin: 71.0ms (4.4% of total)
ival-exp: 52.0ms (3.2% of total)
ival-sinh: 46.0ms (2.9% of total)
ival-sub: 44.0ms (2.7% of total)
ival-fmod: 41.0ms (2.6% of total)
ival-div: 36.0ms (2.2% of total)
ival-acos: 32.0ms (2% of total)
ival-pow2: 21.0ms (1.3% of total)
ival-true: 9.0ms (0.6% of total)
ival-pow: 8.0ms (0.5% of total)
ival-hypot: 8.0ms (0.5% of total)
ival-neg: 7.0ms (0.4% 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)

analyze3.2s (3.6%)

Memory
34.6MiB live, 2 804.0MiB allocated; 1.2s 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)

series2.7s (3.1%)

Memory
169.8MiB live, 2 988.1MiB allocated; 693ms collecting garbage
Counts
1 425 → 6 193
Calls

387 calls:

TimeVariablePointExpression
100.0ms
x
@0
((/ (+ (* (asin (- 1 x)) (asin (+ -1 x))) (pow (/ (PI) 2) 2)) (+ (/ (PI) 2) (asin (- 1 x)))) (+ (* (asin (- 1 x)) (asin (+ -1 x))) (pow (/ (PI) 2) 2)) (asin (- 1 x)) (- 1 x) 1 x (asin (+ -1 x)) (+ -1 x) -1 (pow (/ (PI) 2) 2) (/ (PI) 2) (PI) 2 (+ (/ (PI) 2) (asin (- 1 x))) (- (/ (PI) 2) (asin (- 1 x))) (- (* 1/2 (PI)) (asin (- 1 x))) (* 1/2 (PI)) 1/2 (- (/ (PI) 2) (/ 1 (pow (asin (- 1 x)) -1))) (/ 1 (pow (asin (- 1 x)) -1)) (pow (asin (- 1 x)) -1) (- (/ (PI) 2) (asin (- 1 x))) (asin (- 1 x)) (- 1 x) (* (- (exp (* (log x) -1)) 1) x) (- (exp (* (log x) -1)) 1) (* (log x) -1) (log x) (- (/ (PI) 2) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2))) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2)) (pow (asin (- 1 x)) 1/2))
89.0ms
hi
@inf
((/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (/ (+ 1 (pow (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 3)) (+ 1 (- (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (* 1 (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)))))) (+ 1 (pow (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 3)) 1 (pow (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 3) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo) (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) (+ (* (/ (- x hi) lo) hi) (neg hi)) (/ (- x hi) lo) (- x hi) x hi lo (neg hi) 3 (+ 1 (- (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (* 1 (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))))) (- (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (* 1 (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)))) (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (* 1 (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo) (/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) (neg (/ (+ (* hi (/ (- x hi) lo)) x) lo)) (/ (+ (* hi (/ (- x hi) lo)) x) lo) (+ (* hi (/ (- x hi) lo)) x) (/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (+ (* (/ (+ (+ (* hi (/ (- x hi) lo)) (neg hi)) x) lo) -1) 1) (/ (+ (+ (* hi (/ (- x hi) lo)) (neg hi)) x) lo) (+ (+ (* hi (/ (- x hi) lo)) (neg hi)) x) (+ (* hi (/ (- x hi) lo)) (neg hi)) (/ (- x hi) lo) (* (- (/ (/ x hi) lo) (pow lo -1)) hi) (- (/ (/ x hi) lo) (pow lo -1)) (/ (/ x hi) lo) (/ x hi) (pow lo -1) -1 (/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (/ (+ (pow (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 3) 1) (+ (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (- 1 (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 1)))) (+ (pow (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 3) 1) (+ (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo))) (- 1 (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 1))) (- 1 (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 1)) (* (neg (/ (+ (+ (* (/ (- x hi) lo) hi) (neg hi)) x) lo)) 1))
75.0ms
b
@-inf
((* r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a))))) r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (sin b) b (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (cos b) (cos a) a (* (sin b) (sin a)) (sin a) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (tan b) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (cos (+ a b)) (+ a b) (* r (/ (sin b) (sin (+ (neg (+ a b)) (/ (PI) 2))))) (/ (sin b) (sin (+ (neg (+ a b)) (/ (PI) 2)))) (sin (+ (neg (+ a b)) (/ (PI) 2))) (+ (neg (+ a b)) (/ (PI) 2)) (neg (+ a b)) (+ a b) (/ (PI) 2) (PI) 2 (* r (/ (exp (* (log (sin b)) 1)) (cos (+ a b)))) (/ (exp (* (log (sin b)) 1)) (cos (+ a b))) (exp (* (log (sin b)) 1)) (* (log (sin b)) 1) (log (sin b)) 1 (cos (+ a b)))
66.0ms
x
@0
((* (pow x 1/2) (pow (* 2 x) 1/2)) (pow x 1/2) x 1/2 (pow (* 2 x) 1/2) (* 2 x) 2 (sqrt (+ (* x x) (* x x))) (+ (* x x) (* x x)) (sqrt (+ (* x x) (* x x))) (* (sqrt 2) x) (sqrt 2) (* (sqrt x) (sqrt (* 2 x))) (sqrt x) (sqrt (* 2 x)) (sqrt (+ (* x x) (exp (* (log x) 2)))) (+ (* x x) (exp (* (log x) 2))) (* x x) (exp (* (log x) 2)) (* (log x) 2) (log x))
58.0ms
l
@0
((* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) w (pow l (exp w)) (pow (pow l (neg (exp w))) -1) (pow l (neg (exp w))) l (neg (exp w)) (exp w) -1 (* (exp (neg w)) (pow l (exp w))) (* (exp (neg w)) (pow l (exp w))) (+ (* (+ (* (log l) l) (neg l)) w) l) (+ (* (log l) l) (neg l)) (log l) (neg l) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) 1 (pow l (exp w)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ (* (+ (* (+ (* -1/6 w) 1/2) w) -1) w) 1) (+ (* (+ (* -1/6 w) 1/2) w) -1) (+ (* -1/6 w) 1/2) -1/6 1/2)

prune2.0s (2.3%)

Memory
-162.0MiB live, 2 829.7MiB allocated; 573ms collecting garbage
Counts
20 868 → 1 367
Compiler

Compiled 70 782 to 37 907 computations (46.4% saved)

bsearch1.2s (1.3%)

Memory
59.6MiB live, 1 149.4MiB allocated; 156ms collecting garbage
Algorithm
48×binary-search
7×left-value
Stop Event
46×narrow-enough
2×predicate-same
Samples
488.0ms1 838×1valid
171.0ms2 098×0valid
137.0ms144×2valid
Compiler

Compiled 15 142 to 12 502 computations (17.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 641.0ms
ival-tan: 210.0ms (32.7% of total)
ival-exp: 122.0ms (19% of total)
adjust: 87.0ms (13.6% of total)
ival-cos: 53.0ms (8.3% of total)
ival-add: 40.0ms (6.2% of total)
ival-mult: 28.0ms (4.4% of total)
ival-sub: 21.0ms (3.3% of total)
ival-sin: 18.0ms (2.8% of total)
ival-fmod: 16.0ms (2.5% of total)
ival-div: 15.0ms (2.3% of total)
ival-pow2: 10.0ms (1.6% of total)
ival-pow: 7.0ms (1.1% of total)
ival-sqrt: 6.0ms (0.9% of total)
ival-true: 3.0ms (0.5% of total)
ival-neg: 3.0ms (0.5% of total)
ival-assert: 2.0ms (0.3% of total)
exact: 0.0ms (0% of total)

simplify826.0ms (0.9%)

Memory
-129.8MiB live, 730.8MiB allocated; 99ms collecting garbage
Stop Event
15×node limit
5×saturated

start1.0ms (0%)

Memory
1.7MiB live, 1.6MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...