1 /* Test BD_Shape::bounded_affine_preimage().
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 namespace {
27 
28 bool
test01()29 test01() {
30   Variable A(0);
31   Variable B(1);
32 
33   TBD_Shape bds(2);
34   bds.add_constraint(A >= 0);
35   bds.add_constraint(A <= 4);
36   bds.add_constraint(B >= 0);
37   bds.add_constraint(B <= 4);
38   bds.add_constraint(A - B <= 2);
39   bds.add_constraint(A - B >= -2);
40 
41   print_constraints(bds, "*** bds ***");
42 
43   bds.bounded_affine_preimage(A, Linear_Expression(7), Linear_Expression(3));
44 
45   BD_Shape<mpq_class> known_result(2, EMPTY);
46 
47   bool ok = check_result(bds, known_result);
48 
49   print_constraints(bds,
50                     "*** bds.bounded_affine_preimage(A, 7, 3) ***");
51 
52   return ok;
53 }
54 
55 bool
test02()56 test02() {
57   Variable A(0);
58   Variable B(1);
59 
60   TBD_Shape bds(2);
61   bds.add_constraint(A >= 0);
62   bds.add_constraint(A <= 4);
63   bds.add_constraint(B >= 0);
64   bds.add_constraint(B <= 4);
65   bds.add_constraint(A - B <= 2);
66   bds.add_constraint(A - B >= -2);
67 
68   print_constraints(bds, "*** bds ***");
69 
70   BD_Shape<mpq_class> known_result(2);
71   known_result.add_constraint(B >= 1);
72   known_result.add_constraint(B <= 4);
73 
74   bds.bounded_affine_preimage(A, Linear_Expression(3), Linear_Expression(7));
75 
76   bool ok = check_result(bds, known_result);
77 
78   print_constraints(bds,
79                     "*** bds.bounded_affine_preimage(A, 3, 7) ***");
80 
81   return ok;
82 }
83 
84 bool
test03()85 test03() {
86   Variable A(0);
87   Variable B(1);
88 
89   TBD_Shape bds(2);
90   bds.add_constraint(A >= 0);
91   bds.add_constraint(A <= 4);
92   bds.add_constraint(B >= 0);
93   bds.add_constraint(B <= 4);
94   bds.add_constraint(A - B <= 2);
95   bds.add_constraint(A - B >= -2);
96 
97   print_constraints(bds, "*** bds ***");
98 
99   BD_Shape<mpq_class> known_result(2, EMPTY);
100 
101   bds.bounded_affine_preimage(A, Linear_Expression(3), Linear_Expression(7),
102                               -1);
103 
104   bool ok = check_result(bds, known_result);
105 
106   print_constraints(bds,
107                     "*** bds.bounded_affine_preimage(A, 3, 7, -1) ***");
108 
109   return ok;
110 }
111 
112 bool
test04()113 test04() {
114   Variable A(0);
115   Variable B(1);
116 
117   TBD_Shape bds(2);
118   bds.add_constraint(A >= 0);
119   bds.add_constraint(A <= 4);
120   bds.add_constraint(B >= 0);
121   bds.add_constraint(B <= 4);
122   bds.add_constraint(A - B <= 2);
123   bds.add_constraint(A - B >= -2);
124 
125   print_constraints(bds, "*** bds ***");
126 
127   BD_Shape<mpq_class> known_result(2, EMPTY);
128 
129   bds.bounded_affine_preimage(A, Linear_Expression(7),
130                               Linear_Expression(3), -1);
131 
132   bool ok = check_result(bds, known_result);
133 
134   print_constraints(bds,
135                     "*** bds.bounded_affine_preimage(A, 7, 3, -1) ***");
136 
137   return ok;
138 }
139 
140 bool
test05()141 test05() {
142   Variable A(0);
143   Variable B(1);
144 
145   TBD_Shape bds(2);
146   bds.add_constraint(A >= 0);
147   bds.add_constraint(A <= 4);
148   bds.add_constraint(B >= 0);
149   bds.add_constraint(B <= 4);
150   bds.add_constraint(A - B <= 2);
151   bds.add_constraint(A - B >= -2);
152 
153   print_constraints(bds, "*** bds ***");
154 
155 
156   BD_Shape<mpq_class> known_result(2);
157   known_result.add_constraint(A >= 1);
158   known_result.add_constraint(B >= 1);
159   known_result.add_constraint(B <= 4);
160   known_result.add_constraint(B - A <= 3);
161 
162   bds.bounded_affine_preimage(A, Linear_Expression(3), A+2);
163 
164   bool ok = check_result(bds, known_result);
165 
166   print_constraints(bds,
167                     "*** bds.bounded_affine_preimage(A, 3, A+2) ***");
168 
169   return ok;
170 }
171 
172 bool
test06()173 test06() {
174   Variable A(0);
175   Variable B(1);
176 
177   TBD_Shape bds(2);
178   bds.add_constraint(A >= 0);
179   bds.add_constraint(A <= 4);
180   bds.add_constraint(B >= 0);
181   bds.add_constraint(B <= 4);
182   bds.add_constraint(A - B <= 2);
183   bds.add_constraint(A - B >= -2);
184 
185   print_constraints(bds, "*** bds ***");
186 
187   BD_Shape<mpq_class> known_result(2);
188   known_result.add_constraint(A <= -1);
189   known_result.add_constraint(B >= 1);
190   known_result.add_constraint(B <= 4);
191 
192   bds.bounded_affine_preimage(A, Linear_Expression(3), -A+2);
193 
194   bool ok = check_result(bds, known_result);
195 
196   print_constraints(bds,
197                     "*** bds.bounded_affine_preimage(A, 3, -A+2) ***");
198 
199   return ok;
200 }
201 
202 bool
test07()203 test07() {
204   Variable A(0);
205   Variable B(1);
206 
207   TBD_Shape bds(2);
208   bds.add_constraint(A >= 0);
209   bds.add_constraint(A <= 4);
210   bds.add_constraint(B >= 0);
211   bds.add_constraint(B <= 4);
212   bds.add_constraint(A - B <= 2);
213   bds.add_constraint(A - B >= -2);
214 
215   print_constraints(bds, "*** bds ***");
216 
217   BD_Shape<mpq_class> known_result(2);
218   known_result.add_constraint(B >= 1);
219   known_result.add_constraint(B <= 4);
220 
221   bds.bounded_affine_preimage(A, Linear_Expression(3), B+5);
222 
223   bool ok = check_result(bds, known_result);
224 
225   print_constraints(bds,
226                     "*** bds.bounded_affine_preimage(A, 3, B+5) ***");
227 
228   return ok;
229 }
230 
231 bool
test08()232 test08() {
233   Variable A(0);
234   Variable B(1);
235 
236   TBD_Shape bds(2);
237   bds.add_constraint(A >= 0);
238   bds.add_constraint(A <= 4);
239   bds.add_constraint(B >= 0);
240   bds.add_constraint(B <= 4);
241   bds.add_constraint(A - B <= 2);
242   bds.add_constraint(A - B >= -2);
243 
244   print_constraints(bds, "*** bds ***");
245 
246   BD_Shape<mpq_class> known_result(2);
247   known_result.add_constraint(B >= 0);
248   known_result.add_constraint(2*B <= 8);
249 
250   bds.bounded_affine_preimage(A, Linear_Expression(3), B-5, -1);
251 
252   bool ok = check_result(bds, known_result);
253 
254   print_constraints(bds,
255                     "*** bds.bounded_affine_preimage(A, 3, B-5, -1) ***");
256 
257   return ok;
258 }
259 
260 bool
test09()261 test09() {
262   Variable A(0);
263   Variable B(1);
264 
265   TBD_Shape bds(2);
266   bds.add_constraint(A >= 0);
267   bds.add_constraint(A <= 4);
268   bds.add_constraint(B >= 0);
269   bds.add_constraint(B <= 4);
270   bds.add_constraint(A - B <= 2);
271   bds.add_constraint(A - B >= -2);
272 
273   print_constraints(bds, "*** bds ***");;
274 
275   BD_Shape<mpq_class> known_result(2);
276   known_result.add_constraint(4*A >= -5);
277   known_result.add_constraint(B >= 0);
278   known_result.add_constraint(B <= 4);
279   known_result.add_constraint(4*(B - A) <= 21);
280 
281   bds.bounded_affine_preimage(A, Linear_Expression(2), 4*A + 3*B - 5);
282 
283   bool ok = check_result(bds, known_result);
284 
285   print_constraints(bds,
286                     "*** bds.bounded_affine_preimage(A, 2, 4*A + 3*B - 5) ***");
287 
288   return ok;
289 }
290 
291 bool
test10()292 test10() {
293   Variable A(0);
294   Variable B(1);
295 
296   TBD_Shape bds(2);
297   bds.add_constraint(A >= 0);
298   bds.add_constraint(A <= 4);
299   bds.add_constraint(B >= 0);
300   bds.add_constraint(B <= 4);
301   bds.add_constraint(A - B <= 2);
302   bds.add_constraint(A - B >= -2);
303 
304   print_constraints(bds, "*** bds ***");
305 
306   BD_Shape<mpq_class> known_result(2);
307   known_result.add_constraint(4*A <= 5);
308   known_result.add_constraint(B >= 0);
309   known_result.add_constraint(B <= 4);
310 
311   bds.bounded_affine_preimage(A, Linear_Expression(2), 4*A + 3*B - 5, -2);
312 
313   bool ok = check_result(bds, known_result);
314 
315   print_constraints(bds,
316                     "*** bds.bounded_affine_preimage(A, 2, "
317                     "4*A + 3*B - 5, -2) ***");
318 
319   return ok;
320 }
321 
322 bool
test11()323 test11() {
324   Variable A(0);
325 
326   TBD_Shape bds(1);
327   bds.add_constraint(A >= 0);
328   bds.add_constraint(A <= 4);
329 
330   print_constraints(bds, "*** bds ***");
331 
332   BD_Shape<mpq_class> known_result(1);
333   known_result.add_constraint(A >= 0);
334   known_result.add_constraint(A <= 4);
335 
336   bds.bounded_affine_preimage(A, A, A);
337 
338   bool ok = check_result(bds, known_result);
339 
340   print_constraints(bds,
341                     "*** bds.bounded_affine_preimage(A, A, A) ***");
342 
343   return ok;
344 }
345 
346 bool
test12()347 test12() {
348   Variable A(0);
349   Variable C(2);
350 
351   BD_Shape<mpz_class> bds(3);
352   bds.add_constraint(C == 5);
353 
354   print_constraints(bds, "*** bds ***");
355 
356   bds.bounded_affine_preimage(C, A, A, 5);
357 
358   BD_Shape<mpz_class> known_result(3);
359   bool ok = check_result(bds, known_result);
360 
361   print_constraints(bds, "*** bds.bounded_affine_preimage(C, A, A, 5) ***");
362 
363   return ok;
364 }
365 
366 } // namespace
367 
368 BEGIN_MAIN
369   DO_TEST(test01);
370   DO_TEST(test02);
371   DO_TEST(test03);
372   DO_TEST(test04);
373   DO_TEST(test05);
374   DO_TEST(test06);
375   DO_TEST(test07);
376   DO_TEST(test08);
377   DO_TEST(test09);
378   DO_TEST(test10);
379   DO_TEST(test11);
380   DO_TEST(test12);
381 END_MAIN
382