logs (example 3.8)

Time bar (total: 20.9s)

analyze3.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%23.7%76.3%0%0%0%0
0%0%23.7%76.3%0%0%0%1
50%11.9%11.9%76.3%0%0%0%2
75%17.8%5.9%76.3%0%0%0%3
87.5%20.8%3%76.3%0%0%0%4
93.8%22.2%1.5%76.3%0%0%0%5
96.9%23%0.7%76.3%0%0%0%6
98.4%23.3%0.4%76.3%0%0%0%7
99.2%23.5%0.2%76.3%0%0%0%8
99.6%23.6%0.1%76.3%0%0%0%9
99.8%23.7%0%76.3%0%0%0%10
99.9%23.7%0%76.3%0%0%0%11
100%23.7%0%76.3%0%0%0%12
Compiler

Compiled 19 to 14 computations (26.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.0ms
Operation ival-log, time spent: 1.0ms, 58.0% of total-time
Operation ival-sub, time spent: 0.0ms, 0.0% of total-time
Operation const, time spent: 0.0ms, 0.0% of total-time
Operation ival-mult, time spent: 0.0ms, 0.0% of total-time
Operation ival-add, time spent: 0.0ms, 0.0% of total-time
Operation ival->, time spent: 0.0ms, 0.0% of total-time

sample9.9s (47.5%)

Results
7.6s5407×1valid
1.7s2848×0valid
1.0ms0valid
Precisions
Click to see histograms. Total time spent on operations: 7.4s
Operation ival-log, time spent: 2.6s, 36.0% of total-time
Operation ival-add, time spent: 1.8s, 24.0% of total-time
Operation ival-sub, time spent: 1.6s, 22.0% of total-time
Operation ival-mult, time spent: 696.0ms, 9.0% of total-time
Operation ival->, time spent: 511.0ms, 7.0% of total-time
Operation const, time spent: 131.0ms, 2.0% of total-time
Bogosity

preprocess4.5s (21.5%)

Algorithm
egg-herbie
Rules
2386×associate--l+
1216×sub-neg
1060×unsub-neg
966×fma-neg
808×distribute-neg-in
FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
00-0-(log.f64 (+.f64 n 1))
00-0-(+.f64 n 1)
00-0-(*.f64 n (log.f64 n))
00-0-(log.f64 n)
00-0-(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n)))
00-0-(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
00-0-(*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1)))
00-0-1
00-0-n
Iterations

Useful iterations: 4 (0.0ms)

IterNodesCost
023256
161208
2163200
3523200
42076196
54562196
65650196
76508196
86954196
97137196
107152196
117155196
127155196
137158196
147212196
157212196
Stop Event
node limit
Calls
Call 1
Inputs
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
(-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) 1) (log.f64 (+.f64 (neg.f64 n) 1))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) 1)
(neg.f64 (-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) 1) (log.f64 (+.f64 (neg.f64 n) 1))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) 1))
Outputs
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
(-.f64 (*.f64 (+.f64 n 1) (log1p.f64 n)) (fma.f64 n (log.f64 n) 1))
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
(-.f64 (*.f64 (+.f64 n 1) (log1p.f64 n)) (fma.f64 n (log.f64 n) 1))
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
(-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) 1) (log.f64 (+.f64 (neg.f64 n) 1))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) 1)
(+.f64 (+.f64 (*.f64 (+.f64 1 (neg.f64 n)) (log.f64 (+.f64 1 (neg.f64 n)))) (*.f64 n (log.f64 (neg.f64 n)))) -1)
(+.f64 (fma.f64 (-.f64 1 n) (log1p.f64 (neg.f64 n)) (*.f64 n (log.f64 (neg.f64 n)))) -1)
(fma.f64 (-.f64 1 n) (log1p.f64 (neg.f64 n)) (fma.f64 n (log.f64 (neg.f64 n)) -1))
(fma.f64 n (log.f64 (neg.f64 n)) (fma.f64 (-.f64 1 n) (log1p.f64 (neg.f64 n)) -1))
(neg.f64 (-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) 1) (log.f64 (+.f64 (neg.f64 n) 1))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) 1))
(neg.f64 (+.f64 (+.f64 (*.f64 (+.f64 1 (neg.f64 n)) (log.f64 (+.f64 1 (neg.f64 n)))) (*.f64 n (log.f64 (neg.f64 n)))) -1))
(+.f64 (neg.f64 (fma.f64 (-.f64 1 n) (log1p.f64 (neg.f64 n)) (*.f64 n (log.f64 (neg.f64 n))))) 1)
(-.f64 1 (fma.f64 n (log.f64 (neg.f64 n)) (*.f64 (-.f64 1 n) (log1p.f64 (neg.f64 n)))))
(-.f64 1 (fma.f64 (-.f64 1 n) (log1p.f64 (neg.f64 n)) (*.f64 n (log.f64 (neg.f64 n)))))
Compiler

