- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(ppl-0_12-branch): Recompute the sign of the special_equality_row after modyfying it.
by Enea Zaffanella 05 May '12

05 May '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: cbc2fc98c3af5eed865648ce953553d69f5ef637 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cbc2fc98c3af… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 4 10:13:05 2012 +0200 Recompute the sign of the special_equality_row after modyfying it. This fixes the bug shown by test04() in tests/PIP_Problem/pipproblem3.cc. --- src/PIP_Tree.cc | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index f434d7d..7ce9848 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -2424,6 +2424,7 @@ PIP_Solution_Node const dimension_type m_eq = mapping[special_equality_row]; sub_assign(tableau.s[m_eq], v_row); sub_assign(tableau.t[m_eq], p_row); + sign[m_eq] = row_sign(tableau.t[m_eq], big_dimension); } } }

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Inclusions reordered to match the PPL coding standard.
by Roberto Bagnara 05 May '12

05 May '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: f70936756efd067c891ac1a24a44fa4d56af343a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f70936756efd… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 5 14:08:35 2012 +0200 Inclusions reordered to match the PPL coding standard. --- src/Watchdog.inlines.hh | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) diff --git a/src/Watchdog.inlines.hh b/src/Watchdog.inlines.hh index c1262b5..30798ef 100644 --- a/src/Watchdog.inlines.hh +++ b/src/Watchdog.inlines.hh @@ -24,9 +24,8 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_Watchdog_inlines_hh #define PPL_Watchdog_inlines_hh 1 -#include <stdexcept> - #include "Handler.defs.hh" +#include <stdexcept> namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Added missing inclusion of <stdexcept>.
by Roberto Bagnara 05 May '12

05 May '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: ed687b7f8d4f4bf21d920a212354338a62148b40 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ed687b7f8d4f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 5 14:08:00 2012 +0200 Added missing inclusion of <stdexcept>. --- src/globals.inlines.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh index 7832558..2f500b2 100644 --- a/src/globals.inlines.hh +++ b/src/globals.inlines.hh @@ -24,10 +24,11 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_globals_inlines_hh #define PPL_globals_inlines_hh 1 +#include "compiler.hh" #include <limits> #include <cassert> #include <cctype> -#include "compiler.hh" +#include <stdexcept> namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/ppl(master): Inclusions reordered to match the PPL coding standard.
by Roberto Bagnara 05 May '12

05 May '12

Module: ppl/ppl Branch: master Commit: 2bfa68aaf70d66197a4e220dc0f59702841afa17 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2bfa68aaf70d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 5 14:08:35 2012 +0200 Inclusions reordered to match the PPL coding standard. --- src/Watchdog.inlines.hh | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) diff --git a/src/Watchdog.inlines.hh b/src/Watchdog.inlines.hh index c1262b5..30798ef 100644 --- a/src/Watchdog.inlines.hh +++ b/src/Watchdog.inlines.hh @@ -24,9 +24,8 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_Watchdog_inlines_hh #define PPL_Watchdog_inlines_hh 1 -#include <stdexcept> - #include "Handler.defs.hh" +#include <stdexcept> namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/ppl(master): Added missing inclusion of <stdexcept>.
by Roberto Bagnara 05 May '12

05 May '12

Module: ppl/ppl Branch: master Commit: 339b75d89fae9462239b96c767d059770c19d862 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=339b75d89fae… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 5 14:08:00 2012 +0200 Added missing inclusion of <stdexcept>. --- src/globals.inlines.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh index 748f6dc..8250d63 100644 --- a/src/globals.inlines.hh +++ b/src/globals.inlines.hh @@ -24,12 +24,13 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_globals_inlines_hh #define PPL_globals_inlines_hh 1 +#include "compiler.hh" #include <limits> #include <cassert> #include <istream> #include <ostream> #include <cctype> -#include "compiler.hh" +#include <stdexcept> namespace Parma_Polyhedra_Library {

1 0

Re: [PPL-devel] Another question
by Ezio Bartocci 04 May '12

04 May '12

