April 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Corrected typo in shift_unprimed_variables().
by Enea Zaffanella 13 Apr '10

13 Apr '10

Module: ppl/ppl Branch: master Commit: d0d4c00944c419e76af09a5f4bee186571a9111e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d0d4c00944c4… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Apr 13 18:09:45 2010 +0200 Corrected typo in shift_unprimed_variables(). --- src/termination.cc | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index bd9bc7e..30cdf19 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -97,7 +97,8 @@ shift_unprimed_variables(Constraint_System& cs) { if (a_i_j != 0) add_mul_assign(le_i_shifted, a_i_j, Variable(cs_space_dim + j)); } - cs_shifted.insert(le_i_shifted >= c_i.inhomogeneous_term()); + le_i_shifted += c_i.inhomogeneous_term(); + cs_shifted.insert(le_i_shifted >= 0); } cs.swap(cs_shifted); }

1 0

[GIT] ppl/ppl(master): Added further tests for the termination methods.
by Patricia Hill 13 Apr '10

13 Apr '10

Module: ppl/ppl Branch: master Commit: a3804165053e07f0ccd2de728932480ed0b58f68 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a3804165053e… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Apr 13 16:26:15 2010 +0100 Added further tests for the termination methods. --- ...face_generator_prolog_generated_test_pl_code.m4 | 112 +++++++++++++ tests/Polyhedron/Makefile.am | 3 + tests/Polyhedron/termination1.cc | 11 ++ tests/Polyhedron/termination2.cc | 165 ++++++++++++++++++++ 4 files changed, 291 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=a3804165…

1 0

[GIT] ppl/ppl(master): Avoid assertion crash on universe polyhedra.
by Enea Zaffanella 13 Apr '10

13 Apr '10

