Module: ppl/ppl Branch: master Commit: 43ec65852330b6023cf957b25db0c72398ad3de7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=43ec65852330b...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Wed Mar 31 01:21:14 2010 +0200

Fixed assign_all_inequalities_approximation for shapes.

---

src/termination.cc | 27 +++++++++++++++++++++++++ src/termination.templates.hh | 44 +++++------------------------------------ 2 files changed, 33 insertions(+), 38 deletions(-)

diff --git a/src/termination.cc b/src/termination.cc index bfadb64..3ba1213 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -31,6 +31,33 @@ namespace Implementation {

namespace Termination {

+void +assign_all_inequalities_approximation(const Constraint_System& cs_in, + Constraint_System& cs_out) { + if (cs_in.has_strict_inequalities() || cs_in.has_equalities()) { + // Here we have some strict inequality and/or equality constraints: + // translate them into non-strict inequality constraints. + for (Constraint_System::const_iterator i = cs_in.begin(), + i_end = cs_in.end(); i != i_end; ++i) { + const Constraint& c = *i; + if (c.is_equality()) { + // Insert the two corresponding opposing inequalities. + cs_out.insert(Linear_Expression(c) >= 0); + cs_out.insert(Linear_Expression(c) <= 0); + } + else if (c.is_strict_inequality()) + // Insert the non-strict approximation. + cs_out.insert(Linear_Expression(c) >= 0); + else + // Insert as is. + cs_out.insert(c); + } + } + else + // No strict inequality and no equality constraints. + cs_out = cs_in; +} + template <> void assign_all_inequalities_approximation(const C_Polyhedron& ph, diff --git a/src/termination.templates.hh b/src/termination.templates.hh index 79abb37..f60573c 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -132,33 +132,15 @@ output_function_PR(std::ostream& s, const Variable& v) { } #endif

-template <typename PSET> void +assign_all_inequalities_approximation(const Constraint_System& cs_in, + Constraint_System& cs_out); + +template <typename PSET> +inline void assign_all_inequalities_approximation(const PSET& pset, Constraint_System& cs) { - const Constraint_System& pset_cs = pset.minimized_constraints(); - if (pset_cs.has_strict_inequalities() || pset_cs.has_equalities()) { - // Here we have some strict inequality and/or equality constraints: - // translate them into non-strict inequality constraints. - for (Constraint_System::const_iterator i = pset_cs.begin(), - i_end = pset_cs.end(); i != i_end; ++i) { - const Constraint& c = *i; - if (c.is_equality()) { - // Insert the two corresponding opposing inequalities. - cs.insert(Linear_Expression(c) >= 0); - cs.insert(Linear_Expression(c) <= 0); - } - else if (c.is_strict_inequality()) - // Insert the non-strict approximation. - cs.insert(Linear_Expression(c) >= 0); - else - // Insert as is. - cs.insert(c); - } - } - else - // No strict inequality and no equality constraints. - cs = pset_cs; + assign_all_inequalities_approximation(pset.minimized_constraints(), cs); }

template <> @@ -166,20 +148,6 @@ void assign_all_inequalities_approximation(const C_Polyhedron& ph, Constraint_System& cs);

-template <typename T> -void -assign_all_inequalities_approximation(const BD_Shape<T>& bds, - Constraint_System& cs) { - cs = bds.minimized_constraints(); -} - -template <typename T> -void -assign_all_inequalities_approximation(const Octagonal_Shape<T>& ocs, - Constraint_System& cs) { - cs = ocs.minimized_constraints(); -} - void shift_unprimed_variables(Constraint_System& cs);