1 /* Pointset_Powerset class implementation: non-inline functions.
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-config.h"
25 #include "Pointset_Powerset_defs.hh"
26 #include "Grid_defs.hh"
27 #include <utility>
28
29 namespace PPL = Parma_Polyhedra_Library;
30
31 template <>
32 void
33 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
difference_assign(const Pointset_Powerset & y)34 ::difference_assign(const Pointset_Powerset& y) {
35 Pointset_Powerset& x = *this;
36 using std::swap;
37 // Ensure omega-reduction.
38 x.omega_reduce();
39 y.omega_reduce();
40 Sequence new_sequence = x.sequence;
41 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
42 const NNC_Polyhedron& ph_yi = yi->pointset();
43 Sequence tmp_sequence;
44 for (Sequence_const_iterator itr = new_sequence.begin(),
45 ns_end = new_sequence.end(); itr != ns_end; ++itr) {
46 const std::pair<NNC_Polyhedron, Pointset_Powerset<NNC_Polyhedron> >
47 partition = linear_partition(ph_yi, itr->pointset());
48 const Pointset_Powerset<NNC_Polyhedron>& residues = partition.second;
49 // Append the contents of `residues' to `tmp_sequence'.
50 std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
51 }
52 swap(tmp_sequence, new_sequence);
53 }
54 swap(x.sequence, new_sequence);
55 x.reduced = false;
56 PPL_ASSERT_HEAVY(x.OK());
57 }
58
59 template <>
60 bool
61 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
geometrically_covers(const Pointset_Powerset & y) const62 ::geometrically_covers(const Pointset_Powerset& y) const {
63 const Pointset_Powerset& x = *this;
64 for (const_iterator yi = y.begin(), y_end = y.end();
65 yi != y_end; ++yi) {
66 if (!check_containment(yi->pointset(), x)) {
67 return false;
68 }
69 }
70 return true;
71 }
72
73 /*! \relates Parma_Polyhedra_Library::Pointset_Powerset */
74 bool
check_containment(const NNC_Polyhedron & ph,const Pointset_Powerset<NNC_Polyhedron> & ps)75 PPL::check_containment(const NNC_Polyhedron& ph,
76 const Pointset_Powerset<NNC_Polyhedron>& ps) {
77 if (ph.is_empty()) {
78 return true;
79 }
80 Pointset_Powerset<NNC_Polyhedron> tmp(ph.space_dimension(), EMPTY);
81 tmp.add_disjunct(ph);
82 for (Pointset_Powerset<NNC_Polyhedron>::const_iterator
83 i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
84 const NNC_Polyhedron& pi = i->pointset();
85 for (Pointset_Powerset<NNC_Polyhedron>::iterator
86 j = tmp.begin(); j != tmp.end(); ) {
87 const NNC_Polyhedron& pj = j->pointset();
88 if (pi.contains(pj)) {
89 j = tmp.drop_disjunct(j);
90 }
91 else {
92 ++j;
93 }
94 }
95 if (tmp.empty()) {
96 return true;
97 }
98 else {
99 Pointset_Powerset<NNC_Polyhedron> new_disjuncts(ph.space_dimension(),
100 EMPTY);
101 for (Pointset_Powerset<NNC_Polyhedron>::iterator
102 j = tmp.begin(); j != tmp.end(); ) {
103 const NNC_Polyhedron& pj = j->pointset();
104 if (pj.is_disjoint_from(pi)) {
105 ++j;
106 }
107 else {
108 const std::pair<NNC_Polyhedron, Pointset_Powerset<NNC_Polyhedron> >
109 partition = linear_partition(pi, pj);
110 new_disjuncts.upper_bound_assign(partition.second);
111 j = tmp.drop_disjunct(j);
112 }
113 }
114 tmp.upper_bound_assign(new_disjuncts);
115 }
116 }
117 return false;
118 }
119
120
121 namespace {
122
123 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
124 //! Uses the congruence \p c to approximately partition the grid \p gr.
125 /*! \relates Parma_Polyhedra_Library::Pointset_Powerset
126 On exit, the intersection of \p gr and congruence \p c is stored
127 in \p gr, whereas a finite set of grids whose set-theoretic union
128 contains the intersection of \p gr with the negation of \p c
129 is added, as a set of new disjuncts, to the powerset \p r.
130 */
131 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
132 bool
approximate_partition_aux(const PPL::Congruence & c,PPL::Grid & gr,PPL::Pointset_Powerset<PPL::Grid> & r)133 approximate_partition_aux(const PPL::Congruence& c,
134 PPL::Grid& gr,
135 PPL::Pointset_Powerset<PPL::Grid>& r) {
136 using namespace PPL;
137 const Coefficient& c_modulus = c.modulus();
138 const Grid gr_copy(gr);
139 gr.add_congruence(c);
140 if (gr.is_empty()) {
141 r.add_disjunct(gr_copy);
142 return true;
143 }
144
145 const Congruence_System cgs = gr.congruences();
146 const Congruence_System cgs_copy = gr_copy.congruences();
147 // When c is an equality, not satisfied by Grid gr
148 // then add gr to the set r. There is no finite
149 // partition in this case.
150 if (c_modulus == 0) {
151 if (cgs.num_equalities() != cgs_copy.num_equalities()) {
152 r.add_disjunct(gr_copy);
153 return false;
154 }
155 return true;
156 }
157
158 // When c is a proper congruence but, in gr, this direction has
159 // no congruence, then add gr to the set r. There is no finite
160 // partition in this case.
161 if (cgs.num_proper_congruences() != cgs_copy.num_proper_congruences()) {
162 r.add_disjunct(gr_copy);
163 return false;
164 }
165
166 // When c is a proper congruence and gr also is discrete
167 // in this direction, then there is a finite partition and that
168 // is added to r.
169 const Coefficient& c_inhomogeneous_term = c.inhomogeneous_term();
170 Linear_Expression le(c.expression());
171 le -= c_inhomogeneous_term;
172 PPL_DIRTY_TEMP_COEFFICIENT(n);
173 rem_assign(n, c_inhomogeneous_term, c_modulus);
174 if (n < 0) {
175 n += c_modulus;
176 }
177 PPL_DIRTY_TEMP_COEFFICIENT(i);
178 for (i = c_modulus; i-- > 0; ) {
179 if (i != n) {
180 Grid gr_tmp(gr_copy);
181 gr_tmp.add_congruence((le+i %= 0) / c_modulus);
182 if (!gr_tmp.is_empty()) {
183 r.add_disjunct(gr_tmp);
184 }
185 }
186 }
187 return true;
188 }
189
190 } // namespace
191
192 /*! \relates Parma_Polyhedra_Library::Pointset_Powerset */
193 std::pair<PPL::Grid, PPL::Pointset_Powerset<PPL::Grid> >
approximate_partition(const Grid & p,const Grid & q,bool & finite_partition)194 PPL::approximate_partition(const Grid& p, const Grid& q,
195 bool& finite_partition) {
196 using namespace PPL;
197 finite_partition = true;
198 Pointset_Powerset<Grid> r(p.space_dimension(), EMPTY);
199 // Ensure that the congruence system of q is minimized
200 // before copying and calling approximate_partition_aux().
201 (void) q.minimized_congruences();
202 Grid gr = q;
203 const Congruence_System& p_congruences = p.congruences();
204 for (Congruence_System::const_iterator i = p_congruences.begin(),
205 p_congruences_end = p_congruences.end();
206 i != p_congruences_end; ++i) {
207 if (!approximate_partition_aux(*i, gr, r)) {
208 finite_partition = false;
209 const Pointset_Powerset<Grid> s(q);
210 return std::make_pair(gr, s);
211 }
212 }
213 return std::make_pair(gr, r);
214 }
215
216 /*! \relates Parma_Polyhedra_Library::Pointset_Powerset */
217 bool
check_containment(const Grid & ph,const Pointset_Powerset<Grid> & ps)218 PPL::check_containment(const Grid& ph,
219 const Pointset_Powerset<Grid>& ps) {
220 if (ph.is_empty()) {
221 return true;
222 }
223 Pointset_Powerset<Grid> tmp(ph.space_dimension(), EMPTY);
224 tmp.add_disjunct(ph);
225 for (Pointset_Powerset<Grid>::const_iterator
226 i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
227 const Grid& pi = i->pointset();
228 for (Pointset_Powerset<Grid>::iterator
229 j = tmp.begin(); j != tmp.end(); ) {
230 const Grid& pj = j->pointset();
231 if (pi.contains(pj)) {
232 j = tmp.drop_disjunct(j);
233 }
234 else {
235 ++j;
236 }
237 }
238 if (tmp.empty()) {
239 return true;
240 }
241 else {
242 Pointset_Powerset<Grid> new_disjuncts(ph.space_dimension(),
243 EMPTY);
244 for (Pointset_Powerset<Grid>::iterator
245 j = tmp.begin(); j != tmp.end(); ) {
246 const Grid& pj = j->pointset();
247 if (pj.is_disjoint_from(pi)) {
248 ++j;
249 }
250 else {
251 bool finite_partition;
252 const std::pair<Grid, Pointset_Powerset<Grid> >
253 partition = approximate_partition(pi, pj, finite_partition);
254
255 // If there is a finite partition, then we add the new
256 // disjuncts to the temporary set of disjuncts and drop pj.
257 // If there is no finite partition, then by the
258 // specification of approximate_partition(), we can
259 // ignore checking the remaining temporary disjuncts as they
260 // will all have the same lines and equalities and therefore
261 // also not have a finite partition with respect to pi.
262 if (!finite_partition) {
263 break;
264 }
265 new_disjuncts.upper_bound_assign(partition.second);
266 j = tmp.drop_disjunct(j);
267 }
268 }
269 tmp.upper_bound_assign(new_disjuncts);
270 }
271 }
272 return false;
273 }
274
275 template <>
276 void
277 PPL::Pointset_Powerset<PPL::Grid>
difference_assign(const Pointset_Powerset & y)278 ::difference_assign(const Pointset_Powerset& y) {
279 Pointset_Powerset& x = *this;
280 using std::swap;
281 // Ensure omega-reduction.
282 x.omega_reduce();
283 y.omega_reduce();
284 Sequence new_sequence = x.sequence;
285 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
286 const Grid& gr_yi = yi->pointset();
287 Sequence tmp_sequence;
288 for (Sequence_const_iterator itr = new_sequence.begin(),
289 ns_end = new_sequence.end(); itr != ns_end; ++itr) {
290 bool finite_partition;
291 const std::pair<Grid, Pointset_Powerset<Grid> > partition
292 = approximate_partition(gr_yi, itr->pointset(), finite_partition);
293 const Pointset_Powerset<Grid>& residues = partition.second;
294 // Append the contents of `residues' to `tmp_sequence'.
295 std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
296 }
297 swap(tmp_sequence, new_sequence);
298 }
299 swap(x.sequence, new_sequence);
300 x.reduced = false;
301 PPL_ASSERT_HEAVY(x.OK());
302 }
303
304 template <>
305 bool
306 PPL::Pointset_Powerset<PPL::Grid>
geometrically_covers(const Pointset_Powerset & y) const307 ::geometrically_covers(const Pointset_Powerset& y) const {
308 const Pointset_Powerset& x = *this;
309 for (const_iterator yi = y.begin(), y_end = y.end();
310 yi != y_end; ++yi) {
311 if (!check_containment(yi->pointset(), x)) {
312 return false;
313 }
314 }
315 return true;
316 }
317
318 template <>
319 template <>
320 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
Pointset_Powerset(const Pointset_Powerset<C_Polyhedron> & y,Complexity_Class)321 ::Pointset_Powerset(const Pointset_Powerset<C_Polyhedron>& y,
322 Complexity_Class)
323 : Base(), space_dim(y.space_dimension()) {
324 Pointset_Powerset& x = *this;
325 for (Pointset_Powerset<C_Polyhedron>::const_iterator i = y.begin(),
326 y_end = y.end(); i != y_end; ++i) {
327 x.sequence.push_back(Determinate<NNC_Polyhedron>
328 (NNC_Polyhedron(i->pointset())));
329 }
330 x.reduced = y.reduced;
331 PPL_ASSERT_HEAVY(x.OK());
332 }
333
334 template <>
335 template <>
336 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
Pointset_Powerset(const Pointset_Powerset<Grid> & y,Complexity_Class)337 ::Pointset_Powerset(const Pointset_Powerset<Grid>& y,
338 Complexity_Class)
339 : Base(), space_dim(y.space_dimension()) {
340 Pointset_Powerset& x = *this;
341 for (Pointset_Powerset<Grid>::const_iterator i = y.begin(),
342 y_end = y.end(); i != y_end; ++i) {
343 x.sequence.push_back(Determinate<NNC_Polyhedron>
344 (NNC_Polyhedron(i->pointset())));
345 }
346 x.reduced = false;
347 PPL_ASSERT_HEAVY(x.OK());
348 }
349
350 template <>
351 template <>
352 PPL::Pointset_Powerset<PPL::C_Polyhedron>
Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron> & y,Complexity_Class)353 ::Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron>& y,
354 Complexity_Class)
355 : Base(), space_dim(y.space_dimension()) {
356 Pointset_Powerset& x = *this;
357 for (Pointset_Powerset<NNC_Polyhedron>::const_iterator i = y.begin(),
358 y_end = y.end(); i != y_end; ++i) {
359 x.sequence.push_back(Determinate<C_Polyhedron>
360 (C_Polyhedron(i->pointset())));
361 }
362
363 // Note: this might be non-reduced even when `y' is known to be
364 // omega-reduced, because the constructor of C_Polyhedron, by
365 // enforcing topological closure, may have made different elements
366 // comparable.
367 x.reduced = false;
368 PPL_ASSERT_HEAVY(x.OK());
369 }
370