Herbie run

Date:Friday, September 27th, 2024
Commit:c2e5e391 on varun10p-identities
Hostname:nightly with Racket 8.10
Seed:2024271
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: 57.6s)

sample12.3s (21.3%)

Memory
296.1MiB live, 12 382.1MiB allocated
Samples
8.2s70 194×0valid
777.0ms4 101×2valid
349.0ms1 878×0invalid
1.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 6.4s
ival-mult: 2.2s (34.2% of total)
ival-div: 1.4s (22.4% of total)
ival-sub: 648.0ms (10.2% of total)
ival-add: 511.0ms (8% of total)
ival-sqrt: 435.0ms (6.8% of total)
ival-neg: 245.0ms (3.8% of total)
ival-fabs: 232.0ms (3.6% of total)
ival-if: 123.0ms (1.9% of total)
ival->=: 119.0ms (1.9% of total)
ival-log: 118.0ms (1.8% of total)
adjust: 116.0ms (1.8% of total)
ival-exp: 78.0ms (1.2% of total)
exact: 57.0ms (0.9% of total)
ival-true: 56.0ms (0.9% of total)
ival-assert: 29.0ms (0.5% of total)
Bogosity

simplify9.8s (17%)

Memory
59.5MiB live, 7 616.9MiB allocated
Algorithm
69×egg-herbie
Stop Event
88×iter limit
43×node limit
28×saturated
Counts
8 664 → 8 503

soundness7.3s (12.7%)

Memory
7.5MiB live, 3 551.7MiB allocated
Stop Event
49×iter limit
31×node limit
done
fuel
saturated
Compiler

Compiled 8 340 to 4 051 computations (51.4% saved)

eval6.8s (11.8%)

Memory
167.4MiB live, 9 218.6MiB allocated
Compiler

Compiled 1 075 984 to 80 094 computations (92.6% saved)

rewrite6.7s (11.6%)

Memory
-177.4MiB live, 6 469.1MiB allocated
Stop Event
64×iter limit
28×node limit
unsound
saturated
Counts
317 → 15 441

localize4.5s (7.8%)

Memory
90.0MiB live, 4 306.1MiB allocated
Samples
1.3s906×2valid
1.0s6 071×0valid
699.0ms582×1valid
149.0ms121×3valid
Compiler

