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