September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Removed garbage
by Fabio Biselli 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 46f18dbe19ab34fc351017acf1a5a8f83503862f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=46f18dbe19ab… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Mon Sep 14 11:58:10 2009 +0200 Removed garbage --- src/Octagonal_Shape.defs.hh | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 536d9bc..5ac7536 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -420,6 +420,7 @@ private: #endif public: + //! The numeric base type upon which OSs are built. typedef T coefficient_type_base;

1 0

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

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: bd64da813c519c335d4aa434c3d275e766fda20d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bd64da813c51… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 16 11:25:27 2009 +0200 Added some tests. --- tests/Floating_Point_Expression/affineimage3.cc | 209 +++++++++++++++++++++-- 1 files changed, 196 insertions(+), 13 deletions(-) diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index d1ab707..a2bdc0f 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -24,17 +24,51 @@ 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); + Octagonal_Shape<double> oc1(0); + bool ok1 = false; + Linear_Form<db_r_oc> l(A); + + try { + oc1.affine_image(A, l); + } + catch(std::invalid_argument e) { + nout << "oc1_space_dim < lf_space_dim" << endl; + ok1 = true; + } + + bool ok2 = false; + Octagonal_Shape<double> oc2(1); + + try { + oc2.affine_image(B, l); + } + catch(std::invalid_argument e) { + nout << "space_dim < var_id + 1" << endl; + oc2.affine_image(A, l); + Constraint_System cs(A < A); + oc2.add_constraints(cs); + oc2.affine_image(A, l); + ok2 = true; + } + + return ok1 && ok2; +} + +// tests affine_image(A, [-2, 1]) +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); - print_constraints(oc1, "*** oc1 ***"); fl_r_oc free_term(-2); free_term.join_assign(1); Linear_Form<fl_r_oc> l(free_term); @@ -53,8 +87,36 @@ test01() { } -// tests affine_image(A, [-1, -1]*A) -bool test02() { +// tests affine_image(A, [-1, -1]*A + [0.5, 2]) +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 free_term(0.5); + free_term.join_assign(2); + Linear_Form<db_r_oc> l(-A); + l += free_term; + oc1.affine_image(A, l); + print_constraints(oc1, "*** oc1.affine_image(A, -A + [0.5, 2]) ***"); + + Octagonal_Shape<double> known_result(3); + known_result.add_constraint(-2 * A <= 3); + known_result.add_constraint(B <= 2); + known_result.add_constraint(2*B - 2*A <= 7); + print_constraints(known_result, "*** known_result ***"); + bool ok = (oc1 == known_result); + + return ok; + +} + + +// tests affine_image(B, [1, 1]*B + [-1, 3]) +bool test04() { Variable A(0); Variable B(1); @@ -62,12 +124,102 @@ bool test02() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); - Linear_Form<fl_r_oc> l(-A); + fl_r_oc free_term(-1); + free_term.join_assign(3); + Linear_Form<fl_r_oc> l(B); + l += free_term; + oc1.affine_image(B, l); + print_constraints(oc1, "*** oc1.affine_image(B, B + [-1, 3]) ***"); + oc1.ascii_dump(); + Octagonal_Shape<float> known_result(3); + /* known_result.add_constraint(A >= -2); + known_result.add_constraint(B <= 2); + known_result.add_constraint(B - A <= 4); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; + */ + return true; +} + +// tests affine_image(A, [1, 1]*B + [-2, 0.5]) +bool test05() { + 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 free_term(-2); + free_term.join_assign(0.5); + Linear_Form<db_r_oc> l(B); + l += free_term; oc1.affine_image(A, l); - print_constraints(oc1, "*** oc1.affine_image(A, [-1, -1]*A) ***"); + print_constraints(oc1, "*** oc1.affine_image(A, B + [-2, 0.5]) ***"); + oc1.ascii_dump(); + Octagonal_Shape<double> known_result(3); + /* known_result.add_constraint(A >= -2); + known_result.add_constraint(B <= 2); + known_result.add_constraint(B - A <= 4); + print_constraints(known_result, "*** known_result ***"); + bool ok = (oc1 == known_result); + + return ok; + */ + return true; +} + +// tests affine_image(B, [1, 1]*A + [-3, 1]) +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 free_term(-3); + free_term.join_assign(1); + Linear_Form<db_r_oc> l(A); + l += free_term; + oc1.affine_image(B, l); + print_constraints(oc1, "*** oc1.affine_image(B, A + [-3, 1]) ***"); + oc1.ascii_dump(); + Octagonal_Shape<double> known_result(3); + /* known_result.add_constraint(A >= -2); + known_result.add_constraint(B <= 2); + known_result.add_constraint(B - A <= 4); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; + */ + return true; +} + +// tests affine_image(B, [-1, -1]*A + [0, 4]) +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 free_term(0); + free_term.join_assign(4); + Linear_Form<fl_r_oc> l(-A); + l += free_term; + oc1.affine_image(B, l); + print_constraints(oc1, "*** oc1.affine_image(B, -A + [0, 4]) ***"); + oc1.ascii_dump(); Octagonal_Shape<float> known_result(3); - known_result.add_constraint(A >= -2); + /* known_result.add_constraint(A >= -2); known_result.add_constraint(B <= 2); known_result.add_constraint(B - A <= 4); print_constraints(known_result, "*** known_result ***"); @@ -75,23 +227,54 @@ bool test02() { bool ok = (oc1 == known_result); return ok; + */ + return true; } -/* -// tests affine_image(A, [-1, 1]*B) -bool test03() { +// tests affine_image(A, [-1, -1]*B + [0, 2]) +bool test08() { + 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 free_term(0); + free_term.join_assign(2); + Linear_Form<fl_r_oc> l(-B); + l += free_term; + oc1.affine_image(A, l); + print_constraints(oc1, "*** oc1.affine_image(A, -B + [0, 2]) ***"); + oc1.ascii_dump(); + Octagonal_Shape<float> known_result(3); + /* known_result.add_constraint(A >= -2); + known_result.add_constraint(B <= 2); + known_result.add_constraint(B - A <= 4); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; + */ return true; } -// tests affine_image(A, i + i1*A + i2*B) -bool test04() { +// tests affine_image(A, i + i1 * A + i2 * B) +bool test09() { return true; } -*/ } //namespace BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); + DO_TEST(test03); /* FIXME: Not yet tested! + DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); + DO_TEST(test07); + DO_TEST(test08); + DO_TEST(test09); */ END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added a first, untested implementation of
by Fabio Bossi 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 27853708a791db900a1c40ff490f5a5c630f9559 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=27853708a791… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 15 18:06:23 2009 +0200 Added a first, untested implementation of refine_fp_interval_abstract_store. --- src/Octagonal_Shape.defs.hh | 5 ++++ src/Octagonal_Shape.templates.hh | 43 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 1ed356b..536d9bc 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -47,6 +47,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.types.hh" #include "Linear_Form.types.hh" #include <vector> +#include <map> #include <cstddef> #include <climits> #include <iosfwd> @@ -1696,6 +1697,10 @@ public: */ void fold_space_dimensions(const Variables_Set& vars, Variable dest); + template <typename Interval_Info> + void refine_fp_interval_abstract_store( + std::map< dimension_type, Interval<T, Interval_Info> >& store); + //@} // Member Functions that May Modify the Dimension of the Vector Space PPL_OUTPUT_DECLARATIONS diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 46cf817..9251559 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5231,6 +5231,49 @@ interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, } template <typename T> +template <typename Interval_Info> +void +Octagonal_Shape<T>:: +refine_fp_interval_abstract_store( + std::map< dimension_type, Interval<T, Interval_Info> >& store) { + + // Check that T is a floating point type. + PPL_ASSERT(!std::numeric_limits<T>::is_exact); + + strong_closure_assign(); + + typedef Interval<T, Interval_Info> FP_Interval_Type; + typedef typename std::map<dimension_type, FP_Interval_Type>::iterator + Map_Iterator; + + PPL_DIRTY_TEMP(N, upper_bound); + Map_Iterator store_end = store.end(); + for (Map_Iterator ite = store.begin(); ite != store_end; ++ite) { + dimension_type curr_var = ite->first; + PPL_ASSERT(curr_var < space_dim); + dimension_type n_curr_var = curr_var * 2; + FP_Interval_Type& curr_int = &(ite->second); + T& lb = curr_int.lower(); + T& ub = curr_int.upper(); + // FIXME: are we sure that ROUND_IGNORE is good? + // Now get the upper bound for curr_var in the octagon. + assign_r(upper_bound, matrix[n_curr_var+1][n_curr_var], ROUND_NOT_NEEDED); + div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_IGNORE); + + if (upper_bound < ub) + ub = upper_bound; + + // Now get the lower bound for curr_var in the octagon. + neg_assign_r(upper_bound, matrix[n_curr_var][n_curr_var+1], + ROUND_NOT_NEEDED); + div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_IGNORE); + + if (upper_bound > lb) + lb = upper_bound; + } +} + +template <typename T> void Octagonal_Shape<T>::affine_preimage(const Variable var, const Linear_Expression& expr,

