October 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(pip): Version number bumped.
by Roberto Bagnara 27 Oct '09

27 Oct '09

Module: ppl/ppl Branch: pip Commit: da9e3b638d7543342ba2d8c31e19ab2d892d87cd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=da9e3b638d75… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Oct 27 17:08:11 2009 +0100 Version number bumped. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index 7da6e56..e1bc039 100644 --- a/configure.ac +++ b/configure.ac @@ -23,7 +23,7 @@ # Process this file with Autoconf to produce a configure script. # Every other copy of the package version number gets its value from here. -AC_INIT([the Parma Polyhedra Library], [0.11pre7], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.11pre8], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(pip): Fixed the C interface and the documentation for PIP_Tree_Node methods.
by François Galea 27 Oct '09

27 Oct '09

Module: ppl/ppl Branch: pip Commit: 73a0148ba9c9d0a46e0fa56f120287bda92b989c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=73a0148ba9c9… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Oct 27 16:31:42 2009 +0100 Fixed the C interface and the documentation for PIP_Tree_Node methods. The concerned methods are insert_artificials and get_parametric_values. --- interfaces/C/ppl_c_header.h | 55 ++++++++++++++++++++------- interfaces/C/ppl_c_implementation_common.cc | 15 +++++-- src/PIP_Tree.defs.hh | 18 +++++++-- 3 files changed, 65 insertions(+), 23 deletions(-) diff --git a/interfaces/C/ppl_c_header.h b/interfaces/C/ppl_c_header.h index af77a18..6913c87 100644 --- a/interfaces/C/ppl_c_header.h +++ b/interfaces/C/ppl_c_header.h @@ -2854,14 +2854,31 @@ PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, ppl_Artificial_Parameter_Sequence_const_iterator_t pit)); /*! \relates ppl_PIP_Tree_Node_tag \brief - Insert in parameter set the parameter indices corresponding to local + Inserts in parameter set the parameter indices corresponding to local artificials. - \param params - the Variables_Set to be updated + This utility method can typically be used by user programs when spanning a + solution tree. As new parameters may be defined in tree nodes by the solver, + local solutions are likely to be expressed in terms of both the upper level + parameters and the local ones. - \param space_dimension - the space dimension for \p *this + The resulting space dimension is the sum of \p space_dim and the + returned number of inserts indices. + + \param pip_tree + the pip tree node whose artificial parameter indices are queried about + + \param ds + an array containing the current parameter indices, which will be updated + with the local indices, and must be properly dimensioned in order the new + indices to be inserted + + \param n + number of current valid parameter indices in \p ds (excluding the values to + be inserted) + + \param space_dim + the space dimension for \p pip_tree (excluding the local parameters) \return the number of inserted indices @@ -2871,23 +2888,33 @@ ppl_PIP_Tree_Node_insert_artificials PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, ppl_dimension_type ds[], size_t n, - ppl_dimension_type space_dim, - ppl_dimension_type inserted)); + ppl_dimension_type space_dim)); /*! \relates ppl_PIP_Tree_Node_tag \brief - Writes to \p le a parametric expression of the values of variable \p v. + Writes to \p le a const pointer to the parametric expression of the values + of variable \p v in solution node \p pip_sol. The linear expression assigned to \p le only involves parameters. - \return PPL_ERROR_INVALID_ARGUMENT - Returned if \p v is dimension-incompatible with \p *this - or if \p v is a parameter. + \param pip_sol + the solution tree node \param v - The variable which is queried about + the variable which is queried about \param pars - A set of indices of the parameters in the constraints + a set of indices of the parameters in the constraints, including those for + all artificials from the solution tree root to this node (included) + + \param n + number of valid elements in \p pars + + \param le + the returned expression of variable \p v + + \return PPL_ERROR_INVALID_ARGUMENT + Returned if \p v is dimension-incompatible with \p *this + or if \p v is a parameter. */ int ppl_PIP_Solution_Node_get_parametric_values @@ -2895,7 +2922,7 @@ PPL_PROTO((ppl_const_PIP_Solution_Node_t pip_sol, ppl_dimension_type v, ppl_dimension_type pars[], size_t n, - ppl_Linear_Expression_t le)); + ppl_const_Linear_Expression_t* le)); /*! \relates ppl_PIP_Tree_Node_tag \brief Writes to \p pip_tree a const pointer to the \p b (true or false) branch diff --git a/interfaces/C/ppl_c_implementation_common.cc b/interfaces/C/ppl_c_implementation_common.cc index 68cf73a..810f291 100644 --- a/interfaces/C/ppl_c_implementation_common.cc +++ b/interfaces/C/ppl_c_implementation_common.cc @@ -2324,14 +2324,19 @@ int ppl_PIP_Tree_Node_insert_artificials(ppl_const_PIP_Tree_Node_t pip_tree, ppl_dimension_type ds[], size_t n, - ppl_dimension_type space_dim, - ppl_dimension_type inserted) try { + ppl_dimension_type space_dim) try { const PIP_Tree_Node& spip_tree = *to_const(pip_tree); Variables_Set vars; - for (ppl_dimension_type i = n; i-- > 0; ) - vars.insert(ds[i]); + ppl_dimension_type inserted; + ppl_dimension_type i; inserted = spip_tree.insert_artificials(vars, space_dim); - return 0; + if (inserted > 0) { + Variables_Set::const_iterator end = vars.end(); + Variables_Set::const_iterator v; + for (i = n, v = vars.begin(); v != end; ++i, ++v) + ds[i] = *v; + } + return inserted; } CATCH_ALL diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 8c3704f..40400ac 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -102,14 +102,22 @@ public: Artificial_Parameter_Sequence::const_iterator art_parameter_end() const; /*! \brief - Insert in parameter set the parameter indices corresponding to local - artificials. + Inserts in parameter set \p params the parameter indices corresponding to + local artificials. + + This utility method can typically be used by user programs when spanning a + solution tree. As new parameters may be defined in tree nodes by the + solver, local solutions are likely to be expressed in terms of both the + upper level parameters and the local ones. + + The resulting space dimension is the sum of \p space_dimension and the + returned number of inserts indices. \param params the Variables_Set to be updated \param space_dimension - the space dimension for \p *this + the space dimension for \p *this (excluding the local parameters) \return the number of inserted indices @@ -218,7 +226,9 @@ public: the variable which is queried about \param parameters - a \c std::set of indices of the parameters in the constraints + a \c std::set of indices of the parameters in the constraints, including + those for all artificials from the solution tree root to this node + (included) \exception std::invalid_argument Thrown if \p v is dimension-incompatible with \p *this

1 0

Fix needed to build gcc for x86/solaris
by Daniel Gutson 26 Oct '09

26 Oct '09

Hi, there's a problem (already fixed in git) that impedes gcc to build for x86/solaris. The fix is http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9a08d1d3a98c… Is there an ETA estimate for this fix to be released (0.10.3)? That would be very helpful. Thanks!, Daniel. -- Daniel Gutson CodeSourcery www.codesourcery.com

2 6

[GIT] ppl/ppl(pip): Another pass on the C interface for PIP_Problem related classes.
by Enea Zaffanella 26 Oct '09

26 Oct '09

Module: ppl/ppl Branch: pip Commit: 250a996c0147a7d30475c068a8a8c7aeeb3b17e2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=250a996c0147… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Oct 26 21:30:20 2009 +0100 Another pass on the C interface for PIP_Problem related classes. Removed a few useless functions and added a few missing ones, including input/output utilities; also slightly improved the documentation. --- interfaces/C/ppl_c_header.h | 98 +++++++++------------------ interfaces/C/ppl_c_implementation_common.cc | 44 ++---------- 2 files changed, 40 insertions(+), 102 deletions(-) diff --git a/interfaces/C/ppl_c_header.h b/interfaces/C/ppl_c_header.h index 9a14839..af77a18 100644 --- a/interfaces/C/ppl_c_header.h +++ b/interfaces/C/ppl_c_header.h @@ -694,11 +694,26 @@ PPL_TYPE_DECLARATION(MIP_Problem) towards \extref{Parma_Polyhedra_Library::PIP_Problem, PIP_Problem}. */ PPL_TYPE_DECLARATION(PIP_Problem) + +/*! \interface ppl_PIP_Tree_Node_tag + \brief + Types and functions for PIP tree nodes. +*/ PPL_TYPE_DECLARATION(PIP_Tree_Node) PPL_TYPE_DECLARATION(PIP_Decision_Node) PPL_TYPE_DECLARATION(PIP_Solution_Node) + +/*! \interface ppl_Artificial_Parameter_tag + \brief + Types and functions for PIP artificial parameters. +*/ PPL_TYPE_DECLARATION(Artificial_Parameter) PPL_TYPE_DECLARATION(Artificial_Parameter_Sequence) + +/*! \interface ppl_Artificial_Parameter_Sequence_const_iterator_tag + \brief + Types and functions for iterating on PIP artificial parameters. +*/ PPL_TYPE_DECLARATION(Artificial_Parameter_Sequence_const_iterator) @@ -2601,6 +2616,9 @@ PPL_PROTO((ppl_MIP_Problem_t mip, int value)); /*@}*/ /* Querying/Setting Control Parameters */ +/*! \brief \name Constructors, Assignment and Destructor */ +/*@{*/ + /*! \relates ppl_PIP_Problem_tag \brief Builds a trivial PIP problem of dimension \p d and writes an handle to it at address \p pmip. @@ -2782,7 +2800,7 @@ PPL_PROTO((ppl_const_PIP_Problem_t pip, /*@}*/ /* Computing the Solution of the PIP_Problem */ -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Writes to \p dpip_tree the solution node if \p spip_tree is a solution node, and 0 otherwise. */ @@ -2791,7 +2809,7 @@ ppl_PIP_Tree_Node_as_solution PPL_PROTO((ppl_const_PIP_Tree_Node_t spip_tree, ppl_const_PIP_Solution_Node_t* dpip_tree)); -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Writes to \p dpip_tree the decision node if \p spip_tree is a decision node, and 0 otherwise. */ @@ -2800,7 +2818,7 @@ ppl_PIP_Tree_Node_as_decision PPL_PROTO((ppl_const_PIP_Tree_Node_t spip_tree, ppl_const_PIP_Decision_Node_t* dpip_tree)); -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Writes to \p pcs the local system of parameter constraints at the pip tree node \p pip_tree. */ @@ -2809,7 +2827,7 @@ ppl_PIP_Tree_Node_get_constraints PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, ppl_const_Constraint_System_t* pcs)); -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Returns a positive integer if \p pip_tree is well formed, i.e., if it satisfies all its implementation invariants; returns 0 and perhaps makes some noise if \p pip_tree is broken. Useful for debugging purposes. @@ -2817,14 +2835,7 @@ PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, int ppl_PIP_Tree_Node_OK PPL_PROTO((ppl_const_PIP_Tree_Node_t pip)); -/*! \relates ppl_PIP_Problem_tag \brief - Invalidates the handle \p pip_tree: this makes sure the corresponding - resources will eventually be released. -*/ -int -ppl_delete_PIP_Tree_Node PPL_PROTO((ppl_const_PIP_Tree_Node_t pip)); - -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Assigns to \p pit a const iterator "pointing" to the beginning of the artificial parameter sequence in the pip tree node \p pip_tree. */ @@ -2833,7 +2844,7 @@ ppl_PIP_Tree_Node_begin PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, ppl_Artificial_Parameter_Sequence_const_iterator_t pit)); -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Assigns to \p pit a const iterator "pointing" to the end of the artificial parameter sequence in the pip tree node \p pip_tree. */ @@ -2842,7 +2853,7 @@ ppl_PIP_Tree_Node_end PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, ppl_Artificial_Parameter_Sequence_const_iterator_t pit)); -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Insert in parameter set the parameter indices corresponding to local artificials. @@ -2863,21 +2874,7 @@ PPL_PROTO((ppl_const_PIP_Tree_Node_t pip_tree, ppl_dimension_type space_dim, ppl_dimension_type inserted)); -/*! \relates ppl_PIP_Problem_tag \brief - Builds a trivial PIP problem of dimension \p d and writes an - handle to it at address \p pmip. -*/ -int -ppl_new_PIP_Solution_Node PPL_PROTO((ppl_PIP_Solution_Node_t* ppip_sol)); - -/*! \relates ppl_PIP_Problem_tag \brief - Invalidates the handle \p pip_sol: this makes sure the corresponding - resources will eventually be released. -*/ -int -ppl_delete_PIP_Solution_Node PPL_PROTO((ppl_const_PIP_Solution_Node_t pip_sol)); - -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Writes to \p le a parametric expression of the values of variable \p v. The linear expression assigned to \p le only involves parameters. @@ -2900,15 +2897,7 @@ PPL_PROTO((ppl_const_PIP_Solution_Node_t pip_sol, size_t n, ppl_Linear_Expression_t le)); - -/*! \relates ppl_PIP_Problem_tag \brief - Invalidates the handle \p pip_dec: this makes sure the corresponding - resources will eventually be released. -*/ -int -ppl_delete_PIP_Decision_Node PPL_PROTO((ppl_const_PIP_Decision_Node_t pip_dec)); - -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_PIP_Tree_Node_tag \brief Writes to \p pip_tree a const pointer to the \p b (true or false) branch of \p pip_dec. */ @@ -2918,36 +2907,15 @@ PPL_PROTO((ppl_const_PIP_Decision_Node_t pip_dec, int b, ppl_const_PIP_Tree_Node_t* pip_tree)); -/*! \relates ppl_PIP_Problem_tag \brief - Creates a new artificial parameter corresponding to the constant 0 in a - zero-dimensional space; writes a handle for the new artificial - parameter at address \p pap. -*/ -int -ppl_new_Artificial_Parameter PPL_PROTO((ppl_Artificial_Parameter_t* pap)); - -/*! \relates ppl_PIP_Problem_tag \brief - Builds an artificial parameter that is the result of - integer division of the linear expression \p le by \p coeff; - writes a handle for the newly created artificial parameter - at address \p pap. +/*! \relates ppl_Artificial_Parameter_tag \brief + Writes to \p le the linear expression in artificial parameter \p ap. */ int -ppl_new_Artificial_Parameter_from_Linear_Expression -PPL_PROTO((ppl_Artificial_Parameter_t* pap, - ppl_const_Linear_Expression_t le, - ppl_Coefficient_t coeff)); - -/*! \relates ppl_PIP_Problem_tag \brief - Builds an artificial parameter that is a copy of \p ap; writes a handle - for the newly created artificial parameter at address \p pap. -*/ -int -ppl_new_Artificial_Parameter_from_Artificial_Parameter -PPL_PROTO((ppl_Artificial_Parameter_t* pap, - ppl_const_Artificial_Parameter_t ap)); +ppl_Artificial_Parameter_get_Linear_Expression +PPL_PROTO((ppl_const_Artificial_Parameter_t ap, + ppl_const_Linear_Expression_t* le)); -/*! \relates ppl_PIP_Problem_tag \brief +/*! \relates ppl_Artificial_Parameter_tag \brief Writes to \p coeff the denominator in artificial parameter \p ap. */ int diff --git a/interfaces/C/ppl_c_implementation_common.cc b/interfaces/C/ppl_c_implementation_common.cc index e0988c3..68cf73a 100644 --- a/interfaces/C/ppl_c_implementation_common.cc +++ b/interfaces/C/ppl_c_implementation_common.cc @@ -2336,20 +2336,6 @@ ppl_PIP_Tree_Node_insert_artificials(ppl_const_PIP_Tree_Node_t pip_tree, CATCH_ALL int -ppl_new_PIP_Solution_Node(ppl_PIP_Solution_Node_t* ppip_sol) try { - *ppip_sol = to_nonconst(new PIP_Solution_Node()); - return 0; -} -CATCH_ALL - -int -ppl_delete_PIP_Solution_Node(ppl_const_PIP_Solution_Node_t pip_sol) try { - delete to_const(pip_sol); - return 0; -} -CATCH_ALL - -int ppl_PIP_Solution_Node_get_parametric_values (ppl_const_PIP_Solution_Node_t pip_sol, ppl_dimension_type v, @@ -2395,30 +2381,12 @@ ppl_PIP_Decision_Node_get_child_node(ppl_const_PIP_Decision_Node_t pip_dec, CATCH_ALL int -ppl_new_Artificial_Parameter(ppl_Artificial_Parameter_t* pap) try { - *pap = to_nonconst(new Artificial_Parameter()); - return 0; -} -CATCH_ALL - -int -ppl_new_Artificial_Parameter_from_Linear_Expression -(ppl_Artificial_Parameter_t* pap, - ppl_const_Linear_Expression_t le, - ppl_const_Coefficient_t coef) try { - const Linear_Expression& sle = *to_const(le); - const Coefficient& scoef = *to_const(coef); - *pap = to_nonconst(new Artificial_Parameter(sle, scoef)); - return 0; -} -CATCH_ALL - -int -ppl_new_Artificial_Parameter_from_Artificial_Parameter -(ppl_Artificial_Parameter_t* pap, - ppl_const_Artificial_Parameter_t ap) try { +ppl_Artificial_Parameter_get_Linear_Expression +(ppl_const_Artificial_Parameter_t ap, + ppl_const_Linear_Expression_t* le) try { const Artificial_Parameter& sap = *to_const(ap); - *pap = to_nonconst(new Artificial_Parameter(sap)); + const Linear_Expression& lle = static_cast<const Linear_Expression&>(sap); + *le = to_const(&lle); return 0; } CATCH_ALL @@ -2558,6 +2526,8 @@ DEFINE_OUTPUT_FUNCTIONS(MIP_Problem) DEFINE_OUTPUT_FUNCTIONS(PIP_Problem) +DEFINE_OUTPUT_FUNCTIONS(Artificial_Parameter) + char* ppl_io_wrap_string(const char* src, unsigned indent_depth,

1 0

[GIT] ppl/ppl(pip): Interfaced constructor/ destructor for Artificial_Parameter_Sequence iterators.
by Enea Zaffanella 25 Oct '09

25 Oct '09

Module: ppl/ppl Branch: pip Commit: bcd32b2e03105829d1bd8aa035c45bb5e9883cb8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bcd32b2e0310… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Oct 25 17:25:07 2009 +0100 Interfaced constructor/destructor for Artificial_Parameter_Sequence iterators. These iterators should be used similarly to the ones defined on systems of constraints or generators. Corrected a couple of bugs in the documentation. --- interfaces/C/ppl_c_header.h | 125 +++++++++++++++----------- interfaces/C/ppl_c_implementation_common.cc | 49 ++++++++++- src/PIP_Problem.defs.hh | 4 +- 3 files changed, 120 insertions(+), 58 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=bcd32b2e…

1 0

[Fwd: Re: Modified PPL 0.10.2 source distribution for Solaris]
by Roberto Bagnara 25 Oct '09

25 Oct '09

-------- Original Message -------- Subject: Re: Modified PPL 0.10.2 source distribution for Solaris Date: Sun, 25 Oct 2009 01:54:36 +0200 From: XXX Organization: YYY To: Roberto Bagnara <bagnara(a)cs.unipr.it> References: <4AD7B802.8070601(a)codesourcery.com> <4AD811C4.2040004(a)cs.unipr.it> <4AD87DF5.6010701(a)codesourcery.com> <4AE0B76D.30902(a)cs.unipr.it> <4AE1E9D2.5050600(a)codesourcery.com> <4AE2F556.5020505(a)cs.unipr.it> compiles perfectly fine. thanks a lot! tested on solaris10/x86, solaris10/sparc, solaris9/sparc, solaris8/sparc, linux/x86 aaaa On Sat, 24 Oct 2009 14:38:46 +0200 Roberto Bagnara wrote: > > [Apologies if you are no longer interested. RB] > > Hi there. > > In order to facilitate Solaris users, we have just uploaded > modified PPL 0.10.2 source distributions that, by simply renaming > a few template variables, work around the Solaris bug whereby > <sys/regset.h> is unnecessarily included. > The archives are here: > > ftp://ftp.cs.unipr.it/pub/ppl/releases/0.10.2/solaris/ > > We would appreciate knowing how they go. > 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

[GIT] ppl/ppl(pip): Added increment, dereference and equal functions
by Patricia Hill 24 Oct '09

24 Oct '09

Module: ppl/ppl Branch: pip Commit: 65ebba9954ea5539339c264d4a20493002d31607 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=65ebba9954ea… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Sat Oct 24 17:34:19 2009 +0100 Added increment, dereference and equal functions for ppl_Artificial_Parameter_Sequence_const_iterator_t's Fixed a couple of bugs. --- interfaces/C/ppl_c_header.h | 31 +++++++++++++++++++++++++- interfaces/C/ppl_c_implementation_common.cc | 30 ++++++++++++++++++++++++++ interfaces/C/tests/pip_test.c | 2 +- 3 files changed, 60 insertions(+), 3 deletions(-) diff --git a/interfaces/C/ppl_c_header.h b/interfaces/C/ppl_c_header.h index 8dc92be..065ef0a 100644 --- a/interfaces/C/ppl_c_header.h +++ b/interfaces/C/ppl_c_header.h @@ -2780,7 +2780,7 @@ ppl_PIP_Problem_solve PPL_PROTO((ppl_const_PIP_Problem_t pip)); Thrown if the PIP problem is not satisfiable. */ int -ppl_PPL_Problem_solution PPL_PROTO((ppl_const_PIP_Problem_t pip, +ppl_PIP_Problem_solution PPL_PROTO((ppl_const_PIP_Problem_t pip, ppl_const_PIP_Tree_Node_t* pip_tree)); /*! \relates ppl_PIP_Problem_tag \brief @@ -2797,7 +2797,7 @@ ppl_PPL_Problem_solution PPL_PROTO((ppl_const_PIP_Problem_t pip, if the PIP problem is unbounded or not satisfiable. */ int -ppl_PPL_Problem_optimizing_solution +ppl_PIP_Problem_optimizing_solution PPL_PROTO((ppl_const_PIP_Problem_t pip, ppl_const_PIP_Tree_Node_t* pip_tree)); @@ -2975,6 +2975,33 @@ int ppl_Artificial_Parameter_get_denominator PPL_PROTO((ppl_const_Artificial_Parameter_t ap, ppl_const_Coefficient_t* coef)); +/*! \relates ppl_Artificial_Parameter_Sequence_const_iterator_tag \brief + Dereference \p git writing a const handle to the resulting + grid generator at address \p pg. +*/ +int +ppl_Artificial_Parameter_Sequence_const_iterator_dereference +PPL_PROTO((ppl_const_Artificial_Parameter_Sequence_const_iterator_t apit, + ppl_const_Artificial_Parameter_t* pap)); + +/*! \relates ppl_Artificial_Parameter_Sequence_const_iterator_tag \brief + Increment \p git so that it "points" to the next grid generator. +*/ +int +ppl_Artificial_Parameter_Sequence_const_iterator_increment +PPL_PROTO((ppl_Artificial_Parameter_Sequence_const_iterator_t apit)); + +/*! \relates ppl_Artificial_Parameter_Sequence_const_iterator_tag \brief + Returns a positive integer if the iterators corresponding to \p x and + \p y are equal; returns 0 if they are different. +*/ +int +ppl_Artificial_Parameter_Sequence_const_iterator_equal_test +PPL_PROTO((ppl_const_Artificial_Parameter_Sequence_const_iterator_t x, + ppl_const_Artificial_Parameter_Sequence_const_iterator_t y)); + +/*@}*/ /* Dereferencing, Incrementing and Equality Testing */ + /*@}*/ /* Querying/Setting Control Parameters */ PPL_DECLARE_AND_DOCUMENT_IO_FUNCTIONS(MIP_Problem) diff --git a/interfaces/C/ppl_c_implementation_common.cc b/interfaces/C/ppl_c_implementation_common.cc index 1ef11f1..5d6dc0a 100644 --- a/interfaces/C/ppl_c_implementation_common.cc +++ b/interfaces/C/ppl_c_implementation_common.cc @@ -2431,6 +2431,36 @@ ppl_Artificial_Parameter_get_denominator(ppl_const_Artificial_Parameter_t ap, CATCH_ALL int +ppl_Artificial_Parameter_Sequence_const_iterator_dereference +(ppl_const_Artificial_Parameter_Sequence_const_iterator_t apit, + ppl_const_Artificial_Parameter_t* pap) try { + const Artificial_Parameter_Sequence::const_iterator& papit = *to_const(apit); + const Artificial_Parameter& ap = *papit; + *pap = to_const(&ap); + return 0; +} +CATCH_ALL + +int +ppl_Artificial_Parameter_Sequence_const_iterator_increment +(ppl_Artificial_Parameter_Sequence_const_iterator_t apit) try { + Artificial_Parameter_Sequence::const_iterator& papit = *to_nonconst(apit); + ++papit; + return 0; +} +CATCH_ALL + +int +ppl_Artificial_Parameter_Sequence_const_iterator_equal_test +(ppl_const_Artificial_Parameter_Sequence_const_iterator_t x, + ppl_const_Artificial_Parameter_Sequence_const_iterator_t y) try { + const Artificial_Parameter_Sequence::const_iterator& xx = *to_const(x); + const Artificial_Parameter_Sequence::const_iterator& yy = *to_const(y); + return (xx == yy) ? 1 : 0; +} +CATCH_ALL + +int ppl_io_print_variable(ppl_dimension_type var) try { const char* b = c_variable_output_function(var); if (b == 0 || puts(b) < 0) diff --git a/interfaces/C/tests/pip_test.c b/interfaces/C/tests/pip_test.c index 5152853..ab56dbf 100644 --- a/interfaces/C/tests/pip_test.c +++ b/interfaces/C/tests/pip_test.c @@ -104,7 +104,7 @@ main(int argc, char **argv) { ppl_dimension_type dim; ppl_const_PIP_Tree_Node_t solution; ppl_PIP_Problem_space_dimension(pip, &dim); - ppl_PPL_Problem_solution(pip, &solution); + ppl_PIP_Problem_solution(pip, &solution); /* display_solution(solution, N_VARS, N_PARAMETERS, parameter_dim); */ }

1 0

Sample examples of use of PPL
by Étienne André 24 Oct '09

24 Oct '09

Dear PPL developers, I am interesting in testing PPL in order to use it in a prototype tool for verification using parametric timed automata (written in OCaml). I did not find on the PPL website any sample example of code showing how to use PPL. I wonder if you had any somewhere (preferably using the interface with OCaml), or if you could give me any advice to find such a piece of code. Thank you very much. Best regards, Étienne ANDRÉ

2 1

[GIT] ppl/ppl(pip): Added test program for PIP C interface.
by François Galea 23 Oct '09

23 Oct '09

Module: ppl/ppl Branch: pip Commit: 0848cf9eb545480aefc689b7fd951b65ace7cf63 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0848cf9eb545… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Oct 23 17:03:27 2009 +0200 Added test program for PIP C interface. --- interfaces/C/tests/Makefile.am | 6 ++- interfaces/C/tests/pip_test.c | 114 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 119 insertions(+), 1 deletions(-) diff --git a/interfaces/C/tests/Makefile.am b/interfaces/C/tests/Makefile.am index bdb7233..ec94e92 100644 --- a/interfaces/C/tests/Makefile.am +++ b/interfaces/C/tests/Makefile.am @@ -64,7 +64,8 @@ $(top_builddir)/interfaces/C/libppl_c.la \ @extra_libraries@ NORMAL_TESTS = \ -formatted_output +formatted_output \ +pip_test # # Sources for the tests @@ -75,6 +76,9 @@ formatted_output.c \ print_to_buffer.h \ print_to_buffer.c +pip_test_SOURCES = \ +pip_test.c + # Dummy C++ source to cause C++ linking. # FIXME: why isn't enough to do this for libppl_c_tests.a? nodist_EXTRA_formatted_output_SOURCES = \ diff --git a/interfaces/C/tests/pip_test.c b/interfaces/C/tests/pip_test.c new file mode 100644 index 0000000..5152853 --- /dev/null +++ b/interfaces/C/tests/pip_test.c @@ -0,0 +1,114 @@ +/* Test the use of the PPL PIP solver from C code. + Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)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 3 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., 51 Franklin Street, Fifth Floor, 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_c_test.h" + +#include <stdio.h> +#include <stdlib.h> +#include <stdarg.h> + +static const char* program_name = 0; + +static void +my_exit(int status) { + (void) ppl_finalize(); + exit(status); +} + +static void +fatal(const char* format, ...) { + va_list ap; + fprintf(stderr, "%s: ", program_name); + va_start(ap, format); + vfprintf(stderr, format, ap); + va_end(ap); + fprintf(stderr, "\n"); + my_exit(1); +} + +#define N_VARS 2 +#define N_PARAMETERS 2 +#define N_CONSTRAINTS 4 +int +main(int argc, char **argv) { + ppl_PIP_Problem_t pip; + ppl_Constraint_t ct; + ppl_Coefficient_t c; + ppl_Linear_Expression_t le; + ppl_dimension_type i, j; + mpz_t mpc; + int ok; + + static int coef[N_CONSTRAINTS][N_VARS+N_PARAMETERS+1] = { + { 2, 3, 0, 0, -8 }, + { 4, -1, 0, 0, -4 }, + { 0, -1, 0, 1, 0 }, + { -1, 0, 1, 0, 0 }, + }; + ppl_dimension_type parameter_dim[N_PARAMETERS]; + + program_name = argv[0]; + if (argc != 1) { + fprintf(stderr, "usage: %s\n", program_name); + exit(1); + } + if (ppl_initialize() < 0) + fatal("cannot initialize the Parma Polyhedra Library"); + + for (i=0; i<N_PARAMETERS; ++i) + parameter_dim[i] = i + N_VARS; + ppl_new_PIP_Problem_from_space_dimension(&pip, N_VARS+N_PARAMETERS); + ppl_PIP_Problem_add_to_parameter_space_dimensions(pip, parameter_dim, + N_PARAMETERS); + mpz_init(mpc); + ppl_new_Coefficient(&c); + for (i=0; i<N_CONSTRAINTS; ++i) { + ppl_new_Linear_Expression(&le); + for (j=0; j<N_VARS+N_PARAMETERS; ++j) { + mpz_set_si(mpc, coef[i][j]); + ppl_assign_Coefficient_from_mpz_t(c, mpc); + ppl_Linear_Expression_add_to_coefficient(le, j, c); + } + mpz_set_si(mpc, coef[i][j]); + ppl_assign_Coefficient_from_mpz_t(c, mpc); + ppl_Linear_Expression_add_to_inhomogeneous(le, c); + ppl_new_Constraint(&ct, le, PPL_CONSTRAINT_TYPE_GREATER_OR_EQUAL); + ppl_PIP_Problem_add_constraint(pip, ct); + ppl_delete_Constraint(ct); + ppl_delete_Linear_Expression(le); + } + ppl_delete_Coefficient(c); + mpz_clear(mpc); + + ok = (ppl_PIP_Problem_solve(pip) == PPL_PIP_PROBLEM_STATUS_OPTIMIZED); + if (ok) { + ppl_dimension_type dim; + ppl_const_PIP_Tree_Node_t solution; + ppl_PIP_Problem_space_dimension(pip, &dim); + ppl_PPL_Problem_solution(pip, &solution); + /* display_solution(solution, N_VARS, N_PARAMETERS, parameter_dim); */ + } + + ppl_delete_PIP_Problem(pip); + ppl_finalize(); + return ok ? 0 : 1; +}

1 0

[GIT] ppl/ppl(pip): New parameter choice method. Updated the C interface.
by François Galea 23 Oct '09

23 Oct '09

Module: ppl/ppl Branch: pip Commit: 4c95e73449a6e069596deac0a5780cd6d0e4cb23 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4c95e73449a6… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Oct 23 17:00:25 2009 +0200 New parameter choice method. Updated the C interface. --- interfaces/C/ppl_c_header.h | 4 ++-- interfaces/C/ppl_c_implementation_common.cc | 12 ++++++++++++ src/PIP_Problem.cc | 27 +++++++++++++++++++++++++++ src/PIP_Problem.defs.hh | 15 +++++++++++++-- 4 files changed, 54 insertions(+), 4 deletions(-) diff --git a/interfaces/C/ppl_c_header.h b/interfaces/C/ppl_c_header.h index 8d48fbe..8dc92be 100644 --- a/interfaces/C/ppl_c_header.h +++ b/interfaces/C/ppl_c_header.h @@ -2720,11 +2720,11 @@ PPL_PROTO((ppl_PIP_Problem_t pip, /*! \relates ppl_PIP_Problem_tag \brief Sets the space dimensions that are specified in first \p n positions - of the array \p ds to be integer dimensions of problem \p pip. + of the array \p ds to be parameter dimensions of problem \p pip. The presence of duplicates in \p ds is a waste but an innocuous one. */ int -ppl_PIP_Problem_add_to_integer_space_dimensions +ppl_PIP_Problem_add_to_parameter_space_dimensions PPL_PROTO((ppl_PIP_Problem_t pip, ppl_dimension_type ds[], size_t n)); /*! \relates ppl_PIP_Problem_tag \brief diff --git a/interfaces/C/ppl_c_implementation_common.cc b/interfaces/C/ppl_c_implementation_common.cc index 2d5f45d..1ef11f1 100644 --- a/interfaces/C/ppl_c_implementation_common.cc +++ b/interfaces/C/ppl_c_implementation_common.cc @@ -2196,6 +2196,18 @@ ppl_PIP_Problem_add_space_dimensions_and_embed(ppl_PIP_Problem_t pip, } CATCH_ALL int +ppl_PIP_Problem_add_to_parameter_space_dimensions(ppl_PIP_Problem_t pip, + ppl_dimension_type ds[], + size_t n) try { + PIP_Problem& ppip = *to_nonconst(pip); + Variables_Set vars; + for (ppl_dimension_type i = n; i-- > 0; ) + vars.insert(ds[i]); + ppip.add_to_parameter_space_dimensions(vars); + return 0; +} +CATCH_ALL +int ppl_PIP_Problem_add_constraint(ppl_PIP_Problem_t pip, ppl_const_Constraint_t c) try { const Constraint& cc = *to_const(c); diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index f2fb1c3..b228911 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -390,6 +390,33 @@ PPL::PIP_Problem } void +PPL::PIP_Problem +::add_to_parameter_space_dimensions(const Variables_Set& p_vars) { + if (p_vars.space_dimension() > external_space_dim) + throw std::invalid_argument("PPL::PIP_Problem::" + "add_to_parameter_space_dimension(p_vars):\n" + "*this and p_vars are dimension" + "incompatible."); + const dimension_type original_size = parameters.size(); + parameters.insert(p_vars.begin(), p_vars.end()); + // Do not allow to turn variables into parameters + Variables_Set::const_iterator p; + Variables_Set::const_iterator end = p_vars.end(); + for (p=p_vars.begin(); p!=end; ++p) { + if (*p < internal_space_dim) { + throw std::invalid_argument("PPL::PIP_Problem::" + "add_to_parameter_space_dimension(p_vars):" + "p_vars contain variable indices."); + } + } + + // If a new parameter was inserted, set the internal status to + // PARTIALLY_SATISFIABLE. + if (parameters.size() != original_size && status != UNSATISFIABLE) + status = PARTIALLY_SATISFIABLE; +} + +void PPL::PIP_Problem::add_constraint(const Constraint& c) { if (c.space_dimension() > external_space_dim) { std::ostringstream s; diff --git a/src/PIP_Problem.defs.hh b/src/PIP_Problem.defs.hh index 0096879..64fe7e9 100644 --- a/src/PIP_Problem.defs.hh +++ b/src/PIP_Problem.defs.hh @@ -87,7 +87,7 @@ class Parma_Polyhedra_Library::PIP_Problem { public: //! Builds a trivial PIP problem. /*! - A trivial PIP problem requires to maximize the objective function + A trivial PIP problem requires to minimize the objective function \f$0\f$ on a vector space under no constraints and with no parameters: the origin of the vector space is an optimal solution. @@ -108,7 +108,8 @@ public: interpreted as parameters. \param dim - The dimension of the vector space enclosing \p *this. + The dimension of the vector space (variables and parameters) enclosing + \p *this. \param first An input iterator to the start of the sequence of constraints. @@ -208,6 +209,16 @@ public: dimension_type m_pip_params); /*! \brief + Sets the space dimensions whose indexes which are in set \p p_vars to be + parameter space dimensions. + + \exception std::invalid_argument + Thrown if some index in \p p_vars does not correspond to + a space dimension in \p *this. + */ + void add_to_parameter_space_dimensions(const Variables_Set& p_vars); + + /*! \brief Adds a copy of constraint \p c to the PIP problem. \exception std::invalid_argument

1 0