September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Removed a temporary using sub_assign_r instead of add_assign_r
by Fabio Biselli 20 Sep '09

20 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 3e9f4582ce7ab1d65f1d606feb49231c76bd951b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e9f4582ce7a… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Sun Sep 20 13:20:56 2009 +0200 Removed a temporary using sub_assign_r instead of add_assign_r --- src/BD_Shape.templates.hh | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index a90470f..6d44f5e 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4117,7 +4117,7 @@ BD_Shape<T>::affine_image(const Variable& var, PPL_ASSERT(OK()); } -// Case 1: var = [-mlb, ub]. +// Case 1: var = [-b, b]. template <typename T> template <typename Interval_Info> void @@ -4218,11 +4218,9 @@ void BD_Shape<T> // We have to add the constraint `v + w == b', over-approximating it // by computing lower and upper bounds for `w'. const N& lb_w = dbm[w_id][0]; - PPL_DIRTY_TEMP(N, minus_lb_w); - neg_assign_r(minus_lb_w, lb_w, ROUND_UP); if (!is_plus_infinity(lb_w)) { // Add the constraint `v <= ub - lb_w'. - add_assign_r(dbm[0][var_id], b_ub, minus_lb_w, ROUND_UP); + sub_assign_r(dbm[0][var_id], b_ub, lb_w, ROUND_UP); reset_shortest_path_closed(); } const N& ub_w = dbm[0][w_id];

1 0

[GIT] ppl/ppl(floating_point): Bugs fixes
by Fabio Biselli 20 Sep '09

20 Sep '09

