expq3 (problem 3.4.2)

Time bar (total: 1.4min)

analyze449.0ms (0.5%)

Algorithm
1×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%25.4%74.6%0%0%0%0
0%0%25.4%74.6%0%0%0%1
0%0%25.4%74.6%0%0%0%2
0%0%25.4%74.6%0%0%0%3
0%0%22.2%77.8%0%0%0%4
0%0%20.6%79.4%0%0%0%5
0%0%18.3%81.7%0%0%0%6
0%0%10.7%89.3%0%0%0%7
0%0%9.3%90.7%0%0%0%8
0%0%8.2%91.8%0%0%0%9
0%0%5.7%94.3%0%0%0%10
0%0%5%95%0%0%0%11
0%0%4.4%95.6%0%0%0%12
Compiler

Compiled 54 to 30 computations (44.4% saved)

sample1.4min (99.1%)

Results
16.1s5968×2valid-rival
836.0ms5949×2valid-sollya
3.4s2287×1valid-rival
303.0ms2279×1valid-sollya
95.0ms19×2exit-sollya
40.0ms8×1exit-sollya
0.0ms1×0valid-sollya
1.0ms1×0valid-rival
Bogosity

preprocess204.0ms (0.2%)

Algorithm
1×egg-herbie
Rules
662×times-frac
578×div-sub
499×fma-define
425×distribute-lft-in
424×distribute-rgt-in
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
095937
1292921
2754921
32307921
47707921
Stop Event
1×node limit
Calls
Call 1
Inputs
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64))))
(/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64))))
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))))
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64)))))
(neg.f64 (/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64)))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 b a) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))))
(/.f64 (*.f64 a (-.f64 (exp.f64 (*.f64 (+.f64 eps b) a)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 eps a)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b a)) #s(literal 1 binary64))))
(/.f64 (*.f64 b (-.f64 (exp.f64 (*.f64 (+.f64 a eps) b)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a b)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 eps b)) #s(literal 1 binary64))))
Outputs
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps b))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (expm1.f64 (*.f64 eps a))))
(*.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps b)))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps b))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (expm1.f64 (*.f64 eps a))))
(*.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps b)))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps (neg.f64 a)))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 b (neg.f64 a)))) (expm1.f64 (*.f64 eps b))))
(*.f64 eps (/.f64 (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (expm1.f64 (*.f64 eps b))) (expm1.f64 (*.f64 a (neg.f64 eps)))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 a (neg.f64 eps))))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 eps (neg.f64 a))))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b))))))
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps (neg.f64 b)))) (/.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (expm1.f64 (*.f64 eps a))))
(*.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b))))))
(/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64))))
(*.f64 (/.f64 (neg.f64 eps) (expm1.f64 (*.f64 eps (neg.f64 a)))) (/.f64 (expm1.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) (expm1.f64 (*.f64 eps (neg.f64 b)))))
(*.f64 (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b)))) (/.f64 (neg.f64 eps) (*.f64 (expm1.f64 (*.f64 a (neg.f64 eps))) (expm1.f64 (*.f64 eps (neg.f64 b))))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b)))) (*.f64 (expm1.f64 (*.f64 eps (neg.f64 b))) (neg.f64 (expm1.f64 (*.f64 a (neg.f64 eps)))))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 (neg.f64 b) a))) (*.f64 (expm1.f64 (*.f64 eps (neg.f64 a))) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 b)))))))
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))))
(/.f64 (*.f64 eps (expm1.f64 (*.f64 eps (+.f64 b (neg.f64 a))))) (neg.f64 (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 eps (neg.f64 a))))))
(*.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps b)) (neg.f64 (expm1.f64 (*.f64 a (neg.f64 eps)))))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (*.f64 (expm1.f64 (*.f64 eps b)) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 a)))))))
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64)))))
(/.f64 (*.f64 eps (expm1.f64 (*.f64 eps (-.f64 a b)))) (neg.f64 (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b))))))
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (*.f64 (expm1.f64 (*.f64 eps a)) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 b)))))))
(*.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 b)))))))
(*.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (/.f64 (neg.f64 eps) (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b))))))
(neg.f64 (/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64)))))
(/.f64 (*.f64 (neg.f64 eps) (expm1.f64 (*.f64 (+.f64 a b) (neg.f64 eps)))) (neg.f64 (*.f64 (expm1.f64 (*.f64 eps (neg.f64 a))) (expm1.f64 (*.f64 eps (neg.f64 b))))))
(/.f64 (*.f64 eps (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b))))) (*.f64 (expm1.f64 (*.f64 a (neg.f64 eps))) (expm1.f64 (*.f64 eps (neg.f64 b)))))
(*.f64 (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b)))) (/.f64 (/.f64 eps (expm1.f64 (*.f64 a (neg.f64 eps)))) (expm1.f64 (*.f64 eps (neg.f64 b)))))
(*.f64 eps (/.f64 (/.f64 (expm1.f64 (*.f64 eps (-.f64 (neg.f64 b) a))) (expm1.f64 (*.f64 eps (neg.f64 b)))) (expm1.f64 (*.f64 eps (neg.f64 a)))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 b a) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))))
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps b))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (expm1.f64 (*.f64 eps a))))
(*.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps b)))))
(/.f64 (*.f64 a (-.f64 (exp.f64 (*.f64 (+.f64 eps b) a)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 eps a)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b a)) #s(literal 1 binary64))))
(*.f64 a (/.f64 (expm1.f64 (*.f64 a (+.f64 eps b))) (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 a b)))))
(*.f64 (expm1.f64 (*.f64 a (+.f64 eps b))) (/.f64 a (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 a b)))))
(/.f64 (*.f64 b (-.f64 (exp.f64 (*.f64 (+.f64 a eps) b)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a b)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 eps b)) #s(literal 1 binary64))))
(*.f64 (/.f64 b (expm1.f64 (*.f64 a b))) (/.f64 (expm1.f64 (*.f64 b (+.f64 eps a))) (expm1.f64 (*.f64 eps b))))
(*.f64 b (/.f64 (expm1.f64 (*.f64 b (+.f64 eps a))) (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 a b)))))
(*.f64 (expm1.f64 (*.f64 b (+.f64 eps a))) (/.f64 b (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 a b)))))
Symmetry

(sort a b)

Compiler

Compiled 27 to 17 computations (37% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
0.0%
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
Compiler

Compiled 54 to 34 computations (37% saved)

simplify7.0ms (0%)

Algorithm
1×egg-herbie
Rules
6×*-commutative
5×+-commutative
4×unsub-neg
4×sub-neg
3×1-exp
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
02497
13997
24597
34897
45197
55697
Stop Event
1×saturated
Calls
Call 1
Inputs
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
Outputs
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 eps (+.f64 a b))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 eps a)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 eps b)) #s(literal 1 binary64))))
(/.f64 (*.f64 eps (+.f64 (exp.f64 (*.f64 eps (+.f64 a b))) #s(literal -1 binary64))) (*.f64 (+.f64 (exp.f64 (*.f64 eps a)) #s(literal -1 binary64)) (+.f64 (exp.f64 (*.f64 eps b)) #s(literal -1 binary64))))

soundness1.0ms (0%)

Stop Event
1×fuel
Compiler

Compiled 27 to 17 computations (37% saved)

preprocess111.0ms (0.1%)

Remove

(sort a b)

Compiler

Compiled 236 to 150 computations (36.4% saved)

end0.0ms (0%)

Profiling

Loading profile data...