- PPL-devel - BUGSENG Mailman

Fwd: Question regarding OCaml Interface of PPL
by Roberto Bagnara 07 Mar '12

07 Mar '12

-------- Original Message -------- Subject: Question regarding OCaml Interface of PPL Date: Tue, 6 Mar 2012 13:49:10 -0500 From: Brian Pak <bpak(a)andrew.cmu.edu> To: support(a)bugseng.com Hi all, I'm a student in Carnegie Mellon University in US, and trying to use PPL for my research project. First, thank you for your great work! It is truly amazing :) I was fiddling with the library and interfaces (especially OCaml), and got stuck on one thing. I wanted to use 'get_interval' or 'get_lower/upper_bound' functions in Box class, but it seems it's not available in OCaml interface. Is there any way to get around this? I'm not too familiar with these mathematical concepts (I'm reading materials to grasp better understanding, though), but here's what I want to accomplish: - Given n variables where each of them is bounded (in some linear relation) -- build a constraint system out of these - Generate an n-polytope that above equations describe (currently planning to use C_Polyhedron) - I want to enumerate integer points in this polytope, but that's known to be difficult (please correct me if I'm wrong) - Create an n-dimensional Box object from C_Polyhedron we generated (which is basically a hyper-rectangle surrounding the polytope, possibly?) - Get the interval (low and upper bound) for each variable for the Box above. - Pick a random point in the Box (hopefully this is easier since we know the interval of each dimension) - Perform a rejection sampling to check if the picked point is contained in the polytope. - There doesn't seem to be a way to do this natively, so I'm planning to use the trick where I make a very small polytope that is constrained by Variable(0) == c_1 && Variable(1) == c_2 && … && Variable(n-1) == c_n, and use 'contains' function to check if it's contained in the polytope (represented by C_Polyhedron object above). Thanks for your help in advance! :D -Brian

2 2

[GIT] ppl/ppl(master): Avoid implicit conversions to bool ( prefer explicit tests against zero).
by Enea Zaffanella 01 Mar '12

01 Mar '12

Module: ppl/ppl Branch: master Commit: 7cab131006b0385c9855b298de5e0b85d8f05101 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7cab131006b0… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 1 22:24:52 2012 +0100 Avoid implicit conversions to bool (prefer explicit tests against zero). Detected by ECLAIR service utypflag. --- src/Polyhedron_public.cc | 12 ++++++++---- 1 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index 0f8e3cf..31f2c7d 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -1191,28 +1191,32 @@ PPL::Polyhedron::OK(bool check_not_empty) const { for (dimension_type i = sat_c.num_rows(); i-- > 0; ) { const Generator tmp_gen = gen_sys[i]; const Bit_Row tmp_sat = sat_c[i]; - for (dimension_type j = sat_c.num_columns(); j-- > 0; ) - if (Scalar_Products::sign(con_sys[j], tmp_gen) != tmp_sat[j]) { + for (dimension_type j = sat_c.num_columns(); j-- > 0; ) { + const bool sat_j = (Scalar_Products::sign(con_sys[j], tmp_gen) == 0); + if (sat_j == tmp_sat[j]) { #ifndef NDEBUG cerr << "sat_c is declared up-to-date, but it is not!" << endl; #endif goto bomb; } + } } if (sat_g_is_up_to_date()) for (dimension_type i = sat_g.num_rows(); i-- > 0; ) { const Constraint tmp_con = con_sys[i]; const Bit_Row tmp_sat = sat_g[i]; - for (dimension_type j = sat_g.num_columns(); j-- > 0; ) - if (Scalar_Products::sign(tmp_con, gen_sys[j]) != tmp_sat[j]) { + for (dimension_type j = sat_g.num_columns(); j-- > 0; ) { + const bool sat_j = (Scalar_Products::sign(tmp_con, gen_sys[j]) == 0); + if (sat_j == tmp_sat[j]) { #ifndef NDEBUG cerr << "sat_g is declared up-to-date, but it is not!" << endl; #endif goto bomb; } + } } if (has_pending_constraints()) {

1 0

[GIT] ppl/ppl(master): Avoid implicit cast narrowing a signed integer value .
by Enea Zaffanella 01 Mar '12

01 Mar '12

Module: ppl/ppl Branch: master Commit: b6c3449ce47087c1e3957d2e37f717f5239c9796 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b6c3449ce470… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 1 22:23:29 2012 +0100 Avoid implicit cast narrowing a signed integer value. Detected by ECLAIR service utypflag. --- src/Row_Flags.cc | 3 +-- 1 files changed, 1 insertions(+), 2 deletions(-) diff --git a/src/Row_Flags.cc b/src/Row_Flags.cc index cb4d758..1d5a882 100644 --- a/src/Row_Flags.cc +++ b/src/Row_Flags.cc @@ -33,8 +33,7 @@ PPL::Row_Flags::ascii_dump(std::ostream& s) const { s << "0x"; std::ios::fmtflags old_flags = s.setf(std::ios::hex, std::ios::basefield); - const std::streamsize new_sz - = static_cast<std::streamsize>(2 * sizeof(Row_Flags::base_type)); + const int new_sz = 2 * static_cast<int>(sizeof(Row_Flags::base_type)); s << std::setw(new_sz) << std::setfill('0') << bits; s.flags(old_flags); }

1 0

[GIT] ppl/ppl(master): Removed unused static const data member.
by Enea Zaffanella 01 Mar '12

01 Mar '12

Module: ppl/ppl Branch: master Commit: 49f8811aeaabece9332d1fece40ac88e05e2c3d8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=49f8811aeaab… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 1 22:21:07 2012 +0100 Removed unused static const data member. --- src/Row_Flags.defs.hh | 3 --- 1 files changed, 0 insertions(+), 3 deletions(-) diff --git a/src/Row_Flags.defs.hh b/src/Row_Flags.defs.hh index cfff314..00f71ae 100644 --- a/src/Row_Flags.defs.hh +++ b/src/Row_Flags.defs.hh @@ -66,9 +66,6 @@ protected: //! Index of the first bit derived classes can use. static const unsigned first_free_bit = 0; - //! Total number of bits that can be stored. - static const unsigned num_bits = sizeof_to_bits(sizeof(base_type)); - //! Constructs an object with flags set as in \p n. explicit Row_Flags(base_type n);

1 0

[GIT] ppl/ppl(master): Avoid implicit coversion to bool.
by Enea Zaffanella 01 Mar '12

01 Mar '12

Module: ppl/ppl Branch: master Commit: ef23118849edd5ed1003afae43466566e63e1616 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ef23118849ed… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 1 22:17:42 2012 +0100 Avoid implicit coversion to bool. Detected by Boolean service utypflag. --- src/assert.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/assert.hh b/src/assert.hh index 09c84a1..35c2ef1 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -61,7 +61,7 @@ site: http://bugseng.com/products/ppl/ . */ W_Traits::Threshold old_weight__ = W_Traits::weight; \ PPL_ASSERT_IMPL_(cond__); \ PPL_ASSERT_IMPL_(old_weight__ == W_Traits::weight \ - && "PPL_ASSERT_HEAVY have to be used here"); \ + && ("PPL_ASSERT_HEAVY has to be used here" != 0)); \ } while (false) #endif // !defined(NDEBUG) && PPL_DEBUG_PPL_ASSERT

1 0

[GIT] ppl/ppl(master): Avoid implicit conversions to bool.
by Enea Zaffanella 01 Mar '12

01 Mar '12

Module: ppl/ppl Branch: master Commit: d745cfa91fc74f852df242bc0507ca2a53a0a14a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d745cfa91fc7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 1 22:19:18 2012 +0100 Avoid implicit conversions to bool. Detected by ECLAIR service utypflag. --- interfaces/C/ppl_c_implementation_common.cc | 2 +- .../C/ppl_c_implementation_common.inlines.hh | 2 +- interfaces/C/ppl_interface_generator_c_cc_code.m4 | 2 +- src/Pointset_Powerset.templates.hh | 3 ++- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/interfaces/C/ppl_c_implementation_common.cc b/interfaces/C/ppl_c_implementation_common.cc index 4422053..045765c 100644 --- a/interfaces/C/ppl_c_implementation_common.cc +++ b/interfaces/C/ppl_c_implementation_common.cc @@ -2430,7 +2430,7 @@ int ppl_PIP_Decision_Node_get_child_node(ppl_const_PIP_Decision_Node_t pip_dec, int b, ppl_const_PIP_Tree_Node_t* pip_tree) try { - *pip_tree = to_const(to_const(pip_dec)->child_node(b)); + *pip_tree = to_const(to_const(pip_dec)->child_node(b != 0)); return 0; } CATCH_ALL diff --git a/interfaces/C/ppl_c_implementation_common.inlines.hh b/interfaces/C/ppl_c_implementation_common.inlines.hh index 5a8f853..3057913 100644 --- a/interfaces/C/ppl_c_implementation_common.inlines.hh +++ b/interfaces/C/ppl_c_implementation_common.inlines.hh @@ -178,7 +178,7 @@ Array_Partial_Function_Wrapper::has_empty_codomain() const { break; } } - return empty; + return (empty != 0); } inline dimension_type diff --git a/interfaces/C/ppl_interface_generator_c_cc_code.m4 b/interfaces/C/ppl_interface_generator_c_cc_code.m4 index 87d446d..478a36a 100644 --- a/interfaces/C/ppl_interface_generator_c_cc_code.m4 +++ b/interfaces/C/ppl_interface_generator_c_cc_code.m4 @@ -1381,7 +1381,7 @@ ppl_@CLASS@_wrap_assign for (ppl_dimension_type i = n; i-- > 0; ) vars.insert(ds[i]); const Constraint_System* ccs = to_const(*pcs); - bool b = wrap_individually; + bool b = (wrap_individually != 0); pph.wrap_assign(vars, bounded_integer_type_width(w), bounded_integer_type_representation(r), diff --git a/src/Pointset_Powerset.templates.hh b/src/Pointset_Powerset.templates.hh index f2cb3c7..550573a 100644 --- a/src/Pointset_Powerset.templates.hh +++ b/src/Pointset_Powerset.templates.hh @@ -115,7 +115,8 @@ Pointset_Powerset<PSET>::concatenate_assign(const Pointset_Powerset& y) { new_x.sequence.push_back(zi); } ++xi; - if (abandon_expensive_computations && xi != x_end && y_begin != y_end) { + if ((abandon_expensive_computations != 0) + && (xi != x_end) && (y_begin != y_end)) { // Hurry up! PSET x_ph = xi->pointset(); for (++xi; xi != x_end; ++xi)

1 0

[GIT] ppl/ppl(master): Added missing parentheses around a macro arguments.
by Roberto Bagnara 29 Feb '12

29 Feb '12

Module: ppl/ppl Branch: master Commit: ae02418951a247595a8f8ade2090e3401bd8520c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ae02418951a2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Feb 29 21:41:34 2012 +0100 Added missing parentheses around a macro arguments. Detected by ECLAIR service macrbody. --- src/checked_numeric_limits.hh | 74 ++++++++++++++++++++-------------------- 1 files changed, 37 insertions(+), 37 deletions(-) diff --git a/src/checked_numeric_limits.hh b/src/checked_numeric_limits.hh index ba49fcd..caa3e1d 100644 --- a/src/checked_numeric_limits.hh +++ b/src/checked_numeric_limits.hh @@ -33,43 +33,43 @@ namespace std { using namespace Parma_Polyhedra_Library; #define PPL_SPECIALIZE_LIMITS_INT(T) \ -/*! \brief Partial specialization of std::numeric_limits. */ \ -template <typename Policy> \ - class numeric_limits<Checked_Number<T, Policy> > \ - : public numeric_limits<T> { \ - private: \ - typedef Checked_Number<T, Policy> Type; \ - \ - public: \ - static const bool has_infinity = Policy::has_infinity; \ - static const bool has_quiet_NaN = Policy::has_nan; \ + /*! \brief Partial specialization of std::numeric_limits. */ \ + template <typename Policy> \ + class numeric_limits<Checked_Number<PPL_U(T), Policy> > \ + : public numeric_limits<PPL_U(T)> { \ + private: \ + typedef Checked_Number<PPL_U(T), Policy> Type; \ + \ + public: \ + static const bool has_infinity = Policy::has_infinity; \ + static const bool has_quiet_NaN = Policy::has_nan; \ \ - static Type min() { \ - Type v; \ - v.raw_value() = Checked::Extended_Int<Policy, T>::min; \ - return v; \ - } \ + static Type min() { \ + Type v; \ + v.raw_value() = Checked::Extended_Int<Policy, PPL_U(T)>::min; \ + return v; \ + } \ \ - static Type max() { \ - Type v; \ - v.raw_value() = Checked::Extended_Int<Policy, T>::max; \ - return v; \ - } \ + static Type max() { \ + Type v; \ + v.raw_value() = Checked::Extended_Int<Policy, PPL_U(T)>::max; \ + return v; \ + } \ \ - static Type infinity() { \ - Type v; \ - Checked::assign_special<Policy>(v.raw_value(), VC_PLUS_INFINITY, \ - ROUND_IGNORE); \ - return v; \ - } \ + static Type infinity() { \ + Type v; \ + Checked::assign_special<Policy>(v.raw_value(), VC_PLUS_INFINITY, \ + ROUND_IGNORE); \ + return v; \ + } \ \ - static Type quiet_NaN() { \ - Type v; \ - Checked::assign_special<Policy>(v.raw_value(), VC_NAN, \ - ROUND_IGNORE); \ - return v; \ - } \ -}; + static Type quiet_NaN() { \ + Type v; \ + Checked::assign_special<Policy>(v.raw_value(), VC_NAN, \ + ROUND_IGNORE); \ + return v; \ + } \ + }; PPL_SPECIALIZE_LIMITS_INT(char) @@ -88,10 +88,10 @@ PPL_SPECIALIZE_LIMITS_INT(unsigned long long) #undef PPL_SPECIALIZE_LIMITS_INT #define PPL_SPECIALIZE_LIMITS_FLOAT(T) \ -/*! \brief Partial specialization of std::numeric_limits. */ \ -template <typename Policy> \ -struct numeric_limits<Checked_Number<T, Policy> > \ - : public numeric_limits<T> { \ + /*! \brief Partial specialization of std::numeric_limits. */ \ + template <typename Policy> \ + struct numeric_limits<Checked_Number<PPL_U(T), Policy> > \ + : public numeric_limits<PPL_U(T)> { \ }; #if PPL_SUPPORTED_FLOAT

1 0

[GIT] ppl/ppl(master): Avoid mixing plain character data with numeric data.
by Roberto Bagnara 29 Feb '12

29 Feb '12

Module: ppl/ppl Branch: master Commit: e7c06758ef7dfcbf8139b1158e702dcc56ce7ce8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e7c06758ef7d… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Feb 29 20:55:37 2012 +0100 Avoid mixing plain character data with numeric data. Detected by ECLAIR service utypflag. --- src/ppl-config.cc.in | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ppl-config.cc.in b/src/ppl-config.cc.in index 19518fe..6691fd5 100644 --- a/src/ppl-config.cc.in +++ b/src/ppl-config.cc.in @@ -174,13 +174,13 @@ to_lower(char c) { bool strcaseeq(const char* s1, const char* s2) { - while (*s1 != 0) { - if (*s2 == 0 || to_lower(*s1) != to_lower(*s2)) + while (*s1 != '\0') { + if (*s2 == '\0' || to_lower(*s1) != to_lower(*s2)) return false; ++s1; ++s2; } - return *s2 == 0; + return *s2 == '\0'; } void

1 0

[GIT] ppl/ppl(master): Code layout fixed.
by Roberto Bagnara 29 Feb '12

29 Feb '12

Module: ppl/ppl Branch: master Commit: 37adcae2f9399565ab4052853371f2fd446c003e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=37adcae2f939… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Feb 29 20:55:05 2012 +0100 Code layout fixed. --- src/ppl-config.cc.in | 12 ++++++++---- 1 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ppl-config.cc.in b/src/ppl-config.cc.in index e54519d..19518fe 100644 --- a/src/ppl-config.cc.in +++ b/src/ppl-config.cc.in @@ -158,14 +158,18 @@ warning(const char* format, ...) { } */ -void internal_error() __attribute__((__noreturn__)); +void +internal_error() __attribute__((__noreturn__)); -void internal_error() { +void +internal_error() { fatal("internal error: please submit a bug report to ppl-devel(a)cs.unipr.it"); } -inline char to_lower(char c) { - return static_cast<char>(tolower(static_cast<int>(static_cast<unsigned char>(c)))); +inline char +to_lower(char c) { + return + static_cast<char>(tolower(static_cast<int>(static_cast<unsigned char>(c)))); } bool

1 0

[GIT] ppl/ppl(master): Updated.
by Roberto Bagnara 29 Feb '12

29 Feb '12

Module: ppl/ppl Branch: master Commit: c8f677733f78eda065f381d50d00afd7a24113f9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c8f677733f78… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Feb 29 10:36:23 2012 +0100 Updated. --- CREDITS | 16 ++++++++-------- 1 files changed, 8 insertions(+), 8 deletions(-) diff --git a/CREDITS b/CREDITS index 82b9bf7..12fe199 100644 --- a/CREDITS +++ b/CREDITS @@ -199,10 +199,9 @@ People: this possibility, porting the PPL to the ARM's ABIs would have taken ages. - Bruno Haible [19] (ILOG) made it possible (by writing the - AC_LIB_LINKFLAGS macro and explaining how - to use it) to allow the use of versions of the - GMP library installed in nonstandard places. + Bruno Haible [19] (ILOG) helped us in our first steps towards + using versions of the GMP library installed in + nonstandard places. Bertrand Jeannet [20] (IRISA) wrote the New Polka library [21] and made it available. We had several @@ -236,7 +235,8 @@ People: analyze the same Prolog programs. Since these systems did not share a single line of code, this gave us excellent opportunities for our - initial testing and debugging work. + initial testing and debugging work. Fred has + also helped us to port the PPL to Mac OS X. Ken Mixter (then at Carnegie Mellon University) provided useful feedback while working on an @@ -321,9 +321,9 @@ We are grateful for the following contributions: numerical abstractions and how the PPL can help. Special thanks go to Albert Cohen [57] for this sponsorship. -- INRIA [56] is supporting Abramo Bagnara from January 1st to May 31st, - 2009, to work on the PPL and its development infrastructure. - Many thanks go, in particular, to Albert Cohen [57]. +- INRIA [56] supported the work of Abramo Bagnara from January 1st to + May 31st, 2009, to work on the PPL and its development + infrastructure. Many thanks go, in particular, to Albert Cohen [57]. Some of our research work has been partly supported by the following

1 0