- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): The `|' character cannot be used to produce proper paired delimiters.
by Roberto Bagnara 24 Mar '10

24 Mar '10

Module: ppl/ppl Branch: master Commit: cb165556dd22a919425ed9803156dfcb63896f62 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cb165556dd22… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Mar 24 06:43:33 2010 +0400 The `|' character cannot be used to produce proper paired delimiters. --- doc/definitions.dox | 17 +++++++++-------- doc/ppl.sty | 3 +++ 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 1a2a048..6e9ec24 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2211,11 +2211,12 @@ the frequency \f$f\f$ and a value \f$\mathrm{val} = \langle \vect{a}, \vect{w} \rangle + b\f$ where \f$\vect{w} \in \cL\f$ and \f[ - |\mathrm{val}| - = \min\Bigl\{\, - \big|\langle \vect{a}, \vect{v} \rangle + b - \big| \Bigm| \vect{v} \in \cL - \,\Bigr\}. + \lvert\mathrm{val}\rvert + = \min\Bigl\{\, + \bigl\lvert\langle \vect{a}, \vect{v} \rangle + b \bigr\rvert + \Bigm| + \vect{v} \in \cL + \,\Bigr\}. \f] Observe that the above definition is also applied to other simple objects in @@ -4786,13 +4787,13 @@ For \f$x\f$, \f$y \in \Zset\f$ with \f$y \ne 0\f$, we have x \brem y = \begin{cases} - x \brem |y|, & \text{if $x \ge 0$;} \\ - -(|x| \brem |y|), & \text{if $x < 0$.} + x \brem \abs{y}, & \text{if $x \ge 0$;} \\ + -(\abs{x} \brem \abs{y}), & \text{if $x < 0$.} \end{cases} \f] <B><EM>Proof</EM></B> -Throughout the proof we write \f$x_0 = |x|\f$ and \f$y_0 = |y|\f$. +Throughout the proof we write \f$x_0 = \abs{x}\f$ and \f$y_0 = \abs{y}\f$. First, assume that \f$x \ge 0\f$ and that \f$y < 0\f$. Let \f$k = \phi(x / y_0) = - \phi(x / y)\f$, by the property above. We have diff --git a/doc/ppl.sty b/doc/ppl.sty index 0678319..43fc889 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -136,6 +136,9 @@ \newcommand*{\relsym}{\mathrel{\bowtie}} \newcommand*{\relsyms}[1]{\mathrel{\bowtie_{#1}}} +% Absolute value. +\newcommand*{\abs}[1]{\lvert #1 \rvert} + % Vectors. \renewcommand*{\vec}[1]{\mathchoice{\mbox{\boldmath$\displaystyle#1$}} {\mbox{\boldmath$\textstyle#1$}}

1 0

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

23 Mar '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e3ac94be0dd3… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 22:26:34 2010 +0100 PIP_Tree.cc: use combine_needs_second() instead of combine() in sub_assign(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fceb46357849… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 22:24:39 2010 +0100 PIP_Tree.cc: use combine_needs_second() instead of combine() in add_mul_assign_row(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1efca9aac7a4… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 22:23:56 2010 +0100 Dense_Row: add combine_needs_first() and combine_needs_second() methods. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4b51fe286c9f… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 22:23:39 2010 +0100 Sparse_Row, Sparse_Row_Reference: add combine_needs_first() and combine_needs_second() methods. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b31687efa4e8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 22:22:56 2010 +0100 Unlimited_Sparse_Row: add combine_needs_first() and combine_needs_second() methods. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3c1f288ed80b… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 21:45:24 2010 +0100 MIP_Problem: use combine() in second version of linear_combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b91ce9e6ec4c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 21:44:48 2010 +0100 Unlimited_Sparse_Row: fixed combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7b528ee1b7d5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 21:32:01 2010 +0100 MIP_Problem: use combine() in first version of linear_combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=33111f08cee4… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 20:46:14 2010 +0100 PIP_Tree.cc: use combine() in add_mul_assign_row(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=596cd44e2e88… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 20:38:20 2010 +0100 PIP_Tree.cc: use combine() in sub_assign(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c08d49d36531… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 20:30:51 2010 +0100 Dense_Row: add combine() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=97c282e3c08e… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 20:30:01 2010 +0100 Sparse_Row, Sparse_Row_Reference: add combine() methods. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0cae2dd38b9a… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 20:28:18 2010 +0100 Unlimited_Sparse_Row: add method combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f81397772770… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 18:57:30 2010 +0100 PIP_Solution_Node: cache value s_i[pj] instead of accessing it multiple times, in solve(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=940a6a194d39… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 18:44:48 2010 +0100 PIP_Solution_Node: sort using std::sort on a vector instead of using std::map, in update_tableau(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d3b3541b223d… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 18:36:23 2010 +0100 PIP_Solution_Node: use find_create() instead of operator[], in update_tableau().