Compiled 122 to 76 computations (37.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.9s
Operation ival-log, time spent: 1.5s, 53.0% of total-time
Operation ival-add, time spent: 802.0ms, 28.0% of total-time
Operation ival-sub, time spent: 319.0ms, 11.0% of total-time
Operation ival-mult, time spent: 193.0ms, 7.0% of total-time
Operation const, time spent: 53.0ms, 2.0% of total-time

eval1.0ms (0%)

Compiler

Compiled 39 to 23 computations (41% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
3.1%
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
31.1%
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
Compiler

Compiled 28 to 19 computations (32.1% saved)

localize5.4s (26%)

Compiler

Compiled 76 to 35 computations (53.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 3.8s
Operation ival-log, time spent: 1.6s, 42.0% of total-time
Operation ival-add, time spent: 969.0ms, 26.0% of total-time
Operation ival-log1p, time spent: 609.0ms, 16.0% of total-time
Operation ival-sub, time spent: 208.0ms, 6.0% of total-time
Operation ival-fma, time spent: 162.0ms, 4.0% of total-time
Operation ival-mult, time spent: 152.0ms, 4.0% of total-time
Operation const, time spent: 63.0ms, 2.0% of total-time

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune2.0ms (0%)

Pruning

2 alts after pruning (0 fresh and 2 done)

PrunedKeptTotal
New000
Fresh000
Picked022
Done000
Total022
Accuracy
31.1%
Counts
2 → 2
Alt Table
Click to see full alt table
StatusAccuracyProgram
3.1%
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
31.1%
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
Compiler

Compiled 70 to 45 computations (35.7% saved)

regimes11.0ms (0.1%)

Counts
3 → 1
Calls
Call 1
Inputs
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
Outputs
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
Calls

3 calls:

5.0ms
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n)))
3.0ms
n
2.0ms
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
Results
AccuracySegmentsBranch
31.1%1n
31.1%1(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
31.1%1(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n)))
Compiler

Compiled 32 to 23 computations (28.1% saved)

regimes7.0ms (0%)

Accuracy

Total -1.0b remaining (-1.6%)

Threshold costs -1b (-1.6%)

Counts
2 → 1
Calls
Call 1
Inputs
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
Outputs
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
Calls

3 calls:

3.0ms
n
2.0ms
(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
2.0ms
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n)))
Results
AccuracySegmentsBranch
3.1%1(-.f64 (-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n))) 1)
3.1%1(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (*.f64 n (log.f64 n)))
3.1%1n
Compiler

Compiled 32 to 23 computations (28.1% saved)

simplify5.0ms (0%)

Algorithm
egg-herbie
Rules
20×+-commutative
14×sub-neg
14×*-commutative
10×neg-mul-1
10×neg-sub0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
020102
134102
244102
359102
471102
574102
675102
Stop Event
done
saturated
Calls
Call 1
Inputs
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
Outputs
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) -1))
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 (*.f64 n (log.f64 n)) 1))
(-.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (+.f64 1 (*.f64 n (log.f64 n))))
(+.f64 (*.f64 (+.f64 n 1) (log.f64 (+.f64 n 1))) (-.f64 -1 (*.f64 n (log.f64 n))))
Compiler

Compiled 28 to 19 computations (32.1% saved)

soundness949.0ms (4.5%)

Rules
2386×associate--l+
2386×associate--l+
1216×sub-neg
1216×sub-neg
1060×unsub-neg
Iterations

Useful iterations: 4 (0.0ms)

IterNodesCost
023256
161208
2163200
3523200
42076196
54562196
65650196
76508196
86954196
97137196
107152196
117155196
127155196
137158196
147212196
157212196
023256
161208
2163200
3523200
42076196
54562196
65650196
76508196
86954196
97137196
107152196
117155196
127155196
137158196
147212196
157212196
Stop Event
node limit
node limit
Compiler

Compiled 200 to 118 computations (41% saved)

end0.0ms (0%)

preprocess59.0ms (0.3%)

Compiler

Compiled 136 to 98 computations (27.9% saved)

Profiling

Loading profile data...