[PPL-devel] [GIT] ppl/ppl(floating_point): Added missing assertion and FIXME note.
Fabio Bossi
bossi at cs.unipr.it
Tue Sep 15 11:21:52 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: 85157d3ca3cd5b5d6332cbe16637a494608d7028
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=85157d3ca3cd5b5d6332cbe16637a494608d7028
Author: Fabio Bossi <bossi at 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);
More information about the PPL-devel
mailing list