September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Added Roberto Amadini to the list of current contributors.
by Roberto Bagnara 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 630590eb2beb329240e5e06f87df97ce2b582e71 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=630590eb2beb… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 17 20:55:32 2009 +0200 Added Roberto Amadini to the list of current contributors. --- CREDITS | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/CREDITS b/CREDITS index 1df21ca..79b6899 100644 --- a/CREDITS +++ b/CREDITS @@ -35,6 +35,10 @@ Current Contributors: intervals. He also helps on several other design and implementation issues. + Roberto Amadini (student of the University of Parma) + is working on the PPL support for the approximation + of floating point computations. + Fabio Biselli (student of the University of Parma) is working on the PPL support for the approximation of floating point computations.

1 0

[GIT] ppl/ppl(floating_point): Pass variables to affine_image as const references.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 61aa0fda07d541f45bd297f8a8b19f37c485b1cf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=61aa0fda07d5… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 18:16:57 2009 +0200 Pass variables to affine_image as const references. --- src/Octagonal_Shape.defs.hh | 2 +- src/Octagonal_Shape.templates.hh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 5377ca3..b5a6055 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1147,7 +1147,7 @@ public: is not a dimension of \p *this. */ template <typename Interval_Info> - void affine_image(Variable var, + void affine_image(const Variable& var, const Linear_Form< Interval<T, Interval_Info> >& lf); /*! \brief diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 3b83054..6734c48 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5054,7 +5054,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, template <typename T> template <typename Interval_Info> void -Octagonal_Shape<T>::affine_image(Variable var, +Octagonal_Shape<T>::affine_image(const Variable& var, const Linear_Form< Interval<T, Interval_Info> >& lf) { // Check that T is a floating point type.

1 0

[GIT] ppl/ppl(floating_point): Removed the check on empty octagons in function test01.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 880ed012ba9c074100892ab32f70bdf7d8671930 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=880ed012ba9c… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 17:49:28 2009 +0200 Removed the check on empty octagons in function test01. --- tests/Floating_Point_Expression/refinelf1.cc | 3 --- 1 files changed, 0 insertions(+), 3 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 5dd1b5b..4515350 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -57,9 +57,6 @@ test01() { l1 += tmp; l2 += tmp; oc2.refine_with_linear_form_inequality(l1, l2); - Constraint_System cs(A < A); - oc2.add_constraints(cs); - oc2.refine_with_linear_form_inequality(l2, l1); ok2 = true; }

1 0

[GIT] ppl/ppl(floating_point): Removed useless emptiness check.
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 42d43d4ce329beb3cc2f3bbe7fb7377484b13c6a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=42d43d4ce329… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 17:37:24 2009 +0200 Removed useless emptiness check. --- src/Octagonal_Shape.templates.hh | 4 ---- 1 files changed, 0 insertions(+), 4 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 5598b0d..3b83054 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -506,10 +506,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( throw_dimension_incompatible( "refine_with_linear_form_inequality(left, right)", "right", right); - // FIXME: maybe it would be best to create a no_check variant. - if (marked_empty()) - return; - // Number of non-zero coefficients in `left': will be set to // 0, 1, or 2, the latter value meaning any value greater than 1. dimension_type left_t = 0;

1 0

[GIT] ppl/ppl(floating_point): Assert that the octagon is not empty when refining, since the analyzer
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f165fb07116d9289a92fcc5eac0f13363df64f16 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f165fb07116d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 17:35:34 2009 +0200 Assert that the octagon is not empty when refining, since the analyzer should not try to apply filters in an unreachable state. --- src/Octagonal_Shape.templates.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 7710b61..5598b0d 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -490,7 +490,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( "Octagonal_Shape<T>::refine_with_linear_form_inequality:" " T not a floating point type."); - // FIXME: what to do when empty? + // We assume that the analyzer will not try to apply an unreachable filter. + PPL_ASSERT(!marked_empty()); // Dimension-compatibility checks. // The dimensions of `left' and `right' should not be greater than the

1 0

[GIT] ppl/ppl(floating_point): Do not reset strong closure manually since add_octagonal_constraint
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a7172dfc7c1e1d81a6ea0a46cae7b47fa590600a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7172dfc7c1e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 17:30:05 2009 +0200 Do not reset strong closure manually since add_octagonal_constraint already does it automatically. --- src/Octagonal_Shape.templates.hh | 3 --- 1 files changed, 0 insertions(+), 3 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index e33df08..7710b61 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -724,9 +724,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( // General case. - // In the following, strong closure will be definitely lost. - reset_strongly_closed(); - // FIRST, update the binary constraints for each pair of DIFFERENT variables // in `left' and `right'.

1 0

[GIT] ppl/ppl(floating_point): Always use add_octagon_constraint to update contraints in
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 8ae6135af4d6a659459fad4c01fd077de32d4562 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8ae6135af4d6… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 17:24:24 2009 +0200 Always use add_octagon_constraint to update contraints in refine_with_linear_form_inequality instead of overwriting blindly. --- src/Octagonal_Shape.templates.hh | 18 ++++++------------ 1 files changed, 6 insertions(+), 12 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index ecc284f..e33df08 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -791,20 +791,16 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( dimension_type n_second_var = second_v * 2; linear_form_upper_bound(right_minus_left - first + second, upper_bound); - assign_r(matrix[n_second_var+1][n_first_var+1], - upper_bound, ROUND_NOT_NEEDED); + add_octagonal_constraint(n_second_var+1, n_first_var+1, upper_bound); linear_form_upper_bound(right_minus_left + first + second, upper_bound); - assign_r(matrix[n_second_var+1][n_first_var], - upper_bound, ROUND_NOT_NEEDED); + add_octagonal_constraint(n_second_var+1, n_first_var, upper_bound); linear_form_upper_bound(right_minus_left - first - second, upper_bound); - assign_r(matrix[n_second_var][n_first_var+1], - upper_bound, ROUND_NOT_NEEDED); + add_octagonal_constraint(n_second_var, n_first_var+1, upper_bound); linear_form_upper_bound(right_minus_left + first - second, upper_bound); - assign_r(matrix[n_second_var][n_first_var], - upper_bound, ROUND_NOT_NEEDED); + add_octagonal_constraint(n_second_var, n_first_var, upper_bound); } } } @@ -853,14 +849,12 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( for (dimension_type i = 0; m_ite != m_end; i += 2) { Row_Reference upper = *m_ite; N& ul = upper[i]; - N& ur = upper[i+1]; - assign_r(ur, ul, ROUND_NOT_NEEDED); + add_octagonal_constraint(i, i+1, ul); assign_r(ul, PLUS_INFINITY, ROUND_NOT_NEEDED); ++m_ite; Row_Reference lower = *m_ite; - N& ll = lower[i]; N& lr = lower[i+1]; - assign_r(ll, lr, ROUND_NOT_NEEDED); + add_octagonal_constraint(i+1, i, lr); assign_r(lr, PLUS_INFINITY, ROUND_NOT_NEEDED); ++m_ite; }

1 0

[GIT] ppl/ppl(floating_point): Removed a bug in test functions. Added a test for general case.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: df74c77ffb0f50cb20eecd9c9e453923225f9a76 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=df74c77ffb0f… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 16:54:03 2009 +0200 Removed a bug in test functions. Added a test for general case. --- tests/Floating_Point_Expression/refinelf1.cc | 42 ++++++++++++++++++++++---- 1 files changed, 36 insertions(+), 6 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 5ed3111..5dd1b5b 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -76,6 +76,7 @@ test02() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); + Octagonal_Shape<float> known_result(oc1); fl_r_oc tmp(-1); tmp.join_assign(2); Linear_Form<fl_r_oc> l1(tmp); @@ -86,7 +87,6 @@ test02() { oc1.refine_with_linear_form_inequality(l1, l2); print_constraints(oc1, "*** [-1, 2] <= [-4, -1] + A ***"); - Octagonal_Shape<float> known_result(oc1); known_result.add_constraint(-A <= 0); print_constraints(known_result, "*** known_result1 ***"); @@ -114,6 +114,7 @@ test03() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); + Octagonal_Shape<double> known_result(oc1); db_r_oc tmp(3.5); tmp.join_assign(6); Linear_Form<db_r_oc> l1(tmp); @@ -124,7 +125,6 @@ test03() { oc1.refine_with_linear_form_inequality(l1, l2); print_constraints(oc1, "*** [3.5, 6] <= [-2.5, 0] - A ***"); - Octagonal_Shape<double> known_result(oc1); known_result.add_constraint(2*A <= -7); print_constraints(known_result, "*** known_result ***"); @@ -152,6 +152,7 @@ test04() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); + Octagonal_Shape<double> known_result(oc1); db_r_oc tmp(-0.5); tmp.join_assign(1); Linear_Form<db_r_oc> l1(A); @@ -163,7 +164,6 @@ test04() { oc1.refine_with_linear_form_inequality(l1, l2); print_constraints(oc1, "*** [-0.5, 1] + A <= [2.5, 5] + B ***"); - Octagonal_Shape<double> known_result(oc1); known_result.add_constraint(2*A - 2*B <= 11); print_constraints(known_result, "*** known_result ***"); @@ -191,6 +191,7 @@ test05() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); + Octagonal_Shape<float> known_result(oc1); fl_r_oc tmp(4); Linear_Form<fl_r_oc> l2(-B); l2 += tmp; @@ -201,7 +202,6 @@ test05() { oc1.refine_with_linear_form_inequality(l1, l2); print_constraints(oc1, "*** [1, 3] + A <= [4, 4] - B ***"); - Octagonal_Shape<float> known_result(oc1); known_result.add_constraint(A + B <= 3); print_constraints(known_result, "*** known_result ***"); @@ -229,6 +229,7 @@ test06() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); + Octagonal_Shape<double> known_result(oc1); db_r_oc tmp(-2); Linear_Form<db_r_oc> l2(B); l2 += tmp; @@ -239,7 +240,6 @@ test06() { oc1.refine_with_linear_form_inequality(l1, l2); print_constraints(oc1, "*** [1, 4] - A <= [-2, -2] + B ***"); - Octagonal_Shape<double> known_result(oc1); known_result.add_constraint(-B - A <= -3); print_constraints(known_result, "*** known_result ***"); @@ -267,6 +267,7 @@ test07() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); + Octagonal_Shape<float> known_result(oc1); fl_r_oc tmp(-2); tmp.join_assign(-1); Linear_Form<fl_r_oc> l2(-B); @@ -278,7 +279,6 @@ test07() { oc1.refine_with_linear_form_inequality(l1, l2); print_constraints(oc1, "*** [-3, -0.5] - A <= [-2, -1] - B ***"); - Octagonal_Shape<float> known_result(oc1); known_result.add_constraint(B - A <= 2); print_constraints(known_result, "*** known_result ***"); @@ -296,6 +296,35 @@ test07() { } +// tests [1, 3] * B <= [-1.5, 0] * A +bool +test08() { + Variable A(0); + Variable B(1); + + Octagonal_Shape<double> oc1(3); + oc1.add_constraint(A <= 2); + oc1.add_constraint(A - B <= 3); + oc1.add_constraint(B <= 2); + Octagonal_Shape<double> known_result(oc1); + db_r_oc tmp(1); + tmp.join_assign(3); + Linear_Form<db_r_oc> l1(B); + l1 *= tmp; + Linear_Form<db_r_oc> l2(A); + tmp.lower() = -1.5; + tmp.upper() = 0; + l2 *= tmp; + oc1.refine_with_linear_form_inequality(l1, l2); + print_constraints(oc1, "*** [1, 3] * B <= [-1.5, 0] * A ***"); + + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; +} + } //namespace BEGIN_MAIN @@ -306,4 +335,5 @@ BEGIN_MAIN DO_TEST(test05); DO_TEST(test06); DO_TEST(test07); + DO_TEST(test08); END_MAIN

1 0

[GIT] ppl/ppl(master): Fixed several rounding modes in Octagonal_Shape methods.
by Enea Zaffanella 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: master Commit: ba44339f4373e21010bc42e609c16cbba87bdceb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ba44339f4373… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Sep 17 16:12:17 2009 +0200 Fixed several rounding modes in Octagonal_Shape methods. --- src/Octagonal_Shape.templates.hh | 38 +++++++++++++++++++------------------- 1 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index a9590a7..65561f7 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -2008,10 +2008,10 @@ Octagonal_Shape<T>::tight_closure_assign() { const dimension_type ci = i+1; N& mat_i_ci = matrix[i][ci]; if (!is_plus_infinity(mat_i_ci) && !is_even(mat_i_ci)) - sub_assign_r(mat_i_ci, mat_i_ci, temp_one, ROUND_NOT_NEEDED); + sub_assign_r(mat_i_ci, mat_i_ci, temp_one, ROUND_UP); N& mat_ci_i = matrix[ci][i]; if (!is_plus_infinity(mat_ci_i) && !is_even(mat_ci_i)) - sub_assign_r(mat_ci_i, mat_ci_i, temp_one, ROUND_NOT_NEEDED); + sub_assign_r(mat_ci_i, mat_ci_i, temp_one, ROUND_UP); } // Propagate tightened unary constraints. strong_coherence_assign(); @@ -4006,7 +4006,7 @@ Octagonal_Shape<T>::refine(const Variable var, if (pinf_count == 0) { // Add the constraint `v <= sum'. PPL_DIRTY_TEMP(N, double_sum); - mul_2exp_assign_r(double_sum, sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_sum, sum, 1, ROUND_UP); matrix[n_var+1][n_var] = double_sum; // Deduce constraints of the form `v +/- u', where `u != v'. deduce_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, sum); @@ -4051,7 +4051,7 @@ Octagonal_Shape<T>::refine(const Variable var, if (neg_pinf_count == 0) { // Add the constraint `v >= -neg_sum', i.e., `-v <= neg_sum'. PPL_DIRTY_TEMP(N, double_neg_sum); - mul_2exp_assign_r(double_neg_sum, neg_sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_neg_sum, neg_sum, 1, ROUND_UP); matrix[n_var][n_var+1] = double_neg_sum; // Deduce constraints of the form `-v +/- u', where `u != v'. deduce_minus_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, neg_sum); @@ -4140,7 +4140,7 @@ Octagonal_Shape<T>::refine(const Variable var, if (pinf_count == 0) { // Add the constraint `v <= sum'. PPL_DIRTY_TEMP(N, double_sum); - mul_2exp_assign_r(double_sum, sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_sum, sum, 1, ROUND_UP); add_octagonal_constraint(n_var+1, n_var, double_sum); // Deduce constraints of the form `v +/- u', where `u != v'. deduce_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, sum); @@ -4225,7 +4225,7 @@ Octagonal_Shape<T>::refine(const Variable var, if (pinf_count == 0) { // Add the constraint `v >= -neg_sum', i.e., `-v <= neg_sum'. PPL_DIRTY_TEMP(N, double_sum); - mul_2exp_assign_r(double_sum, sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_sum, sum, 1, ROUND_UP); add_octagonal_constraint(n_var, n_var+1, double_sum); // Deduce constraints of the form `-v +/- u', where `u != v'. deduce_minus_v_pm_u_bounds(var_id, pinf_index, sc_expr, sc_den, sum); @@ -4376,10 +4376,10 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); } // Now update unary constraints on var. - mul_2exp_assign_r(d, d, 1, ROUND_IGNORE); + mul_2exp_assign_r(d, d, 1, ROUND_UP); N& m_cv_v = m_cv[n_var]; add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_IGNORE); + mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); N& m_v_cv = m_v[n_var+1]; add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); } @@ -4403,11 +4403,11 @@ Octagonal_Shape<T>::affine_image(const Variable var, // adding or subtracting the value `b/denominator'. PPL_DIRTY_TEMP(N, d); div_round_up(d, b, denominator); - mul_2exp_assign_r(d, d, 1, ROUND_IGNORE); + mul_2exp_assign_r(d, d, 1, ROUND_UP); add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); PPL_DIRTY_TEMP(N, minus_d); div_round_up(minus_d, b, minus_den); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_IGNORE); + mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); } incremental_strong_closure_assign(var); @@ -4594,7 +4594,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, if (pos_pinf_count == 0) { // Add the constraint `v <= pos_sum'. PPL_DIRTY_TEMP(N, double_pos_sum); - mul_2exp_assign_r(double_pos_sum, pos_sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_pos_sum, pos_sum, 1, ROUND_UP); matrix[n_var+1][n_var] = double_pos_sum; // Deduce constraints of the form `v +/- u', where `u != v'. deduce_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, pos_sum); @@ -4637,7 +4637,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, if (neg_pinf_count == 0) { // Add the constraint `v >= -neg_sum', i.e., `-v <= neg_sum'. PPL_DIRTY_TEMP(N, double_neg_sum); - mul_2exp_assign_r(double_neg_sum, neg_sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_neg_sum, neg_sum, 1, ROUND_UP); matrix[n_var][n_var+1] = double_neg_sum; // Deduce constraints of the form `-v +/- u', where `u != v'. deduce_minus_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, neg_sum); @@ -4919,7 +4919,7 @@ Octagonal_Shape<T> assign_r(m_v[k], PLUS_INFINITY, ROUND_NOT_NEEDED); add_assign_r(m_cv[k], m_cv[k], d, ROUND_UP); } - mul_2exp_assign_r(d, d, 1, ROUND_IGNORE); + mul_2exp_assign_r(d, d, 1, ROUND_UP); add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); assign_r(m_v_cv, PLUS_INFINITY, ROUND_NOT_NEEDED); } @@ -4927,7 +4927,7 @@ Octagonal_Shape<T> // Here `w_coeff == -denominator'. // `expr' is of the form: -a*var + b. N& m_v_cv = matrix[n_var][n_var+1]; - mul_2exp_assign_r(d, d, 1, ROUND_IGNORE); + mul_2exp_assign_r(d, d, 1, ROUND_UP); add_assign_r(matrix[n_var+1][n_var], m_v_cv, d, ROUND_UP); assign_r(m_v_cv, PLUS_INFINITY, ROUND_NOT_NEEDED); forget_binary_octagonal_constraints(var_id); @@ -4986,7 +4986,7 @@ Octagonal_Shape<T> add_assign_r(m_v[k], m_v[k], d, ROUND_UP); assign_r(m_cv[k], PLUS_INFINITY, ROUND_NOT_NEEDED); } - mul_2exp_assign_r(d, d, 1, ROUND_IGNORE); + mul_2exp_assign_r(d, d, 1, ROUND_UP); add_assign_r(m_v_cv, m_v_cv, d, ROUND_UP); assign_r(m_cv_v, PLUS_INFINITY, ROUND_NOT_NEEDED); } @@ -4994,7 +4994,7 @@ Octagonal_Shape<T> // Here `w_coeff == -denominator'. // `expr' is of the form: -a*var + b. N& m_cv_v = matrix[n_var+1][n_var]; - mul_2exp_assign_r(d, d, 1, ROUND_IGNORE); + mul_2exp_assign_r(d, d, 1, ROUND_UP); add_assign_r(matrix[n_var][n_var+1], m_cv_v, d, ROUND_UP); assign_r(m_cv_v, PLUS_INFINITY, ROUND_NOT_NEEDED); forget_binary_octagonal_constraints(var_id); @@ -5134,7 +5134,7 @@ Octagonal_Shape<T> if (pinf_count == 0) { // Add the constraint `v <= pos_sum'. PPL_DIRTY_TEMP(N, double_sum); - mul_2exp_assign_r(double_sum, sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_sum, sum, 1, ROUND_UP); matrix[n_var+1][n_var] = double_sum; // Deduce constraints of the form `v +/- u', where `u != v'. deduce_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, sum); @@ -5229,7 +5229,7 @@ Octagonal_Shape<T> if (pinf_count == 0) { // Add the constraint `v >= -neg_sum', i.e., `-v <= neg_sum'. PPL_DIRTY_TEMP(N, double_sum); - mul_2exp_assign_r(double_sum, sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_sum, sum, 1, ROUND_UP); matrix[n_var][n_var+1] = double_sum; // Deduce constraints of the form `-v +/- u', where `u != v'. deduce_minus_v_pm_u_bounds(var_id, pinf_index, sc_expr, sc_den, sum); @@ -5712,7 +5712,7 @@ Octagonal_Shape<T>::bounded_affine_image(const Variable var, if (neg_pinf_count == 0) { // Add the constraint `v >= -neg_sum', i.e., `-v <= neg_sum'. PPL_DIRTY_TEMP(N, double_neg_sum); - mul_2exp_assign_r(double_neg_sum, neg_sum, 1, ROUND_IGNORE); + mul_2exp_assign_r(double_neg_sum, neg_sum, 1, ROUND_UP); matrix[n_var][n_var+1] = double_neg_sum; // Deduce constraints of the form `-v +/- u', where `u != v'. deduce_minus_v_pm_u_bounds(var_id, w_id, sc_expr, sc_den, neg_sum);

1 0

[GIT] ppl/ppl(floating_point): Added two tests. Particular cases totally covered.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: da7ab569f2f20006a259ce370cb18d180367a046 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=da7ab569f2f2… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 16:02:17 2009 +0200 Added two tests. Particular cases totally covered. --- tests/Floating_Point_Expression/refinelf1.cc | 79 ++++++++++++++++++++++++++ 1 files changed, 79 insertions(+), 0 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index a0c2f29..5ed3111 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -219,6 +219,83 @@ test05() { } +// tests [1, 4] - A <= [-2, -2] + B and [-2, -2] + B <= [1, 4] - A +bool +test06() { + Variable A(0); + Variable B(1); + + Octagonal_Shape<double> oc1(3); + oc1.add_constraint(A <= 2); + oc1.add_constraint(A - B <= 3); + oc1.add_constraint(B <= 2); + db_r_oc tmp(-2); + Linear_Form<db_r_oc> l2(B); + l2 += tmp; + Linear_Form<db_r_oc> l1(-A); + tmp.lower() = 1; + tmp.upper() = 4; + l1 += tmp; + oc1.refine_with_linear_form_inequality(l1, l2); + print_constraints(oc1, "*** [1, 4] - A <= [-2, -2] + B ***"); + + Octagonal_Shape<double> known_result(oc1); + known_result.add_constraint(-B - A <= -3); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (oc1 == known_result); + + oc1.refine_with_linear_form_inequality(l2, l1); + print_constraints(oc1, "*** [4, 4] - B <= [1, 3] + A ***"); + + known_result.add_constraint(-B - A <= -1); + print_constraints(known_result, "*** known_result2 ***"); + + bool ok2 = (oc1 == known_result); + + return ok1 && ok2; + +} + +// tests [-3, -0.5] - A <= [-2, -1] - B and [-2, -1] - B <= [-3, -0.5] - A +bool +test07() { + Variable A(0); + Variable B(1); + + Octagonal_Shape<float> oc1(3); + oc1.add_constraint(A <= 2); + oc1.add_constraint(A - B <= 3); + oc1.add_constraint(B <= 2); + fl_r_oc tmp(-2); + tmp.join_assign(-1); + Linear_Form<fl_r_oc> l2(-B); + l2 += tmp; + Linear_Form<fl_r_oc> l1(-A); + tmp.lower() = -3; + tmp.upper() = -0.5; + l1 += tmp; + oc1.refine_with_linear_form_inequality(l1, l2); + print_constraints(oc1, "*** [-3, -0.5] - A <= [-2, -1] - B ***"); + + Octagonal_Shape<float> known_result(oc1); + known_result.add_constraint(B - A <= 2); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (oc1 == known_result); + + oc1.refine_with_linear_form_inequality(l2, l1); + print_constraints(oc1, "*** [-2, -1] - B <= [-3, -0.5] - A ***"); + + known_result.add_constraint(-2*B + 2*A <= 3); + print_constraints(known_result, "*** known_result2 ***"); + + bool ok2 = (oc1 == known_result); + + return ok1 && ok2; + +} + } //namespace BEGIN_MAIN @@ -227,4 +304,6 @@ BEGIN_MAIN DO_TEST(test03); DO_TEST(test04); DO_TEST(test05); + DO_TEST(test06); + DO_TEST(test07); END_MAIN

1 0