Dear PPL developers, I forward the message that I sent to Roberto. Since he is traveling, maybe some of you can help us... Thanks a lot Best Regards Ezio On Thu, May 3, 2012 at 4:42 PM, Ezio Bartocci <ezio.bartocci(a)gmail.com> wrote: > Dear Roberto, > > > I have another question. This time in English so that also Radu > and Gregory can read. I have the following points, describing a > polytope: > > 1 0.005 0.007883 > 0.9967750 0.004769 0.007988 > 1 0.000250 0.007883 > 0.9967750 1.900e-05 0.007988 > 1 0.005000 0.004225 > 0.9967750 0.004769 0.004331 > 1 0.000250 0.004225 > 0.9967750 1.900e-05 0.004331 > 1 0.0050000 0.007883 > 0.4194590 0.0047690 0.007988 > 1 0.0002500 0.007883 > 0.4194590 1.9000e-05 0.007988 > 1 0.0050000 0.004225 > 0.4194590 0.0047690 0.004331 > 1 0.0002500 0.004225 > 0.4194590 1.90000e-05 0.004331 > > > From this points stored in a matrix P with rows_P = 16 and cols_P = 3. > > I call this function that I developed to generate a C_Polyhedron (or > Polytope), that uses > > add_generator > > as you suggested and assign to P the result that is private member of > the class ppl_wrap > > > ppl_wrap::ppl_wrap (double * Points, int rows_P, int > cols_P):rows_P(rows_P), cols_P(cols_P) > { > > int debug = 1; > int i, j, k; > > // Convert the standard double representation to a much > // accurate representation > vector<mpf_class> *P1_row = double2mpzclass(Points, &rows_P, &cols_P); > vector<vector<mpf_class> > *P1 = vec2mat(P1_row, &rows_P, &cols_P); > vector<mpf_class> single_point; > > list<Variable> VarList; > list<Variable>::iterator it; > Linear_Expression lin_exp[rows_P]; > if (debug) > cout << "Cols num: " << cols_P << "\n"; > > for(i=0; i< cols_P; i++) // create a list of n_col_C "Variable" objects > VarList.push_back(Variable(i)); > > C_Polyhedron ph (cols_P, EMPTY); > > if (debug) > cout << "Rows num: " << rows_P << "\n"; > for (j = 0; j < rows_P; j++) > { > if (debug) > cout << " j = " << j << "\n"; > single_point.clear(); > > /*Create linear expression for expressing the point*/ > if (debug) > cout << " k = "; > for (k = 0; k < cols_P; k++){ // pick the needed row of matrix C > if (debug) > cout << "(" << k << ") " << (*P1)[k][j] << " "; > single_point.push_back((*P1)[k][j]); > > } > if (debug) > cout << ";\n"; > > > int m; > for ( it=VarList.begin() ; it != VarList.end(); it++ ) // > creates linear expression "lin_exp_temp" by using the iterator of the > Variable-List > { > m = it->id(); > if (debug) > cout << " m = " << m <<"\n"; > lin_exp[j]+=single_point[m]*(*it); > } > > ph.add_generator(point(lin_exp[j])); > } > P = ph; > } > > > > After obtaining a polytope I need to have the following representation > to store the polytope back in matlab C * x <= d. > > Now as I wrote in a previous email I saw that with: > > Constraint_System ConSys_P; > ConSys_P = P.constraints(); > > we can actually obtain the representation: C * x >= d > > but if I print the constraints: > > ConSys_P.print(); > > -A + C >= 0, -C >= -1, A >= 0, B >= 0, -B >= -1 > > This does not seem to match with the points and it seems an over > approximation. I would expected constraints more tight constraints. > > Why is like that ? > > > Thanks, > > Best > > > Ezio > > > > > > > > > -- > Dr. Ezio Bartocci, Assistant Professor > Dependable Systems Group > Department of Computer Engineering > Faculty of informatics > TU Wien, Vienna University of Technology, Austria > Treitlstraße 3, 1040 Vienna, Austria > E-Mail: ezio.bartocci(a)tuwien.ac.at > Phone: +43 (1) 58801 - 18210 > Webiste: http://www.eziobartocci.com -- Dr. Ezio Bartocci, Assistant Professor Dependable Systems Group Department of Computer Engineering Faculty of informatics TU Wien, Vienna University of Technology, Austria Treitlstraße 3, 1040 Vienna, Austria E-Mail: ezio.bartocci(a)tuwien.ac.at Phone: +43 (1) 58801 - 18210 Webiste: http://www.eziobartocci.com

2 6

PIP and SWI-Prolog, bug?
by Fred Mesnard 04 May '12

04 May '12

Hi there! I am using PPL 1.0pre1 (GIT version) with SWI-Prolog 6.1.3 and I think I find a bug wrt PIP: Call: (8) ppl_new_PIP_Problem_from_space_dimension(6, _G10879) ? skip Exit: (8) ppl_new_PIP_Problem_from_space_dimension(6, 935460) ? creep Call: (8) ppl_PIP_Problem_add_constraints(935460, [A-B-C+D>=0, F= -A+B+E, D= -1-A+B+C]) ? creep Exit: (8) ppl_PIP_Problem_add_constraints(935460, []) ? Call: (8) ppl_PIP_Problem_is_satisfiable(935460) ? skip Exit: (8) ppl_PIP_Problem_is_satisfiable(935460) ? IMO, this last call should fail because the [A-B-C+D>=0, F= -A+B+E, D= -1-A+B+C] is not satisfiable. Note that [A-B-C+D>=0, D= -1-A+B+C] is correctly reported as unsatisfiable. Do you confirm it's a bug from PIP? Thanks in advance, Fred ---------------------------------------------------------------------------------------------------------------

2 3

[GIT] ppl/ppl(master): Recompute the sign of the special_equality_row after modyfying it.
by Enea Zaffanella 04 May '12

04 May '12

Module: ppl/ppl Branch: master Commit: 5453b06aa9e87a44354171c588e09397393a0bb6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5453b06aa9e8… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 4 10:13:05 2012 +0200 Recompute the sign of the special_equality_row after modyfying it. This fixes the bug shown by test04() in tests/PIP_Problem/pipproblem3.cc. --- src/PIP_Tree.cc | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 42a568d..9899dc5 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -2416,6 +2416,7 @@ PIP_Solution_Node const dimension_type m_eq = mapping[special_equality_row]; sub_assign(tableau.s[m_eq], v_row); sub_assign(tableau.t[m_eq], p_row); + sign[m_eq] = row_sign(tableau.t[m_eq], big_dimension); } } }

