September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): It is NECESSARY to delay the update of unary constraints on var.
by Fabio Bossi 15 Sep '09

15 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a1e7e39e58515de6438993797f5041b1ae4067c2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a1e7e39e5851… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 15 09:26:44 2009 +0200 It is NECESSARY to delay the update of unary constraints on var. --- src/Octagonal_Shape.templates.hh | 23 +++++++++++------------ 1 files changed, 11 insertions(+), 12 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 5729793..c63676f 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4872,17 +4872,6 @@ Octagonal_Shape<T>::affine_image(Variable var, Linear_Form<FP_Interval_Type> minus_lf(-lf); - PPL_DIRTY_TEMP(N, lf_ub); - linear_form_upper_bound(lf, lf_ub); - PPL_DIRTY_TEMP(N, minus_lf_ub); - linear_form_upper_bound(minus_lf, minus_lf_ub); - - // Update unary constraints on var. - mul_2exp_assign_r(lf_ub, lf_ub, 1, ROUND_IGNORE); - assign_r(matrix[n_var+1][n_var], lf_ub, ROUND_NOT_NEEDED); - mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_IGNORE); - assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED); - // Declare temporaries outside the loop. PPL_DIRTY_TEMP(N, lf_plus_var_ub); PPL_DIRTY_TEMP(N, lf_minus_var_ub); @@ -4897,7 +4886,7 @@ Octagonal_Shape<T>::affine_image(Variable var, ++m_iter; Row_Iterator m_end = matrix.row_end(); - // Update binary constraints on var. + // Update binary constraints on var FIRST. for (dimension_type curr_var = var_id, n_curr_var = n_var - 2; curr_var-- > 0; ) { Variable current(curr_var); @@ -4927,6 +4916,16 @@ Octagonal_Shape<T>::affine_image(Variable var, ++curr_var; } + // Finally, update unary constraints on var. + PPL_DIRTY_TEMP(N, lf_ub); + linear_form_upper_bound(lf, lf_ub); + PPL_DIRTY_TEMP(N, minus_lf_ub); + linear_form_upper_bound(minus_lf, minus_lf_ub); + mul_2exp_assign_r(lf_ub, lf_ub, 1, ROUND_IGNORE); + assign_r(matrix[n_var+1][n_var], lf_ub, ROUND_NOT_NEEDED); + mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_IGNORE); + assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED); + } template <typename T>

1 0

[GIT] ppl/ppl(master): Added missing comment.
by Roberto Bagnara 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: master Commit: cb4d41cada4e9a0cc4146ac0edc234d834fd3584 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cb4d41cada4e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Sep 14 21:21:25 2009 +0200 Added missing comment. --- src/c_streambuf.defs.hh | 2 ++ 1 files changed, 2 insertions(+), 0 deletions(-) diff --git a/src/c_streambuf.defs.hh b/src/c_streambuf.defs.hh index 6e406a8..1233d73 100644 --- a/src/c_streambuf.defs.hh +++ b/src/c_streambuf.defs.hh @@ -31,6 +31,8 @@ class Parma_Polyhedra_Library::c_streambuf public: //! Constructor. c_streambuf(); + + //! Destructor. virtual ~c_streambuf(); protected:

1 0

[GIT] ppl/ppl(floating_point): Fixed two serious bugs in linear_form_upper_bound.
by Fabio Bossi 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: floating_point Commit: ecb0e94a30b0fa34808d2273682db0147a3a8344 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ecb0e94a30b0… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 14 17:56:12 2009 +0200 Fixed two serious bugs in linear_form_upper_bound. --- src/Octagonal_Shape.templates.hh | 7 ++++--- 1 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 783fcfb..5729793 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4943,6 +4943,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, PPL_ASSERT(std::numeric_limits<T>::max_exponent); const dimension_type lf_space_dimension = lf.space_dimension(); + PPL_ASSERT(lf_space_dimension <= space_dim); typedef Interval<T, Interval_Info> FP_Interval_Type; @@ -4968,15 +4969,15 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(curr_ub, curr_coefficient->upper(), ROUND_NOT_NEEDED); if (curr_lb != 0 && curr_ub != 0) { assign_r(curr_var_ub, matrix[n_var+1][n_var], ROUND_NOT_NEEDED); - mul_2exp_assign_r(curr_var_ub, curr_var_ub, -1, ROUND_IGNORE); + div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_IGNORE); neg_assign_r(curr_minus_var_ub, matrix[n_var][n_var+1], ROUND_NOT_NEEDED); - mul_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, -1, ROUND_IGNORE); + div_2exp_assign_r(curr_minus_var_ub, curr_minus_var_ub, 1, ROUND_IGNORE); // Optimize the most common case: curr = +/-[1;1] if (curr_lb == 1 && curr_ub == 1) { add_assign_r(result, result, std::max(curr_var_ub, curr_minus_var_ub), ROUND_UP); } - else if (curr_lb == -1 && curr_ub == 1) { + else if (curr_lb == -1 && curr_ub == -1) { neg_assign_r(negator, std::min(curr_var_ub, curr_minus_var_ub), ROUND_NOT_NEEDED); add_assign_r(result, result, negator, ROUND_UP);

