September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Fixed operator>>(std::istream&, Interval< Boundary, Info>&).
by Roberto Bagnara 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: floating_point Commit: cebcfe41cc8a24316f56e9697fb4025e1c1045d7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cebcfe41cc8a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:34:32 2009 +0200 Fixed operator>>(std::istream&, Interval<Boundary, Info>&). --- src/Interval.templates.hh | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Interval.templates.hh b/src/Interval.templates.hh index fcfecf6..f9d3f1e 100644 --- a/src/Interval.templates.hh +++ b/src/Interval.templates.hh @@ -234,8 +234,9 @@ operator>>(std::istream& is, Interval<Boundary, Info>& x) { bool upper_boundary_infinity = false; switch (lower_r) { case V_EQ: + case V_GE: break; - case V_LE: + case V_GT: lower_open = true; break; case V_EQ_MINUS_INFINITY: @@ -254,8 +255,9 @@ operator>>(std::istream& is, Interval<Boundary, Info>& x) { } switch (upper_r) { case V_EQ: + case V_LE: break; - case V_GE: + case V_LT: upper_open = true; break; case V_EQ_MINUS_INFINITY:

1 0

[GIT] ppl/ppl(floating_point): Spurious print statement removed.
by Roberto Bagnara 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 8f06b8a321099311d83ddceba3786d7ff857543b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8f06b8a32109… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:32:31 2009 +0200 Spurious print statement removed. --- src/Interval.templates.hh | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/src/Interval.templates.hh b/src/Interval.templates.hh index 1e0b3f8..fcfecf6 100644 --- a/src/Interval.templates.hh +++ b/src/Interval.templates.hh @@ -115,7 +115,6 @@ Interval<Boundary, Info>::Interval(const char* s) { assign(EMPTY); break; default: - std::cerr << "lower_r = " << lower_r << std::endl; PPL_ASSERT(false); } switch (upper_r) {

1 0

[GIT] ppl/ppl(master): Fixed operator>>(std::istream&, Interval<Boundary, Info>&).
by Roberto Bagnara 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: master Commit: 513d2127e55faa6f5e7d29938b7315203a712df2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=513d2127e55f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:34:32 2009 +0200 Fixed operator>>(std::istream&, Interval<Boundary, Info>&). --- src/Interval.templates.hh | 6 ++++-- 1 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Interval.templates.hh b/src/Interval.templates.hh index fcfecf6..f9d3f1e 100644 --- a/src/Interval.templates.hh +++ b/src/Interval.templates.hh @@ -234,8 +234,9 @@ operator>>(std::istream& is, Interval<Boundary, Info>& x) { bool upper_boundary_infinity = false; switch (lower_r) { case V_EQ: + case V_GE: break; - case V_LE: + case V_GT: lower_open = true; break; case V_EQ_MINUS_INFINITY: @@ -254,8 +255,9 @@ operator>>(std::istream& is, Interval<Boundary, Info>& x) { } switch (upper_r) { case V_EQ: + case V_LE: break; - case V_GE: + case V_LT: upper_open = true; break; case V_EQ_MINUS_INFINITY:

1 0

[GIT] ppl/ppl(master): Spurious print statement removed.
by Roberto Bagnara 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: master Commit: ccd16569a7d2ce0f02f33c81d765970ebd4213dd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ccd16569a7d2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:32:31 2009 +0200 Spurious print statement removed. --- src/Interval.templates.hh | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/src/Interval.templates.hh b/src/Interval.templates.hh index 1e0b3f8..fcfecf6 100644 --- a/src/Interval.templates.hh +++ b/src/Interval.templates.hh @@ -115,7 +115,6 @@ Interval<Boundary, Info>::Interval(const char* s) { assign(EMPTY); break; default: - std::cerr << "lower_r = " << lower_r << std::endl; PPL_ASSERT(false); } switch (upper_r) {

1 0

[GIT] ppl/ppl(floating_point): Added the constructor Constant_Floating_Point_Expression(const char*).
by Fabio Bossi 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 334ff19fb5ca33f01673d30f970f64791bc61dd8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=334ff19fb5ca… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 24 16:32:57 2009 +0200 Added the constructor Constant_Floating_Point_Expression(const char*). --- src/Constant_Floating_Point_Expression.defs.hh | 6 ++++++ src/Constant_Floating_Point_Expression.inlines.hh | 6 ++++++ 2 files changed, 12 insertions(+), 0 deletions(-) diff --git a/src/Constant_Floating_Point_Expression.defs.hh b/src/Constant_Floating_Point_Expression.defs.hh index 1750a2b..5399523 100644 --- a/src/Constant_Floating_Point_Expression.defs.hh +++ b/src/Constant_Floating_Point_Expression.defs.hh @@ -116,6 +116,12 @@ public: Constant_Floating_Point_Expression(const boundary_type lower_bound, const boundary_type upper_bound); + /*! \brief + Builds a constant floating point expression with the value + expressed by the string \p str_value. + */ + Constant_Floating_Point_Expression(const char* str_value); + //! Destructor. ~Constant_Floating_Point_Expression(); diff --git a/src/Constant_Floating_Point_Expression.inlines.hh b/src/Constant_Floating_Point_Expression.inlines.hh index 0618cd4..1b2c577 100644 --- a/src/Constant_Floating_Point_Expression.inlines.hh +++ b/src/Constant_Floating_Point_Expression.inlines.hh @@ -30,6 +30,12 @@ namespace Parma_Polyhedra_Library { template <typename FP_Interval_Type, typename FP_Format> inline Constant_Floating_Point_Expression<FP_Interval_Type, FP_Format>:: +Constant_Floating_Point_Expression(const char* str_value) + : value(str_value) {} + +template <typename FP_Interval_Type, typename FP_Format> +inline +Constant_Floating_Point_Expression<FP_Interval_Type, FP_Format>:: Constant_Floating_Point_Expression(const boundary_type lb, const boundary_type ub) : value(lb) {

1 0

[GIT] ppl/ppl(floating_point): New commits
by Roberto Bagnara 24 Sep '09

24 Sep '09

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4ffa56a7f08a… Merge: d865b7a741bdb503fdac52edbd5b2a700593a850 e61defee29d0688a72fbe707157351a85c9a35a1 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:25:29 2009 +0200 Merge branch 'master' into floating_point URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e61defee29d0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:23:44 2009 +0200 New constructor explicit Interval::Interval(const char* s). URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0e677160d160… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Sep 18 20:24:35 2009 +0200 Make sure the latest changes to NDEBUG effective. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ba44339f4373… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Sep 17 16:12:17 2009 +0200 Fixed several rounding modes in Octagonal_Shape methods. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=255dd5501e74… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu Sep 17 15:49:53 2009 +0200 Fixed and simplified DIRTY_TEMP for use with -fno-elide-constructors. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cb4d41cada4e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Sep 14 21:21:25 2009 +0200 Added missing comment. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=04affbe1f914… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Sep 11 22:28:09 2009 +0200 Do not include <stdint.h>. The header files <stdint.h> and/or <inttypes.h> are included by ppl-config.h. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2e103e539bb6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Sep 11 22:27:40 2009 +0200 Make sure uintptr_t is defined, if at all possible. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6a1b3b278146… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Sep 10 15:24:16 2009 +0200 Suggest using -fno-elide-constructors when configuring for coverage. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d3dc3a4686aa… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Sep 4 17:00:16 2009 +0200 Corrected a couple of typos in documentation of Variables_Set. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6a96e8612725… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Aug 15 10:05:48 2009 +0200 Mention correction of bug in Pointset_Powerset maximize/minimize methods. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ba692c7b2002… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Aug 15 08:18:50 2009 +0200 Indentation fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b52a2d273f4f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Aug 15 08:15:14 2009 +0200 Corrected a bug in Pointset_Powerset methods minimize() and maximize(). We now return false if the powerset is found to be empty. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dfff7e13e881… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Aug 15 08:10:19 2009 +0200 Corrected a few expected results in Powerset/maxmin1.cc. This uncovered a bug in Pointset_Powerset methods maximize() and minimize(), whereby we are returning true even for empty powersets.

1 0

[GIT] ppl/ppl(master): New constructor explicit Interval::Interval( const char* s).
by Roberto Bagnara 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: master Commit: e61defee29d0688a72fbe707157351a85c9a35a1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e61defee29d0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Sep 24 16:23:44 2009 +0200 New constructor explicit Interval::Interval(const char* s). --- src/Interval.defs.hh | 12 ++++-- src/Interval.templates.hh | 94 +++++++++++++++++++++++++++++++++++++++++++- tests/Box/interval1.cc | 11 +++++ 3 files changed, 110 insertions(+), 7 deletions(-) diff --git a/src/Interval.defs.hh b/src/Interval.defs.hh index d39505a..4fe0463 100644 --- a/src/Interval.defs.hh +++ b/src/Interval.defs.hh @@ -664,16 +664,20 @@ public: return true; } - Interval() - { + Interval() { } template <typename T> - explicit Interval(const T& x) - { + explicit Interval(const T& x) { assign(x); } + /*! \brief + Builds the smallest interval containing the number whose textual + representation is contained in \p s. + */ + explicit Interval(const char* s); + template <typename T> typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, bool>::type diff --git a/src/Interval.templates.hh b/src/Interval.templates.hh index ec5cfcf..1e0b3f8 100644 --- a/src/Interval.templates.hh +++ b/src/Interval.templates.hh @@ -75,6 +75,92 @@ Interval<Boundary, Info>::CC76_widening_assign(const From& y, } template <typename Boundary, typename Info> +Interval<Boundary, Info>::Interval(const char* s) { + // Get the lower bound. + Boundary lower_bound; + Result lower_r = assign_r(lower_bound, s, ROUND_DOWN); + if (lower_r == V_CVT_STR_UNK || lower_r == V_NAN) { + throw std::invalid_argument("PPL::Interval(const char* s)" + " with s invalid"); + } + lower_r = result_relation_class(lower_r); + + // Get the upper bound. + Boundary upper_bound; + Result upper_r = assign_r(upper_bound, s, ROUND_UP); + assert(upper_r != V_CVT_STR_UNK && upper_r != V_NAN); + upper_r = result_relation_class(upper_r); + + // Buld the interval. + bool lower_open = false; + bool upper_open = false; + bool lower_boundary_infinity = false; + bool upper_boundary_infinity = false; + switch (lower_r) { + case V_EQ: + case V_GE: + break; + case V_GT: + lower_open = true; + break; + case V_EQ_MINUS_INFINITY: + case V_GT_MINUS_INFINITY: + lower_boundary_infinity = true; + break; + case V_EQ_PLUS_INFINITY: + case V_LT_PLUS_INFINITY: + if (upper_r == V_EQ_PLUS_INFINITY || upper_r == V_LT_PLUS_INFINITY) + assign(UNIVERSE); + else + assign(EMPTY); + break; + default: + std::cerr << "lower_r = " << lower_r << std::endl; + PPL_ASSERT(false); + } + switch (upper_r) { + case V_EQ: + case V_LE: + break; + case V_LT: + upper_open = true; + break; + case V_EQ_MINUS_INFINITY: + case V_GT_MINUS_INFINITY: + if (lower_r == V_EQ_MINUS_INFINITY || lower_r == V_GT_MINUS_INFINITY) + assign(UNIVERSE); + else + assign(EMPTY); + break; + case V_EQ_PLUS_INFINITY: + case V_LT_PLUS_INFINITY: + upper_boundary_infinity = true; + break; + default: + PPL_ASSERT(false); + } + + if (!lower_boundary_infinity + && !upper_boundary_infinity + && (lower_bound > upper_bound + || (lower_open && lower_bound == upper_bound))) + assign(EMPTY); + else { + if (lower_boundary_infinity) + special_set_boundary_infinity(LOWER, lower(), info()); + else + Boundary_NS::assign(LOWER, lower(), info(), + LOWER, lower_bound, SCALAR_INFO, lower_open); + if (upper_boundary_infinity) + special_set_boundary_infinity(UPPER, upper(), info()); + else + Boundary_NS::assign(UPPER, upper(), info(), + UPPER, upper_bound, SCALAR_INFO, upper_open); + } +} + + +template <typename Boundary, typename Info> inline std::istream& operator>>(std::istream& is, Interval<Boundary, Info>& x) { // Eat leading white space. @@ -105,7 +191,7 @@ operator>>(std::istream& is, Interval<Boundary, Info>& x) { // Get the lower bound. Boundary lower_bound; - Result lower_r = input(lower_bound, is, ROUND_DOWN); + Result lower_r = input(lower_bound, is, ROUND_DOWN); if (lower_r == V_CVT_STR_UNK || lower_r == V_NAN) { is.setstate(std::ios_base::failbit); return is; @@ -197,11 +283,13 @@ operator>>(std::istream& is, Interval<Boundary, Info>& x) { if (lower_boundary_infinity) special_set_boundary_infinity(LOWER, x.lower(), x.info()); else - assign(LOWER, x.lower(), x.info(), LOWER, lower_bound, SCALAR_INFO, lower_open); + assign(LOWER, x.lower(), x.info(), + LOWER, lower_bound, SCALAR_INFO, lower_open); if (upper_boundary_infinity) special_set_boundary_infinity(UPPER, x.upper(), x.info()); else - assign(UPPER, x.upper(), x.info(), UPPER, upper_bound, SCALAR_INFO, upper_open); + assign(UPPER, x.upper(), x.info(), + UPPER, upper_bound, SCALAR_INFO, upper_open); } return is; } diff --git a/tests/Box/interval1.cc b/tests/Box/interval1.cc index a4342bc..1dd786a 100644 --- a/tests/Box/interval1.cc +++ b/tests/Box/interval1.cc @@ -178,6 +178,14 @@ bool test04() { return true; } +template<typename F> +bool +test05() { + typename My_Interval<F>::interval_type x("123.00123"); + nout << "x = " << x << endl; + return true; +} + } // namespace BEGIN_MAIN @@ -187,6 +195,7 @@ BEGIN_MAIN DO_TEST(test02<float>); DO_TEST(test03<float>); DO_TEST(test04<float>); + DO_TEST(test05<float>); #endif // PPL_SUPPORTED_FLOAT #if PPL_SUPPORTED_DOUBLE @@ -194,6 +203,7 @@ BEGIN_MAIN DO_TEST(test02<double>); DO_TEST(test03<double>); DO_TEST(test04<double>); + DO_TEST(test05<double>); #endif // PPL_SUPPORTED_DOUBLE #if PPL_SUPPORTED_LONG_DOUBLE @@ -201,6 +211,7 @@ BEGIN_MAIN DO_TEST(test02<long double>); DO_TEST(test03<long double>); DO_TEST(test04<long double>); + DO_TEST(test05<long double>); #endif // PPL_SUPPORTED_LONG_DOUBLE END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added a couple of assertions.
by Fabio Bossi 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d865b7a741bdb503fdac52edbd5b2a700593a850 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d865b7a741bd… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 24 16:15:20 2009 +0200 Added a couple of assertions. --- src/Polyhedron.templates.hh | 2 ++ 1 files changed, 2 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 51af2b5..074e717 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -307,6 +307,7 @@ Polyhedron::refine_with_linear_form_inequality( "Polyhedron::refine_with_linear_form_inequality:" " FP_Format not a floating point type."); + PPL_ASSERT(space_dim <= store.space_dimension()); PPL_ASSERT(store.is_bounded()); // Dimension compatibility checks. // The dimensions of left and right should not be greater than the @@ -353,6 +354,7 @@ const Box< Interval<FP_Format, Interval_Info> >& store) { "Polyhedron::affine_image:" " FP_Format not a floating point type."); + PPL_ASSERT(space_dim <= store.space_dimension()); PPL_ASSERT(store.is_bounded()); // Dimension compatibility checks. // The dimension of lf should not be greater than the dimension of *this.

1 0

[GIT] ppl/ppl(floating_point): Added some tests in tests/ Floating_Point_Expression/polyhedron1.cc
by Roberto Amadini 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 360425ce18d40049ad6a3bcc581b1f551eb1fdac URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=360425ce18d4… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Thu Sep 24 16:12:32 2009 +0200 Added some tests in tests/Floating_Point_Expression/polyhedron1.cc --- tests/Floating_Point_Expression/polyhedron1.cc | 287 ++++++++++++++++++++++++ 1 files changed, 287 insertions(+), 0 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron1.cc b/tests/Floating_Point_Expression/polyhedron1.cc new file mode 100644 index 0000000..601c82b --- /dev/null +++ b/tests/Floating_Point_Expression/polyhedron1.cc @@ -0,0 +1,287 @@ +/* Test Polyhedron::affine_image() on interval linear forms. + 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_test.hh" + +namespace { + +// tests ph.affine_image(B, 3, store) +bool +test01() { + Variable A(0); + Variable B(1); + Variable C(2); + FP_Interval_Abstract_Store store(3); + FP_Interval tmp(0); + store.set_interval(B, tmp); + tmp.lower() = -2; + tmp.upper() = 2; + store.set_interval(A, tmp); + tmp.lower() = -1; + tmp.upper() = 1; + store.set_interval(C, tmp); + C_Polyhedron ph(3); + ph.add_constraint(C == 0); + ph.add_constraint(A == -2); + tmp = 3; + FP_Linear_Form l(tmp); + + ph.affine_image(B, l, store); + print_constraints(ph, "*** ph.affine_image(B, 3, store) ***"); + + C_Polyhedron known_result(3, EMPTY); + known_result.add_generator(point(-2 * A + 3 * B)); + print_constraints(known_result, "*** know_result ***"); + + bool ok = (ph == known_result); + return ok; +} + +// tests ph.affine_image(A, A + B + 1, store) +bool +test02() { + Variable A(0); + Variable B(1); + FP_Interval_Abstract_Store store(2); + FP_Interval tmp(1); + store.set_interval(A, tmp); + store.set_interval(B, tmp); + C_Polyhedron ph(2); + ph.add_constraint(A >= B); + ph.add_constraint(B >= 0); + ph.add_constraint(A <= 3); + FP_Linear_Form l(A); + l += B; + l += tmp; + ph.affine_image(A, l, store); + print_constraints(ph, "*** ph.affine_image(A, A + B + 1, store) ***"); + + C_Polyhedron known_result(2); + known_result.add_constraint(A - 2*B - 1 >= 0); + known_result.add_constraint(B >= 0); + known_result.add_constraint(A - B <= 4); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (ph == known_result); + + return ok; +} + +// tests ph.affine_image(A, (A + 1) / 2, store) +bool +test03() { + Variable A(0); + Variable B(1); + FP_Interval_Abstract_Store store(2); + FP_Interval tmp(1 / 2.0); + store.set_interval(A, tmp); + store.set_interval(B, tmp); + Generator_System gs; + gs.insert(point()); + gs.insert(ray(A)); + gs.insert(ray(B)); + C_Polyhedron ph(gs); + FP_Linear_Form l(A); + l *= tmp; + l += tmp; + ph.affine_image(A, l, store); + print_constraints(ph, "*** ph.affine_image(A, (A + 1) / 2, store) ***"); + + C_Polyhedron known_result(2); + known_result.add_constraint(2*A >= 1); + known_result.add_constraint(B >= 0); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (ph == known_result); + + return ok; +} + +// tests ph.affine_image(A, (B + 2) / (-3), store) +// FIXME: not passes at the moment. +bool +test04() { + Variable A(0); + Variable B(1); + FP_Interval_Abstract_Store store(2); + FP_Interval tmp(-1 / 3.0); + store.set_interval(A, tmp); + store.set_interval(B, tmp); + C_Polyhedron ph(2, EMPTY); + ph.add_generator(point(A)); + FP_Linear_Form l(B); + l *= tmp; + tmp += tmp; + l += tmp; + ph.affine_image(A, l, store); + print_constraints(ph, "*** ph.affine_image(A, (B + 2) / (-3), store) ***"); + + C_Polyhedron known_result(2, EMPTY); + known_result.add_generator(point(-2*A, 3)); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (ph == known_result); + + return ok; +} +/* +bool +test05() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.add_constraint(A >= 2); + ph.add_constraint(A <= 3); + ph.add_constraint(B >= 1); + ph.add_constraint(2*A >= B); + + print_constraints(ph, "*** ph ***"); + + ph.affine_image(B, A-B+2, -3); + + C_Polyhedron known_result(2, EMPTY); + known_result.add_generator(point(2*A)); + known_result.add_generator(point(2*A - B)); + known_result.add_generator(point(9*A + B, 3)); + known_result.add_generator(point(9*A - 4*B, 3)); + + bool ok = (ph == known_result); + + print_generators(ph, "*** ph after ph.affine_image(B, A-B+2, -3) ***"); + + return ok; +} + +bool +test06() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph1(2, EMPTY); + + print_constraints(ph1, "*** ph1 ***"); + + ph1.affine_image(A, 2*A + B + 1); + + C_Polyhedron known_result(2, EMPTY); + + bool ok = (ph1 == known_result); + + print_constraints(ph1, "*** after ph1.affine_image(A, 2*A + B + 1) ***"); + + return ok; +} + +bool +test07() { + Variable A(0); + Variable B(1); + + Generator_System gs; + gs.insert(point()); + gs.insert(point(A)); + gs.insert(point(B)); + gs.insert(point(A + B)); + C_Polyhedron ph(gs); + + print_generators(ph, "*** ph ***"); + + ph.affine_image(A, -A - 1, -1); + + Generator_System known_gs; + known_gs.insert(point(A)); + known_gs.insert(point(2*A)); + known_gs.insert(point(A + B)); + known_gs.insert(point(2*A + B)); + C_Polyhedron known_result(known_gs); + + bool ok = (ph == known_result); + + print_generators(ph, "*** after ph.affine_image(A, -A - 1, -1) ***"); + + return ok; +} + +bool +test08() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.generators(); + ph.add_constraint(A >= 0); + ph.add_constraint(B >= 0); + C_Polyhedron copy_ph(ph); + + print_constraints(ph, "*** ph ***"); + + ph.affine_image(A, A + 1); + copy_ph.affine_image(A, -A - 1, -1); + + bool ok = (ph == copy_ph); + + print_generators(ph, "*** after ph.affine_image(A, A + 1) ***"); + print_generators(copy_ph, + "*** after copy_ph.affine_image(A, -A - 1, -1) ***"); + + return ok; +} + +bool +test09() { + Variable A(0); + Variable B(1); + + C_Polyhedron ph(2); + ph.generators(); + ph.add_constraint(A >= 0); + ph.add_constraint(B >= 0); + C_Polyhedron copy_ph(ph); + + print_constraints(ph, "*** ph ***"); + + ph.affine_image(B, A + 1); + copy_ph.affine_image(B, -A - 1, -1); + + bool ok = (ph == copy_ph); + + print_generators(ph, "*** after ph.affine_image(B, A + 1) ***"); + print_generators(copy_ph, + "*** after copy_ph.affine_image(B, -A - 1, -1) ***"); + + return ok; +} +*/ +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); /* + DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); + DO_TEST(test07); + DO_TEST(test08); + DO_TEST(test09); */ +END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Forgot to pass the common denominator to bounded_affine_image.
by Fabio Bossi 24 Sep '09

24 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 07bb498a1557b74ad57697c0ed0d20a7b2fafadf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=07bb498a1557… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Sep 24 14:44:33 2009 +0200 Forgot to pass the common denominator to bounded_affine_image. --- src/Polyhedron.defs.hh | 9 +++++++-- src/Polyhedron.templates.hh | 10 ++++++---- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 41c8ae6..74eeb78 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2682,7 +2682,7 @@ protected: Used to store the result. This function ignores the upper bound of intervals in \p lf, - so that in fact the result can be seen as \p lf multiplied by a proper + so that in fact \p result can be seen as \p lf multiplied by a proper normalization constant. */ template <typename FP_Format, typename Interval_Info> @@ -2710,6 +2710,10 @@ protected: \param res_hi_coeff Stores the higher boundary of the inhomogeneous term of the result. + \param denominator + Becomes the common denominator of \p res_low_coeff, \p res_hi_coeff + and all coefficients in \p res. + Results are obtained by normalizing denominators in \p lf, ignoring the upper bounds of variable coefficients in \p lf. */ @@ -2717,7 +2721,8 @@ protected: static void convert_to_integer_expressions( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Expression& res, - Coefficient& res_low_coeff, Coefficient& res_hi_coeff); + Coefficient& res_low_coeff, Coefficient& res_hi_coeff, + Coefficient& denominator); }; diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 491bb20..51af2b5 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -379,11 +379,13 @@ const Box< Interval<FP_Format, Interval_Info> >& store) { Linear_Expression lf_approx_le; PPL_DIRTY_TEMP_COEFFICIENT(lo_coeff); PPL_DIRTY_TEMP_COEFFICIENT(hi_coeff); + PPL_DIRTY_TEMP_COEFFICIENT(denominator); convert_to_integer_expressions(lf_approx, lf_space_dim, lf_approx_le, - lo_coeff, hi_coeff); + lo_coeff, hi_coeff, denominator); // Finally, do the assignment. - bounded_affine_image(var, lf_approx_le + lo_coeff, lf_approx_le + hi_coeff); + bounded_affine_image(var, lf_approx_le + lo_coeff, lf_approx_le + hi_coeff, + denominator); } template <typename FP_Format, typename Interval_Info> @@ -482,7 +484,8 @@ void Polyhedron::convert_to_integer_expressions( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, const dimension_type lf_dimension, Linear_Expression& res, - Coefficient& res_low_coeff, Coefficient& res_hi_coeff) { + Coefficient& res_low_coeff, Coefficient& res_hi_coeff, + Coefficient& lcm) { res = Linear_Expression(); typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; @@ -491,7 +494,6 @@ Polyhedron::convert_to_integer_expressions( // Convert each floating point number to a pair <numerator, denominator> // and compute the lcm of all denominators. - PPL_DIRTY_TEMP_COEFFICIENT(lcm); lcm = 1; const FP_Interval_Type& b = lf.inhomogeneous_term(); numer_denom(b.lower(), numerators[lf_dimension], denominators[lf_dimension]);

1 0