[PPL-devel] [GIT] ppl/ppl(floating_point): Added a trivial implementation of

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Fri Sep 25 11:40:55 2009 +0200

Added a trivial implementation of
generalized_refine_with_linear_form_inequality.

---

 src/Octagonal_Shape.defs.hh    |   34 ++++++++++++++++++++++++++++++++++
 src/Octagonal_Shape.inlines.hh |   27 +++++++++++++++++++++++++++
 2 files changed, 61 insertions(+), 0 deletions(-)

diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh
index 42166af..0accc69 100644
--- a/src/Octagonal_Shape.defs.hh
+++ b/src/Octagonal_Shape.defs.hh
@@ -1014,6 +1014,40 @@ public:
                    const Linear_Form< Interval<T, Interval_Info> >& right);
 
   /*! \brief
+    Refines the system of octagonal constraints defining \p *this using
+    the constraint expressed by \p left \f$\relsym\f$ \p right, where
+    \f$\relsym\f$ is the relation symbol specified by \p relsym.
+
+    \param left
+    The linear form on intervals with floating point boundaries that
+    is at the left of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \param right
+    The linear form on intervals with floating point boundaries that
+    is at the right of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \param relsym
+    The relation symbol.
+
+    \exception std::invalid_argument
+    Thrown if \p left (or \p right) is dimension-incompatible with \p *this.
+
+    \exception std::runtime_error
+    Thrown if \p relsym is not a valid relation symbol.
+
+    This function is used in abstract interpretation to model a filter
+    that is generated by a comparison of two expressions that are correctly
+    approximated by \p left and \p right respectively.
+  */
+  template <typename Interval_Info>
+  void generalized_refine_with_linear_form_inequality(
+                   const Linear_Form< Interval<T, Interval_Info> >& left,
+                   const Linear_Form< Interval<T, Interval_Info> >& right,
+                   Relation_Symbol relsym);
+
+  /*! \brief
     Computes the \ref Cylindrification "cylindrification" of \p *this with
     respect to space dimension \p var, assigning the result to \p *this.
 
diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh
index cee791c..73e4124 100644
--- a/src/Octagonal_Shape.inlines.hh
+++ b/src/Octagonal_Shape.inlines.hh
@@ -615,6 +615,33 @@ Octagonal_Shape<T>::strictly_contains(const Octagonal_Shape& y) const {
 template <typename T>
 template <typename Interval_Info>
 inline void
+Octagonal_Shape<T>::generalized_refine_with_linear_form_inequality(
+		    const Linear_Form< Interval<T, Interval_Info> >& left,
+		    const Linear_Form< Interval<T, Interval_Info> >& right,
+                    Relation_Symbol relsym) {
+  switch (relsym) {
+  case EQUAL:
+    refine_with_linear_form_inequality(left, right);
+    refine_with_linear_form_inequality(right, left);
+    break;
+  case LESS_THAN:
+  case LESS_OR_EQUAL:
+    refine_with_linear_form_inequality(left, right);
+    break;
+  case GREATER_THAN:
+  case GREATER_OR_EQUAL:
+    refine_with_linear_form_inequality(right, left);
+    break;
+  case NOT_EQUAL:
+    break;
+  default:
+    throw std::runtime_error("PPL internal error");
+  }
+}
+
+template <typename T>
+template <typename Interval_Info>
+inline void
 Octagonal_Shape<T>::
 refine_fp_interval_abstract_store(
 	  Box< Interval<T, Interval_Info> >& store) const {