[PPL-devel] [GIT] ppl/ppl(termination): Function renamed. Unwanted stuff removed from comment.
Roberto Bagnara
bagnara at cs.unipr.it
Tue Mar 9 11:31:31 CET 2010
Module: ppl/ppl
Branch: termination
Commit: df002a70c37365fc661bb7674ba60baf71898ccb
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=df002a70c37365fc661bb7674ba60baf71898ccb
Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date: Tue Mar 9 14:31:09 2010 +0400
Function renamed. Unwanted stuff removed from comment.
---
src/termination.cc | 24 +++++++-----------------
src/termination.templates.hh | 14 +++++++-------
2 files changed, 14 insertions(+), 24 deletions(-)
diff --git a/src/termination.cc b/src/termination.cc
index 31b257a..cd1d168 100644
--- a/src/termination.cc
+++ b/src/termination.cc
@@ -176,13 +176,9 @@ 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 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$.
+ - \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$.
The improved Podelski-Rybalchenko method described in the paper
is based on a loop encoding of the form
@@ -259,18 +255,12 @@ fill_constraint_systems_MS(const Constraint_System& cs,
\f$ \vect{u}_3 \in \Qset_-^s \f$.
The space of ranking functions is then spanned by
\f$ \vect{u}_3^\transpose E_C' \vect x \f$.
-
- The allocation of variable indices in the output constraint
- system \p cs_out is as follows:
- - \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,
- const dimension_type n,
- const dimension_type m,
- Constraint_System& cs_out) {
+fill_constraint_system_PR(const Constraint_System& cs,
+ const dimension_type n,
+ const dimension_type m,
+ Constraint_System& cs_out) {
// Determine the partitioning of the m rows into the r rows
// of E_B and the s rows of E'_C|E_C.
std::deque<bool> in_A_B(m, true);
diff --git a/src/termination.templates.hh b/src/termination.templates.hh
index 84b56c3..0b28c19 100644
--- a/src/termination.templates.hh
+++ b/src/termination.templates.hh
@@ -119,10 +119,10 @@ fill_constraint_systems_MS(const Constraint_System& cs,
Constraint_System& cs_out2);
void
-fill_constraint_systems_PR(const Constraint_System& cs,
- const dimension_type n,
- const dimension_type m,
- Constraint_System& cs_out);
+fill_constraint_system_PR(const Constraint_System& cs,
+ const dimension_type n,
+ const dimension_type m,
+ Constraint_System& cs_out);
template <typename PSET>
void
@@ -344,7 +344,7 @@ termination_test_PR(const PSET& pset) {
prepare_input_MS_PR(pset, cs, n, m, "termination_test_PR");
Constraint_System cs_mip;
- fill_constraint_systems_PR(cs, n, m, cs_mip);
+ fill_constraint_system_PR(cs, n, m, cs_mip);
MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip);
@@ -361,7 +361,7 @@ one_affine_ranking_function_PR(const PSET& pset, Generator& mu) {
prepare_input_MS_PR(pset, cs, n, m, "one_affine_ranking_function_PR");
Constraint_System cs_mip;
- fill_constraint_systems_PR(cs, n, m, cs_mip);
+ fill_constraint_system_PR(cs, n, m, cs_mip);
MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip);
@@ -386,7 +386,7 @@ all_affine_ranking_functions_PR(const PSET& pset, C_Polyhedron& mu_space) {
prepare_input_MS_PR(pset, cs, n, m, "all_affine_ranking_functions_PR");
Constraint_System cs_out;
- fill_constraint_systems_PR(cs, n, m, cs_out);
+ fill_constraint_system_PR(cs, n, m, cs_out);
mu_space = C_Polyhedron(n+1, EMPTY);
}
More information about the PPL-devel
mailing list