January 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Forward declare classes before making them friends.
by Enea Zaffanella 25 Jan '10

25 Jan '10

Module: ppl/ppl Branch: master Commit: 3f15af9db40f7ca5148960bd4d572d46c7f2830a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3f15af9db40f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Jan 25 14:41:09 2010 +0100 Forward declare classes before making them friends. Included Grid.types.hh in Congruence_/Grid_Generator_ System.defs.hh. Do not uselessly include Grid.types.hh in Generator_system.defs.hh. --- src/Congruence_System.defs.hh | 1 + src/Generator_System.defs.hh | 1 - src/Grid_Generator_System.defs.hh | 1 + 3 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Congruence_System.defs.hh b/src/Congruence_System.defs.hh index abf2c78..aafa664 100644 --- a/src/Congruence_System.defs.hh +++ b/src/Congruence_System.defs.hh @@ -29,6 +29,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Congruence.types.hh" #include "Grid_Generator.types.hh" #include "Matrix.defs.hh" +#include "Grid.types.hh" #include "Grid_Certificate.types.hh" #include <iosfwd> diff --git a/src/Generator_System.defs.hh b/src/Generator_System.defs.hh index a6413c2..b34f895 100644 --- a/src/Generator_System.defs.hh +++ b/src/Generator_System.defs.hh @@ -31,7 +31,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Constraint.types.hh" #include "Polyhedron.types.hh" #include "Poly_Con_Relation.defs.hh" -#include "Grid.types.hh" #include <iosfwd> namespace Parma_Polyhedra_Library { diff --git a/src/Grid_Generator_System.defs.hh b/src/Grid_Generator_System.defs.hh index 2c3d783..7ad7960 100644 --- a/src/Grid_Generator_System.defs.hh +++ b/src/Grid_Generator_System.defs.hh @@ -27,6 +27,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Generator_System.defs.hh" #include "Grid_Generator.types.hh" #include "Variables_Set.types.hh" +#include "Grid.types.hh" #include <iosfwd> namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/w3ppl(master): BagnaraHZ09CGTA renamed and completed.
by Roberto Bagnara 24 Jan '10

24 Jan '10

Module: ppl/w3ppl Branch: master Commit: 2cb646562378796ad8fb3522dc74f747929ed909 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=2cb6465623… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Jan 24 10:18:14 2010 +0100 BagnaraHZ09CGTA renamed and completed. --- .../{BagnaraHZ09CGTA.pdf => BagnaraHZ10CGTA.pdf} | Bin 347557 -> 347557 bytes htdocs/Documentation/ppl.bib | 9 ++++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/htdocs/Documentation/BagnaraHZ09CGTA.pdf b/htdocs/Documentation/BagnaraHZ10CGTA.pdf similarity index 100% rename from htdocs/Documentation/BagnaraHZ09CGTA.pdf rename to htdocs/Documentation/BagnaraHZ10CGTA.pdf diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 47ba14e..05364bd 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -869,13 +869,16 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ08SCP.pdf" } -@Article{BagnaraHZ09CGTA, +@Article{BagnaraHZ10CGTA, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions", Journal = "Computational Geometry: Theory and Applications", + Volume = 43, + Number = 5, + Pages = "453--473", Publisher = "Elsevier", - Year = 2009, + Year = 2010, Note = "To appear in print. Available online at \url{http://dx.doi.org/10.1016/j.comgeo.2009.09.002}", Abstract = "Deciding whether the union of two convex polyhedra is @@ -904,7 +907,7 @@ abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.", - URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09CGTA.pdf" + URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ10CGTA.pdf" } @Article{BagnaraHZ09TCS,

1 0

[GIT] ppl/ppl(pip): Added a not working incremental solve test.
by François Galea 22 Jan '10

22 Jan '10

Module: ppl/ppl Branch: pip Commit: a7f6b5d260af5b40b81bb75e0575d47f1d06b53e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a7f6b5d260af… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Jan 22 08:15:24 2010 +0100 Added a not working incremental solve test. --- tests/PIP_Problem/pipproblem1.cc | 34 ++++++++++++++++++++++++++++++++++ 1 files changed, 34 insertions(+), 0 deletions(-) diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index c6d0ae7..a90ab9d 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -244,6 +244,39 @@ test06() { return ok; } +bool +test07() { + Variable i(0); + Variable j(1); + Variable m(2); + Variable n(3); + Variables_Set params(m, n); + + PIP_Problem pip(4); + pip.add_to_parameter_space_dimensions(params); + + pip.add_constraint(3*j >= -2*i+8); + pip.add_constraint(j <= 4*i - 4); + pip.add_constraint(i <= n); + pip.add_constraint(n >= 3); + bool ok = (pip.solve() == OPTIMIZED_PIP_PROBLEM); + if (ok) { + const PIP_Tree solution = pip.solution(); + display_solution(solution, params, Variables_Set(i, j), + pip.space_dimension()); + } + + pip.add_constraint(j <= m); + ok &= (pip.solve() == OPTIMIZED_PIP_PROBLEM); + if (ok) { + const PIP_Tree solution = pip.solution(); + display_solution(solution, params, Variables_Set(i, j), + pip.space_dimension()); + } + + return ok; +} + } // namespace BEGIN_MAIN @@ -253,4 +286,5 @@ BEGIN_MAIN DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); + DO_TEST(test07); END_MAIN