Module: ppl/ppl Branch: master Commit: d4d1ad3031cd681d2ff48d1e9d6990b5dbe32089 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d4d1ad3031cd… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Apr 13 10:21:28 2010 +0200 Avoid assertion crash on universe polyhedra. --- src/termination.cc | 7 +++++++ 1 files changed, 7 insertions(+), 0 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index e2749ab..bd9bc7e 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -853,6 +853,13 @@ all_affine_ranking_functions_PR_original(const Constraint_System& cs, const dimension_type n = cs.space_dimension() / 2; const dimension_type m = distance(cs.begin(), cs.end()); + if (m == 0) { + // If there are no constraints at all, we have non-termination, + // i.e., no affine ranking function at all. + mu_space = NNC_Polyhedron(n + 1, EMPTY); + return; + } + Constraint_System cs_eqs; Linear_Expression le_ineq; fill_constraint_system_PR_original(cs, cs_eqs, le_ineq);

1 0

[GIT] ppl/ppl(master): Fixed some bugs in the tests for drop_some_non_integer_points()
by Patricia Hill 13 Apr '10

13 Apr '10

Module: ppl/ppl Branch: master Commit: 543d7d068dc43aa474e497af7c95a4d9efc7a95e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=543d7d068dc4… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Apr 13 07:57:34 2010 +0100 Fixed some bugs in the tests for drop_some_non_integer_points() and added a test for termination_test_*. --- interfaces/Prolog/tests/pl_check.pl | 2 +- ...face_generator_prolog_generated_test_pl_code.m4 | 52 +++++++++++++++----- 2 files changed, 40 insertions(+), 14 deletions(-) diff --git a/interfaces/Prolog/tests/pl_check.pl b/interfaces/Prolog/tests/pl_check.pl index 83d3e48..26e651a 100644 --- a/interfaces/Prolog/tests/pl_check.pl +++ b/interfaces/Prolog/tests/pl_check.pl @@ -1822,7 +1822,7 @@ ok(T) :- % Tests ppl_termination_test_C_Polyhedron_MS/2, % ppl_termination_test_C_Polyhedron_PR/2. -% T ppl_termination_test_NNC_Polyhedron_MS/2, +% ppl_termination_test_NNC_Polyhedron_MS/2, % ppl_termination_test_NNC_Polyhedron_PR/2. termination_test :- make_vars(4, [A, B, C, D]), diff --git a/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 b/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 index 10764e6..03e3f6e 100644 --- a/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 +++ b/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 @@ -1739,8 +1739,7 @@ ppl_@CLASS@_drop_some_non_integer_points_2_test :- ( ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA, PS, Dim), ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(PS, PS_Copy), - ppl_@CLASS@_drop_some_non_integer_points(PS, any_complexity), - ppl_@CLASS@_equals_@CLASS@(PS, PS_Copy), + ppl_@CLASS@_drop_some_non_integer_points(PS, any), ppl_@CLASS@_OK(PS), ppl_delete_@CLASS@(PS), ppl_delete_@CLASS@(PS_Copy) @@ -1750,20 +1749,47 @@ ppl_@CLASS@_drop_some_non_integer_points_2_test :- ') -m4_define(`ppl_@CLASS@_drop_some_non_integer_points_code', +m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', ` -ppl_@CLASS@_drop_some_non_integer_points_2_3_test :- +ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_1_test :- ( - choose_test(TEST_DATA, Dim), + choose_2_tests(TEST_DATA1, TEST_DATA2, Space_Dim), ( - ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA, PS, Dim), - ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(PS, PS_Copy), - make_vars(Dim, Var_List), - ppl_@CLASS@_drop_some_non_integer_points_2(PS, Var_List, any_complexity), - ppl_@CLASS@_equals_@CLASS@(PS, PS_Copy), - ppl_@CLASS@_OK(PS), - ppl_delete_@CLASS@(PS), - ppl_delete_@CLASS@(PS_Copy) + ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA1, PS1, Space_Dim), + ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA2, PS2, Space_Dim), + ppl_@CLASS@_concatenate_assign(PS1, PS2), + (ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@(PS1) -> + true + ; + true + ), + ppl_@CLASS@_OK(PS1), + ppl_delete_@CLASS@(PS1), + ppl_delete_@CLASS@(PS2) + -> + fail ; true) + ). + +') + +m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', +` +ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_2_test :- + ( + choose_2_tests(TEST_DATA1, TEST_DATA2, Space_Dim), + ( + ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA1, PS1, Space_Dim), + ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA2, PS2, Space_Dim), + ppl_@CLASS@_concatenate_assign(PS1, PS2), + (ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2(PS2, PS1) -> + true + ; + true + ), + ppl_@CLASS@_OK(PS1), + ppl_@CLASS@_OK(PS2), + ppl_delete_@CLASS@(PS1), + ppl_delete_@CLASS@(PS2) -> fail ; true) ).

1 0

[GIT] ppl/ppl(master): Added tests to the OCaml interface for new functions
by Patricia Hill 12 Apr '10

12 Apr '10

Module: ppl/ppl Branch: master Commit: c9fd6d302f987aed452b463c418f9aab7a530460 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c9fd6d302f98… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon Apr 12 16:04:04 2010 +0100 Added tests to the OCaml interface for new functions wrap_assign(), drop_some_non_integer_points() and termination_test_*. Bug in termination_test_*. fixed and test showing these added to termination1.cc --- .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 | 3 +- .../OCaml/ppl_interface_generator_ocaml_ml_code.m4 | 3 +- .../ppl_interface_generator_ocaml_mli_code.m4 | 12 +++- .../ppl_interface_generator_ocaml_test_ml_code.m4 | 80 ++++++++++++++++++++ ...face_generator_prolog_generated_test_pl_code.m4 | 39 ++++++++++ src/termination.cc | 6 +- tests/Polyhedron/termination1.cc | 7 ++ 7 files changed, 145 insertions(+), 5 deletions(-) diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 index ad58ad4..8903dd4 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 @@ -1477,11 +1477,12 @@ ppl_@CLASS@_wrap_assign_native } CATCH_ALL +extern "C" CAMLprim value ppl_@CLASS@_wrap_assign_bytecode(value * argv, int) { return ppl_@CLASS@_wrap_assign_native(argv[0], argv[1], argv[2], argv[3], - argv[4], argv[5], argv[6], argv[7]); + argv[4], argv[5], argv[6], argv[7]); } ') diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 index 160121b..10241c8 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_ml_code.m4 @@ -638,11 +638,12 @@ external ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2: m4_define(`ppl_@CLASS@_wrap_assign_code', `dnl external ppl_@CLASS@_wrap_assign: @!CLASS@ + -> int list -> bounded_integer_type_width -> bounded_integer_type_representation -> bounded_integer_type_overflow -> constraint_system - -> int list -> int -> int -> unit + -> int -> int -> unit = "ppl_@CLASS@_wrap_assign_bytecode" "ppl_@CLASS@_wrap_assign_native" diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 index df7eb0e..bed44cf 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_mli_code.m4 @@ -503,6 +503,13 @@ val ppl_@CLASS@_approximate_@PARTITION@: ') +m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', +`dnl +val ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@: + @!CLASS@ -> bool + +') + m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', `dnl val ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2: @@ -552,11 +559,14 @@ val ppl_all_affine_quasi_ranking_functions_MS_@TOPOLOGY@@CLASS@_2: ') +m4_define(`ppl_@CLASS@_wrap_assign_code', +`dnl val ppl_@CLASS@_wrap_assign: @!CLASS@ + -> int list -> bounded_integer_type_width -> bounded_integer_type_representation -> bounded_integer_type_overflow -> constraint_system - -> int list -> int -> int -> unit + -> int -> int -> unit ') diff --git a/interfaces/OCaml/tests/ppl_interface_generator_ocaml_test_ml_code.m4 b/interfaces/OCaml/tests/ppl_interface_generator_ocaml_test_ml_code.m4 index 4c606b1..c5b3035 100644 --- a/interfaces/OCaml/tests/ppl_interface_generator_ocaml_test_ml_code.m4 +++ b/interfaces/OCaml/tests/ppl_interface_generator_ocaml_test_ml_code.m4 @@ -884,3 +884,83 @@ let out in (print_string_if_noisy out);; print_string_if_noisy "\n";; ') + +m4_define(`ppl_@CLASS@_drop_some_non_integer_points_code', +` +print_string_if_noisy "testing ppl_@CLASS@_drop_some_non_integer_points: ";; +let copy01 + = ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(@!TOPOLOGY@@!CLASS@01);; +let u = ppl_@CLASS@_drop_some_non_integer_points copy01 Any_Complexity ;; +let out = if (u = () & ppl_@CLASS@_OK copy01) + then "success" else "failed" + in (print_string_if_noisy out);; +print_string_if_noisy "\n";; +') + +m4_define(`ppl_@CLASS@_drop_some_non_integer_points_2_code', +` +print_string_if_noisy "testing ppl_@CLASS@_drop_some_non_integer_points: ";; +let copy01 + = ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(@!TOPOLOGY@@!CLASS@01);; +let dimensions_integer = [1];; +let u = ppl_@CLASS@_drop_some_non_integer_points_2 copy01 dimensions_integer Any_Complexity ;; +let out = if (u = () & ppl_@CLASS@_OK copy01) + then "success" else "failed" + in (print_string_if_noisy out);; +print_string_if_noisy "\n";; +') + +m4_define(`ppl_@CLASS@_wrap_assign_code', +` +print_string_if_noisy "testing ppl_@CLASS@_wrap_assign: ";; +let copy01 + = ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(@!TOPOLOGY@@!CLASS@01);; +let dimensions_integer = [1];; +let u = ppl_@CLASS@_wrap_assign copy01 [] Bits_8 Unsigned Overflow_Wraps + [] 0 1;; +let out = if (u = () & ppl_@CLASS@_OK copy01) + then "success" else "failed" + in (print_string_if_noisy out);; +print_string_if_noisy "\n";; +') + +m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_code', +` +print_string_if_noisy + "testing ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@: ";; +let copy01 + = ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(@!TOPOLOGY@@!CLASS@01);; +let univ + = ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension 2 Universe;; +let u = ppl_@CLASS@_concatenate_assign copy01 @!TOPOLOGY@@!CLASS@01;; +let result1 = ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ univ;; +let result2 + = ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@ copy01;; +let out = if (not result1 & not result2 & ppl_@CLASS@_OK copy01) + then "success" else "failed" + in (print_string_if_noisy out);; +print_string_if_noisy "\n";; +') + +m4_define(`ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2_code', +` +print_string_if_noisy + "testing ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2: ";; +let copy01 + = ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(@!TOPOLOGY@@!CLASS@01);; +let copy02 + = ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(@!TOPOLOGY@@!CLASS@02);; +let u = ppl_@CLASS@_concatenate_assign copy02 @!TOPOLOGY@@!CLASS@02;; +let result1 + = ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2 copy01 copy02;; +let univ01 + = ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension 2 Universe;; +let univ02 + = ppl_new_@TOPOLOGY@@CLASS@_from_space_dimension 4 Universe;; +let result2 + = ppl_termination_test_@TERMINATION_ID@_@TOPOLOGY@@CLASS@_2 univ01 univ02;; +let out = if (not result1 & not result2 & ppl_@CLASS@_OK copy01) + then "success" else "failed" + in (print_string_if_noisy out);; +print_string_if_noisy "\n";; +') diff --git a/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 b/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 index 4ed6891..10764e6 100644 --- a/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 +++ b/interfaces/Prolog/tests/ppl_interface_generator_prolog_generated_test_pl_code.m4 @@ -1731,4 +1731,43 @@ ppl_@CLASS@_wrap_assign_8_test :- ') +m4_define(`ppl_@CLASS@_drop_some_non_integer_points_code', +` +ppl_@CLASS@_drop_some_non_integer_points_2_test :- + ( + choose_test(TEST_DATA, Dim), + ( + ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA, PS, Dim), + ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(PS, PS_Copy), + ppl_@CLASS@_drop_some_non_integer_points(PS, any_complexity), + ppl_@CLASS@_equals_@CLASS@(PS, PS_Copy), + ppl_@CLASS@_OK(PS), + ppl_delete_@CLASS@(PS), + ppl_delete_@CLASS@(PS_Copy) + -> + fail ; true) + ). + +') + +m4_define(`ppl_@CLASS@_drop_some_non_integer_points_code', +` +ppl_@CLASS@_drop_some_non_integer_points_2_3_test :- + ( + choose_test(TEST_DATA, Dim), + ( + ppl_@TOPOLOGY@@CLASS@_build_test_object(TEST_DATA, PS, Dim), + ppl_new_@TOPOLOGY@@CLASS@_from_@TOPOLOGY@@CLASS@(PS, PS_Copy), + make_vars(Dim, Var_List), + ppl_@CLASS@_drop_some_non_integer_points_2(PS, Var_List, any_complexity), + ppl_@CLASS@_equals_@CLASS@(PS, PS_Copy), + ppl_@CLASS@_OK(PS), + ppl_delete_@CLASS@(PS), + ppl_delete_@CLASS@(PS_Copy) + -> + fail ; true) + ). + +') + dnl ppl_@CLASS@_@NARROWING@_narrowing_assign/2, diff --git a/src/termination.cc b/src/termination.cc index 3ba1213..e2749ab 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -362,7 +362,8 @@ fill_constraint_system_PR(const Constraint_System& cs_before, const dimension_type m = r + s; // Make sure linear expressions are not reallocated multiple times. - le_out = 0 * Variable(m + r - 1); + if (m > 0) + le_out = 0 * Variable(m + r - 1); std::vector<Linear_Expression> les_eq(2*n, le_out); dimension_type row_index = 0; @@ -436,7 +437,8 @@ fill_constraint_system_PR_original(const Constraint_System& cs, const dimension_type m = distance(cs.begin(), cs.end()); // Make sure linear expressions are not reallocated multiple times. - le_out = 0 * Variable(2*m - 1); + if (m > 0) + le_out = 0 * Variable(2*m - 1); std::vector<Linear_Expression> les_eq(3*n, le_out); dimension_type row_index = 0; diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index 0d86c03..0bbe66e 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -491,6 +491,12 @@ test20() { return known_result == witness; } +bool +test21() { + C_Polyhedron ph(2); + return !termination_test_PR(ph); +} + } // namespace BEGIN_MAIN @@ -514,4 +520,5 @@ BEGIN_MAIN DO_TEST(test18); DO_TEST(test19); DO_TEST(test20); + DO_TEST(test21); END_MAIN

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Over_CO_Tree, CO_Tree: major changes. Now all test pass with -DUSE_PPL_SPARSE_BACKEND_CO_TREE.
by Marco Poletti 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 8bfc24464429dace27dc965c0c5bfcda9b1ee845 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8bfc24464429… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Apr 11 19:12:17 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree, CO_Tree: major changes. Now all test pass with -DUSE_PPL_SPARSE_BACKEND_CO_TREE. --- src/CO_Tree.cc | 289 ++++++++++++- src/CO_Tree.defs.hh | 30 ++- src/CO_Tree.inlines.hh | 211 ++++++++-- src/Makefile.am | 1 + src/Unlimited_Sparse_Row.types.hh | 39 ++ src/Unlimited_Sparse_Row_Over_CO_Tree.cc | 43 ++ src/Unlimited_Sparse_Row_Over_CO_Tree.defs.hh | 29 +- src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh | 450 ++++++++++++++++++-- src/Unlimited_Sparse_Row_Over_CO_Tree.templates.hh | 261 ++++++++++++ ...limited_Sparse_Row_Over_Linear_Sequence.defs.hh | 37 +-- ...ed_Sparse_Row_Over_Linear_Sequence.templates.hh | 2 +- tests/CO_Tree/cotree1.cc | 52 +-- 12 files changed, 1277 insertions(+), 167 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=8bfc2446…

1 0

[GIT] ppl/ppl(sparse_matrices): PIP_Solution_Node: fix NOISY_PIP section in generate_cut().
by Marco Poletti 11 Apr '10

11 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: eb4d309115ff8e2eb87b8909e91da407f37ab579 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eb4d309115ff… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Apr 11 18:54:23 2010 +0200 PIP_Solution_Node: fix NOISY_PIP section in generate_cut(). --- src/PIP_Tree.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 97033ca..eb24bfb 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -3330,7 +3330,7 @@ PIP_Solution_Node::generate_cut(const dimension_type index, using namespace IO_Operators; Variables_Set::const_iterator p = parameters.begin(); Linear_Expression expr1(ctx1.get(0)); - Linear_Expression expr2(ctx2_0); + Linear_Expression expr2(ctx2.get(0)); for (dimension_type j = 1; j <= num_params; ++j, ++p) { expr1 += ctx1.get(j) * Variable(*p); expr2 += ctx2.get(j) * Variable(*p);

1 0

[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