October 2010 - PPL-devel - BUGSENG Mailman

Question about PPL: Only one polyhedron-representation
by Sebastian Junges 29 Oct '10

29 Oct '10

Dear PPL-developers, We're currently considering to write a library making use of PPL. The main problem is that for method investigations we would like to make use of only one representation a time for polyhedra. Is there an efficient way of using the existing PPL, in such a manner that we can choose whether a constraint- or generator-based representation of polyhedra is used. We know that most functions are only implemented for only one of the representations, and we would add functions needed for the other representation ourselves. Thus, as question remains if we can efficiently stop the polyhedra from being updated to consistency after a changing function is run. With kind regards, Sebastian Junges Student Assistant RWTH Aachen Department of Computer Science Hybrid Systems Group

3 2

[GIT] ppl/ppl(floating_point): Added missing asserts.
by Fabio Bossi 23 Oct '10

23 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 6ba7085042a9983395f1b15daa1bf88b68a48eff URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6ba7085042a9… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Oct 23 14:48:50 2010 +0200 Added missing asserts. --- src/linearize.hh | 2 ++ 1 files changed, 2 insertions(+), 0 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 72e759a..48f55fa 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -678,6 +678,7 @@ linearize(const Concrete_Expression<Target>& expr, typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; + PPL_ASSERT(expr.type().is_floating_point()); // Check that analyzer_format is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<analyzer_format>::is_exact, "linearize<Target, FP_Interval_Type>:" @@ -789,6 +790,7 @@ linearize(const Concrete_Expression<Target>& expr, Here associated_dimensions.size() > 1. Try to return the LUB of all intervals associated to each space dimension. */ + PPL_ASSERT(associated_dimensions.size() > 1); std::set<dimension_type>::const_iterator i = associated_dimensions.begin(); std::set<dimension_type>::const_iterator i_end = associated_dimensions.end();

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Properly quote the assignment MAKE=$(MAKE).
by Roberto Bagnara 21 Oct '10

21 Oct '10

Module: ppl/ppl Branch: ppl-0_11-branch Commit: af113d9ac3779b5bf15531ba4551ed18430b0c75 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=af113d9ac377… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Oct 21 19:54:21 2010 +0200 Properly quote the assignment MAKE=$(MAKE). (Thanks to Volker Braun.) --- tests/BD_Shape/Makefile.am | 2 +- tests/Box/Makefile.am | 2 +- tests/Octagonal_Shape/Makefile.am | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/BD_Shape/Makefile.am b/tests/BD_Shape/Makefile.am index 0f69dc0..5cab708 100644 --- a/tests/BD_Shape/Makefile.am +++ b/tests/BD_Shape/Makefile.am @@ -124,7 +124,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Box/Makefile.am b/tests/Box/Makefile.am index 16cfbfc..cdb5618 100644 --- a/tests/Box/Makefile.am +++ b/tests/Box/Makefile.am @@ -128,7 +128,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Octagonal_Shape/Makefile.am b/tests/Octagonal_Shape/Makefile.am index c0fd9a3..a889eb5 100644 --- a/tests/Octagonal_Shape/Makefile.am +++ b/tests/Octagonal_Shape/Makefile.am @@ -131,7 +131,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp

1 0

[GIT] ppl/ppl(master): Properly quote the assignment MAKE=$(MAKE).
by Roberto Bagnara 21 Oct '10

21 Oct '10

Module: ppl/ppl Branch: master Commit: 5eb5954e1de39e24dd82ad553a8a06334f8ed607 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5eb5954e1de3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Oct 21 19:52:38 2010 +0200 Properly quote the assignment MAKE=$(MAKE). (Thanks to Volker Braun.) --- tests/BD_Shape/Makefile.am | 2 +- tests/Box/Makefile.am | 2 +- tests/Octagonal_Shape/Makefile.am | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/BD_Shape/Makefile.am b/tests/BD_Shape/Makefile.am index 0f69dc0..5cab708 100644 --- a/tests/BD_Shape/Makefile.am +++ b/tests/BD_Shape/Makefile.am @@ -124,7 +124,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Box/Makefile.am b/tests/Box/Makefile.am index 16cfbfc..cdb5618 100644 --- a/tests/Box/Makefile.am +++ b/tests/Box/Makefile.am @@ -128,7 +128,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Octagonal_Shape/Makefile.am b/tests/Octagonal_Shape/Makefile.am index c0fd9a3..a889eb5 100644 --- a/tests/Octagonal_Shape/Makefile.am +++ b/tests/Octagonal_Shape/Makefile.am @@ -131,7 +131,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp

1 0

[GIT] ppl/ppl(floating_point): Properly quote the assignment MAKE=$(MAKE).
by Roberto Bagnara 21 Oct '10

21 Oct '10

Module: ppl/ppl Branch: floating_point Commit: a8c98f2282f91292c4d511ad676fca4995d30f99 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a8c98f2282f9… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Oct 21 19:49:23 2010 +0200 Properly quote the assignment MAKE=$(MAKE). (Thanks to Volker Braun.) --- tests/BD_Shape/Makefile.am | 2 +- tests/Box/Makefile.am | 2 +- tests/Concrete_Expression/Makefile.am | 2 +- tests/Octagonal_Shape/Makefile.am | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/BD_Shape/Makefile.am b/tests/BD_Shape/Makefile.am index 0f69dc0..5cab708 100644 --- a/tests/BD_Shape/Makefile.am +++ b/tests/BD_Shape/Makefile.am @@ -124,7 +124,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Box/Makefile.am b/tests/Box/Makefile.am index 16cfbfc..cdb5618 100644 --- a/tests/Box/Makefile.am +++ b/tests/Box/Makefile.am @@ -128,7 +128,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Concrete_Expression/Makefile.am b/tests/Concrete_Expression/Makefile.am index 59f673b..4675a65 100644 --- a/tests/Concrete_Expression/Makefile.am +++ b/tests/Concrete_Expression/Makefile.am @@ -89,7 +89,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp diff --git a/tests/Octagonal_Shape/Makefile.am b/tests/Octagonal_Shape/Makefile.am index c0fd9a3..a889eb5 100644 --- a/tests/Octagonal_Shape/Makefile.am +++ b/tests/Octagonal_Shape/Makefile.am @@ -131,7 +131,7 @@ TESTS = run_tests.stamp .PHONY: run_tests.stamp run_tests.stamp: run_tests - +MAKE=$(MAKE) $(srcdir)/run_tests + +MAKE="$(MAKE)" $(srcdir)/run_tests echo "true" >run_tests.stamp chmod +x run_tests.stamp

1 0

[GIT] ppl/ppl(floating_point): Reflect latest changes to affine_image into
by Fabio Bossi 19 Oct '10

19 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 78e6e881955e7a87db62de79d6c21c5dae49494c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=78e6e881955e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 19 11:39:45 2010 +0200 Reflect latest changes to affine_image into affine_form_image. --- src/Octagonal_Shape.templates.hh | 101 +++++++++++--------------- tests/Concrete_Expression/octagonalshape1.cc | 2 + 2 files changed, 43 insertions(+), 60 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 9335e62..426b6fb 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5281,68 +5281,49 @@ Octagonal_Shape<T>::affine_form_image(const Variable var, if (is_w_coeff_one || is_w_coeff_minus_one) { // Case 2: lf = w_coeff*w + b, with w_coeff = [+/-1;+/-1]. 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'. - const Row_Iterator m_begin = matrix.row_begin(); - const Row_Iterator m_end = matrix.row_end(); - Row_Iterator m_iter = m_begin + n_var; - Row_Reference m_v = *m_iter; - ++m_iter; - Row_Reference m_cv = *m_iter; - ++m_iter; - // NOTE: delay update of unary constraints on `var' - for (dimension_type j = n_var; j-- > 0; ) { - N& m_v_j = m_v[j]; - add_assign_r(m_v_j, m_v_j, b_mlb, ROUND_UP); - N& m_cv_j = m_cv[j]; - add_assign_r(m_cv_j, m_cv_j, b_ub, ROUND_UP); - } - for ( ; m_iter != m_end; ++m_iter) { - Row_Reference m_i = *m_iter; - N& m_i_v = m_i[n_var]; - add_assign_r(m_i_v, m_i_v, b_ub, ROUND_UP); - N& m_i_cv = m_i[n_var+1]; - add_assign_r(m_i_cv, m_i_cv, b_mlb, ROUND_UP); - } - // Now update unary constraints on var. - mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP); - N& m_cv_v = m_cv[n_var]; - add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); - mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); - N& m_v_cv = m_v[n_var+1]; - add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); - reset_strongly_closed(); - } + // Here lf = w_coeff*v + b, with w_coeff = [+/-1;+/-1]. + if (is_w_coeff_one && is_b_zero) + // The transformation is the identity function. + return; + // Translate all the constraints on `var' by adding the value + // `b_ub' or subtracting the value `b_lb'. + if (is_w_coeff_minus_one) + std::swap(b_ub, b_mlb); + const Row_Iterator m_begin = matrix.row_begin(); + const Row_Iterator m_end = matrix.row_end(); + Row_Iterator m_iter = m_begin + n_var; + Row_Reference m_v = *m_iter; + ++m_iter; + Row_Reference m_cv = *m_iter; + ++m_iter; + // NOTE: delay update of unary constraints on `var'. + for (dimension_type j = n_var; j-- > 0; ) { + N& m_v_j = m_v[j]; + add_assign_r(m_v_j, m_v_j, b_mlb, ROUND_UP); + N& m_cv_j = m_cv[j]; + add_assign_r(m_cv_j, m_cv_j, b_ub, ROUND_UP); + if (is_w_coeff_minus_one) + std::swap(m_v_j, m_cv_j); } - else { - // Here `w_coeff = [-1;-1]. - // 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 (!is_b_zero) { - // Translate the unary constraints on `var' by adding the value - // `b_ub' or subtracting the value `b_lb'. - mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP); - mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); - add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); - add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); - } - incremental_strong_closure_assign(var); + for ( ; m_iter != m_end; ++m_iter) { + Row_Reference m_i = *m_iter; + N& m_i_v = m_i[n_var]; + add_assign_r(m_i_v, m_i_v, b_ub, ROUND_UP); + N& m_i_cv = m_i[n_var+1]; + add_assign_r(m_i_cv, m_i_cv, b_mlb, ROUND_UP); + if (is_w_coeff_minus_one) + std::swap(m_i_v, m_i_cv); } + // Now update unary constraints on var. + mul_2exp_assign_r(b_ub, b_ub, 1, ROUND_UP); + N& m_cv_v = m_cv[n_var]; + add_assign_r(m_cv_v, m_cv_v, b_ub, ROUND_UP); + mul_2exp_assign_r(b_mlb, b_mlb, 1, ROUND_UP); + N& m_v_cv = m_v[n_var+1]; + add_assign_r(m_v_cv, m_v_cv, b_mlb, ROUND_UP); + if (is_w_coeff_minus_one) + std::swap(m_cv_v, m_v_cv); + // Note: strong closure is preserved. } else { // Here `w != var', so that `lf' is of the form diff --git a/tests/Concrete_Expression/octagonalshape1.cc b/tests/Concrete_Expression/octagonalshape1.cc index f850641..211d548 100644 --- a/tests/Concrete_Expression/octagonalshape1.cc +++ b/tests/Concrete_Expression/octagonalshape1.cc @@ -100,6 +100,7 @@ bool test03() { free_term.join_assign(2); FP_Linear_Form l(-A); l += free_term; + print_constraints(oc1, "*** oc1 ***"); oc1.affine_form_image(A, l); print_constraints(oc1, "*** oc1.affine_form_image(A, -A + [0.5, 2]) ***"); @@ -107,6 +108,7 @@ bool test03() { known_result.add_constraint(-2 * A <= 3); known_result.add_constraint(B <= 2); known_result.add_constraint(2*B - 2*A <= 7); + known_result.add_constraint(2*A + 2*B >= -5); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result);

1 0

[GIT] ppl/ppl(master): Updated list of bug fixes.
by Enea Zaffanella 19 Oct '10

19 Oct '10

Module: ppl/ppl Branch: master Commit: 91b316106e1d492b61ef2c6f73596fb9114eac3e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=91b316106e1d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 09:10:47 2010 +0200 Updated list of bug fixes. --- NEWS | 8 ++++++++ 1 files changed, 8 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index eca7a4d..fdf1630 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,14 @@ o The input routine for PPL numeric datatypes has been extended to Bugfixes ======== +o Corrected a precision bug in method + + Octagonal_Shape<T>::affine_image() + + whereby in the case of an invertible affine transformation implementing + a variable sign symmetry (and optional translation), the computed result + was correct but unnecessarily imprecise. + o Corrected an efficiency bug in the C language interface function ppl_Linear_Expression_add_to_coefficient().

1 0

[GIT] ppl/ppl(floating_point): New commits
by Roberto Bagnara 19 Oct '10

19 Oct '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b250e9ec20fb… Merge: 951fdb8a9ff89a2ae59fcc1f726a2d4b05af445a 5c95fc0eab6a38442751ed16c6cfa9d538917f3f Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 08:37:09 2010 +0200 Merge branch 'master' into floating_point URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c95fc0eab6a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 08:15:12 2010 +0200 Improved precision of Octagonal_Shape::affine_image(). The method was rather imprecise on sign-symmetry affine transformations. Also noted that strong reduction is preserved in that case. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=78ef497331ef… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 17 08:17:46 2010 +0200 Dense_Row: remove the unused assign() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5cf4362e714d… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:18:04 2010 +0200 Sparse_Matrix: add some methods, to be fully compatible with Dense_Matrix. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=51b8b9197551… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:17:45 2010 +0200 Sparse_Row: add some methods, to be fully compatible with Dense_Row. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d535b8db149… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Oct 16 17:13:35 2010 +0200 CO_Tree: add a max_size() static method.

1 0

Octagonal_Shape::affine_image too imprecise?
by FABIO BOSSI 19 Oct '10

19 Oct '10

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.

2 1

[GIT] ppl/ppl(master): Improved precision of Octagonal_Shape::affine_image( ).
by Enea Zaffanella 19 Oct '10

19 Oct '10

Module: ppl/ppl Branch: master Commit: 5c95fc0eab6a38442751ed16c6cfa9d538917f3f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5c95fc0eab6a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Oct 19 08:15:12 2010 +0200 Improved precision of Octagonal_Shape::affine_image(). The method was rather imprecise on sign-symmetry affine transformations. Also noted that strong reduction is preserved in that case. --- src/Octagonal_Shape.templates.hh | 120 ++++++++++++++------------------- tests/Octagonal_Shape/affineimage1.cc | 24 +++++++ 2 files changed, 74 insertions(+), 70 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 7f74de5..8358b85 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4493,75 +4493,53 @@ Octagonal_Shape<T>::affine_image(const Variable var, // Case 2: expr = w_coeff*w + b, with w_coeff = +/- denominator. if (w_id == var_id) { // Here `expr' is of the form: +/- denominator * v + b. - if (w_coeff == denominator) { - if (b == 0) - // The transformation is the identity function. - return; - else { - // Translate all the constraints on `var' adding or - // subtracting the value `b/denominator'. - PPL_DIRTY_TEMP(N, d); - div_round_up(d, b, denominator); - PPL_DIRTY_TEMP(N, minus_d); - div_round_up(minus_d, b, minus_den); - const Row_Iterator m_begin = matrix.row_begin(); - const Row_Iterator m_end = matrix.row_end(); - Row_Iterator m_iter = m_begin + n_var; - Row_Reference m_v = *m_iter; - ++m_iter; - Row_Reference m_cv = *m_iter; - ++m_iter; - // NOTE: delay update of unary constraints on `var'. - for (dimension_type j = n_var; j-- > 0; ) { - N& m_v_j = m_v[j]; - add_assign_r(m_v_j, m_v_j, minus_d, ROUND_UP); - N& m_cv_j = m_cv[j]; - add_assign_r(m_cv_j, m_cv_j, d, ROUND_UP); - } - for ( ; m_iter != m_end; ++m_iter) { - Row_Reference m_i = *m_iter; - N& m_i_v = m_i[n_var]; - add_assign_r(m_i_v, m_i_v, d, ROUND_UP); - N& m_i_cv = m_i[n_var+1]; - add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); - } - // Now update unary constraints on var. - mul_2exp_assign_r(d, d, 1, ROUND_UP); - N& m_cv_v = m_cv[n_var]; - add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); - mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); - N& m_v_cv = m_v[n_var+1]; - add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); - } - reset_strongly_closed(); + const bool sign_symmetry = (w_coeff != denominator); + if (!sign_symmetry && b == 0) + // The transformation is the identity function. + return; + // Translate all the constraints on `var' adding or + // subtracting the value `b/denominator'. + PPL_DIRTY_TEMP(N, d); + div_round_up(d, b, denominator); + PPL_DIRTY_TEMP(N, minus_d); + div_round_up(minus_d, b, minus_den); + if (sign_symmetry) + std::swap(d, minus_d); + const Row_Iterator m_begin = matrix.row_begin(); + const Row_Iterator m_end = matrix.row_end(); + Row_Iterator m_iter = m_begin + n_var; + Row_Reference m_v = *m_iter; + ++m_iter; + Row_Reference m_cv = *m_iter; + ++m_iter; + // NOTE: delay update of unary constraints on `var'. + for (dimension_type j = n_var; j-- > 0; ) { + N& m_v_j = m_v[j]; + add_assign_r(m_v_j, m_v_j, minus_d, ROUND_UP); + N& m_cv_j = m_cv[j]; + add_assign_r(m_cv_j, m_cv_j, d, ROUND_UP); + if (sign_symmetry) + std::swap(m_v_j, m_cv_j); } - else { - // 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); - } + for ( ; m_iter != m_end; ++m_iter) { + Row_Reference m_i = *m_iter; + N& m_i_v = m_i[n_var]; + add_assign_r(m_i_v, m_i_v, d, ROUND_UP); + N& m_i_cv = m_i[n_var+1]; + add_assign_r(m_i_cv, m_i_cv, minus_d, ROUND_UP); + if (sign_symmetry) + std::swap(m_i_v, m_i_cv); + } + // Now update unary constraints on var. + mul_2exp_assign_r(d, d, 1, ROUND_UP); + N& m_cv_v = m_cv[n_var]; + add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP); + mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP); + N& m_v_cv = m_v[n_var+1]; + add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP); + if (sign_symmetry) + std::swap(m_cv_v, m_v_cv); + // Note: strong closure is preserved. } else { // Here `w != var', so that `expr' is of the form @@ -4570,7 +4548,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, forget_all_octagonal_constraints(var_id); const dimension_type n_w = 2*w_id; // Add the new constraint `var - w = b/denominator'. - if (w_coeff == denominator) + if (w_coeff == denominator) { if (var_id < w_id) { add_octagonal_constraint(n_w, n_var, b, denominator); add_octagonal_constraint(n_w+1, n_var+1, b, minus_den); @@ -4579,7 +4557,8 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_octagonal_constraint(n_var+1, n_w+1, b, denominator); add_octagonal_constraint(n_var, n_w, b, minus_den); } - else + } + else { // Add the new constraint `var + w = b/denominator'. if (var_id < w_id) { add_octagonal_constraint(n_w+1, n_var, b, denominator); @@ -4589,6 +4568,7 @@ Octagonal_Shape<T>::affine_image(const Variable var, add_octagonal_constraint(n_var+1, n_w, b, denominator); add_octagonal_constraint(n_var, n_w+1, b, minus_den); } + } incremental_strong_closure_assign(var); } PPL_ASSERT(OK()); diff --git a/tests/Octagonal_Shape/affineimage1.cc b/tests/Octagonal_Shape/affineimage1.cc index cdb850b..3f4e8b4 100644 --- a/tests/Octagonal_Shape/affineimage1.cc +++ b/tests/Octagonal_Shape/affineimage1.cc @@ -403,6 +403,7 @@ test15() { known_result.add_constraint(2*A <= -1); known_result.add_constraint(2*A >= -3); known_result.add_constraint(B >= 4); + known_result.add_constraint(2*A + 2*B >= 7); bool ok = check_result(oc, known_result); @@ -493,6 +494,28 @@ test18() { return ok; } +bool +test19() { + Variable x(0); + Variable y(1); + + TOctagonal_Shape oc1(2); + oc1.add_constraint(x + y == 0); + + print_constraints(oc1, "*** oc1 ***"); + + oc1.affine_image(x, -x); + + Octagonal_Shape<mpq_class> known_result(2); + known_result.add_constraint(x - y == 0); + + bool ok = (Octagonal_Shape<mpq_class>(oc1) == known_result); + + print_constraints(oc1, "*** oc1.affine_image(x, y) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -514,4 +537,5 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); + DO_TEST(test19); END_MAIN

1 0