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

Author: Roberto Amadini r.amadini@virgilio.it Date: Mon Sep 21 18:02:31 2009 +0200

Implemented a preliminary (yet untested) version of methods BD_Shape::linear_form_upper_bound and BD_Shape::two_variables_affine_image.

---

src/BD_Shape.defs.hh | 14 ++- src/BD_Shape.templates.hh | 119 ++++++++++++++++++++++++++- tests/Floating_Point_Expression/bdshape1.cc | 1 - 3 files changed, 125 insertions(+), 9 deletions(-)

diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 96a3fd7..3dc29bb 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -2088,15 +2088,21 @@ private: const Interval<T, Interval_Info>& w_coeff, const dimension_type& w_id, const dimension_type& space_dim); - + /* \brief Auxiliary function for \ref affine_relation "affine image" that handle the general case: \f$l \equal ax + by + c\f$ */ template <typename Interval_Info> - void two_variables_affine_image(const Variable& var, - const dimension_type& var_id, - const Linear_Form< Interval<T,Interval_Info> >& lf); + void two_variables_affine_image(const dimension_type& var_id, + const Linear_Form< Interval<T,Interval_Info> >& lf, + const dimension_type& space_dim); + + template <typename Interval_Info> + void linear_form_upper_bound( + const Linear_Form< Interval<T, Interval_Info> >& lf, + N& result, + const dimension_type& space_dim) const;

//! An helper function for the computation of affine relations. /*! diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 734f503..5cbf5a5 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4108,7 +4108,7 @@ BD_Shape<T>::affine_image(const Variable& var, return; }

- //two_variables_affine_image(var, var_id, lf); + two_variables_affine_image(var_id, lf, space_dim); PPL_ASSERT(OK()); }

@@ -4237,11 +4237,122 @@ void BD_Shape<T> template <typename T> template <typename Interval_Info> void BD_Shape<T> -::two_variables_affine_image(const Variable& var, - const dimension_type& var_id, - const Linear_Form< Interval<T, Interval_Info> >& lf) { +::two_variables_affine_image(const dimension_type& var_id, + const Linear_Form< Interval<T, Interval_Info> >& lf, + const dimension_type& space_dim) { + + reset_shortest_path_closed(); + + Linear_Form< Interval<T, Interval_Info> > minus_lf(lf); + minus_lf.negate(); + + // Declare temporaries outside the loop. + PPL_DIRTY_TEMP(N, upper_bound); + + // Update binary constraints on var FIRST. + for (dimension_type curr_var = 1; curr_var < var_id; ++curr_var) { + Variable current(curr_var - 1); + linear_form_upper_bound(lf - current, upper_bound, space_dim); + assign_r(dbm[curr_var][var_id], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf + current, upper_bound, space_dim); + assign_r(dbm[var_id][curr_var], upper_bound, ROUND_NOT_NEEDED); + } + for (dimension_type curr_var = var_id + 1; curr_var <= space_dim; + ++curr_var) { + Variable current(curr_var - 1); + linear_form_upper_bound(lf - current, upper_bound, space_dim); + assign_r(dbm[curr_var][var_id], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf + current, upper_bound, space_dim); + assign_r(dbm[var_id][curr_var], upper_bound, ROUND_NOT_NEEDED); + } + // Finally, update unary constraints on var. + PPL_DIRTY_TEMP(N, lf_ub); + linear_form_upper_bound(lf, lf_ub, space_dim); + PPL_DIRTY_TEMP(N, minus_lf_ub); + linear_form_upper_bound(minus_lf, minus_lf_ub, space_dim); + assign_r(dbm[0][var_id], lf_ub, ROUND_NOT_NEEDED); + assign_r(dbm[var_id][0], minus_lf_ub, ROUND_NOT_NEEDED); }

+template <typename T> +template <typename Interval_Info> +void +BD_Shape<T>:: +linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, + N& result, + const dimension_type& space_dim) const { + + // Check that T is a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "BD_Shape<T>::linear_form_upper_bound:" + " T not a floating point type."); + + const dimension_type lf_space_dimension = lf.space_dimension(); + PPL_ASSERT(lf_space_dimension <= space_dim); + + typedef Interval<T, Interval_Info> FP_Interval_Type; + + PPL_DIRTY_TEMP(N, curr_lb); + PPL_DIRTY_TEMP(N, curr_ub); + PPL_DIRTY_TEMP(N, curr_var_ub); + PPL_DIRTY_TEMP(N, curr_minus_var_ub); + + PPL_DIRTY_TEMP(N, first_comparison_term); + PPL_DIRTY_TEMP(N, second_comparison_term); + + PPL_DIRTY_TEMP(N, negator); + + assign_r(result, lf.inhomogeneous_term().upper(), ROUND_NOT_NEEDED); + + for (dimension_type curr_var = 0, n_var = 0; curr_var < lf_space_dimension; + ++curr_var) { + n_var = curr_var + 1; + const FP_Interval_Type& curr_coefficient = + lf.coefficient(Variable(curr_var)); + assign_r(curr_lb, curr_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(curr_ub, curr_coefficient.upper(), ROUND_NOT_NEEDED); + if (curr_lb != 0 || curr_ub != 0) { + assign_r(curr_var_ub, dbm[0][n_var], ROUND_NOT_NEEDED); + neg_assign_r(curr_minus_var_ub, dbm[n_var][0], ROUND_NOT_NEEDED); + // Optimize the most commons cases: curr = +/-[1;1] + if (curr_lb == 1 && curr_ub == 1) { + add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub), + ROUND_UP); + } + else if (curr_lb == -1 && curr_ub == -1) { + neg_assign_r(negator, std::min(curr_var_ub, curr_minus_var_ub), + ROUND_NOT_NEEDED); + add_assign_r(result, result, negator, ROUND_UP); + } + else { + // Next addend will be the maximum of four quantities. + assign_r(first_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, + ROUND_UP); + add_mul_assign_r(second_comparison_term, curr_var_ub, curr_lb, + ROUND_UP); + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, + ROUND_UP); + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_lb, + ROUND_UP); + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + + add_assign_r(result, result, first_comparison_term, ROUND_UP); + } + } + } +}

template <typename T> void diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index a9886b4..e5f06d1 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -244,7 +244,6 @@ bool test08() { known_result.add_constraint(A <= 12); known_result.add_constraint(B <= 2); known_result.add_constraint(B >= -10); - //known_result.add_constraint(-B - A <= 0); known_result.add_constraint(-A + B <= 4); known_result.add_constraint(A - B <= 22); print_constraints(known_result, "*** known_result ***");