September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed and simplified DIRTY_TEMP for use with -fno-elide-constructors.
by Abramo Bagnara 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: master Commit: 255dd5501e74f492c8270e62f052846254dac6cb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=255dd5501e74… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu Sep 17 15:49:53 2009 +0200 Fixed and simplified DIRTY_TEMP for use with -fno-elide-constructors. --- src/Temp.defs.hh | 20 ++++++++++++++------ src/Temp.inlines.hh | 27 +++++++-------------------- 2 files changed, 21 insertions(+), 26 deletions(-) diff --git a/src/Temp.defs.hh b/src/Temp.defs.hh index 202dea3..c25a80a 100644 --- a/src/Temp.defs.hh +++ b/src/Temp.defs.hh @@ -69,8 +69,8 @@ private: template <typename T> class Temp_Reference_Holder { public: - //! Constructs an holder holding \p p. - Temp_Reference_Holder(Temp_Item<T>& p); + //! Constructs an holder holding a dirty temp. + Temp_Reference_Holder(); //! Destructor. ~Temp_Reference_Holder(); @@ -79,6 +79,12 @@ public: T& item(); private: + //! Copy constructor: private and intentionally not implemented. + Temp_Reference_Holder(const Temp_Reference_Holder&); + + //! Assignment operator: private and intentionally not implemented. + Temp_Reference_Holder& operator=(const Temp_Reference_Holder&); + //! The held item, encapsulated. Temp_Item<T>& held; }; @@ -96,6 +102,12 @@ public: T item(); private: + //! Copy constructor: private and intentionally not implemented. + Temp_Value_Holder(const Temp_Value_Holder&); + + //! Assignment operator: private and intentionally not implemented. + Temp_Value_Holder& operator=(const Temp_Value_Holder&); + //! The held item. T item_; }; @@ -111,8 +123,6 @@ struct Temp_From_Free_List { //! The type of the holder. typedef Temp_Reference_Holder<T> holder_type; - //! Obtain the holder for a new temporary. - static holder_type obtain_holder(); }; #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS @@ -126,8 +136,6 @@ struct Temp_From_Local_Variable { //! The type of the holder. typedef Temp_Value_Holder<T> holder_type; - //! Obtain the holder for a new temporary. - static holder_type obtain_holder(); }; #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS diff --git a/src/Temp.inlines.hh b/src/Temp.inlines.hh index 55cfbe2..92f7d1b 100644 --- a/src/Temp.inlines.hh +++ b/src/Temp.inlines.hh @@ -60,8 +60,8 @@ Temp_Item<T>::release(Temp_Item& p) { template <typename T> inline -Temp_Reference_Holder<T>::Temp_Reference_Holder(Temp_Item<T>& p) - : held(p) { +Temp_Reference_Holder<T>::Temp_Reference_Holder() + : held(Temp_Item<T>::obtain()) { } template <typename T> @@ -87,29 +87,16 @@ Temp_Value_Holder<T>::item() { return item_; } -template <typename T> -inline typename Temp_From_Free_List<T>::holder_type -Temp_From_Free_List<T>::obtain_holder() { - return Temp_Reference_Holder<T>(Temp_Item<T>::obtain()); -} - -template <typename T> -inline typename Temp_From_Local_Variable<T>::holder_type -Temp_From_Local_Variable<T>::obtain_holder() { - return Temp_Value_Holder<T>(); -} - } // namespace Parma_Polyhedra_Library #define PPL_DIRTY_TEMP(T, id) \ - typename Parma_Polyhedra_Library::Dirty_Temp<T>::holder_type holder ## id = \ - Parma_Polyhedra_Library::Dirty_Temp<T>::obtain_holder(); \ - typename Parma_Polyhedra_Library::Dirty_Temp<T>::type id = \ - holder ## id.item() + typename \ + Parma_Polyhedra_Library::Dirty_Temp<T>::holder_type holder ## id; \ + typename \ + Parma_Polyhedra_Library::Dirty_Temp<T>::type id = holder ## id.item() #define PPL_DIRTY_TEMP0(T, id) \ - Parma_Polyhedra_Library::Dirty_Temp<T>::holder_type holder ## id = \ - Parma_Polyhedra_Library::Dirty_Temp<T>::obtain_holder(); \ + Parma_Polyhedra_Library::Dirty_Temp<T>::holder_type holder ## id; \ Parma_Polyhedra_Library::Dirty_Temp<T>::type id = holder ## id.item() #endif // !defined(PPL_Temp_inlines_hh)

1 0

[GIT] ppl/ppl(floating_point): Removed comments.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: b42fe4766fe4c8838994ab22557c60b00cc5ffe3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b42fe4766fe4… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 15:41:32 2009 +0200 Removed comments. --- tests/Floating_Point_Expression/refinelf1.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 747154e..a0c2f29 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -222,9 +222,9 @@ test05() { } //namespace BEGIN_MAIN -/*DO_TEST(test01); + DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); - DO_TEST(test04); */ + DO_TEST(test04); DO_TEST(test05); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added another test.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1b0f1e5529a5c4e330650d7c941035f3b2592304 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1b0f1e5529a5… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 15:38:05 2009 +0200 Added another test. --- tests/Floating_Point_Expression/refinelf1.cc | 43 ++++++++++++++++++++++++- 1 files changed, 41 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 9130b69..747154e 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -181,11 +181,50 @@ test04() { } +// tests [1, 3] + A <= [4, 4] - B and [4, 4] - B <= [1, 3] + A +bool +test05() { + 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(4); + Linear_Form<fl_r_oc> l2(-B); + l2 += tmp; + Linear_Form<fl_r_oc> l1(A); + tmp.lower() = 1; + tmp.upper() = 3; + l1 += tmp; + 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 ***"); + + 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; + +} + } //namespace BEGIN_MAIN - DO_TEST(test01); +/*DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); - DO_TEST(test04); + DO_TEST(test04); */ + DO_TEST(test05); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed one nasty cut & paste error.
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d3eef431c3bdc8e4b30d4e5bf15babf7c6544d43 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d3eef431c3bd… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 15:40:26 2009 +0200 Fixed one nasty cut & paste error. --- src/Octagonal_Shape.templates.hh | 8 -------- 1 files changed, 0 insertions(+), 8 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 6a68750..ecc284f 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -671,8 +671,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right, n_left, c_plus_minus_a_minus); else @@ -687,8 +685,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right+1, n_left, c_plus_minus_a_minus); else @@ -703,8 +699,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right, n_left+1, c_plus_minus_a_minus); else @@ -719,8 +713,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_UP); if (left_w_id < right_w_id) add_octagonal_constraint(n_right+1, n_left+1, c_plus_minus_a_minus); else

