PPL  1.2
Constraint_System_inlines.hh
Go to the documentation of this file.
1 /* Constraint_System class implementation: 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 #ifndef PPL_Constraint_System_inlines_hh
25 #define PPL_Constraint_System_inlines_hh 1
26 
27 #include "Constraint_defs.hh"
28 
29 namespace Parma_Polyhedra_Library {
30 
31 inline
33  : sys(NECESSARILY_CLOSED, r) {
34 }
35 
36 inline
38  : sys(c.topology(), r) {
39  sys.insert(c);
40 }
41 
42 inline
44  : sys(cs.sys) {
45 }
46 
47 inline
50  : sys(cs.sys, r) {
51 }
52 
53 inline
55  : sys(topol, r) {
56 }
57 
58 inline
60  const dimension_type space_dim,
62  : sys(topol, space_dim, r) {
63 }
64 
65 inline
67 }
68 
69 inline Constraint_System&
71  Constraint_System tmp = y;
72  swap(*this, tmp);
73  return *this;
74 }
75 
76 inline const Constraint&
78  return sys[k];
79 }
80 
81 inline Representation
83  return sys.representation();
84 }
85 
86 inline void
88  sys.set_representation(r);
89 }
90 
91 inline dimension_type
94 }
95 
96 inline dimension_type
98  return sys.space_dimension();
99 }
100 
101 inline void
103  return sys.set_space_dimension(space_dim);
104 }
105 
106 inline void
108  sys.clear();
109 }
110 
111 inline const Constraint_System&
113  PPL_ASSERT(zero_dim_empty_p != 0);
114  return *zero_dim_empty_p;
115 }
116 
117 inline
119  : i(), csp(0) {
120 }
121 
122 inline
124  : i(y.i), csp(y.csp) {
125 }
126 
127 inline
129 }
130 
133  i = y.i;
134  csp = y.csp;
135  return *this;
136 }
137 
138 inline const Constraint&
140  return *i;
141 }
142 
143 inline const Constraint*
145  return i.operator->();
146 }
147 
150  ++i;
151  skip_forward();
152  return *this;
153 }
154 
157  const Constraint_System_const_iterator tmp = *this;
158  operator++();
159  return tmp;
160 }
161 
162 inline bool
164  return i == y.i;
165 }
166 
167 inline bool
169  return i != y.i;
170 }
171 
172 inline
175  const Constraint_System& cs)
176  : i(iter), csp(&cs.sys) {
177 }
178 
181  const_iterator i(sys.begin(), *this);
182  i.skip_forward();
183  return i;
184 }
185 
188  const Constraint_System_const_iterator i(sys.end(), *this);
189  return i;
190 }
191 
192 inline bool
194  return begin() == end();
195 }
196 
197 inline void
199  if (sys.is_necessarily_closed()) {
200  // The positivity constraint.
202  }
203  else {
204  // Add the epsilon constraints.
207  }
208 }
209 
210 inline void
212  swap(sys, y.sys);
213 }
214 
215 inline memory_size_type
217  return sys.external_memory_in_bytes();
218 }
219 
220 inline memory_size_type
222  return external_memory_in_bytes() + sizeof(*this);
223 }
224 
225 inline void
227  sys.simplify();
228 }
229 
230 inline Topology
232  return sys.topology();
233 }
234 
235 inline dimension_type
237  return sys.num_rows();
238 }
239 
240 inline bool
242  return sys.is_necessarily_closed();
243 }
244 
245 inline dimension_type
247  return sys.num_pending_rows();
248 }
249 
250 inline dimension_type
252  return sys.first_pending_row();
253 }
254 
255 inline bool
257  return sys.is_sorted();
258 }
259 
260 inline void
262  sys.unset_pending_rows();
263 }
264 
265 inline void
267  sys.set_index_first_pending_row(i);
268 }
269 
270 inline void
272  sys.set_sorted(b);
273 }
274 
275 inline void
277  sys.remove_row(i, keep_sorted);
278 }
279 
280 inline void
282  bool keep_sorted) {
283  sys.remove_rows(first, last, keep_sorted);
284 }
285 
286 inline void
287 Constraint_System::remove_rows(const std::vector<dimension_type>& indexes) {
288  sys.remove_rows(indexes);
289 }
290 
291 inline void
293  sys.remove_trailing_rows(n);
294 }
295 
296 inline void
299  sys.remove_space_dimensions(vars);
300 }
301 
302 inline void
305  sys.shift_space_dimensions(v, n);
306 }
307 
308 inline void
310 ::permute_space_dimensions(const std::vector<Variable>& cycle) {
311  sys.permute_space_dimensions(cycle);
312 }
313 
314 inline void
317  sys.swap_space_dimensions(v1, v2);
318 }
319 
320 inline bool
322  return sys.has_no_rows();
323 }
324 
325 inline void
327  sys.strong_normalize();
328 }
329 
330 inline void
332  sys.sort_rows();
333 }
334 
335 inline void
337  sys.insert_pending(r.sys, Recycle_Input());
338 }
339 
340 inline void
342  sys.insert(r.sys, Recycle_Input());
343 }
344 
345 inline void
347  sys.insert_pending(r.sys);
348 }
349 
350 inline void
352  sys.merge_rows_assign(y.sys);
353 }
354 
355 inline void
357  sys.insert(y.sys);
358 }
359 
360 inline void
362  sys.mark_as_necessarily_closed();
363 }
364 
365 inline void
367  sys.mark_as_not_necessarily_closed();
368 }
369 
370 inline dimension_type
371 Constraint_System::gauss(dimension_type n_lines_or_equalities) {
372  return sys.gauss(n_lines_or_equalities);
373 }
374 
375 inline void
377  sys.back_substitute(n_lines_or_equalities);
378 }
379 
380 inline void
382  sys.assign_with_pending(y.sys);
383 }
384 
385 inline void
387  sys.sort_pending_and_remove_duplicates();
388 }
389 
390 inline void
392  sys.sort_and_remove_with_sat(sat);
393 }
394 
395 inline bool
397  return sys.check_sorted();
398 }
399 
400 inline dimension_type
402  return sys.num_lines_or_equalities();
403 }
404 
405 inline void
407  sys.add_universe_rows_and_space_dimensions(n);
408 }
409 
410 inline bool
412  return x.sys == y.sys;
413 }
414 
415 inline bool
417  return !(x == y);
418 }
419 
421 inline void
423  x.m_swap(y);
424 }
425 
426 namespace Implementation {
427 
428 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
429 
430 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
431 inline dimension_type
433  return static_cast<dimension_type>(std::distance(cs.begin(), cs.end()));
434 }
435 
436 } // namespace Implementation
437 
438 } // namespace Parma_Polyhedra_Library
439 
440 #endif // !defined(PPL_Constraint_System_inlines_hh)
void m_swap(Constraint_System &y)
Swaps *this with y.
bool operator!=(const Box< ITV > &x, const Box< ITV > &y)
Definition: Box_inlines.hh:264
void shift_space_dimensions(Variable v, dimension_type n)
A linear equality or inequality.
memory_size_type total_memory_in_bytes() const
Returns the total size in bytes of the memory occupied by *this.
void insert_pending(const Constraint &c)
Inserts in *this a copy of the constraint c, increasing the number of space dimensions if needed...
void set_representation(Representation r)
Converts *this to the specified representation.
bool check_sorted() const
Returns true if and only if *this is sorted, without checking for duplicates.
size_t dimension_type
An unsigned integral type for representing space dimensions.
void set_space_dimension(dimension_type space_dim)
Sets the space dimension of the rows in the system to space_dim .
An std::set of variables' indexes.
bool operator!=(const Constraint_System_const_iterator &y) const
Returns true if and only if *this and y are different.
void simplify()
Applies Gaussian elimination and back-substitution so as to provide a partial simplification of the s...
bool is_necessarily_closed() const
Returns true if and only if the system topology is NECESSARILY_CLOSED.
void merge_rows_assign(const Constraint_System &y)
Assigns to *this the result of merging its rows with those of y, obtaining a sorted system...
void assign_with_pending(const Constraint_System &y)
Full assignment operator: pending rows are copied as pending.
const Constraint * operator->() const
Indirect member selector.
dimension_type first_pending_row() const
Returns the index of the first pending row.
static const Constraint_System & zero_dim_empty()
Returns the singleton system containing only Constraint::zero_dim_false().
void insert(const Constraint &c)
Inserts in *this a copy of the constraint c, increasing the number of space dimensions if needed...
Linear_System< Constraint >::const_iterator i
The const iterator over the matrix of constraints.
void add_universe_rows_and_space_dimensions(dimension_type n)
Adds n rows and space dimensions to the system.
dimension_type num_pending_rows() const
Returns the number of rows that are in the pending part of the system.
bool is_sorted() const
Returns the value of the sortedness flag.
Representation representation() const
Returns the current representation of *this.
Topology topology() const
Returns the system topology.
void clear()
Removes all the constraints from the constraint system and sets its space dimension to 0...
const_iterator begin() const
Returns the const_iterator pointing to the first constraint, if *this is not empty; otherwise...
const Linear_System< Constraint > * csp
A const pointer to the matrix of constraints.
void mark_as_not_necessarily_closed()
Marks the last dimension as the epsilon dimension.
bool operator==(const Constraint_System_const_iterator &y) const
Returns true if and only if *this and y are identical.
A dimension of the vector space.
Constraint_System_const_iterator & operator=(const Constraint_System_const_iterator &y)
Assignment operator.
void remove_row(dimension_type i, bool keep_sorted=false)
Makes the system shrink by removing its i-th row.
void skip_forward()
*this skips to the next non-trivial constraint.
void permute_space_dimensions(const std::vector< Variable > &cycle)
Permutes the space dimensions of the matrix.
static const Constraint & epsilon_geq_zero()
Returns the zero-dimension space constraint .
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
bool empty() const
Returns true if and only if *this has no constraints.
const_iterator end() const
Returns the past-the-end const_iterator.
memory_size_type external_memory_in_bytes() const
Returns the size in bytes of the memory managed by *this.
dimension_type num_lines_or_equalities() const
Returns the number of rows in the system that represent either lines or equalities.
void sort_and_remove_with_sat(Bit_Matrix &sat)
Sorts the system, removing duplicates, keeping the saturation matrix consistent.
static const Constraint_System * zero_dim_empty_p
Holds (between class initialization and finalization) a pointer to the singleton system containing on...
const Constraint & operator[](dimension_type k) const
Returns a constant reference to the k- th constraint of the system.
Swapping_Vector< Row >::const_iterator const_iterator
void sort_rows()
Sorts the non-pending rows (in growing order) and eliminates duplicated ones.
dimension_type num_constraints(const Constraint_System &cs)
Constraint_System_const_iterator & operator++()
Prefix increment operator.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Constraint_System can handle.
void remove_rows(const std::vector< dimension_type > &indexes)
The entire library is confined to this namespace.
Definition: version.hh:61
void remove_trailing_rows(dimension_type n)
Makes the system shrink by removing its n trailing rows.
void remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the constraint system.
void strong_normalize()
Strongly normalizes the system.
static const Constraint & epsilon_leq_one()
The zero-dimension space constraint (used to implement NNC polyhedra).
static const Constraint & zero_dim_positivity()
The true (zero-dimension space) constraint , also known as positivity constraint. ...
Constraint_System(Representation r=default_representation)
Default constructor: builds an empty system of constraints.
void unset_pending_rows()
Sets the index to indicate that the system has no pending rows.
void add_low_level_constraints()
Adds low-level constraints to the constraint system.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Linear_System can handle.
bool operator==(const Box< ITV > &x, const Box< ITV > &y)
const Constraint & operator*() const
Dereference operator.
void set_sorted(bool b)
Sets the sortedness flag of the system to b.
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
Coefficient c
Definition: PIP_Tree.cc:64
Constraint_System & operator=(const Constraint_System &y)
Assignment operator.
void sort_pending_and_remove_duplicates()
Sorts the pending rows and eliminates those that also occur in the non-pending part of the system...
void back_substitute(dimension_type n_lines_or_equalities)
Back-substitutes the coefficients to reduce the complexity of the system.
void set_index_first_pending_row(dimension_type i)
Sets the index of the first pending row to i.
void swap_space_dimensions(Variable v1, Variable v2)
Swaps the coefficients of the variables v1 and v2 .
void mark_as_necessarily_closed()
Marks the epsilon dimension as a standard dimension.
dimension_type gauss(dimension_type n_lines_or_equalities)
Minimizes the subsystem of equations contained in *this.
Topology
Kinds of polyhedra domains.
void swap(Constraint_System &x, Constraint_System &y)