November 2016 - PPL-devel - BUGSENG Mailman

Rational polyhedra
by Stefan Schupp 24 Nov '16

24 Nov '16

Hi, I am using PPL for my project which is related to verification. In this context I require my computations to be exact or, if that is not possible, to be over-approximating. From what I read in the documentation, PPL ensures such an over-approximation, which is nice. I am using C_Polyhedron as my data type and currently interested in using rational arithmetic (mpq_class) in combination with that. From what I see, you can use the mpz_class type for C_Polyhedron, but not mpq_class directly. Is there a way intended to overcome this problem? In my current setup I use the double interface, but this requires conversion and most probably introduces rounding errors. Furthermore a usage question: Is there an intended way on how to compute a linear transformation of a polyhedron with a matrix? Best regards, Stefan -- Stefan Schupp M.Sc. RWTH Aachen University Computer Science Department, Informatik 2 D-52056 Aachen, Germany http://ths.rwth-aachen.de/people/stefan-schupp/ Tel.: +49 241 80 21244

2 5

[GIT] ppl/ppl(devel): Tests renamed.
by Enea Zaffanella 06 Nov '16

06 Nov '16

Module: ppl/ppl Branch: devel Commit: 90b459f699f8cc7f5d341aeb1b938e4c7cb6a551 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90b459f699f8… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Nov 6 16:17:53 2016 +0100 Tests renamed. --- tests/Polyhedron/mapspacedims1.cc | 24 ++++++++++++------------ 1 files changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/Polyhedron/mapspacedims1.cc b/tests/Polyhedron/mapspacedims1.cc index 129b4ad..86ab9fe 100644 --- a/tests/Polyhedron/mapspacedims1.cc +++ b/tests/Polyhedron/mapspacedims1.cc @@ -137,7 +137,7 @@ test04() { } bool -test06() { +test05() { Variable A(0); Variable B(1); @@ -167,7 +167,7 @@ test06() { } bool -test09() { +test06() { Partial_Function function; function.insert(0, 1); function.insert(1, 0); @@ -189,7 +189,7 @@ test09() { } bool -test10() { +test07() { Variable x(0); Variable y(1); Variable z(2); @@ -259,7 +259,7 @@ test10() { } bool -test11() { +test08() { Variable A(0); Variable B(1); Variable C(2); @@ -292,7 +292,7 @@ test11() { } bool -test12() { +test09() { Variable A(0); Variable B(1); @@ -325,14 +325,14 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - DO_TEST(test06); - DO_TEST(test09); - // test10() only fails when using C_Polyhedron and 8 bit coefficients. + DO_TEST(test05); + DO_TEST(test07); + // test07() only fails when using C_Polyhedron and 8 bit coefficients. #ifdef DERIVED_TEST - DO_TEST(test10); + DO_TEST(test07); #else - DO_TEST_F8(test10); + DO_TEST_F8(test07); #endif // !defined(DERIVED_TEST) - DO_TEST(test11); - DO_TEST(test12); + DO_TEST(test08); + DO_TEST(test09); END_MAIN

1 0

[GIT] ppl/ppl(devel): Removed tests 05, 07, 08 and 13.
by Enea Zaffanella 06 Nov '16

06 Nov '16

Module: ppl/ppl Branch: devel Commit: cefb3aef4ce31c9b8e53e43d7d7f722968d2a534 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cefb3aef4ce3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Nov 6 16:13:20 2016 +0100 Removed tests 05, 07, 08 and 13. These tests were checking the behavior of map_space_dimension() beyond its own specification (the partial function given as input was *adding* space dimensions). --- tests/Polyhedron/mapspacedims1.cc | 144 ------------------------------------- 1 files changed, 0 insertions(+), 144 deletions(-) diff --git a/tests/Polyhedron/mapspacedims1.cc b/tests/Polyhedron/mapspacedims1.cc index 2ebfd8d..129b4ad 100644 --- a/tests/Polyhedron/mapspacedims1.cc +++ b/tests/Polyhedron/mapspacedims1.cc @@ -137,38 +137,6 @@ test04() { } bool -test05() { - Variable A(0); - Variable B(1); - - Partial_Function function; - function.insert(2, 0); - function.insert(3, 2); - function.insert(4, 1); - - Generator_System gs; - gs.insert(point()); - gs.insert(ray(A)); - gs.insert(ray(B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(3, EMPTY); - known_result.add_generator(point()); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - -bool test06() { Variable A(0); Variable B(1); @@ -199,77 +167,6 @@ test06() { } bool -test07() { - Variable A(0); - Variable B(1); - - Partial_Function function; - function.insert(0, 1); - function.insert(1, 0); - function.insert(2, 2); - function.insert(3, 3); - - Generator_System gs; - gs.insert(point()); - gs.insert(point(A)); - gs.insert(point(2*B)); - gs.insert(point(A + 2*B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(4, EMPTY); - known_result.add_generator(point()); - known_result.add_generator(point(B)); - known_result.add_generator(point(2*A)); - known_result.add_generator(point(2*A + B)); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - -bool -test08() { - Variable A(0); - Variable B(1); - - Partial_Function function; - function.insert(0, 0); - function.insert(2, 1); - function.insert(3, 2); - - Generator_System gs; - gs.insert(point()); - gs.insert(point(A)); - gs.insert(ray(B)); - gs.insert(ray(A + B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(3, EMPTY); - known_result.add_generator(point()); - known_result.add_generator(ray(A)); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - -bool test09() { Partial_Function function; function.insert(0, 1); @@ -421,43 +318,6 @@ test12() { return ok; } -bool -test13() { - Variable A(0); - Variable B(1); - Variable C(2); - Variable D(3); - - Partial_Function function; - function.insert(0, 2); - function.insert(1, 3); - - Generator_System gs; - gs.insert(point()); - gs.insert(point(A)); - gs.insert(point(2*B)); - gs.insert(point(A + 2*B)); - - C_Polyhedron ph1(gs); - - print_function(function, "*** function ***"); - print_generators(ph1, "*** ph1 ***"); - - ph1.map_space_dimensions(function); - - C_Polyhedron known_result(4, EMPTY); - known_result.add_generator(point()); - known_result.add_generator(point(C)); - known_result.add_generator(point(2*D)); - known_result.add_generator(point(C + 2*D)); - - bool ok = (ph1 == known_result); - - print_generators(ph1, "*** after ph1.map_space_dimensions(function) ***"); - - return ok; -} - } // namespace BEGIN_MAIN @@ -465,10 +325,7 @@ BEGIN_MAIN DO_TEST(test02); DO_TEST(test03); DO_TEST(test04); - DO_TEST(test05); DO_TEST(test06); - DO_TEST(test07); - DO_TEST(test08); DO_TEST(test09); // test10() only fails when using C_Polyhedron and 8 bit coefficients. #ifdef DERIVED_TEST @@ -478,5 +335,4 @@ BEGIN_MAIN #endif // !defined(DERIVED_TEST) DO_TEST(test11); DO_TEST(test12); - DO_TEST(test13); END_MAIN

1 0