Module: ppl/ppl Branch: floating_point Commit: 7d65c1696bed13d29185ce2b078d558188b81d45 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d65c1696bed1... Author: Fabio Bossi <bossi@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 {