[PPL-devel] [GIT] ppl/ppl(floating_point): Implemented generalized_refine_with_linear_form_inequality.

[Fabio Bossi]

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

Author: Fabio Bossi <bossi at cs.unipr.it>
Date:   Fri Sep 25 14:31:28 2009 +0200

Implemented generalized_refine_with_linear_form_inequality.
Adapted refine_with_linear_form_inequality to accept strict inequalities
on not necessarily closed polyhedra.

---

 src/Polyhedron.defs.hh      |   51 ++++++++++++++++++++++++++++++++++++++++--
 src/Polyhedron.inlines.hh   |   31 ++++++++++++++++++++++++++
 src/Polyhedron.templates.hh |    8 +++++-
 3 files changed, 85 insertions(+), 5 deletions(-)

diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index 74eeb78..c3a33cb 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -978,9 +978,10 @@ public:
   */
   void refine_with_congruences(const Congruence_System& cgs);
 
-  /*!
-    Refines \p *this with the constraint expressed by \p left \f$\leq\f$
-    \p right.
+  /*! \brief
+    Refines \p *this with the constraint expressed by \p left \f$<\f$
+    \p right if \p is_strict is set, with the constraint \p left \f$\leq\f$
+    \p right otherwise.
 
     \param left
     The linear form on intervals with floating point boundaries that
@@ -997,6 +998,9 @@ public:
     performed. All variables that occur in \p left or \p right MUST have
     an associated interval in it, and all of these intervals MUST be bounded.
 
+    \param is_strict
+    True if the comparison is strict.
+
     \exception std::invalid_argument
     Thrown if \p left (or \p right) is dimension-incompatible with \p *this.
 
@@ -1008,6 +1012,47 @@ public:
   void refine_with_linear_form_inequality(
   const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
   const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
+  const Box< Interval<FP_Format, Interval_Info> >& store,
+  bool is_strict = false);
+
+  /*! \brief
+    Refines \p *this with 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 on 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 on the right of the comparison operator. All of its coefficients
+    MUST be bounded.
+
+    \param relsym
+    The relation symbol.
+
+    \param store
+    The interval abstract store in which the test defining the filter is
+    performed. All variables that occur in \p left or \p right MUST have
+    an associated interval in it, and all of these intervals MUST be bounded.
+
+    \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 FP_Format, typename Interval_Info>
+  void generalized_refine_with_linear_form_inequality(
+  const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
+  const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
+  Relation_Symbol relsym,
   const Box< Interval<FP_Format, Interval_Info> >& store);
 
   //! Refines \p store with the constraints defining \p *this.
diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh
index 5de0af8..affc433 100644
--- a/src/Polyhedron.inlines.hh
+++ b/src/Polyhedron.inlines.hh
@@ -374,6 +374,37 @@ Polyhedron::add_recycled_congruences(Congruence_System& cgs) {
 
 template <typename FP_Format, typename Interval_Info>
 inline void
+Polyhedron::generalized_refine_with_linear_form_inequality(
+	    const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
+	    const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
+            Relation_Symbol relsym,
+            const Box< Interval<FP_Format, Interval_Info> >& store) {
+  switch (relsym) {
+  case EQUAL:
+    refine_with_linear_form_inequality(left, right, store, false);
+    refine_with_linear_form_inequality(right, left, store, false);
+    break;
+  case LESS_THAN:
+    refine_with_linear_form_inequality(left, right, store, true);
+    break;
+  case LESS_OR_EQUAL:
+    refine_with_linear_form_inequality(left, right, store, false);
+    break;
+  case GREATER_THAN:
+    refine_with_linear_form_inequality(right, left, store, true);
+    break;
+  case GREATER_OR_EQUAL:
+    refine_with_linear_form_inequality(right, left, store, false);
+    break;
+  case NOT_EQUAL:
+    break;
+  default:
+    throw std::runtime_error("PPL internal error");
+  }
+}
+
+template <typename FP_Format, typename Interval_Info>
+inline void
 Polyhedron::
 refine_fp_interval_abstract_store(
        Box< Interval<FP_Format, Interval_Info> >& store) const {
diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh
index 074e717..e12b6fd 100644
--- a/src/Polyhedron.templates.hh
+++ b/src/Polyhedron.templates.hh
@@ -300,7 +300,8 @@ void
 Polyhedron::refine_with_linear_form_inequality(
   const Linear_Form< Interval<FP_Format, Interval_Info> >& left,
   const Linear_Form< Interval<FP_Format, Interval_Info> >& right,
-  const Box< Interval<FP_Format, Interval_Info> >& store) {
+  const Box< Interval<FP_Format, Interval_Info> >& store,
+  bool is_strict) {
 
   // Check that FP_Format is indeed a floating point type.
   PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,
@@ -340,7 +341,10 @@ Polyhedron::refine_with_linear_form_inequality(
   convert_to_integer_expression(lf_approx, lf_space_dim, lf_approx_le);
 
   // Finally, do the refinement.
-  refine_with_constraint(lf_approx_le <= 0);
+  if (!is_strict || is_necessarily_closed())
+    refine_with_constraint(lf_approx_le <= 0);
+  else
+    refine_with_constraint(lf_approx_le < 0);
 }
 
 template <typename FP_Format, typename Interval_Info>