[PPL-devel] [GIT] ppl/ppl(master): Finished the documentation about the wrapping operator.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sun May 17 17:42:14 2009 +0200

Finished the documentation about the wrapping operator.

---

 doc/definitions.dox  |   49 ++++++++++++++++++++++++++++++++++++++++++++-----
 src/globals.types.hh |    6 +++---
 2 files changed, 47 insertions(+), 8 deletions(-)

diff --git a/doc/definitions.dox b/doc/definitions.dox
index c651cdf..ff19299 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -437,7 +437,17 @@ library user to provide the PPL's method with approximations of reality
 that are consistent with respect to the desired results.
 
 
-\section Approximating_Bounded_Arithmetic Approximating Bounded Arithmetic
+\section Approximating_Integers Approximating Integers
+
+FIXME(0.11): to be written.
+
+
+\subsection Dropping_Non_Integer_Points Dropping Non-Integer Points
+
+FIXME(0.11): to be written.
+
+
+\subsection Approximating_Bounded_Integers Approximating Bounded Integers
 
 The Parma Polyhedra Library provides services that allow to compute
 correct approximations of bounded arithmetic as available in widespread
@@ -494,7 +504,7 @@ Supported overflow behaviors are:
 FIXME(0.11): to be continued.
 
 
-\subsection Wrapping_Operator Wrapping Operator
+\subsubsection Wrapping_Operator Wrapping Operator
 
 One possibility to precisely approximate the semantics of programs that
 operate on bounded integer variables is to follow the approach described
@@ -522,9 +532,38 @@ combinations.
 
 The PPL provides a general wrapping operator that is parametric with
 respect to the set of space dimensions (variables) to be wrapped,
-the width, representation and overflow behavior of all these variables,
-
-FIXME(0.11): to be continued.
+the width, representation and overflow behavior of all these variables.
+An optional constraint system allows, when given, to increase the
+precision.  This constraint system, which must only depend on variables
+with respect to which wrapping is performed, is assumed to represent
+the conditional or looping construct guard with respect to which
+wrapping is performed.  Since wrapping requires the computation of
+upper bounds and due to non-distributivity of constraint refinement
+over upper bounds, passing a constraint system in this way can be more
+precise than refining the result of the wrapping operation afterwards.
+The general wrapping operator offered by the PPL also allows to control
+the complexity/precision ratio by means of two additional parameters:
+an unsigned integer encoding a complexity threshold, with higher values
+resulting in possibly improved precision; and a Boolean controlling
+whether space dimensions should be wrapped individually, something that
+results in much greater efficiency to the detriment of precision,
+or collectively.
+
+Note that the PPL assumes that any space dimension subject to wrapping
+is being used to capture the value of bounded integer values.  As a
+consequence the library is free to drop, from the involved numerical
+abstraction, any point having a non-integer coordinate in correspondence
+of a space dimension subject to wrapping.  It must be stressed that
+freedom to drop such points does not constitute an obligation to remove
+all of them (especially because this would be extraordinarily expensive
+on some numerical abstractions).
+The PPL provides operators for the more systematic
+\ref Dropping_Non_Integer_Points
+"removal of points with non-integral coordinates".
+
+The wrapping operator will only remove some of these points
+as a byproduct of its main task and only when this comes at a negligible
+extra cost.
 
 
 \section convex_polys Convex Polyhedra
diff --git a/src/globals.types.hh b/src/globals.types.hh
index 5ed9e76..546445d 100644
--- a/src/globals.types.hh
+++ b/src/globals.types.hh
@@ -75,7 +75,7 @@ enum Optimization_Mode {
   Widths of bounded integer types.
 
   See the section on
-  \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic".
+  \ref Approximating_Bounded_Integers "approximating bounded integers".
 */
 enum Bounded_Integer_Type_Width {
   //! \hideinitializer 8 bits.
@@ -98,7 +98,7 @@ enum Bounded_Integer_Type_Width {
   Representation of bounded integer types.
 
   See the section on
-  \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic".
+  \ref Approximating_Bounded_Integers "approximating bounded integers".
 */
 enum Bounded_Integer_Type_Representation {
   //! Unsigned binary.
@@ -115,7 +115,7 @@ enum Bounded_Integer_Type_Representation {
   Overflow behavior of bounded integer types.
 
   See the section on
-  \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic".
+  \ref Approximating_Bounded_Integers "approximating bounded integers".
 */
 enum Bounded_Integer_Type_Overflow {
   /*! \brief