April 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Both GNU Prolog 1.3.0 and GNU Prolog 1.3. 1 have bugs that affect the PPL.
by Roberto Bagnara 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: master Commit: e17e80c8940b435d646eaac97bba591ee744ef34 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e17e80c8940b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Apr 15 17:39:08 2010 +0200 Both GNU Prolog 1.3.0 and GNU Prolog 1.3.1 have bugs that affect the PPL. --- interfaces/Prolog/GNU/README.gprolog | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/interfaces/Prolog/GNU/README.gprolog b/interfaces/Prolog/GNU/README.gprolog index 32d814a..4acb035 100644 --- a/interfaces/Prolog/GNU/README.gprolog +++ b/interfaces/Prolog/GNU/README.gprolog @@ -1,7 +1,7 @@ The GNU Prolog interface to the Parma Polyhedra Library (PPL) is available both as a PPL-enhanced GNU Prolog interpreter and as a library that can be linked to GNU Prolog programs. Only GNU Prolog -version 1.3.0 and later versions are supported. +version 1.3.2(20100322) and later versions are supported. So that it can be used with the GNU Prolog PPL interface (and, for that matter, with any foreign code), the GNU Prolog installation must

1 0

[GIT] ppl/ppl(master): Minor improvements to documentation.
by Enea Zaffanella 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: master Commit: bcc4ff72caf513a585ec003e5adaff6aec2fb05b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bcc4ff72caf5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Apr 15 15:06:28 2010 +0200 Minor improvements to documentation. Deal with the special cse of an empty input pointset for methods all_affine_*. Adapted and improved test10 in termination2.cc. --- src/termination.defs.hh | 29 ++++++++++++++----------- src/termination.templates.hh | 39 ++++++++++++++++++++++++++++++++- tests/Polyhedron/termination2.cc | 43 +++++++++++++++++++++++-------------- 3 files changed, 80 insertions(+), 31 deletions(-) diff --git a/src/termination.defs.hh b/src/termination.defs.hh index 8ccfc41..c64ed58 100644 --- a/src/termination.defs.hh +++ b/src/termination.defs.hh @@ -23,8 +23,9 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_termination_defs_hh #define PPL_termination_defs_hh 1 -#include "Generator.defs.hh" -#include "C_Polyhedron.defs.hh" +#include "Generator.types.hh" +#include "C_Polyhedron.types.hh" +#include "NNC_Polyhedron.types.hh" namespace Parma_Polyhedra_Library { @@ -408,15 +409,15 @@ all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before, C_Polyhedron& bounded_mu_space); /*! \brief - Like termination_test_MS() but using an improvement - of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". + Like termination_test_MS() but using the method by Podelski and + Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool termination_test_PR(const PSET& pset); /*! \brief - Like termination_test_MS_2() but using an improvement + Like termination_test_MS_2() but using an alternative formalization of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> @@ -424,16 +425,17 @@ bool 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 \ref BMPZ10 "[BMPZ10]". + Like one_affine_ranking_function_MS() but using the method by Podelski + and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool 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 \ref BMPZ10 "[BMPZ10]". + Like one_affine_ranking_function_MS_2() but using an alternative + formalization of the method by Podelski and Rybalchenko + \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> bool @@ -442,16 +444,17 @@ one_affine_ranking_function_PR_2(const PSET& pset_before, Generator& mu); /*! \brief - Like all_affine_ranking_functions_MS() but using an improvement - of the method by Podelski and Rybalchenko \ref BMPZ10 "[BMPZ10]". + Like all_affine_ranking_functions_MS() but using the method by Podelski + and Rybalchenko \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> void 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 \ref BMPZ10 "[BMPZ10]". + Like all_affine_ranking_functions_MS_2() but using an alternative + formalization of the method by Podelski and Rybalchenko + \ref BMPZ10 "[BMPZ10]". */ template <typename PSET> void diff --git a/src/termination.templates.hh b/src/termination.templates.hh index f60573c..8582e22 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -23,10 +23,13 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_termination_templates_hh #define PPL_termination_templates_hh 1 +#include "globals.defs.hh" +#include "Variable.defs.hh" +#include "Generator.defs.hh" #include "Constraint_System.defs.hh" #include "C_Polyhedron.defs.hh" -#include "BD_Shape.defs.hh" -#include "Octagonal_Shape.defs.hh" + +#include <stdexcept> #define PRINT_DEBUG_INFO 0 @@ -301,6 +304,11 @@ all_affine_ranking_functions_MS(const PSET& pset, C_Polyhedron& mu_space) { throw std::invalid_argument(s.str()); } + if (pset.is_empty()) { + mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE); + return; + } + using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset, cs); @@ -324,6 +332,11 @@ all_affine_ranking_functions_MS_2(const PSET& pset_before, throw std::invalid_argument(s.str()); } + if (pset_before.is_empty()) { + mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE); + return; + } + using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset_before, pset_after, cs); @@ -345,6 +358,12 @@ all_affine_quasi_ranking_functions_MS(const PSET& pset, throw std::invalid_argument(s.str()); } + if (pset.is_empty()) { + decreasing_mu_space = C_Polyhedron(1 + space_dim/2, UNIVERSE); + bounded_mu_space = decreasing_mu_space; + return; + } + using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset, cs); @@ -371,6 +390,12 @@ all_affine_quasi_ranking_functions_MS_2(const PSET& pset_before, throw std::invalid_argument(s.str()); } + if (pset_before.is_empty()) { + decreasing_mu_space = C_Polyhedron(1 + before_space_dim, UNIVERSE); + bounded_mu_space = decreasing_mu_space; + return; + } + using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset_before, pset_after, cs); @@ -479,6 +504,11 @@ all_affine_ranking_functions_PR_2(const PSET& pset_before, throw std::invalid_argument(s.str()); } + if (pset_before.is_empty()) { + mu_space = NNC_Polyhedron(1 + before_space_dim); + return; + } + using namespace Implementation::Termination; Constraint_System cs_before; Constraint_System cs_after; @@ -500,6 +530,11 @@ all_affine_ranking_functions_PR(const PSET& pset_after, throw std::invalid_argument(s.str()); } + if (pset_after.is_empty()) { + mu_space = NNC_Polyhedron(1 + space_dim/2); + return; + } + using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset_after, cs); diff --git a/tests/Polyhedron/termination2.cc b/tests/Polyhedron/termination2.cc index 43fcceb..496a476 100644 --- a/tests/Polyhedron/termination2.cc +++ b/tests/Polyhedron/termination2.cc @@ -128,26 +128,37 @@ test09() { bool test10() { - C_Polyhedron ph1(2, EMPTY); - C_Polyhedron ph2(4, EMPTY); + C_Polyhedron ph_before(2, EMPTY); + C_Polyhedron ph_after(4, EMPTY); C_Polyhedron c_mu_space; NNC_Polyhedron nnc_mu_space; - all_affine_ranking_functions_MS(ph1, c_mu_space); - all_affine_ranking_functions_MS_2(ph1, ph2, c_mu_space); - all_affine_ranking_functions_PR(ph1, nnc_mu_space); - all_affine_ranking_functions_PR_2(ph1, ph2, nnc_mu_space); + C_Polyhedron c_known_result(3, UNIVERSE); + NNC_Polyhedron nnc_known_result(3, UNIVERSE); + bool ok = true; - C_Polyhedron c_known_result(2, EMPTY); - c_known_result.add_generator(point()); - NNC_Polyhedron nnc_known_result(3, EMPTY); - nnc_known_result.add_generator(point()); + all_affine_ranking_functions_MS(ph_after, c_mu_space); + ok &= (c_mu_space == c_known_result); - print_constraints(ph1, "*** ph ***"); - print_constraints(c_mu_space, "*** c_mu_space ***"); - print_constraints(nnc_known_result, "*** nnc_known_result ***"); - print_constraints(nnc_mu_space, "*** nnc_mu_space ***"); + all_affine_ranking_functions_MS_2(ph_before, ph_after, c_mu_space); + ok &= (c_mu_space == c_known_result); - return ph1.OK() && (nnc_mu_space == nnc_known_result); +// all_affine_ranking_functions_PR(ph_after, nnc_mu_space); +// ok &= (nnc_mu_space == nnc_known_result); + + all_affine_ranking_functions_PR_2(ph_before, ph_after, nnc_mu_space); + ok &= (nnc_mu_space == nnc_known_result); + + print_constraints(ph_after, "*** ph_after ***"); + + print_generators(c_known_result.minimized_generators(), + "*** c_known_result ***"); + print_generators(nnc_known_result.minimized_generators(), + "*** nnc_known_result ***"); + + print_generators(c_mu_space.minimized_generators(), "*** c_mu_space ***"); + print_generators(nnc_mu_space.minimized_generators(), "*** nnc_mu_space ***"); + + return ok; } } // namespace @@ -162,5 +173,5 @@ BEGIN_MAIN DO_TEST(test07); DO_TEST(test08); DO_TEST(test09); - DO_TEST_F(test10); + DO_TEST(test10); END_MAIN

