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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
/*
IF THESE EXAMPLES CHANGE, CHANGE construction.tex CORRESPONDINGLY
S1 := { [t] : 1 <= t <= n }
S2 := { [x] : (0 <= x <= 100 and
exists y : (2n <= y <= x and y is odd))
or x = 17 }
R := { [i,j] -> [i',j'] : 1 <= i <= i' <= n and not (F(i) = F(i'))
and 1 <= j, j' <= m }
*/
//BEGIN PART 1
#include <omega.h>
using namespace omega;
int main() {
Relation S1(1), S2(1), R(2,2);
S1.name_set_var(1, "t");
S2.name_set_var(1, "x");
assert(!R.is_set());
assert(S1.is_set());
assert(S2.is_set());
Free_Var_Decl n("n");
Free_Var_Decl m("m");
Free_Var_Decl f("F", 1);
Variable_ID S1s_n = S1.get_local(&n);
Variable_ID S2s_n = S2.get_local(&n);
Variable_ID Rs_n = R.get_local(&n);
Variable_ID Rs_m = R.get_local(&m);
Variable_ID Rs_f_in = R.get_local(&f, Input_Tuple);
Variable_ID Rs_f_out = R.get_local(&f, Output_Tuple);
R.name_input_var(1, "i");
R.name_input_var(2, "j");
R.name_output_var(1, "i'");
R.name_output_var(2, "j'");
Variable_ID i = R.input_var(1);
Variable_ID j = R.input_var(2);
Variable_ID i2 = R.output_var(1);
Variable_ID j2 = R.output_var(2);
Variable_ID t = S1.set_var(1);
Variable_ID x = S2.set_var(1);
//END PART 1
//BEGIN PART 2
F_And *S1_root = S1.add_and();
GEQ_Handle tmin = S1_root->add_GEQ(); // t-1 >= 0
tmin.update_coef(t, 10);
tmin.update_coef(t, -9); // t now has coef. 1
tmin.update_const(-1);
GEQ_Handle tmax = S1_root->add_GEQ(); // n-t >= 0
tmax.update_coef(S1s_n,1);
tmax.update_coef(t, -1);
F_Or *S2_root = S2.add_or();
F_And *part1 = S2_root->add_and();
GEQ_Handle xmin = part1->add_GEQ();
xmin.update_coef(x,1);
GEQ_Handle xmax = part1->add_GEQ();
xmax.update_coef(x,-1);
xmax.update_const(100);
F_Exists *exists_y = part1->add_exists();
Variable_ID y = exists_y->declare("y");
F_And *y_stuff = exists_y->add_and();
GEQ_Handle ymin = y_stuff->add_GEQ();
ymin.update_coef(y,1);
ymin.update_coef(S2s_n,-2);
GEQ_Handle ymax = y_stuff->add_GEQ();
ymax.update_coef(x,1);
ymax.update_coef(y,-1);
Stride_Handle y_even = y_stuff->add_stride(2);
y_even.update_coef(y,1);
y_even.update_const(1);
F_And *part2 = S2_root->add_and();
EQ_Handle xvalue = part2->add_EQ();
xvalue.update_coef(x,1);
xvalue.update_const(-17);
//END PART 2
//BEGIN PART 3
F_And *R_root = R.add_and();
GEQ_Handle imin = R_root->add_GEQ();
imin.update_coef(i,1);
imin.update_const(-1);
GEQ_Handle imax = R_root->add_GEQ();
imax.update_coef(i2,1);
imax.update_coef(i,-1);
GEQ_Handle i2max = R_root->add_GEQ();
i2max.update_coef(Rs_n,1);
i2max.update_coef(i2,-1);
EQ_Handle f_eq = R_root->add_not()->add_and()->add_EQ();
f_eq.update_coef(Rs_f_in,-1);
f_eq.update_coef(Rs_f_out,1); // F(In) - F(Out) = 0
GEQ_Handle jmin = R_root->add_GEQ();
jmin.update_coef(j,1);
jmin.update_const(-1);
GEQ_Handle jmax = R_root->add_GEQ();
jmax.update_coef(Rs_m,1);
jmax.update_coef(j,-1);
GEQ_Handle j2min = R_root->add_GEQ();
j2min.update_coef(j2,1);
j2min.update_const(-1);
GEQ_Handle j2max = R_root->add_GEQ();
j2max.update_coef(Rs_m,1);
j2max.update_coef(j2,-1);
//END PART 3
//BEGIN PART 4
S1.print_with_subs(stdout);
assert(S1.is_upper_bound_satisfiable());
assert(!S1.is_tautology());
S1.print_with_subs(stdout); // same as above print
printf("\n");
S2.print();
assert(S2.is_upper_bound_satisfiable());
assert(!S2.is_tautology());
S2.print(); // different from above
printf("\n");
assert(R.is_upper_bound_satisfiable());
assert(!R.is_tautology());
R.print_with_subs(stdout);
coef_t lb, ub;
bool coupled;
R.query_difference(i2, i, lb, ub, coupled);
assert(lb == 1); // i < i2: i2 - i1 > 0
assert(ub == posInfinity);
for(DNF_Iterator di(R.query_DNF()); di; di++) {
printf("In next conjunct,\n");
for(EQ_Iterator ei = (*di)->EQs(); ei; ei++) {
printf(" In next equality constraint,\n");
for(Constr_Vars_Iter cvi(*ei); cvi; cvi++)
printf(" Variable %s has coefficient "coef_fmt"\n",
(*cvi).var->char_name(),
(*cvi).coef);
}
for(GEQ_Iterator gi = (*di)->GEQs(); gi; gi++) {
printf(" In next inequality constraint,\n");
for(Constr_Vars_Iter cvi(*gi); cvi; cvi++)
printf(" Variable %s has coefficient "coef_fmt"\n",
(*cvi).var->char_name(),
(*cvi).coef);
int c = (*gi).get_const();
if (c != 0)
printf(" Constant %d\n", c);
}
printf("\n");
}
//END PART 4
//BEGIN PART 5
Relation S1_or_S2 = Union(copy(S1), copy(S2));
// NOTE! THE FOLLOWING KILLS S1 AND S2
Relation S1_and_S2 = Intersection(S1, S2);
S1_or_S2.is_upper_bound_satisfiable();
S1_and_S2.is_upper_bound_satisfiable();
S1_or_S2.print();
printf("\n");
S1_and_S2.print();
printf("\n");
Relation R_R = Composition(copy(R), R);
R_R.query_difference(i2, i, lb, ub, coupled);
assert(lb == 2);
assert(ub == posInfinity);
return 0;
}
//END PART 5
|
