February 2012 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Prefer testing against zero.
by Enea Zaffanella 15 Feb '12

15 Feb '12

Module: ppl/ppl Branch: master Commit: 0691decf11e6f384b602d762c3060af30bf43a50 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0691decf11e6… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 15 15:21:01 2012 +0100 Prefer testing against zero. --- src/checked_float.inlines.hh | 8 ++++---- 1 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index ffb5bd0..6c2b97a 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -190,14 +190,14 @@ template <typename Policy, typename T> inline bool is_minf_float(const T v) { Float<T> f(v); - return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() == -1)); + return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() < 0)); } template <typename Policy, typename T> inline bool is_pinf_float(const T v) { Float<T> f(v); - return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() == 1)); + return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() > 0)); } @@ -233,7 +233,7 @@ pred_float(T& v) { Float<T> f(v); PPL_ASSERT(!f.u.binary.is_nan()); PPL_ASSERT(f.u.binary.inf_sign() >= 0); - if (f.u.binary.zero_sign() == 1) { + if (f.u.binary.zero_sign() > 0) { f.u.binary.negate(); f.u.binary.inc(); } @@ -252,7 +252,7 @@ succ_float(T& v) { Float<T> f(v); PPL_ASSERT(!f.u.binary.is_nan()); PPL_ASSERT(f.u.binary.inf_sign() <= 0); - if (f.u.binary.zero_sign() == -1) { + if (f.u.binary.zero_sign() < 0) { f.u.binary.negate(); f.u.binary.inc(); }

1 0

[GIT] ppl/ppl(master): For clarity, renamed three-state Float method is_inf () as inf_sign().
by Enea Zaffanella 15 Feb '12

15 Feb '12

Module: ppl/ppl Branch: master Commit: 2bcc4ac88501983c95dc035d8fc7ff5dbbf76975 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2bcc4ac88501… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 15 14:39:43 2012 +0100 For clarity, renamed three-state Float method is_inf() as inf_sign(). Similarly, renamed is_zero() as zero_sign(). --- src/Float.defs.hh | 24 ++++++++++++------------ src/Float.inlines.hh | 24 ++++++++++++------------ src/checked_float.inlines.hh | 28 ++++++++++++++++------------ 3 files changed, 40 insertions(+), 36 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 81e3799..597b2dc 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -65,9 +65,9 @@ struct float_ieee754_half { static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); static const Floating_Point_Format floating_point_format = IEEE754_HALF; - int is_inf() const; + int inf_sign() const; bool is_nan() const; - int is_zero() const; + int zero_sign() const; bool sign_bit() const; void negate(); void dec(); @@ -98,9 +98,9 @@ struct float_ieee754_single { static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); static const Floating_Point_Format floating_point_format = IEEE754_SINGLE; - int is_inf() const; + int inf_sign() const; bool is_nan() const; - int is_zero() const; + int zero_sign() const; bool sign_bit() const; void negate(); void dec(); @@ -144,9 +144,9 @@ struct float_ieee754_double { static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); static const Floating_Point_Format floating_point_format = IEEE754_DOUBLE; - int is_inf() const; + int inf_sign() const; bool is_nan() const; - int is_zero() const; + int zero_sign() const; bool sign_bit() const; void negate(); void dec(); @@ -176,9 +176,9 @@ struct float_ibm_single { static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); static const Floating_Point_Format floating_point_format = IBM_SINGLE; - int is_inf() const; + int inf_sign() const; bool is_nan() const; - int is_zero() const; + int zero_sign() const; bool sign_bit() const; void negate(); void dec(); @@ -229,9 +229,9 @@ struct float_intel_double_extended { - static_cast<int>(MANTISSA_BITS); static const Floating_Point_Format floating_point_format = INTEL_DOUBLE_EXTENDED; - int is_inf() const; + int inf_sign() const; bool is_nan() const; - int is_zero() const; + int zero_sign() const; bool sign_bit() const; void negate(); void dec(); @@ -268,9 +268,9 @@ struct float_ieee754_quad { static const int EXPONENT_MIN = -EXPONENT_MAX + 1; static const int EXPONENT_MIN_DENORM = EXPONENT_MIN - static_cast<int>(MANTISSA_BITS); - int is_inf() const; + int inf_sign() const; bool is_nan() const; - int is_zero() const; + int zero_sign() const; bool sign_bit() const; void negate(); void dec(); diff --git a/src/Float.inlines.hh b/src/Float.inlines.hh index c9b0108..88bb1a1 100644 --- a/src/Float.inlines.hh +++ b/src/Float.inlines.hh @@ -31,7 +31,7 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { inline int -float_ieee754_half::is_inf() const { +float_ieee754_half::inf_sign() const { if (word == NEG_INF) return -1; if (word == POS_INF) @@ -45,7 +45,7 @@ float_ieee754_half::is_nan() const { } inline int -float_ieee754_half::is_zero() const { +float_ieee754_half::zero_sign() const { if (word == NEG_ZERO) return -1; if (word == POS_ZERO) @@ -92,7 +92,7 @@ float_ieee754_half::build(bool negative, mpz_t mantissa, int exponent) { } inline int -float_ieee754_single::is_inf() const { +float_ieee754_single::inf_sign() const { if (word == NEG_INF) return -1; if (word == POS_INF) @@ -106,7 +106,7 @@ float_ieee754_single::is_nan() const { } inline int -float_ieee754_single::is_zero() const { +float_ieee754_single::zero_sign() const { if (word == NEG_ZERO) return -1; if (word == POS_ZERO) @@ -153,7 +153,7 @@ float_ieee754_single::build(bool negative, mpz_t mantissa, int exponent) { } inline int -float_ieee754_double::is_inf() const { +float_ieee754_double::inf_sign() const { if (lsp != LSP_INF) return 0; if (msp == MSP_NEG_INF) @@ -170,7 +170,7 @@ float_ieee754_double::is_nan() const { } inline int -float_ieee754_double::is_zero() const { +float_ieee754_double::zero_sign() const { if (lsp != LSP_ZERO) return 0; if (msp == MSP_NEG_ZERO) @@ -239,7 +239,7 @@ float_ieee754_double::build(bool negative, mpz_t mantissa, int exponent) { } inline int -float_ibm_single::is_inf() const { +float_ibm_single::inf_sign() const { if (word == NEG_INF) return -1; if (word == POS_INF) @@ -253,7 +253,7 @@ float_ibm_single::is_nan() const { } inline int -float_ibm_single::is_zero() const { +float_ibm_single::zero_sign() const { if (word == NEG_ZERO) return -1; if (word == POS_ZERO) @@ -300,7 +300,7 @@ float_ibm_single::build(bool negative, mpz_t mantissa, int exponent) { } inline int -float_intel_double_extended::is_inf() const { +float_intel_double_extended::inf_sign() const { if (lsp != LSP_INF) return 0; uint32_t a = msp & MSP_NEG_INF; @@ -318,7 +318,7 @@ float_intel_double_extended::is_nan() const { } inline int -float_intel_double_extended::is_zero() const { +float_intel_double_extended::zero_sign() const { if (lsp != LSP_ZERO) return 0; uint32_t a = msp & MSP_NEG_INF; @@ -382,7 +382,7 @@ float_intel_double_extended::build(bool negative, } inline int -float_ieee754_quad::is_inf() const { +float_ieee754_quad::inf_sign() const { if (lsp != LSP_INF) return 0; if (msp == MSP_NEG_INF) @@ -399,7 +399,7 @@ float_ieee754_quad::is_nan() const { } inline int -float_ieee754_quad::is_zero() const { +float_ieee754_quad::zero_sign() const { if (lsp != LSP_ZERO) return 0; if (msp == MSP_NEG_ZERO) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 16fff99..ffb5bd0 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -153,11 +153,15 @@ classify_float(const T v, bool nan, bool inf, bool sign) { if ((nan || sign) && CHECK_P(Policy::has_nan, f.u.binary.is_nan())) return V_NAN; if (inf) { - int i = CHECK_P(Policy::has_infinity, f.u.binary.is_inf()); - if (i < 0) - return V_EQ_MINUS_INFINITY; - if (i > 0) - return V_EQ_PLUS_INFINITY; + if (Policy::has_infinity) { + int sign = f.u.binary.inf_sign(); + if (sign < 0) + return V_EQ_MINUS_INFINITY; + if (sign > 0) + return V_EQ_PLUS_INFINITY; + } + else + PPL_ASSERT(f.u.binary.inf_sign() == 0); } if (sign) { if (v < 0) @@ -180,20 +184,20 @@ template <typename Policy, typename T> inline bool is_inf_float(const T v) { Float<T> f(v); - return CHECK_P(Policy::has_infinity, (f.u.binary.is_inf() != 0)); + return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() != 0)); } template <typename Policy, typename T> inline bool is_minf_float(const T v) { Float<T> f(v); - return CHECK_P(Policy::has_infinity, (f.u.binary.is_inf() < 0)); + return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() == -1)); } template <typename Policy, typename T> inline bool is_pinf_float(const T v) { Float<T> f(v); - return CHECK_P(Policy::has_infinity, (f.u.binary.is_inf() > 0)); + return CHECK_P(Policy::has_infinity, (f.u.binary.inf_sign() == 1)); } @@ -228,8 +232,8 @@ inline void pred_float(T& v) { Float<T> f(v); PPL_ASSERT(!f.u.binary.is_nan()); - PPL_ASSERT(f.u.binary.is_inf() >= 0); - if (f.u.binary.is_zero() > 0) { + PPL_ASSERT(f.u.binary.inf_sign() >= 0); + if (f.u.binary.zero_sign() == 1) { f.u.binary.negate(); f.u.binary.inc(); } @@ -247,8 +251,8 @@ inline void succ_float(T& v) { Float<T> f(v); PPL_ASSERT(!f.u.binary.is_nan()); - PPL_ASSERT(f.u.binary.is_inf() <= 0); - if (f.u.binary.is_zero() < 0) { + PPL_ASSERT(f.u.binary.inf_sign() <= 0); + if (f.u.binary.zero_sign() == -1) { f.u.binary.negate(); f.u.binary.inc(); }

1 0

[GIT] ppl/ppl(master): Avoid long lines and try to improve readability.
by Enea Zaffanella 15 Feb '12

15 Feb '12

Module: ppl/ppl Branch: master Commit: 90cb4b9b18069d2fb809704fcc0edce6bef20834 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90cb4b9b1806… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 15 13:09:49 2012 +0100 Avoid long lines and try to improve readability. In particular, when using helper function i_constraint(), prefer passing in an already built Relation_Symbol object if its computation is nontrivial. --- src/Box.inlines.hh | 16 ++--- src/Box.templates.hh | 147 ++++++++++++++++++++++++++++-------------------- src/Interval.defs.hh | 6 +- src/intervals.defs.hh | 3 +- 4 files changed, 98 insertions(+), 74 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=90cb4b9b…

1 0

[GIT] ppl/ppl(master): Completed previous commit, fixing is_{m, p}inf_float.
by Enea Zaffanella 15 Feb '12

15 Feb '12

Module: ppl/ppl Branch: master Commit: 912481ec1055d52b37ee8a64e97ad3be70cd1a7b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=912481ec1055… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 15 12:34:32 2012 +0100 Completed previous commit, fixing is_{m,p}inf_float. --- src/checked_float.inlines.hh | 8 +++++--- 1 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 7c06757..16fff99 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -180,18 +180,20 @@ template <typename Policy, typename T> inline bool is_inf_float(const T v) { Float<T> f(v); - return CHECK_P(Policy::has_infinity, f.u.binary.is_inf()); + return CHECK_P(Policy::has_infinity, (f.u.binary.is_inf() != 0)); } template <typename Policy, typename T> inline bool is_minf_float(const T v) { - return is_inf_float<Policy>(v) < 0; + Float<T> f(v); + return CHECK_P(Policy::has_infinity, (f.u.binary.is_inf() < 0)); } template <typename Policy, typename T> inline bool is_pinf_float(const T v) { - return is_inf_float<Policy>(v) > 0; + Float<T> f(v); + return CHECK_P(Policy::has_infinity, (f.u.binary.is_inf() > 0)); }

1 0

[GIT] ppl/ppl(master): Let is_inf_float() return a Boolean value, rather than an integer.
by Enea Zaffanella 15 Feb '12

15 Feb '12

Module: ppl/ppl Branch: master Commit: 2e81747bef37b0c49447ca598e75312691526bf8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2e81747bef37… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 15 08:26:47 2012 +0100 Let is_inf_float() return a Boolean value, rather than an integer. Detected by ECLAIR service utypflag. --- src/checked_float.inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 77c3f13..7c06757 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -177,7 +177,7 @@ is_nan_float(const T v) { } template <typename Policy, typename T> -inline int +inline bool is_inf_float(const T v) { Float<T> f(v); return CHECK_P(Policy::has_infinity, f.u.binary.is_inf());

1 0

[GIT] ppl/ppl(master): Prefer using logical (wrt bitwise) operators on Boolean values.
by Enea Zaffanella 15 Feb '12

15 Feb '12

Module: ppl/ppl Branch: master Commit: 68cc056b563b384a43a45278fb30c97907901240 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=68cc056b563b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Feb 15 08:25:15 2012 +0100 Prefer using logical (wrt bitwise) operators on Boolean values. Detected by ECLAIR service utypflag. --- src/Box.templates.hh | 4 ++-- src/Pointset_Powerset.templates.hh | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 13e51f5..1e59a3d 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -3125,7 +3125,7 @@ Box<ITV> assign_r(q.get_num(), numer_lower, ROUND_NOT_NEEDED); assign_r(q.get_den(), denom_lower, ROUND_NOT_NEEDED); q.canonicalize(); - open_lower |= !included; + open_lower = (open_lower || !included); if ((ub_var_coeff >= 0) ? !negative_denom : negative_denom) seq_var.add_constraint(i_constraint(open_lower ? GREATER_THAN : GREATER_OR_EQUAL, q)); else @@ -3158,7 +3158,7 @@ Box<ITV> assign_r(q.get_num(), numer_upper, ROUND_NOT_NEEDED); assign_r(q.get_den(), denom_upper, ROUND_NOT_NEEDED); q.canonicalize(); - open_upper |= !included; + open_upper = (open_upper || !included); if ((lb_var_coeff >= 0) ? !negative_denom : negative_denom) seq_var.add_constraint(i_constraint(open_upper ? LESS_THAN : LESS_OR_EQUAL, q)); else diff --git a/src/Pointset_Powerset.templates.hh b/src/Pointset_Powerset.templates.hh index f1b1ade..76c1b9b 100644 --- a/src/Pointset_Powerset.templates.hh +++ b/src/Pointset_Powerset.templates.hh @@ -674,8 +674,8 @@ Pointset_Powerset<PSET> PSET context_i(si->pointset()); context_i.intersection_assign(enlarged); PSET enlarged_i(dest); - nonempty_intersection - |= enlarged_i.simplify_using_context_assign(context_i); + if (enlarged_i.simplify_using_context_assign(context_i)) + nonempty_intersection = true; // TODO: merge the sorted constraints of `enlarged' and `enlarged_i'? enlarged.intersection_assign(enlarged_i); }

1 0

a bug in PPL Java bindings
by Gianluca Amato 14 Feb '12

14 Feb '12

Hi, I'm here again with another problem concerning boxes and Java bindings. I found by chance a sequence of operations which gives a wrong result. It is difficult to describe what happens, therefore I prepared a small Java program exhibiting the bad behavior. The program should print A in 0, B in 1 A in 0, B in 1 A in 0, B in 4 false A in 0, B in 4 but it prints: A in 0, B in 1 A in 0, B in 1 A in 0, B in 4 false A in 0, B in [1, 4] Cheers, --gianluca

3 2

[GIT] ppl/ppl(master): Fixed a bug in Box<ITV>::upper_bound_assign( _if_exact).
by Enea Zaffanella 14 Feb '12

14 Feb '12

Module: ppl/ppl Branch: master Commit: 50bf9eb645f7db8db9157788112b41d88cf18f08 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=50bf9eb645f7… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Feb 14 11:53:23 2012 +0100 Fixed a bug in Box<ITV>::upper_bound_assign(_if_exact). Calling the method with an empty argument that, due to computational laziness, is not yet flagged as being empty was producing wrong results. (Note: here `wrong' means unnecessarily imprecise; from the point of view of approximation, the results were still correct). See test08 in tests/Box/upperbound1.cc. --- src/Box.templates.hh | 8 ++++---- 1 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 341c111..13e51f5 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1205,9 +1205,9 @@ Box<ITV>::upper_bound_assign_if_exact(const Box& y) { x.throw_dimension_incompatible("upper_bound_assign_if_exact(y)", y); // The lub of a box with an empty box is equal to the first box. - if (y.marked_empty()) + if (y.is_empty()) return true; - if (x.marked_empty()) { + if (x.is_empty()) { x = y; return true; } @@ -1753,9 +1753,9 @@ Box<ITV>::upper_bound_assign(const Box& y) { x.throw_dimension_incompatible("upper_bound_assign(y)", y); // The lub of a box with an empty box is equal to the first box. - if (y.marked_empty()) + if (y.is_empty()) return; - if (x.marked_empty()) { + if (x.is_empty()) { x = y; return; }

1 0

[GIT] ppl/ppl(master): Restored a few tests commented out long time ago.
by Enea Zaffanella 14 Feb '12

14 Feb '12

Module: ppl/ppl Branch: master Commit: 2fcad61ebee93894f4c465da36f49db9a32d921e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fcad61ebee9… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Feb 14 11:51:11 2012 +0100 Restored a few tests commented out long time ago. Added a new test (synthesized from a Java test provided by Gianluca Amato) showing a problem in the implementation of Box<ITV>::upper_bound_assign(). --- tests/Box/upperbound1.cc | 92 +++++++++++++++++++--------------------------- 1 files changed, 38 insertions(+), 54 deletions(-) diff --git a/tests/Box/upperbound1.cc b/tests/Box/upperbound1.cc index 464436f..d011423 100644 --- a/tests/Box/upperbound1.cc +++ b/tests/Box/upperbound1.cc @@ -35,13 +35,10 @@ test01() { TBox box1(5); box1.add_constraint(x1 <= 5); box1.add_constraint(x2 <= -1); - box1.add_constraint(x1 -x2 <= 10); TBox box2(5); - box2.add_constraint(x1 <= 2); + box2.add_constraint(x1 <= 2); box2.add_constraint(x4 <= 7); - box2.add_constraint(x1 - x2 <= 20); - box2.add_constraint(x4 - x3 <= 3); print_constraints(box1, "*** box1 ***"); print_constraints(box2, "*** box2 ***"); @@ -50,7 +47,6 @@ test01() { Rational_Box known_result(5); known_result.add_constraint(x1 <= 5); - known_result.add_constraint(x1 - x2 <= 20); bool ok = check_result(box1, known_result); @@ -69,10 +65,8 @@ test02() { box1.add_constraint(-x <= -1); box1.add_constraint(y <= 3); box1.add_constraint(-y <= -1); - box1.add_constraint(x - y <= 1); TBox box2(3); - box2.add_constraint(y - x <= -1); box2.add_constraint(x <= 3); box2.add_constraint(-y <= 5); @@ -84,10 +78,6 @@ test02() { Rational_Box known_result(3); known_result.add_constraint(x <= 4); known_result.add_constraint(y >= -5); - known_result.add_constraint(x >= -4); - known_result.add_constraint(y <= 3); - known_result.add_constraint(x - y <= 8); - known_result.add_constraint(y - x <= 2); bool ok = check_result(box1, known_result); @@ -106,10 +96,8 @@ test03() { box1.add_constraint(-x <= -1); box1.add_constraint(y <= 3); box1.add_constraint(-y <= -1); - box1.add_constraint(x - y <= 1); TBox box2(2); - box2.add_constraint(y - x <= -1); box2.add_constraint(x <= 3); box2.add_constraint(x >= 5); @@ -137,12 +125,11 @@ test04() { box1.add_constraint(A >= 1); box1.add_constraint(B <= 3); box1.add_constraint(-B <= -1); - box1.add_constraint(A - B <= 1); TBox box2(2); - box2.add_constraint(B - A <= -1); - box2.add_constraint(A <= 3); + box2.add_constraint(A <= 8); box2.add_constraint(-B <= 5); + box2.add_constraint(B <= 0); print_constraints(box1, "*** box1 ***"); print_constraints(box2, "*** box2 ***"); @@ -150,12 +137,9 @@ test04() { box1.upper_bound_assign(box2); Rational_Box known_result(2); - known_result.add_constraint(A <= 4); + known_result.add_constraint(A <= 8); known_result.add_constraint(B >= -5); - known_result.add_constraint(A >= -4); known_result.add_constraint(B <= 3); - known_result.add_constraint(A - B <= 8); - known_result.add_constraint(B - A <= 2); bool ok = check_result(box1, known_result); @@ -186,31 +170,6 @@ test05() { bool test06() { - Variable x(0); - Variable y(1); - - TBox box1(2); - box1.add_constraint(x >= y); - - TBox box2(3); - - try { - // This is an invalid use of method - // Box::upper_bound_assign(box2): it is illegal - // to apply the method to two polyhedra of different dimensions. - box1.upper_bound_assign(box2); - } - catch (std::invalid_argument& e) { - nout << "std::invalid_argument: " << endl; - return true; - } - catch (...) { - } - return false; -} - -bool -test07() { Variable A(0); TBox box1(1); @@ -236,7 +195,7 @@ test07() { } bool -test08() { +test07() { Variable x1(0); TBox box1(1); @@ -252,16 +211,41 @@ test08() { return true; } +bool +test08() { + Variable A(0); + Variable B(1); + + TBox box1(2, UNIVERSE); + box1.add_constraint(A == 0); + box1.add_constraint(B == 1); + + TBox box2(box1); + box1.affine_image(B, Linear_Expression(4)); + + box2.add_constraint(A > 1); + box1.upper_bound_assign(box2); + + TBox known_result(2, UNIVERSE); + known_result.add_constraint(A == 0); + known_result.add_constraint(B == 4); + + bool ok = check_result(box1, known_result); + + print_constraints(box1, "=== box1 ==="); + print_constraints(box2, "=== known_result ==="); + return ok; +} + } // namespace BEGIN_MAIN -// CHECKME: why test from 1 to 7 are commented out? -// DO_TEST(test01); -// DO_TEST(test02); -// DO_TEST(test03); -// DO_TEST(test04); -// DO_TEST(test05); -// DO_TEST(test06); -// DO_TEST(test07); + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); + DO_TEST(test06); + DO_TEST(test07); DO_TEST(test08); END_MAIN

1 0

narrowing and Java bindings
by Gianluca Amato 13 Feb '12

13 Feb '12

Hi all, I'm trying the Java bindings for PPL. It seems that some domains (namely boxes) miss the CC76_narrowing_assign method. Is it just an oversight, or there are more fundamental issues behind? Thanks, --gianluca

2 3