1 0

[GIT] ppl/ppl(master): Added implementations for the original PR termination tests.
by Enea Zaffanella 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 490971b3d76a92e448803fa6437ca8e08abb7955 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=490971b3d76a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Mar 23 19:22:14 2010 +0100 Added implementations for the original PR termination tests. These are activated when the preprocessor flag USE_ORIGINAL_PR_METHOD is set. The flag is now active. --- src/termination.cc | 227 +++++++++++++++++++++++++++++++++++++++++- src/termination.templates.hh | 34 ++++++ 2 files changed, 259 insertions(+), 2 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=490971b3…

1 0

[GIT] ppl/ppl(master): Improved documentation for frequency.
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: aa99fbdd05ff71b6ddd9ace3d7401ca4a967af5b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aa99fbdd05ff… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 17:51:20 2010 +0000 Improved documentation for frequency. --- doc/definitions.dox | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 6d9a73b..1a2a048 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2212,10 +2212,10 @@ the frequency \f$f\f$ and a value where \f$\vect{w} \in \cL\f$ and \f[ |\mathrm{val}| - = \min\Bigl\{ + = \min\Bigl\{\, \big|\langle \vect{a}, \vect{v} \rangle + b \big| \Bigm| \vect{v} \in \cL - \Bigr\}. + \,\Bigr\}. \f] Observe that the above definition is also applied to other simple objects in

1 0

[GIT] ppl/ppl(master): Type error fixed.
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 6821ba41f0d1c8a8f08c839fe33781e5a2f7b314 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6821ba41f0d1… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 17:38:48 2010 +0000 Type error fixed. --- .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 index 5ec23cd..1922588 100644 --- a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 +++ b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 @@ -1348,7 +1348,7 @@ ppl_@CLASS@_wrap_assign_native build_ppl_bounded_integer_type_overflow(oflow); Constraint_System ppl_cs = build_ppl_Constraint_System(cs); unsigned ppl_complexity = value_to_unsigned<unsigned>(complexity); - bool ppl_wrap_ind = Int_val(wrap_ind); + bool ppl_wrap_ind = Bool_val(wrap_ind); pph.wrap_assign(ppl_vset, build_ppl_bounded_integer_type_width(width), build_ppl_bounded_integer_type_representation(rep),

1 0

[GIT] ppl/ppl(master): Added interface code for wrap_assign().
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 8e9040044889a3a72c7c496827236916ae717b24 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8e9040044889… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 17:31:12 2010 +0000 Added interface code for wrap_assign(). --- .../ppl_interface_generator_sicstus_sd_cc.m4 | 57 ++++++ .../ppl_interface_generator_prolog_cc_code.m4 | 74 ++++++++ .../ppl_interface_generator_prolog_hh_code.m4 | 14 ++ ...erface_generator_prolog_procedure_generators.m4 | 1 + interfaces/Prolog/ppl_prolog_common.cc | 179 ++++++++++++++++++++ interfaces/Prolog/ppl_prolog_common.defs.hh | 79 +++++++++ ...face_generator_prolog_generated_test_pl_code.m4 | 20 +++ 7 files changed, 424 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=8e904004…

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: bc6dffb591691b0986eb73aad6214d8e15ed630c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bc6dffb59169… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 17:30:05 2010 +0000 Typo fixed. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 403cf99..6d9a73b 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2214,7 +2214,7 @@ where \f$\vect{w} \in \cL\f$ and |\mathrm{val}| = \min\Bigl\{ \big|\langle \vect{a}, \vect{v} \rangle + b - \bigm| \Big| \vect{v} \in \cL + \big| \Bigm| \vect{v} \in \cL \Bigr\}. \f]

