May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed a typo.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 01d418b281367a2a8cd71fb2fa35e12a719ba3d0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=01d418b28136… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:51:14 2009 +0200 Fixed a typo. --- 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 a245829..4dd7fda 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -290,7 +290,7 @@ template <typename Policy> inline Result result_relation(Rounding_Dir dir) { if (Policy::fpu_check_inexact && - !round_not_needed(dir) && round_strict_relation(dir)) + !round_not_needed(dir) && round_strict_relation(dir)) { switch (fpu_check_inexact()) { case 0: return V_EQ;

1 0

[GIT] ppl/ppl(master): Added an assert(false) for unreachable code.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 1734ba44f5b535206d0642daa5fef274eb7b19aa URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1734ba44f5b5… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:23:19 2009 +0200 Added an assert(false) for unreachable code. --- src/checked_int.inlines.hh | 2 ++ src/checked_mpz.inlines.hh | 2 ++ 2 files changed, 4 insertions(+), 0 deletions(-) diff --git a/src/checked_int.inlines.hh b/src/checked_int.inlines.hh index 8b9e75c..43557e5 100644 --- a/src/checked_int.inlines.hh +++ b/src/checked_int.inlines.hh @@ -515,6 +515,8 @@ assign_int_float(To& to, const From from, Rounding_Dir dir) { return round_lt_int<To_Policy>(to, dir); if (from > i_from) return round_gt_int<To_Policy>(to, dir); + assert(false); + return V_NAN; } PPL_SPECIALIZE_ASSIGN(assign_int_float, signed char, float) diff --git a/src/checked_mpz.inlines.hh b/src/checked_mpz.inlines.hh index 5ba5433..2272c57 100644 --- a/src/checked_mpz.inlines.hh +++ b/src/checked_mpz.inlines.hh @@ -280,6 +280,8 @@ assign_mpz_float(mpz_class& to, const From from, Rounding_Dir dir) { return round_lt_mpz<To_Policy>(to, dir); if (from > i_from) return round_gt_mpz<To_Policy>(to, dir); + assert(false); + return V_NAN; } PPL_SPECIALIZE_ASSIGN(assign_mpz_float, mpz_class, float)

1 0

[GIT] ppl/ppl(master): Avoid two warnings.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: dbac03988bc9b337213d671745f974c64ce58c72 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=dbac03988bc9… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:22:21 2009 +0200 Avoid two warnings. --- src/checked.inlines.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/checked.inlines.hh b/src/checked.inlines.hh index 6627ba7..34d7ce6 100644 --- a/src/checked.inlines.hh +++ b/src/checked.inlines.hh @@ -452,7 +452,7 @@ inline typename Enable_If<(!Safe_Int_Comparison<S, U>::value && C_Integer<U>::value && C_Integer<S>::is_signed), bool>::type lt(const S& x, const U& y) { - return x < 0 || x < y; + return x < 0 || static_cast<typename C_Integer<S>::other_type>(x) < y; } template <typename U, typename S> @@ -468,7 +468,7 @@ inline typename Enable_If<(!Safe_Int_Comparison<S, U>::value && C_Integer<U>::value && C_Integer<S>::is_signed), bool>::type le(const S& x, const U& y) { - return x < 0 || x <= y; + return x < 0 || static_cast<typename C_Integer<S>::other_type>(x) <= y; } template <typename U, typename S>

1 0

[GIT] ppl/ppl(master): Renamed and commented ROUND_STRICT_RELATION. Added some use of it. Added some optimizations when ROUND_NOT_NEEDED is specified.
by Abramo Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 3ec4eb24ac151c9904f29eeafd583741240650b6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ec4eb24ac15… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Fri May 15 16:15:47 2009 +0200 Renamed and commented ROUND_STRICT_RELATION. Added some use of it. Added some optimizations when ROUND_NOT_NEEDED is specified. --- src/Boundary.defs.hh | 2 +- src/Rounding_Dir.defs.hh | 10 +++++++--- src/Rounding_Dir.inlines.hh | 4 ++-- src/checked.inlines.hh | 2 +- src/checked_float.inlines.hh | 6 ++++-- src/checked_mpz.inlines.hh | 30 +++++++++++++++++++++++------- src/intervals.defs.hh | 8 ++++---- 7 files changed, 42 insertions(+), 20 deletions(-) diff --git a/src/Boundary.defs.hh b/src/Boundary.defs.hh index 6557099..93a113e 100644 --- a/src/Boundary.defs.hh +++ b/src/Boundary.defs.hh @@ -56,7 +56,7 @@ enum Boundary_Type { inline Rounding_Dir round_dir_check(Boundary_Type t, bool check = false) { if (check) - return static_cast<Rounding_Dir>(t | ROUND_FPU_CHECK_INEXACT); + return static_cast<Rounding_Dir>(t | ROUND_STRICT_RELATION); else return static_cast<Rounding_Dir>(t); } diff --git a/src/Rounding_Dir.defs.hh b/src/Rounding_Dir.defs.hh index 68cb245..540a29e 100644 --- a/src/Rounding_Dir.defs.hh +++ b/src/Rounding_Dir.defs.hh @@ -59,9 +59,13 @@ enum Rounding_Dir { ROUND_DIR_MASK = 7, - ROUND_FPU_CHECK_INEXACT = 8, + /*! \hideinitializer + The client code is willing to pay an extra price to know the exact + relation beetwen the exact result and the computed one. + */ + ROUND_STRICT_RELATION = 8, - ROUND_CHECK = ROUND_DIRECT | ROUND_FPU_CHECK_INEXACT + ROUND_CHECK = ROUND_DIRECT | ROUND_STRICT_RELATION }; /*! \brief @@ -79,7 +83,7 @@ bool round_not_requested(Rounding_Dir dir); bool round_direct(Rounding_Dir dir); bool round_inverse(Rounding_Dir dir); -bool round_fpu_check_inexact(Rounding_Dir dir); +bool round_strict_relation(Rounding_Dir dir); fpu_rounding_direction_type round_fpu_dir(Rounding_Dir dir); diff --git a/src/Rounding_Dir.inlines.hh b/src/Rounding_Dir.inlines.hh index 686f674..45546ae 100644 --- a/src/Rounding_Dir.inlines.hh +++ b/src/Rounding_Dir.inlines.hh @@ -68,8 +68,8 @@ round_inverse(Rounding_Dir dir) { } inline bool -round_fpu_check_inexact(Rounding_Dir dir) { - return dir & ROUND_FPU_CHECK_INEXACT; +round_strict_relation(Rounding_Dir dir) { + return dir & ROUND_STRICT_RELATION; } #if PPL_CAN_CONTROL_FPU diff --git a/src/checked.inlines.hh b/src/checked.inlines.hh index 7e2e664..6627ba7 100644 --- a/src/checked.inlines.hh +++ b/src/checked.inlines.hh @@ -539,7 +539,7 @@ le(const T1& x, const T2& y) { Result r = assign_r(tmp, y, - static_cast<Rounding_Dir>(ROUND_UP | ROUND_FPU_CHECK_INEXACT)); + static_cast<Rounding_Dir>(ROUND_UP | ROUND_STRICT_RELATION)); if (!result_representable(r)) return true; switch (result_relation(r)) { diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index f7dc1c2..a245829 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -281,14 +281,16 @@ round_gt_float(To& to, Rounding_Dir dir) { template <typename Policy> inline void prepare_inexact(Rounding_Dir dir) { - if (Policy::fpu_check_inexact && round_fpu_check_inexact(dir)) + if (Policy::fpu_check_inexact && + !round_not_needed(dir) && round_strict_relation(dir)) fpu_reset_inexact(); } template <typename Policy> inline Result result_relation(Rounding_Dir dir) { - if (Policy::fpu_check_inexact && round_fpu_check_inexact(dir)) { + if (Policy::fpu_check_inexact && + !round_not_needed(dir) && round_strict_relation(dir)) switch (fpu_check_inexact()) { case 0: return V_EQ; diff --git a/src/checked_mpz.inlines.hh b/src/checked_mpz.inlines.hh index 765a848..5ba5433 100644 --- a/src/checked_mpz.inlines.hh +++ b/src/checked_mpz.inlines.hh @@ -311,7 +311,11 @@ PPL_SPECIALIZE_ASSIGN(assign_mpz_long_double, mpz_class, long double) template <typename To_Policy, typename From_Policy> inline Result assign_mpz_mpq(mpz_class& to, const mpq_class& from, Rounding_Dir dir) { - if (round_not_requested(dir)) { + if (round_not_needed(dir)) { + to = from.get_num(); + return V_LGE; + } + if (round_ignore(dir)) { to = from; return V_LGE; } @@ -319,12 +323,16 @@ assign_mpz_mpq(mpz_class& to, const mpq_class& from, Rounding_Dir dir) { mpz_srcptr d = from.get_den().get_mpz_t(); if (round_down(dir)) { mpz_fdiv_q(to.get_mpz_t(), n, d); - return mpz_divisible_p(n, d) ? V_EQ : V_GT; + if (round_strict_relation(dir)) + return mpz_divisible_p(n, d) ? V_EQ : V_GT; + return V_GE; } else { assert(round_up(dir)); mpz_cdiv_q(to.get_mpz_t(), n, d); - return mpz_divisible_p(n, d) ? V_EQ : V_LT; + if (round_strict_relation(dir)) + return mpz_divisible_p(n, d) ? V_EQ : V_LT; + return V_LE; } } @@ -389,12 +397,16 @@ div_mpz(mpz_class& to, const mpz_class& x, const mpz_class& y, } if (round_down(dir)) { mpz_fdiv_q(to.get_mpz_t(), n, d); - return mpz_divisible_p(n, d) ? V_EQ : V_GT; + if (round_strict_relation(dir)) + return mpz_divisible_p(n, d) ? V_EQ : V_GT; + return V_GE; } else { assert(round_up(dir)); mpz_cdiv_q(to.get_mpz_t(), n, d); - return mpz_divisible_p(n, d) ? V_EQ : V_LT; + if (round_strict_relation(dir)) + return mpz_divisible_p(n, d) ? V_EQ : V_LT; + return V_LE; } } @@ -474,12 +486,16 @@ div_2exp_mpz(mpz_class& to, const mpz_class& x, unsigned int exp, } if (round_down(dir)) { mpz_fdiv_q_2exp(to.get_mpz_t(), n, exp); - return mpz_divisible_2exp_p(n, exp) ? V_EQ : V_GT; + if (round_strict_relation(dir)) + return mpz_divisible_2exp_p(n, exp) ? V_EQ : V_GT; + return V_GE; } else { assert(round_up(dir)); mpz_cdiv_q_2exp(to.get_mpz_t(), n, exp); - return mpz_divisible_2exp_p(n, exp) ? V_EQ : V_LT; + if (round_strict_relation(dir)) + return mpz_divisible_2exp_p(n, exp) ? V_EQ : V_LT; + return V_LE; } } diff --git a/src/intervals.defs.hh b/src/intervals.defs.hh index 2cc2dfd..92be62f 100644 --- a/src/intervals.defs.hh +++ b/src/intervals.defs.hh @@ -172,7 +172,7 @@ public: case V_LGE: return r; case V_LE: - r = assign_r(to, c.value(), static_cast<Rounding_Dir>(ROUND_UP | ROUND_FPU_CHECK_INEXACT)); + r = assign_r(to, c.value(), static_cast<Rounding_Dir>(ROUND_UP | ROUND_STRICT_RELATION)); r = result_relation_class(r); if (r == V_EQ) return V_LE; @@ -195,7 +195,7 @@ public: } break; case V_GE: - r = assign_r(to, c.value(), static_cast<Rounding_Dir>(ROUND_DOWN | ROUND_FPU_CHECK_INEXACT)); + r = assign_r(to, c.value(), static_cast<Rounding_Dir>(ROUND_DOWN | ROUND_STRICT_RELATION)); r = result_relation_class(r); if (r == V_EQ) return V_GE; @@ -295,7 +295,7 @@ public: case V_LT: if (is_integer(to)) { rel = sub_assign_r(to, to, T(1), - static_cast<Rounding_Dir>(ROUND_UP | ROUND_FPU_CHECK_INEXACT)); + static_cast<Rounding_Dir>(ROUND_UP | ROUND_STRICT_RELATION)); rel = result_relation_class(rel); return rel == V_EQ ? V_LE : rel; } @@ -308,7 +308,7 @@ public: case V_GT: if (is_integer(to)) { rel = add_assign_r(to, to, T(1), - static_cast<Rounding_Dir>(ROUND_DOWN | ROUND_FPU_CHECK_INEXACT)); + static_cast<Rounding_Dir>(ROUND_DOWN | ROUND_STRICT_RELATION)); rel = result_relation_class(rel); return rel == V_EQ ? V_GE : rel; }

1 0

[GIT] ppl/ppl(master): Improved method Polyhedron::relation_with( const Congruence&) const.
by Enea Zaffanella 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: eca9369a8272645ba0db81f3244004691623bcba URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eca9369a8272… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 15:40:35 2009 +0200 Improved method Polyhedron::relation_with(const Congruence&) const. Avoided several temporary objects; added a FIXME asking for the rounding mode. --- src/Polyhedron_public.cc | 71 +++++++++++++++++++++------------------------ 1 files changed, 33 insertions(+), 38 deletions(-) diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index 1e8f2c5..a805773 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -303,69 +303,64 @@ PPL::Polyhedron::relation_with(const Congruence& cg) const { && Poly_Con_Relation::is_included() && Poly_Con_Relation::is_disjoint(); - // Find the equality corresponding to the congruence (ignoring the modulus). - Linear_Expression expr; - for (dimension_type i = cg_space_dim; i-- > 0; ) { - const Variable v(i); - expr += cg.coefficient(v) * v; - } - expr += cg.inhomogeneous_term(); + // Build the equality corresponding to the congruence (ignoring the modulus). + Linear_Expression expr = Linear_Expression(cg); Constraint c(expr == 0); // The polyhedron is non-empty so that there exists a point. - // For an arbitrary generator point find the scalar product with + // For an arbitrary generator point, compute the scalar product with // the equality. PPL_DIRTY_TEMP_COEFFICIENT(point_val); - for (Generator_System::const_iterator g = gen_sys.begin(), - gen_sys_end = gen_sys.end(); g != gen_sys_end; ++g) { - if (g->is_point()) { - Scalar_Products::assign(point_val, c, *g); + for (Generator_System::const_iterator gs_i = gen_sys.begin(), + gs_end = gen_sys.end(); gs_i != gs_end; ++gs_i) { + if (gs_i->is_point()) { + Scalar_Products::assign(point_val, c, *gs_i); break; } } - // Find the 2 hyperplanes that satisfies the congruence and are - // nearest to the point such that the point lies on or between these - // hyperplanes. + // Find 2 hyperplanes that satisfy the congruence and are near to + // the generating point (so that the point lies on or between these + // hyperplanes). // Then use the relations between the polyhedron and the corresponding - // half-spaces to determine its relation with the congruence. + // halfspaces to determine its relation with the congruence. const Coefficient& modulus = cg.modulus(); - PPL_DIRTY_TEMP_COEFFICIENT(div); - div = modulus; - + // FIXME: specify rounding mode. PPL_DIRTY_TEMP_COEFFICIENT(nearest); - nearest = (point_val / div) * div; + nearest = (point_val / modulus) * modulus; point_val -= nearest; expr -= nearest; if (point_val == 0) return relation_with(expr == 0); - Linear_Expression next_expr; - if (point_val > 0) { - next_expr = expr - modulus; - } - else { - expr = - (expr); - next_expr = expr - modulus; - } + // Build first halfspace. + const bool positive = (point_val > 0); + Constraint first_halfspace = positive ? (expr >= 0) : (expr <= 0); - Poly_Con_Relation relations = relation_with(expr >= 0); - assert(!relations.implies(Poly_Con_Relation::saturates()) - && !relations.implies(Poly_Con_Relation::is_disjoint())); - if (relations.implies(Poly_Con_Relation::strictly_intersects())) + Poly_Con_Relation first_rels = relation_with(first_halfspace); + assert(!first_rels.implies(Poly_Con_Relation::saturates()) + && !first_rels.implies(Poly_Con_Relation::is_disjoint())); + if (first_rels.implies(Poly_Con_Relation::strictly_intersects())) return Poly_Con_Relation::strictly_intersects(); - assert(relations == Poly_Con_Relation::is_included()); - Poly_Con_Relation next_relations = relation_with(next_expr <= 0); - assert(!next_relations.implies(Poly_Con_Relation::saturates()) - && !next_relations.implies(Poly_Con_Relation::is_disjoint())); - if (next_relations.implies(Poly_Con_Relation::strictly_intersects())) + // Build second halfspace. + if (positive) + expr -= modulus; + else + expr += modulus; + Constraint second_halfspace = positive ? (expr <= 0) : (expr >= 0); + + assert(first_rels == Poly_Con_Relation::is_included()); + Poly_Con_Relation second_rels = relation_with(second_halfspace); + assert(!second_rels.implies(Poly_Con_Relation::saturates()) + && !second_rels.implies(Poly_Con_Relation::is_disjoint())); + if (second_rels.implies(Poly_Con_Relation::strictly_intersects())) return Poly_Con_Relation::strictly_intersects(); - assert(next_relations == Poly_Con_Relation::is_included()); + assert(second_rels == Poly_Con_Relation::is_included()); return Poly_Con_Relation::is_disjoint(); }

1 0

[GIT] ppl/ppl(master): Fixed the invocation of the generic implementation of wrap_assign().
by Roberto Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 99eba6af02765f0fb6b9f717b2cb39724cf58f00 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=99eba6af0276… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 15:28:11 2009 +0200 Fixed the invocation of the generic implementation of wrap_assign(). --- src/Box.templates.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index e6117a2..95386d1 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1423,7 +1423,8 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, #if 1 // Generic implementation commented out. Implementation::wrap_assign(*this, vars, w, s, o, pcs, - complexity_threshold, wrap_individually); + complexity_threshold, wrap_individually, + "Box"); #else // Specialized implementation. used(wrap_individually); used(complexity_threshold);

1 0

[GIT] ppl/ppl(master): Check that all variables upon which `*pcs' depends are in `vars'.
by Roberto Bagnara 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: baa08eff6430b3f4934730a9f604fc9e1339055a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=baa08eff6430… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 15 15:12:50 2009 +0200 Check that all variables upon which `*pcs' depends are in `vars'. An assertion is violated otherwise. --- src/wrap_assign.hh | 31 +++++++++++++++++++++++++------ 1 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index b53d79e..c6c76eb 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -110,12 +110,31 @@ wrap_assign(PSET& pointset, // Dimension-compatibility check of `*pcs', if any. const dimension_type vars_space_dim = vars.space_dimension(); - if (pcs != 0 && pcs->space_dimension() > vars_space_dim) { - std::ostringstream s; - s << "PPL::" << class_name << "::wrap_assign(..., pcs, ...):" << std::endl - << "vars.space_dimension() == " << vars_space_dim - << ", pcs->space_dimension() == " << pcs->space_dimension() << "."; - throw std::invalid_argument(s.str()); + if (pcs != 0) { + if (pcs->space_dimension() > vars_space_dim) { + std::ostringstream s; + s << "PPL::" << class_name << "::wrap_assign(..., pcs, ...):" + << std::endl + << "vars.space_dimension() == " << vars_space_dim + << ", pcs->space_dimension() == " << pcs->space_dimension() << "."; + throw std::invalid_argument(s.str()); + } + +#ifndef NDEBUG + // Check that all variables upon which `*pcs' depends are in `vars'. + // An assertion is violated otherwise. + const Constraint_System cs = *pcs; + dimension_type cs_space_dim = cs.space_dimension(); + Variables_Set::const_iterator vars_end = vars.end(); + for (Constraint_System::const_iterator i = cs.begin(), + cs_end = cs.end(); i != cs_end; ++i) { + const Constraint& c = *i; + for (dimension_type d = cs_space_dim; d-- > 0; ) { + assert(c.coefficient(Variable(d)) == 0 + || vars.find(d) != vars_end); + } + } +#endif } // Wrapping no variable only requires refining with *pcs, if any.

1 0

[GIT] ppl/ppl(master): Several improvements to Octagonal_Shape<T>:: relation_with(const Congruence&).
by Enea Zaffanella 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: db4eb892c0382ac837fd8c2473450ed58ad35df3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=db4eb892c038… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 14:54:23 2009 +0200 Several improvements to Octagonal_Shape<T>::relation_with(const Congruence&). Alaso added a couple of FIXME regarding missing comments and rounding modes. --- src/Octagonal_Shape.templates.hh | 41 ++++++++++++++++++++----------------- 1 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 021e235..464a87a 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -1206,36 +1206,39 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { if (space_dim == 0) { if (cg.is_inconsistent()) return Poly_Con_Relation::is_disjoint(); - else if (cg.inhomogeneous_term() % cg.modulus() == 0) + else { + assert(cg.is_tautological()); return Poly_Con_Relation::saturates() && Poly_Con_Relation::is_included(); + } } - PPL_DIRTY_TEMP(Coefficient, min_num); - PPL_DIRTY_TEMP(Coefficient, min_den); + // FIXME: the following code has to be checked and improved. + // Add comment to explain what we are doing and why. + const Coefficient& inhomo = cg.inhomogeneous_term(); + Linear_Expression le = Linear_Expression(cg); + le -= inhomo; + PPL_DIRTY_TEMP_COEFFICIENT(min_num); + PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; - PPL_DIRTY_TEMP_COEFFICIENT(mod); - mod = cg.modulus(); - Linear_Expression le; - for (dimension_type i = cg_space_dim; i-- > 0; ) - le += cg.coefficient(Variable(i)) * Variable(i); bool bounded_below = minimize(le, min_num, min_den, min_included); if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - PPL_DIRTY_TEMP_COEFFICIENT(v); - PPL_DIRTY_TEMP_COEFFICIENT(lower_num); - PPL_DIRTY_TEMP_COEFFICIENT(lower_den); + PPL_DIRTY_TEMP_COEFFICIENT(val); + neg_assign(val, inhomo); + PPL_DIRTY_TEMP_COEFFICIENT(lower); - assign_r(lower_num, min_num, ROUND_NOT_NEEDED); - assign_r(lower_den, min_den, ROUND_NOT_NEEDED); - neg_assign(v, cg.inhomogeneous_term()); - lower = lower_num / lower_den; - v += ((lower / mod) * mod); - if (v * lower_den < lower_num) - v += mod; - const Constraint& c(le == v); + // FIXME: specify rounding mode. + lower = min_num / min_den; + + const Coefficient& mod = cg.modulus(); + // FIXME: specify rounding mode. + val += ((lower / mod) * mod); + if (val * min_den < min_num) + val += mod; + Constraint c(le == val); return relation_with(c); }

1 0

[GIT] ppl/ppl(master): Corrected typo in explanatory output.
by Enea Zaffanella 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 72619d2aafd034b54115e17459cb8c5b19da8280 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=72619d2aafd0… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 14:48:24 2009 +0200 Corrected typo in explanatory output. --- tests/Octagonal_Shape/relatwithcons2.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Octagonal_Shape/relatwithcons2.cc b/tests/Octagonal_Shape/relatwithcons2.cc index b763558..5f2026c 100644 --- a/tests/Octagonal_Shape/relatwithcons2.cc +++ b/tests/Octagonal_Shape/relatwithcons2.cc @@ -440,7 +440,7 @@ test20() { print_constraints(oc, "--- oc ---"); print_congruence(cg, "--- cg ---"); using namespace IO_Operators; - nout << "oc.relation_with((A %= 0)/1) == " << rel << endl; + nout << "oc.relation_with((A + 3*B %= 0)/1) == " << rel << endl; Poly_Con_Relation known_result = Poly_Con_Relation::strictly_intersects();

1 0

[GIT] ppl/ppl(master): Minor improvement.
by Enea Zaffanella 15 May '09

15 May '09

Module: ppl/ppl Branch: master Commit: 1736b8c74e21704643ebd5a878dcf0f7db0f9dc5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1736b8c74e21… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 15 14:47:30 2009 +0200 Minor improvement. --- doc/definitions.dox | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 9cbdb65..83cd6a7 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2072,15 +2072,15 @@ is the grid The library provides operators for checking the relation holding between a grid and -a congruence, a grid generator, constraint or a (polyhedron) generator. +a congruence, a grid generator, a constraint or a (polyhedron) generator. Suppose \f$\cL\f$ is a grid and \f$\cC\f$ an arbitrary congruence system representing \f$\cL\f$. Suppose also that \f$ \cg = \bigl( - \langle \vect{a}, \vect{x} \rangle \equiv_f b - \bigr) + \langle \vect{a}, \vect{x} \rangle \equiv_f b + \bigr) \f$ is a congruence relation with \f$\cL_{\cg} = \gcon\bigl(\{\cg\}\bigr)\f$.

1 0