1 0

[GIT] ppl/ppl(floating_point): Added a test.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 23e43a61830b3bb3c4435f125bb8cc0f969700b3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=23e43a61830b… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 14:59:59 2009 +0200 Added a test. --- tests/Floating_Point_Expression/refinelf1.cc | 41 +++++++++++++++++--------- 1 files changed, 27 insertions(+), 14 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index d639016..9130b69 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -49,6 +49,9 @@ test01() { catch(std::invalid_argument e) { nout << "space_dim < right_space_dim" << endl; Octagonal_Shape<double> oc2(1); + oc2.refine_with_linear_form_inequality(l1, l1); + oc2.refine_with_linear_form_inequality(-l1, l1); + oc2.refine_with_linear_form_inequality(l1, -l1); db_r_oc tmp; l1 -= A; l1 += tmp; @@ -138,10 +141,10 @@ test03() { return ok1 && ok2; } -/* -// tests [3.5, 6] <= [-2.5, 0] + A + +// tests [-0.5, 1] + A <= [2.5, 5] + B and [2.5, 5] + B <= [-0.5, 1] + A bool -test03() { +test04() { Variable A(0); Variable B(1); @@ -149,25 +152,34 @@ test03() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); - db_r_oc tmp(3.5); - tmp.join_assign(6); - Linear_Form<db_r_oc> l1(tmp); - Linear_Form<db_r_oc> l2(-A); - tmp.lower() = -2.5; - tmp.upper() = 0; + db_r_oc tmp(-0.5); + tmp.join_assign(1); + Linear_Form<db_r_oc> l1(A); + l1 += tmp; + Linear_Form<db_r_oc> l2(B); + tmp.lower() = 2.5; + tmp.upper() = 5; l2 += tmp; oc1.refine_with_linear_form_inequality(l1, l2); - print_constraints(oc1, "*** [3.5, 6] <= [-2.5, 0] + A ***"); + print_constraints(oc1, "*** [-0.5, 1] + A <= [2.5, 5] + B ***"); Octagonal_Shape<double> known_result(oc1); - known_result.add_constraint(A <= -3.5); + known_result.add_constraint(2*A - 2*B <= 11); print_constraints(known_result, "*** known_result ***"); - bool ok = (oc1 == known_result); + bool ok1 = (oc1 == known_result); - return ok; + oc1.refine_with_linear_form_inequality(l2, l1); + print_constraints(oc1, "*** [2.5, 5] + B <= [-0.5, 1] + 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 @@ -175,4 +187,5 @@ BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); + DO_TEST(test04); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Use references instead of pointers whenever possible.
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 6ea2e2f10098cdd737fbab5612414dd77d614311 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6ea2e2f10098… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 14:46:51 2009 +0200 Use references instead of pointers whenever possible. --- src/Octagonal_Shape.templates.hh | 64 +++++++++++++++++++------------------- 1 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 6432fe4..6a68750 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -750,42 +750,42 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( for (dimension_type first_v = 0; first_v < max_w_id; ++first_v) { for (dimension_type second_v = first_v+1; second_v <= max_w_id; ++second_v) { - const FP_Interval_Type* lfv_coefficient = - &(left.coefficient(Variable(first_v))); - const FP_Interval_Type* lsv_coefficient = - &(left.coefficient(Variable(second_v))); - const FP_Interval_Type* rfv_coefficient = - &(right.coefficient(Variable(first_v))); - const FP_Interval_Type* rsv_coefficient = - &(right.coefficient(Variable(second_v))); + const FP_Interval_Type& lfv_coefficient = + left.coefficient(Variable(first_v)); + const FP_Interval_Type& lsv_coefficient = + left.coefficient(Variable(second_v)); + const FP_Interval_Type& rfv_coefficient = + right.coefficient(Variable(first_v)); + const FP_Interval_Type& rsv_coefficient = + right.coefficient(Variable(second_v)); // We update the constraints only when both variables appear in at // least one argument. bool do_update = false; - assign_r(low_coeff, lfv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, lfv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, lfv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lfv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) { - assign_r(low_coeff, lsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, lsv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, lsv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lsv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) do_update = true; else { - assign_r(low_coeff, rsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, rsv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, rsv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rsv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) do_update = true; } } else { - assign_r(low_coeff, rfv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, rfv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, rfv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rfv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) { - assign_r(low_coeff, lsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, lsv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, lsv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lsv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) do_update = true; else { - assign_r(low_coeff, rsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, rsv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, rsv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rsv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) do_update = true; } @@ -819,20 +819,20 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( // Finally, update the unary constraints. for (dimension_type v = 0; v <= max_w_id; ++v) { - const FP_Interval_Type* lv_coefficient = - &(left.coefficient(Variable(v))); - const FP_Interval_Type* rv_coefficient = - &(right.coefficient(Variable(v))); + const FP_Interval_Type& lv_coefficient = + left.coefficient(Variable(v)); + const FP_Interval_Type& rv_coefficient = + right.coefficient(Variable(v)); // We update the constraints only if v appears in at least one of the // two arguments. bool do_update = false; - assign_r(low_coeff, lv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, lv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, lv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) do_update = true; else { - assign_r(low_coeff, rv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(high_coeff, rv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(low_coeff, rv_coefficient.lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rv_coefficient.upper(), ROUND_NOT_NEEDED); if (low_coeff != 0 || high_coeff != 0) do_update = true; } @@ -5341,7 +5341,6 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, typedef Interval<T, Interval_Info> FP_Interval_Type; - const FP_Interval_Type* curr_coefficient; PPL_DIRTY_TEMP(N, curr_lb); PPL_DIRTY_TEMP(N, curr_ub); PPL_DIRTY_TEMP(N, curr_var_ub); @@ -5356,9 +5355,10 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, for (dimension_type curr_var = 0, n_var = 0; curr_var < lf_space_dimension; ++curr_var) { - 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); + 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, matrix[n_var+1][n_var], ROUND_NOT_NEEDED); div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_UP);

1 0

[GIT] ppl/ppl(floating_point): Added and modified tests.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 33f20542b9b6d690f2bf243e9991e6b36b423195 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=33f20542b9b6… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 14:02:50 2009 +0200 Added and modified tests. --- tests/Floating_Point_Expression/refinelf1.cc | 81 +++++++++++++++++++++++++- 1 files changed, 79 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index a866e3c..d639016 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -63,7 +63,7 @@ test01() { return ok1 && ok2; } -// tests [-1, 2] <= [-4, -1] + A +// tests [-1, 2] <= [-4, -1] + A and [-4, -1] + A <= [-1, 2] bool test02() { Variable A(0); @@ -85,17 +85,94 @@ test02() { Octagonal_Shape<float> known_result(oc1); known_result.add_constraint(-A <= 0); + print_constraints(known_result, "*** known_result1 ***"); + + bool ok1 = (oc1 == known_result); + + oc1.refine_with_linear_form_inequality(l2, l1); + print_constraints(oc1, "*** [-4, -1] + A <= [-1, 2] ***"); + + known_result.add_constraint(A <= 6); + print_constraints(known_result, "*** known_result2 ***"); + + bool ok2 = (oc1 == known_result); + + return ok1 && ok2; + +} + +// tests [3.5, 6] <= [-2.5, 0] - A and [-2.5, 0] - A <= [3.5, 6] +bool +test03() { + 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(3.5); + tmp.join_assign(6); + Linear_Form<db_r_oc> l1(tmp); + Linear_Form<db_r_oc> l2(-A); + tmp.lower() = -2.5; + tmp.upper() = 0; + l2 += tmp; + 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 ***"); + + bool ok1 = (oc1 == known_result); + + oc1.refine_with_linear_form_inequality(l2, l1); + print_constraints(oc1, "*** [-2.5, 0] - A <= [3.5, 6] ***"); + + known_result.add_constraint(2*A >= -17); + print_constraints(known_result, "*** known_result2 ***"); + + bool ok2 = (oc1 == known_result); + + return ok1 && ok2; + +} +/* +// tests [3.5, 6] <= [-2.5, 0] + A +bool +test03() { + 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(3.5); + tmp.join_assign(6); + Linear_Form<db_r_oc> l1(tmp); + Linear_Form<db_r_oc> l2(-A); + tmp.lower() = -2.5; + tmp.upper() = 0; + l2 += tmp; + 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(A <= -3.5); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result); return ok; -} +} */ } //namespace BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); + DO_TEST(test03); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Optimized refine_with_linear_form_inequality , removing six temporaries
by Fabio Bossi 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 6dd29aa6e3060c03b2794fe757fe03739ca80131 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6dd29aa6e306… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 17 12:24:43 2009 +0200 Optimized refine_with_linear_form_inequality, removing six temporaries in the process. --- src/Octagonal_Shape.templates.hh | 81 +++++++++++++++++++++++++------------ 1 files changed, 55 insertions(+), 26 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 33290b8..6432fe4 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -544,6 +544,9 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( typedef typename OR_Matrix<N>::const_row_reference_type Row_reference; typedef Interval<T, Interval_Info> FP_Interval_Type; + // FIXME: there is plenty of duplicate code in the following lines. We could + // shorten it at the expense of a bit of efficiency. + if (left_t == 0) { if (right_t == 0) { // The constraint involves constants only. Ignore it: it is up to @@ -736,14 +739,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( // in `left' and `right'. // Declare temporaries outside of the loop. - PPL_DIRTY_TEMP(N, lf_lb); - PPL_DIRTY_TEMP(N, lf_ub); - PPL_DIRTY_TEMP(N, ls_lb); - PPL_DIRTY_TEMP(N, ls_ub); - PPL_DIRTY_TEMP(N, rf_lb); - PPL_DIRTY_TEMP(N, rf_ub); - PPL_DIRTY_TEMP(N, rs_lb); - PPL_DIRTY_TEMP(N, rs_ub); + PPL_DIRTY_TEMP(N, low_coeff); + PPL_DIRTY_TEMP(N, high_coeff); PPL_DIRTY_TEMP(N, upper_bound); Linear_Form<FP_Interval_Type> right_minus_left(right); @@ -761,18 +758,41 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( &(right.coefficient(Variable(first_v))); const FP_Interval_Type* rsv_coefficient = &(right.coefficient(Variable(second_v))); - assign_r(lf_lb, lfv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(lf_ub, lfv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(ls_lb, lsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(ls_ub, lsv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(rf_lb, rfv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(rf_ub, rfv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(rs_lb, rsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(rs_ub, rsv_coefficient->upper(), ROUND_NOT_NEEDED); - // true when both variables appear in at least one argument. - if ((lf_lb != 0 || lf_ub != 0 || rf_lb != 0 || rf_ub != 0) - && - (ls_lb != 0 || ls_ub != 0 || rs_lb != 0 || rs_lb != 0)) { + // We update the constraints only when both variables appear in at + // least one argument. + bool do_update = false; + assign_r(low_coeff, lfv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lfv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) { + assign_r(low_coeff, lsv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lsv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) + do_update = true; + else { + assign_r(low_coeff, rsv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rsv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) + do_update = true; + } + } + else { + assign_r(low_coeff, rfv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rfv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) { + assign_r(low_coeff, lsv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lsv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) + do_update = true; + else { + assign_r(low_coeff, rsv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rsv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) + do_update = true; + } + } + } + + if (do_update) { Variable first(first_v); Variable second(second_v); dimension_type n_first_var = first_v * 2; @@ -803,12 +823,21 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( &(left.coefficient(Variable(v))); const FP_Interval_Type* rv_coefficient = &(right.coefficient(Variable(v))); - assign_r(lf_lb, lv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(lf_ub, lv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(rf_lb, rv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(rf_ub, rv_coefficient->upper(), ROUND_NOT_NEEDED); - // true if variable v appears in one of the two arguments. - if (lf_lb != 0 || lf_ub != 0 || rf_lb != 0 || rf_ub != 0) { + // We update the constraints only if v appears in at least one of the + // two arguments. + bool do_update = false; + assign_r(low_coeff, lv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, lv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) + do_update = true; + else { + assign_r(low_coeff, rv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(high_coeff, rv_coefficient->upper(), ROUND_NOT_NEEDED); + if (low_coeff != 0 || high_coeff != 0) + do_update = true; + } + + if (do_update) { Variable var(v); dimension_type n_var = 2 * v; /*

1 0

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

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 88575c56b5ccb3b73f85c42dd2cae0227b646f2e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=88575c56b5cc… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 11:43:11 2009 +0200 Added two tests. --- tests/Floating_Point_Expression/refinelf1.cc | 101 ++++++++++++++++++++++++++ 1 files changed, 101 insertions(+), 0 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc new file mode 100644 index 0000000..a866e3c --- /dev/null +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -0,0 +1,101 @@ +/* Test Octagonal_Shape::refine_fp_interval_abstract_store and + 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). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +// tests trivial cases +bool +test01() { + Variable A(0); + Variable B(1); + Octagonal_Shape<double> oc1(0); + bool ok1 = false; + Linear_Form<db_r_oc> l1(A); + Linear_Form<db_r_oc> l2; + try { + oc1.refine_with_linear_form_inequality(l1, l2); + } + catch(std::invalid_argument e) { + nout << "space_dim < left_space_dim" << endl; + ok1 = true; + } + + bool ok2 = false; + try { + oc1.refine_with_linear_form_inequality(l2, l1); + } + catch(std::invalid_argument e) { + nout << "space_dim < right_space_dim" << endl; + Octagonal_Shape<double> oc2(1); + db_r_oc tmp; + l1 -= A; + 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; + } + + return ok1 && ok2; +} + +// tests [-1, 2] <= [-4, -1] + A +bool +test02() { + 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(-1); + tmp.join_assign(2); + Linear_Form<fl_r_oc> l1(tmp); + Linear_Form<fl_r_oc> l2(A); + tmp.lower() = -4; + tmp.upper() = -1; + l2 += tmp; + 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_result ***"); + + bool ok = (oc1 == known_result); + + return ok; + +} + +} //namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); +END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Start to test Octagonal_Shape:: refine_with_linear_form_inequality.
by Roberto Amadini 17 Sep '09

17 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1d86fe8a21720d077ed617f2906aa563599d4f9a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1d86fe8a2172… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 17 11:37:38 2009 +0200 Start to test Octagonal_Shape::refine_with_linear_form_inequality. --- src/Octagonal_Shape.templates.hh | 4 ++-- tests/Floating_Point_Expression/Makefile.am | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 3eac070..33290b8 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -630,8 +630,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( bool is_right_coeff_one = (right_w_coeff == 1); bool is_right_coeff_minus_one = (right_w_coeff == -1); if (left_w_id == right_w_id) { - if (is_left_coeff_one && is_right_coeff_one || - is_left_coeff_minus_one && is_right_coeff_minus_one) { + if ((is_left_coeff_one && is_right_coeff_one) || + (is_left_coeff_minus_one && is_right_coeff_minus_one)) { // Here we have an identity or a constants-only constraint. return; } diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index 4039297..ba5c2e7 100755 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -50,7 +50,8 @@ $(top_builddir)/src/libppl.la \ @extra_libraries@ TESTS = floatingpointexpr1 \ -affineimage3 +affineimage3 \ +refinelf1 XFAIL_TESTS = @@ -62,6 +63,7 @@ BUGS = floatingpointexpr1_SOURCES = floatingpointexpr1.cc affineimage3_SOURCES = affineimage3.cc +refinelf1_SOURCES = refinelf1.cc check_PROGRAMS = \ $(TESTS) \

1 0