Module: ppl/ppl Branch: termination Commit: c59646077762fcf090705ece6876b8ef35623c8b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c59646077762f...
Author: Roberto Bagnara bagnara@cs.unipr.it Date: Mon Mar 8 15:41:23 2010 +0400
Comments improved.
---
src/termination.cc | 49 +++++++++++++++++++++++++++++-------------------- 1 files changed, 29 insertions(+), 20 deletions(-)
diff --git a/src/termination.cc b/src/termination.cc index d0d1909..a643997 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -60,8 +60,10 @@ assign_all_inequalities_approximation(const C_Polyhedron& ph, \param cs The input constraint system, where variables indices are allocated as follows: - - \f$ x'_1, \ldots, x'_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ x_1, \ldots, x_n \f$ go onto \f$ n, \ldots, 2n-1 \f$. + - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions + \f$ 0, \ldots, n-1 \f$, + - \f$ x_1, \ldots, x_n \f$ go onto space dimensions + \f$ n, \ldots, 2n-1 \f$, . The system does not contain any equality.
@@ -80,17 +82,20 @@ assign_all_inequalities_approximation(const C_Polyhedron& ph,
The allocation of variable indices in the output constraint systems \p cs_out1 and \p cs_out2 is as follows: - - \f$ \mu_1, \ldots, \mu_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ \mu_0\f$ goes onto \f$ n \f$; - - \f$ y_1, \ldots, y_m \f$ go onto \f$ n+1, \ldots, n+m \f$; - + - \f$ \mu_1, \ldots, \mu_n \f$ go onto space dimensions + \f$ 0, \ldots, n-1 \f$; + - \f$ \mu_0\f$ goes onto space dimension \f$ n \f$; + - \f$ y_1, \ldots, y_m \f$ go onto space dimensions + \f$ n+1, \ldots, n+m \f$; + . if we use the same constraint system, that is <CODE>&cs_out1 == &cs_out2</CODE>, then - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ - go onto \f$ n+m+1, ..., n+2*m+2 \f$; - + - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions + \f$ n+m+1, ..., n+2*m+2 \f$; + . otherwise - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto \f$ n+1, ..., n+m+2 \f$. + - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions + \f$ n+1, ..., n+m+2 \f$. */ void fill_constraint_systems_MS(const Constraint_System& cs, @@ -155,8 +160,10 @@ fill_constraint_systems_MS(const Constraint_System& cs, \param cs The input constraint system, where variables indices are allocated as follows: - - \f$ x'_1, \ldots, x'_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ x_1, \ldots, x_n \f$ go onto \f$ n, \ldots, 2n-1 \f$; + - \f$ x'_1, \ldots, x'_n \f$ go onto space dimensions + \f$ 0, \ldots, n-1 \f$, + - \f$ x_1, \ldots, x_n \f$ go onto space dimensions + \f$ n, \ldots, 2n-1 \f$, . The system does not contain any equality.
@@ -169,11 +176,13 @@ fill_constraint_systems_MS(const Constraint_System& cs, \param cs_out The output constraint system, where variables indices are allocated as follows: - - \f$ \mu_1, \ldots, \mu_n \f$ go onto \f$ 0, \ldots, n-1 \f$; - - \f$ \mu_0\f$ goes onto \f$ n \f$; - - \f$ y_1, \ldots, y_m \f$ go onto \f$ n+1, \ldots, n+m \f$; - - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ - go onto \f$ n+m+1, ..., n+2*m+2 \f$. + - \f$ \mu_1, \ldots, \mu_n \f$ go onto space dimensions + \f$ 0, \ldots, n-1 \f$; + - \f$ \mu_0\f$ goes onto space dimension \f$ n \f$; + - \f$ y_1, \ldots, y_m \f$ go onto space dimensions + \f$ n+1, \ldots, n+m \f$; + - \f$ z_1, ..., z_m, z_{m+1}, z_{m+2} \f$ go onto space dimensions + \f$ n+m+1, ..., n+2*m+2 \f$.
The improved Podelski-Rybalchenko method described in the paper is based on a loop encoding of the form @@ -250,9 +259,9 @@ fill_constraint_systems_MS(const Constraint_System& cs,
The allocation of variable indices in the output constraint system \p cs_out is as follows: - - \f$ u_3 \f$ goes onto \f$ 0, \ldots, s-1 \f$; - - \f$ u_2 \f$ goes onto \f$ s, \ldots, s+r-1 \f$; - - \f$ u_1 \f$ goes onto \f$ s+r, \ldots, s+2r-1 \f$. + - \f$ u_3 \f$ goes onto space dimensions \f$ 0, \ldots, s-1 \f$; + - \f$ u_2 \f$ goes onto space dimensions \f$ s, \ldots, s+r-1 \f$; + - \f$ u_1 \f$ goes onto space dimensions \f$ s+r, \ldots, s+2r-1 \f$. */ void fill_constraint_systems_PR(const Constraint_System& cs,