logs (example 3.8)

Time bar (total: 16.5s)

analyze4.0ms (0%)

Algorithm
1×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 11 computations (42.1% saved)

sample16.0s (97.2%)

Results
4.5s8256×1valid-rival
2.8s8216×1valid-sollya
200.0ms40×1exit-sollya
Bogosity

preprocess327.0ms (2%)

Algorithm
1×egg-herbie
Rules
1186×fma-define
470×fma-neg
276×sub-neg
225×associate-+l-
206×unsub-neg
Iterations

Useful iterations: 4 (0.0ms)

IterNodesCost
023256
161208
2161200
3505200
41745196
53243196
64066196
74274196
84290196
94290196
105234196
115236196
125236196
Stop Event
1×saturated
Calls
Call 1
Inputs
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
(-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)) (log.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) #s(literal 1 binary64))
(neg.f64 (-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)) (log.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) #s(literal 1 binary64)))
Outputs
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
(-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (+.f64 (*.f64 n (log.f64 n)) #s(literal 1 binary64)))
(-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log1p.f64 n)) (fma.f64 n (log.f64 n) #s(literal 1 binary64)))
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) #s(literal -1 binary64)))
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
(-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (+.f64 (*.f64 n (log.f64 n)) #s(literal 1 binary64)))
(-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log1p.f64 n)) (fma.f64 n (log.f64 n) #s(literal 1 binary64)))
(+.f64 (log1p.f64 n) (fma.f64 n (-.f64 (log1p.f64 n) (log.f64 n)) #s(literal -1 binary64)))
(-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)) (log.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) #s(literal 1 binary64))
(+.f64 (+.f64 (*.f64 (+.f64 #s(literal 1 binary64) (neg.f64 n)) (log.f64 (+.f64 #s(literal 1 binary64) (neg.f64 n)))) (*.f64 n (log.f64 (neg.f64 n)))) #s(literal -1 binary64))
(+.f64 (fma.f64 (-.f64 #s(literal 1 binary64) n) (log1p.f64 (neg.f64 n)) (*.f64 n (log.f64 (neg.f64 n)))) #s(literal -1 binary64))
(fma.f64 (-.f64 #s(literal 1 binary64) n) (log1p.f64 (neg.f64 n)) (fma.f64 n (log.f64 (neg.f64 n)) #s(literal -1 binary64)))
(fma.f64 n (log.f64 (neg.f64 n)) (fma.f64 (-.f64 #s(literal 1 binary64) n) (log1p.f64 (neg.f64 n)) #s(literal -1 binary64)))
(neg.f64 (-.f64 (-.f64 (*.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)) (log.f64 (+.f64 (neg.f64 n) #s(literal 1 binary64)))) (*.f64 (neg.f64 n) (log.f64 (neg.f64 n)))) #s(literal 1 binary64)))
(neg.f64 (+.f64 (+.f64 (*.f64 (+.f64 #s(literal 1 binary64) (neg.f64 n)) (log.f64 (+.f64 #s(literal 1 binary64) (neg.f64 n)))) (*.f64 n (log.f64 (neg.f64 n)))) #s(literal -1 binary64)))
(neg.f64 (+.f64 (fma.f64 (-.f64 #s(literal 1 binary64) n) (log1p.f64 (neg.f64 n)) (*.f64 n (log.f64 (neg.f64 n)))) #s(literal -1 binary64)))
(-.f64 #s(literal 1 binary64) (fma.f64 n (log.f64 (neg.f64 n)) (*.f64 (-.f64 #s(literal 1 binary64) n) (log1p.f64 (neg.f64 n)))))
(-.f64 #s(literal 1 binary64) (fma.f64 (-.f64 #s(literal 1 binary64) n) (log1p.f64 (neg.f64 n)) (*.f64 n (log.f64 (neg.f64 n)))))
Compiler

Compiled 16 to 9 computations (43.8% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
1.5%
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
Compiler

Compiled 32 to 18 computations (43.8% saved)

simplify6.0ms (0%)

Algorithm
1×egg-herbie
Rules
10×neg-mul-1
9×unsub-neg
8×+-commutative
7×*-commutative
6×sub-neg
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01457
12957
24357
35457
47157
59457
69657
Stop Event
1×saturated
Calls
Call 1
Inputs
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
Outputs
(-.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal 1 binary64))
(+.f64 (-.f64 (*.f64 (+.f64 n #s(literal 1 binary64)) (log.f64 (+.f64 n #s(literal 1 binary64)))) (*.f64 n (log.f64 n))) #s(literal -1 binary64))

soundness1.0ms (0%)

Stop Event
1×fuel
Compiler

Compiled 16 to 10 computations (37.5% saved)

preprocess125.0ms (0.8%)

Compiler

Compiled 114 to 72 computations (36.8% saved)

end0.0ms (0%)

Profiling

Loading profile data...