March 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(sparse_matrices): MIP_Problem: clarify code in linear_combine ().
by Marco Poletti 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: cac1e8a25713772bc81811871e10baa46ff7dfbd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cac1e8a25713… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Mar 25 19:08:34 2010 +0100 MIP_Problem: clarify code in linear_combine(). --- src/MIP_Problem.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index f673c42..d316260 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -1243,7 +1243,7 @@ PPL::MIP_Problem::linear_combine(matrix_row_reference_type x, const dimension_type k) { WEIGHT_BEGIN(); const dimension_type x_size = x.size(); - Coefficient& x_k = x[k]; + const Coefficient& x_k = x.get(k); const Coefficient& y_k = y.get(k); PPL_ASSERT(y_k != 0 && x_k != 0); // Let g be the GCD between `x[k]' and `y[k]'. @@ -1269,7 +1269,7 @@ PPL::MIP_Problem::linear_combine(row_type& x, const dimension_type k) { WEIGHT_BEGIN(); const dimension_type x_size = x.size(); - Coefficient& x_k = x[k]; + const Coefficient& x_k = x.get(k); const Coefficient& y_k = y.get(k); PPL_ASSERT(y_k != 0 && x_k != 0); // Let g be the GCD between `x[k]' and `y[k]'.

1 0

[GIT] ppl/ppl(sparse_matrices): PIP_Solution_Node: swap elements instead of copy-constructing them, in update_tableau().
by Marco Poletti 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: 76c398b3ee72ab472c15d19bd5db2ee3b7887a2d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=76c398b3ee72… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Mar 25 18:54:39 2010 +0100 PIP_Solution_Node: swap elements instead of copy-constructing them, in update_tableau(). --- src/PIP_Tree.cc | 45 ++++++++++++++++++++++++++++++--------------- 1 files changed, 30 insertions(+), 15 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 9f95009..97033ca 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -2255,14 +2255,19 @@ PIP_Solution_Node::update_tableau(const PIP_Problem& pip, { std::sort(buffer.begin(), buffer.end()); std::vector<std::pair<dimension_type,Coefficient> > - ::const_iterator j = buffer.begin(); + ::iterator j = buffer.begin(); std::vector<std::pair<dimension_type,Coefficient> > - ::const_iterator j_end = buffer.end(); + ::iterator j_end = buffer.end(); if (j != j_end) { - matrix_row_iterator itr = v_row.find_create(*j); + matrix_row_iterator itr = v_row.find_create(j->first); + // We need to do (*itr).second = j->second, this is faster. + std::swap((*itr).second, j->second); ++j; - for ( ; j != j_end; ++j) - itr = v_row.find_create(*j, itr); + for ( ; j != j_end; ++j) { + itr = v_row.find_create(j->first, itr); + // We need to do (*itr).second = j->second, this is faster. + std::swap((*itr).second, j->second); + } } } buffer.clear(); @@ -2302,14 +2307,19 @@ PIP_Solution_Node::update_tableau(const PIP_Problem& pip, { std::sort(buffer.begin(), buffer.end()); std::vector<std::pair<dimension_type,Coefficient> > - ::const_iterator j = buffer.begin(); + ::iterator j = buffer.begin(); std::vector<std::pair<dimension_type,Coefficient> > - ::const_iterator j_end = buffer.end(); + ::iterator j_end = buffer.end(); if (j != j_end) { - matrix_row_iterator itr = v_row.find_create(*j); + matrix_row_iterator itr = v_row.find_create(j->first); + // We need to do (*itr).second = j->second, this is faster. + std::swap((*itr).second, j->second); ++j; - for ( ; j != j_end; ++j) - itr = v_row.find_create(*j, itr); + for ( ; j != j_end; ++j) { + itr = v_row.find_create(j->first, itr); + // We need to do (*itr).second = j->second, this is faster. + std::swap((*itr).second, j->second); + } } } buffer.clear(); @@ -2324,14 +2334,19 @@ PIP_Solution_Node::update_tableau(const PIP_Problem& pip, { std::sort(buffer.begin(), buffer.end()); std::vector<std::pair<dimension_type,Coefficient> > - ::const_iterator j = buffer.begin(); + ::iterator j = buffer.begin(); std::vector<std::pair<dimension_type,Coefficient> > - ::const_iterator j_end = buffer.end(); + ::iterator j_end = buffer.end(); if (j != j_end) { - matrix_row_iterator itr = v_row.find_create(*j); + matrix_row_iterator itr = v_row.find_create(j->first); + // We need to do (*itr).second = j->second, this is faster. + std::swap((*itr).second, j->second); ++j; - for ( ; j != j_end; ++j) - itr = v_row.find_create(*j, itr); + for ( ; j != j_end; ++j) { + itr = v_row.find_create(j->first, itr); + // We need to do (*itr).second = j->second, this is faster. + std::swap((*itr).second, j->second); + } } } buffer.clear();

1 0

[GIT] ppl/ppl(sparse_matrices): PIP_Tree_Node: avoid insertion in method compatibility_check(), may be very slow with some backends.
by Marco Poletti 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: a843c36d1af584099d79f3b0515b45f843f5698f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a843c36d1af5… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Mar 25 18:48:38 2010 +0100 PIP_Tree_Node: avoid insertion in method compatibility_check(), may be very slow with some backends. --- src/PIP_Tree.cc | 16 ++++++++++++---- 1 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index c838a45..9f95009 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -2002,14 +2002,22 @@ PIP_Tree_Node::compatibility_check(matrix_type& s) { matrix_const_row_const_iterator row_i = s_mi.begin(); matrix_const_row_const_iterator row_end = s_mi.end(); if (row_i != row_end) { - cut_i = cut.find_create(*row_i); - mod_assign((*cut_i).second,(*cut_i).second,den); + if ((*row_i).first == 0) { + cut_i = cut.find_create(*row_i); + mod_assign((*cut_i).second,(*cut_i).second,den); + (*cut_i).second -= den; + } else { + cut_i = cut.find_create(0, den); + neg_assign((*cut_i).second); + cut_i = cut.find_create(*row_i, cut_i); + mod_assign((*cut_i).second,(*cut_i).second,den); + } for (++row_i; row_i != row_end; ++row_i) { cut_i = cut.find_create(*row_i, cut_i); mod_assign((*cut_i).second,(*cut_i).second,den); } - } - cut[0] -= den; + } else + cut[0] -= den; scaling.push_back(den); } // Check if an integer solution was found.

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row: swap elements instead of copy-constructing them, in combine().
by Marco Poletti 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: 36b217b5a355d92d68c6c16fdcf7530af6ce412b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=36b217b5a355… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Mar 25 18:40:25 2010 +0100 Unlimited_Sparse_Row: swap elements instead of copy-constructing them, in combine(). --- src/Unlimited_Sparse_Row.templates.hh | 26 ++++++++++++++++++-------- 1 files changed, 18 insertions(+), 8 deletions(-) diff --git a/src/Unlimited_Sparse_Row.templates.hh b/src/Unlimited_Sparse_Row.templates.hh index ada3a3d..d990c55 100644 --- a/src/Unlimited_Sparse_Row.templates.hh +++ b/src/Unlimited_Sparse_Row.templates.hh @@ -354,15 +354,17 @@ Unlimited_Sparse_Row::combine(const Unlimited_Sparse_Row& y, const Func1& f, const Func2& g, const Func3& h) { Unlimited_Sparse_Row row; iterator itr = row.end(); - const_iterator i = begin(); - const_iterator i_end = end(); + iterator i = begin(); + iterator i_end = end(); const_iterator j = y.begin(); const_iterator j_end = y.end(); if (i == i_end && j == j_end) return; if (j == j_end || (i != i_end && (*i).first < (*j).first)) { - itr = row.find_create(*i); + itr = row.find_create((*i).first); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); f((*itr).second); ++i; } else @@ -375,7 +377,9 @@ Unlimited_Sparse_Row::combine(const Unlimited_Sparse_Row& y, const Func1& f, PPL_ASSERT(i != i_end); PPL_ASSERT(j != j_end); PPL_ASSERT((*i).first == (*j).first); - itr = row.find_create(*i); + itr = row.find_create((*i).first); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); g((*itr).second, (*j).second); ++i; ++j; @@ -383,17 +387,21 @@ Unlimited_Sparse_Row::combine(const Unlimited_Sparse_Row& y, const Func1& f, PPL_ASSERT(itr != row.end()); while (i != i_end && j != j_end) { if ((*i).first < (*j).first) { - itr = row.find_create(*i,itr); + itr = row.find_create((*i).first, itr); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); f((*itr).second); ++i; } else { if ((*i).first > (*j).first) { - itr = row.find_create(*j,itr); + itr = row.find_create((*j).first, itr); h((*itr).second, (*j).second); ++j; } else { PPL_ASSERT((*i).first == (*j).first); - itr = row.find_create(*i,itr); + itr = row.find_create((*i).first, itr); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); g((*itr).second, (*j).second); ++i; ++j; @@ -401,7 +409,9 @@ Unlimited_Sparse_Row::combine(const Unlimited_Sparse_Row& y, const Func1& f, } } while (i != i_end) { - itr = row.find_create(*i,itr); + itr = row.find_create((*i).first, itr); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); f((*itr).second); ++i; }

1 0

[GIT] ppl/ppl(sparse_matrices): Unlimited_Sparse_Row: swap elements instead of copy-constructing them, in combine_needs_second() .
by Marco Poletti 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: sparse_matrices Commit: 6d7dd4361749a6d2782acb2ec0b3d5da2aad7d13 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6d7dd4361749… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Thu Mar 25 18:30:10 2010 +0100 Unlimited_Sparse_Row: swap elements instead of copy-constructing them, in combine_needs_second(). --- src/Unlimited_Sparse_Row.templates.hh | 22 +++++++++++++++------- 1 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/Unlimited_Sparse_Row.templates.hh b/src/Unlimited_Sparse_Row.templates.hh index 4b18c51..ada3a3d 100644 --- a/src/Unlimited_Sparse_Row.templates.hh +++ b/src/Unlimited_Sparse_Row.templates.hh @@ -180,15 +180,17 @@ Unlimited_Sparse_Row::combine_needs_second(const Unlimited_Sparse_Row& y, const Func1& g, const Func2& h) { Unlimited_Sparse_Row row; iterator itr = row.end(); - const_iterator i = begin(); - const_iterator i_end = end(); + iterator i = begin(); + iterator i_end = end(); const_iterator j = y.begin(); const_iterator j_end = y.end(); if (i == i_end && j == j_end) return; if (j == j_end || (i != i_end && (*i).first < (*j).first)) { - itr = row.find_create(*i); + itr = row.find_create((*i).first); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); ++i; } else if (i == i_end @@ -200,7 +202,9 @@ Unlimited_Sparse_Row::combine_needs_second(const Unlimited_Sparse_Row& y, PPL_ASSERT(i != i_end); PPL_ASSERT(j != j_end); PPL_ASSERT((*i).first == (*j).first); - itr = row.find_create(*i); + itr = row.find_create((*i).first); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); g((*itr).second, (*j).second); ++i; ++j; @@ -208,16 +212,20 @@ Unlimited_Sparse_Row::combine_needs_second(const Unlimited_Sparse_Row& y, PPL_ASSERT(itr != row.end()); while (i != i_end && j != j_end) { if ((*i).first < (*j).first) { - itr = row.find_create(*i, itr); + itr = row.find_create((*i).first, itr); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); ++i; } else { if ((*i).first > (*j).first) { - itr = row.find_create(*j, itr); + itr = row.find_create((*j).first, itr); h((*itr).second, (*j).second); ++j; } else { PPL_ASSERT((*i).first == (*j).first); - itr = row.find_create(*i, itr); + itr = row.find_create((*i).first, itr); + // We need to do (*itr).second = (*i).second, but this is faster. + std::swap((*itr).second, (*i).second); g((*itr).second, (*j).second); ++i; ++j;

1 0

[GIT] ppl/ppl(master): Fixed bugs leading to warning messages.
by Patricia Hill 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: 8988758c44cc31cfd7afe3ca3b5e172a7d46970b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8988758c44cc… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Thu Mar 25 13:32:24 2010 +0000 Fixed bugs leading to warning messages. --- interfaces/Java/jni/ppl_java_globals.cc | 20 ++++++++++++-------- 1 files changed, 12 insertions(+), 8 deletions(-) diff --git a/interfaces/Java/jni/ppl_java_globals.cc b/interfaces/Java/jni/ppl_java_globals.cc index b4de11f..e1c3688 100644 --- a/interfaces/Java/jni/ppl_java_globals.cc +++ b/interfaces/Java/jni/ppl_java_globals.cc @@ -452,19 +452,23 @@ Java_parma_1polyhedra_1library_Linear_1Expression_1Variable_initIDs JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_Linear_1Expression_is_1zero -(JNIEnv* env, jobject j_this) try { - Linear_Expression* this_ptr = &build_cxx_linear_expression(env, j_this); - return this_ptr->is_zero(); +(JNIEnv* env, jobject j_this) { + try { + return build_cxx_linear_expression(env, j_this).is_zero(); + } + CATCH_ALL + return false; } -CATCH_ALL JNIEXPORT jboolean JNICALL Java_parma_1polyhedra_1library_Linear_1Expression_all_1homogeneous_1terms_1are_1zero -(JNIEnv* env, jobject j_this) try { - Linear_Expression* this_ptr = &build_cxx_linear_expression(env, j_this); - return this_ptr->all_homogeneous_terms_are_zero(); +(JNIEnv* env, jobject j_this) { + try { + return build_cxx_linear_expression(env, j_this).all_homogeneous_terms_are_zero(); + } + CATCH_ALL + return false; } -CATCH_ALL JNIEXPORT void JNICALL Java_parma_1polyhedra_1library_MIP_1Problem_1Status_initIDs

1 0

[GIT] ppl/ppl(master): Avoid nonpositivity constraints in the enhanced PR methods by changing sign .
by Enea Zaffanella 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: e7cb392b7d54c2badadd7a7ab67a83a62f1c8565 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e7cb392b7d54… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 25 14:10:31 2010 +0100 Avoid nonpositivity constraints in the enhanced PR methods by changing sign. This is going to speed up the MIP_Problem based methods. --- src/termination.cc | 37 ++++++++++++++++++------------------- 1 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 160cead..93aaa88 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -301,12 +301,12 @@ fill_constraint_system_PR(const Constraint_System& cs_before, Variable u2_i(s + row_index); const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { - Coefficient_traits::const_reference k = c_i.coefficient(Variable(j)); + Coefficient_traits::const_reference A_ij_B = c_i.coefficient(Variable(j)); // (u1 - u2) A_B, in the context of j-th constraint. - add_mul_assign(les_eq[j], k, u1_i); - sub_mul_assign(les_eq[j], k, u2_i); + add_mul_assign(les_eq[j], A_ij_B, u1_i); + sub_mul_assign(les_eq[j], A_ij_B, u2_i); // u2 A_B, in the context of (j+n)-th constraint. - add_mul_assign(les_eq[j + n], k, u2_i); + add_mul_assign(les_eq[j + n], A_ij_B, u2_i); } // u2 b_B, in the context of the strict inequality constraint. add_mul_assign(le_out, c_i.inhomogeneous_term(), u2_i); @@ -334,9 +334,9 @@ fill_constraint_system_PR(const Constraint_System& cs_before, add_mul_assign(le_out, c_i.inhomogeneous_term(), u3_i); } - // Add the nonpositivity constraints for u_1, u_2 and u_3. + // Add the nonnegativity constraints for u_1, u_2 and u_3. for (dimension_type i = s + 2*r; i-- > 0; ) - cs_out.insert(Variable(i) <= 0); + cs_out.insert(Variable(i) >= 0); // FIXME: iterate backwards once the debugging phase is over. //for (dimension_type j = 2*n; j-- > 0; ) @@ -588,7 +588,7 @@ termination_test_PR(const Constraint_System& cs_before, #endif MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip, - le_ineq, MAXIMIZATION); + le_ineq, MINIMIZATION); switch (mip.solve()) { case UNFEASIBLE_MIP_PROBLEM: return false; @@ -600,7 +600,7 @@ termination_test_PR(const Constraint_System& cs_before, PPL_DIRTY_TEMP_COEFFICIENT(den); mip.optimal_value(num, den); PPL_ASSERT(den > 0); - return num > 0; + return num < 0; } } @@ -634,20 +634,20 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, #endif MIP_Problem mip = MIP_Problem(cs_mip.space_dimension(), cs_mip, - le_ineq, MAXIMIZATION); + le_ineq, MINIMIZATION); switch (mip.solve()) { case UNFEASIBLE_MIP_PROBLEM: return false; case UNBOUNDED_MIP_PROBLEM: - // We know that the supremum is plus infinity, which would suffice + // We know that the infimum is minus infinity, which would suffice // for a yes/no answer on termination. But we need to add a constraint // to the LP problem to be sure that the value of the objective - // function computed in the feasible point is positive. + // function computed in the feasible point is negative. finish: { - // We can impose that le_ineq is >= 1 because every positive + // We can impose that le_ineq is <= -1 because every positive // multiple of the linear expression is acceptable. - mip.add_constraint(le_ineq >= 1); + mip.add_constraint(le_ineq <= -1); Generator fp = mip.feasible_point(); PPL_ASSERT(fp.is_point()); @@ -669,7 +669,7 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, for (dimension_type j = n; j-- > 0; ) { Variable vj(j); k = fp_i * c_i.coefficient(vj); - add_mul_assign(le, k, vj); + sub_mul_assign(le, k, vj); } } // Note that we can neglect the divisor of `fp' since it is positive. @@ -682,7 +682,7 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, PPL_DIRTY_TEMP_COEFFICIENT(den); mip.optimal_value(num, den); PPL_ASSERT(den > 0); - if (num > 0) + if (num < 0) goto finish; else return false; @@ -724,7 +724,7 @@ one_affine_ranking_function_PR_original(const Constraint_System& cs, // function computed in the feasible point is negative. finish: { - // We can impose that le_ineq is <= -1 because every negative + // We can impose that le_ineq is <= -1 because every positive // multiple of the linear expression is acceptable. mip.add_constraint(le_ineq <= -1); Generator fp = mip.feasible_point(); @@ -796,7 +796,7 @@ all_affine_ranking_functions_PR(const Constraint_System& cs_before, #endif NNC_Polyhedron ph(cs_eqs); - ph.add_constraint(le_ineq > 0); + ph.add_constraint(le_ineq < 0); // u_3 corresponds to space dimensions 0, ..., s - 1. const dimension_type s = distance(cs_after.begin(), cs_after.end()); ph.remove_higher_space_dimensions(s); @@ -808,7 +808,6 @@ all_affine_ranking_functions_PR(const Constraint_System& cs_before, Variable::set_output_function(p_default_output_function); #endif - // FIXME: is this useful? const dimension_type n = cs_before.space_dimension(); const Generator_System& gs_in = ph.generators(); @@ -836,7 +835,7 @@ all_affine_ranking_functions_PR(const Constraint_System& cs_before, for (dimension_type j = n; j-- > 0; ) { Variable vj(j); k = g_i * c_i.coefficient(vj); - add_mul_assign(le, k, vj); + sub_mul_assign(le, k, vj); } } }

1 0

[GIT] ppl/ppl(master): Use original PR method if a single pointset is provided.
by Enea Zaffanella 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: fb01a69486339554291adcdba80fbf749c0437ea URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fb01a6948633… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 25 12:58:42 2010 +0100 Use original PR method if a single pointset is provided. Prefer the enhanced method if two pointsets (before/after) are provided. --- src/termination.templates.hh | 26 -------------------------- 1 files changed, 0 insertions(+), 26 deletions(-) diff --git a/src/termination.templates.hh b/src/termination.templates.hh index 3713cde..bf754d3 100644 --- a/src/termination.templates.hh +++ b/src/termination.templates.hh @@ -30,8 +30,6 @@ site: http://www.cs.unipr.it/ppl/ . */ #define PRINT_DEBUG_INFO 0 -#define USE_ORIGINAL_PR_METHOD 1 - #if PRINT_DEBUG_INFO #include <iostream> #endif @@ -402,18 +400,10 @@ termination_test_PR(const PSET& pset_after) { throw std::invalid_argument(s.str()); } -#if USE_ORIGINAL_PR_METHOD using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset_after, cs); return termination_test_PR_original(cs); -#else - // FIXME: this may be inefficient. - PSET pset_before(pset_after); - Variables_Set primed_variables(Variable(0), Variable(space_dim/2 - 1)); - pset_before.remove_space_dimensions(primed_variables); - return termination_test_PR_2(pset_before, pset_after); -#endif } template <typename PSET> @@ -452,18 +442,10 @@ one_affine_ranking_function_PR(const PSET& pset_after, Generator& mu) { throw std::invalid_argument(s.str()); } -#if USE_ORIGINAL_PR_METHOD using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset_after, cs); return one_affine_ranking_function_PR_original(cs, mu); -#else - // FIXME: this may be inefficient. - PSET pset_before(pset_after); - Variables_Set primed_variables(Variable(0), Variable(space_dim/2 - 1)); - pset_before.remove_space_dimensions(primed_variables); - return one_affine_ranking_function_PR_2(pset_before, pset_after, mu); -#endif } template <typename PSET> @@ -503,18 +485,10 @@ all_affine_ranking_functions_PR(const PSET& pset_after, throw std::invalid_argument(s.str()); } -#if USE_ORIGINAL_PR_METHOD using namespace Implementation::Termination; Constraint_System cs; assign_all_inequalities_approximation(pset_after, cs); all_affine_ranking_functions_PR_original(cs, mu_space); -#else - // FIXME: this may be inefficient. - PSET pset_before(pset_after); - Variables_Set primed_variables(Variable(0), Variable(space_dim/2 - 1)); - pset_before.remove_space_dimensions(primed_variables); - all_affine_ranking_functions_PR_2(pset_before, pset_after, mu_space); -#endif } } // namespace Parma_Polyhedra_Library

1 0

[GIT] ppl/ppl(master): Avoid the creation of many temporary linear expressions.
by Enea Zaffanella 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: c7fb3d1d0cee754ee43efa570ed8e8c6267f9b95 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c7fb3d1d0cee… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 25 12:37:25 2010 +0100 Avoid the creation of many temporary linear expressions. --- src/termination.cc | 88 +++++++++++++++++++++++++++++----------------------- 1 files changed, 49 insertions(+), 39 deletions(-) diff --git a/src/termination.cc b/src/termination.cc index 6876232..160cead 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -66,7 +66,7 @@ shift_unprimed_variables(Constraint_System& cs) { Coefficient_traits::const_reference a_i_j = c_i.coefficient(Variable(j)); if (a_i_j != 0) - le_i_shifted += a_i_j*Variable(cs_space_dim + j); + add_mul_assign(le_i_shifted, a_i_j, Variable(cs_space_dim + j)); } cs_shifted.insert(le_i_shifted >= c_i.inhomogeneous_term()); } @@ -138,15 +138,15 @@ fill_constraint_systems_MS(const Constraint_System& cs, Coefficient_traits::const_reference b_i = c_i.inhomogeneous_term(); // Note that b_i is to the left ot the relation sign, hence here // we have -= and not += just to avoid negating b_i. - y_le -= b_i*Variable(y); + sub_mul_assign(y_le, b_i, Variable(y)); cs_out1.insert(Variable(y) >= 0); // We have -= and not += for the same reason mentioned above. - z_le -= b_i*Variable(z); + sub_mul_assign(z_le, b_i, Variable(z)); cs_out2.insert(Variable(z) >= 0); for (dimension_type j = 2*n; j-- > 0; ) { Coefficient_traits::const_reference a_i_j = c_i.coefficient(Variable(j)); - y_les[j] += a_i_j*Variable(y); - z_les[j] += a_i_j*Variable(z); + add_mul_assign(y_les[j], a_i_j, Variable(y)); + add_mul_assign(z_les[j], a_i_j, Variable(z)); } ++y; ++z; @@ -297,31 +297,41 @@ fill_constraint_system_PR(const Constraint_System& cs_before, cs_before_end = cs_before.end(); i != cs_before_end; ++i, ++row_index) { + Variable u1_i(m + row_index); + Variable u2_i(s + row_index); const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { Coefficient_traits::const_reference k = c_i.coefficient(Variable(j)); - les_eq[j] += k*Variable(m + row_index); - les_eq[j] -= k*Variable(s + row_index); - les_eq[j + n] += k*Variable(s + row_index); + // (u1 - u2) A_B, in the context of j-th constraint. + add_mul_assign(les_eq[j], k, u1_i); + sub_mul_assign(les_eq[j], k, u2_i); + // u2 A_B, in the context of (j+n)-th constraint. + add_mul_assign(les_eq[j + n], k, u2_i); } - le_out += c_i.inhomogeneous_term()*Variable(s + row_index); + // u2 b_B, in the context of the strict inequality constraint. + add_mul_assign(le_out, c_i.inhomogeneous_term(), u2_i); } - row_index = 0; for (Constraint_System::const_iterator i = cs_after.begin(), cs_after_end = cs_after.end(); i != cs_after_end; ++i, ++row_index) { + Variable u3_i(row_index); const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { - PPL_DIRTY_TEMP_COEFFICIENT(k); - k = c_i.coefficient(Variable(j + n)); - les_eq[j] -= k*Variable(row_index); - k += c_i.coefficient(Variable(j)); - les_eq[j + n] += k*Variable(row_index); + Coefficient_traits::const_reference + A_ij_C = c_i.coefficient(Variable(j + n)); + Coefficient_traits::const_reference + Ap_ij_C = c_i.coefficient(Variable(j)); + // - u3 A_C, in the context of the j-th constraint. + sub_mul_assign(les_eq[j], A_ij_C, u3_i); + // u3 (A_C + Ap_C), in the context of the (j+n)-th constraint. + add_mul_assign(les_eq[j+n], A_ij_C, u3_i); + add_mul_assign(les_eq[j+n], Ap_ij_C, u3_i); } - le_out += c_i.inhomogeneous_term()*Variable(row_index); + // u3 b_C, in the context of the strict inequality constraint. + add_mul_assign(le_out, c_i.inhomogeneous_term(), u3_i); } // Add the nonpositivity constraints for u_1, u_2 and u_3. @@ -347,22 +357,22 @@ fill_constraint_system_PR_original(const Constraint_System& cs, for (Constraint_System::const_iterator i = cs.begin(), cs_end = cs.end(); i != cs_end; ++i, ++row_index) { const Constraint& c_i = *i; - const Variable lambda_1(row_index); - const Variable lambda_2(m + row_index); + const Variable lambda1_i(row_index); + const Variable lambda2_i(m + row_index); for (dimension_type j = n; j-- > 0; ) { - Coefficient_traits::const_reference Apj = c_i.coefficient(Variable(j)); - Coefficient_traits::const_reference Aj = c_i.coefficient(Variable(j+n)); + Coefficient_traits::const_reference Ap_ij = c_i.coefficient(Variable(j)); + Coefficient_traits::const_reference A_ij = c_i.coefficient(Variable(j+n)); // lambda_1 A' - les_eq[j] += Apj * lambda_1; + add_mul_assign(les_eq[j], Ap_ij, lambda1_i); // (lambda_1 - lambda_2) A - les_eq[j+n] += Aj * lambda_1; - les_eq[j+n] -= Aj * lambda_2; + add_mul_assign(les_eq[j+n], A_ij, lambda1_i); + sub_mul_assign(les_eq[j+n], A_ij, lambda2_i); // lambda_2 (A + A') - les_eq[j+n+n] += Aj * lambda_2; - les_eq[j+n+n] += Apj * lambda_2; + add_mul_assign(les_eq[j+n+n], A_ij, lambda2_i); + add_mul_assign(les_eq[j+n+n], Ap_ij, lambda2_i); } // lambda2 b - le_out += c_i.inhomogeneous_term() * lambda_2; + add_mul_assign(le_out, c_i.inhomogeneous_term(), lambda2_i); } // Add the non-negativity constraints for lambda_1 and lambda_2. @@ -450,7 +460,7 @@ one_affine_ranking_function_MS(const Constraint_System& cs, Generator& mu) { Linear_Expression le; for (dimension_type i = n+1; i-- > 0; ) { Variable vi(i); - le += vi*fp.coefficient(vi); + add_mul_assign(le, fp.coefficient(vi), vi); } mu = point(le, fp.divisor()); return true; @@ -658,8 +668,8 @@ one_affine_ranking_function_PR(const Constraint_System& cs_before, const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { Variable vj(j); - k = fp_i*c_i.coefficient(vj); - le += k*vj; + k = fp_i * c_i.coefficient(vj); + add_mul_assign(le, k, vj); } } // Note that we can neglect the divisor of `fp' since it is positive. @@ -735,9 +745,9 @@ one_affine_ranking_function_PR_original(const Constraint_System& cs, const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { Variable vj(j); - Coefficient_traits::const_reference Ap_j = c_i.coefficient(vj); - k = fp_i * Ap_j; - le -= k * vj; + Coefficient_traits::const_reference Ap_ij = c_i.coefficient(vj); + k = fp_i * Ap_ij; + sub_mul_assign(le, k, vj); } } } @@ -825,8 +835,8 @@ all_affine_ranking_functions_PR(const Constraint_System& cs_before, const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { Variable vj(j); - k = g_i*c_i.coefficient(vj); - le += k*vj; + k = g_i * c_i.coefficient(vj); + add_mul_assign(le, k, vj); } } } @@ -897,15 +907,15 @@ all_affine_ranking_functions_PR_original(const Constraint_System& cs, PPL_DIRTY_TEMP_COEFFICIENT(k); for (Constraint_System::const_iterator i = cs.begin(), cs_end = cs.end(); i != cs_end; ++i, ++row_index) { - Variable lambda_2(row_index); - Coefficient_traits::const_reference g_i = g.coefficient(lambda_2); + Variable lambda2_i(row_index); + Coefficient_traits::const_reference g_i = g.coefficient(lambda2_i); if (g_i != 0) { const Constraint& c_i = *i; for (dimension_type j = n; j-- > 0; ) { Variable vj(j); - Coefficient_traits::const_reference Ap_j = c_i.coefficient(vj); - k = g_i * Ap_j; - le -= k * vj; + Coefficient_traits::const_reference Ap_ij = c_i.coefficient(vj); + k = g_i * Ap_ij; + sub_mul_assign(le, k, vj); } } }

1 0

[GIT] ppl/ppl(master): Added helper function sub_mul_assign() to Linear_Expression interface.
by Enea Zaffanella 25 Mar '10

25 Mar '10

Module: ppl/ppl Branch: master Commit: 6f07d12fc19f7b867a5b43f6f143f2fd202ff928 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6f07d12fc19f… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Thu Mar 25 12:00:22 2010 +0100 Added helper function sub_mul_assign() to Linear_Expression interface. --- src/Linear_Expression.cc | 19 +++++++++++++++++++ src/Linear_Expression.defs.hh | 9 +++++++++ 2 files changed, 28 insertions(+), 0 deletions(-) diff --git a/src/Linear_Expression.cc b/src/Linear_Expression.cc index f7d50a3..cd8ace8 100644 --- a/src/Linear_Expression.cc +++ b/src/Linear_Expression.cc @@ -373,6 +373,25 @@ PPL::add_mul_assign(Linear_Expression& e, return e; } +/*! \relates Parma_Polyhedra_Library::Linear_Expression */ +PPL::Linear_Expression& +PPL::sub_mul_assign(Linear_Expression& e, + Coefficient_traits::const_reference n, + const Variable v) { + const dimension_type v_space_dim = v.space_dimension(); + if (v_space_dim > Linear_Expression::max_space_dimension()) + throw std::length_error("Linear_Expression& " + "PPL::sub_mul_assign(e, n, v):\n" + "v exceeds the maximum allowed space dimension."); + const dimension_type e_size = e.size(); + if (e_size <= v_space_dim) { + Linear_Expression new_e(e, v_space_dim+1); + e.swap(new_e); + } + e[v_space_dim] -= n; + return e; +} + bool PPL::Linear_Expression::OK() const { return Linear_Row::OK(); diff --git a/src/Linear_Expression.defs.hh b/src/Linear_Expression.defs.hh index 5e4c81d..222ba57 100644 --- a/src/Linear_Expression.defs.hh +++ b/src/Linear_Expression.defs.hh @@ -172,6 +172,12 @@ Linear_Expression& add_mul_assign(Linear_Expression& e, Coefficient_traits::const_reference n, Variable v); +//! Returns the linear expression \p e - \p n * \p v and assigns it to \p e. +/*! \relates Linear_Expression */ +Linear_Expression& +sub_mul_assign(Linear_Expression& e, + Coefficient_traits::const_reference n, Variable v); + namespace IO_Operators { //! Output operator. @@ -469,6 +475,9 @@ private: friend Linear_Expression& add_mul_assign(Linear_Expression& e, Coefficient_traits::const_reference n, Variable v); + friend Linear_Expression& + sub_mul_assign(Linear_Expression& e, + Coefficient_traits::const_reference n, Variable v); friend std::ostream& Parma_Polyhedra_Library::IO_Operators

1 0