[PPL-devel] Octagonal_Shape::affine_image too imprecise?

[FABIO BOSSI]

Octagonal_Shape::affine_image seems a bit too imprecise when treating
assignments of the form Y = -Y + c.

Here's the code involved:

          // Here `w_coeff == -denominator'.
          // Remove the binary constraints on `var'.
          forget_binary_octagonal_constraints(var_id);
          const Row_Iterator m_begin = matrix.row_begin();
          Row_Iterator m_iter = m_begin + n_var;
          N& m_v_cv = (*m_iter)[n_var+1];
          ++m_iter;
          N& m_cv_v = (*m_iter)[n_var];
          // Swap the unary constraints on `var'.
          std::swap(m_v_cv, m_cv_v);
          // Strong closure is not preserved.
          reset_strongly_closed();
          if (b != 0) {
            // Translate the unary constraints on `var',
            // adding or subtracting the value `b/denominator'.
            PPL_DIRTY_TEMP(N, d);
            div_round_up(d, b, denominator);
            mul_2exp_assign_r(d, d, 1, ROUND_UP);
            add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP);
            PPL_DIRTY_TEMP(N, minus_d);
            div_round_up(minus_d, b, minus_den);
            mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP);
            add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP);
          }
          incremental_strong_closure_assign(var);
         }

This approach that discards all old binary constraints on the assigned
variable looks a little too naive to me. Consider for instance this
assigment sequence:

X = Y;
Y = -Y;

The octagonal domain will not be able to deduce X + Y = 0 as I would expect.
A similar problem probably exists for BD Shapes.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20101018/915b9c55/attachment.htm>