owned this note
owned this note
Published
Linked with GitHub
# Optimize constraints
## Simple example
```
∀ a0: int.
(a0 ≥ 0) =>
$k0(a0, 0)[a0]
∀ a1: int, a2: int.
$k0(a1, a2)[a0] =>
¬(a2 < a1) => (a2 = a0)
(a2 < a1) => $k0(a1, a2 + 1)[a0]
```
The intuition is that the only application of `$k0` that "constraint" the first argument is `$k0(a0, 0)[a0]`, thus we can remove the argument. Another way to look at this is that the value `a0` flows into all applications of `$k0`. We can do that by first defining a fresh kvar `$k0'` with two arguments and define the substitution `$k0(x, y)[z] := $k0'(y)[z] ∧ x = a0`. I claim that applying the substitution makes the constraint equisatisfiable
```
∀ a0: int.
(a0 ≥ 0) =>
$k0'(0)[a0] ∧ a0 = a0
∀ a1: int, a2: int.
$k0'(a2)[a0] ∧ a1 = a0 =>
¬(a2 < a1) => (a2 = a0)
(a2 < a1) => $k0'(a2 + 1)[a0] ∧ a1 = a0
```
We can further optimize the constraint by doing "constant propagation" and "constant folding"
```
∀ a0: int.
(a0 ≥ 0) =>
$k0'(0)[a0]
∀ a1: int, a2: int.
$k0'(a2)[a0] ∧ a1 = a0 =>
¬(a2 < a0) => (a2 = a0)
(a2 < a0) => $k0'(a2 + 1)[a0]
```
Finally, we can remove `∀a1:int` and `a1 = a0` because `a1 = a0` is only being used in assumptive position
```
∀ a0: int.
(a0 ≥ 0) =>
$k0'(0)[a0]
∀ a2: int.
$k0'(a2)[a0] =>
¬(a2 < a0) => (a2 = a0)
(a2 < a0) => $k0'(a2 + 1)[a0]
```
## A more complicated example
The following example is a variation of the first example where kvars are in a cycle involving more than one variable
```
∀ a0: int.
(a0 ≥ 0) =>
$k0(a0, 0)[a0]
∀ a1: int, a2: int.
$k0(a1, a2)[a0] =>
¬(a2 < a1) => (a2 = a0)
(a2 < a1) => $k1(a1, a2 + 1)[a0]
∀ a1: int, a2: int.
$k1(a1, a2)[a0] => $k0(a1, a2)[a0]
```
In this example we can simultaneously apply the substitutions `$k0(x, y)[z] := $k0'(y)[z] ∧ x = a0` and `$k1(x, y)[z] := $k1'(y)[z] ∧ x = a0` to get the equisatisfiable constraint:
```
∀ a0: int.
(a0 ≥ 0) =>
$k0'(0)[a0] ∧ a0 = a0
∀ a1: int, a2: int.
$k0'(a2)[a0] ∧ a1 = a0 =>
¬(a2 < a1) => (a2 = a0)
(a2 < a1) => $k1'(a2 + 1)[a0] ∧ a1 = a0
∀ a1: int, a2: int.
$k1'(a2)[a0] ∧ a1 = a0 => $k0'(a2)[a0] ∧ a1 = a0
```
And after constrant propagation and quantifier elimination
```
∀ a0: int.
(a0 ≥ 0) =>
$k0'(0)[a0]
∀ a2: int.
$k0'(a2)[a0] =>
¬(a2 < a0) => (a2 = a0)
(a2 < a0) => $k1'(a2 + 1)[a0]
∀ a2: int.
$k1'(a2)[a0] => $k0'(a2)[a0]
```
## FFT
### Optimized
```
bb3: [a0: int] for<b0, b1> $k3 ⇒ {
_1: &'?29 mut RVec<f32>[RVec { a0 }],
_2: &'?30 mut RVec<f32>[RVec { a0 }],
_3: usize[a0 - 1],
_6: usize[b1],
_7: usize[b0],
}
bb6: [a0: int , a1: int, a2: int] for<b0> $k2 ⇒ {
_1: &'?29 mut RVec<f32>[RVec { a0 }],
_2: &'?30 mut RVec<f32>[RVec { a0 }],
_3: usize[a0 - 1],
_6: usize[a2],
_7: usize[a1],
_14: f32,
_18: f32,
_20: f32,
_21: f32,
_22: usize[b0],
}
bb16: [a0: int, a1: int, a2: int, a3: int, a4: int, a5: int] for<b0, b1, b2, b3> $k0 ⇒ {
_1: &'?29 mut RVec<f32>[RVec { a0 }],
_2: &'?30 mut RVec<f32>[RVec { a0 }],
_3: usize[a0 - 1],
_6: usize[a2],
_7: usize[a1],
_14: f32,
_18: f32,
_20: f32,
_21: f32,
_22: usize[a3],
_27: f32,
_29: f32,
_31: f32,
_33: f32,
_39: usize[a5],
_40: usize[a4],
_46: usiz e[b2],
_47: usize[b1],
_50: usize[b0],
_53: usize[b3],
}
bb13: [a0: int, a1: int, a2: int, a3: int] for<b0, b1> $k1 ⇒ {
_1: &'?29 mut RVec<f32>[RVec { a0 }],
_2: &'?30 mut RVec<f32>[RVec { a0 }],
_3: usize[a0 - 1],
_6: usize[a2],
_7: usize[a1],
_14: f32,
_18: f32,
_20: f32,
_21: f32,
_22: usize[a3],
_27: f32,
_29: f32,
_31: f32,
_33: f32,
_39: usize[b1],
_40: usize[b0],
}
```
```
∀ a0: int.
(RVec { a0 } > RVec { 0 } ∧ 0 ≤ a0 ∧ 0 ≤ a0 ∧ a0 ≥ 0) =>
(a0 - 1 ≥ 0) ~ Overflow at 22:13: 22:25
true =>
$k3((a0 - 1)/4, a0 - 1)[a0] ~ Goto(bb3) at 24:9: 24:15
∀ a1: int, a2: int.
($k3(a1, a2)[a0] ∧ 2 < a2) =>
$k2(1)[a0, a1, a2] ~ Goto(bb6) at 31:13: 31:18
∀ a3: int.
$k2(a3)[a0, a1, a2] =>
¬(a3 ≤ a1) => $k3(a1/2, a2/2)[a0] ~ Goto(bb3) at 26:18: 85:6
(a3 ≤ a1) =>
$k1(2 * a2, a3)[a0, a1, a2, a3] ~ Goto(bb13) at 41:17: 41:23
∀ a4: int, a5: int.
$k1(a4, a5)[a0, a1, a2, a3] =>
¬(a5 < a0 - 1) => $k2(a3 + 1)[a0, a1, a2] ~ Goto(bb6) at 81:13: 81:19
(a5 < a0 - 1) =>
$k0(a5 + a1 + a1, a5 + a1, a5, a5 + a1 + a1 + a1)[a0, a1, a2, a3, a4, a5] ~ Goto(bb16) at 47:21: 47:27
∀ a6: int, a7: int, a8: int, a9: int.
$k0(a6, a7, a8, a9)[a0, a1, a2, a3, a4, a5] =>
¬(a9 ≤ a0 - 1) =>
(2 * a4 - a2 ≥ 0) ~ Overflow at 77:22: 77:33
$k1(4 * a4, 2 * a4 - a2 + a3)[a0, a1, a2, a3] ~ Goto(bb13) at 42:26: 79:14
(a9 ≤ a0 - 1) =>
(a8 < a0) ~ Call at 52:32: 52:36
(a6 < a0) ~ Call at 52:41: 52:45
(a8 < a0) ~ Call at 53:32: 53:36
(a6 < a0) ~ Call at 53:41: 53:45
(a8 < a0) ~ Call at 53:23: 53:27
(a7 < a0) ~ Call at 54:32: 54:36
(a9 < a0) ~ Call at 54:41: 54:45
(a7 < a0) ~ Call at 55:32: 55:36
(a9 < a0) ~ Call at 55:41: 55:45
(a7 < a0) ~ Call at 55:23: 55:27
(a8 < a0) ~ Call at 56:32: 56:36
(a6 < a0) ~ Call at 56:41: 56:45
(a8 < a0) ~ Call at 57:32: 57:36
(a6 < a0) ~ Call at 57:41: 57:45
(a8 < a0) ~ Call at 57:23: 57:27
(a7 < a0) ~ Call at 58:32: 58:36
(a9 < a0) ~ Call at 58:41: 58:45
(a7 < a0) ~ Call at 59:32: 59:36
(a9 < a0) ~ Call at 59:41: 59:45
(a7 < a0) ~ Call at 59:23: 59:27
(a6 < a0) ~ Call at 65:23: 65:27
(a6 < a0) ~ Call at 66:23: 66:27
(a9 < a0) ~ Call at 67:23: 67:27
(a9 < a0) ~ Call at 68:23: 68:27
$k0(a6 + a4, a7 + a4, a8 + a4, a9 + a4)[a0, a1, a2, a3, a4, a5] ~ Goto(bb16) at 49:31: 74:18
```
### Unoptimized
```
bb3: [a0: int] for<b0, b1, b2> $k4 ⇒ {
_1: &'?29 mut ∃b3. { RVec<{ f32 | $k8(b3.0)[b0, b1, b2, a0] }>[b3] | $k7(b3.0)[b0, b1, b2, a0] },
_2: &'?30 mut ∃b4. { RVec<{ f32 | $k6(b4.0)[b0, b1, b2, a0] }>[b4] | $k5(b4.0)[b0, b1, b2, a0] },
_3: usize[b2],
_6: usize[b1],
_7: usize[b0],
}
bb6: [a0: int, a1: int, a2: int, a3: int] for<b0, b1, b2, b3> $k9 ⇒ {
_1: &'?29 mut ∃b4. { RVec<{ f32 | $k13 }>[b4] | $k12 },
_2: &'?30 mut ∃b5. { RVec<{ f32 | $k11 }>[b5] | $k10 },
_3: usize[b2],
_6: usize[b1],
_7: usize[b0],
_14: f32,
_18: f32,
_20: f32,
_21: f32,
_22: usize[b3],
}
bb13: [a0: int, a1: int, a2: int, a3: int, a4: int, a5: int, a6: int, a7: int] for<b0, b1, b2, b3, b4, b5> $k14 ⇒ {
_1: &'?29 mut ∃b6. { RVec<{ f32 | $k18 }>[b6] | $k17 },
_2: &'?30 mut ∃b7. { RVec<{ f32 | $k16 }>[b7] | $k15 },
_3: usize[b4],
_6: usize[b2],
_7: usize[b0],
_14: f32,
_18: f32,
_20: f32,
_21: f32,
_22: usize[b5],
_27: f32,
_29: f32,
_31: f32,
_33: f32,
_39: usize[b3],
_40: usize[b1],
}
bb16: [a0: int, a1: int, a2: int, a3: int, a4: int, a5: int, a6: int, a7: int, a8: int, a9: int, a10: int, a11: int, a12: int, a13: int] for<b0, b1, b2, b3, b4, b5, b6, b7, b8, b9> $k19 ⇒ {
_1: &'?29 mut ∃b10. { RVec<{ f32 | $k23 }>[b10] | $k22 },
_2: &'?30 mut ∃b11. { RVec<{ f32 | $k21 }>[b11] | $k20 },
_3: usize[b6],
_6: usize[b4],
_7: usize[b0],
_14: f32,
_18: f32,
_20: f32,
_21: f32,
_22: usize[b8],
_27: f32,
_29: f32,
_31: f32,
_33: f32,
_39: usize[b5],
_40: usize[b2],
_46: usize[b7],
_47: usize[b3],
_50: usize[b1],
_53: usize[b9],
}
```
```
∀ a0: int.
(RVec { a0 } > RVec { 0 } ∧ 0 ≤ a0 ∧ 0 ≤ a0 ∧ a0 ≥ 0) =>
(a0 - 1 ≥ 0) ~ Overflow at 22:13: 22:25
true =>
$k4((a0 - 1)/4, a0 - 1, a0 - 1)[a0] ~ Goto(bb3) at 24:9: 24:15
$k5(a0)[(a0 - 1)/4, a0 - 1, a0 - 1, a0] ~ Goto(bb3) at 24:9: 24:15
$k6(a0)[(a0 - 1)/4, a0 - 1, a0 - 1, a0] ~ Goto(bb3) at 24:9: 24:15
∀ a1: int.
$k5(a1)[(a0 - 1)/4, a0 - 1, a0 - 1, a0] => (a1 = a0) ~ Goto(bb3) at 24:9: 24:15
$k7(a0)[(a0 - 1)/4, a0 - 1, a0 - 1, a0] ~ Goto(bb3) at 24:9: 24:15
$k8(a0)[(a0 - 1)/4, a0 - 1, a0 - 1, a0] ~ Goto(bb3) at 24:9: 24:15
∀ a1: int.
$k7(a1)[(a0 - 1)/4, a0 - 1, a0 - 1, a0] => (a1 = a0) ~ Goto(bb3) at 24:9: 24:15
∀ a1: int, a2: int, a3: int.
($k4(a1, a2, a3)[a0] ∧ 2 < a2) =>
$k9(a1, a2, a3, 1)[a0, a1, a2, a3] ~ Goto(bb6) at 31:13: 31:18
∀ a4: int.
$k5(a4)[a1, a2, a3, a0] =>
$k10(a4)[a1, a2, a3, 1, a0, a1, a2, a3] ~ Goto(bb6) at 31:13: 31:18
$k6(a4)[a1, a2, a3, a0] => $k11(a4)[a1, a2, a3, 1, a0, a1, a2, a3] ~ Goto(bb6) at 31:13: 31:18
∀ a4: int.
$k10(a4)[a1, a2, a3, 1, a0, a1, a2, a3] =>
$k5(a4)[a1, a2, a3, a0] ~ Goto(bb6) at 31:13: 31:18
$k11(a4)[a1, a2, a3, 1, a0, a1, a2, a3] => $k6(a4)[a1, a2, a3, a0] ~ Goto(bb6) at 31:13: 31:18
∀ a4: int.
$k7(a4)[a1, a2, a3, a0] =>
$k12(a4)[a1, a2, a3, 1, a0, a1, a2, a3] ~ Goto(bb6) at 31:13: 31:18
$k8(a4)[a1, a2, a3, a0] => $k13(a4)[a1, a2, a3, 1, a0, a1, a2, a3] ~ Goto(bb6) at 31:13: 31:18
∀ a4: int.
$k12(a4)[a1, a2, a3, 1, a0, a1, a2, a3] =>
$k7(a4)[a1, a2, a3, a0] ~ Goto(bb6) at 31:13: 31:18
$k13(a4)[a1, a2, a3, 1, a0, a1, a2, a3] => $k8(a4)[a1, a2, a3, a0] ~ Goto(bb6) at 31:13: 31:18
∀ a4: int, a5: int, a6: int, a7: int.
$k9(a4, a5, a6, a7)[a0, a1, a2, a3] =>
¬(a7 ≤ a4) =>
$k4(a4/2, a5/2, a6)[a0] ~ Goto(bb3) at 26:18: 85:6
∀ a8: int.
$k10(a8)[a4, a5, a6, a7, a0, a1, a2, a3] =>
$k5(a8)[a4/2, a5/2, a6, a0] ~ Goto(bb3) at 26:18: 85:6
$k11(a8)[a4, a5, a6, a7, a0, a1, a2, a3] => $k6(a8)[a4/2, a5/2, a6, a0] ~ Goto(bb3) at 26:18: 85:6
∀ a8: int.
$k5(a8)[a4/2, a5/2, a6, a0] =>
$k10(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb3) at 26:18: 85:6
$k6(a8)[a4/2, a5/2, a6, a0] => $k11(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb3) at 26:18: 85:6
∀ a8: int.
$k12(a8)[a4, a5, a6, a7, a0, a1, a2, a3] =>
$k7(a8)[a4/2, a5/2, a6, a0] ~ Goto(bb3) at 26:18: 85:6
$k13(a8)[a4, a5, a6, a7, a0, a1, a2, a3] => $k8(a8)[a4/2, a5/2, a6, a0] ~ Goto(bb3) at 26:18: 85:6
∀ a8: int.
$k7(a8)[a4/2, a5/2, a6, a0] =>
$k12(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb3) at 26:18: 85:6
$k8(a8)[a4/2, a5/2, a6, a0] => $k13(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb3) at 26:18: 85:6
(a7 ≤ a4) =>
$k14(a4, 2 * a5, a5, a7, a6, a7)[a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 41:17: 41:23
∀ a8: int.
$k10(a8)[a4, a5, a6, a7, a0, a1, a2, a3] =>
$k15(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 41:17: 41:23
$k11(a8)[a4, a5, a6, a7, a0, a1, a2, a3] => $k16(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 41:17: 41:23
∀ a8: int.
$k15(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k10(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb13) at 41:17: 41:23
$k16(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] => $k11(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb13) at 41:17: 41:23
∀ a8: int.
$k12(a8)[a4, a5, a6, a7, a0, a1, a2, a3] =>
$k17(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 41:17: 41:23
$k13(a8)[a4, a5, a6, a7, a0, a1, a2, a3] => $k18(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 41:17: 41:23
∀ a8: int.
$k17(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k12(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb13) at 41:17: 41:23
$k18(a8)[a4, 2 * a5, a5, a7, a6, a7, a0, a1, a2, a3, a4, a5, a6, a7] => $k13(a8)[a4, a5, a6, a7, a0, a1, a2, a3] ~ Goto(bb13) at 41:17: 41:23
∀ a8: int, a9: int, a10: int, a11: int, a12: int, a13: int.
$k14(a8, a9, a10, a11, a12, a13)[a0, a1, a2, a3, a4, a5, a6, a7] =>
¬(a11 < a12) =>
$k9(a8, a10, a12, a13 + 1)[a0, a1, a2, a3] ~ Goto(bb6) at 81:13: 81:19
∀ a14: int.
$k15(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k10(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] ~ Goto(bb6) at 81:13: 81:19
$k16(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] => $k11(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] ~ Goto(bb6) at 81:13: 81:19
∀ a14: int.
$k10(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] =>
$k15(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb6) at 81:13: 81:19
$k11(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] => $k16(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb6) at 81:13: 81:19
∀ a14: int.
$k17(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k12(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] ~ Goto(bb6) at 81:13: 81:19
$k18(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] => $k13(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] ~ Goto(bb6) at 81:13: 81:19
∀ a14: int.
$k12(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] =>
$k17(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb6) at 81:13: 81:19
$k13(a14)[a8, a10, a12, a13 + 1, a0, a1, a2, a3] => $k18(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb6) at 81:13: 81:19
(a11 < a12) =>
$k19(a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8)[a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 47:21: 47:27
∀ a14: int.
$k15(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k20(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 47:21: 47:27
$k16(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] => $k21(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 47:21: 47:27
∀ a14: int.
$k20(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k15(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb16) at 47:21: 47:27
$k21(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k16(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb16) at 47:21: 47:27
∀ a14: int.
$k17(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k22(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 47:21: 47:27
$k18(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] => $k23(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 47:21: 47:27
∀ a14: int.
$k22(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k17(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb16) at 47:21: 47:27
$k23(a14)[a8, a11 + a8 + a8, a9, a11 + a8, a10, a11, a12, a11, a13, a11 + a8 + a8 + a8, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k18(a14)[a8, a9, a10, a11, a12, a13, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb16) at 47:21: 47:27
∀ a14: int, a15: int, a16: int, a17: int, a18: int, a19: int, a20: int, a21: int, a22: int, a23: int.
$k19(a14, a15, a16, a17, a18, a19, a20, a21, a22, a23)[a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
¬(a23 ≤ a20) =>
(2 * a16 - a18 ≥ 0) ~ Overflow at 77:22: 77:33
$k14(a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22)[a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 42:26: 79:14
∀ a24: int.
$k20(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k15(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 42:26: 79:14
$k21(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k16(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 42:26: 79:14
∀ a24: int.
$k15(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k20(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb13) at 42:26: 79:14
$k16(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] => $k21(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb13) at 42:26: 79:14
∀ a24: int.
$k22(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k17(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 42:26: 79:14
$k23(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k18(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] ~ Goto(bb13) at 42:26: 79:14
∀ a24: int.
$k17(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] =>
$k22(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb13) at 42:26: 79:14
$k18(a24)[a14, 4 * a16, a18, 2 * a16 - a18 + a22, a20, a22, a0, a1, a2, a3, a4, a5, a6, a7] => $k23(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb13) at 42:26: 79:14
(a23 ≤ a20) =>
∀ a24: int.
($k22(a24)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a24) =>
(a21 < a24) ~ Call at 52:32: 52:36
∀ a25: int.
($k22(a25)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a25) =>
(a15 < a25) ~ Call at 52:41: 52:45
∀ a26: int.
($k22(a26)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a26) =>
(a21 < a26) ~ Call at 53:32: 53:36
∀ a27: int.
($k22(a27)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a27) =>
(a15 < a27) ~ Call at 53:41: 53:45
∀ a28: int.
$k22(a28)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k23(a28)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 53:23: 53:27
(a21 < a28) ~ Call at 53:23: 53:27
∀ a29: int.
($k22(a29)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a29) =>
(a17 < a29) ~ Call at 54:32: 54:36
∀ a30: int.
($k22(a30)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a30) =>
(a23 < a30) ~ Call at 54:41: 54:45
∀ a31: int.
($k22(a31)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a31) =>
(a17 < a31) ~ Call at 55:32: 55:36
∀ a32: int.
($k22(a32)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a32) =>
(a23 < a32) ~ Call at 55:41: 55:45
∀ a33: int.
$k22(a33)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k23(a33)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 55:23: 55:27
(a17 < a33) ~ Call at 55:23: 55:27
∀ a34: int.
($k20(a34)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a34) =>
(a21 < a34) ~ Call at 56:32: 56:36
∀ a35: int.
($k20(a35)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a35) =>
(a15 < a35) ~ Call at 56:41: 56:45
∀ a36: int.
($k20(a36)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a36) =>
(a21 < a36) ~ Call at 57:32: 57:36
∀ a37: int.
($k20(a37)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a37) =>
(a15 < a37) ~ Call at 57:41: 57:45
∀ a38: int.
$k20(a38)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k21(a38)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 57:23: 57:27
(a21 < a38) ~ Call at 57:23: 57:27
∀ a39: int.
($k20(a39)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a39) =>
(a17 < a39) ~ Call at 58:32: 58:36
∀ a40: int.
($k20(a40)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a40) =>
(a23 < a40) ~ Call at 58:41: 58:45
∀ a41: int.
($k20(a41)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a41) =>
(a17 < a41) ~ Call at 59:32: 59:36
∀ a42: int.
($k20(a42)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ∧ 0 ≤ a42) =>
(a23 < a42) ~ Call at 59:41: 59:45
∀ a43: int.
$k20(a43)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k21(a43)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 59:23: 59:27
(a17 < a43) ~ Call at 59:23: 59:27
∀ a44: int.
$k22(a44)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k23(a44)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 65:23: 65:27
(a15 < a44) ~ Call at 65:23: 65:27
∀ a45: int.
$k20(a45)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k21(a45)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 66:23: 66:27
(a15 < a45) ~ Call at 66:23: 66:27
∀ a46: int.
$k22(a46)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k23(a46)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 67:23: 67:27
(a23 < a46) ~ Call at 67:23: 67:27
∀ a47: int.
$k20(a47)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k21(a47)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Call at 68:23: 68:27
(a23 < a47) ~ Call at 68:23: 68:27
$k19(a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16)[a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
∀ a48: int.
$k20(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k20(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
$k21(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k21(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
∀ a48: int.
$k20(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k20(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
$k21(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k21(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
∀ a48: int.
$k22(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k22(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
$k23(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k23(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
∀ a48: int.
$k22(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] =>
$k22(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
$k23(a48)[a14, a15 + a16, a16, a17 + a16, a18, a19, a20, a21 + a16, a22, a23 + a16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] => $k23(a48)[a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13] ~ Goto(bb16) at 49:31: 74:18
```
Google Drive
Gist
Clipboard
Sign in with Wallet