Module: ppl/ppl Branch: floating_point Commit: aeb5980a47c2659e5c2b6cd17369ee8e0bafcb47 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aeb5980a47c2… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Sun Sep 20 02:09:24 2009 +0200 Bugs fixes --- src/BD_Shape.defs.hh | 20 +++----- src/BD_Shape.templates.hh | 71 ++++++++++++++------------- tests/Floating_Point_Expression/bdshape1.cc | 10 ++-- 3 files changed, 50 insertions(+), 51 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 549e6b2..96a3fd7 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -2075,24 +2075,20 @@ private: the general case: \f$l \equal c\f$ */ template <typename Interval_Info> - void inhomogeneous_affine_image(const Variable& var, - const dimension_type& var_id, - const N& ub, - const N& mlb); + void inhomogeneous_affine_image(const dimension_type& var_id, + const Interval<T, Interval_Info>& b); /* \brief Auxiliary function for \ref affine_relation "affine image" that handle the general case: \f$l \equal ax + c\f$ */ template <typename Interval_Info> - void one_variable_affine_image(const Variable& var, - const dimension_type& var_id, - const Interval<T, Interval_Info>& w_coeff, - const dimension_type& w_id, - const N& ub, - const N& mlb, - const dimension_type& space_dim); - + void one_variable_affine_image(const dimension_type& var_id, + const Interval<T, Interval_Info>& b, + 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$ diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index c4b6417..a90470f 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4096,20 +4096,14 @@ BD_Shape<T>::affine_image(const Variable& var, // variable; // - If t == 2, the linear form 'lf' is of the general form. - PPL_DIRTY_TEMP(N, b_ub); - assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); - PPL_DIRTY_TEMP(N, b_mlb); - neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED); - if (t == 0) { - inhomogeneous_affine_image(var, var_id, b_ub, b_mlb); + inhomogeneous_affine_image(var_id, b); PPL_ASSERT(OK()); return; } else if (t == 1) { const FP_Interval_Type& w_coeff = lf.coefficient(Variable(w_id - 1)); - one_variable_affine_image(var, var_id, b, w_coeff, w_id, - b_ub, b_mlb, space_dim); + one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim); PPL_ASSERT(OK()); return; } @@ -4119,7 +4113,7 @@ BD_Shape<T>::affine_image(const Variable& var, // lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, // or t == 1, lf == i*w + b, but i <> [+/-1;+/-1]. - two_variables_affine_image(var, var_id, lf); + //two_variables_affine_image(var, var_id, lf); PPL_ASSERT(OK()); } @@ -4127,18 +4121,21 @@ BD_Shape<T>::affine_image(const Variable& var, template <typename T> template <typename Interval_Info> void -BD_Shape<T>::inhomogeneous_affine_image(const Variable& var, - const dimension_type& var_id, - const N& ub, - const N& mlb) { +BD_Shape<T>::inhomogeneous_affine_image(const dimension_type& var_id, + const Interval<T, Interval_Info>& b) { + PPL_DIRTY_TEMP(N, b_ub); + assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, b_mlb); + neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED); + // Remove all constraints on `var'. - forget_all_dbm_constraints(var); + forget_all_dbm_constraints(var_id); // Shortest-path closure is preserved, but not reduction. if (marked_shortest_path_reduced()) reset_shortest_path_reduced(); // Add the constraint `var >= lb && var <= ub'. - add_dbm_constraint(0, var_id, ub); - add_dbm_constraint(var_id, 0, mlb); + add_dbm_constraint(0, var_id, b_ub); + add_dbm_constraint(var_id, 0, b_mlb); return; } @@ -4146,18 +4143,20 @@ BD_Shape<T>::inhomogeneous_affine_image(const Variable& var, // or another variable. template <typename T> template <typename Interval_Info> -void -BD_Shape<T>::one_variable_affine_image(const Variable& var, - const dimension_type& var_id, - const Interval<T, Interval_Info>& w_coeff, - const dimension_type& w_id, - const N& ub, - const N& mlb, - const dimension_type& space_dim) { +void BD_Shape<T> +::one_variable_affine_image(const dimension_type& var_id, + const Interval<T, Interval_Info>& b, + const Interval<T, Interval_Info>& w_coeff, + const dimension_type& w_id, + const dimension_type& space_dim) { + PPL_DIRTY_TEMP(N, b_ub); + assign_r(b_ub, b.upper(), ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, b_mlb); + neg_assign_r(b_mlb, b.lower(), ROUND_NOT_NEEDED); // true if b = [b_lb, b_ub] = [-mlb, ub] = [0;0]. - bool is_b_zero = (mlb == 0 && ub == 0); + bool is_b_zero = (b_mlb == 0 && b_ub == 0); // true if w_coeff = [1;1] bool is_w_coeff_one = (w_coeff == 1); // true if w_coeff = [-1;-1]. @@ -4175,9 +4174,9 @@ BD_Shape<T>::one_variable_affine_image(const Variable& var, DB_Row<N>& dbm_v = dbm[var_id]; for (dimension_type i = space_dim + 1; i-- > 0; ) { N& dbm_vi = dbm_v[i]; - add_assign_r(dbm_vi, dbm_vi, mlb, ROUND_UP); + add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP); N& dbm_iv = dbm[i][var_id]; - add_assign_r(dbm_iv, dbm_iv, ub, ROUND_UP); + add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP); } // Both shortest-path closure and reduction are preserved. } @@ -4186,7 +4185,7 @@ BD_Shape<T>::one_variable_affine_image(const Variable& var, else { // Here `w_coeff = [-1;-1]. // Remove the binary constraints on `var'. - forget_binary_dbm_constraints(var); + forget_binary_dbm_constraints(var_id); std::swap(dbm[var_id][0], dbm[0][var_id]); // Shortest-path closure is not preserved. reset_shortest_path_closed(); @@ -4194,9 +4193,9 @@ BD_Shape<T>::one_variable_affine_image(const Variable& var, // Translate the unary constraints on `var' by adding the value // `b_ub' or subtracting the value `b_lb'. N& dbm_v0 = dbm[var_id][0]; - add_assign_r(dbm_v0, dbm_v0, ub, ROUND_UP); + add_assign_r(dbm_v0, dbm_v0, b_ub, ROUND_UP); N& dbm_0v = dbm[0][var_id]; - add_assign_r(dbm_v0, dbm_0v, mlb, ROUND_UP); + add_assign_r(dbm_v0, dbm_0v, b_mlb, ROUND_UP); } } } @@ -4204,7 +4203,7 @@ BD_Shape<T>::one_variable_affine_image(const Variable& var, // Here `w != var', so that `lf' is of the form // [+/-1;+/-1] * w + b. // Remove all constraints on `var'. - forget_all_dbm_constraints(var); + forget_all_dbm_constraints(var_id); // Shortest-path closure is preserved, but not reduction. if (marked_shortest_path_reduced()) reset_shortest_path_reduced(); @@ -4212,22 +4211,24 @@ BD_Shape<T>::one_variable_affine_image(const Variable& var, if (is_w_coeff_one) { // Add the new constraints `var - w >= b_lb' // `and var - w <= b_ub'. - add_dbm_constraint(w_id, var_id, ub); - add_dbm_constraint(var_id, w_id, mlb); + add_dbm_constraint(w_id, var_id, b_ub); + add_dbm_constraint(var_id, w_id, b_mlb); } else { // We have to add the constraint `v + w == b', over-approximating it // by computing lower and upper bounds for `w'. const N& lb_w = dbm[w_id][0]; + PPL_DIRTY_TEMP(N, minus_lb_w); + neg_assign_r(minus_lb_w, lb_w, ROUND_UP); if (!is_plus_infinity(lb_w)) { // Add the constraint `v <= ub - lb_w'. - add_assign_r(dbm[0][var_id], ub, -lb_w, ROUND_UP); + add_assign_r(dbm[0][var_id], b_ub, minus_lb_w, ROUND_UP); reset_shortest_path_closed(); } const N& ub_w = dbm[0][w_id]; if (!is_plus_infinity(ub_w)) { // Add the constraint `v >= lb - ub_w'. - add_assign_r(dbm[var_id][0], ub_w, mlb, ROUND_UP); + add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP); reset_shortest_path_closed(); } } diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index 09c20f5..cd17822 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -67,7 +67,7 @@ test02() { Variable A(0); Variable B(1); - BD_Shape<float> bd1(3); + BD_Shape<float> bd1(2); bd1.add_constraint(A <= 2); bd1.add_constraint(A - B <= 3); bd1.add_constraint(B <= 2); @@ -77,12 +77,14 @@ test02() { bd1.affine_image(A, l); print_constraints(bd1, "*** bd1.affine_image(A, [-2, 1]) ***"); + bd1.ascii_dump(); // At the moment, affine_image is simply an identity function. - BD_Shape<float> known_result(3); - known_result.add_constraint(A <= 2); + BD_Shape<float> known_result(2); + known_result.add_constraint(A <= 1); + known_result.add_constraint(- A <= 2); known_result.add_constraint(B <= 2); - known_result.add_constraint(A - B <= 3); + print_constraints(known_result, "*** known_result ***"); bool ok = (bd1 == known_result);

1 0

[GIT] ppl/ppl(floating_point): Finished writing a first implementation of convert_to_integer_expression
by Fabio Bossi 19 Sep '09

19 Sep '09

Module: ppl/ppl Branch: floating_point Commit: ecffc8c69e21896893ea1732b3725ab0063def44 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ecffc8c69e21… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Sep 19 18:53:32 2009 +0200 Finished writing a first implementation of convert_to_integer_expression and convert_to_integer_expressions. --- src/Polyhedron.defs.hh | 4 +- src/Polyhedron.templates.hh | 98 ++++++++++++++++++++++++++++++++++++++---- 2 files changed, 90 insertions(+), 12 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 1391f53..d904386 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2587,8 +2587,8 @@ protected: template <typename FP_Format, typename Interval_Info> static void convert_to_integer_expressions( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, - const dimension_type lf_dimension, - Linear_Expression& first, Linear_Expression& second); + const dimension_type lf_dimension, Linear_Expression& res, + Coefficient& res_low_coeff, Coefficient& res_hi_coeff); }; diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index c8772df..ab61ee1 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -304,19 +304,19 @@ 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::overapproximate_linear_form:" + "Polyhedron::affine_image:" " FP_Format not a floating point type."); // Dimension compatibility checks. // The dimension of lf should not be greater than the dimension of *this. const dimension_type lf_space_dim = lf.space_dimension(); if (space_dim < lf_space_dim) - throw_dimension_incompatible("affine_image(v, l)", "l", lf); + throw_dimension_incompatible("affine_image(v, l, s)", "l", lf); // `var' should be one of the dimensions of the polyhedron. const dimension_type var_id = var.id(); if (space_dim < var_id + 1) - throw_dimension_incompatible("affine_image(v, l)", var.id()+1); + throw_dimension_incompatible("affine_image(v, l, s)", var.id()+1); PPL_ASSERT(!marked_empty()); @@ -380,28 +380,106 @@ void convert_to_integer_expression( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Expression& result) { + result = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + std::vector<Coefficient> numerators(lf_dimension+1); + std::vector<Coefficient> denominators(lf_dimension+1); + + // Convert each floating point number to a pair <numerator, denominator> + // and compute the lcm of all denominators. + PPL_DIRTY_TEMP_COEFFICIENT(lcm); + 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], + denominators[lf_dimension]); + if (numerators[lf_dimension] != 0) + lcm_assign(lcm, lcm, denominators[lf_dimension]); + for (dimension_type i = 0; i < lf_dimension; ++i) { + const FP_Interval_Type& curr_int = lf.coefficient(Variable(i)); + numer_denom(curr_int.lower(), numerators[i], denominators[i]); + if (numerators[i] != 0) + lcm_assign(lcm, lcm, denominators[i]); + } + + for (dimension_type i = 0; i < lf_dimension; ++i) { + if (numerators[i] != 0) { + exact_div_assign(denominators[i], lcm, denominators[i]); + numerators[i] *= denominators[i]; + result += numerators[i] * Variable(i); + } + } + + if (numerators[lf_dimension] != 0) { + exact_div_assign(denominators[lf_dimension], + lcm, denominators[lf_dimension]); + numerators[lf_dimension] *= denominators[lf_dimension]; + result += numerators[lf_dimension]; + } } template <typename FP_Format, typename Interval_Info> void convert_to_integer_expressions( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, - const dimension_type lf_dimension, - Linear_Expression& first, Linear_Expression& second) { + const dimension_type lf_dimension, Linear_Expression& res, + Coefficient& res_low_coeff, Coefficient& res_hi_coeff) { + res = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; - std::vector<Coefficient> coefficients(lf_dimension+2); - std::vector<Coefficient> norm_factors(lf_dimension+2); - - coefficients[lf_dimension] = lf.inhomogeneous_term().lower(); - coefficients[lf_dimension+1] = lf.inhomogeneous_term().upper(); + std::vector<Coefficient> numerators(lf_dimension+2); + std::vector<Coefficient> denominators(lf_dimension+2); + + // Convert each floating point number to a pair <numerator, denominator> + // and compute the lcm of all denominators. + PPL_DIRTY_TEMP_COEFFICIENT(lcm); + lcm = 1; + const FP_Interval_Type& b = lf.inhomogeneous_term(); + numer_denom(b.lower(), numerators[lf_dimension], denominators[lf_dimension]); + // FIXME: are these checks numerator[i] != 0 really necessary? + if (numerators[lf_dimension] != 0) + lcm_assign(lcm, lcm, denominators[lf_dimension]); + + numer_denom(b.upper(), numerators[lf_dimension+1], + denominators[lf_dimension+1]); + if (numerators[lf_dimension+1] != 0) + lcm_assign(lcm, lcm, denominators[lf_dimension+1]); + for (dimension_type i = 0; i < lf_dimension; ++i) { + const FP_Interval_Type& curr_int = lf.coefficient(Variable(i)); + numer_denom(curr_int.lower(), numerators[i], denominators[i]); + if (numerators[i] != 0) + lcm_assign(lcm, lcm, denominators[i]); + } + for (dimension_type i = 0; i < lf_dimension; ++i) { + if (numerators[i] != 0) { + exact_div_assign(denominators[i], lcm, denominators[i]); + numerators[i] *= denominators[i]; + res += numerators[i] * Variable(i); + } + } + if (numerators[lf_dimension] != 0) { + exact_div_assign(denominators[lf_dimension], + lcm, denominators[lf_dimension]); + numerators[lf_dimension] *= denominators[lf_dimension]; + res_low_coeff = numerators[lf_dimension]; + } + else + res_low_coeff = Coefficient(0); + + if (numerators[lf_dimension+1] != 0) { + exact_div_assign(denominators[lf_dimension+1], + lcm, denominators[lf_dimension+1]); + numerators[lf_dimension+1] *= denominators[lf_dimension+1]; + res_hi_coeff = numerators[lf_dimension+1]; + } + else + res_hi_coeff = Coefficient(0); } } // namespace Parma_Polyhedra_Library

