1 /* Constraint_System 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_System_defs.hh"
26 #include "Constraint_System_inlines.hh"
27 #include "Generator_defs.hh"
28 #include "Scalar_Products_defs.hh"
29 #include "Scalar_Products_inlines.hh"
30 #include "Congruence_System_defs.hh"
31 #include "Congruence_System_inlines.hh"
32 #include "assertions.hh"
33 #include <string>
34 #include <vector>
35 #include <iostream>
36 #include <stdexcept>
37
38 namespace PPL = Parma_Polyhedra_Library;
39
Constraint_System(const Congruence_System & cgs,Representation r)40 PPL::Constraint_System::Constraint_System(const Congruence_System& cgs,
41 Representation r)
42 : sys(NECESSARILY_CLOSED, cgs.space_dimension(), r) {
43 for (Congruence_System::const_iterator i = cgs.begin(),
44 cgs_end = cgs.end(); i != cgs_end; ++i) {
45 if (i->is_equality()) {
46 Constraint tmp(*i);
47 insert(tmp, Recycle_Input());
48 }
49 }
50 PPL_ASSERT(OK());
51 }
52
53 bool
54 PPL::Constraint_System::
adjust_topology_and_space_dimension(const Topology new_topology,const dimension_type new_space_dim)55 adjust_topology_and_space_dimension(const Topology new_topology,
56 const dimension_type new_space_dim) {
57 PPL_ASSERT(space_dimension() <= new_space_dim);
58
59 if (sys.topology() == NOT_NECESSARILY_CLOSED
60 && new_topology == NECESSARILY_CLOSED) {
61 // A NOT_NECESSARILY_CLOSED constraint system
62 // can be converted to a NECESSARILY_CLOSED one
63 // only if it does not contain strict inequalities.
64 if (has_strict_inequalities()) {
65 return false;
66 }
67 // Since there were no strict inequalities,
68 // the only constraints that may have a non-zero epsilon coefficient
69 // are the eps-leq-one and the eps-geq-zero constraints.
70 // If they are present, we erase these rows, so that the
71 // epsilon column will only contain zeroes: as a consequence,
72 // we just decrement the number of columns to be added.
73 const bool was_sorted = sys.is_sorted();
74
75 // Note that num_rows() is *not* constant, because it is decreased by
76 // remove_row().
77 for (dimension_type i = 0; i < num_rows(); ) {
78 if (sys[i].epsilon_coefficient() != 0) {
79 sys.remove_row(i, false);
80 }
81 else {
82 ++i;
83 }
84 }
85
86 // If `cs' was sorted we sort it again.
87 if (was_sorted) {
88 sys.sort_rows();
89 }
90 }
91
92 sys.set_topology(new_topology);
93 sys.set_space_dimension(new_space_dim);
94
95 // We successfully adjusted space dimensions and topology.
96 PPL_ASSERT(OK());
97 return true;
98 }
99
100 bool
has_equalities() const101 PPL::Constraint_System::has_equalities() const {
102 // We verify if the system has equalities also in the pending part.
103 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
104 if (sys[i].is_equality()) {
105 return true;
106 }
107 }
108 return false;
109 }
110
111 bool
has_strict_inequalities() const112 PPL::Constraint_System::has_strict_inequalities() const {
113 if (sys.is_necessarily_closed()) {
114 return false;
115 }
116 // We verify if the system has strict inequalities
117 // also in the pending part.
118 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
119 const Constraint& c = sys[i];
120 // Optimized type checking: we already know the topology;
121 // also, equalities have the epsilon coefficient equal to zero.
122 // NOTE: the constraint eps_leq_one should not be considered
123 // a strict inequality.
124 if (c.epsilon_coefficient() < 0 && !c.is_tautological()) {
125 return true;
126 }
127 }
128 return false;
129 }
130
131 void
insert(const Constraint & r)132 PPL::Constraint_System::insert(const Constraint& r) {
133 Constraint tmp = r;
134 insert(tmp, Recycle_Input());
135 }
136
137 void
insert(Constraint & c,Recycle_Input)138 PPL::Constraint_System::insert(Constraint& c, Recycle_Input) {
139 // We are sure that the matrix has no pending rows
140 // and that the new row is not a pending constraint.
141 PPL_ASSERT(sys.num_pending_rows() == 0);
142
143 if (sys.topology() != c.topology()) {
144 if (sys.topology() == NECESSARILY_CLOSED) {
145 sys.set_topology(NOT_NECESSARILY_CLOSED);
146 }
147 else {
148 c.set_topology(NOT_NECESSARILY_CLOSED);
149 }
150 }
151
152 sys.insert(c, Recycle_Input());
153
154 PPL_ASSERT(OK());
155 }
156
157 void
insert_pending(const Constraint & r)158 PPL::Constraint_System::insert_pending(const Constraint& r) {
159 Constraint tmp = r;
160 insert_pending(tmp, Recycle_Input());
161 }
162
163 void
insert_pending(Constraint & c,Recycle_Input)164 PPL::Constraint_System::insert_pending(Constraint& c, Recycle_Input) {
165 if (sys.topology() != c.topology()) {
166 if (sys.topology() == NECESSARILY_CLOSED) {
167 sys.set_topology(NOT_NECESSARILY_CLOSED);
168 }
169 else {
170 c.set_topology(NOT_NECESSARILY_CLOSED);
171 }
172 }
173
174 sys.insert_pending(c, Recycle_Input());
175 PPL_ASSERT(OK());
176 }
177
178 PPL::dimension_type
num_inequalities() const179 PPL::Constraint_System::num_inequalities() const {
180 // We are sure that we call this method only when
181 // the matrix has no pending rows.
182 PPL_ASSERT(sys.num_pending_rows() == 0);
183 const Constraint_System& cs = *this;
184 dimension_type n = 0;
185 // If the Base happens to be sorted, take advantage of the fact
186 // that inequalities are at the bottom of the system.
187 if (sys.is_sorted()) {
188 for (dimension_type i = sys.num_rows();
189 i > 0 && cs[--i].is_inequality(); ) {
190 ++n;
191 }
192 }
193 else {
194 for (dimension_type i = sys.num_rows(); i-- > 0 ; ) {
195 if (cs[i].is_inequality()) {
196 ++n;
197 }
198 }
199 }
200 return n;
201 }
202
203 PPL::dimension_type
num_equalities() const204 PPL::Constraint_System::num_equalities() const {
205 // We are sure that we call this method only when
206 // the matrix has no pending rows.
207 PPL_ASSERT(sys.num_pending_rows() == 0);
208 return sys.num_rows() - num_inequalities();
209 }
210
211 void
skip_forward()212 PPL::Constraint_System_const_iterator::skip_forward() {
213 const Linear_System<Constraint>::const_iterator csp_end = csp->end();
214 while (i != csp_end && (*this)->is_tautological()) {
215 ++i;
216 }
217 }
218
219 bool
satisfies_all_constraints(const Generator & g) const220 PPL::Constraint_System::satisfies_all_constraints(const Generator& g) const {
221 PPL_ASSERT(g.space_dimension() <= space_dimension());
222
223 // Setting `sps' to the appropriate scalar product sign operator.
224 // This also avoids problems when having _legal_ topology mismatches
225 // (which could also cause a mismatch in the number of columns).
226 const Topology_Adjusted_Scalar_Product_Sign sps(g);
227
228 if (sys.is_necessarily_closed()) {
229 if (g.is_line()) {
230 // Lines must saturate all constraints.
231 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
232 if (sps(g, sys[i]) != 0) {
233 return false;
234 }
235 }
236 }
237 else {
238 // `g' is either a ray, a point or a closure point.
239 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
240 const Constraint& c = sys[i];
241 const int sp_sign = sps(g, c);
242 if (c.is_inequality()) {
243 // As `cs' is necessarily closed,
244 // `c' is a non-strict inequality.
245 if (sp_sign < 0) {
246 return false;
247 }
248 }
249 else {
250 // `c' is an equality.
251 if (sp_sign != 0) {
252 return false;
253 }
254 }
255 }
256 }
257 }
258 else {
259 // `cs' is not necessarily closed.
260 switch (g.type()) {
261
262 case Generator::LINE:
263 // Lines must saturate all constraints.
264 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
265 if (sps(g, sys[i]) != 0) {
266 return false;
267 }
268 }
269
270 break;
271
272 case Generator::POINT:
273 // Have to perform the special test
274 // when dealing with a strict inequality.
275 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
276 const Constraint& c = sys[i];
277 const int sp_sign = sps(g, c);
278 switch (c.type()) {
279 case Constraint::EQUALITY:
280 if (sp_sign != 0) {
281 return false;
282 }
283 break;
284 case Constraint::NONSTRICT_INEQUALITY:
285 if (sp_sign < 0) {
286 return false;
287 }
288 break;
289 case Constraint::STRICT_INEQUALITY:
290 if (sp_sign <= 0) {
291 return false;
292 }
293 break;
294 }
295 }
296 break;
297
298 case Generator::RAY:
299 // Intentionally fall through.
300 case Generator::CLOSURE_POINT:
301 for (dimension_type i = sys.num_rows(); i-- > 0; ) {
302 const Constraint& c = sys[i];
303 const int sp_sign = sps(g, c);
304 if (c.is_inequality()) {
305 // Constraint `c' is either a strict or a non-strict inequality.
306 if (sp_sign < 0) {
307 return false;
308 }
309 }
310 else
311 // Constraint `c' is an equality.
312 if (sp_sign != 0) {
313 return false;
314 }
315 }
316 break;
317 }
318 }
319
320 // If we reach this point, `g' satisfies all constraints.
321 return true;
322 }
323
324
325 void
326 PPL::Constraint_System
affine_preimage(const Variable v,const Linear_Expression & expr,Coefficient_traits::const_reference denominator)327 ::affine_preimage(const Variable v,
328 const Linear_Expression& expr,
329 Coefficient_traits::const_reference denominator) {
330 PPL_ASSERT(v.space_dimension() <= sys.space_dimension());
331 PPL_ASSERT(expr.space_dimension() <= sys.space_dimension());
332 PPL_ASSERT(denominator > 0);
333
334 Coefficient_traits::const_reference expr_v = expr.coefficient(v);
335
336 const dimension_type n_rows = sys.num_rows();
337 const bool not_invertible = (v.space_dimension() > expr.space_dimension()
338 || expr_v == 0);
339
340 for (dimension_type i = n_rows; i-- > 0; ) {
341 Constraint& row = sys.rows[i];
342 Coefficient_traits::const_reference row_v = row.coefficient(v);
343 if (row_v != 0) {
344 const Coefficient c = row_v;
345 if (denominator != 1) {
346 row.expr *= denominator;
347 }
348 row.expr.linear_combine(expr, 1, c, 0, expr.space_dimension() + 1);
349 if (not_invertible) {
350 row.expr.set_coefficient(v, Coefficient_zero());
351 }
352 else {
353 row.expr.set_coefficient(v, c * expr_v);
354 }
355 row.strong_normalize();
356 PPL_ASSERT(row.OK());
357 }
358 }
359
360 // Strong normalization also resets the sortedness flag.
361 sys.strong_normalize();
362
363 PPL_ASSERT(sys.OK());
364 }
365
366 void
ascii_dump(std::ostream & s) const367 PPL::Constraint_System::ascii_dump(std::ostream& s) const {
368 sys.ascii_dump(s);
369 }
370
PPL_OUTPUT_DEFINITIONS(Constraint_System)371 PPL_OUTPUT_DEFINITIONS(Constraint_System)
372
373 bool
374 PPL::Constraint_System::ascii_load(std::istream& s) {
375 if (!sys.ascii_load(s)) {
376 return false;
377 }
378
379 PPL_ASSERT(OK());
380 return true;
381 }
382
383 const PPL::Constraint_System* PPL::Constraint_System::zero_dim_empty_p = 0;
384
385 void
initialize()386 PPL::Constraint_System::initialize() {
387 PPL_ASSERT(zero_dim_empty_p == 0);
388 zero_dim_empty_p
389 = new Constraint_System(Constraint::zero_dim_false());
390 }
391
392 void
finalize()393 PPL::Constraint_System::finalize() {
394 PPL_ASSERT(zero_dim_empty_p != 0);
395 delete zero_dim_empty_p;
396 zero_dim_empty_p = 0;
397 }
398
399 bool
OK() const400 PPL::Constraint_System::OK() const {
401 return sys.OK();
402 }
403
404 /*! \relates Parma_Polyhedra_Library::Constraint_System */
405 std::ostream&
operator <<(std::ostream & s,const Constraint_System & cs)406 PPL::IO_Operators::operator<<(std::ostream& s, const Constraint_System& cs) {
407 Constraint_System_const_iterator i = cs.begin();
408 const Constraint_System_const_iterator cs_end = cs.end();
409 if (i == cs_end) {
410 s << "true";
411 }
412 else {
413 while (i != cs_end) {
414 s << *i;
415 ++i;
416 if (i != cs_end) {
417 s << ", ";
418 }
419 }
420 }
421 return s;
422 }
423