Module: ppl/ppl Branch: master Commit: f28c8bf97087a04310fb24a1bed44163c371ee33 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f28c8bf97087a... Author: Enea Zaffanella <zaffanella@cs.unipr.it> Date: Sat May 16 12:04:14 2009 +0200 Further cleaning of relation_with(Congruence) implementations. --- src/BD_Shape.templates.hh | 45 +++++++++++++------------------------ src/Octagonal_Shape.templates.hh | 31 ++++++++++---------------- src/Polyhedron_public.cc | 37 ++++++++++++++++--------------- 3 files changed, 47 insertions(+), 66 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index f00a885..c57d575 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -1204,24 +1204,17 @@ BD_Shape<T>::max_min(const Linear_Expression& expr, template <typename T> Poly_Con_Relation BD_Shape<T>::relation_with(const Congruence& cg) const { - const dimension_type cg_space_dim = cg.space_dimension(); const dimension_type space_dim = space_dimension(); // Dimension-compatibility check. - if (cg_space_dim > space_dim) + if (cg.space_dimension() > space_dim) throw_dimension_incompatible("relation_with(cg)", cg); // If the congruence is a bounded difference equality, // find the relation with the equivalent equality constraint. if (cg.is_equality()) { Constraint c(cg); - dimension_type num_vars = 0; - dimension_type i = 0; - dimension_type j = 0; - PPL_DIRTY_TEMP_COEFFICIENT(coeff); - if (extract_bounded_difference(c, cg_space_dim, num_vars, - i, j, coeff)) - return relation_with(c); + return relation_with(c); } shortest_path_closure_assign(); @@ -1234,36 +1227,30 @@ BD_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 return Poly_Con_Relation::saturates() && Poly_Con_Relation::is_included(); } - PPL_DIRTY_TEMP(Coefficient, min_num); - PPL_DIRTY_TEMP(Coefficient, min_den); + // FIXME: add proper comments to the following. + Linear_Expression le = Linear_Expression(cg); + 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(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); + PPL_DIRTY_TEMP_COEFFICIENT(value); + value = min_num / min_den; + const Coefficient& modulus = cg.modulus(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); + signed_distance = value % modulus; + value -= signed_distance; + if (value * min_den < min_num) + value += modulus; + Constraint c(le == value); return relation_with(c); } diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index df6de2d..8f4973b 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -1190,9 +1190,8 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { dimension_type cg_space_dim = cg.space_dimension(); // Dimension-compatibility check. - if (cg_space_dim > space_dim) { + if (cg_space_dim > space_dim) throw_dimension_incompatible("relation_with(cg)", cg); - } // If the congruence is an equality, // find the relation with the equivalent equality constraint. @@ -1211,18 +1210,14 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { if (space_dim == 0) { if (cg.is_inconsistent()) return Poly_Con_Relation::is_disjoint(); - else { - assert(cg.is_tautological()); + else return Poly_Con_Relation::saturates() && Poly_Con_Relation::is_included(); - } } // 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; @@ -1231,19 +1226,17 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - PPL_DIRTY_TEMP_COEFFICIENT(val); - neg_assign(val, inhomo); - - PPL_DIRTY_TEMP_COEFFICIENT(lower); - // 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); + PPL_DIRTY_TEMP_COEFFICIENT(value); + value = min_num / min_den; + + const Coefficient& modulus = cg.modulus(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); + signed_distance = value % modulus; + value -= signed_distance; + if (value * min_den < min_num) + value += modulus; + Constraint c(le == value); return relation_with(c); } diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index a805773..94393b1 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -310,34 +310,35 @@ PPL::Polyhedron::relation_with(const Congruence& cg) const { // The polyhedron is non-empty so that there exists a point. // For an arbitrary generator point, compute the scalar product with // the equality. - PPL_DIRTY_TEMP_COEFFICIENT(point_val); - + PPL_DIRTY_TEMP_COEFFICIENT(sp_point); 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); + Scalar_Products::assign(sp_point, c, *gs_i); + expr -= sp_point; break; } } - // Find 2 hyperplanes that satisfy the congruence and are near to + // Find two 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 - // halfspaces to determine its relation with the congruence. - const Coefficient& modulus = cg.modulus(); - - // FIXME: specify rounding mode. - PPL_DIRTY_TEMP_COEFFICIENT(nearest); - nearest = (point_val / modulus) * modulus; + // two hyperplanes). + // Then use the relations between the polyhedron and the halfspaces + // corresponding to the hyperplanes to determine the result. - point_val -= nearest; - expr -= nearest; - if (point_val == 0) - return relation_with(expr == 0); + // Compute the distance from the point to an hyperplane. + const Coefficient& modulus = cg.modulus(); + PPL_DIRTY_TEMP_COEFFICIENT(signed_distance); + signed_distance = sp_point % modulus; + if (signed_distance == 0) + // The point is lying on the hyperplane. + return relation_with(expr == 0); + else + // The point is not lying on the hyperplane. + expr += signed_distance; - // Build first halfspace. - const bool positive = (point_val > 0); + // Build first halfspace constraint. + const bool positive = (signed_distance > 0); Constraint first_halfspace = positive ? (expr >= 0) : (expr <= 0); Poly_Con_Relation first_rels = relation_with(first_halfspace);