Fabio Bossi bossi at cs.unipr.it
Wed Sep 16 17:23:56 CEST 2009

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Wed Sep 16 17:26:27 2009 +0200

---

src/Octagonal_Shape.defs.hh |   48 +++++++++++++++++++++++++++++++++++++++++++
1 files changed, 48 insertions(+), 0 deletions(-)

diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh
index 5ac7536..6ebd381 100644
--- a/src/Octagonal_Shape.defs.hh
+++ b/src/Octagonal_Shape.defs.hh
@@ -988,6 +988,23 @@ public:
*/
void refine_with_congruences(const Congruence_System& cgs);

+  /*! \brief
+    Refines the system of octagonal constraints defining \p *this using
+    the constraint expressed by \p left \f$\f$ \p right.
+
+    \param left
+    The linear form on intervals with floating point coefficients that
+    is on the left of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \param right
+    The linear form on intervals with floating point coefficients that
+    is on the right of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \exception std::invalid_argument
+    Thrown if \p left (or \p right) is dimension-incompatible with \p *this.
+  */
template <typename Interval_Info>
void refine_with_linear_form_inequality(
const Linear_Form< Interval<T, Interval_Info> >& left,
@@ -1113,6 +1130,22 @@ public:
Coefficient_traits::const_reference  denominator
= Coefficient_one());

+  /*! \brief
+    Assigns to \p *this the \ref affine_relation "affine image"
+    of \p *this under the function mapping variable \p var into the
+    affine expression(s) specified by \p lf.
+
+    \param var
+    The variable to which the affine expression is assigned.
+
+    \param lf
+    The linear form on intervals with floating point coefficients that
+    defines the affine expression. ALL of its coefficients MUST be boundend.
+
+    \exception std::invalid_argument
+    Thrown if \p lf and \p *this are dimension-incompatible or if \p var
+    is not a dimension of \p *this.
+  */
template <typename Interval_Info>
void affine_image(Variable var,
const Linear_Form< Interval<T, Interval_Info> >& lf);
@@ -1698,6 +1731,11 @@ public:
*/
void fold_space_dimensions(const Variables_Set& vars, Variable dest);

+  //! Refines \p store with the constraints defining \p *this.
+  /*!
+    \param store
+    The interval floating point abstract store to refine.
+  */
template <typename Interval_Info>
void refine_fp_interval_abstract_store(
std::map< dimension_type, Interval<T, Interval_Info> >& store);
@@ -1803,6 +1841,16 @@ private:
N& matrix_at(dimension_type i, dimension_type j);
const N& matrix_at(dimension_type i, dimension_type j) const;

+  /*! \brief
+    Returns an upper bound for \p lf according to the constraints
+    embedded in \p *this.
+
+    \p lf must be a linear form on intervals with floating point coefficients.
+    If all coefficients in \p lf are bounded, then \p result will become a
+    correct overapproximation of the value of \p lf when variables in
+    \p lf satisfy the constraints expressed by \p *this. Otherwise the
+    behavior of the method is undefined.
+  */
template <typename Interval_Info>
void linear_form_upper_bound(
const Linear_Form< Interval<T, Interval_Info> >& lf,