Module: ppl/ppl Branch: floating_point Commit: 7de79be86951bff882f83eea17bcfcfbcd7a52b5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7de79be86951b...
Author: Fabio Biselli fabio.biselli@studenti.unipr.it Date: Thu Sep 10 12:37:26 2009 +0200
Updated intervalize documentation; Updated Opposite_Floating_Point_Expression documentation;
---
src/Floating_Point_Expression.defs.hh | 16 +++++++++++++--- src/Opposite_Floating_Point_Expression.defs.hh | 16 +++++++++++----- 2 files changed, 24 insertions(+), 8 deletions(-)
diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index f8c8df3..16ca411 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -52,7 +52,7 @@ struct IEEE754_Double { A floating point expression on a given format.
This class represents a concrete - <EM>floating point expression</EM> of format \f$$\mathbf{f}$\f$, this + <EM>floating point expression</EM> of format \f$$\mathbf{f}$\f$, this includes constants, variables of format \f$$\mathbf{f}$\f$, binary and unary arithmetic operators.
@@ -114,7 +114,7 @@ public: \param int_store The interval abstract store. \param lf_store The linear form abstract store. \param result The modified linear form. - + All variables occuring in the floating point expression MUST have an associated interval in \p int_store. If this precondition is not met, calling the method causes an @@ -162,7 +162,7 @@ public: (\textrm{max}(|a|,|b|) \amifp [-2^{-\textrm{p}};2^{-\textrm{p}}]) + \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) - \amifp + \amifp [-2^{-\textrm{p}};2^{-\textrm{p}}])v \f] where p is the fraction size in bits for the format \f$\mathbf{f}\f$. @@ -176,6 +176,16 @@ public: \param lf The linear form to aproximate. \param store The abstract store. \param result The linear form that will be modified. + + This method modifies the given linear form <CODE>result</CODE> like + a function \f$\iota(l)\rho^{#}\f$ on a linear form \f$l\f$ in an + abstract store \f$\rho^{#}\f$, such as: + \f[ + \iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{#} + = + i \asifp \left(\bigoplus_{v \in \cV}{}_{\mathbf{f}}^{#}i_{v} \amifp + \rho^{#}(v)\right) + \f] */ static void intervalize(const FP_Linear_Form& lf, const FP_Interval_Abstract_Store& store, diff --git a/src/Opposite_Floating_Point_Expression.defs.hh b/src/Opposite_Floating_Point_Expression.defs.hh index 627545c..16245bf 100644 --- a/src/Opposite_Floating_Point_Expression.defs.hh +++ b/src/Opposite_Floating_Point_Expression.defs.hh @@ -43,12 +43,13 @@ void swap(Parma_Polyhedra_Library::Opposite_Floating_Point_Expression<
namespace Parma_Polyhedra_Library {
-//! A generic Opposite Floating Point Expression -/*! \ingroup PPL_CXX_interface - The class template type parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. +/*! \brief + A generic Opposite Floating Point Expression. + \ingroup PPL_CXX_interface
- The class template type parameter \p FP_Format represents the format + - The class template type parameter \p FP_Interval_Type represents the type + 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. */ template <typename FP_Interval_Type, typename FP_Format> @@ -109,6 +110,11 @@ public: /* \brief Returns a linear form in the abstract store \p store that simply represents the opposite of the operand linearization. + + \param int_store The interval abstract store. + \param lf_store The linear form abstract store. + \param result The modified linear form. + */ void linearize(const FP_Interval_Abstract_Store& int_store, const FP_Linear_Form_Abstract_Store& lf_store,