1 0

[GIT] ppl/ppl(floating_point): Fixed an error introduced by previous commit .
by Fabio Bossi 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 992d25ba23f3660bb462276ed5f921743179a4bf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=992d25ba23f3… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 14 17:06:20 2009 +0200 Fixed an error introduced by previous commit. --- src/Linear_Form.templates.hh | 10 +++++----- 1 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index db09aaf..fc7e81e 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -58,7 +58,7 @@ Linear_Form<C>::Linear_Form(const Variable v, const Variable w) vec.resize(space_dim+1, zero); if (v_space_dim != w_space_dim) { vec[v_space_dim] = static_cast<C>(1.0); - vec[w_space_dim] = -static_cast<C>(1.0); + vec[w_space_dim] = static_cast<C>(-1.0); } } @@ -385,18 +385,18 @@ IO_Operators::operator<<(std::ostream& s, const Linear_Form<C>& f) { const C& fv = f[v+1]; if (fv != 0) { if (first) { - if (fv == -static_cast<C>(1.0)) + if (fv == 1.0) s << "-"; - else if (fv != static_cast<C>(1.0)) + else if (fv != 1.0) s << fv << "*"; first = false; } else { - if (fv == -static_cast<C>(1.0)) + if (fv == -1.0) s << " - "; else { s << " + "; - if (fv != static_cast<C>(1.0)) + if (fv != 1.0) s << fv << "*"; } }

1 0

[GIT] ppl/ppl(pip): Implemented the first steps of the parametric simplex algorithm.
by François Galea 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: pip Commit: 41ead44c160d6d940db2844baae95db469a68beb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=41ead44c160d… Author: François Galea <francois.galea(a)uvsq.fr> Date: Mon Sep 14 17:32:25 2009 +0200 Implemented the first steps of the parametric simplex algorithm. --- src/PIP_Tree.cc | 129 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 files changed, 127 insertions(+), 2 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index c43715e..173d39f 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -467,8 +467,133 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, } PIP_Problem_Status -PIP_Solution_Node::solve(PIP_Tree_Node** /* parent_ref */, - const Constraint_System& /* context */) { +PIP_Solution_Node::solve(PIP_Tree_Node** parent_ref, + const Matrix& ctx) { + Matrix context(ctx); + merge_assign(context, constraints_); + const dimension_type n_a_d = not_a_dimension(); + + // Main loop of the simplex algorithm + for(;;) { + dimension_type i; + dimension_type i_ = n_a_d; + dimension_type i__ = n_a_d; + dimension_type num_rows = tableau.t.num_rows(); + dimension_type num_vars = tableau.s.num_columns(); + dimension_type num_params = tableau.t.num_columns(); + Row_Sign s; + + for (i=0; i<num_rows; ++i) { + Row_Sign s = sign[i]; + if (s == UNKNOWN) { + s = row_sign(tableau.t[i]); + sign[i] = s; + } + /* Locate first row with negative parameter row */ + if (s == NEGATIVE && i_ == n_a_d) + i_ = i; + /* Locate first row with unknown-signed parameter row */ + if (s == MIXED && i__ == n_a_d) + i__ = i; + } + + /* If no negative parameter row found, try to refine the sign of + undetermined rows using compatibility checks with the current context + */ + if (i_ == n_a_d && i__ != n_a_d) { + for (i=i__; i<num_rows; ++i) { + if (sign[i] != MIXED) + continue; + s = ZERO; + if (compatibility_check(context, tableau.t[i])) + // constraint t_i(z) >= 0 is compatible with the context + s = POSITIVE; + Row c(num_params, Row::Flags()); + negate_assign(c, tableau.t[i]); + if (compatibility_check(context, c)) { + // constraint t_i(z) < 0 <=> -t_i(z)-1 >= 0 is compatible + if (s == POSITIVE) + s = MIXED; + else + s = NEGATIVE; + } + if (s == NEGATIVE && i_ == n_a_d) + // first negative row found + i_ = i; + if (s != MIXED) { + // clear first mixed-sign row index if row is found to be not mixed + if (i == i__) + i__ = n_a_d; + } else if (i__ == n_a_d) + // first mixed-sign row found + i__ = i; + sign[i] = s; + } + } + + /* If we have found a row i_ with negative parameters : + Either the problem is empty, or a pivoting step is required + */ + if (i_ != n_a_d) { +#if NOISY_PIP + std::cout << "Found row with negative parameters: " << i_ + << std::endl; +#endif + dimension_type j; + Coefficient z(0); + Coefficient sij, cij, cij_; + Coefficient c; + Row &row = tableau.s[i_]; + /* Look for a positive S_ij such as the j^th column/S_ij is + lexico-minimal + */ + dimension_type j_ = n_a_d; + for (j=0; j<num_vars; ++j) { + if (row[j] > 0) { + if (j_ == n_a_d) { + j_ = j; + sij = row[j]; + } else { + /* Determine which column (j or j_) is lexico-minimal */ + dimension_type k = 0; + do { + dimension_type mk = mapping[k]; + if (basis[k]) { + /* reconstitute the identity submatrix part of S */ + cij = (mk==j) ? tableau.s.get_denominator() : 0; + cij_ = (mk==j_) ? tableau.s.get_denominator() : 0; + } else { + cij = tableau.s[mk][j]; + cij_ = tableau.s[mk][j_]; + } + } while (k < num_vars && cij * sij == cij_ * row[j]); + if (k < num_vars && cij * sij < cij_ * row[j]) { + j_ = j; + sij = row[j]; + } + } + } + } + + /* If no positive S_ij: problem is empty */ + if (j_ == n_a_d) { +#if NOISY_PIP + std::cout << "No positive pivot found: Solution = _|_" + << std::endl; +#endif + *parent_ref = 0; + delete this; + return UNFEASIBLE_PIP_PROBLEM; + } +#if NOISY_PIP + std::cout << "Pivot column: " << j_ + << std::endl; +#endif + + } + + } // Main loop of the simplex algorithm + //FIXME return OPTIMIZED_PIP_PROBLEM; }

1 0

[GIT] ppl/ppl(pip): Changed modelization of contexts from Constraint_System to Matrix.
by François Galea 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: pip Commit: e8b3c7c191b3abc667676f0dc00fcf15af5b9bb5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e8b3c7c191b3… Author: François Galea <francois.galea(a)uvsq.fr> Date: Mon Sep 14 13:13:27 2009 +0200 Changed modelization of contexts from Constraint_System to Matrix. --- src/PIP_Problem.cc | 2 +- src/PIP_Tree.cc | 43 ++++++++++++++++++++++++++++--------------- src/PIP_Tree.defs.hh | 6 +++--- 3 files changed, 32 insertions(+), 19 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index 86777f5..34affcd 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -85,7 +85,7 @@ PPL::PIP_Problem::solve() const { input_cs, parameters); - Constraint_System initial_context; + Matrix initial_context(0, parameters.size()+1); return_value = x.current_solution->solve(&x.current_solution, initial_context); diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index b7948f5..c43715e 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -37,12 +37,29 @@ add_assign(Row& x, const Row& y, Coefficient_traits::const_reference c) { add_mul_assign(x[i], c, y[i]); } -// Merge constraint systems such as x = x U y +// Merge constraint system to a Matrix-form context such as x = x U y void -merge_assign(Constraint_System& x, const Constraint_System& y) { +merge_assign(Matrix& x, const Constraint_System& y) { + dimension_type width = x.num_columns(); + PPL_ASSERT(y.empty() || y.begin()->space_dimension() == width-1); + Row row(width, Row::Flags()); for (Constraint_System::const_iterator y_i = y.begin(), - y_end = y.end(); y_i != y_end; ++y_i) - x.insert(*y_i); + y_end = y.end(); y_i != y_end; ++y_i) { + PPL_ASSERT(y_i->is_nonstrict_inequality()); + for (dimension_type j=width-1; j-- > 0; ) + row[j+1] = y_i->coefficient(Variable(j)); + row[0] = -y_i->inhomogeneous_term(); + x.add_row(row); + } +} + +// Tranform expression "expr" into "-expr-1" +void +negate_assign(Row& x, const Row& y) { + PPL_ASSERT(x.size() == y.size()); + for (dimension_type i = x.size(); i-- > 0; ) + x[i] = -y[i]; + x[0] -= 1; } } // namespace @@ -204,24 +221,20 @@ PIP_Decision_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, } PIP_Problem_Status -PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref, - const Constraint_System& context) { +PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref, const Matrix& context) { PIP_Problem_Status return_status; PIP_Problem_Status stt; PIP_Problem_Status stf = UNFEASIBLE_PIP_PROBLEM; - Constraint_System context_true(context); + Matrix context_true(context); merge_assign(context_true, constraints_); stt = true_child->solve(&true_child, context_true); if (false_child) { // Decision nodes with false child must have exactly one constraint PPL_ASSERT(1 == std::distance(constraints_.begin(), constraints_.end())); - Constraint_System context_false(context); - Constraint_System::const_iterator ci = constraints_.begin(); - PPL_ASSERT(ci->is_nonstrict_inequality()); - Linear_Expression expr = Linear_Expression(*ci); - expr += 1; - Constraint c(expr <= 0); - context_false.insert(c); + Matrix context_false(context); + merge_assign(context_false, constraints_); + Row &last = context_false[context_false.num_rows()-1]; + negate_assign(last, last); stf = false_child->solve(&false_child, context_false); } @@ -326,7 +339,7 @@ PIP_Solution_Node::compatibility_check(const Matrix &ctx, const Row &cnst) { dimension_type num_cols = s.num_columns(); bool result = false; - /* Perform nonparametric simplex pivots until we find an empty solution + /* Perform simplex pivots on the context until we find an empty solution * or an optimum */ for(;;) { // Look for a negative RHS (=constant term, stored in matrix column 0) diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 5393c02..c8b2a16 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -121,7 +121,7 @@ protected: attempt (unfeasible or optimized problem). */ virtual PIP_Problem_Status solve(PIP_Tree_Node **parent_ref, - const Constraint_System& context) = 0; + const Matrix& context) = 0; }; //! A tree node representing part of the space of solutions. @@ -308,7 +308,7 @@ protected: attempt (unfeasible or optimized problem). */ virtual PIP_Problem_Status solve(PIP_Tree_Node **parent_ref, - const Constraint_System& context); + const Matrix& context); // FIXME: constructors to be decided. }; @@ -415,7 +415,7 @@ protected: attempt (unfeasible or optimized problem). */ virtual PIP_Problem_Status solve(PIP_Tree_Node **parent_ref, - const Constraint_System& context); + const Matrix& context); }; typedef const PIP_Tree_Node* PIP_Tree;

1 0

[GIT] ppl/ppl(floating_point): Added missing static_casts in Linear_Form.
by Fabio Bossi 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 9e8267747161ddd33e7092ade570cbaf2e1529bd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9e8267747161… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 14 16:02:12 2009 +0200 Added missing static_casts in Linear_Form. Fixed one bug in linear_form_upper_bound. Added a first complete implementation of affine_image. --- src/Linear_Form.templates.hh | 24 ++++++------ src/Octagonal_Shape.defs.hh | 1 - src/Octagonal_Shape.templates.hh | 71 ++++++++++++++++++++++++++++++------- 3 files changed, 69 insertions(+), 27 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index 335207f..db09aaf 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -40,7 +40,7 @@ Linear_Form<C>::Linear_Form(const Variable v) "space dimension."); vec.reserve(compute_capacity(space_dim+1, vec_type().max_size())); vec.resize(space_dim+1, zero); - vec[v.space_dimension()] = 1.0; + vec[v.space_dimension()] = static_cast<C>(1.0); } template <typename C> @@ -57,8 +57,8 @@ Linear_Form<C>::Linear_Form(const Variable v, const Variable w) vec.reserve(compute_capacity(space_dim+1, vec_type().max_size())); vec.resize(space_dim+1, zero); if (v_space_dim != w_space_dim) { - vec[v_space_dim] = 1.0; - vec[w_space_dim] = -1.0; + vec[v_space_dim] = static_cast<C>(1.0); + vec[w_space_dim] = -static_cast<C>(1.0); } } @@ -125,7 +125,7 @@ operator+(const Variable v, const Linear_Form<C>& f) { Linear_Form<C> r(f); if (v_space_dim > f.space_dimension()) r.extend(v_space_dim+1); - r[v_space_dim] += 1.0; + r[v_space_dim] += static_cast<C>(1.0); return r; } @@ -199,7 +199,7 @@ operator-(const Variable v, const Linear_Form<C>& f) { r.extend(v_space_dim+1); for (dimension_type i = f.size(); i-- > 0; ) r[i].neg_assign(r[i]); - r[v_space_dim] += 1.0; + r[v_space_dim] += static_cast<C>(1.0); return r; } @@ -216,7 +216,7 @@ operator-(const Linear_Form<C>& f, const Variable v) { Linear_Form<C> r(f); if (v_space_dim > f.space_dimension()) r.extend(v_space_dim+1); - r[v_space_dim] -= 1.0; + r[v_space_dim] -= static_cast<C>(1.0); return r; } @@ -266,7 +266,7 @@ operator+=(Linear_Form<C>& f, const Variable v) { "v exceeds the maximum allowed space dimension."); if (v_space_dim > f.space_dimension()) f.extend(v_space_dim+1); - f[v_space_dim] += 1.0; + f[v_space_dim] += static_cast<C>(1.0); return f; } @@ -294,7 +294,7 @@ operator-=(Linear_Form<C>& f, const Variable v) { "v exceeds the maximum allowed space dimension."); if (v_space_dim > f.space_dimension()) f.extend(v_space_dim+1); - f[v_space_dim] -= 1.0; + f[v_space_dim] -= static_cast<C>(1.0); return f; } @@ -385,18 +385,18 @@ IO_Operators::operator<<(std::ostream& s, const Linear_Form<C>& f) { const C& fv = f[v+1]; if (fv != 0) { if (first) { - if (fv == -1.0) + if (fv == -static_cast<C>(1.0)) s << "-"; - else if (fv != 1.0) + else if (fv != static_cast<C>(1.0)) s << fv << "*"; first = false; } else { - if (fv == -1.0) + if (fv == -static_cast<C>(1.0)) s << " - "; else { s << " + "; - if (fv != 1.0) + if (fv != static_cast<C>(1.0)) s << fv << "*"; } } diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 3bb7cd1..ab89bcd 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1795,7 +1795,6 @@ private: template <typename Interval_Info> void linear_form_upper_bound( const Linear_Form< Interval<T, Interval_Info> >& lf, - const dimension_type last_coefficient, N& result) const; // FIXME: the name is questionable. diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 54c8e59..783fcfb 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4867,22 +4867,65 @@ Octagonal_Shape<T>::affine_image(Variable var, // expr == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, // or t == 1, expr == i*w + b, but i <> [+/-1;+/-1]. - // Calculate upper bounds for lf, -lf, lf + var, lf - var, - // var - lf, - lf - var. + // In the following, strong closure will be definitely lost. + reset_strongly_closed(); + + Linear_Form<FP_Interval_Type> minus_lf(-lf); + PPL_DIRTY_TEMP(N, lf_ub); - assign_r(lf_ub, b_ub, ROUND_NOT_NEEDED); + linear_form_upper_bound(lf, lf_ub); PPL_DIRTY_TEMP(N, minus_lf_ub); - assign_r(minus_lf_ub, b_mlb, ROUND_NOT_NEEDED); + linear_form_upper_bound(minus_lf, minus_lf_ub); + + // Update unary constraints on var. + mul_2exp_assign_r(lf_ub, lf_ub, 1, ROUND_IGNORE); + assign_r(matrix[n_var+1][n_var], lf_ub, ROUND_NOT_NEEDED); + mul_2exp_assign_r(minus_lf_ub, minus_lf_ub, 1, ROUND_IGNORE); + assign_r(matrix[n_var][n_var+1], minus_lf_ub, ROUND_NOT_NEEDED); + + // Declare temporaries outside the loop. PPL_DIRTY_TEMP(N, lf_plus_var_ub); - assign_r(lf_plus_var_ub, b_ub, ROUND_NOT_NEEDED); PPL_DIRTY_TEMP(N, lf_minus_var_ub); - assign_r(lf_minus_var_ub, b_ub, ROUND_NOT_NEEDED); PPL_DIRTY_TEMP(N, var_minus_lf_ub); - assign_r(var_minus_lf_ub, b_mlb, ROUND_NOT_NEEDED); PPL_DIRTY_TEMP(N, minus_lf_minus_var_ub); - assign_r(minus_lf_minus_var_ub, b_mlb, ROUND_NOT_NEEDED); - linear_form_upper_bound(lf, w_id, lf_ub); + Row_Iterator m_iter = matrix.row_begin(); + m_iter += n_var; + Row_Reference var_ite = *m_iter; + ++m_iter; + Row_Reference var_cv_ite = *m_iter; + ++m_iter; + Row_Iterator m_end = matrix.row_end(); + + // Update binary constraints on var. + for (dimension_type curr_var = var_id, n_curr_var = n_var - 2; + curr_var-- > 0; ) { + Variable current(curr_var); + linear_form_upper_bound(lf + current, lf_plus_var_ub); + linear_form_upper_bound(lf - current, lf_minus_var_ub); + linear_form_upper_bound(minus_lf + current, var_minus_lf_ub); + linear_form_upper_bound(minus_lf - current, minus_lf_minus_var_ub); + assign_r(var_ite[n_curr_var], var_minus_lf_ub, ROUND_NOT_NEEDED); + assign_r(var_ite[n_curr_var+1], minus_lf_minus_var_ub, ROUND_NOT_NEEDED); + assign_r(var_cv_ite[n_curr_var], lf_plus_var_ub, ROUND_NOT_NEEDED); + assign_r(var_cv_ite[n_curr_var+1], lf_minus_var_ub, ROUND_NOT_NEEDED); + n_curr_var -= 2; + } + for (dimension_type curr_var = var_id+1; m_iter != m_end; ++m_iter) { + Row_Reference m_v_ite = *m_iter; + ++m_iter; + Row_Reference m_cv_ite = *m_iter; + Variable current(curr_var); + linear_form_upper_bound(lf + current, lf_plus_var_ub); + linear_form_upper_bound(lf - current, lf_minus_var_ub); + linear_form_upper_bound(minus_lf + current, var_minus_lf_ub); + linear_form_upper_bound(minus_lf - current, minus_lf_minus_var_ub); + assign_r(m_v_ite[n_var], lf_minus_var_ub, ROUND_NOT_NEEDED); + assign_r(m_v_ite[n_var+1], minus_lf_minus_var_ub, ROUND_NOT_NEEDED); + assign_r(m_cv_ite[n_var], lf_plus_var_ub, ROUND_NOT_NEEDED); + assign_r(m_cv_ite[n_var+1], var_minus_lf_ub, ROUND_NOT_NEEDED); + ++curr_var; + } } @@ -4891,10 +4934,7 @@ template <typename Interval_Info> void Octagonal_Shape<T>:: linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, - const dimension_type last_coefficient, N& result) const { - PPL_ASSERT(last_coefficient < lf.space_dimension()); - /* FIXME: this way for checking that T is a floating point type is a bit unelengant. @@ -4902,7 +4942,10 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, // Check that T is a floating point type. PPL_ASSERT(std::numeric_limits<T>::max_exponent); + const dimension_type lf_space_dimension = lf.space_dimension(); + typedef Interval<T, Interval_Info> FP_Interval_Type; + const FP_Interval_Type* curr_coefficient; PPL_DIRTY_TEMP(N, curr_lb); PPL_DIRTY_TEMP(N, curr_ub); @@ -4916,9 +4959,9 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, PPL_DIRTY_TEMP(N, negator); - assign_r(result, 0, ROUND_NOT_NEEDED); + assign_r(result, lf.inhomogeneous_term().upper(), ROUND_NOT_NEEDED); - for (dimension_type curr_var = 0, n_var = 0; curr_var <= last_coefficient; + for (dimension_type curr_var = 0, n_var = 0; curr_var < lf_space_dimension; ++curr_var) { curr_coefficient = &(lf.coefficient(Variable(curr_var))); assign_r(curr_lb, curr_coefficient->lower(), ROUND_NOT_NEEDED);

1 0

[GIT] ppl/ppl(floating_point): Added another helper function.
by Fabio Bossi 14 Sep '09

14 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 47bf5799b4b5c216f4b176a8cad2d223095383c1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=47bf5799b4b5… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 14 12:16:04 2009 +0200 Added another helper function. Removed garbage code. --- src/Octagonal_Shape.defs.hh | 6 ++ src/Octagonal_Shape.templates.hh | 186 +++++++++++++++----------------------- 2 files changed, 81 insertions(+), 111 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=47bf5799…

1 0

[GIT] ppl/ppl(floating_point): Added an auxiliary method.
by Fabio Bossi 13 Sep '09

13 Sep '09

Module: ppl/ppl Branch: floating_point Commit: b3262f50a53d3b90d13dd43d74c10b30ba6a4ced URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b3262f50a53d… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sun Sep 13 19:21:41 2009 +0200 Added an auxiliary method. Sorry for the huge amount of commented code: it will be fixed soon. --- src/Octagonal_Shape.defs.hh | 6 ++ src/Octagonal_Shape.templates.hh | 179 ++++++++++++++++++++++++++++++++++++-- 2 files changed, 178 insertions(+), 7 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 4035b35..5e86819 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1792,6 +1792,12 @@ private: N& matrix_at(dimension_type i, dimension_type j); const N& matrix_at(dimension_type i, dimension_type j) const; + // FIXME: the name is questionable. + static void interval_coefficient_upper_bound(const N& var_ub, + const N& minus_var_ub, + const N& int_ub, const N& int_lb, + N& result); + /*! \brief Uses the constraint \p c to refine \p *this. diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index fa61f15..f78b969 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -4757,14 +4757,10 @@ Octagonal_Shape<T>::affine_image(Variable var, if (t == 1) { // The one and only non-zero homogeneous coefficient in `lf'. const FP_Interval_Type& w_coeff = lf.coefficient(Variable(w_id)); - PPL_DIRTY_TEMP(N, w_coeff_lb); - PPL_DIRTY_TEMP(N, w_coeff_ub); - assign_r(w_coeff_lb, w_coeff.lower(), ROUND_NOT_NEEDED); - assign_r(w_coeff_ub, w_coeff.upper(), ROUND_NOT_NEEDED); // true if w_coeff = [1;1]. - bool is_w_coeff_one = (w_coeff_lb == 1 && w_coeff_ub == 1); + bool is_w_coeff_one = (w_coeff == 1); // true if w_coeff = [-1;-1]. - bool is_w_coeff_minus_one = (w_coeff_lb == -1 && w_coeff_ub == -1); + bool is_w_coeff_minus_one = (w_coeff == -1); if (is_w_coeff_one || is_w_coeff_minus_one) { // Case 2: lf = w_coeff*w + b, with w_coeff = [+/-1;+/-1]. if (w_id == var_id) { @@ -4871,7 +4867,176 @@ Octagonal_Shape<T>::affine_image(Variable var, // expr == i_1*x_1 + i_2*x_2 + ... + i_n*x_n + b, where n >= 2, // or t == 1, expr == i*w + b, but i <> [+/-1;+/-1]. - // FIXME: complete the implementation. + // Calculate upper bounds for lf, -lf, lf + var, lf - var, + // var - lf, - lf - var. + PPL_DIRTY_TEMP(N, lf_ub); + assign_r(lf_ub, b_ub, ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, minus_lf_ub); + assign_r(minus_lf_ub, b_mlb, ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, lf_plus_var_ub); + assign_r(lf_plus_var_ub, b_ub, ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, lf_minus_var_ub); + assign_r(lf_minus_var_ub, b_ub, ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, var_minus_lf_ub); + assign_r(var_minus_lf_ub, b_mlb, ROUND_NOT_NEEDED); + PPL_DIRTY_TEMP(N, minus_lf_minus_var_ub); + assign_r(minus_lf_minus_var_ub, b_mlb, ROUND_NOT_NEEDED); + + // FIXME: the commented part is WRONG. + /* + PPL_DIRTY_TEMP(N, l_curr); + PPL_DIRTY_TEMP(N, u_curr); + PPL_DIRTY_TEMP(N, u_var); + PPL_DIRTY_TEMP(N, u_minus_var); + PPL_DIRTY_TEMP(N, first_comparison_term); + PPL_DIRTY_TEMP(N, second_comparison_term); + PPL_DIRTY_TEMP(N, third_comparison_term); + PPL_DIRTY_TEMP(N, fourth_comparison_term); + + for (dimension_type curr_var = 0, n_curr_var = 0; + curr_var <= w_id; ++curr_var) { + FP_Interval_Type curr_coeff = lf.coefficient(i); + assign_r(l_curr, curr_coeff.lower(), ROUND_NOT_NEEDED); + assign_r(u_curr, curr_coeff.upper(), ROUND_NOT_NEEDED); + if (curr_var == var) { + // This is the case where we need special treatment for + // the upper bounds of quantities that contain var. + + // Upper bound for var. + assign_r(u_var, matrix[n_curr_var+1][n_curr_var], ROUND_NOT_NEEDED); + // -Upper bound for -var. + neg_assign_r(u_minus_var, matrix[n_curr_var][n_curr_var + 1], + ROUND_NOT_NEEDED); + + // FIXME: implement this case. + + } + else if (l_curr != 0 && u_curr != 0) { + // Here we treat the upper bounds of quantities that contain var + // in the same way as those who don't. + + // Upper bound for curr_var. + assign_r(u_var, matrix[n_curr_var+1][n_curr_var], ROUND_NOT_NEEDED); + // -Upper bound for -curr_var. + neg_assign_r(u_minus_var, matrix[n_curr_var][n_curr_var + 1], + ROUND_NOT_NEEDED); + + // Now compute the next addend for upper bounds of linear forms + // that contain +lf. + + // FIXME: this should probably be done in a separate function. + // Next addend will be the maximum of these four products. + assign_r(first_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(first_comparison_term, u_var, u_curr, ROUND_UP); + add_mul_assign_r(second_comparison_term, u_minus_var, u_curr, ROUND_UP); + add_mul_assign_r(third_comparison_term, u_var, l_curr, ROUND_UP); + add_mul_assign_r(fourth_comparison_term, u_minus_var, l_curr, ROUND_UP); + + // NOTE: next addend will be stored in first_comparison_term + // to avoid temporaries. + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + assign_r(first_comparison_term, std::max(first_comparison_term, + third_comparison_term), + ROUND_NOT_NEEDED); + assign_r(first_comparison_term, std::max(first_comparison_term, + fourth_comparison_term), + ROUND_NOT_NEEDED); + + // Now add the next addend to all upper bounds. + add_assign_r(lf_ub, lf_ub, first_comparison_term, ROUND_UP); + add_assign_r(lf_plus_var_ub, lf_plus_var_ub, first_comparison_term, + ROUND_UP); + add_assign_r(lf_minus_var_ub, lf_minus_var_ub, first_comparison_term, + ROUND_UP); + + // Now compute the next addend for upper bounds of linear forms + // that contain -lf. + neg_assign_r(l_curr, l_curr, ROUND_NOT_NEEDED); + neg_assign_r(u_curr, u_curr, ROUND_NOT_NEEDED); + // NOTE: now l_curr > u_curr! + + // FIXME: this should probably be done in a separate function. + // Next addend will be the maximum of these four products. + assign_r(first_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); + add_mul_assign_r(first_comparison_term, u_var, l_curr, ROUND_UP); + add_mul_assign_r(second_comparison_term, u_minus_var, l_curr, ROUND_UP); + add_mul_assign_r(third_comparison_term, u_var, u_curr, ROUND_UP); + add_mul_assign_r(fourth_comparison_term, u_minus_var, u_curr, ROUND_UP); + + // NOTE: next addend will be stored in first_comparison_term + // to avoid temporaries. + assign_r(first_comparison_term, std::max(first_comparison_term, + second_comparison_term), + ROUND_NOT_NEEDED); + assign_r(first_comparison_term, std::max(first_comparison_term, + third_comparison_term), + ROUND_NOT_NEEDED); + assign_r(first_comparison_term, std::max(first_comparison_term, + fourth_comparison_term), + ROUND_NOT_NEEDED); + + // Now add the next addend to all upper bounds. + add_assign_r(minus_lf_ub, minus_lf_ub, first_comparison_term, ROUND_UP); + add_assign_r(var_minus_lf_ub, var_minus_lf_ub, first_comparison_term, + ROUND_UP); + add_assign_r(minus_lf_minus_var_ub, minus_lf_minus_var_ub, + first_comparison_term, ROUND_UP); + + } + } + + // In the following, strong closure will be definitely lost. + reset_strongly_closed(); + + // Now update all constraints on var. + Row_Iterator m_iter = matrix.row_begin() + n_var; + Row_Reference m_i = (*m_iter); + ++m_iter; + Row_Reference m_ci = (*m_iter); + // First + */ + +} + +template <typename T> +void +Octagonal_Shape<T>:: +interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, + const N& int_ub, const N& int_lb, + N& result) { + /* + FIXME: this way for checking that T is a floating point type is a bit + unelengant. + */ + // Check that T is a floating point type. + PPL_ASSERT(std::numeric_limits<T>::max_exponent); + + // NOTE: we store the first comparison term directly into result. + PPL_DIRTY_TEMP(N, second_comparison_term); + PPL_DIRTY_TEMP(N, third_comparison_term); + PPL_DIRTY_TEMP(N, fourth_comparison_term); + + assign_r(result, 0, ROUND_NOT_NEEDED); + assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); + assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); + + add_mul_assign_r(result, var_ub, int_ub, ROUND_UP); + add_mul_assign_r(second_comparison_term, minus_var_ub, int_ub, ROUND_UP); + add_mul_assign_r(third_comparison_term, var_ub, int_lb, ROUND_UP); + add_mul_assign_r(fourth_comparison_term, minus_var_ub, int_lb, ROUND_UP); + + assign_r(result, std::max(result, second_comparison_term), ROUND_NOT_NEEDED); + assign_r(result, std::max(result, third_comparison_term), ROUND_NOT_NEEDED); + assign_r(result, std::max(result, fourth_comparison_term), ROUND_NOT_NEEDED); }

1 0

[GIT] ppl/ppl(master): Do not include <stdint.h>.
by Roberto Bagnara 11 Sep '09

11 Sep '09

Module: ppl/ppl Branch: master Commit: 04affbe1f914df631a682bf661b86232023c6d4e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=04affbe1f914… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Sep 11 22:28:09 2009 +0200 Do not include <stdint.h>. The header files <stdint.h> and/or <inttypes.h> are included by ppl-config.h. --- interfaces/marked_pointers.hh | 2 -- 1 files changed, 0 insertions(+), 2 deletions(-) diff --git a/interfaces/marked_pointers.hh b/interfaces/marked_pointers.hh index 2ba6f6b..e9e534f 100644 --- a/interfaces/marked_pointers.hh +++ b/interfaces/marked_pointers.hh @@ -26,8 +26,6 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace Parma_Polyhedra_Library { -#include <stdint.h> - #define PPL_MARKED_POINTERS_MASK ((uintptr_t) 1) /*! \brief

1 0