Henrywood and Agarwal, Equation (3)
Time bar (total: 2.0s)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 0 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 1 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 2 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 3 |
| 0% | 0% | 99.8% | 0.2% | 0% | 0% | 0% | 4 |
| 12.5% | 12.5% | 87.3% | 0.2% | 0% | 0% | 0% | 5 |
| 12.5% | 12.5% | 87.3% | 0.2% | 0% | 0% | 0% | 6 |
| 12.5% | 12.5% | 87.3% | 0.2% | 0% | 0% | 0% | 7 |
| 18.8% | 18.7% | 81.1% | 0.2% | 0% | 0% | 0% | 8 |
| 28.6% | 28.1% | 70.2% | 0.2% | 0% | 1.6% | 0% | 9 |
| 28.6% | 28.1% | 70.2% | 0.2% | 0% | 1.6% | 0% | 10 |
| 28.8% | 28.1% | 69.4% | 0.2% | 0% | 2.3% | 0% | 11 |
| 36.1% | 32.7% | 58.1% | 0.2% | 0% | 9% | 0% | 12 |
Compiled 10 to 10 computations (0% saved)
| 613.0ms | 8 256× | 0 | valid |
| 439.0ms | 6 848× | 0 | invalid |
ival-mult!: 275.0ms (49.8% of total)ival-sqrt: 153.0ms (27.7% of total)ival-div!: 121.0ms (21.9% of total)adjust: 3.0ms (0.5% of total)Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 51 | 130 |
| 1 | 133 | 130 |
| 2 | 257 | 130 |
| 3 | 440 | 130 |
| 4 | 480 | 130 |
| 5 | 514 | 130 |
| 6 | 549 | 130 |
| 7 | 563 | 130 |
| 1× | saturated |
| Status | Accuracy | Program |
|---|---|---|
| ▶ | 73.9% | (*.f64 c0 (sqrt.f64 (/.f64 A (*.f64 V l)))) |
(negabs c0)
(sort V l)
Compiled 16 to 16 computations (0% saved)
| Inputs |
|---|
(*.f64 c0 (sqrt.f64 (/.f64 A (*.f64 V l)))) |
c0 |
(sqrt.f64 (/.f64 A (*.f64 V l))) |
(/.f64 A (*.f64 V l)) |
A |
(*.f64 V l) |
V |
l |
| Outputs |
|---|
#s(approx (* c0 (sqrt (/ A (* V l)))) #s(hole binary64 (* (sqrt (/ A (* V l))) c0))) |
#s(approx c0 #s(hole binary64 c0)) |
#s(approx (sqrt (/ A (* V l))) #s(hole binary64 (sqrt (/ A (* V l))))) |
#s(approx (/ A (* V l)) #s(hole binary64 (/ A (* V l)))) |
#s(approx A #s(hole binary64 A)) |
#s(approx (* c0 (sqrt (/ A (* V l)))) #s(hole binary64 (* -1 (* (sqrt (/ A (* V l))) (* c0 (* (sqrt -1) (sqrt -1))))))) |
#s(approx (sqrt (/ A (* V l))) #s(hole binary64 (* -1 (* (sqrt (/ A (* V l))) (* (sqrt -1) (sqrt -1)))))) |
#s(approx (* V l) #s(hole binary64 (* V l))) |
#s(approx V #s(hole binary64 V)) |
#s(approx (* c0 (sqrt (/ A (* V l)))) #s(hole binary64 (* (sqrt (/ A (* V l))) (* c0 (* (sqrt -1) (sqrt -1)))))) |
#s(approx (sqrt (/ A (* V l))) #s(hole binary64 (* (sqrt (/ A (* V l))) (* (sqrt -1) (sqrt -1))))) |
#s(approx l #s(hole binary64 l)) |
12 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 28.0ms | c0 | @ | -inf | ((* c0 (sqrt (/ A (* V l)))) c0 (sqrt (/ A (* V l))) (/ A (* V l)) A (* V l) V l) |
| 27.0ms | V | @ | inf | ((* c0 (sqrt (/ A (* V l)))) c0 (sqrt (/ A (* V l))) (/ A (* V l)) A (* V l) V l) |
| 8.0ms | A | @ | -inf | ((* c0 (sqrt (/ A (* V l)))) c0 (sqrt (/ A (* V l))) (/ A (* V l)) A (* V l) V l) |
| 7.0ms | V | @ | -inf | ((* c0 (sqrt (/ A (* V l)))) c0 (sqrt (/ A (* V l))) (/ A (* V l)) A (* V l) V l) |
| 7.0ms | l | @ | -inf | ((* c0 (sqrt (/ A (* V l)))) c0 (sqrt (/ A (* V l))) (/ A (* V l)) A (* V l) V l) |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 33 | 174 |
| 0 | 38 | 174 |
| 1× | iter-limit |
| 1× | iter-limit |
| 1× | unsound |
| 1× | iter-limit |
| Inputs |
|---|
(*.f64 c0 (sqrt.f64 (/.f64 A (*.f64 V l)))) |
c0 |
(sqrt.f64 (/.f64 A (*.f64 V l))) |
(/.f64 A (*.f64 V l)) |
A |
(*.f64 V l) |
V |
l |
#s(approx (* c0 (sqrt (/ A (* V l)))) #s(hole binary64 (* (sqrt (/ A (* V l))) c0))) |
#s(approx c0 #s(hole binary64 c0)) |
#s(approx (sqrt (/ A (* V l))) #s(hole binary64 (sqrt (/ A (* V l))))) |
#s(approx (/ A (* V l)) #s(hole binary64 (/ A (* V l)))) |
#s(approx A #s(hole binary64 A)) |
#s(approx (* c0 (sqrt (/ A (* V l)))) #s(hole binary64 (* -1 (* (sqrt (/ A (* V l))) (* c0 (* (sqrt -1) (sqrt -1))))))) |
#s(approx (sqrt (/ A (* V l))) #s(hole binary64 (* -1 (* (sqrt (/ A (* V l))) (* (sqrt -1) (sqrt -1)))))) |
#s(approx (* V l) #s(hole binary64 (* V l))) |
#s(approx V #s(hole binary64 V)) |
#s(approx (* c0 (sqrt (/ A (* V l)))) #s(hole binary64 (* (sqrt (/ A (* V l))) (* c0 (* (sqrt -1) (sqrt -1)))))) |
#s(approx (sqrt (/ A (* V l))) #s(hole binary64 (* (sqrt (/ A (* V l))) (* (sqrt -1) (sqrt -1))))) |
#s(approx l #s(hole binary64 l)) |
| Outputs |
|---|
(*.f64 c0 (sqrt.f64 (/.f64 A (*.f64 V l)))) |
c0 |
(sqrt.f64 (/.f64 A (*.f64 V l))) |
(/.f64 A (*.f64 V l)) |
A |
(*.f64 V l) |
V |
l |
#s(approx (* c0 (sqrt (/ A (* V l)))) (*.f64 (sqrt.f64 (/.f64 A (*.f64 V l))) c0)) |
#s(approx c0 c0) |
#s(approx (sqrt (/ A (* V l))) (sqrt.f64 (/.f64 A (*.f64 V l)))) |
#s(approx (/ A (* V l)) (/.f64 A (*.f64 V l))) |
#s(approx A A) |
#s(approx (* c0 (sqrt (/ A (* V l)))) (*.f64 #s(literal -1 binary64) (*.f64 (sqrt.f64 (/.f64 A (*.f64 V l))) (*.f64 c0 (*.f64 (sqrt.f64 #s(literal -1 binary64)) (sqrt.f64 #s(literal -1 binary64))))))) |
#s(approx (sqrt (/ A (* V l))) (*.f64 #s(literal -1 binary64) (*.f64 (sqrt.f64 (/.f64 A (*.f64 V l))) (*.f64 (sqrt.f64 #s(literal -1 binary64)) (sqrt.f64 #s(literal -1 binary64)))))) |
#s(approx (* V l) (*.f64 V l)) |
#s(approx V V) |
#s(approx (* c0 (sqrt (/ A (* V l)))) (*.f64 (sqrt.f64 (/.f64 A (*.f64 V l))) (*.f64 c0 (*.f64 (sqrt.f64 #s(literal -1 binary64)) (sqrt.f64 #s(literal -1 binary64)))))) |
#s(approx (sqrt (/ A (* V l))) (*.f64 (sqrt.f64 (/.f64 A (*.f64 V l))) (*.f64 (sqrt.f64 #s(literal -1 binary64)) (sqrt.f64 #s(literal -1 binary64))))) |
#s(approx l l) |
Compiled 106 to 52 computations (50.9% saved)
1 alts after pruning (0 fresh and 1 done)
| Pruned | Kept | Total | |
|---|---|---|---|
| New | 12 | 0 | 12 |
| Fresh | 0 | 0 | 0 |
| Picked | 0 | 1 | 1 |
| Done | 0 | 0 | 0 |
| Total | 12 | 1 | 13 |
| Status | Accuracy | Program |
|---|---|---|
| ✓ | 73.9% | (*.f64 c0 (sqrt.f64 (/.f64 A (*.f64 V l)))) |
Compiled 16 to 16 computations (0% saved)
| 1× | done |
Compiled 8 to 8 computations (0% saved)
(sort V l)
(negabs c0)
Compiled 48 to 48 computations (0% saved)
Loading profile data...