1 0

[GIT] ppl/ppl(floating_point): For consistency, use std::numeric_limits<T>: :is_exact in order to check
by Fabio Bossi 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a58815158ed248c49e2955593c07d71fd0274b1c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a58815158ed2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 15 17:00:40 2009 +0200 For consistency, use std::numeric_limits<T>::is_exact in order to check if T is a floating point type. --- src/Octagonal_Shape.templates.hh | 28 ++++++++-------------------- 1 files changed, 8 insertions(+), 20 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index ce65f96..46cf817 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -483,12 +483,9 @@ void Octagonal_Shape<T>::refine_with_linear_form_inequality( const Linear_Form< Interval<T, Interval_Info> >& left, const Linear_Form< Interval<T, Interval_Info> >& right) { - /* - FIXME: this way for checking that T is a floating point type is a bit - unelengant. - */ + // Check that T is a floating point type. - PPL_ASSERT(std::numeric_limits<T>::max_exponent); + PPL_ASSERT(!std::numeric_limits<T>::is_exact); // FIXME: what to do when empty? @@ -4870,12 +4867,9 @@ template <typename Interval_Info> void Octagonal_Shape<T>::affine_image(Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf) { - /* - FIXME: this way for checking that T is a floating point type is a bit - unelengant. - */ + // Check that T is a floating point type. - PPL_ASSERT(std::numeric_limits<T>::max_exponent); + PPL_ASSERT(!std::numeric_limits<T>::is_exact); // Dimension-compatibility checks. // The dimension of `lf' should not be greater than the dimension @@ -5128,12 +5122,9 @@ void Octagonal_Shape<T>:: linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, N& result) const { - /* - FIXME: this way for checking that T is a floating point type is a bit - unelengant. - */ + // Check that T is a floating point type. - PPL_ASSERT(std::numeric_limits<T>::max_exponent); + PPL_ASSERT(!std::numeric_limits<T>::is_exact); const dimension_type lf_space_dimension = lf.space_dimension(); PPL_ASSERT(lf_space_dimension <= space_dim); @@ -5214,12 +5205,9 @@ Octagonal_Shape<T>:: interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, const N& int_ub, const N& int_lb, N& result) { - /* - FIXME: this way for checking that T is a floating point type is a bit - unelengant. - */ + // Check that T is a floating point type. - PPL_ASSERT(std::numeric_limits<T>::max_exponent); + PPL_ASSERT(!std::numeric_limits<T>::is_exact); // NOTE: we store the first comparison term directly into result. PPL_DIRTY_TEMP(N, second_comparison_term);

1 0

[GIT] ppl/ppl(floating_point): Added a first implementation of refine_with_linear_form_inequality.
by Fabio Bossi 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: cf40c1ee096f612eab5f8353298f39e84e3f5880 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cf40c1ee096f… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 15 16:16:15 2009 +0200 Added a first implementation of refine_with_linear_form_inequality. Two small optimizations for affine_image. --- src/Octagonal_Shape.templates.hh | 138 ++++++++++++++++++++++++++++++-------- 1 files changed, 110 insertions(+), 28 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 761a468..ce65f96 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -490,6 +490,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( // Check that T is a floating point type. PPL_ASSERT(std::numeric_limits<T>::max_exponent); + // FIXME: what to do when empty? + // Dimension-compatibility checks. // The dimensions of `left' and `right' should not be greater than the // dimension of `*this'. @@ -503,6 +505,10 @@ 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; + /* FIXME: these are not really necessary right now. They will come in handy when we optimize the most common cases. @@ -546,6 +552,9 @@ 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'. @@ -558,19 +567,22 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( PPL_DIRTY_TEMP(N, rf_ub); PPL_DIRTY_TEMP(N, rs_lb); PPL_DIRTY_TEMP(N, rs_ub); + PPL_DIRTY_TEMP(N, upper_bound); - // FIXME: to complete. + Linear_Form<FP_Interval_Type> right_minus_left(right); + right_minus_left -= left; dimension_type max_w_id = std::max(left_w_id, right_w_id); - for (dimension_type first_v = 0; first_v <= max_w_id; ++first_v) { - for (dimension_type second_v = first_v; second_v <= max_w_id; ++second_v) { - FP_Interval_Type* lfv_coefficient = + 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))); - FP_Interval_Type* lsv_coefficient = + const FP_Interval_Type* lsv_coefficient = &(left.coefficient(Variable(second_v))); - FP_Interval_Type* rfv_coefficient = + const FP_Interval_Type* rfv_coefficient = &(right.coefficient(Variable(first_v))); - FP_Interval_Type* rsv_coefficient = + 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); @@ -580,10 +592,82 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( 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)) { + Variable first(first_v); + Variable second(second_v); + dimension_type n_first_var = first_v * 2; + 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); + 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); + 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); + 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); + } } } // 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))); + 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) { + Variable var(v); + dimension_type n_var = 2 * v; + /* + VERY DIRTY trick: since we need to keep the old unary constraints + while computing the new ones, we momentarily keep the new coefficients + in the main diagonal of the matrix. They will be moved later. + */ + linear_form_upper_bound(right_minus_left + var, upper_bound); + assign_r(matrix[n_var+1][n_var+1], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(right_minus_left - var, upper_bound); + assign_r(matrix[n_var][n_var], upper_bound, ROUND_NOT_NEEDED); + } + } + + /* + Now move the newly computed coefficients from the main diagonal to + their proper place, and restore +infinity on the diagonal. + */ + Row_Iterator m_ite = matrix.row_begin(); + Row_Iterator m_end = matrix.row_end(); + 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); + 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); + assign_r(lr, PLUS_INFINITY, ROUND_NOT_NEEDED); + ++m_ite; + } + + PPL_ASSERT(OK()); } @@ -4980,13 +5064,11 @@ Octagonal_Shape<T>::affine_image(Variable var, // In the following, strong closure will be definitely lost. reset_strongly_closed(); - Linear_Form<FP_Interval_Type> minus_lf(-lf); + Linear_Form<FP_Interval_Type> minus_lf(lf); + minus_lf.negate(); // Declare temporaries outside the loop. - PPL_DIRTY_TEMP(N, lf_plus_var_ub); - PPL_DIRTY_TEMP(N, lf_minus_var_ub); - PPL_DIRTY_TEMP(N, var_minus_lf_ub); - PPL_DIRTY_TEMP(N, minus_lf_minus_var_ub); + PPL_DIRTY_TEMP(N, upper_bound); Row_Iterator m_iter = matrix.row_begin(); m_iter += n_var; @@ -5000,14 +5082,14 @@ Octagonal_Shape<T>::affine_image(Variable var, for (dimension_type curr_var = var_id, n_curr_var = n_var - 2; curr_var-- > 0; ) { Variable current(curr_var); - linear_form_upper_bound(lf + current, lf_plus_var_ub); - linear_form_upper_bound(lf - current, lf_minus_var_ub); - linear_form_upper_bound(minus_lf + current, var_minus_lf_ub); - linear_form_upper_bound(minus_lf - current, minus_lf_minus_var_ub); - assign_r(var_ite[n_curr_var], var_minus_lf_ub, ROUND_NOT_NEEDED); - assign_r(var_ite[n_curr_var+1], minus_lf_minus_var_ub, ROUND_NOT_NEEDED); - assign_r(var_cv_ite[n_curr_var], lf_plus_var_ub, ROUND_NOT_NEEDED); - assign_r(var_cv_ite[n_curr_var+1], lf_minus_var_ub, ROUND_NOT_NEEDED); + linear_form_upper_bound(lf + current, upper_bound); + assign_r(var_cv_ite[n_curr_var], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(lf - current, upper_bound); + assign_r(var_cv_ite[n_curr_var+1], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf + current, upper_bound); + assign_r(var_ite[n_curr_var], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf - current, upper_bound); + assign_r(var_ite[n_curr_var+1], upper_bound, ROUND_NOT_NEEDED); n_curr_var -= 2; } for (dimension_type curr_var = var_id+1; m_iter != m_end; ++m_iter) { @@ -5015,14 +5097,14 @@ Octagonal_Shape<T>::affine_image(Variable var, ++m_iter; Row_Reference m_cv_ite = *m_iter; Variable current(curr_var); - linear_form_upper_bound(lf + current, lf_plus_var_ub); - linear_form_upper_bound(lf - current, lf_minus_var_ub); - linear_form_upper_bound(minus_lf + current, var_minus_lf_ub); - linear_form_upper_bound(minus_lf - current, minus_lf_minus_var_ub); - assign_r(m_v_ite[n_var], lf_minus_var_ub, ROUND_NOT_NEEDED); - assign_r(m_v_ite[n_var+1], minus_lf_minus_var_ub, ROUND_NOT_NEEDED); - assign_r(m_cv_ite[n_var], lf_plus_var_ub, ROUND_NOT_NEEDED); - assign_r(m_cv_ite[n_var+1], var_minus_lf_ub, ROUND_NOT_NEEDED); + linear_form_upper_bound(lf + current, upper_bound); + assign_r(m_cv_ite[n_var], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(lf - current, upper_bound); + assign_r(m_v_ite[n_var], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf + current, upper_bound); + assign_r(m_cv_ite[n_var+1], upper_bound, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf - current, upper_bound); + assign_r(m_v_ite[n_var+1], upper_bound, ROUND_NOT_NEEDED); ++curr_var; }

1 0

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

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 8196e08325165286e583b4e6202c39ecf6d3376f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8196e0832516… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 15 15:16:05 2009 +0200 Added new test. --- tests/Floating_Point_Expression/affineimage3.cc | 28 +++++++++++++++++++--- 1 files changed, 24 insertions(+), 4 deletions(-) diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index cb619a5..d1ab707 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -34,8 +34,7 @@ test01() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); - Octagonal_Shape<float> oc2(3); - + print_constraints(oc1, "*** oc1 ***"); fl_r_oc free_term(-2); free_term.join_assign(1); Linear_Form<fl_r_oc> l(free_term); @@ -53,12 +52,32 @@ test01() { return ok; } -/* + // tests affine_image(A, [-1, -1]*A) bool test02() { - return true; + 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); + Linear_Form<fl_r_oc> l(-A); + oc1.affine_image(A, l); + print_constraints(oc1, "*** oc1.affine_image(A, [-1, -1]*A) ***"); + + Octagonal_Shape<float> known_result(3); + known_result.add_constraint(A >= -2); + known_result.add_constraint(B <= 2); + known_result.add_constraint(B - A <= 4); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; } +/* // tests affine_image(A, [-1, 1]*B) bool test03() { return true; @@ -74,4 +93,5 @@ bool test04() { BEGIN_MAIN DO_TEST(test01); + DO_TEST(test02); END_MAIN

1 0

[GIT] ppl/ppl(pip): Implemented simplex pivot on rational matrices.
by François Galea 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: pip Commit: b8e1cbd1782c3fa553331b6199668f4bb26581b1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b8e1cbd1782c… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Sep 15 15:09:08 2009 +0200 Implemented simplex pivot on rational matrices. --- src/PIP_Tree.cc | 111 +++++++++++++++++++++++++++++++++++++++++++++++++- src/PIP_Tree.defs.hh | 3 + 2 files changed, 112 insertions(+), 2 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 173d39f..c9f576a 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -253,6 +253,16 @@ PIP_Solution_Node::Rational_Matrix::normalize() { } void +PIP_Solution_Node::Rational_Matrix::scale(const Coefficient &ratio) { + dimension_type i, j; + dimension_type i_max = num_rows(); + dimension_type j_max = num_columns(); + for (i=0; i<i_max; ++i) + for (j=0; j<j_max; ++j) + rows[i][j] *= ratio; +} + +void PIP_Solution_Node::Rational_Matrix::ascii_dump(std::ostream& s) const { s << "denominator " << denominator << "\n"; Matrix::ascii_dump(s); @@ -472,6 +482,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node** parent_ref, Matrix context(ctx); merge_assign(context, constraints_); const dimension_type n_a_d = not_a_dimension(); + Coefficient gcd; // Main loop of the simplex algorithm for(;;) { @@ -539,7 +550,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node** parent_ref, std::cout << "Found row with negative parameters: " << i_ << std::endl; #endif - dimension_type j; + dimension_type j, k; Coefficient z(0); Coefficient sij, cij, cij_; Coefficient c; @@ -590,11 +601,107 @@ PIP_Solution_Node::solve(PIP_Tree_Node** parent_ref, << std::endl; #endif + /* ** Perform pivot operation ** */ + + /* Check if column j_ or row i_ correspond to a problem variable */ + dimension_type var_j = n_a_d; + dimension_type var_i = n_a_d; + for (j=0; j<num_vars; ++j) { + if (basis[j]) { + if (mapping[j] == j_) + var_j = j; + } else { + if (mapping[j] == i_) + var_i = j; + } + } + /* update basis */ + if (var_j != n_a_d) { + basis[var_j] = false; + mapping[var_j] = i_; + } + if (var_i != n_a_d) { + basis[var_i] = true; + mapping[var_i] = j_; + } + + /* create the identity matrix row corresponding to basic variable j_ */ + Row prs(num_vars, tableau.s.capacity(), Row::Flags()); + Row prt(num_params, tableau.t.capacity(), Row::Flags()); + prs[j_] = tableau.s.get_denominator(); + /* swap it with pivot row which would become identity after pivoting */ + prs.swap(tableau.s[i_]); + prt.swap(tableau.t[i_]); + sign[i_] = ZERO; + for (j=0; j<num_vars; ++j) { + if (j==j_) + continue; + for (k=0; k<num_rows; ++k) { + Coefficient mult = prs[j] * tableau.s[k][j_]; + if (mult % sij != 0) { + // Must scale matrix to stay in integer case + gcd_assign(gcd, mult, sij); + Coefficient scale_factor = sij/gcd; + tableau.s.scale(scale_factor); + mult *= scale_factor; + } + tableau.s[k][j] -= mult / sij; + } + } + + /* create the identity matrix row corresponding to basic variable j_ */ + for (j=0; j<num_params; ++j) { + for (k=0; k<num_rows; ++k) { + Coefficient c = prt[j] * tableau.s[k][j_]; + if (c % sij != 0) { + // Must scale matrix to stay in integer case + gcd_assign(gcd, c, sij); + Coefficient scale_factor = sij/gcd; + tableau.t.scale(scale_factor); + c *= scale_factor; + } + c /= sij; + tableau.t[k][j] -= c; + + s = sign[k]; + if (s != MIXED) { + switch (s) { + case ZERO: + if (c > 0) + sign[k] = NEGATIVE; + else if (c < 0) + sign[k] = POSITIVE; + break; + case POSITIVE: + if (c > 0) + sign[k] = MIXED; + break; + case NEGATIVE: + if (c < 0) + sign[k] = MIXED; + break; + default: + break; + } + } + } + } + + for (k=0; k<num_rows; ++k) { + Coefficient &c = tableau.s[k][j_]; + if (c % sij != 0) { + Coefficient gcd; + gcd_assign(gcd, c, sij); + Coefficient scale_factor = sij/gcd; + tableau.s.scale(scale_factor); + } + c /= sij; + } } + //FIXME: to be finished } // Main loop of the simplex algorithm - //FIXME return OPTIMIZED_PIP_PROBLEM; } diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index c8b2a16..e88aa0f 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -180,6 +180,9 @@ private: //! Copy constructor. Rational_Matrix(const Rational_Matrix& y); + //! Multiplies all coefficients and denominator with ratio. + void scale(const Coefficient &ratio); + //! Normalizes the modulo of coefficients so that they are mutually prime. /*! Computes the Greatest Common Divisor (GCD) among the elements of

1 0

[GIT] ppl/ppl(floating_point): Added a test for Octagonal_Shape:: affine_image in
by Roberto Amadini 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4670807b162f2b4a09893794bac6cf56829bc4fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4670807b162f… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 15 14:52:41 2009 +0200 Added a test for Octagonal_Shape::affine_image in tests/Floating_Point_Expression/affineimage3.cc --- tests/Floating_Point_Expression/Makefile.am | 4 +- tests/Floating_Point_Expression/affineimage3.cc | 77 +++++++++++++++++++++++ 2 files changed, 80 insertions(+), 1 deletions(-) diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index e455a93..4039297 100755 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -49,7 +49,8 @@ $(top_builddir)/tests/libppl_tests.a \ $(top_builddir)/src/libppl.la \ @extra_libraries@ -TESTS = floatingpointexpr1 +TESTS = floatingpointexpr1 \ +affineimage3 XFAIL_TESTS = @@ -60,6 +61,7 @@ BUGS = # floatingpointexpr1_SOURCES = floatingpointexpr1.cc +affineimage3_SOURCES = affineimage3.cc check_PROGRAMS = \ $(TESTS) \ diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc new file mode 100644 index 0000000..cb619a5 --- /dev/null +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -0,0 +1,77 @@ +/* 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). + +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 affine_image(A, [-2, 1]) +bool +test01() { + 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); + Octagonal_Shape<float> oc2(3); + + 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]) ***"); + + Octagonal_Shape<float> known_result(3); + known_result.add_constraint(A >= -2); + known_result.add_constraint(B <= 2); + known_result.add_constraint(A <= 1); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; +} + +/* +// tests affine_image(A, [-1, -1]*A) +bool test02() { + return true; +} + +// tests affine_image(A, [-1, 1]*B) +bool test03() { + return true; +} + +// tests affine_image(A, i + i1*A + i2*B) +bool test04() { + return true; +} +*/ + +} //namespace + +BEGIN_MAIN + DO_TEST(test01); +END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed a few typos preventing compilation.
by Fabio Bossi 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 30f2d12b77f8ffd9a6bcd1df187ff833eb23f730 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=30f2d12b77f8… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 15 11:50:10 2009 +0200 Fixed a few typos preventing compilation. --- src/Octagonal_Shape.templates.hh | 52 +++++++++++++++++++------------------- 1 files changed, 26 insertions(+), 26 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 2e0384e..761a468 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -550,36 +550,36 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( // in `left' and `right'. // Declare temporaries outside of the loop. - PPL_DIRTY_TEMP(N, ff_lb); - PPL_DIRTY_TEMP(N, ff_ub); - PPL_DIRTY_TEMP(N, fs_lb); - PPL_DIRTY_TEMP(N, fs_ub); - PPL_DIRTY_TEMP(N, sf_lb); - PPL_DIRTY_TEMP(N, sf_ub); - PPL_DIRTY_TEMP(N, ss_lb); - PPL_DIRTY_TEMP(N, ss_ub); + 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); // FIXME: to complete. dimension_type max_w_id = std::max(left_w_id, right_w_id); - for (dimension_type first_v = 0; first_v <= max_id; ++first_v) { - for (dimension_type second_v = first_v; second_v <= max_id; ++second_v) { - FP_Interval_Type* ffv_coefficient = - &(first.coefficient(Variable(first_v))); - FP_Interval_Type* fsv_coefficient = - &(first.coefficient(Variable(second_v))); - FP_Interval_Type* sfv_coefficient = - &(second.coefficient(Variable(first_v))); - FP_Interval_Type* ssv_coefficient = - &(second.coefficient(Variable(second_v))); - assign_r(ff_lb, ffv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(ff_ub, ffv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(fs_lb, fsv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(fs_ub, fsv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(sf_lb, sfv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(sf_ub, sfv_coefficient->upper(), ROUND_NOT_NEEDED); - assign_r(ss_lb, ssv_coefficient->lower(), ROUND_NOT_NEEDED); - assign_r(ss_ub, ssv_coefficient->upper(), ROUND_NOT_NEEDED); + for (dimension_type first_v = 0; first_v <= max_w_id; ++first_v) { + for (dimension_type second_v = first_v; second_v <= max_w_id; ++second_v) { + FP_Interval_Type* lfv_coefficient = + &(left.coefficient(Variable(first_v))); + FP_Interval_Type* lsv_coefficient = + &(left.coefficient(Variable(second_v))); + FP_Interval_Type* rfv_coefficient = + &(right.coefficient(Variable(first_v))); + 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); } }

1 0

[GIT] ppl/ppl(floating_point): Added missing assertion and FIXME note.
by Fabio Bossi 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 85157d3ca3cd5b5d6332cbe16637a494608d7028 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=85157d3ca3cd… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 15 11:24:39 2009 +0200 Added missing assertion and FIXME note. Started the implementation of refine_with_linear_form_inequality. --- src/Octagonal_Shape.defs.hh | 5 ++ src/Octagonal_Shape.templates.hh | 113 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 118 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index ab89bcd..1ed356b 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -986,6 +986,11 @@ public: */ void refine_with_congruences(const Congruence_System& cgs); + template <typename Interval_Info> + void refine_with_linear_form_inequality( + const Linear_Form< Interval<T, Interval_Info> >& left, + const Linear_Form< Interval<T, Interval_Info> >& right); + /*! \brief Computes the \ref Cylindrification "cylindrification" of \p *this with respect to space dimension \p var, assigning the result to \p *this. diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index c63676f..2e0384e 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -478,6 +478,116 @@ Octagonal_Shape<T>::add_congruence(const Congruence& cg) { } template <typename T> +template <typename Interval_Info> +void +Octagonal_Shape<T>::refine_with_linear_form_inequality( + const Linear_Form< Interval<T, Interval_Info> >& left, + const Linear_Form< Interval<T, Interval_Info> >& right) { + /* + FIXME: this way for checking that T is a floating point type is a bit + unelengant. + */ + // Check that T is a floating point type. + PPL_ASSERT(std::numeric_limits<T>::max_exponent); + + // Dimension-compatibility checks. + // The dimensions of `left' and `right' should not be greater than the + // dimension of `*this'. + const dimension_type left_space_dim = left.space_dimension(); + if (space_dim < left_space_dim) + throw_dimension_incompatible( + "refine_with_linear_form_inequality(left, right)", "left", left); + + const dimension_type right_space_dim = right.space_dimension(); + if (space_dim < right_space_dim) + throw_dimension_incompatible( + "refine_with_linear_form_inequality(left, right)", "right", right); + + /* + FIXME: these are not really necessary right now. They will come in + handy when we optimize the most common cases. + */ + // 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; + // Variable-index of the last non-zero coefficient in `left', if any. + dimension_type left_w_id = 0; + // Number of non-zero coefficients in `right': will be set to + // 0, 1, or 2, the latter value meaning any value greater than 1. + dimension_type right_t = 0; + // Variable-index of the last non-zero coefficient in `right', if any. + dimension_type right_w_id = 0; + + // Get information about the number of non-zero coefficients in `left'. + for (dimension_type i = left_space_dim; i-- > 0; ) + if (left.coefficient(Variable(i)) != 0) { + if (left_t++ == 1) + break; + else + left_w_id = i; + } + + // Get information about the number of non-zero coefficients in `right'. + for (dimension_type i = right_space_dim; i-- > 0; ) + if (right.coefficient(Variable(i)) != 0) { + if (right_t++ == 1) + break; + else + right_w_id = i; + } + + typedef typename OR_Matrix<N>::row_iterator Row_Iterator; + typedef typename OR_Matrix<N>::row_reference_type Row_Reference; + typedef typename OR_Matrix<N>::const_row_iterator Row_iterator; + typedef typename OR_Matrix<N>::const_row_reference_type Row_reference; + typedef Interval<T, Interval_Info> FP_Interval_Type; + + // TODO: optimize the most common cases. + + // General case. + + // FIRST, update the binary constraints for each pair of DIFFERENT variables + // in `left' and `right'. + + // Declare temporaries outside of the loop. + PPL_DIRTY_TEMP(N, ff_lb); + PPL_DIRTY_TEMP(N, ff_ub); + PPL_DIRTY_TEMP(N, fs_lb); + PPL_DIRTY_TEMP(N, fs_ub); + PPL_DIRTY_TEMP(N, sf_lb); + PPL_DIRTY_TEMP(N, sf_ub); + PPL_DIRTY_TEMP(N, ss_lb); + PPL_DIRTY_TEMP(N, ss_ub); + + // FIXME: to complete. + + dimension_type max_w_id = std::max(left_w_id, right_w_id); + for (dimension_type first_v = 0; first_v <= max_id; ++first_v) { + for (dimension_type second_v = first_v; second_v <= max_id; ++second_v) { + FP_Interval_Type* ffv_coefficient = + &(first.coefficient(Variable(first_v))); + FP_Interval_Type* fsv_coefficient = + &(first.coefficient(Variable(second_v))); + FP_Interval_Type* sfv_coefficient = + &(second.coefficient(Variable(first_v))); + FP_Interval_Type* ssv_coefficient = + &(second.coefficient(Variable(second_v))); + assign_r(ff_lb, ffv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(ff_ub, ffv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(fs_lb, fsv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(fs_ub, fsv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(sf_lb, sfv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(sf_ub, sfv_coefficient->upper(), ROUND_NOT_NEEDED); + assign_r(ss_lb, ssv_coefficient->lower(), ROUND_NOT_NEEDED); + assign_r(ss_ub, ssv_coefficient->upper(), ROUND_NOT_NEEDED); + } + } + + // Finally, update the unary constraints. + +} + +template <typename T> void Octagonal_Shape<T>::refine_no_check(const Constraint& c) { PPL_ASSERT(!marked_empty()); @@ -4926,6 +5036,8 @@ Octagonal_Shape<T>::affine_image(Variable var, mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_IGNORE); assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED); + PPL_ASSERT(OK()); + } template <typename T> @@ -4967,6 +5079,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, 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) { + // FIXME: ensure that ROUND_IGNORE works fine with divisions by 2. 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_IGNORE); neg_assign_r(curr_minus_var_ub, matrix[n_var][n_var+1], ROUND_NOT_NEEDED);

1 0