1 /* Test Box::refine_with_congruences(const Congruence_System&).
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 // Universe Box, zero dimensions and trivial congruence.
29 bool
test01()30 test01() {
31 Congruence cg(Linear_Expression(0) %= 1);
32 TBox box(0);
33 box.refine_with_congruence(cg);
34
35 Rational_Box known_result(0);
36
37 bool ok = check_result(box, known_result);
38
39 print_constraints(box, "*** box ***");
40
41 return ok;
42 }
43
44 // Universe Box, 4 dimensions and refine with a proper congruence
45 bool
test02()46 test02() {
47 Variable A(0);
48 Variable B(1);
49 Variable C(2);
50 Variable D(3);
51
52 Congruence cg(A + B %= 0);
53 TBox box(4);
54 box.refine_with_congruence(cg);
55
56 Rational_Box known_result(4);
57
58 bool ok = check_result(box, known_result);
59
60 print_constraints(box, "*** box ***");
61
62 return ok;
63 }
64
65 // Universe Box in 3D and refine with an equality congruence.
66 bool
test03()67 test03() {
68 Variable A(0);
69 Variable B(1);
70 Variable C(2);
71
72 Congruence cg((A %= 7) / 0);
73
74 TBox box(3);
75 box.refine_with_congruence(cg);
76
77 Rational_Box known_result(3);
78 known_result.add_constraint(A == 7);
79
80 bool ok = check_result(box, known_result);
81
82 print_constraints(box, "*** box ***");
83
84 return ok;
85 }
86
87 // Box in 1D and refine with an inconsistent proper congruence.
88 bool
test04()89 test04() {
90 Variable A(0);
91
92 Congruence cg((0*A %= 1) / 2);
93
94 TBox box(1);
95 box.refine_with_congruence(cg);
96
97 Rational_Box known_result(1, EMPTY);
98
99 bool ok = check_result(box, known_result);
100
101 print_constraints(box, "*** box ***");
102
103 return ok;
104 }
105
106 // refine_with_congruence()
107 bool
test05()108 test05() {
109 Variable A(0);
110 Variable B(1);
111 Variable C(2);
112 Variable D(3);
113
114 Constraint_System cs;
115 cs.insert(A <= 5);
116 cs.insert(A >= 0);
117 cs.insert(B <= 5);
118 cs.insert(B >= 0);
119 cs.insert(C <= 5);
120 cs.insert(C >= 0);
121 cs.insert(D <= 5);
122 cs.insert(D >= 0);
123 TBox box(cs);
124 box.refine_with_congruence((1*A + 2*B + 3*C + 4*D %= 0) / 0);
125
126 Constraint_System known_cs;
127 known_cs.insert(A == 0);
128 known_cs.insert(B == 0);
129 known_cs.insert(C == 0);
130 known_cs.insert(D == 0);
131 Rational_Box known_result(known_cs);
132
133 bool ok = check_result(box, known_result);
134
135 print_constraints(box, "*** box ***");
136
137 return ok;
138 }
139
140
141 bool
test06()142 test06() {
143 Variable x(0);
144 Variable y(1);
145 Variable z(2);
146
147 TBox box1(2);
148
149 try {
150 // This is an invalid use of method
151 // Box::refine_with_congruence: it is illegal
152 // to refine with a congruence with bigger dimension.
153 box1.refine_with_congruence(x %= 0);
154 box1.refine_with_congruence(y - x + z %= 0);
155 }
156 catch (std::invalid_argument& e) {
157 nout << "std::invalid_argument: " << endl;
158 return true;
159 }
160 catch (...) {
161 }
162 return false;
163 }
164
165 bool
test07()166 test07() {
167 Variable y(1);
168
169 TBox box(1);
170
171 try {
172 // This is an invalid use of the method
173 // Box::refine_with_congruence(c): it is illegal to refine with a
174 // congruence that contains a variable that is not in the space
175 // of the box.
176 box.refine_with_congruence((y %= 0) / 0);
177 }
178 catch (std::invalid_argument& e) {
179 nout << "std::invalid_argument: " << endl;
180 return true;
181 }
182 catch (...) {
183 }
184 return false;
185 }
186
187 } // namespace
188
189 BEGIN_MAIN
190 DO_TEST(test01);
191 DO_TEST(test02);
192 DO_TEST(test03);
193 DO_TEST(test04);
194 DO_TEST(test05);
195 DO_TEST(test06);
196 DO_TEST(test07);
197 END_MAIN
198