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

Author: Fabio Bossi bossi@cs.unipr.it Date: Mon Sep 21 14:19:43 2009 +0200

Wrote a first implementation of refine_with_linear_form_inequality.

---

src/Polyhedron.defs.hh | 6 ++++ src/Polyhedron.templates.hh | 54 ++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 57 insertions(+), 3 deletions(-)

diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index d904386..0ef020c 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -979,6 +979,12 @@ public: */ void refine_with_congruences(const Congruence_System& cgs);

+ template <typename FP_Format, typename Interval_Info> + 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 std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store); + /*! \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/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 9f4f333..a8e2a07 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -298,6 +298,53 @@ Polyhedron::map_space_dimensions(const Partial_Function& pfunc) {

template <typename FP_Format, typename Interval_Info> 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 std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { + + // Check that FP_Format is indeed a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, + "Polyhedron::affine_image:" + " FP_Format not a floating point type."); + + // Dimension compatibility checks. + // The dimensions of left and right should not be greater than the + // dimension of *this. + const dimension_type left_space_dim = left.space_dimension(); + if (space_dim < left_space_dim) + throw_dimension_incompatible( + "refine_with_linear_form_inequality(l1, l2, s)", "l1", left); + + const dimension_type right_space_dim = right.space_dimension(); + if (space_dim < right_space_dim) + throw_dimension_incompatible( + "refine_with_linear_form_inequality(l1, l2, s)", "l2", right); + + // We assume that the analyzer will not refine an unreachable test. + PPL_ASSERT(!marked_empty()); + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; + + // Overapproximate left - right. + FP_Linear_Form left_minus_right(left); + left_minus_right -= right; + dimension_type lf_space_dim = left_minus_right.space_dimension(); + FP_Linear_Form lf_approx; + overapproximate_linear_form(left_minus_right, lf_space_dim, store, lf_approx); + + // Normalize left - right. + Linear_Expression lf_approx_le; + convert_to_integer_expression(lf_approx, lf_space_dim, lf_approx_le); + + // Finally, do the refinement. + refine_with_constraint(lf_approx_le <= 0); + +} + +template <typename FP_Format, typename Interval_Info> +void Polyhedron::affine_image(const Variable& var, const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { @@ -318,7 +365,7 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) { if (space_dim < var_id + 1) throw_dimension_incompatible("affine_image(v, l, s)", "v", var);

- // We suppose that the analyzer will not filter an unreachable test. + // We assume that the analyzer will not perform an unreachable assignment. PPL_ASSERT(!marked_empty());

typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; @@ -363,6 +410,7 @@ Polyhedron::overapproximate_linear_form( typedef std::map<dimension_type, FP_Interval_Type> Interval_Abstract_Store;

result = FP_Linear_Form(lf.inhomogeneous_term()); + // FIXME: this may not be policy-neutral. const FP_Interval_Type aux_divisor1(static_cast<FP_Format>(0.5)); FP_Interval_Type aux_divisor2(aux_divisor1); aux_divisor2.lower() = static_cast<FP_Format>(-0.5); @@ -398,7 +446,7 @@ Polyhedron::convert_to_integer_expression( result = Linear_Expression();

typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+1); std::vector<Coefficient> denominators(lf_dimension+1);

@@ -408,7 +456,7 @@ Polyhedron::convert_to_integer_expression( lcm = 1; const FP_Interval_Type& b = lf.inhomogeneous_term(); // FIXME: are these checks numerator[i] != 0 really necessary? - numer_denom(b.upper(), numerators[lf_dimension], + numer_denom(b.lower(), numerators[lf_dimension], denominators[lf_dimension]); if (numerators[lf_dimension] != 0) lcm_assign(lcm, lcm, denominators[lf_dimension]);