[PPL-devel] [GIT] ppl/ppl(master): Comments improved.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at 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_