logq (problem 3.4.3)

Time bar (total: 11.8s)

analyze3.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%50%50%0%0%0%0
0%0%50%50%0%0%0%1
0%0%50%50%0%0%0%2
50%25%25%50%0%0%0%3
75%37.5%12.5%50%0%0%0%4
87.5%43.7%6.2%50%0%0%0%5
93.8%46.8%3.1%50%0%0%0%6
96.9%48.4%1.6%50%0%0%0%7
98.4%49.2%0.8%50%0%0%0%8
99.2%49.6%0.4%50%0%0%0%9
99.6%49.8%0.2%50%0%0%0%10
99.8%49.9%0.1%50%0%0%0%11
99.9%49.9%0%50%0%0%0%12
Compiler

Compiled 13 to 8 computations (38.5% saved)

sample11.6s (98.6%)

Results
2.2s6069×1valid
680.0ms6055×1valid-sollya
1.2s1979×2valid
226.0ms1973×2valid-sollya
23.0ms208×0valid
20.0ms208×0valid-sollya
2.0ms14×1exit-sollya
1.0ms2exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-9.87692897741125e-83)1.97538579548225e-82(0.0 2.168404344971009e-19)+nan.0validexit10.14064700000000002#f
(3.14260222583598e-164)-6.28520445167196e-164(-1.6263032587282567e-19 0.0)+nan.0validexit10.114956#f
(6.5332127824491e-54)-1.30664255648982e-53(-1.6263032587282567e-19 0.0)+nan.0validexit10.083416#f
(3.7628280985129485e-222)-7.525656197025897e-222(-1.6263032587282567e-19 0.0)+nan.0validexit10.143266#f
(3.6303343581580803e-162)-7.260668716316161e-162(-1.6263032587282567e-19 0.0)+nan.0validexit10.110983#f
(-2.1161074211038644e-188)4.232214842207729e-188(0.0 2.168404344971009e-19)+nan.0validexit20.13337000000000002#f
(1.176462802049151e-73)-2.352925604098302e-73(-1.6263032587282567e-19 0.0)+nan.0validexit10.11708#f
(2.112551535354744e-128)-4.225103070709488e-128(-1.6263032587282567e-19 0.0)+nan.0validexit10.076642#f
(-2.993044459579937e-271)5.986088919159874e-271(0.0 2.168404344971009e-19)+nan.0validexit20.141231#f
(1.45753048954044e-12)-2.91506097908088e-12(-2.915060987739112e-12 -2.9150607708986773e-12)+nan.0validexit10.116527#f
(-7.439957996259388e-260)1.4879915992518776e-259(0.0 2.168404344971009e-19)+nan.0validexit20.109764#f
(5.518363257803638e-266)-1.1036726515607275e-265(-1.6263032587282567e-19 0.0)+nan.0validexit10.07658#f
(-3.989647879774808e-232)7.979295759549616e-232(0.0 2.168404344971009e-19)+nan.0validexit20.081622#f
(2.360425124506982e-302)-4.720850249013964e-302(-1.6263032587282567e-19 0.0)+nan.0validexit10.129962#f
(2.1702537391500976e-196)-4.340507478300195e-196(-1.6263032587282567e-19 0.0)+nan.0validexit10.076746#f
(1.454610774633958e-261)-2.909221549267916e-261(-1.6263032587282567e-19 0.0)+nan.0validexit10.15237399999999998#f
(-6.571881382568851e-230)1.3143762765137703e-229(0.0 2.168404344971009e-19)+nan.0validexit20.14699099999999998#f
(2.339648109813577e-93)-4.679296219627154e-93(-1.6263032587282567e-19 0.0)+nan.0validexit10.1747#f
(-7.110454972917861e-307)1.4220909945835722e-306(0.0 2.168404344971009e-19)+nan.0validexit20.121529#f
(9.152764783099069e-213)-1.8305529566198137e-212(-1.6263032587282567e-19 0.0)+nan.0validexit10.110036#f
Sollya timings
Total time spent in Sollya 928.0ms
Bogosity

preprocess90.0ms (0.8%)

Algorithm
egg-herbie
Rules
315×fma-define
222×fma-neg
80×times-frac
67×associate-*l*
62×div-sub
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
017128
138120
263120
3127120
4256120
5592120
61257120
71498120
81578120
Stop Event
saturated
Calls
Call 1
Inputs
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 eps)) (+.f64 #s(literal 1 binary64) (neg.f64 eps))))
(neg.f64 (log.f64 (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 eps)) (+.f64 #s(literal 1 binary64) (neg.f64 eps)))))
Outputs
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 eps)) (+.f64 #s(literal 1 binary64) (neg.f64 eps))))
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 eps)) (-.f64 #s(literal 1 binary64) eps)))
(log.f64 (/.f64 (+.f64 #s(literal 1 binary64) eps) (-.f64 #s(literal 1 binary64) eps)))
(neg.f64 (log.f64 (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 eps)) (+.f64 #s(literal 1 binary64) (neg.f64 eps)))))
(neg.f64 (log.f64 (/.f64 (-.f64 #s(literal 1 binary64) (neg.f64 eps)) (-.f64 #s(literal 1 binary64) eps))))
(neg.f64 (log.f64 (/.f64 (+.f64 #s(literal 1 binary64) eps) (-.f64 #s(literal 1 binary64) eps))))
Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
8.2%
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))
Compiler

Compiled 18 to 12 computations (33.3% saved)

simplify19.0ms (0.2%)

Algorithm
egg-herbie
Rules
1-exp
+-commutative
sub-neg
*-commutative
neg-sub0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01129
11929
22329
32529
42629
Stop Event
saturated
Calls
Call 1
Inputs
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))
Outputs
(log.f64 (/.f64 (-.f64 #s(literal 1 binary64) eps) (+.f64 #s(literal 1 binary64) eps)))

soundness3.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 6 computations (33.3% saved)

preprocess48.0ms (0.4%)

Compiler

Compiled 50 to 34 computations (32% saved)

end0.0ms (0%)

Profiling

Loading profile data...