1 0

[GIT] ppl/ppl(master): Wrong latex fixed.
by Patricia Hill 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 706a703a5546abc8c54fc35ad2c2574429aadc40 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=706a703a5546… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue Mar 23 16:49:55 2010 +0000 Wrong latex fixed. --- doc/definitions.dox | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 469ce91..403cf99 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2214,7 +2214,7 @@ where \f$\vect{w} \in \cL\f$ and |\mathrm{val}| = \min\Bigl\{ \big|\langle \vect{a}, \vect{v} \rangle + b - \big| \Big| \vect{v} \in \cL + \bigm| \Big| \vect{v} \in \cL \Bigr\}. \f]

1 0

[GIT] ppl/ppl(master): Added two new tests.
by Roberto Bagnara 23 Mar '10

23 Mar '10

Module: ppl/ppl Branch: master Commit: 418e4ff3dc14d5c18445ca52c0668c8eb2d68289 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=418e4ff3dc14… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Mar 23 20:01:58 2010 +0400 Added two new tests. --- tests/Polyhedron/termination1.cc | 68 ++++++++++++++++++++++++++++++++++++++ 1 files changed, 68 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/termination1.cc b/tests/Polyhedron/termination1.cc index b17af5b..0d86c03 100644 --- a/tests/Polyhedron/termination1.cc +++ b/tests/Polyhedron/termination1.cc @@ -425,6 +425,72 @@ test18() { return !termination_test_PR(ph); } +bool +test19() { + Variable D(0); + Variable E(1); + Variable F(2); + Variable A(3); + Variable B(4); + Variable C(5); + C_Polyhedron ph(6); + + ph.add_constraint(A == D); + ph.add_constraint(B == E); + ph.add_constraint(B - F >= 0); + ph.add_constraint(A - F >= 0); + ph.add_constraint(C >=0); + ph.add_constraint(C - F <= -1); + + Generator witness(point()); + one_affine_ranking_function_PR(ph, witness); + + print_generator(witness, "*** witness ***"); + + Variable mu1(0); + Variable mu2(1); + Variable mu3(2); + Variable mu0(3); + Generator known_result(point(0*mu0 + 1*mu1 - 1*mu3)); + + print_generator(known_result, "*** known_result ***"); + + return known_result == witness; +} + +bool +test20() { + Variable D(0); + Variable E(1); + Variable F(2); + Variable A(3); + Variable B(4); + Variable C(5); + C_Polyhedron ph(6); + + ph.add_constraint(A == D); + ph.add_constraint(B == E); + ph.add_constraint(B - F >= 0); + ph.add_constraint(A - F >= 0); + ph.add_constraint(C >=0); + ph.add_constraint(C - F <= -1); + + Generator witness(point()); + one_affine_ranking_function_MS(ph, witness); + + print_generator(witness, "*** witness ***"); + + Variable mu1(0); + Variable mu2(1); + Variable mu3(2); + Variable mu0(3); + Generator known_result(point(-1*mu0 + 1*mu1 - 1*mu3)); + + print_generator(known_result, "*** known_result ***"); + + return known_result == witness; +} + } // namespace BEGIN_MAIN @@ -446,4 +512,6 @@ BEGIN_MAIN DO_TEST(test16); DO_TEST(test17); DO_TEST(test18); + DO_TEST(test19); + DO_TEST(test20); END_MAIN

1 0

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

23 Mar '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fa2e479513ed… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 16:00:22 2010 +0100 PIP_Solution_Node: use two-argument add_zero_columns() in update_tableau() method. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=372e574ca99b… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:59:29 2010 +0100 Dense_Matrix: add two-argument add_zero_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a9eb5d2e74da… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:59:06 2010 +0100 Dense_Matrix: fix assertion in permute_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c9300432feb8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:57:16 2010 +0100 Sparse_Matrix: add two-argument add_zero_columns(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=52721116a3dd… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:56:34 2010 +0100 Unlimited_Sparse_Row: add method add_zeroes_and_shift(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7e8eabade51c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:08:28 2010 +0100 PIP_Tree_Node: use the newer find_create() versions in compatibility_check(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d67a9ccb10f… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Tue Mar 23 15:07:46 2010 +0100 Dense_Row: add other versions of find_create().

1 0