Herbie run

Date:Wednesday, March 5th, 2025
Commit:141e80a8 on main
Seed:2025064
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:1 060 640.6 MB

Time bar (total: 16.6min)

sample6.1min (36.6%)

Memory
3 484.4MiB live, 373 538.1MiB allocated; 2.4min collecting garbage
Samples
3.7min2 144 775×0valid
23.2s69 466×1valid
9.4s63 622×0invalid
1.8s5 947×2valid
1.4s1 567×5exit
501.0ms1 816×1invalid
200.0ms674×3valid
1.0ms2×4valid
Precisions
Click to see histograms. Total time spent on operations: 2.7min
ival-mult: 54.5s (34.2% of total)
ival-sub: 23.0s (14.4% of total)
ival-add: 19.0s (11.9% of total)
ival-div: 17.1s (10.7% of total)
const: 10.9s (6.8% of total)
ival-log: 8.0s (5% of total)
ival-cos: 6.2s (3.9% of total)
adjust: 5.9s (3.7% of total)
ival-sqrt: 5.4s (3.4% of total)
ival-sin: 3.9s (2.5% of total)
ival-exp: 1.7s (1.1% of total)
exact: 1.4s (0.9% of total)
ival-assert: 776.0ms (0.5% of total)
ival-cosh: 290.0ms (0.2% of total)
ival-sinh: 284.0ms (0.2% of total)
ival-hypot: 271.0ms (0.2% of total)
ival-tan: 251.0ms (0.2% of total)
ival-acos: 182.0ms (0.1% of total)
ival-fabs: 173.0ms (0.1% of total)
ival-tanh: 83.0ms (0.1% of total)
Bogosity

rewrite3.2min (19.3%)

Memory
3 264.5MiB live, 192 322.7MiB allocated; 51.2s collecting garbage
Stop Event
2 222×iter limit
845×node limit
71×unsound
12×saturated
Counts
125 180 → 229 451

derivations1.1min (6.9%)

Memory
-193.0MiB live, 57 216.9MiB allocated; 16.0s collecting garbage
Stop Event
150×fuel
119×done
Compiler

Compiled 137 485 to 18 896 computations (86.3% saved)

preprocess1.1min (6.7%)

Memory
1 991.3MiB live, 64 321.4MiB allocated; 19.9s collecting garbage
Stop Event
538×iter limit
341×node limit
197×saturated
Compiler

Compiled 312 850 to 61 108 computations (80.5% saved)

regimes1.1min (6.5%)

Memory
539.8MiB live, 82 992.9MiB allocated; 16.7s collecting garbage
Counts
32 502 → 4 867
Calls

512 calls:

10.9s
x
8.6s
y
6.9s
z
3.8s
t
2.6s
a
Compiler

Compiled 37 110 to 56 021 computations (-51% saved)

series55.8s (5.6%)

Memory
774.6MiB live, 67 376.3MiB allocated; 17.1s collecting garbage
Counts
18 729 → 106 451
Calls

8886 calls:

