June 2010 - PPL-devel - BUGSENG Mailman

Problems with test suite on alpha
by Michael Tautschnig 09 Sep '10

09 Sep '10

Hi PPL developers, I've reported problems with some test cases because of suspected gcc bugs on alpha earlier already. Now it seems that even more test cases are broken, most probably because of the very same bug (I suspect it to be http://gcc.gnu.org/bugzilla/show_bug.cgi?id=8966). My question now is: How to proceed? Shall I specifically disable the failing test cases by surrounding them with an #ifndef __alpha__ or disable the entire test suite on alpha? Thanks, Michael

2 6

[GIT] ppl/ppl(master): Improved specification and implementation of erase_artificials().
by Enea Zaffanella 28 Jun '10

28 Jun '10

Module: ppl/ppl Branch: master Commit: 16cbdda5d7d356f811034951fa25bb45f89aa9cc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=16cbdda5d7d3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Jun 28 09:36:56 2010 +0200 Improved specification and implementation of erase_artificials(). --- src/MIP_Problem.cc | 29 ++++++++++++++--------------- src/MIP_Problem.defs.hh | 12 ++++++++++++ 2 files changed, 26 insertions(+), 15 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index 30e88e6..c388715 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -832,8 +832,8 @@ PPL::MIP_Problem::process_pending_constraints() { base[i] = artificial_index; ++artificial_index; } - // The last column index of the tableau containing an artificial variable. - const dimension_type end_artificials = artificial_index - 1; + // One past the last tableau column index containing an artificial variable. + const dimension_type end_artificials = artificial_index; // Set the extra-coefficient of the cost functions to record its sign. // This is done to keep track of the possible sign's inversion. @@ -1326,16 +1326,18 @@ PPL::MIP_Problem::compute_simplex_using_exact_pricing() { void PPL::MIP_Problem::erase_artificials(const dimension_type begin_artificials, const dimension_type end_artificials) { - const dimension_type tableau_last_index = tableau.num_columns() - 1; + PPL_ASSERT(0 < begin_artificials && begin_artificials < end_artificials); + + const dimension_type old_last_column = tableau.num_columns() - 1; dimension_type tableau_n_rows = tableau.num_rows(); // Step 1: try to remove from the base all the remaining slack variables. for (dimension_type i = 0; i < tableau_n_rows; ++i) - if (begin_artificials <= base[i] && base[i] <= end_artificials) { + if (begin_artificials <= base[i] && base[i] < end_artificials) { // Search for a non-zero element to enter the base. Row& tableau_i = tableau[i]; bool redundant = true; - for (dimension_type j = end_artificials+1; j-- > 1; ) - if (!(begin_artificials <= j && j <= end_artificials) + for (dimension_type j = end_artificials; j-- > 1; ) + if (!(begin_artificials <= j && j < end_artificials) && tableau_i[j] != 0) { pivot(j, i); redundant = false; @@ -1360,21 +1362,18 @@ PPL::MIP_Problem::erase_artificials(const dimension_type begin_artificials, // Step 2: Adjust data structures so as to enter phase 2 of the simplex. - // Compute the dimensions of the new tableau. - dimension_type num_artificials = 0; - for (dimension_type i = end_artificials + 1; i-- > 1; ) - if (begin_artificials <= i && i <= end_artificials) { - ++num_artificials; - tableau.remove_trailing_columns(1); - } + // Resize the tableau. + const dimension_type num_artificials = end_artificials - begin_artificials; + tableau.remove_trailing_columns(num_artificials); // Zero the last column of the tableau. + const dimension_type new_last_column = tableau.num_columns() - 1; for (dimension_type i = tableau_n_rows; i-- > 0; ) - tableau[i][tableau.num_columns()-1] = 0; + tableau[i][new_last_column] = 0; // ... then properly set the element in the (new) last column, // encoding the kind of optimization; ... - working_cost[tableau.num_columns()-1] = working_cost[tableau_last_index]; + working_cost[new_last_column] = working_cost[old_last_column]; // ... and finally remove redundant columns. const dimension_type working_cost_new_size = working_cost.size() - num_artificials; diff --git a/src/MIP_Problem.defs.hh b/src/MIP_Problem.defs.hh index f39f453..63a39db 100644 --- a/src/MIP_Problem.defs.hh +++ b/src/MIP_Problem.defs.hh @@ -728,6 +728,18 @@ private: /*! \brief Drop unnecessary artificial variables from the tableau and get ready for the second phase of the simplex algorithm. + + \note + The two parameters denote a STL-like half-open range. + It is assumed that \p begin_artificials is strictly greater than 0 + and smaller than \p end_artificials. + + \param begin_artificials + The start of the tableau column index range for artificial variables. + + \param end_artificials + The end of the tableau column index range for artificial variables. + Note that column index end_artificial is \e excluded from the range. */ void erase_artificials(dimension_type begin_artificials, dimension_type end_artificials);