1 0

[GIT] ppl/ppl(master): Added a new test showing a bug in PIP_Problem.
by Enea Zaffanella 04 May '12

04 May '12

Module: ppl/ppl Branch: master Commit: 62166e5b03fd6c3f33168ff6b52e72d732c7a0c9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=62166e5b03fd… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 4 09:35:26 2012 +0200 Added a new test showing a bug in PIP_Problem. The test was reduced from a slightly bigger one provided by Fred Mesnard. --- tests/PIP_Problem/pipproblem3.cc | 20 ++++++++++++++++++++ 1 files changed, 20 insertions(+), 0 deletions(-) diff --git a/tests/PIP_Problem/pipproblem3.cc b/tests/PIP_Problem/pipproblem3.cc index c8f3af8..fd75b32 100644 --- a/tests/PIP_Problem/pipproblem3.cc +++ b/tests/PIP_Problem/pipproblem3.cc @@ -150,10 +150,30 @@ test03() { return ok; } +bool +test04() { + Variable A(0); + Variable B(1); + Variable C(2); + + Constraint_System cs; + cs.insert(A >= 0); + cs.insert(A == B); + cs.insert(A == -1); + + PIP_Problem pip(2); + pip.add_constraints(cs); + + bool ok = !pip.is_satisfiable(); + + return ok; +} + } // namespace BEGIN_MAIN DO_TEST_F8(test01); DO_TEST_F8(test02); DO_TEST_F8(test03); + DO_TEST(test04); END_MAIN

1 0

[GIT] ppl/ppl(master): New commits
by Roberto Bagnara 03 May '12

03 May '12

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b1156e92516d… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 3 21:40:34 2012 +0200 Make sure template specializations are declared. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3500e3bcc9c9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 3 19:11:24 2012 +0200 Avoid implicit conversions changing integer signedness. Detected by ECLAIR service utypflag. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6c49cfb2f3fa… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 3 15:55:11 2012 +0200 Fixed indentation. Detected by ECLAIR service indntion. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=af42e4fdf6e4… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 3 15:17:34 2012 +0200 Avoid C-style casts. Detected by ECLAIR service castexpr. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b36a41761e47… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu May 3 14:55:23 2012 +0200 Prefer PPL_UNREACHABLE to PPL_ASSERT(false). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f9e934bb246a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed May 2 08:55:48 2012 +0200 Avoid redundant explicit casts. Detected by ECLAIR service castexpr. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=afcc028e5c82… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed May 2 08:23:11 2012 +0200 Avoid unsigned integer wrap-around in constant expressions. Detected by ECLAIR service cnstwrap. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=42943b3d8e70… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue May 1 15:18:29 2012 +0200 Prefer parentheses to excessive reliance on C++ operator precedence rules. Detected by ECLAIR service exprprns. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=10a80c332f47… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue May 1 15:15:29 2012 +0200 Reduced scope of local variable. Detected by ECLAIR service minscope. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=329c4acd3ead… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue May 1 15:13:33 2012 +0200 Fixed comment about case-block termination. Detected by ECLAIR service swchsynt. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=294b398c6e9e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue May 1 15:10:49 2012 +0200 Fixed file comment block. Detected by ECLAIR service cmntfile.

1 0