Examples.Basics.ProofTests:f4 from sbv-4.4

Time bar (total: 1.0s)

start0.0ms (0%)

Memory
0.1MiB live, 0.1MiB allocated

analyze0.0ms (0%)

Memory
0.6MiB live, 0.6MiB allocated
Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
100%99.9%0%0.1%0%0%0%1
Compiler

Compiled 15 to 11 computations (26.7% saved)

sample690.0ms (67.6%)

Memory
15.9MiB live, 974.9MiB allocated
Samples
454.0ms8 256×0valid
Precisions
Click to see histograms. Total time spent on operations: 297.0ms
ival-mult: 215.0ms (72.4% of total)
ival-add: 68.0ms (22.9% of total)
ival-true: 6.0ms (2% of total)
exact: 5.0ms (1.7% of total)
ival-assert: 3.0ms (1% of total)
Bogosity

explain138.0ms (13.5%)

Memory
-12.2MiB live, 237.2MiB allocated
FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
120-0-(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
30-0-(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
00-0-(*.f64 x #s(literal 2 binary64))
00-0-(*.f64 x x)
00-0-(*.f64 (*.f64 x #s(literal 2 binary64)) y)
00-0-y
00-0-#s(literal 2 binary64)
00-0-(*.f64 y y)
00-0-x
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
+.f64(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))nan-rescue120
(*.f64 x x)overflow71
(*.f64 (*.f64 x #s(literal 2 binary64)) y)overflow32
+.f64(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))nan-rescue30
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))overflow75
(*.f64 x x)overflow71
(*.f64 (*.f64 x #s(literal 2 binary64)) y)overflow32
(*.f64 y y)overflow56
Confusion
Predicted +Predicted -
+140
-0242
Precision
1.0
Recall
1.0
Confusion?
Predicted +Predicted MaybePredicted -
+1400
-00242
Precision?
1.0
Recall?
1.0
Freqs
test
numberfreq
0242
113
21
Total Confusion?
Predicted +Predicted MaybePredicted -
+100
-000
Precision?
1.0
Recall?
1.0
Samples
45.0ms512×0valid
Compiler

Compiled 134 to 40 computations (70.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 17.0ms
ival-mult: 12.0ms (70.3% of total)
ival-add: 4.0ms (23.4% of total)
ival-true: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)

preprocess3.0ms (0.3%)

Memory
6.0MiB live, 6.0MiB allocated
Algorithm
egg-herbie
Calls
Call 1
Inputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Outputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Compiler

Compiled 13 to 9 computations (30.8% saved)

eval0.0ms (0%)

Memory
0.2MiB live, 0.2MiB allocated
Compiler

Compiled 0 to 2 computations (-∞% saved)

prune0.0ms (0%)

Memory
0.8MiB live, 0.8MiB allocated
Alt Table
Click to see full alt table
StatusAccuracyProgram
94.5%
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Compiler

Compiled 13 to 9 computations (30.8% saved)

simplify0.0ms (0%)

Memory
1.0MiB live, 1.0MiB allocated
Algorithm
egg-herbie
Localize:

Found 4 expressions of interest:

NewMetricScoreProgram
cost-diff0
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
cost-diff0
(*.f64 x x)
cost-diff0
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
cost-diff0
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Calls
Call 1
Inputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
x
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
#s(literal 2 binary64)
y
(*.f64 y y)
Outputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
x
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
#s(literal 2 binary64)
y
(*.f64 y y)

localize25.0ms (2.5%)

Memory
3.6MiB live, 41.6MiB allocated
Localize:

Found 4 expressions of interest:

NewMetricScoreProgram
accuracy0.0
(*.f64 x x)
accuracy0.0
(*.f64 x #s(literal 2 binary64))
accuracy0.6054687500000001
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
accuracy2.453122935830206
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
Samples
19.0ms256×0valid
Compiler

Compiled 80 to 20 computations (75% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.0ms
ival-mult: 6.0ms (71.4% of total)
ival-add: 2.0ms (23.8% of total)
ival-true: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)

series7.0ms (0.7%)

Memory
13.3MiB live, 13.3MiB allocated
Counts
5 → 17
Calls
Call 1
Inputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
Outputs
(pow y 2)
(+ (* 2 (* x y)) (pow y 2))
(+ (* x (+ x (* 2 y))) (pow y 2))
(* 2 (* x y))
(* x (+ x (* 2 y)))
(pow x 2)
(* 2 x)
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+ (* 2 (* x y)) (pow x 2))
(+ (* y (+ y (* 2 x))) (pow x 2))
(* (pow y 2) (+ 1 (* 2 (/ x y))))
(* (pow y 2) (+ 1 (+ (* 2 (/ x y)) (/ (pow x 2) (pow y 2)))))
(* y (+ (* 2 x) (/ (pow x 2) y)))
(* (pow y 2) (+ 1 (* -1 (/ (+ (* -2 x) (* -1 (/ (pow x 2) y))) y))))
(* -1 (* y (+ (* -2 x) (* -1 (/ (pow x 2) y)))))
Calls

6 calls:

TimeVariablePointExpression
1.0ms
x
@inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x x) (* (* x 2) y) (* x 2))
1.0ms
x
@0
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x x) (* (* x 2) y) (* x 2))
1.0ms
y
@0
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x x) (* (* x 2) y) (* x 2))
1.0ms
x
@-inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x x) (* (* x 2) y) (* x 2))
1.0ms
y
@inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x x) (* (* x 2) y) (* x 2))

