1 /* Test refine_with_constraint() and refine_with_constraints()..
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #include "ppl_test.hh"
25
26 using namespace Parma_Polyhedra_Library::IO_Operators;
27 #define REVERSED_TEST
28 #include "partially_reduced_product_test.hh"
29
30 typedef NNC_Polyhedron DOMAIN1;
31 typedef Grid DOMAIN2;
32 typedef Domain_Product<DOMAIN1x, DOMAIN2x>::Constraints_Product Product;
33
34 namespace {
35
36 // Refine with an equality constraint.
37 bool
test01()38 test01() {
39 Variable A(0);
40
41 Product prp(1);
42 prp.refine_with_constraint(A == 0);
43
44 DOMAIN2 gr(1);
45 gr.refine_with_constraint(A == 0);
46 Product known_result(gr);
47
48 bool ok = (prp == known_result);
49
50 print_constraints(prp, "*** prp constraints ***");
51 print_congruences(prp, "*** prp congruences ***");
52
53 return ok && prp.OK();
54 }
55
56 // Refine with a proper constraint.
57 bool
test02()58 test02() {
59 Variable A(0);
60
61 Product prp(1);
62 prp.refine_with_constraint(A >= 4);
63
64 DOMAIN1 ph(1);
65 ph.refine_with_constraint(A >= 4);
66 Product known_result(ph);
67
68 bool ok = (prp == known_result);
69
70 print_constraints(prp, "*** prp constraints ***");
71 print_congruences(prp, "*** prp congruences ***");
72
73 return ok && prp.OK();
74 }
75
76 // Refine with constraints.
77 bool
test03()78 test03() {
79 Variable A(0);
80 Variable B(1);
81
82 Constraint_System cs;
83 cs.insert(2*A <= 1);
84 cs.insert(A + B >= 1);
85
86 Product prp(2);
87 prp.refine_with_constraints(cs);
88
89 DOMAIN1 ph(2);
90 ph.refine_with_constraints(cs);
91 Product known_result(ph);
92
93 bool ok = (prp == known_result);
94
95 print_constraints(prp, "*** prp constraints ***");
96 print_congruences(prp, "*** prp congruences ***");
97
98 return ok && prp.OK();
99 }
100
101 // Universe product with 0 dimensions.
102 bool
test04()103 test04() {
104
105 Product prp(0);
106 prp.refine_with_constraint(Linear_Expression(0) >= 1);
107
108 Product known_result(0, EMPTY);
109
110 bool ok = (prp == known_result);
111
112 print_constraints(prp, "*** prp constraints ***");
113 print_congruences(prp, "*** prp congruences ***");
114
115 return ok && prp.OK();
116 }
117
118 // Empty product with 0 dimensions.
119 bool
test05()120 test05() {
121
122 Product prp(0, EMPTY);
123 prp.refine_with_constraint(Linear_Expression(0) == 0);
124
125 Product known_result(0, EMPTY);
126
127 bool ok = (prp == known_result);
128
129 print_constraints(prp, "*** prp constraints ***");
130 print_congruences(prp, "*** prp congruences ***");
131
132 return ok && prp.OK();
133 }
134
135 // refine_with_constraints
136 bool
test06()137 test06() {
138
139 Variable A(0);
140 Variable B(1);
141 Variable C(2);
142
143 Constraint_System cs;
144 cs.insert(A >= 0);
145 cs.insert(B == 0);
146
147 Product prp(2);
148
149 print_constraints(prp, "*** prp constraints ***");
150 print_congruences(prp, "*** prp congruences ***");
151
152 prp.refine_with_constraints(cs);
153
154 Product known_prp(2);
155 known_prp.refine_with_constraint(A >= 0);
156 known_prp.refine_with_constraint(B == 0);
157
158 bool ok = (prp == known_prp);
159
160 print_constraints(prp, "*** prp constraints ***");
161 print_congruences(prp, "*** prp congruences ***");
162
163 return ok;
164 }
165
166 // refine_with_constraints
167 bool
test07()168 test07() {
169 Variable A(0);
170 Variable B(1);
171
172 Constraint_System cs;
173 cs.insert(A + B <= 0);
174
175 Product prp(2);
176
177 print_constraints(prp, "*** prp constraints ***");
178 print_congruences(prp, "*** prp congruences ***");
179
180 prp.refine_with_constraints(cs);
181
182 Product known_prp(2);
183 known_prp.refine_with_constraint(A + B <= 0);
184
185 bool ok = (prp == known_prp);
186
187 print_constraints(prp, "*** prp constraints ***");
188 print_congruences(prp, "*** prp congruences ***");
189
190 return ok;
191 }
192
193 // refine_with_constraints
194 bool
test08()195 test08() {
196 Variable A(0);
197 Variable B(1);
198
199 Constraint_System cs;
200 cs.insert(A >= 0);
201 cs.insert(A + B == 0);
202
203 Product prp(2);
204
205 print_constraints(prp, "*** prp constraints ***");
206 print_congruences(prp, "*** prp congruences ***");
207
208 prp.refine_with_constraints(cs);
209 bool ok = !prp.is_empty();
210
211 Product known_prp(2);
212 known_prp.refine_with_constraint(A >= 0);
213 known_prp.refine_with_constraint(A + B == 0);
214
215 ok = ok && (prp == known_prp);
216
217 return ok;
218 }
219
220 // refine_with_constraints
221 bool
test09()222 test09() {
223 Variable A(0);
224 Variable B(1);
225
226 Constraint_System cs;
227 cs.insert(B >= 0);
228 cs.insert(A - B == 0);
229
230 Product prp(2);
231
232 print_constraints(prp, "*** prp constraints ***");
233 print_congruences(prp, "*** prp congruences ***");
234
235 prp.refine_with_constraints(cs);
236 bool ok = !prp.is_empty();
237
238 Product known_prp(2);
239 known_prp.refine_with_constraint(B >= 0);
240 known_prp.refine_with_constraint(A - B == 0);
241
242 ok = ok && (prp == known_prp);
243
244 print_constraints(prp, "*** prp constraints ***");
245 print_congruences(prp, "*** prp congruences ***");
246
247 return ok;
248 }
249
250 // refine_with_constraints() and refine_with_congruences()
251 bool
test10()252 test10() {
253 Variable A(0);
254 Variable B(1);
255
256 Product prp(2);
257 Constraint_System cs;
258 cs.insert(A >= 1);
259 cs.insert(A <= 6);
260 prp.refine_with_constraints(cs);
261
262 Product known_prp(prp);
263
264 Constraint_System cs1;
265 cs1.insert(A > 2);
266 cs1.insert(B >= 2);
267 Congruence_System cgs1;
268 cgs1.insert((B %= 2) / 4);
269 cgs1.insert((A + B %= 6) / 0);
270 prp.refine_with_constraint(A > 2);
271 prp.refine_with_constraint(B >= 2);
272 prp.refine_with_congruence((B %= 2) / 4);
273 prp.refine_with_congruence((A + B %= 6) / 0);
274
275 bool ok = prp.OK();
276
277 known_prp.refine_with_constraint(A > 2);
278 known_prp.refine_with_constraint(B >= 2);
279 known_prp.refine_with_congruence((B %= 2) / 4);
280 known_prp.refine_with_congruence((A + B %= 6) / 0);
281
282 ok = ok && prp == known_prp;
283
284 print_congruences(prp, "*** after ok check: prp congruences ***");
285 print_constraints(prp, "*** after ok check: prp constraints ***");
286
287 return ok;
288 }
289
290 // refine_with_constraints() and refine_with_congruences()
291 bool
test11()292 test11() {
293 Variable A(0);
294 Variable B(1);
295
296 Product prp(2);
297 Constraint_System cs;
298 cs.insert(A >= 1);
299 cs.insert(A <= 6);
300 prp.refine_with_constraints(cs);
301
302 Product known_prp(prp);
303
304 Constraint_System cs1;
305 cs1.insert(A > 2);
306 cs1.insert(B >= 2);
307 Congruence_System cgs1;
308 cgs1.insert((B %= 2) / 4);
309 cgs1.insert((A + B %= 6) / 0);
310 prp.refine_with_constraints(cs1);
311 prp.refine_with_congruences(cgs1);
312
313 bool ok = prp.OK();
314
315 known_prp.refine_with_constraint(A > 2);
316 known_prp.refine_with_constraint(B >= 2);
317 known_prp.refine_with_congruence((B %= 2) / 4);
318 known_prp.refine_with_congruence((A + B %= 6) / 0);
319
320 ok = ok && prp == known_prp;
321
322 print_congruences(prp, "*** after ok check: prp congruences ***");
323 print_constraints(prp, "*** after ok check: prp constraints ***");
324
325 return ok;
326 }
327
328 } // namespace
329
330 BEGIN_MAIN
331 DO_TEST(test01);
332 DO_TEST(test02);
333 DO_TEST(test03);
334 DO_TEST(test04);
335 DO_TEST(test05);
336 DO_TEST(test06);
337 DO_TEST(test07);
338 DO_TEST(test08);
339 DO_TEST(test09);
340 DO_TEST(test10);
341 DO_TEST(test11);
342 END_MAIN
343