1 0

[GIT] ppl/ppl(master): Use PPL_ASSERT() instead of plain assert().
by Enea Zaffanella 28 Jun '10

28 Jun '10

Module: ppl/ppl Branch: master Commit: e23face68ebfc2b001ed1fa82014ec61cd8be0db URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e23face68ebf… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon Jun 28 08:48:32 2010 +0200 Use PPL_ASSERT() instead of plain assert(). --- src/MIP_Problem.cc | 12 ++++++------ 1 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index 72b6c87..30e88e6 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -456,10 +456,10 @@ PPL::MIP_Problem std::deque<bool>& is_nonnegative_variable, std::deque<bool>& is_remergeable_variable) const { // Initially all containers are empty. - assert(is_tableau_constraint.empty() - && is_satisfied_inequality.empty() - && is_nonnegative_variable.empty() - && is_remergeable_variable.empty()); + PPL_ASSERT(is_tableau_constraint.empty() + && is_satisfied_inequality.empty() + && is_nonnegative_variable.empty() + && is_remergeable_variable.empty()); const dimension_type cs_space_dim = external_space_dim; const dimension_type cs_num_rows = input_cs.size(); @@ -616,7 +616,7 @@ PPL::MIP_Problem is_nonnegative_variable[nonzero_var_index] = true; if (nonzero_coeff_column_index < mapping_size) { // Remember to merge back the positive and negative parts. - assert(nonzero_var_index < internal_space_dim); + PPL_ASSERT(nonzero_var_index < internal_space_dim); is_remergeable_variable[nonzero_var_index] = true; } } @@ -625,7 +625,7 @@ PPL::MIP_Problem } // Cases 8-9: apply method A. else { - assert(cs_i.is_inequality()); + PPL_ASSERT(cs_i.is_inequality()); ++additional_slack_variables; } }

1 0

[GIT] ppl/ppl(master): Improved MIP_Problem preprocessing phase and solved an efficiency bug.
by Enea Zaffanella 26 Jun '10

26 Jun '10

Module: ppl/ppl Branch: master Commit: 40ab909d8ec60f8391fb7e7de21493219f23d81a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=40ab909d8ec6… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Jun 26 21:40:44 2010 +0200 Improved MIP_Problem preprocessing phase and solved an efficiency bug. Rewritten private methods parse_constraints(), merge_split_variable() and process_pending_constraints(): specification clarified and implementation improved to avoid allocating more tableau rows and columns than needed. This results in an overall speedup, in particular when solving problems incrementally. --- src/MIP_Problem.cc | 458 ++++++++++++++++++++++++++-------------------- src/MIP_Problem.defs.hh | 95 ++++++---- 2 files changed, 314 insertions(+), 239 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=40ab909d…

1 0

[GIT] ppl/ppl(sparse_matrices): New commits
by Roberto Bagnara 19 Jun '10

19 Jun '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9488ac9a2d22… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Jun 18 10:26:29 2010 +0200 CO_Tree: optimize const and non-const go_down_searching_key() methods for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fee348d7653c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Jun 18 09:47:25 2010 +0200 CO_Tree: optimize redistribute_elements_in_subtree_helper() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f4121b07435c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 23:17:18 2010 +0200 CO_Tree: optimize redistribute_elements_in_subtree_helper() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9dc20d0452db… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 22:06:41 2010 +0200 CO_Tree: use follow_right_childs_with_value(), in compact_elements_in_the_rightmost_end(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fc9eeaf904d8… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 22:06:17 2010 +0200 CO_Tree: use follow_left_childs_with_value() and follow_right_childs_with_value(), in erase(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a676a6d5df7b… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 21:47:02 2010 +0200 CO_Tree: fix follow_left_childs_with_value() and follow_right_childs_with_value() methods of inorder_iterator and inorder_const_iterator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=456d4f2cb9c0… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 21:41:36 2010 +0200 CO_Tree: use follow_right_childs() in redistribute_elements_in_subtree(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3c42e79313bb… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 21:40:42 2010 +0200 Remove .orig file, tracked by mistake. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=97ac0c0b1307… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 21:36:02 2010 +0200 CO_Tree: add assertions in follow_left_childs() and follow_right_childs() methods, in inorder_iterator and inorder_const_iterator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9b054f66c3ff… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 21:07:50 2010 +0200 CO_Tree: add methods follow_left_childs_with_value() and follow_right_childs_with_value(), in inorder_iterator and inorder_const_iterator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a0189482a5ea… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 21:07:12 2010 +0200 CO_Tree: add methods follow_left_childs() and follow_right_childs(), in inorder_iterator and inorder_const_iterator. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bedbfab1743e… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:24:33 2010 +0200 CO_Tree::unordered_const_iterator: optimize operator++(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=459fb16367b5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:23:54 2010 +0200 CO_Tree::unordered_iterator: optimize operator++(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=133aa5392b2c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:22:10 2010 +0200 CO_Tree::inorder_const_iterator: optimize get_right_child_value() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4fe1619de8d7… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:21:30 2010 +0200 CO_Tree::inorder_const_iterator: optimize get_left_child_value() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=10a4a7e1bf04… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:20:00 2010 +0200 CO_Tree::inorder_const_iterator: optimize operator==() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d49287a91b68… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:16:38 2010 +0200 CO_Tree::inorder_iterator: optimize get_right_child_value() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22afc7b6f3a2… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:13:38 2010 +0200 CO_Tree::inorder_iterator: optimize get_left_child_value() for the DFS layout. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6da8d06efe7c… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Jun 17 19:09:35 2010 +0200 CO_Tree::inorder_iterator: optimize operator->() for the DFS layout.

1 0

[GIT] ppl/ppl(master): Updated from Libtool 2.2.10.
by Roberto Bagnara 17 Jun '10

17 Jun '10

Module: ppl/ppl Branch: master Commit: 3e33e00ded13fdfae2f93dee29c5b3e40ba4287a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3e33e00ded13… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 17 16:29:18 2010 +0200 Updated from Libtool 2.2.10. --- Watchdog/config.guess | 13 +- Watchdog/config.sub | 68 ++- Watchdog/install-sh | 8 +- Watchdog/ltmain.sh | 1747 ++++++++++++++++++++++++++------------------ Watchdog/m4/libtool.m4 | 998 ++++++++++++++------------ Watchdog/m4/ltoptions.m4 | 13 +- Watchdog/m4/ltversion.m4 | 10 +- Watchdog/m4/lt~obsolete.m4 | 12 +- config.guess | 13 +- config.sub | 68 ++- install-sh | 8 +- ltmain.sh | 1747 ++++++++++++++++++++++++++------------------ m4/libtool.m4 | 998 ++++++++++++++------------ m4/ltoptions.m4 | 13 +- m4/ltversion.m4 | 10 +- m4/lt~obsolete.m4 | 12 +- 16 files changed, 3326 insertions(+), 2412 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=3e33e00d…

1 0

[GIT] ppl/ppl(master): Added missing argument names.
by Roberto Bagnara 17 Jun '10

17 Jun '10

Module: ppl/ppl Branch: master Commit: 044730210d62651c866a7f368e848d4da9d9e86b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=044730210d62… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 17 16:20:34 2010 +0200 Added missing argument names. --- src/Box.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Box.defs.hh b/src/Box.defs.hh index e812c45..4d6f412 100644 --- a/src/Box.defs.hh +++ b/src/Box.defs.hh @@ -718,7 +718,7 @@ public: \exception std::invalid_argument Thrown if \p x and \p y are dimension-incompatible. */ - bool contains(const Box&) const; + bool contains(const Box& y) const; /*! \brief Returns <CODE>true</CODE> if and only if \p *this strictly contains \p y. @@ -726,7 +726,7 @@ public: \exception std::invalid_argument Thrown if \p x and \p y are dimension-incompatible. */ - bool strictly_contains(const Box&) const; + bool strictly_contains(const Box& y) const; /*! \brief Returns <CODE>true</CODE> if and only if \p *this and \p y are disjoint.

1 0

Re: [PPL-devel] floating point behaviour
by Roberto Bagnara 17 Jun '10

17 Jun '10

On 06/15/10 23:30, piotrm wrote: > That explains most of it. Thanks! > > The man page suggest that the restore and set rounding mode are to be > used merely if one relies on some rounding mode. I'm not interested in > particular rounding modes. I am, however, interested in floats printed > in such a way that they can be scanned back in as floats, and "0.:00000" > is not an example of such a float. I did notice that restoring rounding > mode lets one print floats "correctly" but I'm skeptical that > restore/set rounding mode before / after printing things is the intended > usage of ppl. Indeed. But the problem is that you stumbled upon a bug in the implementation of printf(). Apparently, the implementation you are using does weird things when invoked on a non-default rounding mode (notice that ':' is ASCII 3A, one more than ASCII 39, which corresponds to '9'). Unfortunately, if you approach the authors of your printf() and try to convince them that there is a problem, they will react badly (been there, done that). This is the reason why in the PPL we have our own input and output routines. All the best, Roberto -- 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

[GIT] ppl/ppl(sparse_matrices): New commits
by Roberto Bagnara 17 Jun '10

17 Jun '10

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c98797b0e563… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 22:20:38 2010 +0200 Unlimited_Sparse_Row_Over_Linear_Sequence: call reset() on all zeroes, in combine(). WARNING: this breaks the custom_slist backend. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cc9b02a72356… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 21:17:36 2010 +0200 Unlimited_Sparse_Row_Over_Linear_Sequence: temporarily add unneeded include, to please KDevelop4. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f394b7c16f2a… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 21:15:44 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: call reset() on all zeroes, in combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0c3979f1e3f3… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 21:03:03 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: optimize combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=62e29d3d5f33… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 20:54:22 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: optimize combine_needs_first(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=62ceeddd3755… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 20:43:40 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: call reset() on all zeroes, in combine_needs_first(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=044f75fa3c01… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 20:33:46 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: simplify code in combine_needs_first(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=13bfb7fd5172… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Wed Jun 16 19:38:05 2010 +0200 Unlimited_Sparse_Row_Over_CO_Tree: simplify code in combine(). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a592a13b118e… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sat Jun 5 11:53:48 2010 +0200 CO_Tree: fix comment.

1 0

Fwd: Re: floating point behaviour
by Roberto Bagnara 16 Jun '10

16 Jun '10

-------- Original Message -------- Subject: Re: [PPL-devel] floating point behaviour Date: Tue, 15 Jun 2010 17:30:12 -0400 From: piotrm <piotrm(a)cs.umd.edu> To: Roberto Bagnara <bagnara(a)cs.unipr.it> That explains most of it. Thanks! The man page suggest that the restore and set rounding mode are to be used merely if one relies on some rounding mode. I'm not interested in particular rounding modes. I am, however, interested in floats printed in such a way that they can be scanned back in as floats, and "0.:00000" is not an example of such a float. I did notice that restoring rounding mode lets one print floats "correctly" but I'm skeptical that restore/set rounding mode before / after printing things is the intended usage of ppl. Thanks for the help, Piotr On Jun 15, 2010, at 16:48, Roberto Bagnara wrote: > On 06/15/2010 09:36 PM, piotrm wrote: >> Apologies if this is not the right place to inquire about this, >> cannot >> seem to find any other outlet: > > Hi piotrm, > > you should check out the library documentation. > >> Is it correct behavior for floating point calculations to be done >> differently once ppl.hh is included in a c++ program as well as the >> printing of floats? Here is an example of what I'm referring to: >> >> #include <cstdio> >> >> int main() { >> double a = 0.50000000000000011102230246251565404236316680908203125; >> double b = 0.5f / a; >> printf("%0.60f %f %0.60f %f\n", a, a, b, b); >> return 0; >> } >> >> This prints (for me) >> >> 0.500000000000000111022302462515654042363166809082031250000000 >> 0.500000 >> 0.999999999999999777955395074968691915273666381835937500000000 >> 1.000000 >> >> If I include ppl, as in below: >> >> #include <cstdio> >> #include "ppl.hh" >> >> int main() { >> double a = 0.50000000000000011102230246251565404236316680908203125; >> double b = 0.5f / a; >> printf("%0.60f %f %0.60f %f\n", a, a, b, b); >> return 0; >> } >> >> I get the following >> >> 0.500000000000000111022302462515654042363166809082031250000000 >> 0.500000 >> 0.999999999999999888977697537484345957636833190917968750000000 >> 0.:00000 >> >> Notice the strange way the b is printed the second time. I also found >> instances where numbers that are close to 0.01 get printed as >> 0.00:000 >> >> Is this perhaps an installation issue on my part? I noticed this >> using >> the OCaml interface, that is, use of ppl changed the behavior of the >> float types in OCaml in the same way the behavior is changed in C++ >> above. > > See the documentation of > > void Parma_Polyhedra_Library::set_rounding_for_PPL() > void Parma_Polyhedra_Library::restore_pre_PPL_rounding() > void Parma_Polyhedra_Library::initialize() > void Parma_Polyhedra_Library::finalize() > > Use also `man libppl' to see the role played by the > PPL_NO_AUTOMATIC_INITIALIZATION macro. > All the best, > > Roberto > > -- > 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