simplify0.0ms (0%)

Memory
0.9MiB live, 0.9MiB allocated
Algorithm
egg-herbie
Counts
17 → 5
Calls
Call 1
Inputs
(pow y 2)
(+ (* 2 (* x y)) (pow y 2))
(+ (* x (+ x (* 2 y))) (pow y 2))
(* 2 (* x y))
(* x (+ x (* 2 y)))
(pow x 2)
(* 2 x)
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+ (* 2 (* x y)) (pow x 2))
(+ (* y (+ y (* 2 x))) (pow x 2))
(* (pow y 2) (+ 1 (* 2 (/ x y))))
(* (pow y 2) (+ 1 (+ (* 2 (/ x y)) (/ (pow x 2) (pow y 2)))))
(* y (+ (* 2 x) (/ (pow x 2) y)))
(* (pow y 2) (+ 1 (* -1 (/ (+ (* -2 x) (* -1 (/ (pow x 2) y))) y))))
(* -1 (* y (+ (* -2 x) (* -1 (/ (pow x 2) y)))))
Outputs
(pow y 2)
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+ (* 2 (* x y)) (pow y 2))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(+ (* x (+ x (* 2 y))) (pow y 2))
(*.f64 x x)
(* 2 (* x y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(* x (+ x (* 2 y)))
(*.f64 x #s(literal 2 binary64))

rewrite0.0ms (0%)

Memory
0.8MiB live, 0.8MiB allocated
Counts
5 → 5
Calls
Call 1
Inputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
Outputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))

eval1.0ms (0.1%)

Memory
2.3MiB live, 2.3MiB allocated
Compiler

Compiled 168 to 23 computations (86.3% saved)

prune2.0ms (0.2%)

Memory
3.7MiB live, 3.7MiB allocated
Pruning

5 alts after pruning (4 fresh and 1 done)

PrunedKeptTotal
New6410
Fresh000
Picked011
Done000
Total6511
Accuracy
100.0%
Counts
11 → 5
Alt Table
Click to see full alt table
StatusAccuracyProgram
94.5%
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
54.6%
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
47.8%
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
54.5%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
58.1%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Compiler

Compiled 89 to 60 computations (32.6% saved)

simplify1.0ms (0.1%)

Memory
1.6MiB live, 1.6MiB allocated
Algorithm
egg-herbie
Localize:

Found 14 expressions of interest:

NewMetricScoreProgram
cost-diff0
(*.f64 x #s(literal 2 binary64))
cost-diff0
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
cost-diff0
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
cost-diff0
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
cost-diff0
(*.f64 y y)
cost-diff0
(*.f64 x #s(literal 2 binary64))
cost-diff0
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
cost-diff0
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
cost-diff0
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
cost-diff0
(*.f64 x x)
cost-diff0
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
cost-diff0
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
cost-diff0
(*.f64 x x)
cost-diff0
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(*.f64 x x)
x
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
x
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
#s(literal 2 binary64)
y
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
(*.f64 x #s(literal 2 binary64))
x
#s(literal 2 binary64)
(*.f64 y y)
y
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
x
#s(literal 2 binary64)
y
(*.f64 y y)
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(*.f64 x x)
x
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 x x)
x
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
#s(literal 2 binary64)
y
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
(*.f64 x #s(literal 2 binary64))
x
#s(literal 2 binary64)
(*.f64 y y)
y
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(*.f64 x #s(literal 2 binary64))
x
#s(literal 2 binary64)
y
(*.f64 y y)

localize35.0ms (3.5%)

Memory
-26.2MiB live, 57.6MiB allocated
Localize:

Found 14 expressions of interest:

NewMetricScoreProgram
accuracy0.0
(*.f64 y y)
accuracy0.0
(*.f64 x #s(literal 2 binary64))
accuracy0.6054687500000001
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
accuracy28.43093891451354
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
accuracy0.0
(*.f64 y y)
accuracy0.0
(*.f64 x #s(literal 2 binary64))
accuracy0.6054687500000001
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
accuracy61.15554707671633
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
accuracy0.0
(*.f64 x x)
accuracy0.0
(*.f64 x #s(literal 2 binary64))
accuracy2.453122935830206
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
accuracy26.382382273417388
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
accuracy0.0
(*.f64 x x)
accuracy26.839324218886123
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Samples
26.0ms256×0valid
Compiler

Compiled 276 to 32 computations (88.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 15.0ms
ival-mult: 13.0ms (85.6% of total)
ival-add: 2.0ms (13.2% of total)
ival-true: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)

series5.0ms (0.5%)

Memory
11.2MiB live, 11.2MiB allocated
Counts
11 → 17
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(*.f64 x x)
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
(*.f64 x #s(literal 2 binary64))
(*.f64 y y)
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
Outputs
(pow y 2)
(+ (* 2 (* x y)) (pow y 2))
(+ (* x (+ x (* 2 y))) (pow y 2))
(pow x 2)
(* 2 (* x y))
(* x (+ x (* 2 y)))
(* 2 x)
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+ (* 2 (* x y)) (pow x 2))
(+ (* y (+ y (* 2 x))) (pow x 2))
(* (pow y 2) (+ 1 (* 2 (/ x y))))
(* (pow y 2) (+ 1 (+ (* 2 (/ x y)) (/ (pow x 2) (pow y 2)))))
(* y (+ (* 2 x) (/ (pow x 2) y)))
(* (pow y 2) (+ 1 (* -1 (/ (+ (* -2 x) (* -1 (/ (pow x 2) y))) y))))
(* -1 (* y (+ (* -2 x) (* -1 (/ (pow x 2) y)))))
Calls

6 calls:

TimeVariablePointExpression
1.0ms
x
@-inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* x x) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* (* x 2) y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x 2) (* y y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)))
1.0ms
x
@inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* x x) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* (* x 2) y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x 2) (* y y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)))
1.0ms
y
@-inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* x x) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* (* x 2) y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x 2) (* y y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)))
1.0ms
y
@inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* x x) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* (* x 2) y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x 2) (* y y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)))
1.0ms
x
@0
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* x x) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* (* x 2) y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* x 2) (* y y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)))