1 0

[GIT] ppl/ppl(pip): Fixed bugs. Now test07 in pipproblem2.cc is successful.
by François Galea 22 Jan '10

22 Jan '10

Module: ppl/ppl Branch: pip Commit: 91de7841156c141b9c0935e673b6c29fbb3e7859 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=91de7841156c… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Jan 20 08:23:22 2010 +0100 Fixed bugs. Now test07 in pipproblem2.cc is successful. --- src/PIP_Problem.cc | 3 +++ src/PIP_Tree.cc | 3 ++- 2 files changed, 5 insertions(+), 1 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index d08a633..a4b0b2d 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -524,6 +524,9 @@ PPL::PIP_Problem::add_constraint(const Constraint& c) { throw std::invalid_argument(s.str()); } input_cs.push_back(c); + // Update problem status. + if (status != UNSATISFIABLE) + status = PARTIALLY_SATISFIABLE; } void diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 56c79b7..36a60a8 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -1257,7 +1257,8 @@ PIP_Solution_Node::update_tableau(const PIP_Problem& problem, dimension_type i; dimension_type n_params = parameters.size(); dimension_type n_vars = external_space_dim - n_params; - dimension_type internal_space_dim = tableau.t.num_columns()-1; + dimension_type internal_space_dim = tableau.s.num_columns() + + tableau.t.num_columns() - 1; Constraint_Sequence::const_iterator cst; // Create the parameter column, corresponding to the constant term

1 0

suggestion for a ppl configure enhancement
by Rainer Emrich 14 Jan '10

14 Jan '10

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 IMHO it would be a godd idea to add the following two configure options: --with-gmp-include=DIR GMP include directory --with-gmp-lib=DIR GMP lib directory On 64-bit Linux systems you have the libraries in lib64 instead of lib in most cases. With this additional configure options in place you do not need to fiddle with LDFLAFS to find the library. OTOH I think you may drop --with-libgmpxx-prefix because it's very unlikely that libgmpxx is installed in a different place than libgmp. Cheers Rainer -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAktOIAwACgkQoUhjsh59BL5TEgCgrgH+snQjpXlmMp6Xoa7BJH3E n48AoLnpbxfZp8mJzdwNJ8RmyVXn0avL =0krb -----END PGP SIGNATURE-----

2 1

[GIT] ppl/w3ppl(master): BagnaraHZ10FMSD renamed and completed.
by Roberto Bagnara 14 Jan '10

14 Jan '10

