March 2004 - PPL-devel - BUGSENG Mailman

Bignums
by Roberto Bagnara 14 May '04

14 May '04

Hi there, I believe the following behavior of the CVS version of YAP witnesses a bug (or, quite possible, a misunderstanding on my part): $ yap [ Restoring file /usr/local/lib/Yap/startup ] [ YAP version Yap-4.3.23 ] ?- current_prolog_flag(bounded,X). X = false ? ?- X is 333333333333333, integer(X). no ?- X is 33333333, integer(X). X = 33333333 ? ?- X is 333333333333333, float(X). no ?- X is 333333333333333, number_chars(X,L). X = 333333333333333, L = [51,51,51,51,51,51,51,51,51,51,51,51,51,51,51] ? In words, the Prolog engine first declares it is employing unbounded integers, then it silently converts an integer numeral to... to what? Is this a bug? Am I missing something? All the best Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 5

Re: Horrible bug? [Was: Re: Compiling PPL under Cygwin?]
by Roberto Bagnara 26 Mar '04

26 Mar '04

Goran Frehse wrote: > I had a feeling that you might be interested in the bug, but it only > occurred in the process of one specific example after many thousands of > iterations. I was not able to isolate the source, and creating the same > polyhedron by adding the constraints one by one resulted in the correct > empty polyhedron. Dear Goran, yes, we would be more than interested in the phenomenon you observed. > Once I'm past my current workload, I'll be happy to include your test > and see if I can find any strange things happening. Thanks! > I minimized the polyhedron using "mypoly.minimized_constraints()". > Afterwards "mypoly" would be the proper solution. > This I found strange, since minimized_constraints() is declared "const", > so shouldn't it leave mypoly unchanged? It leaves its "essence" unchanged, which means that `mypoly' would continue to be a representation of exactly the same polyhedron. But it may be a different representation. > Is there any reason against using the minimizing versions? Not at all. > Like I said, > it speeded things up for me by about 50%, as far as I can remember, even > though the polyhedra mostly were only generated once, checked for > intersection, and then forgotten. The speedup should be even greater > when the polyhedra are used several times for computations. That is exactly the point in having the minimizing versions available: their careful use (where "careful" here is a highly application-dependent) can result in significant speedups. Cheers, Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

[Fwd: RE: Horrible bug? [Was: Re: Compiling PPL under Cygwin?]]
by Roberto Bagnara 23 Mar '04

23 Mar '04

