
Module: ppl/ppl Branch: master Commit: 2fd3833a17b3c175fca9517ce2e5740686f37aee URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fd3833a17b3c...
Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Sat Mar 27 11:04:12 2010 +0100
Other minor improvements in assign_all_inequalities_approximation().
---
src/termination.cc | 20 +++++++++++--------- src/termination.templates.hh | 29 ++++++++++++++++------------- 2 files changed, 27 insertions(+), 22 deletions(-)
diff --git a/src/termination.cc b/src/termination.cc index 8645b4b..01ab60a 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -35,23 +35,25 @@ template <> void assign_all_inequalities_approximation(const C_Polyhedron& ph, Constraint_System& cs) { - cs = ph.minimized_constraints(); - if (cs.has_equalities() > 0) { - Constraint_System tmp_cs; - for (Constraint_System::const_iterator i = cs.begin(), - cs_end = cs.end(); i != cs_end; ++i) { + const Constraint_System& ph_cs = ph.minimized_constraints(); + if (ph_cs.has_equalities()) { + // Translate equalities into inequalities. + for (Constraint_System::const_iterator i = ph_cs.begin(), + i_end = ph_cs.end(); i != i_end; ++i) { const Constraint& c = *i; if (c.is_equality()) { // Insert the two corresponding opposing inequalities. - tmp_cs.insert(Linear_Expression(c) >= 0); - tmp_cs.insert(Linear_Expression(c) <= 0); + cs.insert(Linear_Expression(c) >= 0); + cs.insert(Linear_Expression(c) <= 0); } else // Insert as is. - tmp_cs.insert(c); + cs.insert(c); } - cs = tmp_cs; } + else + // No equality constraints (and no strict inequalities). + cs = ph_cs; }
void diff --git a/src/termination.templates.hh b/src/termination.templates.hh index bf754d3..f5dc925 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -149,26 +149,29 @@ template <typename PSET> void assign_all_inequalities_approximation(const PSET& pset, Constraint_System& cs) { - cs = pset.minimized_constraints(); - if (cs.has_strict_inequalities() || cs.has_equalities() > 0) { - Constraint_System tmp_cs; - for (Constraint_System::const_iterator i = cs.begin(), - cs_end = cs.end(); i != cs_end; ++i) { + 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. - tmp_cs.insert(Linear_Expression(c) >= 0); - tmp_cs.insert(Linear_Expression(c) <= 0); + // 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. - tmp_cs.insert(Linear_Expression(c) >= 0); + // Insert the non-strict approximation. + cs.insert(Linear_Expression(c) >= 0); else - // Insert as is. - tmp_cs.insert(c); + // Insert as is. + cs.insert(c); } - cs = tmp_cs; } + else + // No strict inequality and no equality constraints. + cs = pset_cs; }
template <>