Module: ppl/ppl Branch: master Commit: 4b09274909915d1908c5a0668390286604a2bda7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4b09274909915...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Fri Feb 24 21:10:28 2012 +0100

Comments improved.

---

src/BD_Shape.templates.hh | 26 ++++++++++++++------------ src/Polyhedron_chdims.cc | 4 ++-- src/simplify.cc | 7 ++++--- 3 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 3d4e132..6bd8c72 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -597,24 +597,26 @@ BD_Shape<T>::contains(const BD_Shape& y) const { }

/* - The `y' bounded difference shape need be closed. - In fact if, for example, in `*this' we have the constraints: + The `y' bounded difference shape must be closed. As an example, + consider the case where in `*this' we have the constraints

- x1 - x2 <= 1; - x1 <= 3; - x2 <= 2; + x1 - x2 <= 1, + x1 <= 3, + x2 <= 2,

- in `y' the constraints are: + and in `y' the constraints are

- x1 - x2 <= 0; - x2 <= 1; + x1 - x2 <= 0, + x2 <= 1.

- without closure it returns "false", instead if we close `y' we have - the implicit constraint + Without closure the (erroneous) analysis of the inhomogeneous terms + would conclude containment does not hold. Closing `y' results into + the "discovery" of the implicit constraint

- x1 <= 1; + x1 <= 1,

- and so we obtain the right result "true". + at which point the inhomogeneous terms can be examined to determine + that containment does hold. */ y.shortest_path_closure_assign();

diff --git a/src/Polyhedron_chdims.cc b/src/Polyhedron_chdims.cc index e4eabda..1ef2024 100644 --- a/src/Polyhedron_chdims.cc +++ b/src/Polyhedron_chdims.cc @@ -229,7 +229,7 @@ PPL::Polyhedron::add_space_dimensions_and_project(dimension_type m) { // In contrast, in the system of constraints, new rows are needed // in order to avoid embedding the old polyhedron in the new space. // Thus, for each new dimensions `x[k]', we add the constraint - // x[k] = 0; this is done by invoking the function add_space_dimensions() + // x[k] = 0: this is done by invoking the function add_space_dimensions() // giving the system of constraints as the second argument. if (constraints_are_up_to_date()) if (generators_are_up_to_date()) { @@ -237,7 +237,7 @@ PPL::Polyhedron::add_space_dimensions_and_project(dimension_type m) { if (!sat_g_is_up_to_date()) update_sat_g(); // Adds rows and/or columns to both matrices. - // `add_space_dimensions' correctly handles pending constraints + // `add_space_dimensions()' correctly handles pending constraints // or generators. add_space_dimensions(gen_sys, con_sys, sat_g, sat_c, m); } diff --git a/src/simplify.cc b/src/simplify.cc index 46b7f2a..cdda027 100644 --- a/src/simplify.cc +++ b/src/simplify.cc @@ -192,11 +192,12 @@ PPL::Polyhedron::simplify(Linear_System& sys, Bit_Matrix& sat) { // condition for an inequality to be irredundant (i.e., it provides // a sufficient condition for identifying redundant inequalities). // Let - // num_saturators[i] = num_sat_lines[i] + num_sat_rays_or_points[i]; - // dim_lin_space = num_irredundant_lines; + // + // num_saturators[i] = num_sat_lines[i] + num_sat_rays_or_points[i], + // dim_lin_space = num_irredundant_lines, // dim_ray_space // = dim_vector_space - num_irredundant_equalities - dim_lin_space - // = num_columns - 1 - num_lines_or_equalities - dim_lin_space; + // = num_columns - 1 - num_lines_or_equalities - dim_lin_space, // min_sat_rays_or_points = dim_ray_space. // // An inequality saturated by less than `dim_ray_space' _rays/points_