1 0

[GIT] ppl/ppl(floating_point): Small progress in writing convert_to_integer_expressions.
by Fabio Bossi 19 Sep '09

19 Sep '09

Module: ppl/ppl Branch: floating_point Commit: b6dc43db2855f737fdc094422efd8c8b2f1d838f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b6dc43db2855… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Sep 19 17:25:19 2009 +0200 Small progress in writing convert_to_integer_expressions. --- src/Polyhedron.templates.hh | 7 +++++++ 1 files changed, 7 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 47ddf4f..c8772df 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -394,6 +394,13 @@ void convert_to_integer_expressions( typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + std::vector<Coefficient> coefficients(lf_dimension+2); + std::vector<Coefficient> norm_factors(lf_dimension+2); + + coefficients[lf_dimension] = lf.inhomogeneous_term().lower(); + coefficients[lf_dimension+1] = lf.inhomogeneous_term().upper(); + + }

1 0

[GIT] ppl/ppl(floating_point): Sterted writing the functions that are used to convert floating point
by Fabio Bossi 19 Sep '09

19 Sep '09

Module: ppl/ppl Branch: floating_point Commit: ca46c285903617911d8ad4b5676b90fbbb3c5f03 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ca46c2859036… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Sep 19 17:18:31 2009 +0200 Sterted writing the functions that are used to convert floating point constraints to integer ones. --- src/Polyhedron.defs.hh | 12 ++++++++++++ src/Polyhedron.templates.hh | 22 ++++++++++++++++++++++ 2 files changed, 34 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index ab4a7ce..1391f53 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2578,6 +2578,18 @@ protected: const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, Linear_Form<Interval <FP_Format, Interval_Info> >& result); + template <typename FP_Format, typename Interval_Info> + static void convert_to_integer_expression( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const dimension_type lf_dimension, + Linear_Expression& result); + + template <typename FP_Format, typename Interval_Info> + static void convert_to_integer_expressions( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const dimension_type lf_dimension, + Linear_Expression& first, Linear_Expression& second); + }; namespace std { diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 9109b83..47ddf4f 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -375,6 +375,28 @@ Polyhedron::overapproximate_linear_form( } +template <typename FP_Format, typename Interval_Info> +void convert_to_integer_expression( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const dimension_type lf_dimension, + Linear_Expression& result) { + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + +} + +template <typename FP_Format, typename Interval_Info> +void convert_to_integer_expressions( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const dimension_type lf_dimension, + Linear_Expression& first, Linear_Expression& second) { + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef typename FP_Interval_Type::coefficient_type FP_Coeff_Type; + +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Polyhedron_templates_hh)

1 0

[GIT] ppl/ppl(floating_point): Implemented methods BD_Shape<T>:: inhomogeneous_affine_image and
by Roberto Amadini 19 Sep '09

19 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f37d16f0e9478a04c09a6f646c7b9d27e852f54f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f37d16f0e947… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Sep 19 17:37:05 2009 +0200 Implemented methods BD_Shape<T>::inhomogeneous_affine_image and BD_Shape<T>::one_variable_affine_image. --- src/BD_Shape.defs.hh | 26 +++--- src/BD_Shape.templates.hh | 157 ++++++++++++++++++++++++++++++-------- src/Octagonal_Shape.templates.hh | 2 +- 3 files changed, 139 insertions(+), 46 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=f37d16f0…

1 0

[GIT] ppl/ppl(floating_point): Converted helpers to work also for native numbers.
by Abramo Bagnara 19 Sep '09

19 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 01dab9748259cee736256a446e6e7451bf0992c0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=01dab9748259… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sat Sep 19 09:51:20 2009 +0200 Converted helpers to work also for native numbers. --- src/math_utilities.defs.hh | 25 ++++++++++++------------- src/math_utilities.inlines.hh | 33 ++++++++++++++++----------------- 2 files changed, 28 insertions(+), 30 deletions(-) diff --git a/src/math_utilities.defs.hh b/src/math_utilities.defs.hh index 2b082ce..be685c5 100644 --- a/src/math_utilities.defs.hh +++ b/src/math_utilities.defs.hh @@ -32,17 +32,17 @@ namespace Parma_Polyhedra_Library { #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Extract the numerator and denominator components of \p from. #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -template <typename T, typename Policy> -void -numer_denom(const Checked_Number<T, Policy>& from, +template <typename T> +typename Enable_If<Is_Native_Or_Checked<T>::value, void>::type +numer_denom(const T& from, Coefficient& num, Coefficient& den); #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Divides \p x by \p y into \p to, rounding the result towards plus infinity. #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -template <typename T, typename Policy> -void -div_round_up(Checked_Number<T, Policy>& to, +template <typename T> +typename Enable_If<Is_Native_Or_Checked<T>::value, void>::type +div_round_up(T& to, Coefficient_traits::const_reference x, Coefficient_traits::const_reference y); @@ -63,17 +63,16 @@ max_assign(N& x, const N& y); #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns <CODE>true</CODE> if and only if \p x is an even number. #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -template <typename T, typename Policy> -bool -is_even(const Checked_Number<T, Policy>& x); +template <typename T> +typename Enable_If<Is_Native_Or_Checked<T>::value, bool>::type +is_even(const T& x); #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns <CODE>true</CODE> if and only if \f$x = -y\f$. #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -template <typename T, typename Policy> -bool -is_additive_inverse(const Checked_Number<T, Policy>& x, - const Checked_Number<T, Policy>& y); +template <typename T> +typename Enable_If<Is_Native_Or_Checked<T>::value, bool>::type +is_additive_inverse(const T& x, const T& y); #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \brief diff --git a/src/math_utilities.inlines.hh b/src/math_utilities.inlines.hh index 14b0f5f..dfa3fc6 100644 --- a/src/math_utilities.inlines.hh +++ b/src/math_utilities.inlines.hh @@ -46,9 +46,9 @@ low_bits_mask(const unsigned n) { return n == 0 ? 0 : ~(~(T(0u)) << n); } -template <typename T, typename Policy> -inline void -numer_denom(const Checked_Number<T, Policy>& from, +template <typename T> +inline typename Enable_If<Is_Native_Or_Checked<T>::value, void>::type +numer_denom(const T& from, Coefficient& num, Coefficient& den) { PPL_ASSERT(!is_not_a_number(from) && !is_minus_infinity(from) @@ -59,9 +59,9 @@ numer_denom(const Checked_Number<T, Policy>& from, den = q.get_den(); } -template <typename T, typename Policy> -inline void -div_round_up(Checked_Number<T, Policy>& to, +template <typename T> +inline typename Enable_If<Is_Native_Or_Checked<T>::value, void>::type +div_round_up(T& to, Coefficient_traits::const_reference x, Coefficient_traits::const_reference y) { PPL_DIRTY_TEMP0(mpq_class, qx); @@ -88,19 +88,18 @@ max_assign(N& x, const N& y) { x = y; } -template <typename T, typename Policy> -inline bool -is_even(const Checked_Number<T, Policy>& x) { - Checked_Number<T, Policy> half_x; - return div_2exp_assign_r(half_x, x, 1, ROUND_DIRECT | ROUND_STRICT_RELATION) == V_EQ - && is_integer(half_x); +template <typename T> +inline typename Enable_If<Is_Native_Or_Checked<T>::value, bool>::type +is_even(const T& x) { + T mod; + return umod_2exp_assign_r(mod, x, 1, ROUND_DIRECT | ROUND_STRICT_RELATION) == V_EQ + && mod == 0; } -template <typename T, typename Policy> -inline bool -is_additive_inverse(const Checked_Number<T, Policy>& x, - const Checked_Number<T, Policy>& y) { - Checked_Number<T, Policy> negated_x; +template <typename T> +inline typename Enable_If<Is_Native_Or_Checked<T>::value, bool>::type +is_additive_inverse(const T& x, const T& y) { + T negated_x; return neg_assign_r(negated_x, x, ROUND_DIRECT | ROUND_STRICT_RELATION) == V_EQ && negated_x == y; }

1 0

[GIT] ppl/ppl(master): Make sure the latest changes to NDEBUG effective.
by Roberto Bagnara 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: master Commit: 0e677160d160688227ea68c318b0872d629f6b8a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0e677160d160… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Sep 18 20:24:35 2009 +0200 Make sure the latest changes to NDEBUG effective. --- src/ppl_header.hh | 3 +++ 1 files changed, 3 insertions(+), 0 deletions(-) diff --git a/src/ppl_header.hh b/src/ppl_header.hh index 28392f0..2f5a655 100644 --- a/src/ppl_header.hh +++ b/src/ppl_header.hh @@ -104,6 +104,9 @@ site: http://www.cs.unipr.it/ppl/ . */ # undef NDEBUG # endif #endif +// Must include <cassert> again in order to make the latest changes to +// NDEBUG effective. +#include <cassert> #include "assert.hh" #ifdef PPL_NO_AUTOMATIC_INITIALIZATION

1 0

[GIT] ppl/ppl(floating_point): Added a test for trivial cases of BD_Shape:: affine_image.
by Roberto Amadini 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: ebe68870ff0f3fc251639c287eb7473d4663a5c1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ebe68870ff0f… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Sep 18 16:32:40 2009 +0200 Added a test for trivial cases of BD_Shape::affine_image. --- src/BD_Shape.templates.hh | 30 ++++++------ tests/Floating_Point_Expression/affineimage3.cc | 2 +- tests/Floating_Point_Expression/bdshape1.cc | 56 +++++++++++++++++++--- tests/Floating_Point_Expression/refinelf1.cc | 2 +- 4 files changed, 65 insertions(+), 25 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index c1bb7d7..96b7738 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4051,7 +4051,7 @@ BD_Shape<T>::affine_image(const Variable& var, // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, - "Octagonal_Shape<T>::affine_image(Variable, Linear_Form):" + "BD_Shape<T>::affine_image(Variable, Linear_Form):" " T not a floating point type."); // Dimension-compatibility checks. @@ -4093,7 +4093,7 @@ BD_Shape<T>::affine_image(const Variable& var, // Now we know the form of `lf': // - If t == 0, then lf == b, with `b' a constant; // - If t == 1, then lf == a*w + b, where `w' can be `v' or another - // variable; + // variable; // - If t == 2, the `expr' is of the general form. PPL_DIRTY_TEMP(N, b_ub); @@ -4112,7 +4112,7 @@ BD_Shape<T>::affine_image(const Variable& var, PPL_ASSERT(OK()); return; } - + // General case. // Either t == 2, so that // lf == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, @@ -4124,30 +4124,30 @@ BD_Shape<T>::affine_image(const Variable& var, template <typename T> template <typename Interval_Info> - void + void BD_Shape<T>::inhomogeneous_affine_image(const Variable& var, - const dimension_type& var_id, - const Interval<T, Interval_Info>& term, - const N& ub, - const N& lb) { + const dimension_type& var_id, + const Interval<T, Interval_Info>& term, + const N& ub, + const N& lb) { } template <typename T> template <typename Interval_Info> - void + void BD_Shape<T>::one_variable_affine_image(const Variable& var, - const dimension_type& var_id, - const Interval<T, Interval_Info>& term, + const dimension_type& var_id, + const Interval<T, Interval_Info>& term, const Interval<T, Interval_Info>& w_coeff, - const N& ub, - const N& lb) { + const N& ub, + const N& lb) { } template <typename T> template <typename Interval_Info> void BD_Shape<T> ::two_variable_affine_image(const Variable& var, - const dimension_type& var_id, + const dimension_type& var_id, const Linear_Form< Interval<T, Interval_Info> >& lf) { } @@ -5976,7 +5976,7 @@ template<typename Interval_Info> void BD_Shape<T>::throw_dimension_incompatible(const char* method, const char* name_row, - const Linear_Form< Interval<T, + const Linear_Form< Interval<T, Interval_Info> >& lf) const { std::ostringstream s; s << "PPL::BD_Shape::" << method << ":" << std::endl diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index 6633d3e..f439275 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -1,4 +1,4 @@ -/* Test Octagonal_Shape::affine_image on interval linear forms. +/* Test Octagonal_Shape::affine_image on interval linear forms Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> This file is part of the Parma Polyhedra Library (PPL). diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc index 33b6685..09c20f5 100644 --- a/tests/Floating_Point_Expression/bdshape1.cc +++ b/tests/Floating_Point_Expression/bdshape1.cc @@ -24,21 +24,60 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace { -// tests affine_image(A, [-2, 1]) +// tests space_dimensions and trivial cases bool test01() { Variable A(0); Variable B(1); + BD_Shape<double> bd1(0); + bool ok1 = false; + Linear_Form<db_r_oc> l(A); + + try { + bd1.affine_image(A, l); + } + catch(std::invalid_argument e) { + nout << "bd1_space_dim < lf_space_dim" << endl; + ok1 = true; + } + + bool ok2 = false; + BD_Shape<double> bd2(1); + + try { + bd2.affine_image(B, l); + } + catch(std::invalid_argument e) { + nout << "space_dim < var_id + 1" << endl; + bd2.affine_image(A, l); + Constraint_System cs(A < A); + bd2.add_constraints(cs); + bd2.affine_image(A, l); + ok2 = true; + } + + return ok1 && ok2; +} + - BD_Shape<float> oc1(3); - oc1.add_constraint(A <= 2); - oc1.add_constraint(A - B <= 3); - oc1.add_constraint(B <= 2); +// tests affine_image(A, [-2, 1]) +// FIXME: It's a preliminary version, not sound at the moment. +bool +test02() { + Variable A(0); + Variable B(1); + + BD_Shape<float> bd1(3); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); fl_r_oc free_term(-2); free_term.join_assign(1); Linear_Form<fl_r_oc> l(free_term); - oc1.affine_image(A, l); - print_constraints(oc1, "*** oc1.affine_image(A, [-2, 1]) ***"); + bd1.affine_image(A, l); + print_constraints(bd1, "*** bd1.affine_image(A, [-2, 1]) ***"); + + // At the moment, affine_image is simply an identity function. BD_Shape<float> known_result(3); known_result.add_constraint(A <= 2); @@ -46,7 +85,7 @@ test01() { known_result.add_constraint(A - B <= 3); print_constraints(known_result, "*** known_result ***"); - bool ok = (oc1 == known_result); + bool ok = (bd1 == known_result); return ok; } @@ -55,4 +94,5 @@ test01() { BEGIN_MAIN DO_TEST(test01); + DO_TEST(test02); END_MAIN diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 5d15285..5c9a7bc 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -1,5 +1,5 @@ /* Test Octagonal_Shape::refine_fp_interval_abstract_store and - Octagonal_Shape::refine_with_linear_form_inequality + Octagonal_Shape::refine_with_linear_form_inequality. Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> This file is part of the Parma Polyhedra Library (PPL).

1 0

[GIT] ppl/ppl(floating_point): Started the implementation of our affine_image variant.
by Fabio Bossi 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 636677b9899ea966fd91bebd7c8692666825894e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=636677b9899e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 18 14:16:25 2009 +0200 Started the implementation of our affine_image variant. --- src/Polyhedron.defs.hh | 7 ++++++- src/Polyhedron.templates.hh | 34 +++++++++++++++++++++++++++++++++- src/Polyhedron_nonpublic.cc | 9 +++++++++ 3 files changed, 48 insertions(+), 2 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 3ea0e58..ab4a7ce 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1147,7 +1147,8 @@ public: template <typename FP_Format, typename Interval_Info> void affine_image(const Variable& var, - const Linear_Form<Interval <FP_Format, Interval_Info> >& lf); + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store); /*! \brief Assigns to \p *this the @@ -2546,6 +2547,10 @@ protected: void throw_dimension_incompatible(const char* method, const char* cgs_name, const Congruence_System& cgs) const; + template <typename C> + void throw_dimension_incompatible(const char* method, + const char* lf_name, + const Linear_Form<C>& lf) const; void throw_dimension_incompatible(const char* method, const char* var_name, Variable var) const; diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 51c98c4..9109b83 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -299,7 +299,38 @@ Polyhedron::map_space_dimensions(const Partial_Function& pfunc) { template <typename FP_Format, typename Interval_Info> void Polyhedron::affine_image(const Variable& var, - const Linear_Form<Interval <FP_Format, Interval_Info> >& lf) { +const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, +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::overapproximate_linear_form:" + " FP_Format not a floating point type."); + + // Dimension compatibility checks. + // The dimension of lf should not be greater than the dimension of *this. + const dimension_type lf_space_dim = lf.space_dimension(); + if (space_dim < lf_space_dim) + throw_dimension_incompatible("affine_image(v, l)", "l", lf); + + // `var' should be one of the dimensions of the polyhedron. + const dimension_type var_id = var.id(); + if (space_dim < var_id + 1) + throw_dimension_incompatible("affine_image(v, l)", var.id()+1); + + PPL_ASSERT(!marked_empty()); + + minimize(); + unconstrain(var); + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; + + FP_Linear_Form lf_approx; + overapproximate_linear_form(lf, lf_space_dim, store, lf_approx); + + + } template <typename FP_Format, typename Interval_Info> @@ -330,6 +361,7 @@ Polyhedron::overapproximate_linear_form( FP_Format curr_lb = curr_coeff.lower(); FP_Format curr_ub = curr_coeff.upper(); if (curr_lb != 0 || curr_ub != 0) { + PPL_ASSERT(store.find(i) != store.end()); FP_Interval_Type curr_addend(curr_ub - curr_lb); curr_addend *= aux_divisor2; curr_addend *= store[i]; diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 1a55c5f..9dce752 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -25,6 +25,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Polyhedron.defs.hh" #include "Scalar_Products.defs.hh" +#include "Linear_Form.types.hh" #include "assert.hh" #include <string> #include <iostream> @@ -2231,6 +2232,14 @@ PPL::Polyhedron::throw_dimension_incompatible(const char* method, throw_dimension_incompatible(method, cgs_name, cgs.space_dimension()); } +template <typename C> +void +PPL::Polyhedron::throw_dimension_incompatible(const char* method, + const char* lf_name, + const Linear_Form<C>& lf) const { + throw_dimension_incompatible(method, lf_name, lf.space_dimension()); +} + void PPL::Polyhedron::throw_dimension_incompatible(const char* method, const char* var_name,

1 0