1 0

[GIT] ppl/ppl(master): Overflow is expected for PIP_Problem tests with 8 bits coefficients.
by Enea Zaffanella 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: master Commit: baa72379c66f766c6ee6a6956e6f3f329cffeba7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=baa72379c66f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Apr 15 13:58:39 2010 +0200 Overflow is expected for PIP_Problem tests with 8 bits coefficients. --- interfaces/OCaml/tests/test1.ml | 162 ++++++++++++++++++++++++--------------- 1 files changed, 101 insertions(+), 61 deletions(-) diff --git a/interfaces/OCaml/tests/test1.ml b/interfaces/OCaml/tests/test1.ml index a3d84aa..e877d34 100644 --- a/interfaces/OCaml/tests/test1.ml +++ b/interfaces/OCaml/tests/test1.ml @@ -506,12 +506,21 @@ print_string_if_noisy "PIP_Problem_OK ";; print_string_if_noisy "and PIP_Tree_Node_is_bottom \n";; let pip = ppl_new_PIP_Problem 3 [e1 >=/ e2; e1 <=/ e2 -/ (linear_expression_of_int 7)] [2];; -let ptree = ppl_PIP_Problem_solution pip;; -let - out = if (ppl_PIP_Problem_OK pip - & ppl_PIP_Tree_Node_is_bottom ptree) - then "success" else "failed" - in (print_string_if_noisy out);; + +begin +try + let ptree = ppl_PIP_Problem_solution pip + in let out = if (ppl_PIP_Problem_OK pip & ppl_PIP_Tree_Node_is_bottom ptree) + then "success" else "failed" + in (print_string_if_noisy out) +with PPL_arithmetic_overflow what -> + let unexpected = (ppl_Coefficient_bits() != 8) + in if (unexpected) + then raise (PPL_arithmetic_overflow(what)); + print_string_if_noisy "Expected overflow exception caught: "; + print_string_if_noisy what; + print_string_if_noisy "\n" +end;; print_string_if_noisy "\n";; print_string_if_noisy "PIP_Problem 2 \n";; @@ -542,22 +551,31 @@ let out = if (not b0 & b1 & (big_par = 7)) else "ppl_PIP_Problem big parameter dimension tests failed" in (print_string_if_noisy out);; print_string_if_noisy "\n";; -let out = if (ppl_PIP_Problem_is_satisfiable pip2) - then "ppl_PIP_Problem_is_satisfiable test succeeded" - else "ppl_PIP_Problem_is_satisfiable test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -print_string_if_noisy "testing ppl_PIP_Problem_ascii_dump: " ;; -(* print_string_if_noisy (ppl_PIP_Problem_ascii_dump pip2);; *) -print_string_if_noisy "\n";; -let ptree2 = ppl_PIP_Problem_solution pip2;; -let _r = ppl_PIP_Problem_OK pip2;; -print_string_if_noisy "\n";; -let out = if (ppl_PIP_Tree_Node_is_bottom ptree2) - then "ppl_PIP_Tree_Node_is_bottom test succeeded" - else "ppl_PIP_Tree_Node_is_bottom test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; + +begin +try + let out = if (ppl_PIP_Problem_is_satisfiable pip2) + then "ppl_PIP_Problem_is_satisfiable test succeeded" + else "ppl_PIP_Problem_is_satisfiable test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + print_string_if_noisy "testing ppl_PIP_Problem_ascii_dump: "; + print_string_if_noisy (ppl_PIP_Problem_ascii_dump pip2); + print_string_if_noisy "\n"; + let ptree2 = ppl_PIP_Problem_solution pip2 + in let out2 = if (ppl_PIP_Tree_Node_is_bottom ptree2) + then "ppl_PIP_Tree_Node_is_bottom test succeeded" + else "ppl_PIP_Tree_Node_is_bottom test failed" + in (print_string_if_noisy out2); + print_string_if_noisy "\n" +with PPL_arithmetic_overflow what -> + let unexpected = (ppl_Coefficient_bits() != 8) + in if (unexpected) + then raise (PPL_arithmetic_overflow(what)); + print_string_if_noisy "Expected overflow exception caught: "; + print_string_if_noisy what; + print_string_if_noisy "\n" +end;; print_string_if_noisy "\nPIP_Problem 3 \n";; let i = Variable 0 @@ -583,45 +601,67 @@ let pip_cs = [pip_c1; pip_c2; pip_c3; pip_c4] ;; let ps = [2; 3];; let pip3 = ppl_new_PIP_Problem 4 pip_cs ps;; -let result = ppl_PIP_Problem_solve pip3;; -let out = if (result == Optimized_Pip_Problem) - then "PIP Problem_solve pip3 test succeeded" - else "PIP Problem_solve pip3 test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -let node = ppl_PIP_Problem_solution pip3;; -let out = if (ppl_PIP_Tree_Node_OK node) - then "ppl_PIP_Tree_Node_OK node test succeeded" - else "ppl_PIP_Tree_Node_OK node test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -let out = if (ppl_PIP_Tree_Node_is_decision node) - then "ppl_PIP_Tree_Node_is_decision node test succeeded" - else "ppl_PIP_Tree_Node_is_decision node test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -let out = if (ppl_PIP_Tree_Node_artificials node = []) - then "ppl_PIP_Tree_Node_artificials node test succeeded" - else "ppl_PIP_Tree_Node_artificials node test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -let _node_cs = ppl_PIP_Tree_Node_constraints node;; -let tchild = ppl_PIP_Tree_Node_true_child node;; -let _fchild = ppl_PIP_Tree_Node_false_child node;; -let out = if (ppl_PIP_Tree_Node_is_decision tchild) - then "ppl_PIP_Tree_Node_is_decision tchild test succeeded" - else "ppl_PIP_Tree_Node_is_decision tchild test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -let ttchild = ppl_PIP_Tree_Node_true_child tchild;; -let ftchild = ppl_PIP_Tree_Node_false_child tchild;; -let out = if (ppl_PIP_Tree_Node_is_solution ttchild) - then "ppl_PIP_Tree_Node_is_decision ttchild test succeeded" - else "ppl_PIP_Tree_Node_is_decision ttchild test failed" - in (print_string_if_noisy out);; -print_string_if_noisy "\n";; -let _par_vals = ppl_PIP_Tree_Node_parametric_values ttchild 0;; -let _ftchild_arts = ppl_PIP_Tree_Node_artificials ftchild;; + +begin +try + let result = ppl_PIP_Problem_solve pip3 in + let out = if (result == Optimized_Pip_Problem) + then "PIP Problem_solve pip3 test succeeded" + else "PIP Problem_solve pip3 test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + let node = ppl_PIP_Problem_solution pip3 in + begin + let out = if (ppl_PIP_Tree_Node_OK node) + then "ppl_PIP_Tree_Node_OK node test succeeded" + else "ppl_PIP_Tree_Node_OK node test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + let out = if (ppl_PIP_Tree_Node_is_decision node) + then "ppl_PIP_Tree_Node_is_decision node test succeeded" + else "ppl_PIP_Tree_Node_is_decision node test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + let out = if (ppl_PIP_Tree_Node_artificials node = []) + then "ppl_PIP_Tree_Node_artificials node test succeeded" + else "ppl_PIP_Tree_Node_artificials node test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + let _node_cs = ppl_PIP_Tree_Node_constraints node in (); + let + _fchild = ppl_PIP_Tree_Node_false_child node + and + tchild = (ppl_PIP_Tree_Node_true_child node) + in ( + let out = if (ppl_PIP_Tree_Node_is_decision tchild) + then "ppl_PIP_Tree_Node_is_decision tchild test succeeded" + else "ppl_PIP_Tree_Node_is_decision tchild test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + let + ttchild = (ppl_PIP_Tree_Node_true_child tchild) + and + ftchild = (ppl_PIP_Tree_Node_false_child tchild) + in ( + let out = if (ppl_PIP_Tree_Node_is_solution ttchild) + then "ppl_PIP_Tree_Node_is_decision ttchild test succeeded" + else "ppl_PIP_Tree_Node_is_decision ttchild test failed" + in (print_string_if_noisy out); + print_string_if_noisy "\n"; + let _par_vals = ppl_PIP_Tree_Node_parametric_values ttchild 0 in (); + let _ftchild_arts = ppl_PIP_Tree_Node_artificials ftchild in () + ) + ); + print_string_if_noisy "\n" + end +with PPL_arithmetic_overflow what -> + let unexpected = (ppl_Coefficient_bits() != 8) + in if (unexpected) + then raise (PPL_arithmetic_overflow(what)); + print_string_if_noisy "Expected overflow exception caught: "; + print_string_if_noisy what; + print_string_if_noisy "\n" +end;; (* Pointset_Powerset_Grid is not enabled by default, the following code is *) (* commented *)

1 0

[GIT] ppl/ppl(sparse_matrices): New commits
by Roberto Bagnara 15 Apr '10

15 Apr '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=98cc6288516f… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:49:35 2010 +0200 PIP_Tree_Node: use unordered iterators in compatibility_check(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=97b78d5061c8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:43:40 2010 +0200 PIP_Solution_Node: optimize update_tableau() for sparse backends with fast random writes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5896c5bffc6c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:39:01 2010 +0200 PIP_Tree.cc: optimize merge_assign() for sparse backends with fast random writes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f7174c49c725… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:33:02 2010 +0200 PIP_Solution_Node: optimize generate_cut() for sparse backends with fast random writes (#3). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=622d9172ec91… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:29:36 2010 +0200 PIP_Solution_Node: optimize generate_cut() for sparse backends with fast random writes (#2). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=028a1074e973… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:25:12 2010 +0200 PIP_Solution_Node: optimize generate_cut() for sparse backends with fast random writes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1e9f1185a41c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:14:36 2010 +0200 PIP_Solution_Node: optimize solve() for sparse backends with fast random writes (#2). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=69331bf4a9c5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 13:06:32 2010 +0200 PIP_Solution_Node: optimize solve() for sparse backends with fast random writes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9e580242fd28… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 12:57:44 2010 +0200 PIP_Solution_Node: optimize update_tableau() for sparse backends with fast random writes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=92bb0278f560… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 12:30:21 2010 +0200 PIP_Tree_Node: optimize compatibility_check() for backends with fast random writes. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=289c56dc96e2… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 12:29:29 2010 +0200 Unlimited_Sparse_Row: define PPL_SPARSE_BACKEND_SLOW_RANDOM_READS and PPL_SPARSE_BACKEND_SLOW_RANDOM_WRITES when appropriate.

1 0

[GIT] ppl/ppl(master): Increased GLOBALSZ for the execution of the automatically generated test.
by Roberto Bagnara 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: master Commit: fb0d779dadba740e2eb6c6c26f7270fe8ab69440 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fb0d779dadba… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Apr 15 12:47:16 2010 +0200 Increased GLOBALSZ for the execution of the automatically generated test. --- interfaces/Prolog/GNU/Makefile.am | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/interfaces/Prolog/GNU/Makefile.am b/interfaces/Prolog/GNU/Makefile.am index 962a9e1..9f4981c 100644 --- a/interfaces/Prolog/GNU/Makefile.am +++ b/interfaces/Prolog/GNU/Makefile.am @@ -289,7 +289,7 @@ ppl_prolog_generated_test: gnu_prolog_generated_test.pl ../tests/ppl_prolog_gen echo "['ppl_prolog_generated_test_main.pl', 'gnu_prolog_generated_test.pl']." \ >script_pgt echo "main." >>script_pgt - GLOBALSZ=65536 $(LIBTOOL) --mode=execute \ + GLOBALSZ=131072 $(LIBTOOL) --mode=execute \ -dlopen ../../../src/libppl.la \ $(WATCHDOG_DLOPEN) \ -dlopen libppl_gprolog.la \

1 0

[GIT] ppl/ppl(master): Add ppl_Coefficient_bits to Prolog and OCaml interfaces.
by Enea Zaffanella 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: master Commit: f00290188682f65683a0e25eb4563df23067cdae URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f00290188682… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Apr 15 11:33:29 2010 +0200 Add ppl_Coefficient_bits to Prolog and OCaml interfaces. Renamed corresponding static method in Java interface. --- interfaces/Java/jni/ppl_java_globals.cc | 2 +- .../Java/parma_polyhedra_library/Coefficient.java | 2 +- interfaces/Java/tests/PIP_Problem_test1.java | 2 +- interfaces/OCaml/OCaml_interface.dox | 4 ++++ interfaces/OCaml/ppl_ocaml_common.cc | 8 ++++++++ interfaces/OCaml/ppl_ocaml_globals.ml | 3 +++ interfaces/OCaml/ppl_ocaml_globals.mli | 3 +++ interfaces/Prolog/Prolog_interface.dox | 5 +++++ interfaces/Prolog/ppl_prolog_common.cc | 9 +++++++++ interfaces/Prolog/ppl_prolog_common.defs.hh | 3 +++ 10 files changed, 38 insertions(+), 3 deletions(-) diff --git a/interfaces/Java/jni/ppl_java_globals.cc b/interfaces/Java/jni/ppl_java_globals.cc index 467ac21..14b32e1 100644 --- a/interfaces/Java/jni/ppl_java_globals.cc +++ b/interfaces/Java/jni/ppl_java_globals.cc @@ -97,7 +97,7 @@ Java_parma_1polyhedra_1library_By_1Reference_initIDs } JNIEXPORT jint JNICALL -Java_parma_1polyhedra_1library_Coefficient_ppl_1bits(JNIEnv*, jclass) { +Java_parma_1polyhedra_1library_Coefficient_bits(JNIEnv*, jclass) { return PPL_COEFFICIENT_BITS; } diff --git a/interfaces/Java/parma_polyhedra_library/Coefficient.java b/interfaces/Java/parma_polyhedra_library/Coefficient.java index 4b89bcb..c8cdd8f 100644 --- a/interfaces/Java/parma_polyhedra_library/Coefficient.java +++ b/interfaces/Java/parma_polyhedra_library/Coefficient.java @@ -75,7 +75,7 @@ public class Coefficient { } //! Returns the number of bits of PPL coefficients; 0 if unbounded. - public static native int ppl_bits(); + public static native int bits(); private static native void initIDs(); static { diff --git a/interfaces/Java/tests/PIP_Problem_test1.java b/interfaces/Java/tests/PIP_Problem_test1.java index 1140207..a5b1121 100644 --- a/interfaces/Java/tests/PIP_Problem_test1.java +++ b/interfaces/Java/tests/PIP_Problem_test1.java @@ -362,7 +362,7 @@ static { pip.solve(); } catch (Overflow_Error_Exception ex) { - if (Coefficient.ppl_bits() != 8) + if (Coefficient.bits() != 8) throw ex; PPL_Test.println_if_noisy("Expected overflow exception caught:"); PPL_Test.println_if_noisy(ex.getMessage()); diff --git a/interfaces/OCaml/OCaml_interface.dox b/interfaces/OCaml/OCaml_interface.dox index affac00..5e68e03 100644 --- a/interfaces/OCaml/OCaml_interface.dox +++ b/interfaces/OCaml/OCaml_interface.dox @@ -177,6 +177,10 @@ included with all instantiations of the OCaml interfaces. <H2><CODE> ppl_max_space_dimension </CODE></H2> Returns the maximum space dimension the C++ interface can handle. +<H2><CODE> ppl_Coefficient_bits </CODE></H2> + Returns the number of bits used in the C++ interface for PPL coefficients; + 0 if unbounded. + <H2><CODE> ppl_Coefficient_is_bounded </CODE></H2> Returns true if and only if the coefficients in the C++ interface are bounded. diff --git a/interfaces/OCaml/ppl_ocaml_common.cc b/interfaces/OCaml/ppl_ocaml_common.cc index a852f53..76a04ca 100644 --- a/interfaces/OCaml/ppl_ocaml_common.cc +++ b/interfaces/OCaml/ppl_ocaml_common.cc @@ -1752,6 +1752,14 @@ CATCH_ALL extern "C" CAMLprim value +ppl_Coefficient_bits(value unit) try { + CAMLparam1(unit); + CAMLreturn(Val_long(PPL_COEFFICIENT_BITS)); +} +CATCH_ALL + +extern "C" +CAMLprim value ppl_Coefficient_is_bounded(value unit) try { CAMLparam1(unit); CAMLreturn(std::numeric_limits<Coefficient>::is_bounded diff --git a/interfaces/OCaml/ppl_ocaml_globals.ml b/interfaces/OCaml/ppl_ocaml_globals.ml index 408febf..a8e6b79 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.ml +++ b/interfaces/OCaml/ppl_ocaml_globals.ml @@ -156,6 +156,9 @@ string -> int -> int -> int -> string = "ppl_io_wrap_string" external ppl_max_space_dimension: unit -> int = "ppl_max_space_dimension" +external ppl_Coefficient_bits: +unit -> int = "ppl_Coefficient_bits" + external ppl_Coefficient_is_bounded: unit -> bool = "ppl_Coefficient_is_bounded" diff --git a/interfaces/OCaml/ppl_ocaml_globals.mli b/interfaces/OCaml/ppl_ocaml_globals.mli index 79cff49..f76d8a8 100644 --- a/interfaces/OCaml/ppl_ocaml_globals.mli +++ b/interfaces/OCaml/ppl_ocaml_globals.mli @@ -151,6 +151,9 @@ val ppl_io_wrap_string: val ppl_max_space_dimension: unit -> int +val ppl_Coefficient_bits: + unit -> int + val ppl_Coefficient_is_bounded: unit -> bool diff --git a/interfaces/Prolog/Prolog_interface.dox b/interfaces/Prolog/Prolog_interface.dox index 485b13f..7a442e4 100644 --- a/interfaces/Prolog/Prolog_interface.dox +++ b/interfaces/Prolog/Prolog_interface.dox @@ -389,6 +389,11 @@ that are included with all instantiations of the Prolog interfaces. warranty whatsoever, the C++ compiler used to build the library, where to report bugs and where to look for further information.</EM> +<P><CODE> ppl_Coefficient_bits </CODE><BR> + + <EM>Unifies the argument with the number of bits used to encode a + Coefficient in the C++ interface; 0 if unbounded.</EM> + <P><CODE> ppl_Coefficient_is_bounded </CODE><BR> <EM>Succeeds if and only if the Coefficients in the C++ interface are bounded.</EM> diff --git a/interfaces/Prolog/ppl_prolog_common.cc b/interfaces/Prolog/ppl_prolog_common.cc index cf55e9a..cd49635 100644 --- a/interfaces/Prolog/ppl_prolog_common.cc +++ b/interfaces/Prolog/ppl_prolog_common.cc @@ -1977,6 +1977,15 @@ ppl_reset_deterministic_timeout() { } extern "C" Prolog_foreign_return_type +ppl_Coefficient_bits(Prolog_term_ref t_bits) { + try { + if (unify_ulong(t_bits, PPL_COEFFICIENT_BITS)) + return PROLOG_SUCCESS; + } + CATCH_ALL; +} + +extern "C" Prolog_foreign_return_type ppl_Coefficient_is_bounded() { try { if (std::numeric_limits<Coefficient>::is_bounded) diff --git a/interfaces/Prolog/ppl_prolog_common.defs.hh b/interfaces/Prolog/ppl_prolog_common.defs.hh index 53a9b63..bf1dfe0 100644 --- a/interfaces/Prolog/ppl_prolog_common.defs.hh +++ b/interfaces/Prolog/ppl_prolog_common.defs.hh @@ -839,6 +839,9 @@ extern "C" Prolog_foreign_return_type ppl_reset_deterministic_timeout(); extern "C" Prolog_foreign_return_type +ppl_Coefficient_bits(Prolog_term_ref t_bits); + +extern "C" Prolog_foreign_return_type ppl_Coefficient_is_bounded(); extern "C" Prolog_foreign_return_type

1 0

[GIT] ppl/ppl(sparse_matrices): MIP_Problem: little optimization in steepest_edge_float_entering_index().
by Marco Poletti 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 19cae9a791014e49edf103f1b3c7ec48eef06059 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=19cae9a79101… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 07:28:05 2010 +0200 MIP_Problem: little optimization in steepest_edge_float_entering_index(). --- src/MIP_Problem.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index a7892fb..6d819cc 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -995,8 +995,8 @@ PPL::MIP_Problem::steepest_edge_float_entering_index() const { if ((*j).first < tableau_num_columns_minus_1) { const dimension_type j_index = (*j).first; const Coefficient& cost_j = working_cost[j_index]; - const Coefficient& tableau_ij = (*j).second; if (sgn(cost_j) == cost_sign) { + const Coefficient& tableau_ij = (*j).second; WEIGHT_BEGIN(); if (tableau_ij != 0) { PPL_ASSERT(tableau_i_base_i != 0);

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Over_CO_Tree: use unordered iterators in normalize().
by Marco Poletti 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: 00e738c7423ee67d5fb85c92251aab37ec66c6dd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=00e738c7423e… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 07:27:19 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: use unordered iterators in normalize(). --- src/Unlimited_Sparse_Row_Over_CO_Tree.cc | 9 +++++---- 1 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Over_CO_Tree.cc b/src/Unlimited_Sparse_Row_Over_CO_Tree.cc index 5d2d708..db3d08a 100644 --- a/src/Unlimited_Sparse_Row_Over_CO_Tree.cc +++ b/src/Unlimited_Sparse_Row_Over_CO_Tree.cc @@ -71,11 +71,11 @@ PPL::Unlimited_Sparse_Row_Over_CO_Tree return true; } -inline void +void PPL::Unlimited_Sparse_Row_Over_CO_Tree::normalize() { // Compute the GCD of all the coefficients. - const_iterator i = begin(); - const const_iterator i_end = end(); + unordered_const_iterator i = unordered_begin(); + unordered_const_iterator i_end = unordered_end(); PPL_DIRTY_TEMP_COEFFICIENT(gcd); for ( ; i != i_end; ++i) { const Coefficient& x_i = i->second; @@ -113,7 +113,8 @@ PPL::Unlimited_Sparse_Row_Over_CO_Tree::normalize() { } } // Divide the coefficients by the GCD. - for (iterator j = begin(), j_end = end(); j != j_end; ++j) { + for (unordered_iterator j = unordered_begin(), j_end = unordered_end(); + j != j_end; ++j) { Coefficient& x_j = j->second; exact_div_assign(x_j, x_j, gcd); }

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row_Over_CO_Tree: un-inline normalize() method.
by Marco Poletti 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: a242fb2c9f20d184e875138841c3d6ab51de26bc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a242fb2c9f20… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 07:26:41 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: un-inline normalize() method. --- src/Unlimited_Sparse_Row_Over_CO_Tree.cc | 50 ++++++++++++++++++++++ src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh | 49 --------------------- 2 files changed, 50 insertions(+), 49 deletions(-) diff --git a/src/Unlimited_Sparse_Row_Over_CO_Tree.cc b/src/Unlimited_Sparse_Row_Over_CO_Tree.cc index 40d2ec8..5d2d708 100644 --- a/src/Unlimited_Sparse_Row_Over_CO_Tree.cc +++ b/src/Unlimited_Sparse_Row_Over_CO_Tree.cc @@ -70,3 +70,53 @@ PPL::Unlimited_Sparse_Row_Over_CO_Tree PPL_ASSERT(OK()); return true; } + +inline void +PPL::Unlimited_Sparse_Row_Over_CO_Tree::normalize() { + // Compute the GCD of all the coefficients. + const_iterator i = begin(); + const const_iterator i_end = end(); + PPL_DIRTY_TEMP_COEFFICIENT(gcd); + for ( ; i != i_end; ++i) { + const Coefficient& x_i = i->second; + if (const int x_i_sign = sgn(x_i)) { + // FIXME: can this be optimized further? + gcd = x_i; + if (x_i_sign < 0) + neg_assign(gcd); + goto compute_gcd; + } + } + // We reach this point only if all the coefficients were zero. + return; + + compute_gcd: + if (gcd == 1) + return; + for (++i; i != i_end; ++i) { + const Coefficient& x_i = i->second; + if (x_i != 0) { + // Note: we use the ternary version instead of a more concise + // gcd_assign(gcd, x_i) to take advantage of the fact that + // `gcd' will decrease very rapidly (see D. Knuth, The Art of + // Computer Programming, second edition, Section 4.5.2, + // Algorithm C, and the discussion following it). Our + // implementation of gcd_assign(x, y, z) for checked numbers is + // optimized for the case where `z' is smaller than `y', so that + // on checked numbers we gain. On the other hand, for the + // implementation of gcd_assign(x, y, z) on GMP's unbounded + // integers we cannot make any assumption, so here we draw. + // Overall, we win. + gcd_assign(gcd, x_i, gcd); + if (gcd == 1) + return; + } + } + // Divide the coefficients by the GCD. + for (iterator j = begin(), j_end = end(); j != j_end; ++j) { + Coefficient& x_j = j->second; + exact_div_assign(x_j, x_j, gcd); + } + PPL_ASSERT(OK()); +} + diff --git a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh index 2bb60b3..65a6020 100644 --- a/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh +++ b/src/Unlimited_Sparse_Row_Over_CO_Tree.inlines.hh @@ -408,55 +408,6 @@ Unlimited_Sparse_Row_Over_CO_Tree::add_zeroes_and_shift(dimension_type n, } inline void -Unlimited_Sparse_Row_Over_CO_Tree::normalize() { - // Compute the GCD of all the coefficients. - const_iterator i = begin(); - const const_iterator i_end = end(); - PPL_DIRTY_TEMP_COEFFICIENT(gcd); - for ( ; i != i_end; ++i) { - const Coefficient& x_i = i->second; - if (const int x_i_sign = sgn(x_i)) { - // FIXME: can this be optimized further? - gcd = x_i; - if (x_i_sign < 0) - neg_assign(gcd); - goto compute_gcd; - } - } - // We reach this point only if all the coefficients were zero. - return; - - compute_gcd: - if (gcd == 1) - return; - for (++i; i != i_end; ++i) { - const Coefficient& x_i = i->second; - if (x_i != 0) { - // Note: we use the ternary version instead of a more concise - // gcd_assign(gcd, x_i) to take advantage of the fact that - // `gcd' will decrease very rapidly (see D. Knuth, The Art of - // Computer Programming, second edition, Section 4.5.2, - // Algorithm C, and the discussion following it). Our - // implementation of gcd_assign(x, y, z) for checked numbers is - // optimized for the case where `z' is smaller than `y', so that - // on checked numbers we gain. On the other hand, for the - // implementation of gcd_assign(x, y, z) on GMP's unbounded - // integers we cannot make any assumption, so here we draw. - // Overall, we win. - gcd_assign(gcd, x_i, gcd); - if (gcd == 1) - return; - } - } - // Divide the coefficients by the GCD. - for (iterator j = begin(), j_end = end(); j != j_end; ++j) { - Coefficient& x_j = j->second; - exact_div_assign(x_j, x_j, gcd); - } - PPL_ASSERT(OK()); -} - -inline void Unlimited_Sparse_Row_Over_CO_Tree::assign(dimension_type i, const Coefficient& x) { if (tree.empty())

1 0

[GIT] ppl/ppl(sparse_matrices): CO_Tree: set max_density to 0.9.
by Marco Poletti 15 Apr '10

15 Apr '10

Module: ppl/ppl Branch: sparse_matrices Commit: bed3dbc5976ca171924cc9950a4c0160c4d05734 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bed3dbc5976c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Apr 15 06:53:21 2010 +0200 CO_Tree: set max_density to 0.9. --- src/CO_Tree.defs.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/CO_Tree.defs.hh b/src/CO_Tree.defs.hh index 5fdc636..c027cf6 100644 --- a/src/CO_Tree.defs.hh +++ b/src/CO_Tree.defs.hh @@ -508,7 +508,7 @@ private: //! The maximum density of used nodes. //! Must be greater than or equal to 0.5 and lower than 1. - static const float max_density = 0.5; + static const float max_density = 0.9; //! The minimum density of used nodes. //! Must be strictly lower than max_density.

1 0