[PPL-devel] Re: PPL-devel Digest, Vol 7, Issue 3
Elena Fersman
fersman at lsv.ens-cachan.fr
Fri Jan 16 16:50:44 CET 2004
Dear Roberto,
Thank you for your helpful answers!
We are planning to use the library in a model checker for hybrid systems.
I will probably have more questions later.
Best regards
Elena
ppl-devel-request at cs.unipr.it wrote:
>Send PPL-devel mailing list submissions to
> ppl-devel at cs.unipr.it
>
>To subscribe or unsubscribe via the World Wide Web, visit
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>or, via email, send a message with subject or body 'help' to
> ppl-devel-request at cs.unipr.it
>
>You can reach the person managing the list at
> ppl-devel-owner at cs.unipr.it
>
>When replying, please edit your Subject line so it is more specific
>than "Re: Contents of PPL-devel digest..."
>
>
>Today's Topics:
>
> 1. Re: PPL-devel Digest, Vol 7, Issue 2 (Elena Fersman)
> 2. Re: Re: PPL-devel Digest, Vol 7, Issue 2 (Roberto Bagnara)
> 3. Re: Re: PPL-devel Digest, Vol 7, Issue 2 (Roberto Bagnara)
>
>
>----------------------------------------------------------------------
>
>Message: 1
>Date: Wed, 14 Jan 2004 12:54:39 +0100
>From: Elena Fersman <fersman at lsv.ens-cachan.fr>
>Subject: [PPL-devel] Re: PPL-devel Digest, Vol 7, Issue 2
>To: ppl-devel at cs.unipr.it
>Message-ID: <40052DFF.1080004 at lsv.ens-cachan.fr>
>Content-Type: text/plain; charset=us-ascii; format=flowed
>
>I have downloaded the latest release version of the library (0.5). I do
>not have problems with compiling the library. But when i try to compile
>the following program:
>#include"ppl.hh"
>main(void){}
>
>with the command gcc file.c -lgmp -lgmpxx -lppl
>
>i am getting lots of syntax errors.
>Compilation of test programs with make test goes well, but there are too
>many compilation options. Could you please help me with the minimal
>example to start using the library?
>
>Best regards
>Elena
>
>
>
>>Message: 1
>>Date: Tue, 13 Jan 2004 17:53:43 +0100
>>From: Elena Fersman <fersman at lsv.ens-cachan.fr>
>>Subject: [PPL-devel] how to start using ppl?
>>To: ppl-devel at cs.unipr.it
>>Message-ID: <40042297.8090006 at lsv.ens-cachan.fr>
>>Content-Type: text/plain; charset=us-ascii; format=flowed
>>
>>Dear PPL Developers,
>>I am a beginner with PPL library and I am having problems with compilation.
>>I am getting error messages like "redeclaration of 'typename', typename
>>previously declared..."
>>Do you have some demo files on usage of ppl? The library file is in ppl.hh?
>>
>>Regards,
>>Elena
>>
>>
>>------------------------------
>>
>>Message: 2
>>Date: Tue, 13 Jan 2004 19:00:08 +0100 (CET)
>>From: Roberto Bagnara <roberto at spartacus.cs.unipr.it>
>>Subject: Re: [PPL-devel] how to start using ppl?
>>To: ppl-devel at cs.unipr.it
>>Message-ID: <200401131800.i0DI08K14387 at spartacus.cs.unipr.it>
>>Content-Type: text/plain; charset=us-ascii
>>
>>
>>
>>
>>
>>>I am a beginner with PPL library and I am having problems with compilation.
>>>
>>>
>>>
>>>
>>Dear Elena,
>>
>>are you having problems compiling the library itself or compiling
>>programs using the library? Which version of the library did you
>>download?
>>
>>
>>
>>
>>
>>>I am getting error messages like "redeclaration of 'typename', typename
>>>previously declared..."
>>>
>>>
>>>
>>>
>>This is strange. Can you provide more details?
>>Which version of which compiler are you using?
>>
>>
>>
>>
>>
>>>Do you have some demo files on usage of ppl?
>>>
>>>
>>>
>>>
>>All the files in the tests subdirectory are, in a sense, demo
>>files. Some are more interesting than others, of course, but
>>all the features of the library are tested in at least one
>>of those.
>>
>>
>>
>>
>>
>>>The library file is in ppl.hh?
>>>
>>>
>>>
>>>
>>Well, the ppl.hh file is the only header file of the library
>>so that including it is all you have to do in order to get
>>your program compiled. If you give us more details about
>>what is going wrong we will be more than happy to help.
>>Response time may be higher than usual these days as most
>>of us are attending the VMCAI and POPL conferences in Venice.
>>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 at cs.unipr.it
>>
>>
>>------------------------------
>>
>>_______________________________________________
>>PPL-devel mailing list
>>PPL-devel at cs.unipr.it
>>http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>>
>>
>>End of PPL-devel Digest, Vol 7, Issue 2
>>***************************************
>>
>>
>>
>>
>>
>
>
>
>------------------------------
>
>Message: 2
>Date: Wed, 14 Jan 2004 14:39:50 +0100 (CET)
>From: Roberto Bagnara <roberto at spartacus.cs.unipr.it>
>Subject: Re: [PPL-devel] Re: PPL-devel Digest, Vol 7, Issue 2
>To: ppl-devel at cs.unipr.it
>Message-ID: <200401141339.i0EDdom04086 at spartacus.cs.unipr.it>
>Content-Type: text/plain; charset=us-ascii
>
>Elena Fersman wrote:
>
>
>>I have downloaded the latest release version of the library (0.5). I do
>>not have problems with compiling the library. But when i try to compile
>>the following program:
>>#include"ppl.hh"
>>main(void){}
>>
>>with the command gcc file.c -lgmp -lgmpxx -lppl
>>
>>i am getting lots of syntax errors.
>>
>>
>
>Dear Elena,
>
>it is now quite clear why you are getting lots of compilation errors.
>If you name a file "file.c" and use the command "gcc" to compile it,
>then the compiler interprets the file as a C program. The include file
>"ppl.hh" is the include file for the C++ interface of the library.
>
>There are thus two possibilities:
>
>1) You want to use the C++ interface: then include, as you are doing,
> "ppl.hh" but name your source "file.cc" and/or use the "g++" command
> instead of "gcc".
>
>2) You want to use the C interface: then include "ppl_c.h" instead of
> "ppl.hh" and you are done.
>
>
>
>>Compilation of test programs with make test goes well, but there are too
>>many compilation options. Could you please help me with the minimal
>>example to start using the library?
>>
>>
>
>Your program is the minimal program using the library, even though it
>does nothing. Just compile it with g++ using the same options you
>are giving to gcc and it should be OK. More interesting examples
>are given in the documentation and, as I said, the tests subdirectory
>is full of examples you can adapt. I am now writing from an uncomfortable
>environment, but I can send you something if you still have problems
>once I am back from the conference.
>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 at cs.unipr.it
>
>
>------------------------------
>
>Message: 3
>Date: Wed, 14 Jan 2004 14:50:41 +0100 (CET)
>From: Roberto Bagnara <roberto at spartacus.cs.unipr.it>
>Subject: Re: [PPL-devel] Re: PPL-devel Digest, Vol 7, Issue 2
>To: ppl-devel at cs.unipr.it
>Message-ID: <200401141350.i0EDofx04238 at spartacus.cs.unipr.it>
>Content-Type: text/plain; charset=us-ascii
>
>Elena Fersman wrote:
>
>
>>Could you please help me with the minimal
>>example to start using the library?
>>
>>
>
>I have managed to quickly hack tests/intersection1.cc
>to provide you with a non-trivial example: call the
>file below the signature "inters.cc" and compile it
>with
>
> g++ -W -Wall -o inters inters.cc -lppl -lgmpcc -lgmp
>
>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 at cs.unipr.it
>
>/* Intersection of an icosahedron with a column.
> Copyright (C) 2001-2003 Roberto Bagnara <bagnara at cs.unipr.it>
>
>This file is part of the Parma Polyhedra Library (PPL).
>
>The PPL is free software; you can redistribute it and/or modify it
>under the terms of the GNU General Public License as published by the
>Free Software Foundation; either version 2 of the License, or (at your
>option) any later version.
>
>The PPL is distributed in the hope that it will be useful, but WITHOUT
>ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
>FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
>for more details.
>
>You should have received a copy of the GNU General Public License
>along with this program; if not, write to the Free Software
>Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307,
>USA.
>
>For the most up-to-date information see the Parma Polyhedra Library
>site: http://www.cs.unipr.it/ppl/ . */
>
>#include <ppl.hh>
>
>using namespace std;
>using namespace Parma_Polyhedra_Library;
>using namespace Parma_Polyhedra_Library::IO_Operators;
>
>int
>main() {
> Variable x(0);
> Variable y(1);
> Variable z(2);
>
> C_Polyhedron icosahedron(3);
> icosahedron.add_constraint(4*x - 2*y - z + 14 >= 0);
> icosahedron.add_constraint(4*x + 2*y - z + 2 >= 0);
> icosahedron.add_constraint(x + y - 1 >= 0);
> icosahedron.add_constraint(x + y + 2*z - 5 >= 0);
> icosahedron.add_constraint(x + 1 >= 0);
> icosahedron.add_constraint(x + z - 1 >= 0);
> icosahedron.add_constraint(2*x + y -2*z + 7 >= 0);
> icosahedron.add_constraint(x - y + 2*z + 1 >= 0);
> icosahedron.add_constraint(x - y + 5 >= 0);
> icosahedron.add_constraint(2*x - y - 2*z + 13 >= 0);
> icosahedron.add_constraint(-2*x - y + 2*z + 1 >= 0);
> icosahedron.add_constraint(-x + y - 1 >= 0);
> icosahedron.add_constraint(-x + y -2*z + 7 >= 0);
> icosahedron.add_constraint(-4*x + 2*y + z - 4 >= 0);
> icosahedron.add_constraint(-2*x + y + 2*z - 5 >= 0);
> icosahedron.add_constraint(-x + 1 >= 0);
> icosahedron.add_constraint(-x - z + 5 >= 0);
> icosahedron.add_constraint(-4*x - 2*y + z + 8 >= 0);
> icosahedron.add_constraint(-x - y + 5 >= 0);
> icosahedron.add_constraint(-x - y -2*z +13 >= 0);
>
> C_Polyhedron column(3);
> column.add_constraint(y >= 2);
> column.add_constraint(y <= 4);
> column.add_constraint(x >= 0);
> column.add_constraint(x <= 1);
>
> C_Polyhedron computed_result = icosahedron;
> computed_result.intersection_assign_and_minimize(column);
>
> C_Polyhedron known_result(3);
> known_result.add_constraint(-4*x - 2*y + z >= -8);
> known_result.add_constraint(-4*x + 2*y + z >= 4);
> known_result.add_constraint(-2*x - y + 2*z >= -1);
> known_result.add_constraint(-2*x + y + 2*z >= 5);
> known_result.add_constraint(-x - y - 2*z >= -13);
> known_result.add_constraint(-x - z >= -5);
> known_result.add_constraint(-x >= -1);
> known_result.add_constraint(-x + y - 2*z >= -7);
> known_result.add_constraint(-y >= -4);
> known_result.add_constraint(y >= 2);
> known_result.add_constraint(x >= 0);
>
> int retval = (computed_result == known_result) ? 0 : 1;
>
> cout << "*** icosahedron ***" << endl
> << icosahedron.constraints() << endl;
> cout << "*** columns ***" << endl
> << column.constraints() << endl;
> cout << "*** computed_result ***" << endl
> << computed_result.constraints() << endl;
>
> return retval;
>}
>
>------------------------------
>
>_______________________________________________
>PPL-devel mailing list
>PPL-devel at cs.unipr.it
>http://www.cs.unipr.it/mailman/listinfo/ppl-devel
>
>
>End of PPL-devel Digest, Vol 7, Issue 3
>***************************************
>
>
>
More information about the PPL-devel
mailing list