Module: ppl/ppl Branch: master Commit: b827904975bbeff4079fbb5aedf66a3ac4cb8e30 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b827904975bbe... Author: Patricia Hill <p.m.hill@leeds.ac.uk> Date: Mon May 18 11:26:03 2009 +0100 Improved the relation_with(Congruence) implementation for the weakly relational domains. --- src/BD_Shape.templates.hh | 61 ++++++++++++++++++++++++++++++------- src/Octagonal_Shape.templates.hh | 58 ++++++++++++++++++++++++++++------- 2 files changed, 95 insertions(+), 24 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index eeafd27..819b99e 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -1209,8 +1209,8 @@ BD_Shape<T>::relation_with(const Congruence& cg) const { 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 the congruence is an equality, find the relation with + // the equivalent equality constraint. if (cg.is_equality()) { Constraint c(cg); return relation_with(c); @@ -1231,26 +1231,63 @@ BD_Shape<T>::relation_with(const Congruence& cg) const { && Poly_Con_Relation::is_included(); } - // FIXME: add proper comments to the following. + // Find the lower bound for a hyperplane with direction + // defined by the congruence. Linear_Expression le = Linear_Expression(cg); PPL_DIRTY_TEMP_COEFFICIENT(min_num); PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; bool bounded_below = minimize(le, min_num, min_den, min_included); + // If there is no lower bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - PPL_DIRTY_TEMP_COEFFICIENT(value); - value = min_num / min_den; - const Coefficient& modulus = cg.modulus(); + // TODO: Consider adding a max_and_min() method, performing both + // maximization and minimization so as to possibly exploit + // incrementality of the MIP solver. + + // Find the upper bound for a hyperplane with direction + // defined by the congruence. + PPL_DIRTY_TEMP_COEFFICIENT(max_num); + PPL_DIRTY_TEMP_COEFFICIENT(max_den); + bool max_included; + bool bounded_above = maximize(le, max_num, max_den, max_included); + + // If there is no upper bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. + if (!bounded_above) + return Poly_Con_Relation::strictly_intersects(); + 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); + + // Find the position value for the hyperplane that satisfies the congruence + // and is above the lower bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + min_value = min_num / min_den; + const Coefficient& modulus = cg.modulus(); + signed_distance = min_value % modulus; + min_value -= signed_distance; + if (min_value * min_den < min_num) + min_value += modulus; + + // Find the position value for the hyperplane that satisfies the congruence + // and is below the upper bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + max_value = max_num / max_den; + signed_distance = max_value % modulus; + max_value += signed_distance; + if (max_value * max_den > max_num) + max_value -= modulus; + + // If the upper bound value is less than the lower bound value, + // then there is an empty intersection with the congruence; + // otherwise it will strictly intersect. + if (max_value < min_value) + return Poly_Con_Relation::is_disjoint(); + else + return Poly_Con_Relation::strictly_intersects(); } diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index de6bab5..4d46ac7 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -1214,29 +1214,63 @@ Octagonal_Shape<T>::relation_with(const Congruence& cg) const { && 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. + // Find the lower bound for a hyperplane with direction + // defined by the congruence. Linear_Expression le = Linear_Expression(cg); PPL_DIRTY_TEMP_COEFFICIENT(min_num); PPL_DIRTY_TEMP_COEFFICIENT(min_den); bool min_included; bool bounded_below = minimize(le, min_num, min_den, min_included); + // If there is no lower bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. if (!bounded_below) return Poly_Con_Relation::strictly_intersects(); - // FIXME: specify rounding mode. - PPL_DIRTY_TEMP_COEFFICIENT(value); - value = min_num / min_den; + // TODO: Consider adding a max_and_min() method, performing both + // maximization and minimization so as to possibly exploit + // incrementality of the MIP solver. + + // Find the upper bound for a hyperplane with direction + // defined by the congruence. + PPL_DIRTY_TEMP_COEFFICIENT(max_num); + PPL_DIRTY_TEMP_COEFFICIENT(max_den); + bool max_included; + bool bounded_above = maximize(le, max_num, max_den, max_included); + + // If there is no upper bound, then some of the hyperplanes defined by + // the congruence will strictly intersect the shape. + if (!bounded_above) + return Poly_Con_Relation::strictly_intersects(); - 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); + + // Find the position value for the hyperplane that satisfies the congruence + // and is above the lower bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + min_value = min_num / min_den; + const Coefficient& modulus = cg.modulus(); + signed_distance = min_value % modulus; + min_value -= signed_distance; + if (min_value * min_den < min_num) + min_value += modulus; + + // Find the position value for the hyperplane that satisfies the congruence + // and is below the upper bound for the shape. + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + max_value = max_num / max_den; + signed_distance = max_value % modulus; + max_value += signed_distance; + if (max_value * max_den > max_num) + max_value -= modulus; + + // If the upper bound value is less than the lower bound value, + // then there is an empty intersection with the congruence; + // otherwise it will strictly intersect. + if (max_value < min_value) + return Poly_Con_Relation::is_disjoint(); + else + return Poly_Con_Relation::strictly_intersects(); } template <typename T>