simplify0.0ms (0%)

Memory
1.0MiB live, 1.0MiB allocated
Algorithm
egg-herbie
Counts
17 → 11
Calls
Call 1
Inputs
(pow y 2)
(+ (* 2 (* x y)) (pow y 2))
(+ (* x (+ x (* 2 y))) (pow y 2))
(pow x 2)
(* 2 (* x y))
(* x (+ x (* 2 y)))
(* 2 x)
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+ (* 2 (* x y)) (pow x 2))
(+ (* y (+ y (* 2 x))) (pow x 2))
(* (pow y 2) (+ 1 (* 2 (/ x y))))
(* (pow y 2) (+ 1 (+ (* 2 (/ x y)) (/ (pow x 2) (pow y 2)))))
(* y (+ (* 2 x) (/ (pow x 2) y)))
(* (pow y 2) (+ 1 (* -1 (/ (+ (* -2 x) (* -1 (/ (pow x 2) y))) y))))
(* -1 (* y (+ (* -2 x) (* -1 (/ (pow x 2) y)))))
Outputs
(pow y 2)
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(+ (* 2 (* x y)) (pow y 2))
(*.f64 x x)
(+ (* x (+ x (* 2 y))) (pow y 2))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(pow x 2)
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(* 2 (* x y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(* x (+ x (* 2 y)))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
(* 2 x)
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(*.f64 x #s(literal 2 binary64))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(*.f64 y y)
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+ (* 2 (* x y)) (pow x 2))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))

