1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
>>> #
>>> # Test floor/ceiling variable definitions in loop bounds
>>> #
>>>
>>> symbolic m, n;
>>>
>>> # loop is strided
>>> #
>>> is := {[i]: exists (alpha: i = 4alpha && m <= 3i <= n)};
>>> codegen is;
for(t1 = 4*intDiv(intDiv(m+2,3)+3,4); t1 <= intDiv(n,3); t1 += 4) {
s1(t1);
}
>>>
>>> # only one single floor/ceiling variable in bound
>>> #
>>> is := {[i]: exists (lb: m-4 < 4*lb <= m && lb <= i <= n)};
>>> codegen is;
for(t1 = intDiv(m-3+3,4); t1 <= n; t1++) {
s1(t1);
}
>>>
>>> # the floor/ceiling variable in bound has coefficient
>>> #
>>> is := {[i]: exists (lb: m-4 < 4*lb <= m && 4*lb <= i <= n)};
>>> codegen is;
for(t1 = 4*intDiv(m,4); t1 <= n; t1++) {
s1(t1);
}
>>>
>>> # mutiple floor/ceiling variables in bound
>>> #
>>> is := {[i]:exists (alpha,beta: m-4<4alpha<=m && m-3<3beta<=m &&
>>> 4alpha+3*beta<=i<=n )};
>>> codegen is;
for(t1 = 3*intDiv(m,3)+4*intDiv(m,4); t1 <= n; t1++) {
s1(t1);
}
>>>
>>> # non-tight floor/ceiling definition
>>> #
>>> is := {[i]: exists (ub: n-2 < 3*ub <= n && m <= i <= 5*ub)};
>>> codegen is;
if (n-1 <= 3*intDiv(n,3)) {
for(t1 = m; t1 <= 5*intDiv(n,3); t1++) {
s1(t1);
}
}
>>>
>>> # chain floor/ceiling definitions
>>> #
>>> is := {[i]: exists (alpha, beta: beta-4<4alpha<=beta &&
>>> m-8<8beta<=m && 4alpha<=i<=n )};
>>> codegen is;
for(t1 = 4*intDiv(m,32); t1 <= n; t1++) {
s1(t1);
}
>>>
>>> # one complicated case
>>> #
>>> is := {[i]: exists (alpha, beta: beta-4<4alpha<=beta &&
>>> m-7<8beta<=m && 4alpha<=i<=n )};
>>> codegen is;
if (m-6 <= 8*intDiv(m,8)) {
for(t1 = 4*intDiv(m,32); t1 <= n; t1++) {
s1(t1);
}
}
|
