1 /* Constraint class declaration.
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_defs_hh
25 #define PPL_Constraint_defs_hh 1
26 
27 #include "Constraint_types.hh"
28 
29 #include "Congruence_types.hh"
30 #include "Variables_Set_types.hh"
31 #include "Polyhedron_types.hh"
32 #include "termination_types.hh"
33 #include "Octagonal_Shape_types.hh"
34 #include "Grid_types.hh"
35 
36 #include "Linear_Expression_defs.hh"
37 #include "Variable_defs.hh"
38 #include "Topology_types.hh"
39 #include "Expression_Hide_Last_defs.hh"
40 
41 #include <iosfwd>
42 
43 namespace Parma_Polyhedra_Library {
44 
45 //! Returns the constraint \p e1 \< \p e2.
46 /*! \relates Constraint */
47 Constraint
48 operator<(const Linear_Expression& e1, const Linear_Expression& e2);
49 
50 //! Returns the constraint \p v1 \< \p v2.
51 /*! \relates Constraint */
52 Constraint
53 operator<(Variable v1, Variable v2);
54 
55 //! Returns the constraint \p e \< \p n.
56 /*! \relates Constraint */
57 Constraint
58 operator<(const Linear_Expression& e, Coefficient_traits::const_reference n);
59 
60 //! Returns the constraint \p n \< \p e.
61 /*! \relates Constraint */
62 Constraint
63 operator<(Coefficient_traits::const_reference n, const Linear_Expression& e);
64 
65 //! Returns the constraint \p e1 \> \p e2.
66 /*! \relates Constraint */
67 Constraint
68 operator>(const Linear_Expression& e1, const Linear_Expression& e2);
69 
70 //! Returns the constraint \p v1 \> \p v2.
71 /*! \relates Constraint */
72 Constraint
73 operator>(Variable v1, Variable v2);
74 
75 //! Returns the constraint \p e \> \p n.
76 /*! \relates Constraint */
77 Constraint
78 operator>(const Linear_Expression& e, Coefficient_traits::const_reference n);
79 
80 //! Returns the constraint \p n \> \p e.
81 /*! \relates Constraint */
82 Constraint
83 operator>(Coefficient_traits::const_reference n, const Linear_Expression& e);
84 
85 //! Returns the constraint \p e1 = \p e2.
86 /*! \relates Constraint */
87 Constraint
88 operator==(const Linear_Expression& e1, const Linear_Expression& e2);
89 
90 //! Returns the constraint \p v1 = \p v2.
91 /*! \relates Constraint */
92 Constraint
93 operator==(Variable v1, Variable v2);
94 
95 //! Returns the constraint \p e = \p n.
96 /*! \relates Constraint */
97 Constraint
98 operator==(const Linear_Expression& e, Coefficient_traits::const_reference n);
99 
100 //! Returns the constraint \p n = \p e.
101 /*! \relates Constraint */
102 Constraint
103 operator==(Coefficient_traits::const_reference n, const Linear_Expression& e);
104 
105 //! Returns the constraint \p e1 \<= \p e2.
106 /*! \relates Constraint */
107 Constraint
108 operator<=(const Linear_Expression& e1, const Linear_Expression& e2);
109 
110 //! Returns the constraint \p v1 \<= \p v2.
111 /*! \relates Constraint */
112 Constraint
113 operator<=(Variable v1, Variable v2);
114 
115 //! Returns the constraint \p e \<= \p n.
116 /*! \relates Constraint */
117 Constraint
118 operator<=(const Linear_Expression& e, Coefficient_traits::const_reference n);
119 
120 //! Returns the constraint \p n \<= \p e.
121 /*! \relates Constraint */
122 Constraint
123 operator<=(Coefficient_traits::const_reference n, const Linear_Expression& e);
124 
125 //! Returns the constraint \p e1 \>= \p e2.
126 /*! \relates Constraint */
127 Constraint
128 operator>=(const Linear_Expression& e1, const Linear_Expression& e2);
129 
130 //! Returns the constraint \p v1 \>= \p v2.
131 /*! \relates Constraint */
132 Constraint
133 operator>=(Variable v1, Variable v2);
134 
135 //! Returns the constraint \p e \>= \p n.
136 /*! \relates Constraint */
137 Constraint
138 operator>=(const Linear_Expression& e, Coefficient_traits::const_reference n);
139 
140 //! Returns the constraint \p n \>= \p e.
141 /*! \relates Constraint */
142 Constraint
143 operator>=(Coefficient_traits::const_reference n, const Linear_Expression& e);
144 
145 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
146 //! The basic comparison function.
147 /*! \relates Constraint
148   \return
149   The returned absolute value can be \f$0\f$, \f$1\f$ or \f$2\f$.
150 
151   \param x
152   A row of coefficients;
153 
154   \param y
155   Another row.
156 
157   Compares \p x and \p y, where \p x and \p y may be of different size,
158   in which case the "missing" coefficients are assumed to be zero.
159   The comparison is such that:
160   -# equalities are smaller than inequalities;
161   -# lines are smaller than points and rays;
162   -# the ordering is lexicographic;
163   -# the positions compared are, in decreasing order of significance,
164      1, 2, ..., \p size(), 0;
165   -# the result is negative, zero, or positive if x is smaller than,
166      equal to, or greater than y, respectively;
167   -# when \p x and \p y are different, the absolute value of the
168      result is 1 if the difference is due to the coefficient in
169      position 0; it is 2 otherwise.
170 
171   When \p x and \p y represent the hyper-planes associated
172   to two equality or inequality constraints, the coefficient
173   at 0 is the known term.
174   In this case, the return value can be characterized as follows:
175   - -2, if \p x is smaller than \p y and they are \e not parallel;
176   - -1, if \p x is smaller than \p y and they \e are parallel;
177   -  0, if \p x and y are equal;
178   - +1, if \p y is smaller than \p x and they \e are parallel;
179   - +2, if \p y is smaller than \p x and they are \e not parallel.
180 */
181 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
182 int compare(const Constraint& x, const Constraint& y);
183 
184 }
185 
186 //! A linear equality or inequality.
187 /*! \ingroup PPL_CXX_interface
188   An object of the class Constraint is either:
189   - an equality: \f$\sum_{i=0}^{n-1} a_i x_i + b = 0\f$;
190   - a non-strict inequality: \f$\sum_{i=0}^{n-1} a_i x_i + b \geq 0\f$; or
191   - a strict inequality: \f$\sum_{i=0}^{n-1} a_i x_i + b > 0\f$;
192 
193   where \f$n\f$ is the dimension of the space,
194   \f$a_i\f$ is the integer coefficient of variable \f$x_i\f$
195   and \f$b\f$ is the integer inhomogeneous term.
196 
197   \par How to build a constraint
198   Constraints are typically built by applying a relation symbol
199   to a pair of linear expressions.
200   Available relation symbols are equality (<CODE>==</CODE>),
201   non-strict inequalities (<CODE>\>=</CODE> and <CODE>\<=</CODE>) and
202   strict inequalities (<CODE>\<</CODE> and <CODE>\></CODE>).
203   The space dimension of a constraint is defined as the maximum
204   space dimension of the arguments of its constructor.
205 
206   \par
207   In the following examples it is assumed that variables
208   <CODE>x</CODE>, <CODE>y</CODE> and <CODE>z</CODE>
209   are defined as follows:
210   \code
211   Variable x(0);
212   Variable y(1);
213   Variable z(2);
214   \endcode
215 
216   \par Example 1
217   The following code builds the equality constraint
218   \f$3x + 5y - z = 0\f$, having space dimension \f$3\f$:
219   \code
220   Constraint eq_c(3*x + 5*y - z == 0);
221   \endcode
222   The following code builds the (non-strict) inequality constraint
223   \f$4x \geq 2y - 13\f$, having space dimension \f$2\f$:
224   \code
225   Constraint ineq_c(4*x >= 2*y - 13);
226   \endcode
227   The corresponding strict inequality constraint
228   \f$4x > 2y - 13\f$ is obtained as follows:
229   \code
230   Constraint strict_ineq_c(4*x > 2*y - 13);
231   \endcode
232   An unsatisfiable constraint on the zero-dimension space \f$\Rset^0\f$
233   can be specified as follows:
234   \code
235   Constraint false_c = Constraint::zero_dim_false();
236   \endcode
237   Equivalent, but more involved ways are the following:
238   \code
239   Constraint false_c1(Linear_Expression::zero() == 1);
240   Constraint false_c2(Linear_Expression::zero() >= 1);
241   Constraint false_c3(Linear_Expression::zero() > 0);
242   \endcode
243   In contrast, the following code defines an unsatisfiable constraint
244   having space dimension \f$3\f$:
245   \code
246   Constraint false_c(0*z == 1);
247   \endcode
248 
249   \par How to inspect a constraint
250   Several methods are provided to examine a constraint and extract
251   all the encoded information: its space dimension, its type
252   (equality, non-strict inequality, strict inequality) and
253   the value of its integer coefficients.
254 
255   \par Example 2
256   The following code shows how it is possible to access each single
257   coefficient of a constraint. Given an inequality constraint
258   (in this case \f$x - 5y + 3z \leq 4\f$), we construct a new constraint
259   corresponding to its complement (thus, in this case we want to obtain
260   the strict inequality constraint \f$x - 5y + 3z > 4\f$).
261   \code
262   Constraint c1(x - 5*y + 3*z <= 4);
263   cout << "Constraint c1: " << c1 << endl;
264   if (c1.is_equality())
265     cout << "Constraint c1 is not an inequality." << endl;
266   else {
267     Linear_Expression e;
268     for (dimension_type i = c1.space_dimension(); i-- > 0; )
269       e += c1.coefficient(Variable(i)) * Variable(i);
270     e += c1.inhomogeneous_term();
271     Constraint c2 = c1.is_strict_inequality() ? (e <= 0) : (e < 0);
272     cout << "Complement c2: " << c2 << endl;
273   }
274   \endcode
275   The actual output is the following:
276   \code
277   Constraint c1: -A + 5*B - 3*C >= -4
278   Complement c2: A - 5*B + 3*C > 4
279   \endcode
280   Note that, in general, the particular output obtained can be
281   syntactically different from the (semantically equivalent)
282   constraint considered.
283 */
284 class Parma_Polyhedra_Library::Constraint {
285 public:
286 
287   //! The constraint type.
288   enum Type {
289     /*! The constraint is an equality. */
290     EQUALITY,
291     /*! The constraint is a non-strict inequality. */
292     NONSTRICT_INEQUALITY,
293     /*! The constraint is a strict inequality. */
294     STRICT_INEQUALITY
295   };
296 
297   //! The representation used for new Constraints.
298   /*!
299     \note The copy constructor and the copy constructor with specified size
300           use the representation of the original object, so that it is
301           indistinguishable from the original object.
302   */
303   static const Representation default_representation = SPARSE;
304 
305   //! Constructs the \f$0<=0\f$ constraint.
306   explicit Constraint(Representation r = default_representation);
307 
308   //! Ordinary copy constructor.
309   /*!
310     \note The new Constraint will have the same representation as `c',
311           not default_representation, so that they are indistinguishable.
312   */
313   Constraint(const Constraint& c);
314 
315   //! Copy constructor with given size.
316   /*!
317     \note The new Constraint will have the same representation as `c',
318           not default_representation, so that they are indistinguishable.
319   */
320   Constraint(const Constraint& c, dimension_type space_dim);
321 
322   //! Copy constructor with given representation.
323   Constraint(const Constraint& c, Representation r);
324 
325   //! Copy constructor with given size and representation.
326   Constraint(const Constraint& c, dimension_type space_dim,
327              Representation r);
328 
329   //! Copy-constructs from equality congruence \p cg.
330   /*!
331     \exception std::invalid_argument
332     Thrown if \p cg is a proper congruence.
333   */
334   explicit Constraint(const Congruence& cg,
335                       Representation r = default_representation);
336 
337   //! Destructor.
338   ~Constraint();
339 
340   //! Returns the current representation of *this.
341   Representation representation() const;
342 
343   //! Converts *this to the specified representation.
344   void set_representation(Representation r);
345 
346   //! Assignment operator.
347   Constraint& operator=(const Constraint& c);
348 
349   //! Returns the maximum space dimension a Constraint can handle.
350   static dimension_type max_space_dimension();
351 
352   //! Returns the dimension of the vector space enclosing \p *this.
353   dimension_type space_dimension() const;
354 
355   //! Sets the dimension of the vector space enclosing \p *this to
356   //! \p space_dim .
357   void set_space_dimension(dimension_type space_dim);
358 
359   //! Swaps the coefficients of the variables \p v1 and \p v2 .
360   void swap_space_dimensions(Variable v1, Variable v2);
361 
362   //! Removes all the specified dimensions from the constraint.
363   /*!
364     The space dimension of the variable with the highest space
365     dimension in \p vars must be at most the space dimension
366     of \p this.
367 
368     Always returns \p true. The return value is needed for compatibility with
369     the Generator class.
370   */
371   bool remove_space_dimensions(const Variables_Set& vars);
372 
373   //! Permutes the space dimensions of the constraint.
374   /*
375     \param cycle
376     A vector representing a cycle of the permutation according to which the
377     space dimensions must be rearranged.
378 
379     The \p cycle vector represents a cycle of a permutation of space
380     dimensions.
381     For example, the permutation
382     \f$ \{ x_1 \mapsto x_2, x_2 \mapsto x_3, x_3 \mapsto x_1 \}\f$ can be
383     represented by the vector containing \f$ x_1, x_2, x_3 \f$.
384   */
385   void permute_space_dimensions(const std::vector<Variable>& cycle);
386 
387   //! Shift by \p n positions the coefficients of variables, starting from
388   //! the coefficient of \p v. This increases the space dimension by \p n.
389   void shift_space_dimensions(Variable v, dimension_type n);
390 
391   //! Returns the constraint type of \p *this.
392   Type type() const;
393 
394   /*! \brief
395     Returns <CODE>true</CODE> if and only if
396     \p *this is an equality constraint.
397   */
398   bool is_equality() const;
399 
400   /*! \brief
401     Returns <CODE>true</CODE> if and only if
402     \p *this is an inequality constraint (either strict or non-strict).
403   */
404   bool is_inequality() const;
405 
406   /*! \brief
407     Returns <CODE>true</CODE> if and only if
408     \p *this is a non-strict inequality constraint.
409   */
410   bool is_nonstrict_inequality() const;
411 
412   /*! \brief
413     Returns <CODE>true</CODE> if and only if
414     \p *this is a strict inequality constraint.
415   */
416   bool is_strict_inequality() const;
417 
418   //! Returns the coefficient of \p v in \p *this.
419   /*!
420     \exception std::invalid_argument thrown if the index of \p v
421     is greater than or equal to the space dimension of \p *this.
422   */
423   Coefficient_traits::const_reference coefficient(Variable v) const;
424 
425   //! Returns the inhomogeneous term of \p *this.
426   Coefficient_traits::const_reference inhomogeneous_term() const;
427 
428   //! Initializes the class.
429   static void initialize();
430 
431   //! Finalizes the class.
432   static void finalize();
433 
434   //! The unsatisfiable (zero-dimension space) constraint \f$0 = 1\f$.
435   static const Constraint& zero_dim_false();
436 
437   /*! \brief
438     The true (zero-dimension space) constraint \f$0 \leq 1\f$,
439     also known as <EM>positivity constraint</EM>.
440   */
441   static const Constraint& zero_dim_positivity();
442 
443   /*! \brief
444     Returns a lower bound to the total size in bytes of the memory
445     occupied by \p *this.
446   */
447   memory_size_type total_memory_in_bytes() const;
448 
449   //! Returns the size in bytes of the memory managed by \p *this.
450   memory_size_type external_memory_in_bytes() const;
451 
452   /*! \brief
453     Returns <CODE>true</CODE> if and only if
454     \p *this is a tautology (i.e., an always true constraint).
455 
456     A tautology can have either one of the following forms:
457     - an equality: \f$\sum_{i=0}^{n-1} 0 x_i + 0 = 0\f$; or
458     - a non-strict inequality: \f$\sum_{i=0}^{n-1} 0 x_i + b \geq 0\f$,
459       where \f$b \geq 0\f$; or
460     - a strict inequality: \f$\sum_{i=0}^{n-1} 0 x_i + b > 0\f$,
461       where \f$b > 0\f$.
462   */
463   bool is_tautological() const;
464 
465   /*! \brief
466     Returns <CODE>true</CODE> if and only if
467     \p *this is inconsistent (i.e., an always false constraint).
468 
469     An inconsistent constraint can have either one of the following forms:
470     - an equality: \f$\sum_{i=0}^{n-1} 0 x_i + b = 0\f$,
471       where \f$b \neq 0\f$; or
472     - a non-strict inequality: \f$\sum_{i=0}^{n-1} 0 x_i + b \geq 0\f$,
473       where \f$b < 0\f$; or
474     - a strict inequality: \f$\sum_{i=0}^{n-1} 0 x_i + b > 0\f$,
475       where \f$b \leq 0\f$.
476   */
477   bool is_inconsistent() const;
478 
479   /*! \brief
480     Returns <CODE>true</CODE> if and only if \p *this and \p y
481     are equivalent constraints.
482 
483     Constraints having different space dimensions are not equivalent.
484     Note that constraints having different types may nonetheless be
485     equivalent, if they both are tautologies or inconsistent.
486   */
487   bool is_equivalent_to(const Constraint& y) const;
488 
489   //! Returns <CODE>true</CODE> if \p *this is identical to \p y.
490   /*!
491     This is faster than is_equivalent_to(), but it may return `false' even
492     for equivalent constraints.
493   */
494   bool is_equal_to(const Constraint& y) const;
495 
496   //! Checks if all the invariants are satisfied.
497   bool OK() const;
498 
499   PPL_OUTPUT_DECLARATIONS
500 
501   /*! \brief
502     Loads from \p s an ASCII representation (as produced by
503     ascii_dump(std::ostream&) const) and sets \p *this accordingly.
504     Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise.
505   */
506   bool ascii_load(std::istream& s);
507 
508   //! Swaps \p *this with \p y.
509   void m_swap(Constraint& y);
510 
511   //! Returns the zero-dimension space constraint \f$\epsilon \geq 0\f$.
512   static const Constraint& epsilon_geq_zero();
513 
514   /*! \brief
515     The zero-dimension space constraint \f$\epsilon \leq 1\f$
516     (used to implement NNC polyhedra).
517   */
518   static const Constraint& epsilon_leq_one();
519 
520   //! The type of the (adapted) internal expression.
521   typedef Expression_Hide_Last<Linear_Expression> expr_type;
522   //! Partial read access to the (adapted) internal expression.
523   expr_type expression() const;
524 
525 private:
526 
527   //! The possible kinds of Constraint objects.
528   enum Kind {
529     LINE_OR_EQUALITY = 0,
530     RAY_OR_POINT_OR_INEQUALITY = 1
531   };
532 
533   Linear_Expression expr;
534 
535   Kind kind_;
536 
537   Topology topology_;
538 
539   /*! \brief
540     Holds (between class initialization and finalization) a pointer to
541     the unsatisfiable (zero-dimension space) constraint \f$0 = 1\f$.
542   */
543   static const Constraint* zero_dim_false_p;
544 
545   /*! \brief
546     Holds (between class initialization and finalization) a pointer to
547     the true (zero-dimension space) constraint \f$0 \leq 1\f$, also
548     known as <EM>positivity constraint</EM>.
549   */
550   static const Constraint* zero_dim_positivity_p;
551 
552   /*! \brief
553     Holds (between class initialization and finalization) a pointer to
554     the zero-dimension space constraint \f$\epsilon \geq 0\f$.
555   */
556   static const Constraint* epsilon_geq_zero_p;
557 
558   /*! \brief
559     Holds (between class initialization and finalization) a pointer to
560     the zero-dimension space constraint \f$\epsilon \leq 1\f$
561     (used to implement NNC polyhedra).
562   */
563   static const Constraint* epsilon_leq_one_p;
564 
565   //! Constructs the \f$0<0\f$ constraint.
566   Constraint(dimension_type space_dim, Kind kind, Topology topology,
567              Representation r = default_representation);
568 
569   /*! \brief
570     Builds a constraint of kind \p kind and topology \p topology,
571     stealing the coefficients from \p e.
572 
573     \note The new Constraint will have the same representation as `e'.
574   */
575   Constraint(Linear_Expression& e, Kind kind, Topology topology);
576 
577   /*! \brief
578     Builds a constraint of type \p type and topology \p topology,
579     stealing the coefficients from \p e.
580 
581     \note The new Constraint will have the same representation as `e'.
582   */
583   Constraint(Linear_Expression& e, Type type, Topology topology);
584 
585   /*! \brief
586     Returns <CODE>true</CODE> if and only if \p *this row
587     represents a line or an equality.
588   */
589   bool is_line_or_equality() const;
590 
591   /*! \brief
592     Returns <CODE>true</CODE> if and only if \p *this row
593     represents a ray, a point or an inequality.
594   */
595   bool is_ray_or_point_or_inequality() const;
596 
597   //! Sets to \p LINE_OR_EQUALITY the kind of \p *this row.
598   void set_is_line_or_equality();
599 
600   //! Sets to \p RAY_OR_POINT_OR_INEQUALITY the kind of \p *this row.
601   void set_is_ray_or_point_or_inequality();
602 
603   //! \name Flags inspection methods
604   //@{
605   //! Returns the topological kind of \p *this.
606   Topology topology() const;
607 
608   /*! \brief
609     Returns <CODE>true</CODE> if and only if the topology
610     of \p *this row is not necessarily closed.
611   */
612   bool is_not_necessarily_closed() const;
613 
614   /*! \brief
615     Returns <CODE>true</CODE> if and only if the topology
616     of \p *this row is necessarily closed.
617   */
618   bool is_necessarily_closed() const;
619   //@} // Flags inspection methods
620 
621   //! \name Flags coercion methods
622   //@{
623 
624   // TODO: Consider setting the epsilon dimension in this method.
625   //! Sets to \p x the topological kind of \p *this row.
626   void set_topology(Topology x);
627 
628   //! Sets to \p NECESSARILY_CLOSED the topological kind of \p *this row.
629   void set_necessarily_closed();
630 
631   //! Sets to \p NOT_NECESSARILY_CLOSED the topological kind of \p *this row.
632   void set_not_necessarily_closed();
633   //@} // Flags coercion methods
634 
635   //! Sets the dimension of the vector space enclosing \p *this to
636   //! \p space_dim .
637   //! Sets the space dimension of the rows in the system to \p space_dim .
638   /*!
639     This method is for internal use, it does *not* assert OK() at the end,
640     so it can be used for invalid objects.
641   */
642   void set_space_dimension_no_ok(dimension_type space_dim);
643 
644   /*! \brief
645     Throws a <CODE>std::invalid_argument</CODE> exception containing
646     error message \p message.
647   */
648   void
649   throw_invalid_argument(const char* method, const char* message) const;
650 
651   /*! \brief
652     Throws a <CODE>std::invalid_argument</CODE> exception
653     containing the appropriate error message.
654   */
655   void
656   throw_dimension_incompatible(const char* method,
657                                const char* name_var,
658                                Variable v) const;
659 
660   //! Returns the epsilon coefficient. The constraint must be NNC.
661   Coefficient_traits::const_reference epsilon_coefficient() const;
662 
663   //! Sets the epsilon coefficient to \p n. The constraint must be NNC.
664   void set_epsilon_coefficient(Coefficient_traits::const_reference n);
665 
666   //! Marks the epsilon dimension as a standard dimension.
667   /*!
668     The row topology is changed to <CODE>NOT_NECESSARILY_CLOSED</CODE>, and
669     the number of space dimensions is increased by 1.
670   */
671   void mark_as_necessarily_closed();
672 
673   //! Marks the last dimension as the epsilon dimension.
674   /*!
675     The row topology is changed to <CODE>NECESSARILY_CLOSED</CODE>, and
676     the number of space dimensions is decreased by 1.
677   */
678   void mark_as_not_necessarily_closed();
679 
680   //! Sets the constraint type to <CODE>EQUALITY</CODE>.
681   void set_is_equality();
682 
683   //! Sets the constraint to be an inequality.
684   /*!
685     Whether the constraint type will become <CODE>NONSTRICT_INEQUALITY</CODE>
686     or <CODE>STRICT_INEQUALITY</CODE> depends on the topology and the value
687     of the low-level coefficients of the constraint.
688   */
689   void set_is_inequality();
690 
691   //! Linearly combines \p *this with \p y so that i-th coefficient is 0.
692   /*!
693     \param y
694     The Constraint that will be combined with \p *this object;
695 
696     \param i
697     The index of the coefficient that has to become \f$0\f$.
698 
699     Computes a linear combination of \p *this and \p y having
700     the i-th coefficient equal to \f$0\f$. Then it assigns
701     the resulting Constraint to \p *this and normalizes it.
702   */
703   void linear_combine(const Constraint& y, dimension_type i);
704 
705   /*! \brief
706     Normalizes the sign of the coefficients so that the first non-zero
707     (homogeneous) coefficient of a line-or-equality is positive.
708   */
709   void sign_normalize();
710 
711   /*! \brief
712     Strong normalization: ensures that different Constraint objects
713     represent different hyperplanes or hyperspaces.
714 
715     Applies both Constraint::normalize() and Constraint::sign_normalize().
716   */
717   void strong_normalize();
718 
719   /*! \brief
720     Returns <CODE>true</CODE> if and only if the coefficients are
721     strongly normalized.
722   */
723   bool check_strong_normalized() const;
724 
725   /*! \brief
726     Builds a new copy of the zero-dimension space constraint
727     \f$\epsilon \geq 0\f$ (used to implement NNC polyhedra).
728   */
729   static Constraint construct_epsilon_geq_zero();
730 
731   friend int
732   compare(const Constraint& x, const Constraint& y);
733 
734   friend class Linear_System<Constraint>;
735   friend class Constraint_System;
736   friend class Polyhedron;
737   friend class Scalar_Products;
738   friend class Topology_Adjusted_Scalar_Product_Sign;
739   friend class Termination_Helpers;
740   friend class Grid;
741   template <typename T>
742   friend class Octagonal_Shape;
743 
744   friend Constraint
745   operator<(const Linear_Expression& e1, const Linear_Expression& e2);
746 
747   friend Constraint
748   operator<(Variable v1, Variable v2);
749 
750   friend Constraint
751   operator<(const Linear_Expression& e, Coefficient_traits::const_reference n);
752 
753   friend Constraint
754   operator<(Coefficient_traits::const_reference n, const Linear_Expression& e);
755 
756   friend Constraint
757   operator>(const Linear_Expression& e1, const Linear_Expression& e2);
758 
759   friend Constraint
760   operator>(Variable v1, Variable v2);
761 
762   friend Constraint
763   operator>(const Linear_Expression& e, Coefficient_traits::const_reference n);
764 
765   friend Constraint
766   operator>(Coefficient_traits::const_reference n, const Linear_Expression& e);
767 
768   friend Constraint
769   operator==(const Linear_Expression& e1, const Linear_Expression& e2);
770 
771   friend Constraint
772   operator==(Variable v1, Variable v2);
773 
774   friend Constraint
775   operator==(const Linear_Expression& e, Coefficient_traits::const_reference n);
776 
777   friend Constraint
778   operator==(Coefficient_traits::const_reference n, const Linear_Expression& e);
779 
780   friend Constraint
781   operator<=(const Linear_Expression& e1, const Linear_Expression& e2);
782 
783   friend Constraint
784   operator<=(Variable v1, Variable v2);
785 
786   friend Constraint
787   operator<=(const Linear_Expression& e, Coefficient_traits::const_reference n);
788 
789   friend Constraint
790   operator<=(Coefficient_traits::const_reference n, const Linear_Expression& e);
791 
792   friend Constraint
793   operator>=(const Linear_Expression& e1, const Linear_Expression& e2);
794 
795   friend Constraint
796   operator>=(Variable v1, Variable v2);
797 
798   friend Constraint
799   operator>=(const Linear_Expression& e, Coefficient_traits::const_reference n);
800 
801   friend Constraint
802   operator>=(Coefficient_traits::const_reference n, const Linear_Expression& e);
803 };
804 
805 namespace Parma_Polyhedra_Library {
806 
807 namespace IO_Operators {
808 
809 //! Output operator.
810 /*! \relates Parma_Polyhedra_Library::Constraint */
811 std::ostream& operator<<(std::ostream& s, const Constraint& c);
812 
813 //! Output operator.
814 /*! \relates Parma_Polyhedra_Library::Constraint */
815 std::ostream& operator<<(std::ostream& s, const Constraint::Type& t);
816 
817 } // namespace IO_Operators
818 
819 //! Returns <CODE>true</CODE> if and only if \p x is equivalent to \p y.
820 /*! \relates Constraint */
821 bool
822 operator==(const Constraint& x, const Constraint& y);
823 
824 //! Returns <CODE>true</CODE> if and only if \p x is not equivalent to \p y.
825 /*! \relates Constraint */
826 bool
827 operator!=(const Constraint& x, const Constraint& y);
828 
829 /*! \relates Constraint */
830 void swap(Constraint& x, Constraint& y);
831 
832 } // namespace Parma_Polyhedra_Library
833 
834 #include "Constraint_inlines.hh"
835 
836 #endif // !defined(PPL_Constraint_defs_hh)
837