-------- Original Message -------- Subject: RE: Horrible bug? [Was: Re: Compiling PPL under Cygwin?] Date: Tue, 23 Mar 2004 14:26:12 -0500 From: Goran Frehse <gfrehse(a)andrew.cmu.edu> To: 'Roberto Bagnara' <bagnara(a)cs.unipr.it> Dear Roberto, I had a feeling that you might be interested in the bug, but it only occurred in the process of one specific example after many thousands of iterations. I was not able to isolate the source, and creating the same polyhedron by adding the constraints one by one resulted in the correct empty polyhedron. Once I'm past my current workload, I'll be happy to include your test and see if I can find any strange things happening. I minimized the polyhedron using "mypoly.minimized_constraints()". Afterwards "mypoly" would be the proper solution. This I found strange, since minimized_constraints() is declared "const", so shouldn't it leave mypoly unchanged? Is there any reason against using the minimizing versions? Like I said, it speeded things up for me by about 50%, as far as I can remember, even though the polyhedra mostly were only generated once, checked for intersection, and then forgotten. The speedup should be even greater when the polyhedra are used several times for computations. Best wishes, Goran -----Original Message----- From: Roberto Bagnara [mailto:bagnara@cs.unipr.it] Sent: 23 March 2004 14:04 To: Goran Frehse Cc: The Parma Polyhedra Library developers' list Subject: Horrible bug? [Was: Re: Compiling PPL under Cygwin?] Goran Frehse wrote: > There is one comment on the PPL I have (I'm sorry it's not more > detailed): > In a long series of computations I obtained a polyhedron (4 > dimensions) with both constraints A<D and A>=D. Unfortunately it > wasn't possible to trace how exactly the polyhedron was created, but > it was simply by intersections with other polyhedra and adding > constraints. When minimizing this polyhedron, the proper solution > (empty) was returned, but the worrying part was this: The emptiness > test returned false on the original! I fixed the problem by using the > minimizing versions of all operators. Since this also gave me an > increase in speed, I've been using these ever since. > > I know this is a very vage description, but maybe it helps somehow. Dear Goran, from what you say, you have witnessed a spectacular bug somewhere: maybe in the PPL, maybe in the compiler you are using... who knows. However, we would be very, very grateful if you could try to reproduce it or help us to reproduce it. If it is a bug in the library, it is a serious one we would definitely like to fix. You say "When minimizing this polyhedron, the proper solution (empty) was returned"; how did you force minimization of the polyhedron? When this possible ambiguity is resolved, I think the problem may be attacked by 1) going back to the non-minimizing versions of the operators, and 2) using something like the function below instead of the usual emptiness test method: bool my_emptiness_test(const NNC_Polyhedron& ph) { bool empty = ph.is_empty(); if (!empty) { NNC_Polyhedron qh = ph; // Force minimization: is it that way that you forced minimization? (void) qh.generators(); if (qh.is_empty()) { std::cerr << "Emptiness test failure!" << std::endl; ph.ascii_dump(std::cerr); } } return empty; } Please let us know if there is something we can do to help you reproduce this bug. If your code is available we may even try ourselves in case you are too busy to do it. Thanks a lot anyway, Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Horrible bug? [Was: Re: Compiling PPL under Cygwin?]
by Roberto Bagnara 23 Mar '04

23 Mar '04

Goran Frehse wrote: > There is one comment on the PPL I have (I'm sorry it's not more > detailed): > In a long series of computations I obtained a polyhedron (4 dimensions) > with both constraints A<D and A>=D. Unfortunately it wasn't possible to > trace how exactly the polyhedron was created, but it was simply by > intersections with other polyhedra and adding constraints. > When minimizing this polyhedron, the proper solution (empty) was > returned, but the worrying part was this: The emptiness test returned > false on the original! > I fixed the problem by using the minimizing versions of all operators. > Since this also gave me an increase in speed, I've been using these ever > since. > > I know this is a very vage description, but maybe it helps somehow. Dear Goran, from what you say, you have witnessed a spectacular bug somewhere: maybe in the PPL, maybe in the compiler you are using... who knows. However, we would be very, very grateful if you could try to reproduce it or help us to reproduce it. If it is a bug in the library, it is a serious one we would definitely like to fix. You say "When minimizing this polyhedron, the proper solution (empty) was returned"; how did you force minimization of the polyhedron? When this possible ambiguity is resolved, I think the problem may be attacked by 1) going back to the non-minimizing versions of the operators, and 2) using something like the function below instead of the usual emptiness test method: bool my_emptiness_test(const NNC_Polyhedron& ph) { bool empty = ph.is_empty(); if (!empty) { NNC_Polyhedron qh = ph; // Force minimization: is it that way that you forced minimization? (void) qh.generators(); if (qh.is_empty()) { std::cerr << "Emptiness test failure!" << std::endl; ph.ascii_dump(std::cerr); } } return empty; } Please let us know if there is something we can do to help you reproduce this bug. If your code is available we may even try ourselves in case you are too busy to do it. Thanks a lot anyway, Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Re: [PPL-devel] Compiling PPL under Cygwin?
by Roberto Bagnara 16 Mar '04

16 Mar '04

Goran Frehse wrote: > I'm sorry for not answering sooner. I was extremely busy these past > weeks, and unfortunately I'm still not able to compile under Cygwin. > I will attach my installation notes so far - they should work under > Mandrake, SuSE and Redhat Linux. Hi Goran, thanks a lot for your installation notes. We will use them to revise the PPL's documentation. > On a different topic, I've submitted two papers on a prototype tool that > I'm working on. It verifies Linear Hybrid Automata using the polyhedral > computations of the PPL. Compared to an existing tool (HyTech) it > performs very nicely, and I am quite pleased with the speed of the PPL. > I tried to give due credit to you in the papers and cited some of your > work. In case you're interested in the topic, I'd be happy to send you > the submitted drafts. We are definitely interested. If you send the drafts to me I will share them with all the group. With a better understanding of what you are doing I am sure we will find room for further collaboration (we may improve the library in ways that benefit your application, you may help us testing our work). By the way, it is great to have new applications of the PPL, as this may give us a more precise statistics of the polyhedra that arise in real problems. All the best, Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

[Fwd: RE: [PPL-devel] Compiling PPL under Cygwin?]
by Roberto Bagnara 16 Mar '04

16 Mar '04

-------- Original Message -------- Subject: RE: [PPL-devel] Compiling PPL under Cygwin? Date: Mon, 15 Mar 2004 18:05:16 -0500 From: Goran Frehse <gfrehse(a)andrew.cmu.edu> To: 'Roberto Bagnara' <bagnara(a)cs.unipr.it> Dear Roberto, I'm sorry for not answering sooner. I was extremely busy these past weeks, and unfortunately I'm still not able to compile under Cygwin. I will attach my installation notes so far - they should work under Mandrake, SuSE and Redhat Linux. On a different topic, I've submitted two papers on a prototype tool that I'm working on. It verifies Linear Hybrid Automata using the polyhedral computations of the PPL. Compared to an existing tool (HyTech) it performs very nicely, and I am quite pleased with the speed of the PPL. I tried to give due credit to you in the papers and cited some of your work. In case you're interested in the topic, I'd be happy to send you the submitted drafts. Best wishes, Goran -- Goran Frehse Department of Electrical and Computer Engineering Carnegie Mellon University -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it ---------------------------------------------------------------------- How to install PPL 0.5 ---------------------------------------------------------------------- 1. Install GMP (4.2) - Run cygwin bash-shell. - Change to gmp-directory (gmp-4.2) - Type: CPPFLAGS=-fexceptions ./configure --enable-cxx - Type: make - Type: make install Take note in which directory gmp was installed. At several places in the output it will say something like: "Libraries have been installed in: /usr/local/lib" 2. Install PPL (0.5) - Change to ppl-directory (ppl-0.5) - Type: ./configure --with-gmp-dir=/usr/local/lib --with-gmp-includes=/usr/local/include Note: These paths vary with your distribution and depend on the installation of GMP. - Type: make - Type: make install ---------------------------------------------------------------------- Testing ---------------------------------------------------------------------- - go to gmp-directory - Type: make check - go to ppl-directory - Type: make check Note: Bug in Cygwin might require fixing libgmpxx.la (see below). ---------------------------------------------------------------------- Compile a test file for GMP ---------------------------------------------------------------------- - If your compiler is gcc: gcc -g test2.c -lgmp ---------------------------------------------------------------------- Compile a program using PPL ---------------------------------------------------------------------- - If your compiler is gcc: gcc -g name.cpp -lgmp -lgmpxx -lppl ---------------------------------------------------------------------- Error in Cygwin 1.5.7-1 ---------------------------------------------------------------------- Symptom: False reference in libgmpxx.la leads to error in libtool when trying to compile programs using the PPL. Fix: In "libgmpxx.la" (usually in /usr/local/lib), replace "/GCC/gcc-3.3.1-3/.inst/package-gcc/usr/lib/./libstdc++.la" with appropriate path, usually "/usr/lib/libstdc++.la" or "lib/libstdc++.la". ---------------------------------------------------------------------- Excerpt from "make install" in GMP that contains path information: ---------------------------------------------------------------------- Libraries have been installed in: /usr/local/lib If you ever happen to want to link against installed libraries in a given directory, LIBDIR, you must either use libtool, and specify the full pathname of the library, or use the `-LLIBDIR' flag during linking and do at least one of the following: - add LIBDIR to the `PATH' environment variable during execution - add LIBDIR to the `LD_RUN_PATH' environment variable during linking - use the `-Wl,--rpath -Wl,LIBDIR' linker flag See any operating system documentation about shared libraries for more information, such as the ld(1) and ld.so(8) manual pages. ----------------------------------------------------------------------

1 0

ppl ./TODO src/ConSys.defs.hh src/GenSys.defs. ...
by Roberto Bagnara 06 Mar '04

06 Mar '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-03-06 09:04:44 Modified files: . : TODO src : ConSys.defs.hh GenSys.defs.hh LinExpression.defs.hh Matrix.defs.hh Log message: Matrix::ascii_dump(), Matrix::ascii_load(), LinExpression::~LinExpression(), Matrix::~Matrix(), ConSys::~ConSys(), GenSys::~GenSys() and ConSys::const_iterator::~const_iterator() are no longer virtual. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/TODO.diff?cvsroot=ppl&r1=1.66… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/ConSys.defs.hh.diff?cvsro… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/GenSys.defs.hh.diff?cvsro… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/LinExpression.defs.hh.dif… http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Matrix.defs.hh.diff?cvsro…

1 0

ppl/src Constraint.defs.hh
by Roberto Bagnara 04 Mar '04

04 Mar '04

CVSROOT: /cvs/ppl Module name: ppl Changes by: roberto(a)cs.unipr.it 2004-03-04 07:45:58 Modified files: src : Constraint.defs.hh Log message: Constraint::Constraint(LinExpression& e) made explicit. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Constraint.defs.hh.diff?c…

1 0