rewrite1.0ms (0.1%)

Memory
1.4MiB live, 1.4MiB allocated
Counts
11 → 11
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(*.f64 x x)
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
(*.f64 x #s(literal 2 binary64))
(*.f64 y y)
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(*.f64 x x)
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y))
(*.f64 (*.f64 x #s(literal 2 binary64)) y)
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64)))
(*.f64 x #s(literal 2 binary64))
(*.f64 y y)
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y))

eval3.0ms (0.3%)

Memory
6.2MiB live, 6.2MiB allocated
Compiler

Compiled 688 to 41 computations (94% saved)

prune5.0ms (0.5%)

Memory
-33.1MiB live, 5.5MiB allocated
Pruning

5 alts after pruning (1 fresh and 4 done)

PrunedKeptTotal
New27128
Fresh000
Picked134
Done011
Total28533
Accuracy
100.0%
Counts
33 → 5
Alt Table
Click to see full alt table
StatusAccuracyProgram
94.5%
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
54.6%
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
54.5%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
55.2%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
58.1%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Compiler

Compiled 89 to 59 computations (33.7% saved)

simplify0.0ms (0%)

Memory
0.5MiB live, 0.5MiB allocated
Algorithm
egg-herbie
Localize:

Found 2 expressions of interest:

NewMetricScoreProgram
cost-diff0
(*.f64 y y)
cost-diff0
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(*.f64 y y)
y
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(*.f64 y y)
y

localize18.0ms (1.8%)

Memory
29.9MiB live, 29.9MiB allocated
Localize:

Found 2 expressions of interest:

NewMetricScoreProgram
accuracy0.0
(*.f64 y y)
accuracy28.692337755577043
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
Samples
13.0ms256×0valid
Compiler

Compiled 40 to 22 computations (45% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.0ms
ival-mult: 6.0ms (73% of total)
ival-add: 2.0ms (24.3% of total)
ival-true: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)

series2.0ms (0.2%)

Memory
3.2MiB live, 3.2MiB allocated
Counts
2 → 12
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(*.f64 y y)
Outputs
(pow y 2)
(+ (* 2 (* x y)) (pow y 2))
(+ (* x (+ x (* 2 y))) (pow y 2))
(pow x 2)
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+ (* 2 (* x y)) (pow x 2))
(+ (* y (+ y (* 2 x))) (pow x 2))
(* (pow y 2) (+ 1 (* 2 (/ x y))))
(* (pow y 2) (+ 1 (+ (* 2 (/ x y)) (/ (pow x 2) (pow y 2)))))
(* (pow y 2) (+ 1 (* -1 (/ (+ (* -2 x) (* -1 (/ (pow x 2) y))) y))))
Calls

6 calls:

TimeVariablePointExpression
0.0ms
y
@inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* y y))
0.0ms
y
@-inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* y y))
0.0ms
y
@0
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* y y))
0.0ms
x
@inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* y y))
0.0ms
x
@-inf
((+ (+ (* x x) (* (* x 2) y)) (* y y)) (* y y))

simplify0.0ms (0%)

Memory
0.6MiB live, 0.6MiB allocated
Algorithm
egg-herbie
Counts
12 → 2
Calls
Call 1
Inputs
(pow y 2)
(+ (* 2 (* x y)) (pow y 2))
(+ (* x (+ x (* 2 y))) (pow y 2))
(pow x 2)
(* (pow x 2) (+ 1 (* 2 (/ y x))))
(* (pow x 2) (+ 1 (+ (* 2 (/ y x)) (/ (pow y 2) (pow x 2)))))
(* (pow x 2) (+ 1 (* -1 (/ (+ (* -2 y) (* -1 (/ (pow y 2) x))) x))))
(+ (* 2 (* x y)) (pow x 2))
(+ (* y (+ y (* 2 x))) (pow x 2))
(* (pow y 2) (+ 1 (* 2 (/ x y))))
(* (pow y 2) (+ 1 (+ (* 2 (/ x y)) (/ (pow x 2) (pow y 2)))))
(* (pow y 2) (+ 1 (* -1 (/ (+ (* -2 x) (* -1 (/ (pow x 2) y))) y))))
Outputs
(pow y 2)
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(+ (* 2 (* x y)) (pow y 2))
(*.f64 y y)

