- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Added static method Coefficient.ppl_bits() to Java interface.
by Enea Zaffanella 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: master Commit: 96df33856cdb2d98f0117f8dc99c12dacb922a03 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=96df33856cdb… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Apr 11 16:17:44 2010 +0200 Added static method Coefficient.ppl_bits() to Java interface. test04 in PIP_Problem_test1.java overflows when using 8-bit checked integers. Fixed method PIP_TREE_Node.toString(). --- interfaces/Java/jni/ppl_java_globals.cc | 16 ++++++++++++++++ .../Java/parma_polyhedra_library/Coefficient.java | 3 +++ .../parma_polyhedra_library/PIP_Tree_Node.java | 3 +++ .../Parma_Polyhedra_Library.java | 4 ---- interfaces/Java/tests/PIP_Problem_test1.java | 18 ++++++++++++++++++ 5 files changed, 40 insertions(+), 4 deletions(-) diff --git a/interfaces/Java/jni/ppl_java_globals.cc b/interfaces/Java/jni/ppl_java_globals.cc index 8b28785..467ac21 100644 --- a/interfaces/Java/jni/ppl_java_globals.cc +++ b/interfaces/Java/jni/ppl_java_globals.cc @@ -96,6 +96,11 @@ Java_parma_1polyhedra_1library_By_1Reference_initIDs cached_FMIDs.By_Reference_init_ID = mID; } +JNIEXPORT jint JNICALL +Java_parma_1polyhedra_1library_Coefficient_ppl_1bits(JNIEnv*, jclass) { + return PPL_COEFFICIENT_BITS; +} + JNIEXPORT void JNICALL Java_parma_1polyhedra_1library_Coefficient_initIDs (JNIEnv* env, jclass j_coeff_class) { @@ -2010,6 +2015,17 @@ Java_parma_1polyhedra_1library_PIP_1Tree_1Node_artificials return null; } +JNIEXPORT jstring JNICALL +Java_parma_1polyhedra_1library_PIP_1Tree_1Node_toString +(JNIEnv* env, jobject j_this) { + PIP_Tree_Node* this_ptr + = reinterpret_cast<PIP_Tree_Node*>(get_ptr(env, j_this)); + using namespace Parma_Polyhedra_Library::IO_Operators; + std::ostringstream s; + s << *this_ptr; + return env->NewStringUTF(s.str().c_str()); +} + JNIEXPORT jobject JNICALL Java_parma_1polyhedra_1library_PIP_1Decision_1Node_child_1node (JNIEnv* env, jobject j_this, jboolean j_branch) { diff --git a/interfaces/Java/parma_polyhedra_library/Coefficient.java b/interfaces/Java/parma_polyhedra_library/Coefficient.java index 61aaf0f..4b89bcb 100644 --- a/interfaces/Java/parma_polyhedra_library/Coefficient.java +++ b/interfaces/Java/parma_polyhedra_library/Coefficient.java @@ -74,6 +74,9 @@ public class Coefficient { return value; } + //! Returns the number of bits of PPL coefficients; 0 if unbounded. + public static native int ppl_bits(); + private static native void initIDs(); static { initIDs(); diff --git a/interfaces/Java/parma_polyhedra_library/PIP_Tree_Node.java b/interfaces/Java/parma_polyhedra_library/PIP_Tree_Node.java index e332188..433c442 100644 --- a/interfaces/Java/parma_polyhedra_library/PIP_Tree_Node.java +++ b/interfaces/Java/parma_polyhedra_library/PIP_Tree_Node.java @@ -75,4 +75,7 @@ public class PIP_Tree_Node extends PPL_Object { */ public native Constraint_System constraints(); + //! Returns a string representation of \p this. + public native String toString(); + } diff --git a/interfaces/Java/parma_polyhedra_library/Parma_Polyhedra_Library.java b/interfaces/Java/parma_polyhedra_library/Parma_Polyhedra_Library.java index 9c99cc1..e1738da 100644 --- a/interfaces/Java/parma_polyhedra_library/Parma_Polyhedra_Library.java +++ b/interfaces/Java/parma_polyhedra_library/Parma_Polyhedra_Library.java @@ -190,10 +190,6 @@ public class Parma_Polyhedra_Library { information. */ public static native String banner(); -/* - public static native boolean - ppl_Termination_MS(C_Polyhedron p); -*/ //@} // Version Checking diff --git a/interfaces/Java/tests/PIP_Problem_test1.java b/interfaces/Java/tests/PIP_Problem_test1.java index d36b8e7..1140207 100644 --- a/interfaces/Java/tests/PIP_Problem_test1.java +++ b/interfaces/Java/tests/PIP_Problem_test1.java @@ -356,6 +356,19 @@ static { cs.add(c_4); PIP_Problem pip = new PIP_Problem(4, cs, params); + + // Known to overflow if PPL uses 8-bits checked integers. + try { + pip.solve(); + } + catch (Overflow_Error_Exception ex) { + if (Coefficient.ppl_bits() != 8) + throw ex; + PPL_Test.println_if_noisy("Expected overflow exception caught:"); + PPL_Test.println_if_noisy(ex.getMessage()); + return true; + } + PIP_Problem_Status pip_status = pip.solve(); boolean ok = (pip_status == PIP_Problem_Status.OPTIMIZED_PIP_PROBLEM); if (!ok) @@ -365,6 +378,11 @@ static { if (!ok) return false; + PPL_Test.println_if_noisy(); + PPL_Test.println_if_noisy("Testing toString():"); + PPL_Test.println_if_noisy(solution.toString()); + PPL_Test.println_if_noisy(); + PIP_Decision_Node root = solution.as_decision(); if (root == null || !root.OK()) return false;

1 0

[GIT] ppl/ppl(master): test01() and test03() always succeed.
by Roberto Bagnara 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: master Commit: 694281b3a925b0b710e97c5cec77242962f17f37 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=694281b3a925… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 11 09:49:50 2010 +0200 test01() and test03() always succeed. --- .../dropsomenonintegerpoints1.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc b/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc index 3b9cf0c..0988001 100644 --- a/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc +++ b/tests/Partially_Reduced_Product/dropsomenonintegerpoints1.cc @@ -125,7 +125,7 @@ test03() { } // namespace BEGIN_MAIN - DO_TEST_F8(test01); + DO_TEST(test01); DO_TEST(test02); - DO_TEST_F8(test03); + DO_TEST(test03); END_MAIN

1 0

[GIT] ppl/ppl(master): Added an entry for the new functionality concerning the synthesis of linear (quasi-) ranking functions.
by Roberto Bagnara 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: master Commit: f6bc3b69e7f30d3993b5292c14d3091891fc4f3a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6bc3b69e7f3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Apr 11 09:25:47 2010 +0200 Added an entry for the new functionality concerning the synthesis of linear (quasi-) ranking functions. --- NEWS | 24 ++++++++++++++++-------- 1 files changed, 16 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 0ed5d9e..0dfcdf6 100644 --- a/NEWS +++ b/NEWS @@ -14,14 +14,22 @@ o New class PIP_Problem provides a Parametric Integer Programming (PIP) problem solver (mainly based on P. Feautrier's specification). The implementation combines a parametric dual simplex algorithm using exact arithmetic with Gomory's cut - generation. - Still under beta testing. - -o New "deterministic" timeout computation facilities: it is now possible - to set computational bounds (on the library calls taking exponential time) - that do not depend on the actual elapsed time and hence are independent - from the actual computation environment (CPU, operating system, etc.). - Still under beta testing. + generation. Still under beta testing. + +o New "deterministic" timeout computation facilities: it is now + possible to set computational bounds (on the library calls taking + exponential time) that do not depend on the actual elapsed time and + hence are independent from the actual computation environment (CPU, + operating system, etc.). Still under beta testing. + +o New support for termination analysis via the automatic synthesis of + linear ranking functions. Given a sound approximation of a loop, + the PPL provides methods to decide whether that approximation + admits a linear ranking function (possibly obtaining one as a + witness for termination) and to compute the space of all such + functions. In addition, methods are provided to obtain the space + of all linear quasi-ranking functions, for use in conditional + termination analysis. Still under beta testing. o All the PPL semantic objects provide new methods

1 0

[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