- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Simplified PPL_DIRTY_TEMP.
by Abramo Bagnara 11 Jul '11

11 Jul '11

Module: ppl/ppl Branch: master Commit: 8e3ada8b858375f122c324662f40d5b6a4c5afd0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8e3ada8b8583… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Mon Jul 11 14:07:46 2011 +0200 Simplified PPL_DIRTY_TEMP. --- interfaces/Prolog/SWI/swi_efli.cc | 4 +- src/BD_Shape.templates.hh | 28 ++++++++-------- src/Bit_Row.inlines.hh | 2 +- src/Box.inlines.hh | 6 ++-- src/Box.templates.hh | 62 ++++++++++++++++++------------------ src/Generator.inlines.hh | 8 ++-- src/Interval_Restriction.defs.hh | 4 +- src/MIP_Problem.cc | 6 ++-- src/Octagonal_Shape.templates.hh | 32 +++++++++--------- src/Polyhedron_nonpublic.cc | 6 ++-- src/Polyhedron_public.cc | 8 ++-- src/Temp.defs.hh | 32 ++----------------- src/Temp.inlines.hh | 12 ++----- src/checked.inlines.hh | 2 +- src/checked_int.inlines.hh | 2 +- src/checked_mpz.inlines.hh | 4 +- src/conversion.cc | 2 +- src/fpu-ia32.cc | 16 +++++----- src/globals.defs.hh | 2 +- src/math_utilities.inlines.hh | 8 ++-- 20 files changed, 107 insertions(+), 139 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=8e3ada8b…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Adjusted documentation and formatting code.
by Alberto Gioia 10 Jul '11

10 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 25524c60cb8991ab2dbd38e16da3c994c36b75ab URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=25524c60cb89… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sun Jul 10 20:33:39 2011 +0200 Adjusted documentation and formatting code. --- doc/definitions.dox | 343 +++++++--------- src/Interval.defs.hh | 4 +- src/Interval.inlines.hh | 629 +++++++++++++++------------ src/Linear_Form.templates.hh | 433 +++++++++++-------- src/linearize.hh | 2 +- src/linearize_integer.hh | 979 +++++++++++++++++++++--------------------- 6 files changed, 1251 insertions(+), 1139 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=25524c60…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Renamed Intero_Interval into Integer_Int_Interval
by Alberto Gioia 10 Jul '11

10 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: b43f03e4182a8fb2f604f77b7f89ff7d4a938a17 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b43f03e4182a… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sun Jul 10 20:28:14 2011 +0200 Renamed Intero_Interval into Integer_Int_Interval --- tests/Concrete_Expression/C_Expr.defs.hh | 10 +- tests/Concrete_Expression/C_Expr.inlines.hh | 2 +- tests/Concrete_Expression/linearize_int.cc | 1084 ++++++++++++++------------- tests/ppl_test.hh | 6 +- 4 files changed, 578 insertions(+), 524 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=b43f03e4…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Deleted white space.
by Alberto Gioia 10 Jul '11

