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