Linear.V3:$cdot from linear-1.19.1.3, B

Time bar (total: 3.3s)

analyze13.0ms (0.4%)

Memory
4.4MiB live, 4.4MiB allocated
Algorithm
1×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.7%0.3%0%0%0%0
100%99.7%0%0.3%0%0%0%1
Compiler

Compiled 31 to 25 computations (19.4% saved)

sample2.9s (87.6%)

Memory
11.1MiB live, 949.4MiB allocated
Samples
717.0ms8 256×0valid-sollya
526.0ms8 256×0valid-baseline
459.0ms8 256×0valid-rival
Bogosity

preprocess376.0ms (11.3%)

Memory
4.4MiB live, 36.7MiB allocated
Algorithm
1×egg-herbie
Rules
1 882×fmm-def
699×fma-define
223×sub-neg
183×associate--r+
177×associate-+l-
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
0991377
12541253
25301237
312221237
426041237
540211237
645791237
746271237
846291237
946291237
1046291237
1146291237
1257181237
1357181237
1457181237
Stop Event
1×saturated
Calls
Call 1
Inputs
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 (neg.f64 x) y) (*.f64 z t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x (neg.f64 y)) (*.f64 z t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 (neg.f64 z) t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z (neg.f64 t))) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 (neg.f64 a) b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a (neg.f64 b)))
(neg.f64 (+.f64 (+.f64 (*.f64 (neg.f64 x) y) (*.f64 z t)) (*.f64 a b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x (neg.f64 y)) (*.f64 z t)) (*.f64 a b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 (neg.f64 z) t)) (*.f64 a b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 z (neg.f64 t))) (*.f64 a b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 (neg.f64 a) b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a (neg.f64 b))))
(+.f64 (+.f64 (*.f64 y x) (*.f64 z t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 z y) (*.f64 x t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 t y) (*.f64 z x)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 a y) (*.f64 z t)) (*.f64 x b))
(+.f64 (+.f64 (*.f64 b y) (*.f64 z t)) (*.f64 a x))
(+.f64 (+.f64 (*.f64 x z) (*.f64 y t)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x t) (*.f64 z y)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x a) (*.f64 z t)) (*.f64 y b))
(+.f64 (+.f64 (*.f64 x b) (*.f64 z t)) (*.f64 a y))
(+.f64 (+.f64 (*.f64 x y) (*.f64 t z)) (*.f64 a b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 a t)) (*.f64 z b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 b t)) (*.f64 a z))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z a)) (*.f64 t b))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z b)) (*.f64 a t))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 b a))
Outputs
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a b)))
(fma.f64 x y (fma.f64 a b (*.f64 z t)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a b)))
(fma.f64 x y (fma.f64 a b (*.f64 z t)))
(+.f64 (+.f64 (*.f64 (neg.f64 x) y) (*.f64 z t)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x (neg.f64 y) (*.f64 z t)))
(fma.f64 x (neg.f64 y) (fma.f64 z t (*.f64 a b)))
(-.f64 (fma.f64 z t (*.f64 a b)) (*.f64 x y))
(-.f64 (fma.f64 a b (*.f64 z t)) (*.f64 x y))
(+.f64 (+.f64 (*.f64 x (neg.f64 y)) (*.f64 z t)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x (neg.f64 y) (*.f64 z t)))
(fma.f64 x (neg.f64 y) (fma.f64 z t (*.f64 a b)))
(-.f64 (fma.f64 z t (*.f64 a b)) (*.f64 x y))
(-.f64 (fma.f64 a b (*.f64 z t)) (*.f64 x y))
(+.f64 (+.f64 (*.f64 x y) (*.f64 (neg.f64 z) t)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x y (*.f64 z (neg.f64 t))))
(fma.f64 x y (fma.f64 z (neg.f64 t) (*.f64 a b)))
(fma.f64 t (neg.f64 z) (fma.f64 x y (*.f64 a b)))
(-.f64 (fma.f64 x y (*.f64 a b)) (*.f64 z t))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z (neg.f64 t))) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x y (*.f64 z (neg.f64 t))))
(fma.f64 x y (fma.f64 z (neg.f64 t) (*.f64 a b)))
(fma.f64 t (neg.f64 z) (fma.f64 x y (*.f64 a b)))
(-.f64 (fma.f64 x y (*.f64 a b)) (*.f64 z t))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 (neg.f64 a) b))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a (neg.f64 b)))
(-.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a (neg.f64 b))))
(fma.f64 a (neg.f64 b) (fma.f64 x y (*.f64 z t)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a (neg.f64 b)))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a (neg.f64 b)))
(-.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a (neg.f64 b))))
(fma.f64 a (neg.f64 b) (fma.f64 x y (*.f64 z t)))
(neg.f64 (+.f64 (+.f64 (*.f64 (neg.f64 x) y) (*.f64 z t)) (*.f64 a b)))
(neg.f64 (+.f64 (*.f64 a b) (fma.f64 x (neg.f64 y) (*.f64 z t))))
(neg.f64 (fma.f64 x (neg.f64 y) (fma.f64 z t (*.f64 a b))))
(-.f64 (*.f64 x y) (fma.f64 z t (*.f64 a b)))
(-.f64 (*.f64 x y) (fma.f64 a b (*.f64 z t)))
(neg.f64 (+.f64 (+.f64 (*.f64 x (neg.f64 y)) (*.f64 z t)) (*.f64 a b)))
(neg.f64 (+.f64 (*.f64 a b) (fma.f64 x (neg.f64 y) (*.f64 z t))))
(neg.f64 (fma.f64 x (neg.f64 y) (fma.f64 z t (*.f64 a b))))
(-.f64 (*.f64 x y) (fma.f64 z t (*.f64 a b)))
(-.f64 (*.f64 x y) (fma.f64 a b (*.f64 z t)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 (neg.f64 z) t)) (*.f64 a b)))
(neg.f64 (+.f64 (*.f64 a b) (fma.f64 x y (*.f64 z (neg.f64 t)))))
(neg.f64 (fma.f64 x y (fma.f64 z (neg.f64 t) (*.f64 a b))))
(-.f64 (*.f64 z t) (fma.f64 x y (*.f64 a b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 z (neg.f64 t))) (*.f64 a b)))
(neg.f64 (+.f64 (*.f64 a b) (fma.f64 x y (*.f64 z (neg.f64 t)))))
(neg.f64 (fma.f64 x y (fma.f64 z (neg.f64 t) (*.f64 a b))))
(-.f64 (*.f64 z t) (fma.f64 x y (*.f64 a b)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 (neg.f64 a) b)))
(neg.f64 (+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a (neg.f64 b))))
(-.f64 (*.f64 a b) (fma.f64 x y (*.f64 z t)))
(neg.f64 (+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a (neg.f64 b))))
(neg.f64 (+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a (neg.f64 b))))
(-.f64 (*.f64 a b) (fma.f64 x y (*.f64 z t)))
(+.f64 (+.f64 (*.f64 y x) (*.f64 z t)) (*.f64 a b))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a b)))
(fma.f64 x y (fma.f64 a b (*.f64 z t)))
(+.f64 (+.f64 (*.f64 z y) (*.f64 x t)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x t (*.f64 y z)))
(fma.f64 y z (fma.f64 x t (*.f64 a b)))
(fma.f64 x t (fma.f64 a b (*.f64 y z)))
(+.f64 (+.f64 (*.f64 t y) (*.f64 z x)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x z (*.f64 y t)))
(fma.f64 x z (fma.f64 y t (*.f64 a b)))
(+.f64 (+.f64 (*.f64 a y) (*.f64 z t)) (*.f64 x b))
(+.f64 (*.f64 y a) (fma.f64 x b (*.f64 z t)))
(fma.f64 x b (fma.f64 y a (*.f64 z t)))
(+.f64 (+.f64 (*.f64 b y) (*.f64 z t)) (*.f64 a x))
(+.f64 (*.f64 y b) (fma.f64 x a (*.f64 z t)))
(fma.f64 x a (fma.f64 y b (*.f64 z t)))
(+.f64 (+.f64 (*.f64 x z) (*.f64 y t)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x z (*.f64 y t)))
(fma.f64 x z (fma.f64 y t (*.f64 a b)))
(+.f64 (+.f64 (*.f64 x t) (*.f64 z y)) (*.f64 a b))
(+.f64 (*.f64 a b) (fma.f64 x t (*.f64 y z)))
(fma.f64 y z (fma.f64 x t (*.f64 a b)))
(fma.f64 x t (fma.f64 a b (*.f64 y z)))
(+.f64 (+.f64 (*.f64 x a) (*.f64 z t)) (*.f64 y b))
(+.f64 (*.f64 y b) (fma.f64 x a (*.f64 z t)))
(fma.f64 x a (fma.f64 y b (*.f64 z t)))
(+.f64 (+.f64 (*.f64 x b) (*.f64 z t)) (*.f64 a y))
(+.f64 (*.f64 y a) (fma.f64 x b (*.f64 z t)))
(fma.f64 x b (fma.f64 y a (*.f64 z t)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 t z)) (*.f64 a b))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a b)))
(fma.f64 x y (fma.f64 a b (*.f64 z t)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 a t)) (*.f64 z b))
(+.f64 (fma.f64 x y (*.f64 t a)) (*.f64 z b))
(fma.f64 x y (fma.f64 t a (*.f64 z b)))
(fma.f64 x y (fma.f64 z b (*.f64 t a)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 b t)) (*.f64 a z))
(+.f64 (fma.f64 x y (*.f64 t b)) (*.f64 z a))
(fma.f64 z a (fma.f64 x y (*.f64 t b)))
(fma.f64 x y (fma.f64 z a (*.f64 t b)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z a)) (*.f64 t b))
(+.f64 (fma.f64 x y (*.f64 t b)) (*.f64 z a))
(fma.f64 z a (fma.f64 x y (*.f64 t b)))
(fma.f64 x y (fma.f64 z a (*.f64 t b)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z b)) (*.f64 a t))
(+.f64 (fma.f64 x y (*.f64 t a)) (*.f64 z b))
(fma.f64 x y (fma.f64 t a (*.f64 z b)))
(fma.f64 x y (fma.f64 z b (*.f64 t a)))
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 b a))
(+.f64 (fma.f64 x y (*.f64 z t)) (*.f64 a b))
(fma.f64 x y (fma.f64 z t (*.f64 a b)))
(fma.f64 x y (fma.f64 a b (*.f64 z t)))
Symmetry

(sort x y)

(sort z t)

(sort a b)

Compiler

Compiled 17 to 11 computations (35.3% saved)

eval0.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated
Compiler

Compiled 6 to 6 computations (0% saved)

prune1.0ms (0%)

Memory
0.9MiB live, 0.9MiB allocated
Alt Table
Click to see full alt table
StatusAccuracyProgram
98.0%
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))
Compiler

Compiled 34 to 22 computations (35.3% saved)

simplify2.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated
Algorithm
1×egg-herbie
Rules
3×*-commutative
2×+-commutative
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
02049
12549
Stop Event
1×saturated
Calls
Call 1
Inputs
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))
Outputs
(+.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 a b))

soundness0.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated
Stop Event
1×fuel
Compiler

Compiled 17 to 11 computations (35.3% saved)

preprocess23.0ms (0.7%)

Memory
-0.6MiB live, 31.0MiB allocated
Remove

(sort a b)

(sort z t)

(sort x y)

Compiler

Compiled 272 to 176 computations (35.3% saved)

end0.0ms (0%)

Memory
0.0MiB live, 0.0MiB allocated

Profiling

Loading profile data...