1 /* Constraint 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 "Constraint_defs.hh"
26 #include "Variable_defs.hh"
27 #include "Variables_Set_defs.hh"
28 #include "Congruence_defs.hh"
29 #include "math_utilities_defs.hh"
30
31 #include <iostream>
32 #include <sstream>
33 #include <stdexcept>
34
35 namespace PPL = Parma_Polyhedra_Library;
36
37 void
throw_invalid_argument(const char * method,const char * message) const38 PPL::Constraint::throw_invalid_argument(const char* method,
39 const char* message) const {
40 std::ostringstream s;
41 s << "PPL::Constraint::" << method << ":" << std::endl
42 << message;
43 throw std::invalid_argument(s.str());
44 }
45
46 void
throw_dimension_incompatible(const char * method,const char * name_var,const Variable v) const47 PPL::Constraint::throw_dimension_incompatible(const char* method,
48 const char* name_var,
49 const Variable v) const {
50 std::ostringstream s;
51 s << "PPL::Constraint::" << method << ":" << std::endl
52 << "this->space_dimension() == " << space_dimension() << ", "
53 << name_var << ".space_dimension() == " << v.space_dimension() << ".";
54 throw std::invalid_argument(s.str());
55 }
56
57 PPL::Constraint
construct_epsilon_geq_zero()58 PPL::Constraint::construct_epsilon_geq_zero() {
59 Linear_Expression e;
60 Constraint c(e, NONSTRICT_INEQUALITY, NOT_NECESSARILY_CLOSED);
61 c.set_epsilon_coefficient(Coefficient_one());
62 PPL_ASSERT(c.OK());
63 return c;
64 }
65
Constraint(const Congruence & cg,Representation r)66 PPL::Constraint::Constraint(const Congruence& cg, Representation r)
67 : expr(cg.expression(), r),
68 kind_(LINE_OR_EQUALITY),
69 topology_(NECESSARILY_CLOSED) {
70 if (!cg.is_equality()) {
71 throw_invalid_argument("Constraint(cg)",
72 "congruence cg must be an equality.");
73 }
74 // Enforce normalization.
75 strong_normalize();
76 PPL_ASSERT(OK());
77 }
78
79 void
swap_space_dimensions(Variable v1,Variable v2)80 PPL::Constraint::swap_space_dimensions(Variable v1, Variable v2) {
81 PPL_ASSERT(v1.space_dimension() <= space_dimension());
82 PPL_ASSERT(v2.space_dimension() <= space_dimension());
83 expr.swap_space_dimensions(v1, v2);
84 // *this is still normalized but it may not be strongly normalized.
85 sign_normalize();
86 PPL_ASSERT(OK());
87 }
88
89 void
90 PPL::Constraint
permute_space_dimensions(const std::vector<Variable> & cycle)91 ::permute_space_dimensions(const std::vector<Variable>& cycle) {
92 if (cycle.size() < 2) {
93 // No-op. No need to call sign_normalize().
94 return;
95 }
96
97 expr.permute_space_dimensions(cycle);
98 // *this is still normalized but may be not strongly normalized:
99 // sign normalization is necessary.
100 sign_normalize();
101 PPL_ASSERT(OK());
102 }
103
104 bool
is_tautological() const105 PPL::Constraint::is_tautological() const {
106 if (expr.all_homogeneous_terms_are_zero()) {
107 if (is_equality()) {
108 return expr.inhomogeneous_term() == 0;
109 }
110 else {
111 // Non-strict inequality constraint.
112 return expr.inhomogeneous_term() >= 0;
113 }
114 }
115 else {
116 // There is a non-zero homogeneous coefficient.
117 if (is_necessarily_closed()) {
118 return false;
119 }
120 else {
121 // The constraint is NOT necessarily closed.
122 const int eps_sign = sgn(epsilon_coefficient());
123 if (eps_sign > 0) {
124 // We have found the constraint epsilon >= 0.
125 return true;
126 }
127 if (eps_sign == 0) {
128 // One of the `true' dimensions has a non-zero coefficient.
129 return false;
130 }
131 else {
132 // Here the epsilon coefficient is negative: strict inequality.
133 if (expr.inhomogeneous_term() <= 0) {
134 // A strict inequality such as `lhs - k > 0',
135 // where k is a non negative integer, cannot be trivially true.
136 return false;
137 }
138 // Checking for another non-zero coefficient.
139 // If the check succeeds, we have the inequality `k > 0',
140 // where k is a positive integer.
141 return expression().all_homogeneous_terms_are_zero();
142 }
143 }
144 }
145 }
146
147 bool
is_inconsistent() const148 PPL::Constraint::is_inconsistent() const {
149 if (expr.all_homogeneous_terms_are_zero()) {
150 // The inhomogeneous term is the only non-zero coefficient.
151 if (is_equality()) {
152 return expr.inhomogeneous_term() != 0;
153 }
154 else {
155 // Non-strict inequality constraint.
156 return expr.inhomogeneous_term() < 0;
157 }
158 }
159 else {
160 // There is a non-zero homogeneous coefficient.
161 if (is_necessarily_closed()) {
162 return false;
163 }
164 else {
165 // The constraint is NOT necessarily closed.
166 if (epsilon_coefficient() >= 0) {
167 // If positive, we have found the constraint epsilon >= 0.
168 // If zero, one of the `true' dimensions has a non-zero coefficient.
169 // In both cases, it is not trivially false.
170 return false;
171 }
172 else {
173 // Here the epsilon coefficient is negative: strict inequality.
174 if (expr.inhomogeneous_term() > 0) {
175 // A strict inequality such as `lhs + k > 0',
176 // where k is a positive integer, cannot be trivially false.
177 return false;
178 }
179 // Checking for another non-zero coefficient.
180 // If the check succeeds, we have the inequality `k > 0',
181 // where k is a positive integer.
182 return expression().all_homogeneous_terms_are_zero();
183 }
184 }
185 }
186 }
187
188 void
linear_combine(const Constraint & y,dimension_type i)189 PPL::Constraint::linear_combine(const Constraint& y, dimension_type i) {
190 expr.linear_combine(y.expr, i);
191 strong_normalize();
192 }
193
194 /*! \relates Parma_Polyhedra_Library::Constraint */
195 int
compare(const Constraint & x,const Constraint & y)196 PPL::compare(const Constraint& x, const Constraint& y) {
197 const bool x_is_line_or_equality = x.is_line_or_equality();
198 const bool y_is_line_or_equality = y.is_line_or_equality();
199 if (x_is_line_or_equality != y_is_line_or_equality) {
200 // Equalities (lines) precede inequalities (ray/point).
201 return y_is_line_or_equality ? 2 : -2;
202 }
203
204 return compare(x.expr, y.expr);
205 }
206
207 bool
is_equivalent_to(const Constraint & y) const208 PPL::Constraint::is_equivalent_to(const Constraint& y) const {
209 const Constraint& x = *this;
210 const dimension_type x_space_dim = x.space_dimension();
211 if (x_space_dim != y.space_dimension()) {
212 return false;
213 }
214
215 const Type x_type = x.type();
216 if (x_type != y.type()) {
217 // Check for special cases.
218 if (x.is_tautological()) {
219 return y.is_tautological();
220 }
221 else {
222 return x.is_inconsistent() && y.is_inconsistent();
223 }
224 }
225
226 if (x_type == STRICT_INEQUALITY) {
227 // Due to the presence of epsilon-coefficients, syntactically
228 // different strict inequalities may actually encode the same
229 // topologically open half-space.
230 // First, drop the epsilon-coefficient ...
231 Linear_Expression x_expr(x.expression());
232 Linear_Expression y_expr(y.expression());
233 // ... then, re-normalize ...
234 x_expr.normalize();
235 y_expr.normalize();
236 // ... and finally check for syntactic equality.
237 return x_expr.is_equal_to(y_expr);
238 }
239
240 // `x' and 'y' are of the same type and they are not strict inequalities;
241 // thus, the epsilon-coefficient, if present, is zero.
242 // It is sufficient to check for syntactic equality.
243 return x.expr.is_equal_to(y.expr);
244 }
245
246 bool
is_equal_to(const Constraint & y) const247 PPL::Constraint::is_equal_to(const Constraint& y) const {
248 return expr.is_equal_to(y.expr) && kind_ == y.kind_ && topology() == y.topology();
249 }
250
251 void
sign_normalize()252 PPL::Constraint::sign_normalize() {
253 if (is_line_or_equality()) {
254 expr.sign_normalize();
255 }
256 }
257
258 bool
check_strong_normalized() const259 PPL::Constraint::check_strong_normalized() const {
260 Constraint tmp = *this;
261 tmp.strong_normalize();
262 return compare(*this, tmp) == 0;
263 }
264
265 const PPL::Constraint* PPL::Constraint::zero_dim_false_p = 0;
266 const PPL::Constraint* PPL::Constraint::zero_dim_positivity_p = 0;
267 const PPL::Constraint* PPL::Constraint::epsilon_geq_zero_p = 0;
268 const PPL::Constraint* PPL::Constraint::epsilon_leq_one_p = 0;
269
270 void
initialize()271 PPL::Constraint::initialize() {
272 PPL_ASSERT(zero_dim_false_p == 0);
273 zero_dim_false_p
274 = new Constraint(Linear_Expression::zero() == Coefficient_one());
275
276 PPL_ASSERT(zero_dim_positivity_p == 0);
277 zero_dim_positivity_p
278 = new Constraint(Linear_Expression::zero() <= Coefficient_one());
279
280 PPL_ASSERT(epsilon_geq_zero_p == 0);
281 epsilon_geq_zero_p
282 = new Constraint(construct_epsilon_geq_zero());
283
284 PPL_ASSERT(epsilon_leq_one_p == 0);
285 epsilon_leq_one_p
286 = new Constraint(Linear_Expression::zero() < Coefficient_one());
287 }
288
289 void
finalize()290 PPL::Constraint::finalize() {
291 PPL_ASSERT(zero_dim_false_p != 0);
292 delete zero_dim_false_p;
293 zero_dim_false_p = 0;
294
295 PPL_ASSERT(zero_dim_positivity_p != 0);
296 delete zero_dim_positivity_p;
297 zero_dim_positivity_p = 0;
298
299 PPL_ASSERT(epsilon_geq_zero_p != 0);
300 delete epsilon_geq_zero_p;
301 epsilon_geq_zero_p = 0;
302
303 PPL_ASSERT(epsilon_leq_one_p != 0);
304 delete epsilon_leq_one_p;
305 epsilon_leq_one_p = 0;
306 }
307
308 void
ascii_dump(std::ostream & s) const309 PPL::Constraint::ascii_dump(std::ostream& s) const {
310 expr.ascii_dump(s);
311
312 s << " ";
313
314 switch (type()) {
315 case Constraint::EQUALITY:
316 s << "=";
317 break;
318 case Constraint::NONSTRICT_INEQUALITY:
319 s << ">=";
320 break;
321 case Constraint::STRICT_INEQUALITY:
322 s << ">";
323 break;
324 }
325 s << " ";
326 if (topology() == NECESSARILY_CLOSED) {
327 s << "(C)";
328 }
329 else {
330 s << "(NNC)";
331 }
332 s << "\n";
333 }
334
335 bool
ascii_load(std::istream & s)336 PPL::Constraint::ascii_load(std::istream& s) {
337 std::string str;
338 std::string str2;
339
340 expr.ascii_load(s);
341
342 if (!(s >> str)) {
343 return false;
344 }
345 if (str == "=") {
346 set_is_equality();
347 }
348 else if (str == ">=" || str == ">") {
349 set_is_inequality();
350 }
351 else {
352 return false;
353 }
354
355 if (!(s >> str2)) {
356 return false;
357 }
358 if (str2 == "(NNC)") {
359 // TODO: Avoid the mark_as_*() methods if possible.
360 if (topology() == NECESSARILY_CLOSED) {
361 mark_as_not_necessarily_closed();
362 }
363 }
364 else {
365 if (str2 == "(C)") {
366 // TODO: Avoid the mark_as_*() methods if possible.
367 if (topology() == NOT_NECESSARILY_CLOSED) {
368 mark_as_necessarily_closed();
369 }
370 }
371 else {
372 return false;
373 }
374 }
375
376 // Checking for equality of actual and declared types.
377 switch (type()) {
378 case EQUALITY:
379 if (str != "=") {
380 return false;
381 }
382 break;
383 case NONSTRICT_INEQUALITY:
384 if (str != ">=") {
385 return false;
386 }
387 break;
388 case STRICT_INEQUALITY:
389 if (str != ">") {
390 return false;
391 }
392 break;
393 }
394
395 return true;
396 }
397
398 /*! \relates Parma_Polyhedra_Library::Constraint */
399 std::ostream&
operator <<(std::ostream & s,const Constraint & c)400 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint& c) {
401 PPL_DIRTY_TEMP_COEFFICIENT(cv);
402 bool first = true;
403 for (Constraint::expr_type::const_iterator i = c.expression().begin(),
404 i_end = c.expression().end(); i != i_end; ++i) {
405 cv = *i;
406 if (!first) {
407 if (cv > 0) {
408 s << " + ";
409 }
410 else {
411 s << " - ";
412 neg_assign(cv);
413 }
414 }
415 else {
416 first = false;
417 }
418 if (cv == -1) {
419 s << "-";
420 }
421 else if (cv != 1) {
422 s << cv << "*";
423 }
424 s << i.variable();
425 }
426 if (first) {
427 s << Coefficient_zero();
428 }
429 const char* relation_symbol = 0;
430 switch (c.type()) {
431 case Constraint::EQUALITY:
432 relation_symbol = " = ";
433 break;
434 case Constraint::NONSTRICT_INEQUALITY:
435 relation_symbol = " >= ";
436 break;
437 case Constraint::STRICT_INEQUALITY:
438 relation_symbol = " > ";
439 break;
440 }
441 s << relation_symbol << -c.inhomogeneous_term();
442 return s;
443 }
444
445 /*! \relates Parma_Polyhedra_Library::Constraint */
446 std::ostream&
operator <<(std::ostream & s,const Constraint::Type & t)447 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint::Type& t) {
448 const char* n = 0;
449 switch (t) {
450 case Constraint::EQUALITY:
451 n = "EQUALITY";
452 break;
453 case Constraint::NONSTRICT_INEQUALITY:
454 n = "NONSTRICT_INEQUALITY";
455 break;
456 case Constraint::STRICT_INEQUALITY:
457 n = "STRICT_INEQUALITY";
458 break;
459 }
460 s << n;
461 return s;
462 }
463
PPL_OUTPUT_DEFINITIONS(Constraint)464 PPL_OUTPUT_DEFINITIONS(Constraint)
465
466 bool
467 PPL::Constraint::OK() const {
468 // Topology consistency checks.
469 if (is_not_necessarily_closed() && expr.space_dimension() == 0) {
470 #ifndef NDEBUG
471 std::cerr << "Constraint has fewer coefficients than the minimum "
472 << "allowed by its topology."
473 << std::endl;
474 #endif
475 return false;
476 }
477
478 if (is_equality() && is_not_necessarily_closed()
479 && epsilon_coefficient() != 0) {
480 #ifndef NDEBUG
481 std::cerr << "Illegal constraint: an equality cannot be strict."
482 << std::endl;
483 #endif
484 return false;
485 }
486
487 // Normalization check.
488 Constraint tmp = *this;
489 tmp.strong_normalize();
490 if (tmp != *this) {
491 #ifndef NDEBUG
492 std::cerr << "Constraint is not strongly normalized as it should be."
493 << std::endl;
494 #endif
495 return false;
496 }
497
498 // All tests passed.
499 return true;
500 }
501