10 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: dc0a74c74cb57a6bf8a92e0f2843d2e34545a9f6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dc0a74c74cb5… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Sun Jul 10 20:23:17 2011 +0200 Deleted white space. --- tests/Concrete_Expression/digitalfilters1.cc | 10 +++++----- 1 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/Concrete_Expression/digitalfilters1.cc b/tests/Concrete_Expression/digitalfilters1.cc index d0fcf3e..8b4d9fa 100644 --- a/tests/Concrete_Expression/digitalfilters1.cc +++ b/tests/Concrete_Expression/digitalfilters1.cc @@ -49,7 +49,7 @@ public: } bool get_integer_constant_value(const Integer_Constant<C_Expr>&, - FP_Interval&) const { + FP_Interval&) const { return false; } @@ -76,7 +76,7 @@ public: result = expr.dimensions; return true; } - + FP_Interval_Abstract_Store int_store; }; @@ -556,7 +556,7 @@ test05() { tmp.lower() = 0; tmp.upper() = 16; oracle.int_store.affine_form_image(D, FP_Linear_Form(tmp)); - bd.affine_form_image(D, FP_Linear_Form(tmp)); + bd.affine_form_image(D, FP_Linear_Form(tmp)); oracle.int_store.intersection_assign(FP_Interval_Abstract_Store(bd)); // S = Y; @@ -765,7 +765,7 @@ test06() { tmp.lower() = 0; tmp.upper() = 16; oracle.int_store.affine_form_image(D, FP_Linear_Form(tmp)); - oc.affine_form_image(D, FP_Linear_Form(tmp)); + oc.affine_form_image(D, FP_Linear_Form(tmp)); oracle.int_store.intersection_assign(FP_Interval_Abstract_Store(oc)); // S = Y; @@ -974,7 +974,7 @@ test07() { tmp.lower() = 0; tmp.upper() = 16; oracle.int_store.affine_form_image(D, FP_Linear_Form(tmp)); - ph.affine_form_image(D, FP_Linear_Form(tmp)); + ph.affine_form_image(D, FP_Linear_Form(tmp)); oracle.int_store.intersection_assign(FP_Interval_Abstract_Store(ph)); // S = Y;

1 0

Fwd: Re: Polyhedra formats and ppl_lcdd
by Roberto Bagnara 10 Jul '11

10 Jul '11

-------- Original Message -------- Subject: Re: [PPL-devel] Polyhedra formats and ppl_lcdd Date: Sat, 9 Jul 2011 18:18:13 +0200 From: Ramakrishna Upadrasta <uramakrishna(a)gmail.com> To: Roberto Bagnara <bagnara(a)cs.unipr.it>, Enea Zaffanella <zaffanella(a)cs.unipr.it> Hi Roberto and Enea, Thanks for the quick response. I appreciate it. More on this subject later! Regards Ramakrishna 2011/7/8 Roberto Bagnara <bagnara(a)cs.unipr.it>: > On 07/08/11 16:17, Ramakrishna Upadrasta wrote: >> >> Hello PPL Users, > > Hi Ramakrishna. > >> I have been interested in performance of different polyhedra libraries >> and was pleasantly surprised to find the following page: >> http://www.cs.unipr.it/ppl/performance >> >> I have a couple of points/questions on the same. >> >> 1. Where can I find the file ppl_lcdd.cc? > > In a PPL source distribution. > >> Does it convert polyhedra of >> format X into Y, where X and Y are in {PolyLib, PPL, CDDLib}? > > No. > >> How can it be used? > > After installation of the PPL, see `man ppl_lcdd'. > If you prefer not to install, then do > > nroff -man ppl_lcdd.1 | less > >> 2. The link to the code to ppl_lcdd.cc seems to be broken and may need >> to be fixed. I am not sure if the doc files talk about it. > > Fixed: thanks! > >> 3. Has the comparison been updated? The dates seem to refer to 2009. >> Please refer me to a recent version of the same, if available. > > No, it has not been updated. But you can reproduce it. > See the lines > > //#define USE_POLKA 1 > //#define USE_POLYLIB 1 > > at the beginning of ppl_lcdd.cc. And of course, you should first install > the right versions of New Polka and PolyLib. > Please let us know how it goes and if you run into problems. > >> Thanks for help in this! > > Our pleasure. > Cheers, > > Roberto > > P.S. What you are working on? We would be glad to know. > > -- > Prof. Roberto Bagnara > Applied Formal Methods Laboratory > Department of Mathematics, University of Parma, Italy > http://www.cs.unipr.it/~bagnara/ > mailto:bagnara@cs.unipr.it >

1 0

[GIT] ppl/ppl(master): Silenced a couple of gcc warnings.
by Enea Zaffanella 09 Jul '11

09 Jul '11

Module: ppl/ppl Branch: master Commit: d0e687c142a12f08873f953e16c32265536b67f2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d0e687c142a1… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Jul 9 18:32:45 2011 +0200 Silenced a couple of gcc warnings. --- src/PIP_Tree.cc | 2 +- src/Sparse_Row.cc | 2 ++ 2 files changed, 3 insertions(+), 1 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 35590cf..3aa76b8 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -134,7 +134,7 @@ merge_assign(Matrix& x, const Constraint_System& y, Row& x_i = x[i]; Coefficient_traits::const_reference inhomogeneous_term = y_i->inhomogeneous_term(); - Variables_Set::const_iterator pj = parameters.begin(); + Variables_Set::const_iterator pj = param_begin; dimension_type j = 1; Row::iterator itr = x_i.end(); if (inhomogeneous_term != 0) diff --git a/src/Sparse_Row.cc b/src/Sparse_Row.cc index 157e992..2760e53 100644 --- a/src/Sparse_Row.cc +++ b/src/Sparse_Row.cc @@ -440,7 +440,9 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, // invalidates all iterators. while (i != end()) { if (*i == 0) { +#ifndef NDEBUG const dimension_type old_index = i.index(); +#endif i = reset(i); PPL_ASSERT(find(old_index) == end()); } else

1 0

MIP or PIP for testing satisfiability of linear arithmetic constraints over the integers
by Fred Mesnard 09 Jul '11

09 Jul '11

Hi all, I plan to use PPL for testing satisfiability of linear arithmetic constraints over the integers. I'm using PPL 0.11.2 with the latest SWI-Prolog. I found two unexpected results, see below, and I'm stuck! I'd like to have your feedback. Thanks in advance! Fred With MIP, here's my Prolog code: z_MIP_satisfiable(Cs) :- user:my_term_variables(Cs,Vars), length(Vars,Dim), user:ppl_new_MIP_Problem_from_space_dimension(Dim,Handle), translate_constraints_BT_ppl(Vars,Cs,PPL_Cs,PPL_Vs), user:ppl_MIP_Problem_add_constraints(Handle,PPL_Cs), user:ppl_MIP_Problem_add_to_integer_space_dimensions(Handle,PPL_Vs), ( user:ppl_MIP_Problem_is_satisfiable(Handle) -> user:ppl_delete_MIP_Problem(Handle) ; user:ppl_delete_MIP_Problem(Handle), fail). In general, it works well but trying z_MIP_satisfiable([X=2*Z, X=2*Y+1]). ie find X both even and odd does not seem to terminate. By the way, which kind of algorithm did you implement for MIP? With PIP, here's my Prolog code, quite similar to the previous one: z_PIP_satisfiable(Cs) :- user:my_term_variables(Cs,Vars), length(Vars,Dim), user:ppl_new_PIP_Problem_from_space_dimension(Dim,Handle), translate_constraints_BT_ppl(Vars,Cs,PPL_Cs,_PPL_Vs), user:ppl_PIP_Problem_add_constraints(Handle,PPL_Cs), ( user:ppl_PIP_Problem_is_satisfiable(Handle) -> user:ppl_delete_PIP_Problem(Handle) ; user:ppl_delete_PIP_Problem(Handle), fail). Trying z_PIP_satisfiable([ X =< -1]). ie find X less than -1 fails. Idem for -2, -3, ... So for PIP, variables are all implicitly >= 0? Cordialement, Fred Mesnard http://personnel.univ-reunion.fr/fred/

2 1

#625417 - ppl: ftbfs with gcc-4.6 -Werror - Debian Bug report logs
by Roberto Bagnara 09 Jul '11

09 Jul '11

http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=625417 -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Polyhedra formats and ppl_lcdd
by Ramakrishna Upadrasta 08 Jul '11

08 Jul '11

Hello PPL Users, I have been interested in performance of different polyhedra libraries and was pleasantly surprised to find the following page: http://www.cs.unipr.it/ppl/performance I have a couple of points/questions on the same. 1. Where can I find the file ppl_lcdd.cc? Does it convert polyhedra of format X into Y, where X and Y are in {PolyLib, PPL, CDDLib}? How can it be used? 2. The link to the code to ppl_lcdd.cc seems to be broken and may need to be fixed. I am not sure if the doc files talk about it. 3. Has the comparison been updated? The dates seem to refer to 2009. Please refer me to a recent version of the same, if available. Thanks for help in this! Regards Ramakrishna

3 2

[GIT] ppl/w3ppl(master): Links updated.
by Roberto Bagnara 08 Jul '11

08 Jul '11

Module: ppl/w3ppl Branch: master Commit: 6f625e83a00f4ab6eadb826e4a941f901a319fa5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=6f625e83a0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jul 8 17:34:55 2011 +0200 Links updated. --- htdocs/performance.raw | 200 ++++++++++++++++++++++++------------------------ 1 files changed, 100 insertions(+), 100 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commitdiff;h=6f625e…

1 0