Compiled 12 215 to 1 315 computations (89.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.1s
ival-mult: 600.0ms (28% of total)
ival-div: 441.0ms (20.5% of total)
ival-add: 381.0ms (17.7% of total)
ival-sub: 185.0ms (8.6% of total)
adjust: 146.0ms (6.8% of total)
ival->=: 103.0ms (4.8% of total)
ival-sqrt: 96.0ms (4.5% of total)
ival-if: 65.0ms (3% of total)
ival-exp: 35.0ms (1.6% of total)
ival-neg: 33.0ms (1.5% of total)
ival-log: 21.0ms (1% of total)
ival-fabs: 17.0ms (0.8% of total)
exact: 11.0ms (0.5% of total)
ival-true: 7.0ms (0.3% of total)
ival-assert: 3.0ms (0.1% of total)

prune2.3s (4%)

Memory
-27.2MiB live, 3 279.3MiB allocated
Counts
30 101 → 289
Compiler

Compiled 13 251 to 7 601 computations (42.6% saved)

preprocess2.0s (3.4%)

Memory
29.3MiB live, 1 392.5MiB allocated
Algorithm
egg-herbie
Stop Event
18×iter limit
13×saturated
node limit
Compiler

Compiled 5 607 to 1 214 computations (78.3% saved)

explain1.6s (2.8%)

Memory
18.5MiB live, 1 933.1MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2730
+.f64#fcancellation1330
-.f64#fcancellation980
sqrt.f64#fuflow-rescue840
/.f64#fu/n310
/.f64#fn/u210
-.f64#fnan-rescue190
*.f64(*.f64 (/.f64 x y) z)n*o90
*.f64(*.f64 (/.f64 x y) z)n*u60
Confusion
Predicted +Predicted -
+30610
-2271761
Precision
0.574108818011257
Recall
0.9683544303797469
Confusion?
Predicted +Predicted MaybePredicted -
+306010
-22701761
Precision?
0.574108818011257
Recall?
0.9683544303797469
Freqs
test
numberfreq
01771
1398
2129
36
Total Confusion?
Predicted +Predicted MaybePredicted -
+400
-005
Precision?
1.0
Recall?
1.0
Samples
282.0ms3 684×0valid
203.0ms570×2valid
74.0ms296×1valid
29.0ms58×3valid
Compiler

Compiled 1 575 to 388 computations (75.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 372.0ms
ival-div: 87.0ms (23.4% of total)
ival-mult: 71.0ms (19.1% of total)
ival-sub: 65.0ms (17.5% of total)
adjust: 37.0ms (10% of total)
ival-sqrt: 34.0ms (9.2% of total)
ival-add: 23.0ms (6.2% of total)
ival-if: 15.0ms (4% of total)
ival-neg: 11.0ms (3% of total)
ival-log: 7.0ms (1.9% of total)
ival-fabs: 5.0ms (1.3% of total)
ival-exp: 4.0ms (1.1% of total)
ival-true: 4.0ms (1.1% of total)
exact: 4.0ms (1.1% of total)
ival->=: 3.0ms (0.8% of total)
ival-assert: 2.0ms (0.5% of total)

series1.5s (2.6%)

Memory
-91.9MiB live, 1 301.7MiB allocated
Counts
317 → 8 664
Calls

180 calls:

TimeVariablePointExpression
59.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) (neg (log (- (/ 1 x) 1))) (+ (log x) x) (neg (log (- (/ 1 x) 1))) (+ (* (+ (* 1/2 x) 1) x) (log x)) (+ (* 1/2 x) 1))
50.0ms
a
@0
((if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (/ 2 (- (sqrt (+ (* b b) (* a (* c -4)))) b)) c)) (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (/ c b) (/ b a)) (if (>= b 0) (* (/ 1/2 a) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (* 2 c) (- (sqrt (- (* b b) (* (* 4 a) c))) b))) (* (/ 1/2 a) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ 1/2 a) (/ (+ (* a (/ c b)) (neg b)) a) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (+ (sqrt (+ (* (* -4 c) a) (* b b))) b) (/ -1/2 a)) (+ (sqrt (+ (* (* -4 c) a) (* b b))) b) (/ (- (neg b) (/ 1 (sqrt (/ 1 (+ (* (* -4 c) a) (* b b)))))) (* 2 a)) (- (neg b) (/ 1 (sqrt (/ 1 (+ (* (* -4 c) a) (* b b)))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (* b b) (* (* 4 a) c)) (sqrt (+ (* b b) (* a (* c -4)))) (- (sqrt (+ (* b b) (* a (* c -4)))) b) (* (/ 2 (- (sqrt (+ (* b b) (* a (* c -4)))) b)) c) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (sqrt (- (* b b) (* (* 4 a) c))) b) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (sqrt (+ (* (* -4 c) a) (* b b))) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (/ 1 (+ (* (* -4 c) a) (* b b)))))
49.0ms
c
@0
((/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (* b b) (* (* 4 a) c)) (>= b 0) (if (>= b 0) (* (/ -2 (- (sqrt (+ (* (* -4 c) a) (* b b))) b)) c) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (- 0 (* (- (sqrt (+ (* (* -4 c) a) (* b b))) b) (/ -1/2 a))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ 1 (* (/ 1/2 c) (- b (sqrt (+ (* (* -4 c) a) (* b b)))))) (* (neg b) (+ (* (* (/ a b) -2) (/ c b)) 1)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (+ (* (* -4 c) a) (* b b))) (- (sqrt (+ (* (* -4 c) a) (* b b))) b) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- b (sqrt (+ (* (* -4 c) a) (* b b)))) (sqrt (- (* b b) (* (* 4 a) c))))
42.0ms
c
@0
((/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (+ (* b b) (* (* -4 c) a)))) (>= b 0) (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (* -2 c) (- (sqrt (+ (* (* -4 c) a) (* b b))) b)) (* (/ 1/2 a) (- (sqrt (+ (* (* -4 c) a) (* b b))) b))) (/ (* -2 c) (- (sqrt (+ (* (* -4 c) a) (* b b))) b)) (* -2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (* b b) (* (* 4 a) c)) (if (>= b 0) (/ 1 (* (/ 1/2 c) (- b (sqrt (+ (* (* -4 c) a) (* b b)))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (* (neg b) (+ (* (* (/ a b) -2) (/ c b)) 2)) (/ 1 (* (/ 1/2 c) (- b (sqrt (+ (* (* -4 c) a) (* b b)))))) (* (/ 1/2 c) (- b (sqrt (+ (* (* -4 c) a) (* b b))))) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (+ (* b b) (* (* -4 c) a))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (+ (* (* -4 c) a) (* b b))) (- (sqrt (+ (* (* -4 c) a) (* b b))) b) (* (/ 1/2 a) (- (sqrt (+ (* (* -4 c) a) (* b b))) b)) (/ 1 (* (/ 1/2 c) (- b (sqrt (+ (* (* -4 c) a) (* b b)))))) (sqrt (- (* b b) (* (* 4 a) c))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- b (sqrt (+ (* (* -4 c) a) (* b b)))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)))
33.0ms
a
@inf
((+ (neg b) (sqrt (+ (* b b) (* (* -4 c) a)))) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (+ (* b b) (* (* -4 c) a)))))) (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (- (/ c (* b b)) (/ 1 a)) b) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* c (/ 2 (- (sqrt (+ (* (* -4 c) a) (* b b))) b)))) (- (/ c b) (/ b a)) (+ (* (/ b a) -1/2) (* (sqrt (+ (* (* -4 c) a) (* b b))) (/ -1/2 a))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (* b b) (* (* 4 a) c)) (sqrt (+ (* b b) (* (* -4 c) a))) (/ (* 2 c) (+ (neg b) (sqrt (+ (* b b) (* (* -4 c) a))))) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ c (* b b)) (sqrt (+ (* (* -4 c) a) (* b b))) (- (sqrt (+ (* (* -4 c) a) (* b b))) b) (* c (/ 2 (- (sqrt (+ (* (* -4 c) a) (* b b))) b))) (sqrt (- (* b b) (* (* 4 a) c))))

