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
77
78
79
80
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# # Compute Sends and receives for the following HPF fragment
#
# I := { [i,j] : 1 <= i <= 14 && 0 <= j <= 14 };
#
# X := { [i,j] -> [3i,3j] };
#
# Y := { [i,j] -> [i',3j] : 3i-1 <= i'<= 3i};
#
# A := { [i,j] -> [3i,3j] };
#
# D := { [t1,t2] -> [p1,p2,c1,c2,l1,l2] :
# t1 = 16c1+4p1+l1
# && t2 = 16c2+4p2+l2
# && 0 <= p1,p2 <= 3
# && 0 <= l1,l2 <= 3 };
#
# P := { [p1,p2,c1,c2,l1,l2] -> [p1,p2]};
#
# C := { [p1,p2,c1,c2,l1,l2] -> [p1,p2,c1,c2]};
#
# own := P(D(A(X))) \I;
#
# own;
{[i,j] -> [p1,p2] : Exists ( alpha,beta : 1 <= i <= 14 && 0 <= j <= 14 && 0 <= p1 <= 3 && 0 <= p2 <= 3 && 4p1+16alpha <= 9i && 4p2+16beta <= 9j && 9i <= 3+4p1+16alpha && 9j <= 3+4p2+16beta)}
#
# need := D(A(Y)) \I;
#
# need;
{[i,j] -> [p1,p2,c1,c2,l1,9j-4p2-16c2] : Exists ( alpha : p1+c1+l1 = 3alpha && 1 <= i <= 14 && 0 <= j <= 14 && 0 <= p1 <= 3 && 0 <= p2 <= 3 && 0 <= l1 <= 3 && 4p2+16c2 <= 9j && 9j <= 3+4p2+16c2 && 9i <= 3+4p1+16c1+l1 && 4p1+16c1+l1 <= 9i)}
#
# different := {[p1,p2] -> [q1,q2,c1,c2,l1,l2] : p1 != q1 || p2 != q2};
#
# ship := (need compose (inverse own) ) intersection different;
#
# symbolic P1,P2;
#
# P := {[P1,P2]};
#
# S := range (ship \ P);
#
# S;
{[3,P2,c1,c2,l1,l2]: Exists ( alpha,beta,gamma : 4P2+l2 = 2c2+9beta && l1+c1 = 3alpha && 0 <= P1 <= -4c1+27 && 0 <= P2 <= 3 && -16c1-6 <= l1 <= 3 && 0 <= l2 <= 3 && 0 <= c2 && 4P2+l2+16c2 <= 126 && 9gamma <= 15+l1+16c1 && 16+4P1+16c1 <= 9gamma)} union
{[In_1,P2,c1,c2,l1,l2]: Exists ( alpha,beta,gamma : 4P2+l2 = 2c2+9beta && In_1+c1+l1 = 3alpha && 0 <= In_1 < P1 <= -4c1+31, 3 && 0 <= P2 <= 3 && 0 <= l2 <= 3 && l1 <= 3 && 6 <= 4In_1+16c1+l1 && 4P1+16c1 <= 9gamma && 0 <= 4P2+l2+16c2 && 4P2+l2+16c2 <= 126 && 9gamma <= 3+4In_1+16c1+l1)}
#
# codegen S;
if (P1 >= 1 && P2 >= 0 && P1 <= 3 && P2 <= 3) {
for(t3 = intDiv(-P1+2+3,4); t3 <= 7; t3++) {
for(t4 = 0; t4 <= 7; t4++) {
for(t5 = 1+intMod(((-P1-t3+1)-1),3); t5 <= 3; t5 += 3) {
if (intMod(4*P1-2*t3+t5-1,9) == 0) {
for(t6 = intMod((-4*P2+2*t4),9); t6 <= 3; t6 += 9) {
s1(P1-1,P2,t3,t4,t5,t6);
}
}
}
}
}
}
if (P1 == 0 && P2 >= 0 && P2 <= 3) {
for(t3 = 0; t3 <= 6; t3++) {
for(t4 = 0; t4 <= 7; t4++) {
for(t5 = 1+intMod((-t3-1),3); t5 <= 3; t5 += 3) {
if (4*t5 == -t3+12) {
for(t6 = intMod((-4*P2+2*t4),9); t6 <= 3; t6 += 9) {
s1(3,P2,-4*t5+12,t4,t5,t6);
}
}
}
}
}
}
#
|
