April 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Worked around a Doxygen bug.
by Roberto Bagnara 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: master Commit: a1a314d3c059b87a8f3bd55c87820cf057b7bbd6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a1a314d3c059… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 11 09:06:13 2010 +0200 Worked around a Doxygen bug. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index f2aa097..ae0562f 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2939,7 +2939,7 @@ C. Ancourt. <DT>[BA05]</DT> <DD> \anchor BA05 -J. M. Bjørndalen and O. Anshus. +J. M. Bjorndalen and O. Anshus. Lessons learned in benchmarking - Floating point benchmarks: Can you trust them? In Proceedings of the Norsk informatikkonferanse 2005

1 0

[GIT] ppl/ppl(master): Cite BMPZ10.
by Roberto Bagnara 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: master Commit: 2658694de46816cb65663f73befc43574f0c86ec URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2658694de468… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 11 08:59:57 2010 +0200 Cite BMPZ10. --- src/termination.defs.hh | 30 ++++++++++++++++-------------- 1 files changed, 16 insertions(+), 14 deletions(-) diff --git a/src/termination.defs.hh b/src/termination.defs.hh index 60ccf66..8ccfc41 100644 --- a/src/termination.defs.hh +++ b/src/termination.defs.hh @@ -30,7 +30,7 @@ namespace Parma_Polyhedra_Library { /*! \brief Termination test using an improvement of the method by Mesnard and - Serebrenik. + Serebrenik \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -63,7 +63,7 @@ termination_test_MS(const PSET& pset); /*! \brief Termination test using an improvement of the method by Mesnard and - Serebrenik. + Serebrenik \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -105,7 +105,7 @@ termination_test_MS_2(const PSET& pset_before, const PSET& pset_after); /*! \brief Termination test with witness ranking function using an improvement - of the method by Mesnard and Serebrenik. + of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -147,7 +147,7 @@ one_affine_ranking_function_MS(const PSET& pset, Generator& mu); /*! \brief Termination test with witness ranking function using an improvement - of the method by Mesnard and Serebrenik. + of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -200,7 +200,7 @@ one_affine_ranking_function_MS_2(const PSET& pset_before, /*! \brief Termination test with ranking function space using an improvement - of the method by Mesnard and Serebrenik. + of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -242,7 +242,7 @@ all_affine_ranking_functions_MS(const PSET& pset, C_Polyhedron& mu_space); /*! \brief Termination test with ranking function space using an improvement - of the method by Mesnard and Serebrenik. + of the method by Mesnard and Serebrenik \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -295,7 +295,8 @@ all_affine_ranking_functions_MS_2(const PSET& pset_before, /*! \brief Computes the spaces of affine \e quasi ranking functions - using an improvement of the method by Mesnard and Serebrenik. + using an improvement of the method by Mesnard and Serebrenik + \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -346,7 +347,8 @@ all_affine_quasi_ranking_functions_MS(const PSET& pset, /*! \brief Computes the spaces of affine \e quasi ranking functions - using an improvement of the method by Mesnard and Serebrenik. + using an improvement of the method by Mesnard and Serebrenik + \ref BMPZ10 "[BMPZ10]". \tparam PSET Any pointset supported by the PPL that provides the @@ -407,7 +409,7 @@ all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before, /*! \brief Like termination_test_MS() but using an improvement - of the method by Podelski and Rybalchenko. + of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool @@ -415,7 +417,7 @@ termination_test_PR(const PSET& pset); /*! \brief Like termination_test_MS_2() but using an improvement - of the method by Podelski and Rybalchenko. + of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool @@ -423,7 +425,7 @@ termination_test_PR_2(const PSET& pset_before, const PSET& pset_after); /*! \brief Like one_affine_ranking_function_MS() but using an improvement - of the method by Podelski and Rybalchenko. + of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool @@ -431,7 +433,7 @@ one_affine_ranking_function_PR(const PSET& pset, Generator& mu); /*! \brief Like one_affine_ranking_function_MS_2() but using an improvement - of the method by Podelski and Rybalchenko. + of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool @@ -441,7 +443,7 @@ one_affine_ranking_function_PR_2(const PSET& pset_before, /*! \brief Like all_affine_ranking_functions_MS() but using an improvement - of the method by Podelski and Rybalchenko. + of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> void @@ -449,7 +451,7 @@ all_affine_ranking_functions_PR(const PSET& pset, NNC_Polyhedron& mu_space); /*! \brief Like all_affine_ranking_functions_MS_2() but using an improvement - of the method by Podelski and Rybalchenko. + of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> void

1 0

[GIT] ppl/ppl(master): Bibliography updated.
by Roberto Bagnara 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: master Commit: ac22982884b25962ce390fe6a6f043fc3352a765 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ac22982884b2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 11 08:45:38 2010 +0200 Bibliography updated. --- doc/definitions.dox | 105 ++++++++++++++++++++++++++++++++++++++++++++------- 1 files changed, 91 insertions(+), 14 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 6e9ec24..f2aa097 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2939,7 +2939,7 @@ C. Ancourt. <DT>[BA05]</DT> <DD> \anchor BA05 -J. M. Bjorndalen and O. Anshus. +J. M. Bjørndalen and O. Anshus. Lessons learned in benchmarking - Floating point benchmarks: Can you trust them? In Proceedings of the Norsk informatikkonferanse 2005 @@ -2980,7 +2980,7 @@ B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborg D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. - In T. AE. Mogensen, D. A. Schmidt, and I. Hal Sudborough, + In T. Æ. Mogensen, D. A. Schmidt, and I. Hal Sudborough, editors, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday], volume 2566 of Lecture Notes in Computer Science, pages @@ -3333,8 +3333,7 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. R. Bagnara, P. M. Hill, and E. Zaffanella. Applications of polyhedral computations to the analysis and verification of hardware and software systems. - Theoretical Computer Science, 2009. - To appear. + Theoretical Computer Science, 410(46):4672-4691, 2009. </DD> @@ -3348,9 +3347,10 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. abstractions. Quaderno 492, Dipartimento di Matematica, Università di Parma, Italy, 2009. - Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. Also - published as <tt>arXiv:cs.CG/0904.1783</tt>, available from - <a href="http://arxiv.org/">http://arxiv.org/</a>. + Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. A corrected + and improved version (corrected an error in the statement of condition (3) of + Theorem 3.6, typos corrected in statement and proof of Theorem 6.8) has been + published in \ref BHZ09c "[BHZ09c]". </DD> @@ -3360,9 +3360,39 @@ R. Bagnara, P. M. Hill, and E. Zaffanella. <DD> \anchor BHZ09c R. Bagnara, P. M. Hill, and E. Zaffanella. + Exact join detection for convex polyhedra and other numerical + abstractions. + Report <tt>arXiv:cs.CG/0904.1783</tt>, 2009. + Available at <a href="http://arxiv.org/">http://arxiv.org/</a> and + <a href="http://www.cs.unipr.it/ppl/">http://www.cs.unipr.it/ppl/</a>. + + +</DD> + + +<DT>[BHZ09d]</DT> +<DD> +\anchor BHZ09d +R. Bagnara, P. M. Hill, and E. Zaffanella. Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. - Submitted for publication, 2009. + Formal Methods in System Design, 35(3):279-323, 2009. + + +</DD> + + +<DT>[BHZ10]</DT> +<DD> +\anchor BHZ10 +R. Bagnara, P. M. Hill, and E. Zaffanella. + Exact join detection for convex polyhedra and other numerical + abstractions. + Computational Geometry: Theory and Applications, + 43(5):453-473, 2010. + To appear in print. Available online at + <a href="http://dx.doi.org/10.1016/j.comgeo.2009.09.002">http://dx.doi.org/10.1016/j.comgeo.2009.09.002</a>. + </DD> @@ -3394,6 +3424,21 @@ V. Balasundaram and K. Kennedy. </DD> +<DT>[BMPZ10]</DT> +<DD> +\anchor BMPZ10 +R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. + The automatic synthesis of linear ranking functions: The complete + unabridged version. + Quaderno 498, Dipartimento di Matematica, Università di Parma, + Italy, 2010. + Available at <a href="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</a>. Also + published as <tt>arXiv:cs.PL/1004.0944</tt>, available from + <a href="http://arxiv.org/">http://arxiv.org/</a>. + +</DD> + + <DT>[BRZH02a]</DT> <DD> \anchor BRZH02a @@ -3535,6 +3580,27 @@ G. B. Dantzig. </DD> +<DT>[FCB07]</DT> +<DD> +\anchor FCB07 +P. Feautrier, J.-F. Collard, and C. Bastoul. + PIP/PipLib: A Solver for Parametric Integer Programming + Problems, 5.0 edition, July 2007. + Distributed with PIP/PipLib 1.4.0. + +</DD> + + +<DT>[Fea88]</DT> +<DD> +\anchor Fea88 +P. Feautrier. + Parametric integer programming. + RAIRO Recherche Opérationnelle, 22(3):243-268, 1988. + +</DD> + + <DT>[FP96]</DT> <DD> \anchor FP96 @@ -3655,8 +3721,8 @@ N. Halbwachs. N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, Computer Aided Verification: - Proceedings of the 5th International Conference, volume 697 of Lecture - Notes in Computer Science, pages 333-346, Elounda, Greece, 1993. + Proceedings of the 5th International Conference (CAV'93), volume 697 of + Lecture Notes in Computer Science, pages 333-346, Elounda, Greece, 1993. Springer-Verlag, Berlin. </DD> @@ -3799,9 +3865,9 @@ H. W. Kuhn. </DD> -<DT>[LeV92]</DT> +<DT>[Le 92]</DT> <DD> -\anchor LeV92 +\anchor Le 92 H. Le Verge. A note on Chernikova's algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, @@ -4128,9 +4194,9 @@ D. Srivastava. </DD> -<DT>[SS07]</DT> +<DT>[SS07a]</DT> <DD> -\anchor SS07 +\anchor SS07a R. Sen and Y. N. Srikant. Executable analysis using abstract interpretation with circular linear progressions. @@ -4141,6 +4207,17 @@ R. Sen and Y. N. Srikant. </DD> +<DT>[SS07b]</DT> +<DD> +\anchor SS07b +R. Sen and Y. N. Srikant. + Executable analysis with circular linear progressions. + Technical Report IISc-CSA-TR-2007-3, Department of Computer Science + and Automation, Indian Institute of Science, Bangalore, India, 2007. + +</DD> + + <DT>[SW70]</DT> <DD> \anchor SW70

1 0

[GIT] ppl/ppl(master): Added drop_some_non_integer_points( const Variables_Set& vars,
by Patricia Hill 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: master Commit: b42b6e35ad512a633e2991d633bc95d28af1d9bf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b42b6e35ad51… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Sat Apr 10 20:39:11 2010 +0100 Added drop_some_non_integer_points(const Variables_Set& vars, Complexity_Class complexity = ANY_COMPLEXITY) --- ...erface_generator_common_procedure_generators.m4 | 4 +- src/Partially_Reduced_Product.defs.hh | 19 +++++++++++ src/Partially_Reduced_Product.inlines.hh | 11 ++++++ .../dropsomenonintegerpoints1.cc | 35 ++++++++++++++++++++ 4 files changed, 67 insertions(+), 2 deletions(-) diff --git a/interfaces/ppl_interface_generator_common_procedure_generators.m4 b/interfaces/ppl_interface_generator_common_procedure_generators.m4 index e93d96b..ff0dda7 100644 --- a/interfaces/ppl_interface_generator_common_procedure_generators.m4 +++ b/interfaces/ppl_interface_generator_common_procedure_generators.m4 @@ -90,8 +90,8 @@ ppl_@CLASS@_remove_higher_space_dimensions/2 *nofail +all, ppl_@CLASS@_expand_space_dimension/3 *nofail +all, ppl_@CLASS@_fold_space_dimensions/3 +all, ppl_@CLASS@_map_space_dimensions/2 +all, -ppl_@CLASS@_drop_some_non_integer_points/2 +simple, -ppl_@CLASS@_drop_some_non_integer_points_2/3 +simple, +ppl_@CLASS@_drop_some_non_integer_points/2 +all, +ppl_@CLASS@_drop_some_non_integer_points_2/3 +all, ppl_@CLASS@_ascii_dump/1 +all, ppl_@CLASS@_@MEMBYTES@/2 +all, dnl diff --git a/src/Partially_Reduced_Product.defs.hh b/src/Partially_Reduced_Product.defs.hh index bb6079f..7e2a97b 100644 --- a/src/Partially_Reduced_Product.defs.hh +++ b/src/Partially_Reduced_Product.defs.hh @@ -1371,6 +1371,25 @@ public: void drop_some_non_integer_points(Complexity_Class complexity = ANY_COMPLEXITY); + /*! \brief + Possibly tightens \p *this by dropping some points with non-integer + coordinates for the space dimensions corresponding to \p vars. + + \param vars + Points with non-integer coordinates for these variables/space-dimensions + can be discarded. + + \param complexity + The maximal complexity of any algorithms used. + + \note + Currently there is no optimality guarantee, not even if + \p complexity is <CODE>ANY_COMPLEXITY</CODE>. + */ + void drop_some_non_integer_points(const Variables_Set& vars, + Complexity_Class complexity + = ANY_COMPLEXITY); + //@} // Space Dimension Preserving Member Functions that May Modify [...] //! \name Member Functions that May Modify the Dimension of the Vector Space diff --git a/src/Partially_Reduced_Product.inlines.hh b/src/Partially_Reduced_Product.inlines.hh index eacbddd..a4c0929 100644 --- a/src/Partially_Reduced_Product.inlines.hh +++ b/src/Partially_Reduced_Product.inlines.hh @@ -454,6 +454,17 @@ Partially_Reduced_Product<D1, D2, R> } template <typename D1, typename D2, typename R> +inline void +Partially_Reduced_Product<D1, D2, R> +::drop_some_non_integer_points(const Variables_Set& vars, + Complexity_Class complexity) { + reduce(); + d1.drop_some_non_integer_points(vars, complexity); + d2.drop_some_non_integer_points(vars, complexity); + clear_reduced_flag(); +} + +template <typename D1, typename D2, typename R> inline Partially_Reduced_Product<D1, D2, R>& Partially_Reduced_Product<D1, D2, R> ::operator=(const Partially_Reduced_Product& y) { diff --git a/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc b/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc index 729e682..3b9cf0c 100644 --- a/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc +++ b/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc @@ -88,9 +88,44 @@ test02() { return ok; } +// drop_some_non_integer_points(vars, ANY_COMPLEXITY) +bool +test03() { + Variable A(0); + Variable B(1); + Variable C(2); + + Variables_Set vars; + vars.insert(A); + + Product prp1(3); + prp1.refine_with_constraint(A >= 0); + prp1.refine_with_constraint(B >= 0); + prp1.refine_with_constraint(A + B >= 3); + prp1.refine_with_constraint(2*A - B == 0); + prp1.refine_with_constraint(3*A + C == 0); + prp1.refine_with_congruence(3*A %= 0); + + prp1.drop_some_non_integer_points(vars, ANY_COMPLEXITY); + + Product known_prp(3); + known_prp.refine_with_constraint(3*A + C == 0); + known_prp.refine_with_constraint(2*A - B == 0); + known_prp.refine_with_constraint(A >= 1); + known_prp.refine_with_congruence(A %= 0); + + bool ok = (prp1 == known_prp); + + print_congruences(prp1, "*** prp1.time_elapse_assign(prp1) congruences ***"); + print_constraints(prp1, "*** prp1.time_elapse_assign(prp1) constraints ***"); + + return ok; +} + } // namespace BEGIN_MAIN DO_TEST_F8(test01); DO_TEST(test02); + DO_TEST_F8(test03); END_MAIN

1 0

[GIT] ppl/ppl(master): Added drop_some_non_integer_points() to the product domain
by Patricia Hill 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: master Commit: cb5a410c4e262c28b62c1c07d72ef0d99358688e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cb5a410c4e26… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Sat Apr 10 20:23:19 2010 +0100 Added drop_some_non_integer_points() to the product domain --- src/Partially_Reduced_Product.defs.hh | 14 +++ src/Partially_Reduced_Product.inlines.hh | 10 ++ tests/Partially_Reduced_Product/Makefile.am | 3 + .../dropsomenonintegerpoints1.cc | 96 ++++++++++++++++++++ 4 files changed, 123 insertions(+), 0 deletions(-) diff --git a/src/Partially_Reduced_Product.defs.hh b/src/Partially_Reduced_Product.defs.hh index 1116633..bb6079f 100644 --- a/src/Partially_Reduced_Product.defs.hh +++ b/src/Partially_Reduced_Product.defs.hh @@ -1357,6 +1357,20 @@ public: void widening_assign(const Partially_Reduced_Product& y, unsigned* tp = NULL); + /*! \brief + Possibly tightens \p *this by dropping some points with non-integer + coordinates. + + \param complexity + The maximal complexity of any algorithms used. + + \note + Currently there is no optimality guarantee, not even if + \p complexity is <CODE>ANY_COMPLEXITY</CODE>. + */ + void drop_some_non_integer_points(Complexity_Class complexity + = ANY_COMPLEXITY); + //@} // Space Dimension Preserving Member Functions that May Modify [...] //! \name Member Functions that May Modify the Dimension of the Vector Space diff --git a/src/Partially_Reduced_Product.inlines.hh b/src/Partially_Reduced_Product.inlines.hh index 88f921f..eacbddd 100644 --- a/src/Partially_Reduced_Product.inlines.hh +++ b/src/Partially_Reduced_Product.inlines.hh @@ -444,6 +444,16 @@ Partially_Reduced_Product<D1, D2, R> } template <typename D1, typename D2, typename R> +inline void +Partially_Reduced_Product<D1, D2, R> +::drop_some_non_integer_points(Complexity_Class complexity) { + reduce(); + d1.drop_some_non_integer_points(complexity); + d2.drop_some_non_integer_points(complexity); + clear_reduced_flag(); +} + +template <typename D1, typename D2, typename R> inline Partially_Reduced_Product<D1, D2, R>& Partially_Reduced_Product<D1, D2, R> ::operator=(const Partially_Reduced_Product& y) { diff --git a/tests/Partially_Reduced_Product/Makefile.am b/tests/Partially_Reduced_Product/Makefile.am index 4bf657d..16db2be 100644 --- a/tests/Partially_Reduced_Product/Makefile.am +++ b/tests/Partially_Reduced_Product/Makefile.am @@ -71,6 +71,7 @@ dimension1 \ directproduct1 \ discrete1 \ disjoint1 \ +dropsomenonintegerpoints1 \ equals1 \ frombdshape1 \ frombox1 \ @@ -146,6 +147,8 @@ discrete1_SOURCES = discrete1.cc disjoint1_SOURCES = disjoint1.cc +dropsomenonintegerpoints1_SOURCES = dropsomenonintegerpoints1.cc + equals1_SOURCES = equals1.cc frombdshape1_SOURCES = frombdshape1.cc diff --git a/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc b/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc new file mode 100644 index 0000000..729e682 --- /dev/null +++ b/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc @@ -0,0 +1,96 @@ +/* Test Product<NNC_Polyhedron, Grid>::drop_some_non_integer_points(). + Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" +#include "partially_reduced_product_test.hh" + +typedef NNC_Polyhedron DOMAIN1; +typedef Grid DOMAIN2; +typedef Domain_Product<DOMAIN1x, DOMAIN2x>::Constraints_Product Product; + +namespace { + +// drop_some_non_integer_points(ANY_COMPLEXITY) +bool +test01() { + Variable A(0); + Variable B(1); + Variable C(2); + + Product prp1(3); + prp1.refine_with_constraint(A >= 0); + prp1.refine_with_constraint(B >= 0); + prp1.refine_with_constraint(A + B >= 3); + prp1.refine_with_constraint(2*A - B == 0); + prp1.refine_with_constraint(3*A + C == 0); + prp1.refine_with_congruence(3*A %= 0); + + prp1.drop_some_non_integer_points(ANY_COMPLEXITY); + + Product known_prp(3); + known_prp.refine_with_constraint(3*A + C == 0); + known_prp.refine_with_constraint(2*A - B == 0); + known_prp.refine_with_constraint(A >= 1); + known_prp.refine_with_congruence(A %= 0); + + bool ok = (prp1 == known_prp); + + print_congruences(prp1, "*** prp1.time_elapse_assign(prp1) congruences ***"); + print_constraints(prp1, "*** prp1.time_elapse_assign(prp1) constraints ***"); + + return ok; +} + +// drop_some_non_integer_points(ANY_COMPLEXITY) +// where the initial products are not reduced +// and the second product has non-intersecting single point components. +bool +test02() { + Variable A(0); + + + Product prp1(1); + + print_congruences(prp1, "*** prp1 congruences ***"); + print_constraints(prp1, "*** prp1 constraints ***"); + + prp1.drop_some_non_integer_points(ANY_COMPLEXITY); + + Product known_prp(1); + known_prp.refine_with_congruence(A %= 0); + + bool ok = prp1.OK() && (prp1 == known_prp); + + print_congruences(prp1, + "*** prp1.drop_some_non_integer_points(ANY_COMPLEXITY) congruences ***"); + print_constraints(prp1, + "*** prp1.drop_some_non_integer_points(ANY_COMPLEXITY) constraints ***"); + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST_F8(test01); + DO_TEST(test02); +END_MAIN

1 0

[GIT] ppl/ppl(master): Trailing whitespace removed.
by Roberto Bagnara 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: master Commit: 5ba66813973abcc3764971b3def20dcb33cc5b71 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5ba66813973a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 10 18:23:12 2010 +0200 Trailing whitespace removed. --- src/Float.inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh index 946a1cf..16e0f21 100644 --- a/src/Float.inlines.hh +++ b/src/Float.inlines.hh @@ -26,7 +26,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include <climits> namespace Parma_Polyhedra_Library { - + inline int float_ieee754_half::is_inf() const { if (word == NEG_INF)

1 0

[GIT] ppl/ppl(master): Variable hiding avoided.
by Roberto Bagnara 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: master Commit: d8126fc4ec706e7c25100b1f3c51d0decaff7c55 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d8126fc4ec70… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 10 18:23:01 2010 +0200 Variable hiding avoided. --- src/Polyhedron_nonpublic.cc | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc index 20049a6..b3ae9ef 100644 --- a/src/Polyhedron_nonpublic.cc +++ b/src/Polyhedron_nonpublic.cc @@ -2184,9 +2184,9 @@ PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars, } // Divide the inhomogeneous coefficients by the GCD. - for (dimension_type i = space_dim+1; --i > 0; ) { - Coefficient& c_i = c[i]; - exact_div_assign(c_i, c_i, gcd); + for (dimension_type k = space_dim+1; --k > 0; ) { + Coefficient& c_k = c[k]; + exact_div_assign(c_k, c_k, gcd); } Coefficient& c_0 = c[0]; const int c_0_sign = sgn(c_0);

1 0

[GIT] ppl/ppl(master): Added a point about the new drop_some_non_integer_points() methods.
by Roberto Bagnara 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: master Commit: b18b92fc50ddb62887f6d42a4d87f74a7fe0f452 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b18b92fc50dd… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 10 12:16:46 2010 +0200 Added a point about the new drop_some_non_integer_points() methods. --- NEWS | 10 ++++++++++ 1 files changed, 10 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index 88347c0..0ed5d9e 100644 --- a/NEWS +++ b/NEWS @@ -23,6 +23,16 @@ o New "deterministic" timeout computation facilities: it is now possible from the actual computation environment (CPU, operating system, etc.). Still under beta testing. +o All the PPL semantic objects provide new methods + + void drop_some_non_integer_points(Complexity_Class) + void drop_some_non_integer_points(const Variables_Set&, + Complexity_Class) + + which possibly tighten the object by dropping some points with + non-integer coordinates (for the space dimensions corresponding to + `vars'), within a certain computational complexity bound. + o New Linear_Expression methods bool is_zero() const

1 0

[GIT] ppl/ppl(sparse_matrices): Renamed Unlimited_Sparse_Row into Unlimited_Sparse_Row_Over_Linear_Sequence . Now Unlimited_Sparse_Row is a typedef, that depends on the selected compile option.
by Marco Poletti 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 349fc7a1d8c56d0dabb01444fe6cf66a844a43b9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=349fc7a1d8c5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Apr 10 18:08:05 2010 +0200 Renamed Unlimited_Sparse_Row into Unlimited_Sparse_Row_Over_Linear_Sequence. Now Unlimited_Sparse_Row is a typedef, that depends on the selected compile option. --- src/CO_Tree.cc | 16 +- src/CO_Tree.defs.hh | 7 + src/CO_Tree.inlines.hh | 5 + src/Makefile.am | 16 +- src/Unlimited_Sparse_Row.defs.hh | 520 +------------------- src/Unlimited_Sparse_Row.types.hh | 13 +- src/Unlimited_Sparse_Row_CO_Tree_Backend.defs.hh | 246 --------- ...Unlimited_Sparse_Row_CO_Tree_Backend.inlines.hh | 188 ------- ...end.cc => Unlimited_Sparse_Row_Over_CO_Tree.cc} | 4 +- src/Unlimited_Sparse_Row_Over_CO_Tree.defs.hh | 390 ++++++++++++++ src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh | 452 ++++++++++++++++ ... => Unlimited_Sparse_Row_Over_CO_Tree.types.hh} | 8 +- ...> Unlimited_Sparse_Row_Over_Linear_Sequence.cc} | 31 +- ...limited_Sparse_Row_Over_Linear_Sequence.defs.hh | 545 ++++++++++++++++++++ ...ted_Sparse_Row_Over_Linear_Sequence.inlines.hh} | 193 ++++---- ...d_Sparse_Row_Over_Linear_Sequence.templates.hh} | 35 +- ...mited_Sparse_Row_Over_Linear_Sequence.types.hh} | 8 +- 17 files changed, 1589 insertions(+), 1088 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=349fc7a1…

1 0

[GIT] ppl/ppl(sparse_matrices): Add new classes: CO_Tree and Unlimited_Sparse_Row_CO_Tree_backend. Add tests for CO_Tree. Avoid conditional inclusion of headers.
by Marco Poletti 10 Apr '10

10 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 7b92c7d8d25de211bf34e02816a2f8fdd475ebf2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7b92c7d8d25d… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Apr 10 15:03:04 2010 +0200 Add new classes: CO_Tree and Unlimited_Sparse_Row_CO_Tree_backend. Add tests for CO_Tree. Avoid conditional inclusion of headers. --- configure.ac | 1 + src/CO_Tree.cc | 762 +++++ src/CO_Tree.defs.hh | 449 +++ src/CO_Tree.inlines.hh | 825 +++++ src/CO_Tree.types.hh | 21 + src/Dense_Row.inlines.hh | 12 + src/MIP_Problem.defs.hh | 7 - src/Makefile.am | 10 + src/PIP_Problem.defs.hh | 8 +- src/Unlimited_Sparse_Row.defs.hh | 24 +- src/Unlimited_Sparse_Row_CO_Tree_Backend.cc | 29 + src/Unlimited_Sparse_Row_CO_Tree_Backend.defs.hh | 246 ++ ...Unlimited_Sparse_Row_CO_Tree_Backend.inlines.hh | 188 ++ src/Unlimited_Sparse_Row_CO_Tree_Backend.types.hh | 21 + tests/CO_Tree/.gitignore | 1 + tests/CO_Tree/Makefile.am | 77 + tests/CO_Tree/cotree1.cc | 3215 ++++++++++++++++++++ tests/Makefile.am | 1 + 18 files changed, 5881 insertions(+), 16 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=7b92c7d8…

1 0