July 2011 - PPL-devel - BUGSENG Mailman

[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

[GIT] ppl/ppl(bounded_arithmetic): Fixed noisy output.
by Alberto Gioia 07 Jul '11

07 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 1dd5888b9a8011279e1caf76c49f990f9e59108f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1dd5888b9a80… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Thu Jul 7 17:50:59 2011 +0200 Fixed noisy output. --- tests/Concrete_Expression/linearize_int.cc | 330 +++++++++++++--------------- 1 files changed, 156 insertions(+), 174 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=1dd5888b…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Fixed bitwise functions.
by Alberto Gioia 07 Jul '11

07 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 278e38a3ad8616c33c6c73b1088a105d64029ed8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=278e38a3ad86… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Thu Jul 7 17:48:46 2011 +0200 Fixed bitwise functions. --- src/Linear_Form.templates.hh | 121 +++++++++++++++++++++++------------------- 1 files changed, 67 insertions(+), 54 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=278e38a3…

1 0

[GIT] ppl/ppl(bounded_arithmetic): Fixed functions lshift_assign and rshift_assign.
by Alberto Gioia 07 Jul '11

07 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: d8fca333c422bb111a15b8c812341f8eb0ffc65d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d8fca333c422… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Thu Jul 7 17:46:53 2011 +0200 Fixed functions lshift_assign and rshift_assign. --- src/Interval.inlines.hh | 28 ++++++++++++++-------------- 1 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/Interval.inlines.hh b/src/Interval.inlines.hh index af1a146..402d815 100644 --- a/src/Interval.inlines.hh +++ b/src/Interval.inlines.hh @@ -1107,7 +1107,7 @@ Interval<To_Boundary, To_Info>::lshift_assign(const From1& x, const From2& y) { } } /* xls >= 0, yus < 0 - 0 <= x << y <= x/(2^y) + 0 <= x << y <= x/(2^|y|) */ else if (yus < 0 ) { @@ -1128,10 +1128,10 @@ Interval<To_Boundary, To_Info>::lshift_assign(const From1& x, const From2& y) { else if (xus < 0 ) { Boundary_NS::assign(UPPER, upper() , to_info, - UPPER, f_upper(Constant<-1>::value), - f_info(Constant<-1>::value)); + UPPER, f_upper(Constant<0>::value), + f_info(Constant<0>::value)); /* xus < 0, yls >= 0 - x*(2^y) <= x << y <= -1 + x*(2^y) <= x << y <= 0 */ if(yls >= 0) { mpz_class tmp_exp((int)ldexp(1.0, f_lower(y))); @@ -1147,7 +1147,7 @@ Interval<To_Boundary, To_Info>::lshift_assign(const From1& x, const From2& y) { } } /* xus < 0, yus < 0 - x/(2^y) <= x << y <= -1 + x/(2^|y|) <= x << y <= 0 */ else if (yus < 0) { @@ -1165,8 +1165,8 @@ Interval<To_Boundary, To_Info>::lshift_assign(const From1& x, const From2& y) { UPPER, f_upper(y), f_info(y)); if (lower() > -1) Boundary_NS::assign(LOWER, lower(), to_info, - LOWER, f_lower(Constant<-1>::value), - f_info(Constant<-1>::value)); + LOWER, f_lower(Constant<0>::value), + f_info(Constant<0>::value)); } @@ -1209,7 +1209,7 @@ Interval<To_Boundary, To_Info>::rshift_assign(const From1& x, const From2& y) { else if (yus < 0) { /* xls >= 0, yus < 0 - 0 <= x >> y <= x*(2^y) + 0 <= x >> y <= x*(2^|y|) */ PPL_DIRTY_TEMP(To_Boundary, tmp_upper); PPL_DIRTY_TEMP(To_Info, tmp_info); @@ -1228,26 +1228,26 @@ Interval<To_Boundary, To_Info>::rshift_assign(const From1& x, const From2& y) { else if (xus < 0) { Boundary_NS::assign(UPPER, upper() , to_info, - UPPER, f_upper(Constant<-1>::value), - f_info(Constant<-1>::value)); + UPPER, f_upper(Constant<0>::value), + f_info(Constant<0>::value)); if(yls >= 0) { /* xls < 0, yus >= 0 - x/(2^y) <= x >> y <= -1 + x/(2^y) <= x >> y <= 0 */ Boundary_NS::div_assign(LOWER, lower(), to_info, LOWER, f_lower(x), f_info(x), LOWER, f_lower(y), f_info(y)); if (lower() > -1) Boundary_NS::assign(LOWER, lower(), to_info, - LOWER, f_lower(Constant<-1>::value), - f_info(Constant<-1>::value)); + LOWER, f_lower(Constant<0>::value), + f_info(Constant<0>::value)); } else if (yus < 0) { /* xus < 0, yus < 0 - x*(2^y) <= x >> y <= -1 + x*(2^|y|) <= x >> y <= 0 */ PPL_DIRTY_TEMP(To_Boundary, tmp_lower); PPL_DIRTY_TEMP(To_Info, tmp_info);

1 0

[GIT] ppl/ppl(bounded_arithmetic): Corrected documentation.
by Alberto Gioia 07 Jul '11

07 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: d3a4393da2940e2ab9fe2af718aecb7de6dda2f7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d3a4393da294… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Thu Jul 7 17:41:12 2011 +0200 Corrected documentation. --- doc/definitions.dox | 28 +++++++++++++------------- src/linearize_integer.hh | 48 +++++++++++++++++++++++----------------------- 2 files changed, 38 insertions(+), 38 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 9b997ed..8735398 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2858,9 +2858,9 @@ The interval bitwise operators are defined as follow: \left[a,b\right] \olessthan ^{\#} \left[a',b'\right] \approx \begin{cases} \left[0, \left(b \amifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } a' \geq 0 \\ - \left[0, \left(b \adivifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\ - \left[\left(a \amifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\ - \left[\left(a \adivifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\ + \left[0, \left(b \adivifp 2^{\left|b'\right|}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\ + \left[\left(a \amifp 2^{a'}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\ + \left[\left(a \adivifp 2^{\left|a'\right|}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\ \end{cases} @@ -2872,9 +2872,9 @@ The interval bitwise operators are defined as follow: \left[a,b\right] \ogreaterthan ^{\#} \left[a',b'\right] \approx \begin{cases} \left[0, \left(b \adivifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } a' \geq 0 \\ - \left[0, \left(b \amifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\ - \left[\left(a \adivifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\ - \left[\left(a \amifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\ + \left[0, \left(b \amifp 2^{\left|b'\right|}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\ + \left[\left(a \adivifp 2^{a'}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\ + \left[\left(a \amifp 2^{\left|a'\right|}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\ \end{cases} @@ -3101,7 +3101,7 @@ have discordand signs, with the first greater than or equal zero, then \leq \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf - 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} + 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} \f] @@ -3117,7 +3117,7 @@ have discordand signs, with the first less than zero, then \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] @@ -3128,11 +3128,11 @@ both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \left(i + \sum_{v \in \cV}i_{v}v \right) \adivlf - 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} + 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] @@ -3176,7 +3176,7 @@ have discordand signs, with the first greater than or equal zero, then \leq \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf - 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} + 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} \f] @@ -3192,7 +3192,7 @@ have discordand signs, with the first less than zero, then \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] Finally, if \f$i + \sum_{v \in V}i_{v}v\f$ and \f$i' + \sum_{v \in V}i'_{v}v\f$ are @@ -3202,11 +3202,11 @@ both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by: \left(i + \sum_{v \in \cV}i_{v}v \right) \amlf - 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)} + 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)} \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] diff --git a/src/linearize_integer.hh b/src/linearize_integer.hh index 1b6a9de..1a0f625 100644 --- a/src/linearize_integer.hh +++ b/src/linearize_integer.hh @@ -1413,7 +1413,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq x \ll y \leq - -1 + 0 \f] Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -1438,7 +1438,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] and we can define the elments of the linear form @@ -1449,7 +1449,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k \leq - -1 + 0 \f] \f[ @@ -1457,7 +1457,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k_{v} \leq - -1 + 0 \f] then @@ -1467,7 +1467,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i \amifp 2^{i'} \right) \bowtie - -1 + 0 \f] \f[ @@ -1475,7 +1475,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i_{v} \amifp 2^{i'_{v}} \right) \bowtie - -1 + 0 \f] Finally, let \f$x\f$ and \f$y\f$ be two integer constants both less then zero, @@ -1486,7 +1486,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq x \ll y \leq - -1 + 0 \f] Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -1511,7 +1511,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] and we can define the elments of the linear form @@ -1522,7 +1522,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k \leq - -1 + 0 \f] \f[ @@ -1530,7 +1530,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k_{v} \leq - -1 + 0 \f] then @@ -1540,7 +1540,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i \adivifp 2^{i'} \right) \bowtie - -1 + 0 \f] \f[ @@ -1548,7 +1548,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i_{v} \adivifp 2^{i'_{v}} \right) \bowtie - -1 + 0 \f] Given an expression \f$e_{1} \leftslice e_{2}\f$ and a composite @@ -1769,7 +1769,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq x \gg y \leq - -1 + 0 \f] Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -1794,7 +1794,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] and we can define the elments of the linear form @@ -1805,7 +1805,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k \leq - -1 + 0 \f] \f[ @@ -1813,7 +1813,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k_{v} \leq - -1 + 0 \f] then @@ -1823,7 +1823,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i \adivifp 2^{i'} \right) \bowtie - -1 + 0 \f] \f[ @@ -1831,7 +1831,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i_{v} \adivifp 2^{i'_{v}} \right) \bowtie - -1 + 0 \f] Finally, let \f$x\f$ and \f$y\f$ be two integer constants both less @@ -1842,7 +1842,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq x \gg y \leq - -1 + 0 \f] Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and @@ -1867,7 +1867,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq \left(k + \sum_{v \in \cV}k_{v}v \right) \leq - -1 + 0 \f] and we can define the elments of the linear form @@ -1878,7 +1878,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k \leq - -1 + 0 \f] \f[ @@ -1886,7 +1886,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \leq k_{v} \leq - -1 + 0 \f] then @@ -1896,7 +1896,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i \amifp 2^{i'} \right) \bowtie - -1 + 0 \f] \f[ @@ -1904,7 +1904,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr, \approx \left(i_{v} \amifp 2^{i'_{v}} \right) \bowtie - -1 + 0 \f] Given an expression \f$e_{1} \rightslice e_{2}\f$ and a composite

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added documentation on Bitwise operators .
by Alberto Gioia 05 Jul '11

05 Jul '11

Module: ppl/ppl Branch: bounded_arithmetic Commit: 572a074935fdf80b394a5242f42f9615dbd74ca7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=572a074935fd… Author: Alberto Gioia <alberto.gioia1(a)studenti.unipr.it> Date: Tue Jul 5 19:34:27 2011 +0200 Added documentation on Bitwise operators. --- doc/definitions.dox | 448 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 448 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=572a0749…

1 0