TimeVariablePointExpression
1.4s
y
@0
((+ (* y x) (* (- 1 y) z)) (* (- x z) y) (- x z) x z y)
462.0ms
x
@0
((- (- (* x (+ (log (pow y 1/2)) (log (pow y 1/2)))) z) y) (- (* x (+ (log (pow y 1/2)) (log (pow y 1/2)))) z) (* x (+ (log (pow y 1/2)) (log (pow y 1/2)))) x (+ (log (pow y 1/2)) (log (pow y 1/2))) (log (pow y 1/2)) (pow y 1/2) y 1/2 z (- (- (* x (log y)) z) y) (neg y) (- (- (* x (log y)) z) y) (- (* x (log y)) z) (neg z) (- (- (* x (log y)) z) y) (- (* (log y) x) z) (* (log y) x) (log y) (- (- (* x (log y)) z) y) (- (* x (log y)) z))
252.0ms
z
@-inf
((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log t) t (- a 1/2) a 1/2 (neg (neg (log z))) (neg (log z)) (log z) z (log (+ y x)) (+ y x) y x (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (log t) a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* x z) (pow t (- a 1/2)))) t) (+ (* (log t) (- a 1/2)) (log (* z x))) (log (* z x)) (* z x) (+ (* (- a 1/2) (log t)) (- (log (* z (+ y x))) t)) (- (log (* z (+ y x))) t) (log (* z (+ y x))) (* z (+ y x)) (+ y x) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (+ x y) (* (- a 1/2) (log t)))
197.0ms
x
@0
((* (neg x) (log (/ y x))) (neg x) x (log (/ y x)) (/ y x) y (* x (- (log x) (log y))) (- (log x) (log y)) (log x) (log y) (+ (* (log (neg x)) x) (* (neg (neg (log (/ -1 y)))) x)) (log (neg x)) (* (neg (neg (log (/ -1 y)))) x) (neg (neg (log (/ -1 y)))) (neg (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) -1 (* x (/ (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (pow (log x) 2)) (- (log (* (/ -1 y) -1)) (log x)))) (/ (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (pow (log x) 2)) (- (log (* (/ -1 y) -1)) (log x))) (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (pow (log x) 2)) (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (log (* (/ -1 y) -1)) (* (/ -1 y) -1) (pow (log x) 2) 2 (- (log (* (/ -1 y) -1)) (log x)) (+ (* (/ (neg (pow (log y) 3)) (+ (* (log x) (log (* x y))) (pow (log y) 2))) x) (* (/ (pow (log x) 3) (+ (* (log x) (log (* x y))) (pow (log y) 2))) x)) (* (/ (neg (pow (log y) 3)) (+ (* (log x) (log (* x y))) (pow (log y) 2))) x) (/ (neg (pow (log y) 3)) (+ (* (log x) (log (* x y))) (pow (log y) 2))) (neg (pow (log y) 3)) (pow (log y) 3) 3 (+ (* (log x) (log (* x y))) (pow (log y) 2)) (log (* x y)) (* x y) (pow (log y) 2) (* (/ (pow (log x) 3) (+ (* (log x) (log (* x y))) (pow (log y) 2))) x) (/ (pow (log x) 3) (+ (* (log x) (log (* x y))) (pow (log y) 2))) (pow (log x) 3))
154.0ms
x
@-inf
((/ (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) y) (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) (- (+ (* y (log z)) (* (- t 1) (log a))) b) (+ (* y (log z)) (* (- t 1) (log a))) (* y (log z)) y (log z) z (* (- t 1) (log a)) (- t 1) t 1 (log a) a b)

eval47.0s (4.7%)

Memory
-152.6MiB live, 59 059.7MiB allocated; 16.7s collecting garbage
Compiler

Compiled 9 419 222 to 1 000 933 computations (89.4% saved)

explain40.6s (4.1%)

Memory
-64.6MiB live, 50 279.2MiB allocated; 10.2s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15851
/.f64#fo/n13300
sqrt.f64#foflow-rescue7860
/.f64#fo/o5890
-.f64#fcancellation5538
*.f64#fn*o5360
+.f64#fnan-rescue4830
-.f64#fnan-rescue4460
cos.f64#fsensitivity3550
/.f64#fn/o3470
+.f64#fcancellation3080
/.f64#fu/n2710
sin.f64#fsensitivity2261
*.f64#fn*u1790
cos.f64#foflow-rescue1450
/.f64#fn/u1280
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity971
log.f64#foflow-rescue930
/.f64#fu/u780
log.f64#fuflow-rescue680
sqrt.f64#fuflow-rescue470
exp.f64(exp.f64 (-.f64 (+.f64 (*.f64 y (log.f64 z)) (*.f64 (-.f64 t #s(literal 1 binary64)) (log.f64 a))) b))sensitivity343
*.f64#fo*u310
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue290
↳(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow29
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue290
↳(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow29
Confusion
Predicted +Predicted -
+6106196
-173960823
Precision
0.7783301465901848
Recall
0.9688987622976832
Confusion?
Predicted +Predicted MaybePredicted -
+61063193
-1739960814
Precision?
0.777523227695049
Recall?
0.9693748016502698
Freqs
test
numberfreq
061019
17029
2731
361
421
53
Total Confusion?
Predicted +Predicted MaybePredicted -
+13200
-00137
Precision?
1.0
Recall?
1.0
Samples
12.8s130 474×0valid
2.1s5 888×1valid
824.0ms1 274×2valid
27.0ms92×3valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 9.1s
ival-mult: 2.8s (30.5% of total)
ival-add: 1.2s (13.5% of total)
ival-sub: 1.1s (12.2% of total)
ival-div: 1.0s (11.1% of total)
ival-log: 893.0ms (9.8% of total)
adjust: 626.0ms (6.9% of total)
const: 443.0ms (4.9% of total)
ival-sin: 244.0ms (2.7% of total)
ival-sqrt: 175.0ms (1.9% of total)
ival-cos: 165.0ms (1.8% of total)
ival-true: 121.0ms (1.3% of total)
ival-exp: 88.0ms (1% of total)
exact: 67.0ms (0.7% of total)
ival-assert: 58.0ms (0.6% of total)
ival-sinh: 38.0ms (0.4% of total)
ival-cosh: 12.0ms (0.1% of total)
ival-tan: 11.0ms (0.1% of total)
ival-fabs: 11.0ms (0.1% of total)
ival-hypot: 9.0ms (0.1% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-acos: 5.0ms (0.1% of total)

bsearch33.6s (3.4%)

Memory
62.5MiB live, 40 256.3MiB allocated; 8.0s collecting garbage
Algorithm
1 730×binary-search
1 060×left-value
Stop Event
1 700×narrow-enough
30×predicate-same
Samples
18.4s146 734×0valid
1.1s4 126×1valid
409.0ms3 426×0invalid
46.0ms201×2valid
7.0ms27×3valid
6.0ms25×1invalid
Compiler

Compiled 927 929 to 672 543 computations (27.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.5s
ival-mult: 5.6s (41.3% of total)
ival-sub: 2.2s (16.1% of total)
ival-add: 1.9s (13.8% of total)
ival-div: 1.2s (8.8% of total)
const: 645.0ms (4.8% of total)
ival-log: 530.0ms (3.9% of total)
ival-sin: 372.0ms (2.8% of total)
adjust: 338.0ms (2.5% of total)
ival-cos: 246.0ms (1.8% of total)
ival-sqrt: 129.0ms (1% of total)
ival-true: 123.0ms (0.9% of total)
ival-exp: 105.0ms (0.8% of total)
ival-assert: 65.0ms (0.5% of total)
exact: 63.0ms (0.5% of total)
ival-sinh: 59.0ms (0.4% of total)
ival-cosh: 15.0ms (0.1% of total)
ival-tanh: 8.0ms (0.1% of total)
ival-fabs: 7.0ms (0.1% of total)

prune25.1s (2.5%)

Memory
-1 560.6MiB live, 37 064.7MiB allocated; 7.5s collecting garbage
Counts
253 974 → 12 270
Compiler

Compiled 759 593 to 416 513 computations (45.2% saved)

analyze23.7s (2.4%)

Memory
341.9MiB live, 22 933.3MiB allocated; 10.4s collecting garbage
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)

simplify14.8s (1.5%)

Memory
-476.7MiB live, 13 254.9MiB allocated; 3.3s collecting garbage
Stop Event
202×node limit
67×saturated

start43.0ms (0%)

Memory
-40.0MiB live, 19.1MiB allocated; 35ms collecting garbage

end2.0ms (0%)

Memory
5.2MiB live, 4.9MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...