[PPL-devel] [GIT] ppl/ppl(floating_point): Added more cases for refine_linear_form_inequality.
Fabio Bossi
bossi at cs.unipr.it
Wed Sep 16 12:21:00 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: e492c9a5c5291b95b3abffee549174744a9c8fe3
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e492c9a5c5291b95b3abffee549174744a9c8fe3
Author: Fabio Bossi <bossi at cs.unipr.it>
Date: Wed Sep 16 12:21:30 2009 +0200
Added more cases for refine_linear_form_inequality.
---
src/Octagonal_Shape.templates.hh | 188 +++++++++++++++++++++++++++++++++++++-
1 files changed, 183 insertions(+), 5 deletions(-)
diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh
index 9d4e70c..08feb94 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(
if (marked_empty())
return;
- /*
- 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;
@@ -545,7 +541,189 @@ 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;
- // TODO: optimize the most common cases.
+ if (left_t == 0) {
+ if (right_t == 0) {
+ // The constraint involves constants only. Ignore it: it is up to
+ // the analyzer to handle it.
+ return;
+ }
+
+ if (right_t == 1) {
+ // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x.
+ // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1].
+ const FP_Interval_Type& right_w_coeff =
+ right.coefficient(Variable(right_w_id));
+ if (right_w_coeff == 1) {
+ const dimension_type n_right = right_w_id * 2;
+ PPL_DIRTY_TEMP(N, b_plus_minus_a_minus);
+ const FP_Interval_Type& left_a = left.inhomogeneous_term();
+ const FP_Interval_Type& right_b = right.inhomogeneous_term();
+ sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(),
+ ROUND_UP);
+ mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1,
+ ROUND_IGNORE);
+ add_octagonal_constraint(n_right, n_right+1, b_plus_minus_a_minus);
+ return;
+ }
+
+ if (right_w_coeff == -1) {
+ const dimension_type n_right = right_w_id * 2;
+ PPL_DIRTY_TEMP(N, b_plus_minus_a_minus);
+ const FP_Interval_Type& left_a = left.inhomogeneous_term();
+ const FP_Interval_Type& right_b = right.inhomogeneous_term();
+ sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(),
+ ROUND_UP);
+ mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1,
+ ROUND_IGNORE);
+ add_octagonal_constraint(n_right+1, n_right, b_plus_minus_a_minus);
+ return;
+ }
+ }
+ }
+ else if (left_t == 1) {
+ if (right_t == 0) {
+ // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+]
+ // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1].
+ const FP_Interval_Type& left_w_coeff =
+ left.coefficient(Variable(left_w_id));
+ if (left_w_coeff == 1) {
+ const dimension_type n_left = left_w_id * 2;
+ PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+ const FP_Interval_Type& left_b = left.inhomogeneous_term();
+ const FP_Interval_Type& right_a = right.inhomogeneous_term();
+ sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+ ROUND_UP);
+ mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1,
+ ROUND_IGNORE);
+ add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus);
+ return;
+ }
+
+ if (left_w_coeff == -1) {
+ const dimension_type n_left = left_w_id * 2;
+ PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+ const FP_Interval_Type& left_b = left.inhomogeneous_term();
+ const FP_Interval_Type& right_a = right.inhomogeneous_term();
+ sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+ ROUND_UP);
+ mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1,
+ ROUND_IGNORE);
+ add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus);
+ return;
+ }
+ }
+
+ if (right_t == 1) {
+ // The constraint has the form:
+ // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y.
+ // Reduce it to the constraint +/-x +/-y <= c+ - a-
+ // if [b-;b+] = +/-[1;1] and [d-;d+] = +/-[1;1].
+ const FP_Interval_Type& left_w_coeff =
+ left.coefficient(Variable(left_w_id));
+ const FP_Interval_Type& right_w_coeff =
+ right.coefficient(Variable(right_w_id));
+ bool is_left_coeff_one = (left_w_coeff == 1);
+ bool is_left_coeff_minus_one = (left_w_coeff == -1);
+ 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_constraint_minus_one) {
+ // Here we have an identity or a constants-only constraint.
+ return;
+ }
+ if (is_left_coeff_one && is_right_coeff_minus_one) {
+ // We fall back to a previous case
+ // (but we do not need to multiply the result by two).
+ const dimension_type n_left = left_w_id * 2;
+ PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+ const FP_Interval_Type& left_b = left.inhomogeneous_term();
+ const FP_Interval_Type& right_a = right.inhomogeneous_term();
+ sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+ ROUND_UP);
+ add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus);
+ return;
+ }
+ if (is_left_coeff_minus_one && is_right_coeff_one) {
+ // We fall back to a previous case
+ // (but we do not need to multiply the result by two).
+ const dimension_type n_left = left_w_id * 2;
+ PPL_DIRTY_TEMP(N, a_plus_minus_b_minus);
+ const FP_Interval_Type& left_b = left.inhomogeneous_term();
+ const FP_Interval_Type& right_a = right.inhomogeneous_term();
+ sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(),
+ ROUND_UP);
+ add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus);
+ return;
+ }
+ }
+ else if (is_left_coeff_one && is_right_coeff_one) {
+ const dimension_type n_left = left_w_id * 2;
+ const dimension_type n_right = right_w_id * 2;
+ PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+ const FP_Interval_Type& left_a = left.inhomogeneous_term();
+ 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(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+ ROUND_IGNORE);
+ if (left_w_id < right_w_id)
+ add_octagonal_constraint(n_right, n_left, c_plus_minus_a_minus);
+ else
+ add_octagonal_constraint(n_left+1, n_right+1, c_plus_minus_a_minus);
+ return;
+ }
+ if (is_left_coeff_one && is_right_coeff_minus_one) {
+ const dimension_type n_left = left_w_id * 2;
+ const dimension_type n_right = right_w_id * 2;
+ PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+ const FP_Interval_Type& left_a = left.inhomogeneous_term();
+ 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(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+ ROUND_IGNORE);
+ if (left_w_id < right_w_id)
+ add_octagonal_constraint(n_right+1, n_left, c_plus_minus_a_minus);
+ else
+ add_octagonal_constraint(n_left+1, n_right, c_plus_minus_a_minus);
+ return;
+ }
+ if (is_left_coeff_minus_one && is_right_coeff_one) {
+ const dimension_type n_left = left_w_id * 2;
+ const dimension_type n_right = right_w_id * 2;
+ PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+ const FP_Interval_Type& left_a = left.inhomogeneous_term();
+ 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(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+ ROUND_IGNORE);
+ if (left_w_id < right_w_id)
+ add_octagonal_constraint(n_right, n_left+1, c_plus_minus_a_minus);
+ else
+ add_octagonal_constraint(n_left, n_right+1, c_plus_minus_a_minus);
+ return;
+ }
+ if (is_left_coeff_minus_one && is_right_coeff_minus_one) {
+ const dimension_type n_left = left_w_id * 2;
+ const dimension_type n_right = right_w_id * 2;
+ PPL_DIRTY_TEMP(N, c_plus_minus_a_minus);
+ const FP_Interval_Type& left_a = left.inhomogeneous_term();
+ 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(c_plus_minus_a_minus, c_plus_minus_a_minus, 1,
+ ROUND_IGNORE);
+ if (left_w_id < right_w_id)
+ add_octagonal_constraint(n_right+1, n_left+1, c_plus_minus_a_minus);
+ else
+ add_octagonal_constraint(n_left, n_right, c_plus_minus_a_minus);
+ return;
+ }
+ }
+
+ }
// General case.
More information about the PPL-devel
mailing list