PPL  1.2
Constraint_inlines.hh
Go to the documentation of this file.
1 /* Constraint 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_inlines_hh
25 #define PPL_Constraint_inlines_hh 1
26 
28 
29 namespace Parma_Polyhedra_Library {
30 
31 inline bool
33  return (topology_ == NECESSARILY_CLOSED);
34 }
35 
36 inline bool
38  return !is_necessarily_closed();
39 }
40 
44 }
45 
46 inline dimension_type
48  return expression().space_dimension();
49 }
50 
51 inline void
54 }
55 
56 inline bool
58  return (kind_ == LINE_OR_EQUALITY);
59 }
60 
61 inline bool
64 }
65 
66 inline Topology
68  return topology_;
69 }
70 
71 inline void
74 }
75 
76 inline void
79 }
80 
81 inline void
83  if (topology() == x) {
84  return;
85  }
86  if (topology() == NECESSARILY_CLOSED) {
87  // Add a column for the epsilon dimension.
89  }
90  else {
91  PPL_ASSERT(expr.space_dimension() != 0);
93  }
94  topology_ = x;
95 }
96 
97 inline void
99  PPL_ASSERT(is_not_necessarily_closed());
101 }
102 
103 inline void
105  PPL_ASSERT(is_necessarily_closed());
107 }
108 
109 inline void
112 }
113 
114 inline void
117 }
118 
119 inline
121  : expr(r),
122  kind_(RAY_OR_POINT_OR_INEQUALITY),
123  topology_(NECESSARILY_CLOSED) {
124  PPL_ASSERT(OK());
125 }
126 
127 inline
129  Representation r)
130  : expr(r),
131  kind_(kind),
132  topology_(topology) {
133  expr.set_space_dimension(space_dim + 1);
134  PPL_ASSERT(space_dimension() == space_dim);
135  PPL_ASSERT(OK());
136 }
137 
138 inline
140  : kind_(kind),
141  topology_(topology) {
142  PPL_ASSERT(kind != RAY_OR_POINT_OR_INEQUALITY || topology == NOT_NECESSARILY_CLOSED);
143  swap(expr, e);
144  if (topology == NOT_NECESSARILY_CLOSED) {
145  // Add the epsilon dimension.
147  }
149  PPL_ASSERT(OK());
150 }
151 
152 inline
154  : topology_(topology) {
155  PPL_ASSERT(type != STRICT_INEQUALITY || topology == NOT_NECESSARILY_CLOSED);
156  swap(expr, e);
157  if (topology == NOT_NECESSARILY_CLOSED) {
159  }
160  if (type == EQUALITY) {
162  }
163  else {
165  }
167  PPL_ASSERT(OK());
168 }
169 
170 inline
172  : expr(c.expr),
173  kind_(c.kind_),
174  topology_(c.topology_) {
175  // NOTE: This does not call PPL_ASSERT(OK()) because this is called by OK().
176 }
177 
178 inline
180  : expr(c.expr, r),
181  kind_(c.kind_),
182  topology_(c.topology_) {
183  PPL_ASSERT(OK());
184 }
185 
186 inline
188  : expr(c.expr, c.is_necessarily_closed() ? space_dim : (space_dim + 1)),
189  kind_(c.kind_), topology_(c.topology_) {
190  PPL_ASSERT(space_dimension() == space_dim);
191  PPL_ASSERT(OK());
192 }
193 
194 inline
196  Representation r)
197  : expr(c.expr, c.is_necessarily_closed() ? space_dim : (space_dim + 1), r),
198  kind_(c.kind_), topology_(c.topology_) {
199  PPL_ASSERT(space_dimension() == space_dim);
200  PPL_ASSERT(OK());
201 }
202 
203 inline
205 }
206 
207 inline Constraint&
209  Constraint tmp = c;
210  swap(*this, tmp);
211 
212  return *this;
213 }
214 
215 inline Representation
217  return expr.representation();
218 }
219 
220 inline void
223 }
224 
225 inline dimension_type
228 }
229 
230 inline void
232  const dimension_type old_expr_space_dim = expr.space_dimension();
233  if (topology() == NECESSARILY_CLOSED) {
234  expr.set_space_dimension(space_dim);
235  }
236  else {
237  const dimension_type old_space_dim = space_dimension();
238  if (space_dim > old_space_dim) {
239  expr.set_space_dimension(space_dim + 1);
240  expr.swap_space_dimensions(Variable(space_dim), Variable(old_space_dim));
241  }
242  else {
243  expr.swap_space_dimensions(Variable(space_dim), Variable(old_space_dim));
244  expr.set_space_dimension(space_dim + 1);
245  }
246  }
247  PPL_ASSERT(space_dimension() == space_dim);
248  if (expr.space_dimension() < old_expr_space_dim) {
250  }
251 }
252 
253 inline void
255  set_space_dimension_no_ok(space_dim);
256  PPL_ASSERT(OK());
257 }
258 
259 inline bool
262  return true;
263 }
264 
265 inline bool
267  return is_line_or_equality();
268 }
269 
270 inline bool
273 }
274 
275 inline Constraint::Type
277  if (is_equality()) {
278  return EQUALITY;
279  }
280  if (is_necessarily_closed()) {
281  return NONSTRICT_INEQUALITY;
282  }
283  if (epsilon_coefficient() < 0) {
284  return STRICT_INEQUALITY;
285  }
286  else {
287  return NONSTRICT_INEQUALITY;
288  }
289 }
290 
291 inline bool
293  return type() == NONSTRICT_INEQUALITY;
294 }
295 
296 inline bool
298  return type() == STRICT_INEQUALITY;
299 }
300 
301 inline void
304 }
305 
306 inline void
309 }
310 
311 inline Coefficient_traits::const_reference
313  if (v.space_dimension() > space_dimension()) {
314  throw_dimension_incompatible("coefficient(v)", "v", v);
315  }
316  return expr.coefficient(v);
317 }
318 
319 inline Coefficient_traits::const_reference
321  return expr.inhomogeneous_term();
322 }
323 
324 inline memory_size_type
327 }
328 
329 inline memory_size_type
331  return sizeof(*this) + external_memory_in_bytes();
332 }
333 
334 inline void
336  expr.normalize();
337  sign_normalize();
338 }
339 
341 inline bool
342 operator==(const Constraint& x, const Constraint& y) {
343  return x.is_equivalent_to(y);
344 }
345 
347 inline bool
348 operator!=(const Constraint& x, const Constraint& y) {
349  return !x.is_equivalent_to(y);
350 }
351 
353 inline Constraint
355  Linear_Expression diff(e1,
356  std::max(e1.space_dimension(), e2.space_dimension()),
358  diff -= e2;
360 }
361 
363 inline Constraint
365  if (v1.space_dimension() > v2.space_dimension()) {
366  swap(v1, v2);
367  }
368  PPL_ASSERT(v1.space_dimension() <= v2.space_dimension());
369 
371  diff -= v2;
373 }
374 
376 inline Constraint
378  Linear_Expression diff(e1,
379  std::max(e1.space_dimension(), e2.space_dimension()),
381  diff -= e2;
383 }
384 
386 inline Constraint
387 operator>=(const Variable v1, const Variable v2) {
389  diff.set_space_dimension(std::max(v1.space_dimension(),
390  v2.space_dimension()));
391  diff += v1;
392  diff -= v2;
394 }
395 
397 inline Constraint
400  diff -= e2;
402 
403  // NOTE: this also enforces normalization.
405  PPL_ASSERT(c.OK());
406 
407  return c;
408 }
409 
411 inline Constraint
412 operator>(const Variable v1, const Variable v2) {
414  diff.set_space_dimension(std::max(v1.space_dimension(),
415  v2.space_dimension()));
416  diff += v1;
417  diff -= v2;
419 
421  PPL_ASSERT(c.OK());
422 
423  return c;
424 }
425 
427 inline Constraint
428 operator==(Coefficient_traits::const_reference n, const Linear_Expression& e) {
430  neg_assign(diff);
431  diff += n;
433 }
434 
436 inline Constraint
437 operator>=(Coefficient_traits::const_reference n, const Linear_Expression& e) {
439  neg_assign(diff);
440  diff += n;
442 }
443 
445 inline Constraint
446 operator>(Coefficient_traits::const_reference n, const Linear_Expression& e) {
448  neg_assign(diff);
449  diff += n;
451 
452  // NOTE: this also enforces normalization.
454  PPL_ASSERT(c.OK());
455 
456  return c;
457 }
458 
460 inline Constraint
461 operator==(const Linear_Expression& e, Coefficient_traits::const_reference n) {
463  diff -= n;
465 }
466 
468 inline Constraint
469 operator>=(const Linear_Expression& e, Coefficient_traits::const_reference n) {
471  diff -= n;
473 }
474 
476 inline Constraint
477 operator>(const Linear_Expression& e, Coefficient_traits::const_reference n) {
479  diff -= n;
481 
482  // NOTE: this also enforces normalization.
484  PPL_ASSERT(c.OK());
485 
486  return c;
487 }
488 
490 inline Constraint
492  return e2 >= e1;
493 }
494 
496 inline Constraint
497 operator<=(const Variable v1, const Variable v2) {
498  return v2 >= v1;
499 }
500 
502 inline Constraint
503 operator<=(Coefficient_traits::const_reference n, const Linear_Expression& e) {
504  return e >= n;
505 }
506 
508 inline Constraint
509 operator<=(const Linear_Expression& e, Coefficient_traits::const_reference n) {
510  return n >= e;
511 }
512 
514 inline Constraint
516  return e2 > e1;
517 }
518 
520 inline Constraint
521 operator<(const Variable v1, const Variable v2) {
522  return v2 > v1;
523 }
524 
526 inline Constraint
527 operator<(Coefficient_traits::const_reference n, const Linear_Expression& e) {
528  return e > n;
529 }
530 
532 inline Constraint
533 operator<(const Linear_Expression& e, Coefficient_traits::const_reference n) {
534  return n > e;
535 }
536 
537 inline const Constraint&
539  PPL_ASSERT(zero_dim_false_p != 0);
540  return *zero_dim_false_p;
541 }
542 
543 inline const Constraint&
545  PPL_ASSERT(zero_dim_positivity_p != 0);
546  return *zero_dim_positivity_p;
547 }
548 
549 inline const Constraint&
551  PPL_ASSERT(epsilon_geq_zero_p != 0);
552  return *epsilon_geq_zero_p;
553 }
554 
555 inline const Constraint&
557  PPL_ASSERT(epsilon_leq_one_p != 0);
558  return *epsilon_leq_one_p;
559 }
560 
561 inline void
563  using std::swap;
564  swap(expr, y.expr);
565  swap(kind_, y.kind_);
567 }
568 
569 inline Coefficient_traits::const_reference
571  PPL_ASSERT(is_not_necessarily_closed());
573 }
574 
575 inline void
576 Constraint::set_epsilon_coefficient(Coefficient_traits::const_reference n) {
577  PPL_ASSERT(is_not_necessarily_closed());
579 }
580 
582 inline void
584  x.m_swap(y);
585 }
586 
587 } // namespace Parma_Polyhedra_Library
588 
589 #endif // !defined(PPL_Constraint_inlines_hh)
Expression_Hide_Last< Linear_Expression > expr_type
The type of the (adapted) internal expression.
memory_size_type total_memory_in_bytes() const
Returns a lower bound to the total size in bytes of the memory occupied by *this. ...
Constraint operator>(const Linear_Expression &e, Coefficient_traits::const_reference n)
void shift_space_dimensions(Variable v, dimension_type n)
void throw_dimension_incompatible(const char *method, const char *name_var, Variable v) const
Throws a std::invalid_argument exception containing the appropriate error message.
Definition: Constraint.cc:47
A linear equality or inequality.
bool is_equality() const
Returns true if and only if *this is an equality constraint.
void swap(CO_Tree &x, CO_Tree &y)
static const Constraint * zero_dim_false_p
Holds (between class initialization and finalization) a pointer to the unsatisfiable (zero-dimension ...
void set_space_dimension(dimension_type n)
Sets the dimension of the vector space enclosing *this to n .
void set_not_necessarily_closed()
Sets to NOT_NECESSARILY_CLOSED the topological kind of *this row.
Constraint(Representation r=default_representation)
Constructs the constraint.
void m_swap(Constraint &y)
Swaps *this with y.
size_t dimension_type
An unsigned integral type for representing space dimensions.
Type type() const
Returns the constraint type of *this.
static const Constraint * epsilon_geq_zero_p
Holds (between class initialization and finalization) a pointer to the zero-dimension space constrain...
bool is_necessarily_closed() const
Returns true if and only if the topology of *this row is necessarily closed.
An std::set of variables' indexes.
void mark_as_necessarily_closed()
Marks the epsilon dimension as a standard dimension.
Coefficient_traits::const_reference inhomogeneous_term() const
Returns the inhomogeneous term of *this.
bool operator!=(const Constraint &x, const Constraint &y)
static const Constraint & zero_dim_false()
The unsatisfiable (zero-dimension space) constraint .
Representation representation() const
Returns the current representation of *this.
bool is_line_or_equality() const
Returns true if and only if *this row represents a line or an equality.
bool operator==(const Constraint &x, const Constraint &y)
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
void set_is_equality()
Sets the constraint type to EQUALITY.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
void set_coefficient(Variable v, Coefficient_traits::const_reference n)
Sets the coefficient of v in *this to n.
Coefficient_traits::const_reference coefficient(Variable v) const
Returns the coefficient of v in *this.
bool is_equivalent_to(const Constraint &y) const
Returns true if and only if *this and y are equivalent constraints.
Definition: Constraint.cc:208
Coefficient_traits::const_reference coefficient(Variable v) const
Returns the coefficient of v in *this.
Constraint operator==(const Linear_Expression &e, Coefficient_traits::const_reference n)
A dimension of the vector space.
bool is_strict_inequality() const
Returns true if and only if *this is a strict inequality constraint.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Linear_Expression can handle.
void set_space_dimension(dimension_type space_dim)
Constraint & operator=(const Constraint &c)
Assignment operator.
bool is_inequality() const
Returns true if and only if *this is an inequality constraint (either strict or non-strict).
void set_representation(Representation r)
Converts *this to the specified representation.
void set_necessarily_closed()
Sets to NECESSARILY_CLOSED the topological kind of *this row.
static const Constraint & epsilon_geq_zero()
Returns the zero-dimension space constraint .
Constraint operator==(Coefficient_traits::const_reference n, const Linear_Expression &e)
bool operator<(const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
void set_is_ray_or_point_or_inequality()
Sets to RAY_OR_POINT_OR_INEQUALITY the kind of *this row.
bool is_not_necessarily_closed() const
Returns true if and only if the topology of *this row is not necessarily closed.
void swap_space_dimensions(Variable v1, Variable v2)
Swaps the coefficients of the variables v1 and v2 .
void set_representation(Representation r)
Converts *this to the specified representation.
void set_epsilon_coefficient(Coefficient_traits::const_reference n)
Sets the epsilon coefficient to n. The constraint must be NNC.
static const Constraint * zero_dim_positivity_p
Holds (between class initialization and finalization) a pointer to the true (zero-dimension space) co...
static const Representation default_representation
The representation used for new Constraints.
bool is_ray_or_point_or_inequality() const
Returns true if and only if *this row represents a ray, a point or an inequality. ...
Constraint operator>(const Variable v1, const Variable v2)
void remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the expression.
void neg_assign(GMP_Integer &x)
The entire library is confined to this namespace.
Definition: version.hh:61
Representation representation() const
Returns the current representation of *this.
Constraint operator>(const Linear_Expression &e1, const Linear_Expression &e2)
void set_is_line_or_equality()
Sets to LINE_OR_EQUALITY the kind of *this row.
Constraint operator>=(const Linear_Expression &e, Coefficient_traits::const_reference n)
void set_is_inequality()
Sets the constraint to be an inequality.
static const Constraint & epsilon_leq_one()
The zero-dimension space constraint (used to implement NNC polyhedra).
Coefficient_traits::const_reference epsilon_coefficient() const
Returns the epsilon coefficient. The constraint must be NNC.
static const Constraint * epsilon_leq_one_p
Holds (between class initialization and finalization) a pointer to the zero-dimension space constrain...
static const Constraint & zero_dim_positivity()
The true (zero-dimension space) constraint , also known as positivity constraint. ...
void set_topology(Topology x)
Sets to x the topological kind of *this row.
Constraint operator==(Variable v1, Variable v2)
bool operator<=(const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
void strong_normalize()
Strong normalization: ensures that different Constraint objects represent different hyperplanes or hy...
Constraint operator>=(const Variable v1, const Variable v2)
bool OK() const
Checks if all the invariants are satisfied.
Definition: Constraint.cc:467
Constraint operator>(Coefficient_traits::const_reference n, const Linear_Expression &e)
void set_space_dimension_no_ok(dimension_type space_dim)
Kind
The possible kinds of Constraint objects.
size_t memory_size_type
An unsigned integral type for representing memory size in bytes.
bool is_nonstrict_inequality() const
Returns true if and only if *this is a non-strict inequality constraint.
Coefficient c
Definition: PIP_Tree.cc:64
Coefficient_traits::const_reference inhomogeneous_term() const
Returns the inhomogeneous term of *this.
expr_type expression() const
Partial read access to the (adapted) internal expression.
static dimension_type max_space_dimension()
Returns the maximum space dimension a Constraint can handle.
Constraint operator>=(const Linear_Expression &e1, const Linear_Expression &e2)
bool remove_space_dimensions(const Variables_Set &vars)
Removes all the specified dimensions from the constraint.
Topology topology() const
Returns the topological kind of *this.
Constraint operator==(const Linear_Expression &e1, const Linear_Expression &e2)
Constraint operator>=(Coefficient_traits::const_reference n, const Linear_Expression &e)
memory_size_type external_memory_in_bytes() const
Returns the size in bytes of the memory managed by *this.
memory_size_type external_memory_in_bytes() const
Returns the size in bytes of the memory managed by *this.
void mark_as_not_necessarily_closed()
Marks the last dimension as the epsilon dimension.
void sign_normalize()
Normalizes the sign of the coefficients so that the first non-zero (homogeneous) coefficient of a lin...
Definition: Constraint.cc:252
An adapter for Linear_Expression that maybe hides the last coefficient.
Topology
Kinds of polyhedra domains.
void swap(Constraint &x, Constraint &y)
void shift_space_dimensions(Variable v, dimension_type n)