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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# symbolic p(2), n, m1, m2, low;
#
#
# R := { [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 };
#
#
# f1i := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 &&
# 1 <= iw <= n && 1 <= jw <= m2 &&
# jw = jr &&
# iw = ir };
#
# f1f := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 &&
# 1 <= iw <= n && 1 <= jw <= m2 &&
# jw = jr &&
# iw < ir };
#
#
# f3i := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 &&
# 1 <= iw <= n && 1 < low <= jw <= m1 &&
# jw-1 = jr &&
# iw = ir };
#
# f3f := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 &&
# 1 <= iw <= n && 1 < low <= jw <= m1 &&
# jw-1 = jr &&
# iw < ir };
#
#
# o31i := { [iw3,jw3] -> [iw1,jw1] : 1 <= iw1 <= n && 1 <= jw1 <= m2 &&
# 1 <= iw3 <= n && 1 < low <= jw3 <= m1 &&
# jw1 = jw3-1 &&
# iw1 = iw3 };
#
#
# o13f := { [iw1,jw1] -> [iw3,jw3] : 1 <= iw1 <= n && 1 <= jw1 <= m2 &&
# 1 <= iw3 <= n && 1 < low <= jw3 <= m1 &&
# jw1 = jw3-1 &&
# iw1 < iw3 };
#
#
# o31f := { [iw3,jw3] -> [iw1,jw1] : 1 <= iw1 <= n && 1 <= jw1 <= m2 &&
# 1 <= iw3 <= n && 1 < low <= jw3 <= m1 &&
# jw1 = jw3-1 &&
# iw3 < iw1 };
#
#
# o11f := { [iw1a,jw1a] -> [iw1b,jw1b] : 1 <=iw1a<= n && 1 <=jw1a<= m2 &&
# 1 <=iw1b<= n && 1 <=jw1b<= m2 &&
# jw1a = jw1b &&
# iw1a < iw1b };
#
# o33f := { [iw3a,jw3a] -> [iw3b,jw3b] : 1 <=iw3a<= n && 1 < low <=jw3a<= m1 &&
# 1 <=iw3b<= n && 1 < low <=jw3b<= m1 &&
# jw3a-1 = jw3b-1 &&
# iw3a < iw3b };
#
#
#
# # FIRST GROUP - 1i and 2i (NO POSSIBLE OUTPUT DEPS. BETWEEN)
# v1i := f1i;
#
# v1i;
{[iw,jw] -> [iw,jw] : 1 <= jw <= m1, m2 && 1 <= iw <= n}
#
#
# Exposed12i := R intersection complement domain f1i;
#
# Exposed12i;
{[In_1,In_2]: 1, m2+1 <= In_2 <= m1 && 1 <= In_1 <= n}
#
#
# # SECOND GROUP - 3i
# v3i := f3i / Exposed12i;
# # / is restrictRange
# v3i;
{[iw,jw] -> [iw,jw-1] : 2 <= low <= jw <= m1 && 1 <= iw <= n && m2 <= jw-2}
#
#
# Exposed3i := R intersection complement domain f3i;
#
# Exposed3i;
{[In_1,In_2]: 1 <= In_1 <= n && 1 <= In_2 <= m1 && low <= 1} union
{[In_1,In_2]: 1 <= In_2 <= m1, low-1 && 1 <= In_1 <= n}
#
#
# # THIRD GROUP - 1,2,3f (THERE ARE POSSIBLE OUTPUT DEPS BETWEEN THEM)
#
# v1f := ( f1f / Exposed3i )
# intersection complement ( f3i compose o13f )
# intersection complement ( f3f compose o13f )
# intersection complement ( f1i compose o11f )
# intersection complement ( f1f compose o11f );
#
# v1f;
{[iw1a,jw1a] -> [ir,jr] : FALSE }
#
#
# # WE SHOULD BE ABLE TO DO v1f WITH SOME VALUE-BASED FLOW DD'S
#
# v1f_val := ( f1f / Exposed3i )
# intersection complement ( v3i compose o13f )
# intersection complement ( f3f compose o13f )
# intersection complement ( v1i compose o11f )
# intersection complement ( f1f compose o11f );
#
# v1f_val;
{[iw1a,jw1a] -> [ir,jr] : FALSE }
#
#
# #
# # The effects of loop-independent flow have been taken out already,
# # so this should work. But it does not. Probably I am stupyd.
# #
#
# v1f_clever := ( f1f / Exposed3i )
# intersection complement ( f3f compose o13f )
# intersection complement ( f1f compose o11f );
#
# v1f_clever;
{[iw1a,jw1a] -> [iw1a+1,jw1a] : 1 <= jw1a <= m2, m1 && 1 <= iw1a < n && low <= 1} union
{[iw1a,jw1a] -> [iw1a+1,jw1a] : 1 <= jw1a <= m2, m1, low-1 && 1 <= iw1a < n}
#
#
# #
# # NOW CHECK FOR EQUIVALENCES - THESE SHOULD BE TRUE
# #
#
# v1f subset v1f_val;
True
#
# v1f_val subset v1f;
True
#
# # v1f subset v1f_clever;
# # v1f_clever subset v1f;
|