Module: ppl/w3ppl Branch: master Commit: 18776b2a1e59fdeae8f7316041b858eca420595a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=18776b2a1e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jan 14 11:18:28 2010 +0100 BagnaraHZ10FMSD renamed and completed. --- .../{BagnaraHZ10FMSD.pdf => BagnaraHZ09FMSD.pdf} | Bin 448185 -> 448185 bytes htdocs/Documentation/ppl.bib | 11 ++++++----- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/htdocs/Documentation/BagnaraHZ10FMSD.pdf b/htdocs/Documentation/BagnaraHZ09FMSD.pdf similarity index 100% rename from htdocs/Documentation/BagnaraHZ10FMSD.pdf rename to htdocs/Documentation/BagnaraHZ09FMSD.pdf diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index a65f5ad..47ba14e 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -936,15 +936,16 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf" } -@Article{BagnaraHZ10FMSD, +@Article{BagnaraHZ09FMSD, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness", Journal = "Formal Methods in System Design", + Volume = 35, + Number = 3, Publisher = "Springer-Verlag, Berlin", - Year = 2010, - Note = "To appear in print. Available online at - \url{http://www.springerlink.com/content/100266/?Content+Status=Accepted}", + Year = 2009, + Pages = "279--323", Abstract = "Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal @@ -972,7 +973,7 @@ rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.", - URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ10FMSD.pdf" + URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09FMSD.pdf" } @Techreport{BagnaraHZ09TRa,

1 0

[GIT] ppl/w3ppl(master): Added Feautrier88.
by Roberto Bagnara 12 Jan '10

12 Jan '10

Module: ppl/w3ppl Branch: master Commit: 00a5a04d1de046b07b157361e74fb3dcc32787a8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=00a5a04d1d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Jan 12 11:18:18 2010 +0100 Added Feautrier88. --- htdocs/Documentation/ppl.bib | 27 +++++++++++++++++++++++++++ 1 files changed, 27 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index f9ebe16..a65f5ad 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -1381,6 +1381,33 @@ Year = 1963 } +@Article{Feautrier88, + Author = "P. Feautrier", + Title = "Parametric Integer Programming", + Journal = "RAIRO Recherche Op\'erationnelle", + Year = 1988, + Volume = 22, + Number = 3, + Pages = "243--268", + Abstract = "When analysing computer programs (especially numerical + programs in which arrays are used extensively), one is + often confronted with integer programming problems. + These problems have three peculiarities: + feasible points are ranked according to lexicographic + order rather than the usual linear economic function; + the feasible set depends on integer parameters; + one is interested only in exact solutions. + The difficulty is somewhat alleviated by the fact that + problems sizes are usually quite small. In this paper we + show that: the classical simplex algorithm has no + difficulty in handling lexicographic ordering; the + algorithm may be executed in symbolic mode, thus giving + the solution of continuous parametric problems; the + method may be extended to problems in integers. We prove + that the resulting algorithm always terminate and give + an estimate of its complexity." +} + @Misc{Fukuda98, Author = "K. Fukuda", Title = "Polyhedral Computation {FAQ}",

1 0

[GIT] ppl/w3ppl(master): Updated BagnaraHZ10FMSD.
by Roberto Bagnara 12 Jan '10

12 Jan '10

Module: ppl/w3ppl Branch: master Commit: c9c0e2d7e7587c39e970e63f0b6e7918dfcd3e15 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=c9c0e2d7e7… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Jan 12 11:03:35 2010 +0100 Updated BagnaraHZ10FMSD. --- htdocs/Documentation/BagnaraHZ10FMSD.pdf | Bin 0 -> 448185 bytes htdocs/Documentation/ppl.bib | 7 ++++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/htdocs/Documentation/BagnaraHZ10FMSD.pdf b/htdocs/Documentation/BagnaraHZ10FMSD.pdf new file mode 100644 index 0000000..21c80da Binary files /dev/null and b/htdocs/Documentation/BagnaraHZ10FMSD.pdf differ diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index cec9899..f9ebe16 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -936,15 +936,15 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf" } -@Article{BagnaraHZ09FMSD, +@Article{BagnaraHZ10FMSD, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness", Journal = "Formal Methods in System Design", Publisher = "Springer-Verlag, Berlin", - Year = 2009, + Year = 2010, Note = "To appear in print. Available online at - \url{http://www.springerlink.com/content/d40842574t1r5877/}", + \url{http://www.springerlink.com/content/100266/?Content+Status=Accepted}", Abstract = "Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal @@ -972,6 +972,7 @@ rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.", + URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ10FMSD.pdf" } @Techreport{BagnaraHZ09TRa,

1 0

[GIT] ppl/ppl(master): Fixed the omissions of ppl_Polyhedron_is_empty/ 1 and ppl_Polyhedron_add_constraints/2.
by Roberto Bagnara 09 Jan '10

09 Jan '10

Module: ppl/ppl Branch: master Commit: 6b04bd57800555128f61996f44fec9b9257dee04 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6b04bd578005… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jan 9 23:28:55 2010 +0100 Fixed the omissions of ppl_Polyhedron_is_empty/1 and ppl_Polyhedron_add_constraints/2. --- interfaces/Prolog/XSB/xsb_clpq.P | 2 ++ interfaces/Prolog/XSB/xsb_clpq2.P | 2 ++ 2 files changed, 4 insertions(+), 0 deletions(-) diff --git a/interfaces/Prolog/XSB/xsb_clpq.P b/interfaces/Prolog/XSB/xsb_clpq.P index f789474..374efe4 100644 --- a/interfaces/Prolog/XSB/xsb_clpq.P +++ b/interfaces/Prolog/XSB/xsb_clpq.P @@ -33,7 +33,9 @@ site: http://www.cs.unipr.it/ppl/ . */ ppl_new_C_Polyhedron_from_C_Polyhedron/2, ppl_new_NNC_Polyhedron_from_NNC_Polyhedron/2, ppl_delete_Polyhedron/1, + ppl_Polyhedron_is_empty/1, ppl_Polyhedron_space_dimension/2, + ppl_Polyhedron_add_constraints/2, ppl_Polyhedron_get_constraints/2, ppl_Polyhedron_add_space_dimensions_and_embed/2, ppl_Polyhedron_remove_higher_space_dimensions/2 diff --git a/interfaces/Prolog/XSB/xsb_clpq2.P b/interfaces/Prolog/XSB/xsb_clpq2.P index 2cc10d9..1f0d045 100644 --- a/interfaces/Prolog/XSB/xsb_clpq2.P +++ b/interfaces/Prolog/XSB/xsb_clpq2.P @@ -33,7 +33,9 @@ site: http://www.cs.unipr.it/ppl/ . */ ppl_new_C_Polyhedron_from_C_Polyhedron/2, ppl_new_NNC_Polyhedron_from_NNC_Polyhedron/2, ppl_delete_Polyhedron/1, + ppl_Polyhedron_is_empty/1, ppl_Polyhedron_space_dimension/2, + ppl_Polyhedron_add_constraints/2, ppl_Polyhedron_get_constraints/2, ppl_Polyhedron_add_space_dimensions_and_embed/2, ppl_Polyhedron_remove_space_dimensions/2,

1 0

[GIT] ppl/ppl(master): Fixed the omission of ppl_set_irrational_precision/ 1 and ppl_irrational_precision/1.
by Roberto Bagnara 09 Jan '10

09 Jan '10

Module: ppl/ppl Branch: master Commit: df9e55f182cd68b1c64a725b0c2eb361bd83ae61 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=df9e55f182cd… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Jan 9 23:25:06 2010 +0100 Fixed the omission of ppl_set_irrational_precision/1 and ppl_irrational_precision/1. --- interfaces/Prolog/XSB/xsb_pl_check.P | 2 ++ 1 files changed, 2 insertions(+), 0 deletions(-) diff --git a/interfaces/Prolog/XSB/xsb_pl_check.P b/interfaces/Prolog/XSB/xsb_pl_check.P index 56b3fa8..4ae27e9 100644 --- a/interfaces/Prolog/XSB/xsb_pl_check.P +++ b/interfaces/Prolog/XSB/xsb_pl_check.P @@ -38,6 +38,8 @@ site: http://www.cs.unipr.it/ppl/ . */ ppl_Coefficient_min/1, ppl_initialize/0, ppl_finalize/0, + ppl_set_irrational_precision/1, + ppl_irrational_precision/1, ppl_set_timeout_exception_atom/1, ppl_timeout_exception_atom/1, ppl_set_timeout/1,

1 0