regimes1.4s (2.4%)

Memory
32.3MiB live, 1 581.3MiB allocated
Counts
788 → 126
Calls

26 calls:

238.0ms
n
202.0ms
b
148.0ms
a
148.0ms
x
124.0ms
z
Compiler

Compiled 1 047 to 892 computations (14.8% saved)

bsearch915.0ms (1.6%)

Memory
-66.3MiB live, 797.8MiB allocated
Algorithm
62×binary-search
left-value
Stop Event
55×narrow-enough
predicate-same
Samples
438.0ms3 264×0valid
50.0ms353×0invalid
4.0ms32×2valid
Compiler

Compiled 22 332 to 17 154 computations (23.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 263.0ms
ival-mult: 110.0ms (41.7% of total)
ival-div: 55.0ms (20.9% of total)
ival-sub: 26.0ms (9.9% of total)
ival-add: 17.0ms (6.5% of total)
ival-sqrt: 16.0ms (6.1% of total)
ival-neg: 10.0ms (3.8% of total)
ival-if: 9.0ms (3.4% of total)
ival->=: 7.0ms (2.7% of total)
ival-fabs: 5.0ms (1.9% of total)
exact: 4.0ms (1.5% of total)
ival-true: 3.0ms (1.1% of total)
ival-exp: 2.0ms (0.8% of total)
adjust: 1.0ms (0.4% of total)
ival-assert: 1.0ms (0.4% of total)

analyze499.0ms (0.9%)

Memory
-67.8MiB live, 544.6MiB allocated
Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
22.2%22.2%77.7%0.1%0%0%0%1
29.4%27.8%66.6%0.1%0%5.6%0%2
50%44.4%44.4%0.1%0%11.1%0%3
59.7%51.3%34.7%0.1%0%13.9%0%4
67.2%56.9%27.7%0.1%0%15.3%0%5
74.4%62.4%21.5%0.1%0%16%0%6
78.9%64.9%17.3%0.1%0%17.7%0%7
80.8%66.3%15.8%0.1%0%17.9%0%8
85.9%69.9%11.5%0.1%0%18.5%0%9
88%70.7%9.7%0.1%0%19.6%0%10
90%72.1%8%0.1%0%19.8%0%11
92.3%73.5%6.2%0.1%0%20.3%0%12
Compiler

Compiled 153 to 106 computations (30.7% saved)

start0.0ms (0%)

Memory
0.6MiB live, 0.6MiB allocated

end0.0ms (0%)

Memory
0.2MiB live, 0.2MiB allocated

Profiling

Loading profile data...