qlog (example 3.10)

Time bar (total: 14.5s)

analyze546.0ms (3.8%)

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
0%0%50%50%0%0%0%3
0%0%50%50%0%0%0%4
0%0%50%50%0%0%0%5
0%0%50%50%0%0%0%6
3.1%1.6%48.4%50%0%0%0%7
6.3%3.1%46.8%50%0%0%0%8
7%3.5%46.4%50%0%0%0%9
7.4%3.7%46.2%50%0%0%0%10
7.8%3.9%46%50%0%0%0%11
8%4%46%50%0%0%0%12
Compiler

Compiled 14 to 9 computations (35.7% saved)

sample13.7s (94.3%)

Results
1.8s4134×1valid
353.0ms4127×1valid-sollya
3.5s3886×2valid
339.0ms3862×2valid-sollya
27.0ms236×0valid
25.0ms236×0valid-sollya
2.0ms24×2exit-sollya
1.0ms1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(6.190464705938283e-260)-1.0(-inf.0 0.0)+nan.0validexit20.089848#f
(-1.125529028682484e-267)-1.0(-inf.0 0.0)+nan.0validexit20.089928#f
(3.7097619310472426e-67)-1.0(-inf.0 0.0)+nan.0validexit10.056767#f
(2.7169173593697113e-34)-1.0(-inf.0 0.0)+nan.0validexit10.059077#f
(4.519135465822608e-92)-1.0(-inf.0 0.0)+nan.0validexit10.0609#f
(3.550018986636292e-283)-1.0(-inf.0 0.0)+nan.0validexit20.088051#f
(-2.2484211545018768e-237)-1.0(-inf.0 0.0)+nan.0validexit20.086643#f
(-4.158190002001743e-201)-1.0(-inf.0 0.0)+nan.0validexit20.12063600000000001#f
(-7.710795519062127e-237)-1.0(-inf.0 0.0)+nan.0validexit20.116014#f
(8.981572648203071e-200)-1.0(-inf.0 0.0)+nan.0validexit20.092076#f
(-1.9094608172547401e-212)-1.0(-inf.0 0.0)+nan.0validexit20.090889#f
(-4.1807796451105164e-75)-1.0(-inf.0 0.0)+nan.0validexit10.09056700000000001#f
(6.128410061851032e-58)-1.0(-inf.0 0.0)+nan.0validexit10.08436#f
(1.2758539932139285e-279)-1.0(-inf.0 0.0)+nan.0validexit20.09555799999999999#f
(1.3892139364496844e-272)-1.0(-inf.0 0.0)+nan.0validexit20.090808#f
(-5.665627953331236e-100)-1.0(-inf.0 0.0)+nan.0validexit10.12155300000000001#f
(7.759364758935875e-185)-1.0(-inf.0 0.0)+nan.0validexit20.09764199999999999#f
(-3.0607444723694977e-181)-1.0(-inf.0 0.0)+nan.0validexit20.102815#f
(-1.7733761662280348e-217)-1.0(-inf.0 0.0)+nan.0validexit20.12813200000000002#f
(-3.989172901318183e-226)-1.0(-inf.0 0.0)+nan.0validexit20.088615#f
(-2.6062660529499766e-280)-1.0(-inf.0 0.0)+nan.0validexit20.059226#f
(-4.516602040525111e-275)-1.0(-inf.0 0.0)+nan.0validexit20.10855#f
(1.0127473488539656e-171)-1.0(-inf.0 0.0)+nan.0validexit20.110019#f
(-1.4344064741101071e-195)-1.0(-inf.0 0.0)+nan.0validexit20.11462800000000001#f
(-3.1652608994703767e-221)-1.0(-inf.0 0.0)+nan.0validexit20.06032#f
(-3.2614260349939585e-116)-1.0(-inf.0 0.0)+nan.0validexit10.05891#f
(1.3296859653269596e-259)-1.0(-inf.0 0.0)+nan.0validexit20.113702#f
(-7.109396945510251e-165)-1.0(-inf.0 0.0)+nan.0validexit20.092154#f
(-4.402283290341417e-175)-1.0(-inf.0 0.0)+nan.0validexit20.087798#f
(-1.565408580392524e-299)-1.0(-inf.0 0.0)+nan.0validexit20.092333#f
(-6.219624197371638e-308)-1.0(-inf.0 0.0)+nan.0validexit20.100346#f
Sollya timings
Total time spent in Sollya 720.0ms
Bogosity

preprocess182.0ms (1.3%)

Algorithm
egg-herbie
Rules
31×fma-neg
29×fma-define
24×sub-neg
11×+-commutative
10×distribute-lft-neg-in
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
019124
140104
261104
3102104
4151104
5203104
6235104
7254104
8274104
9276104
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) x)) (log.f64 (+.f64 #s(literal 1 binary64) x)))
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) x)) (log.f64 (+.f64 #s(literal 1 binary64) x)))
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) (neg.f64 x))) (log.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x))))
(neg.f64 (/.f64 (log.f64 (-.f64 #s(literal 1 binary64) (neg.f64 x))) (log.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x)))))
Outputs
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) x)) (log.f64 (+.f64 #s(literal 1 binary64) x)))
(/.f64 (log1p.f64 (neg.f64 x)) (log1p.f64 x))
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) x)) (log.f64 (+.f64 #s(literal 1 binary64) x)))
(/.f64 (log1p.f64 (neg.f64 x)) (log1p.f64 x))
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) (neg.f64 x))) (log.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x))))
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) (neg.f64 x))) (log1p.f64 (neg.f64 x)))
(/.f64 (log1p.f64 x) (log1p.f64 (neg.f64 x)))
(neg.f64 (/.f64 (log.f64 (-.f64 #s(literal 1 binary64) (neg.f64 x))) (log.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x)))))
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) (neg.f64 x))) (neg.f64 (log1p.f64 (neg.f64 x))))
(/.f64 (neg.f64 (log1p.f64 x)) (log1p.f64 (neg.f64 x)))
(/.f64 (log1p.f64 x) (neg.f64 (log1p.f64 (neg.f64 x))))
Compiler

Compiled 10 to 7 computations (30% saved)

eval1.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

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

Compiled 20 to 14 computations (30% saved)

simplify11.0ms (0.1%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01233
12033
22433
32633
42733
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) x)) (log.f64 (+.f64 #s(literal 1 binary64) x)))
Outputs
(/.f64 (log.f64 (-.f64 #s(literal 1 binary64) x)) (log.f64 (+.f64 #s(literal 1 binary64) x)))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 10 to 7 computations (30% saved)

preprocess86.0ms (0.6%)

Compiler

Compiled 54 to 38 computations (29.6% saved)

end0.0ms (0%)

Profiling

Loading profile data...