Module: ppl/ppl Branch: master Commit: 992e9dc81a58f65429e7650ca2077fd95f1efda1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=992e9dc81a58f... Author: Enea Zaffanella <zaffanella@cs.unipr.it> Date: Sat Mar 31 10:20:08 2012 +0200 Further improvements to documentation of helper functions. --- src/linearize.hh | 190 ++++++++++++++++++++++++++++++++--------------------- 1 files changed, 115 insertions(+), 75 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 6bd75d8..1a074ae 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -32,30 +32,38 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a sum of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - The class template parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. The interval bounds - should have a floating point type. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>ADD</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. + + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. - \return <CODE>true</CODE> if the linearization succeeded, + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>ADD</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of sum floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -132,30 +140,38 @@ add_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a difference of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - The class template parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. The interval bounds - should have a floating point type. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>SUB</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. - \return <CODE>true</CODE> if the linearization succeeded, + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. + + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>SUB</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of difference floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -238,30 +254,38 @@ sub_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a product of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - The class template parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. The interval bounds - should have a floating point type. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>MUL</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. + + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. - \return <CODE>true</CODE> if the linearization succeeded, + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>MUL</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of multiplication floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -428,30 +452,38 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a division of floating point expressions. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - The class template parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. The interval bounds - should have a floating point type. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param bop_expr The binary operator concrete expression to linearize. - Its binary operator type must be <CODE>DIV</CODE>. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. - \return <CODE>true</CODE> if the linearization succeeded, + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. + + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + \param bop_expr + The binary operator concrete expression to linearize. + Its binary operator type must be <CODE>DIV</CODE>. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. + \par Linearization of division floating-point expressions Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -561,28 +593,36 @@ div_linearize(const Binary_Operator<Target>& bop_expr, return !result.overflows(); } -/*! \brief +/*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression Helper function used by <CODE>linearize</CODE> to linearize a cast floating point expression. - \par Template type parameters - - - The class template parameter \p Target specifies the implementation - of Concrete_Expression to be used. - - The class template parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. The interval bounds - should have a floating point type. - Makes \p result become the linearization of \p *this in the given composite abstract store. - \param cast_expr The cast operator concrete expression to linearize. - \param oracle The FP_Oracle to be queried. - \param lf_store The linear form abstract store. - \param result The modified linear form. + \tparam Target + A type template parameter specifying the instantiation of + Concrete_Expression to be used. - \return <CODE>true</CODE> if the linearization succeeded, + \tparam FP_Interval_Type + A type template parameter for the intervals used in the abstract domain. + The interval bounds should have a floating point type. + + \return + <CODE>true</CODE> if the linearization succeeded, <CODE>false</CODE> otherwise. + + \param cast_expr + The cast operator concrete expression to linearize. + + \param oracle + The FP_Oracle to be queried. + + \param lf_store + The linear form abstract store. + + \param result + The modified linear form. */ template <typename Target, typename FP_Interval_Type> static bool @@ -644,7 +684,7 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, } //! Linearizes a floating point expression. -/*! \relates Concrete_Expression +/*! \relates Parma_Polyhedra_Library::Concrete_Expression Makes \p result become a linear form that correctly approximates the value of \p expr in the given composite abstract store.