
Module: ppl/ppl Branch: master Commit: 367a91ec09da66585614d6829dbb089066d57c77 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=367a91ec09da6...
Author: Roberto Bagnara bagnara@cs.unipr.it Date: Fri Nov 4 21:34:30 2011 +0100
Code layout corrections.
---
src/BD_Shape.templates.hh | 6 +++--- src/PIP_Tree.cc | 3 ++- src/checked_int.inlines.hh | 4 ++-- 3 files changed, 7 insertions(+), 6 deletions(-)
diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index 0635784..9d21ed6 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -3756,7 +3756,7 @@ BD_Shape<T>::refine(const Variable var, if (expr.coefficient(Variable(pinf_index-1)) == denominator) // Add the constraint `v - pinf_index <= sum'. add_dbm_constraint(pinf_index, v, sum); - break; + break;
case GREATER_OR_EQUAL: // Compute an upper approximation for `-sc_expr' into `sum'. @@ -4460,7 +4460,7 @@ void BD_Shape<T>::refine_with_linear_form_inequality( return; } } - else if (left_t == 1){ + else if (left_t == 1) { if (left_w_coeff == 1 || left_w_coeff == -1) { if (right_t == 0 || (right_w_coeff == 1 || right_w_coeff == -1)) { left_one_var_refine(left_w_id, right_t, right_w_id, left, right); @@ -4660,7 +4660,7 @@ BD_Shape<T> add_assign_r(ub, ub, a_plus_minus_b_minus, ROUND_UP); add_dbm_constraint(right_w_id + 1, 0, ub); } - return; + return; } if (is_left_coeff_one && is_right_coeff_minus_one) { // over-approximate (if is it possible) the inequality diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 84577a4..11d4603 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -2267,7 +2267,8 @@ PIP_Solution_Node::update_tableau( // Transform (expr > 0) into (expr - 1 >= 0). --p_row0; p_row0 *= denom; - } else + } + else if (constraint.is_strict_inequality()) // Transform (expr > 0) into (expr - 1 >= 0). neg_assign(p_row[0], denom); diff --git a/src/checked_int.inlines.hh b/src/checked_int.inlines.hh index c45f306..f3b7cf9 100644 --- a/src/checked_int.inlines.hh +++ b/src/checked_int.inlines.hh @@ -985,7 +985,7 @@ add_signed_int(Type& to, const Type x, const Type y, Rounding_Dir dir) { return set_pos_overflow_int<To_Policy>(to, dir); } else if (x < Extended_Int<To_Policy, Type>::min - y) - return set_neg_overflow_int<To_Policy>(to, dir); + return set_neg_overflow_int<To_Policy>(to, dir); } to = x + y; return V_EQ; @@ -1014,7 +1014,7 @@ sub_signed_int(Type& to, const Type x, const Type y, Rounding_Dir dir) { return set_neg_overflow_int<To_Policy>(to, dir); } else if (x > Extended_Int<To_Policy, Type>::max + y) - return set_pos_overflow_int<To_Policy>(to, dir); + return set_pos_overflow_int<To_Policy>(to, dir); } to = x - y; return V_EQ;