- PPL-devel - BUGSENG Mailman

ppl-0.11 configure warning
by Livingstone, Paul＠ARB 09 Nov '10

09 Nov '10

Dear PPL developer, Following the instructions in the config.log from configuring PPL-0.11 for updating gcc on a linux machine running Redhat Linux OS version 5.4, I am reporting that there were warnings on the following five header files: (1) fenv.h (2) getopt.h (3) signal.h (4) sys/resource.h (5) sys/time.h The warning messages were: "present but cannot be compiled\n check for missing prerequisite headers?\n see the Autoconf documentation\n section "Present But Cannot Be Compiled"\n proceeding with the compiler's result\n" Your attention will be appreciated. Sincerely, Paul Dr. Paul Livingstone Staff Air Pollution Specialist California Air Resources Board Sacramento, CA 95812 Phone: (916) 327-8543

2 1

[GIT] ppl/ppl(floating_point): Merge branch 'master' into floating_point
by Roberto Bagnara 07 Nov '10

07 Nov '10

Module: ppl/ppl Branch: floating_point Commit: d711641e727be3d69ca817a6bdac006b88d2cd8c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d711641e727b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Nov 7 14:50:31 2010 +0100 Merge branch 'master' into floating_point ---

1 0

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

07 Nov '10

Module: ppl/ppl Branch: floating_point 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): Updated list of bug fixes.
by Enea Zaffanella 07 Nov '10

07 Nov '10

Module: ppl/ppl Branch: floating_point 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

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