Module: ppl/ppl Branch: floating_point Commit: 1e570d889993548394bae0a46b74d99477961748 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1e570d8899935...

Author: Fabio Biselli fabio.biselli@studenti.unipr.it Date: Tue Sep 8 12:33:45 2009 +0200

Fixed documentation

---

doc/ppl.sty | 5 +++++ src/Floating_Point_Expression.defs.hh | 2 ++ src/Sum_Floating_Point_Expression.defs.hh | 12 +++++++++++- 3 files changed, 18 insertions(+), 1 deletions(-)

diff --git a/doc/ppl.sty b/doc/ppl.sty index 7282dc7..b35a373 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -176,3 +176,8 @@ \newcommand*{\entailsP}{\entailss{\smallP}} \newcommand*{\NentailsP}{\Nentailss{\smallP}} \newcommand*{\sentailsP}{\sentailss{\smallP}} + + +% Interval floating point arithmetics + +\newcommand*{\asifp}{\oplus^{#}_{\mathbf{f}}} diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index a3e7b59..079995d 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -103,6 +103,7 @@ public: //! Destructor. virtual ~Floating_Point_Expression();

+ //! Linearizes a floating point expression. /*! \brief Makes \p result become a Linear Form that correctly approximates the value of the floating point expression in the given composite @@ -140,6 +141,7 @@ public: */ static bool overflows(const FP_Linear_Form& lf);

+ //! Computes the relative error of a given linear form. /*! \brief Static helper method that is used by <CODE>linearize</CODE> to account for the relative errors on \p lf. diff --git a/src/Sum_Floating_Point_Expression.defs.hh b/src/Sum_Floating_Point_Expression.defs.hh index fcf1523..0df171c 100644 --- a/src/Sum_Floating_Point_Expression.defs.hh +++ b/src/Sum_Floating_Point_Expression.defs.hh @@ -52,6 +52,16 @@ namespace Parma_Polyhedra_Library { of the intervals used in the abstract domain. - The class template type parameter \p FP_Format represents the format of the floating point variable used in the concrete domain. + + \par Linearizations of floating-point sum expressions + + Let \f$i + \sum_{v \in V}i_{v}v \f$ be a linear form we define an abstract + operator \f$\boxplus^{#}\f$: + \f[ + (i + \sum_{v \in V}i_{v}v)\boxplus^{#}(i' + \sum_{v \in V}i'_{v}v) + = + (i \asifp i') + \sum_{v \in V}(i_{v} \asifp i'_{v})v + \f] */ template <typename FP_Interval_Type, typename FP_Format> class Sum_Floating_Point_Expression @@ -61,7 +71,7 @@ public:

/*! \brief Alias for the Linear_Form<FP_Interval_Type> from - Floating_Point_Expression + Floating_Point_Expression. */ typedef typename Floating_Point_Expression<FP_Interval_Type, FP_Format>