[PPL-devel] [GIT] ppl/ppl(floating_point): Added generalized_refine_with_linear_form_inequality.
Fabio Bossi
bossi at cs.unipr.it
Wed Sep 29 18:21:14 CEST 2010
Module: ppl/ppl
Branch: floating_point
Commit: 7d65c1696bed13d29185ce2b078d558188b81d45
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d65c1696bed13d29185ce2b078d558188b81d45
Author: Fabio Bossi <bossi at cs.unipr.it>
Date: Wed Sep 29 18:20:41 2010 +0200
Added generalized_refine_with_linear_form_inequality.
---
src/BD_Shape.defs.hh | 34 ++++++++++++++++++++++++++++++++++
src/BD_Shape.inlines.hh | 28 ++++++++++++++++++++++++++++
2 files changed, 62 insertions(+), 0 deletions(-)
diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh
index 0ad832c..cd8147f 100644
--- a/src/BD_Shape.defs.hh
+++ b/src/BD_Shape.defs.hh
@@ -1037,6 +1037,40 @@ public:
const Linear_Form< Interval<T, Interval_Info> >& left,
const Linear_Form< Interval<T, Interval_Info> >& right);
+ /*! \brief
+ Refines the system of BD_Shape 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);
+
//! Applies to \p dest the interval constraints embedded in \p *this.
/*!
\param dest
diff --git a/src/BD_Shape.inlines.hh b/src/BD_Shape.inlines.hh
index 275b0df..9fe4f7b 100644
--- a/src/BD_Shape.inlines.hh
+++ b/src/BD_Shape.inlines.hh
@@ -839,6 +839,34 @@ BD_Shape<T>::hash_code() const {
template <typename T>
template <typename Interval_Info>
inline void
+BD_Shape<T>::generalized_refine_with_linear_form_inequality(
+ const Linear_Form< Interval<T, Interval_Info> >& left,
+ const Linear_Form< Interval<T, Interval_Info> >& right,
+ const Relation_Symbol relsym) {
+ switch (relsym) {
+ case EQUAL:
+ // TODO: see if we can handle this case more efficiently.
+ 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
BD_Shape<T>::refine_fp_interval_abstract_store(
Box< Interval<T, Interval_Info> >& store) const {
More information about the PPL-devel
mailing list