rewrite0.0ms (0%)

Memory
0.6MiB live, 0.6MiB allocated
Counts
2 → 2
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(*.f64 y y)
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(*.f64 y y)

eval0.0ms (0%)

Memory
0.7MiB live, 0.7MiB allocated
Compiler

Compiled 65 to 12 computations (81.5% saved)

prune6.0ms (0.6%)

Memory
-33.0MiB live, 5.0MiB allocated
Pruning

5 alts after pruning (0 fresh and 5 done)

PrunedKeptTotal
New303
Fresh000
Picked011
Done044
Total358
Accuracy
100.0%
Counts
8 → 5
Alt Table
Click to see full alt table
StatusAccuracyProgram
94.5%
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
54.6%
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
54.5%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
55.2%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
58.1%
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Compiler

Compiled 195 to 82 computations (57.9% saved)

regimes8.0ms (0.8%)

Memory
16.5MiB live, 16.5MiB allocated
Counts
6 → 2
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Outputs
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Calls

3 calls:

3.0ms
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
2.0ms
x
2.0ms
y
Results
AccuracySegmentsBranch
98.1%2x
97.0%2y
99.3%2(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Compiler

Compiled 15 to 13 computations (13.3% saved)

regimes7.0ms (0.7%)

Memory
13.9MiB live, 13.9MiB allocated
Counts
5 → 3
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Calls

3 calls:

2.0ms
y
2.0ms
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
2.0ms
x
Results
AccuracySegmentsBranch
83.9%3y
85.3%3x
61.2%2(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
Compiler

Compiled 15 to 13 computations (13.3% saved)

regimes2.0ms (0.2%)

Memory
4.7MiB live, 4.7MiB allocated
Counts
4 → 3
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
(+.f64 #s(approx (+ (* x x) (* (* x 2) y)) (*.f64 x #s(literal 2 binary64))) (*.f64 y y))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)))
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 y y))
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Calls

1 calls:

2.0ms
x
Results
AccuracySegmentsBranch
85.2%3x
Compiler

Compiled 1 to 2 computations (-100% saved)

regimes7.0ms (0.7%)

Memory
-28.3MiB live, 9.9MiB allocated
Counts
1 → 1
Calls
Call 1
Inputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Outputs
#s(approx (+ (+ (* x x) (* (* x 2) y)) (* y y)) (*.f64 x x))
Calls

3 calls:

5.0ms
y
1.0ms
(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
1.0ms
x
Results
AccuracySegmentsBranch
58.1%1(+.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 x #s(literal 2 binary64)) y)) (*.f64 y y))
58.1%1y
58.1%1x
Compiler

Compiled 15 to 13 computations (13.3% saved)

bsearch0.0ms (0%)

Memory
0.7MiB live, 0.7MiB allocated
Algorithm
left-value
Steps
TimeLeftRight
0.0ms
+inf
NaN
Compiler

Compiled 16 to 14 computations (12.5% saved)

bsearch28.0ms (2.8%)

Memory
-4.3MiB live, 39.0MiB allocated
Algorithm
binary-search
Stop Event
narrow-enough
narrow-enough
Steps
TimeLeftRight
11.0ms
1.8537279757795364e-34
5.156126720970749e-34
14.0ms
-1.4093867950977207e-46
-1.9134192189231563e-57
Samples
17.0ms240×0valid
Compiler

Compiled 556 to 404 computations (27.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 12.0ms
ival-mult: 10.0ms (83.4% of total)
ival-add: 2.0ms (16.7% of total)
ival-true: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)

bsearch15.0ms (1.5%)

Memory
29.3MiB live, 29.3MiB allocated
Algorithm
binary-search
Stop Event
narrow-enough
narrow-enough
Steps
TimeLeftRight
0.0ms
1.8537279757795364e-34
5.156126720970749e-34
13.0ms
-1.4093867950977207e-46
-1.9134192189231563e-57
Samples
8.0ms144×0valid
Compiler

Compiled 526 to 374 computations (28.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 5.0ms
ival-mult: 3.0ms (62.9% of total)
ival-add: 1.0ms (21% of total)
ival-true: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)

simplify7.0ms (0.7%)

Memory
-26.4MiB live, 11.7MiB allocated

end0.0ms (0%)

Memory
0.0MiB live, 0.0MiB allocated

Profiling

Loading profile data...