[PPL-devel] [GIT] ppl/ppl(floating_point): Fixed a bug in affine_image and modified one_variable_affine_image.
Roberto Amadini
r.amadini at virgilio.it
Mon Sep 21 18:47:25 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: faefe0f0d2247dbd65bdd5aebade57a61b2e6a9b
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=faefe0f0d2247dbd65bdd5aebade57a61b2e6a9b
Author: Roberto Amadini <r.amadini at virgilio.it>
Date: Mon Sep 21 18:45:29 2009 +0200
Fixed a bug in affine_image and modified one_variable_affine_image.
Added a new test for the general case.
---
src/BD_Shape.templates.hh | 130 +++++++++++++--------------
tests/Floating_Point_Expression/bdshape1.cc | 27 ++++++
2 files changed, 90 insertions(+), 67 deletions(-)
diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh
index 5cbf5a5..08b1c5d 100644
--- a/src/BD_Shape.templates.hh
+++ b/src/BD_Shape.templates.hh
@@ -4103,11 +4103,12 @@ BD_Shape<T>::affine_image(const Variable& var,
}
else if (t == 1) {
const FP_Interval_Type& w_coeff = lf.coefficient(Variable(w_id - 1));
- one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim);
- PPL_ASSERT(OK());
- return;
+ if(w_coeff == 1 || w_coeff == -1) {
+ one_variable_affine_image(var_id, b, w_coeff, w_id, space_dim);
+ PPL_ASSERT(OK());
+ return;
+ }
}
-
two_variables_affine_image(var_id, lf, space_dim);
PPL_ASSERT(OK());
}
@@ -4154,76 +4155,71 @@ void BD_Shape<T>
bool is_b_zero = (b_mlb == 0 && b_ub == 0);
// true if w_coeff = [1;1]
bool is_w_coeff_one = (w_coeff == 1);
- // true if w_coeff = [-1;-1].
- bool is_w_coeff_minus_one = (w_coeff == -1);
- if (is_w_coeff_one || is_w_coeff_minus_one) {
- if (w_id == var_id) {
- // Here `lf' is of the form: [+/-1;+/-1] * v + b.
- if (is_w_coeff_one) {
- if (is_b_zero)
- // The transformation is the identity function.
- return;
- else {
- // Translate all the constraints on `var' by adding the value
- // `b_ub' or subtracting the value `b_lb'.
- DB_Row<N>& dbm_v = dbm[var_id];
- for (dimension_type i = space_dim + 1; i-- > 0; ) {
- N& dbm_vi = dbm_v[i];
- add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP);
- N& dbm_iv = dbm[i][var_id];
- add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP);
- }
- // Both shortest-path closure and reduction are preserved.
- }
- }
+ if (w_id == var_id) {
+ // Here `lf' is of the form: [+/-1;+/-1] * v + b.
+ if (is_w_coeff_one) {
+ if (is_b_zero)
+ // The transformation is the identity function.
+ return;
else {
- // Here `w_coeff = [-1;-1].
- // Remove the binary constraints on `var'.
- forget_binary_dbm_constraints(var_id);
- std::swap(dbm[var_id][0], dbm[0][var_id]);
- // Shortest-path closure is not preserved.
- reset_shortest_path_closed();
- if (!is_b_zero) {
- // Translate the unary constraints on `var' by adding the value
- // `b_ub' or subtracting the value `b_lb'.
- N& dbm_v0 = dbm[var_id][0];
- add_assign_r(dbm_v0, dbm_v0, b_mlb, ROUND_UP);
- N& dbm_0v = dbm[0][var_id];
- add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP);
+ // Translate all the constraints on `var' by adding the value
+ // `b_ub' or subtracting the value `b_lb'.
+ DB_Row<N>& dbm_v = dbm[var_id];
+ for (dimension_type i = space_dim + 1; i-- > 0; ) {
+ N& dbm_vi = dbm_v[i];
+ add_assign_r(dbm_vi, dbm_vi, b_mlb, ROUND_UP);
+ N& dbm_iv = dbm[i][var_id];
+ add_assign_r(dbm_iv, dbm_iv, b_ub, ROUND_UP);
}
+ // Both shortest-path closure and reduction are preserved.
+ }
+ }
+ else {
+ // Here `w_coeff = [-1;-1].
+ // Remove the binary constraints on `var'.
+ forget_binary_dbm_constraints(var_id);
+ std::swap(dbm[var_id][0], dbm[0][var_id]);
+ // Shortest-path closure is not preserved.
+ reset_shortest_path_closed();
+ if (!is_b_zero) {
+ // Translate the unary constraints on `var' by adding the value
+ // `b_ub' or subtracting the value `b_lb'.
+ N& dbm_v0 = dbm[var_id][0];
+ add_assign_r(dbm_v0, dbm_v0, b_mlb, ROUND_UP);
+ N& dbm_0v = dbm[0][var_id];
+ add_assign_r(dbm_0v, dbm_0v, b_ub, ROUND_UP);
}
}
+ }
+ else {
+ // Here `w != var', so that `lf' is of the form
+ // [+/-1;+/-1] * w + b.
+ // Remove all constraints on `var'.
+ forget_all_dbm_constraints(var_id);
+ // Shortest-path closure is preserved, but not reduction.
+ if (marked_shortest_path_reduced())
+ reset_shortest_path_reduced();
+ if (is_w_coeff_one) {
+ // Add the new constraints `var - w >= b_lb'
+ // `and var - w <= b_ub'.
+ add_dbm_constraint(w_id, var_id, b_ub);
+ add_dbm_constraint(var_id, w_id, b_mlb);
+ }
else {
- // Here `w != var', so that `lf' is of the form
- // [+/-1;+/-1] * w + b.
- // Remove all constraints on `var'.
- forget_all_dbm_constraints(var_id);
- // Shortest-path closure is preserved, but not reduction.
- if (marked_shortest_path_reduced())
- reset_shortest_path_reduced();
-
- if (is_w_coeff_one) {
- // Add the new constraints `var - w >= b_lb'
- // `and var - w <= b_ub'.
- add_dbm_constraint(w_id, var_id, b_ub);
- add_dbm_constraint(var_id, w_id, b_mlb);
+ // We have to add the constraint `v + w == b', over-approximating it
+ // by computing lower and upper bounds for `w'.
+ const N& mlb_w = dbm[w_id][0];
+ if (!is_plus_infinity(mlb_w)) {
+ // Add the constraint `v <= ub - lb_w'.
+ add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP);
+ reset_shortest_path_closed();
}
- else {
- // We have to add the constraint `v + w == b', over-approximating it
- // by computing lower and upper bounds for `w'.
- const N& mlb_w = dbm[w_id][0];
- if (!is_plus_infinity(mlb_w)) {
- // Add the constraint `v <= ub - lb_w'.
- add_assign_r(dbm[0][var_id], b_ub, mlb_w, ROUND_UP);
- reset_shortest_path_closed();
- }
- const N& ub_w = dbm[0][w_id];
- if (!is_plus_infinity(ub_w)) {
- // Add the constraint `v >= lb - ub_w'.
- add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP);
- reset_shortest_path_closed();
- }
+ const N& ub_w = dbm[0][w_id];
+ if (!is_plus_infinity(ub_w)) {
+ // Add the constraint `v >= lb - ub_w'.
+ add_assign_r(dbm[var_id][0], ub_w, b_mlb, ROUND_UP);
+ reset_shortest_path_closed();
}
}
}
diff --git a/tests/Floating_Point_Expression/bdshape1.cc b/tests/Floating_Point_Expression/bdshape1.cc
index e5f06d1..0c8e305 100644
--- a/tests/Floating_Point_Expression/bdshape1.cc
+++ b/tests/Floating_Point_Expression/bdshape1.cc
@@ -253,6 +253,32 @@ bool test08() {
return ok;
}
+// tests affine_image(B, [-0.5, 0.5]*A)
+bool test09() {
+ Variable A(0);
+ Variable B(1);
+
+ BD_Shape<double> bd1(3);
+ bd1.add_constraint(A <= 2);
+ bd1.add_constraint(A - B <= 3);
+ bd1.add_constraint(B <= 2);
+ db_r_oc coeff(-0.5);
+ coeff.join_assign(0.5);
+ Linear_Form<db_r_oc> l(A);
+ l *= coeff;
+ bd1.affine_image(B, l);
+ print_constraints(bd1, "*** bd1.affine_image(B, [-0.5, 0.5]*A) ***");
+
+ BD_Shape<double> known_result(3);
+ known_result.add_constraint(A <= 2);
+ known_result.add_constraint(A - B <= 3);
+ print_constraints(known_result, "*** known_result ***");
+
+ bool ok = (bd1 == known_result);
+
+ return ok;
+}
+
} // namespace
BEGIN_MAIN
@@ -264,4 +290,5 @@ BEGIN_MAIN
DO_TEST(test06);
DO_TEST(test07);
DO_TEST(test08);
+ DO_TEST(test09);
END_MAIN
More information about the PPL-devel
mailing list