May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Another efficiency improvement to wrap_assign().
by Patricia Hill 12 May '09

12 May '09

Module: ppl/ppl Branch: master Commit: c39276dbadd94769a711940fd0694561aedb0c06 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c39276dbadd9… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue May 12 16:51:46 2009 +0100 Another efficiency improvement to wrap_assign(). --- src/Grid_public.cc | 9 +++++---- 1 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Grid_public.cc b/src/Grid_public.cc index 0fae952..677859d 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2761,10 +2761,11 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // may take any integer within the range of the bounded integer type. PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); const Grid_Generator& point = gen_sys[0]; - Coefficient& div_x = wrap_frequency; - div_x = point.divisor(); + const Coefficient& div = point.divisor(); + max_value *= div; + min_value *= div; for (Variables_Set::const_iterator i = vars.begin(), - vars_end = vars.end(); i != vars.end(); ++i) { + vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); if (!gr.bounds_no_check(x)) { // `x' is not a constant in `gr'. @@ -2778,7 +2779,7 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // If the value `v' for `x' is not within the range for the // bounded integer type, then `x' may wrap to any value `v + z' // where `z' is an integer; otherwise `x' is unchanged. - if (coeff_x > max_value * div_x || coeff_x < min_value * div_x) { + if (coeff_x > max_value || coeff_x < min_value) { add_grid_generator(parameter(x)); } }

1 0

[GIT] ppl/ppl(master): Some efficiency improvements. Comments improved.
by Patricia Hill 12 May '09

12 May '09

Module: ppl/ppl Branch: master Commit: eb54ad2e7508d44ada8ef80161f416e5ec9f48a2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eb54ad2e7508… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue May 12 16:42:06 2009 +0100 Some efficiency improvements. Comments improved. --- src/Grid_public.cc | 38 +++++++++++++++++++++----------------- 1 files changed, 21 insertions(+), 17 deletions(-) diff --git a/src/Grid_public.cc b/src/Grid_public.cc index 498e8a7..0fae952 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2700,13 +2700,13 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, PPL_DIRTY_TEMP_COEFFICIENT(f_d); PPL_DIRTY_TEMP_COEFFICIENT(v_n); PPL_DIRTY_TEMP_COEFFICIENT(v_d); - PPL_DIRTY_TEMP_COEFFICIENT(f); for (Variables_Set::const_iterator i = vars.begin(), - vars_end = vars.end(); i != vars.end(); ++i) { + vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); if (!gr.frequency_no_check(x, f_n, f_d, v_n, v_d)) continue; if (f_n == 0) { + // `x' is a constant in `gr'. if ((v_n > max_value * v_d) || (v_n < min_value * v_d)) { // The value is outside the range of the bounded integer type. @@ -2717,16 +2717,18 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, } assert(o == OVERFLOW_WRAPS); // The value v_n for `x' is wrapped modulo the 'wrap_frequency'. - f = v_d * wrap_frequency; - v_n %= f; + Coefficient& wrap_modulus = f_n; + wrap_modulus = v_d * wrap_frequency; + v_n %= wrap_modulus; // `v_n' is the value closest to 0 and may be negative. if (s == UNSIGNED && v_n < 0) - v_n += f; + v_n += wrap_modulus; unconstrain(x); add_constraint(v_d * x == v_n); } continue; } + // `x' is not a constant in `gr'. if (2*f_n > f_d * wrap_frequency) { // If the grid frequency for `x' in `vars' is more than half the @@ -2737,18 +2739,19 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, v_n *= f_d; add_mul_assign(v_n, f_n, v_d); v_d *= f_d; - PPL_DIRTY_TEMP_COEFFICIENT(gcd); - gcd_assign(gcd, v_n, v_d); - exact_div_assign(v_n, v_n, gcd); - exact_div_assign(v_d, v_d, gcd); } add_constraint(v_d * x == v_n); } + else if (o == OVERFLOW_WRAPS) + // We know that `x' is not a constant, so, if overflow wraps, + // `x' may wrap to a value modulo the `wrap_frequency'. + add_grid_generator(parameter(wrap_frequency * x)); else - if (o == OVERFLOW_WRAPS) - // We know that `x' is not a constant, so `x' may wrap - // to a value modulo the `wrap_frequency'. - add_grid_generator(parameter(wrap_frequency * x)); + // If overflow is impossible but the grid frequency is no more than + // half the wrap frequency, then there is more than one possible + // value for `x' in the range of the bounded integer type, + // so the grid is unchanged. + assert(o == OVERFLOW_IMPOSSIBLE && 2*f_n <= f_d * wrap_frequency); } return; } @@ -2756,6 +2759,10 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, assert(o == OVERFLOW_UNDEFINED); // If overflow is undefined, then all we know is that the variable // may take any integer within the range of the bounded integer type. + PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); + const Grid_Generator& point = gen_sys[0]; + Coefficient& div_x = wrap_frequency; + div_x = point.divisor(); for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); @@ -2767,10 +2774,7 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, } else { // `x' is a constant `v' in `gr'. - PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); - PPL_DIRTY_TEMP_COEFFICIENT(div_x); - coeff_x = gen_sys[0].coefficient(x); - div_x = gen_sys[0].divisor(); + coeff_x = point.coefficient(x); // If the value `v' for `x' is not within the range for the // bounded integer type, then `x' may wrap to any value `v + z' // where `z' is an integer; otherwise `x' is unchanged.

1 0

[GIT] ppl/ppl(master): Updated from Gnulib.
by Roberto Bagnara 12 May '09

12 May '09

Module: ppl/ppl Branch: master Commit: e3460918400e04cf24fda33ff0cf9d18a95840b8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e3460918400e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue May 12 15:49:10 2009 +0200 Updated from Gnulib. --- m4/lib-ld.m4 | 14 +- m4/lib-link.m4 | 352 +++++++++++++++++++++++++++++++++++++++++++----------- m4/lib-prefix.m4 | 81 ++++++++++++- 3 files changed, 363 insertions(+), 84 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=e3460918…

1 0

[GIT] ppl/ppl(master): Simplification and improvement of code for wrap_assign().
by Patricia Hill 12 May '09

12 May '09

Module: ppl/ppl Branch: master Commit: 4615f0d711d1623c1237b697bb07fda99d995ca7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4615f0d711d1… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue May 12 14:19:04 2009 +0100 Simplification and improvement of code for wrap_assign(). The bounds_no_check() and frequency_no_check() assume the generators are minimized and the grid is not empty. --- src/Grid.defs.hh | 6 ++- src/Grid_nonpublic.cc | 7 +-- src/Grid_public.cc | 135 +++++++++++++++++++++--------------------------- 3 files changed, 64 insertions(+), 84 deletions(-) diff --git a/src/Grid.defs.hh b/src/Grid.defs.hh index b8b37ee..3049c31 100644 --- a/src/Grid.defs.hh +++ b/src/Grid.defs.hh @@ -2161,7 +2161,8 @@ private: \warning If \p expr and \p *this are dimension-incompatible, - then the behavior is undefined. + the grid generator system is not minimized or \p *this is + empty, then the behavior is undefined. */ bool frequency_no_check(const Linear_Expression& expr, Coefficient& freq_n, Coefficient& freq_d, @@ -2184,7 +2185,8 @@ private: \warning If \p cg and \p *this are dimension-incompatible, - the behavior is undefined. + the grid generator system is not minimized or \p *this is + empty, then the behavior is undefined. */ void add_congruence_no_check(const Congruence& cg); diff --git a/src/Grid_nonpublic.cc b/src/Grid_nonpublic.cc index 214948c..be5e512 100644 --- a/src/Grid_nonpublic.cc +++ b/src/Grid_nonpublic.cc @@ -317,12 +317,7 @@ PPL::Grid::frequency_no_check(const Linear_Expression& expr, // The dimension of `expr' must be at most the dimension of *this. assert(space_dim >= expr.space_dimension()); - - // The frequency is undefined if the grid is empty; return false. - if (marked_empty()) - return false; - if (!generators_are_minimized() && !minimize()) - return false; + assert(generators_are_minimized() && !marked_empty()); // The generators are up to date and minimized and the grid is non-empty. diff --git a/src/Grid_public.cc b/src/Grid_public.cc index 8d54946..498e8a7 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2641,16 +2641,16 @@ PPL::Grid::external_memory_in_bytes() const { void PPL::Grid::wrap_assign(const Variables_Set& vars, - Bounded_Integer_Type_Width w, - Bounded_Integer_Type_Signedness s, - Bounded_Integer_Type_Overflow o, - const Constraint_System* pcs, - unsigned, - bool) { + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Signedness s, + Bounded_Integer_Type_Overflow o, + const Constraint_System* pcs, + unsigned, + bool) { // Dimension-compatibility check of `*pcs', if any. if (pcs != 0) { - const dimension_type pcs_space_dim = pcs->space_dimension(); + const dimension_type pcs_space_dim = pcs->space_dimension(); if (pcs->space_dimension() != space_dim) throw_dimension_incompatible("wrap_assign(vs, ...)", pcs_space_dim); } @@ -2694,112 +2694,95 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // Generators are up-to-date and minimized. const Grid gr = *this; - // Overflow is impossible. So check if value might become constant. - if (o == OVERFLOW_IMPOSSIBLE) { + // Overflow is impossible or wraps. + if (o == OVERFLOW_IMPOSSIBLE || o == OVERFLOW_WRAPS) { PPL_DIRTY_TEMP_COEFFICIENT(f_n); PPL_DIRTY_TEMP_COEFFICIENT(f_d); PPL_DIRTY_TEMP_COEFFICIENT(v_n); PPL_DIRTY_TEMP_COEFFICIENT(v_d); + PPL_DIRTY_TEMP_COEFFICIENT(f); for (Variables_Set::const_iterator i = vars.begin(), - vars_end = vars.end(); i != vars.end(); ++i) { + vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If the grid frequency for `x' in `vars' is more than half the - // `wrap_frequency', then `x' can only take a unique (ie constant) - // value. if (!gr.frequency_no_check(x, f_n, f_d, v_n, v_d)) continue; if (f_n == 0) { // `x' is a constant in `gr'. if ((v_n > max_value * v_d) || (v_n < min_value * v_d)) { - // If the value is outside the range of the bounded integer type, - // then `x' has no possible value and hence `gr' is set empty. - set_empty(); - return; + // The value is outside the range of the bounded integer type. + if (o == OVERFLOW_IMPOSSIBLE) { + // Then `x' has no possible value and hence `gr' is set empty. + set_empty(); + return; + } + assert(o == OVERFLOW_WRAPS); + // The value v_n for `x' is wrapped modulo the 'wrap_frequency'. + f = v_d * wrap_frequency; + v_n %= f; + // `v_n' is the value closest to 0 and may be negative. + if (s == UNSIGNED && v_n < 0) + v_n += f; + unconstrain(x); + add_constraint(v_d * x == v_n); } + continue; } + // `x' is not a constant in `gr'. if (2*f_n > f_d * wrap_frequency) { - if (s == UNSIGNED) { + // If the grid frequency for `x' in `vars' is more than half the + // `wrap_frequency', then `x' can only take a unique (ie constant) + // value. + if (s == UNSIGNED && v_n < 0) { // `v_n' is the value closest to 0 and may be negative. - if (v_n < 0) { - v_n *= f_d; - add_mul_assign(v_n, f_n, v_d); - v_d *= f_d; - PPL_DIRTY_TEMP_COEFFICIENT(gcd); - gcd_assign(gcd, v_n, v_d); - exact_div_assign(v_n, v_n, gcd); - exact_div_assign(v_d, v_d, gcd); - } + v_n *= f_d; + add_mul_assign(v_n, f_n, v_d); + v_d *= f_d; + PPL_DIRTY_TEMP_COEFFICIENT(gcd); + gcd_assign(gcd, v_n, v_d); + exact_div_assign(v_n, v_n, gcd); + exact_div_assign(v_d, v_d, gcd); } add_constraint(v_d * x == v_n); } + else + if (o == OVERFLOW_WRAPS) + // We know that `x' is not a constant, so `x' may wrap + // to a value modulo the `wrap_frequency'. + add_grid_generator(parameter(wrap_frequency * x)); } return; } + + assert(o == OVERFLOW_UNDEFINED); // If overflow is undefined, then all we know is that the variable // may take any integer within the range of the bounded integer type. - if (o == OVERFLOW_UNDEFINED) { - for (Variables_Set::const_iterator i = vars.begin(), - vars_end = vars.end(); i != vars.end(); ++i) { - const Variable x = Variable(*i); - if (!gr.bounds_no_check(x)) { - // `x' is not a constant in `gr'. - if (gr.constrains(x)) - // We know that `x' is not a constant, so `x' may wrap to any - // value `x + z' where z is an integer. - add_grid_generator(parameter(x)); - } - else { - // `x' is a constant `v' in `gr'. - PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); - PPL_DIRTY_TEMP_COEFFICIENT(div_x); - coeff_x = gen_sys[0].coefficient(x); - div_x = gen_sys[0].divisor(); - // If the value `v' for `x' is not within the range for the - // bounded integer type, then `x' may wrap to any value `v + z' - // where `z' is an integer; otherwise `x' is unchanged. - if (coeff_x > max_value * div_x || coeff_x < min_value * div_x) { - add_grid_generator(parameter(x)); - } - } - } - return; - } - - // Overflow wraps. - assert(o == OVERFLOW_WRAPS); - for (Variables_Set::const_iterator i = vars.begin(), - vars_end = vars.end(); i != vars.end(); ++i) { + vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); if (!gr.bounds_no_check(x)) { // `x' is not a constant in `gr'. - if (gr.constrains(x)) - // We know that `x' is not a constant, so `x' may wrap - // to a value modulo the `wrap_frequency'. - add_grid_generator(parameter(wrap_frequency * x)); + // We know that `x' is not a constant, so `x' may wrap to any + // value `x + z' where z is an integer. + add_grid_generator(parameter(x)); } else { - // `x' is a constant in `gr'. + // `x' is a constant `v' in `gr'. PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); - PPL_DIRTY_TEMP_COEFFICIENT(f_x); + PPL_DIRTY_TEMP_COEFFICIENT(div_x); coeff_x = gen_sys[0].coefficient(x); - f_x = gen_sys[0].divisor(); - // If the value of `x' is not within the range for the bounded - // integer type, then `x' will wrap modulo the `wrap_frequency'; - // otherwise `x' is unchanged. - if (coeff_x > max_value * f_x || coeff_x < min_value * f_x) { - f_x *= wrap_frequency; - coeff_x %= f_x; - if (s == UNSIGNED && coeff_x < 0) - coeff_x += f_x; - unconstrain(x); - add_constraint(x == coeff_x); + div_x = gen_sys[0].divisor(); + // If the value `v' for `x' is not within the range for the + // bounded integer type, then `x' may wrap to any value `v + z' + // where `z' is an integer; otherwise `x' is unchanged. + if (coeff_x > max_value * div_x || coeff_x < min_value * div_x) { + add_grid_generator(parameter(x)); } } } return; } + /*! \relates Parma_Polyhedra_Library::Grid */ std::ostream& PPL::IO_Operators::operator<<(std::ostream& s, const Grid& gr) {

1 0

[GIT] ppl/ppl(master): Several improvements for the wrap_assign() operator for grids.
by Patricia Hill 12 May '09

12 May '09

Module: ppl/ppl Branch: master Commit: 236efc9ce1d06358f0d0313abd2661423ff9249e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=236efc9ce1d0… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Tue May 12 08:37:29 2009 +0100 Several improvements for the wrap_assign() operator for grids. --- doc/definitions.dox | 63 ++++++++++++++++++++++++-------------------------- src/Grid_public.cc | 13 +++++----- 2 files changed, 36 insertions(+), 40 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index a1cc335..e3148c0 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2313,46 +2313,43 @@ A grid \f$\cL\f$ <EM>subsumes</EM> a (polyhedron) ray or line \f$g\f$ if adding the corresponding grid line to any grid generator system representing \f$\cL\f$ does not change \f$\cL\f$. -\subsection Wrapping_Operator Wrapping Operator +\subsection Grid_Wrapping_Operator Wrapping Operator The operator <CODE>wrap_assign</CODE> provided by the library, allows -for the wrapping of a subset of the set of space dimensions so to fit +for the wrapping of a subset of the set of space dimensions so as to fit the given bounded integer type and have the specified overflow behavior. Suppose \f$\cL \in \Gset_n\f$ is a grid and \f$J\f$ a subset of the set of space dimensions \f$\{0, \ldots, n-1\}\f$. Suppose also that the width of the bounded integer type is \f$w\f$ so that -the range of values can be \f$0 - 2^w-1\f$ if the type is unsigned -and \f$-2^{w-1} - 2^{w-1} - 1\f$ otherwise. -Consider a space dimension \f$j \in J\f$. - -If the value in \f$\cL\f$ for the dimension \f$j\f$ is bounded and -hence a constant, no wrapping can take place; in this case the -grid is unchanged. - -Otherwise the value for the dimension \f$j\f$ will be unbounded and -the result of the operation will depend on which of -three possible overflow behaviors has been specified. - -- Overflow impossible: in this case, it is known that no wrapping can - occur; if the grid has exactly one possible value for the given - bounded integer type, then the dimension \f$j\f$ is set equal to - that value, otherwise, the grid is unchanged. - -- Overflow undefined: in this case, the wrapped value can be any - integer within the range of the bounded integer type, so that the - parameter \f$(0, \ldots, 0, v_j, 0, \dots, 0)\f$, where - \f$v_j = 1\f$ is added to the generator system. - -- Overflow wraps: in this case, the \f$j\f$ dimension can be wrapped to - a value modulo \f$2^w\f$, so that the parameter - \f$(0, \ldots, 0, v_j, 0, \dots, 0)\f$, where \f$v_j = 2^w\f$ - is added to the generator system. - -Note that the <CODE>wrap_assign</CODE> is intended for dimensions that -can take integral values; if this not the case for any of the -dimensions in \f$J\f$ for the grid \f$\cL\f$, the behavior is -undefined. +the range of values \f$R = \{0, \ldots, 2^w-1\}\f$ +if the type is unsigned +and \f$R = \{-2^{w-1},\ldots, 0, \ldots, 2^{w-1} - 1\}\f$ otherwise. +Consider a space dimension \f$j \in J\f$ and a variable \f$v_j\f$ +for dimension \f$j\f$. + +If the value in \f$\cL\f$ for the variable \f$v_j\f$ is +a constant in the range \f$R\f$, then it is unchanged. +Otherwise the result of the operation will depend on the +specified overflow behavior. + +- Overflow impossible. In this case, it is known that no wrapping can + occur. If the grid \f$\cL\f$ has no value for the variable \f$v_j\f$ in the + range \f$R\f$, then \f$\cL\f$ is set empty. If \f$v_j\f$ has exactly + one value \f$a \in R\f$ in \f$\cL\f$, then \f$v_j\f$ is set + equal to \f$a\f$. Otherwise, \f$\cL\f$ is unchanged. + +- Overflow undefined. In this case, for each value \f$a\f$ for + \f$v_j\f$ in the grid \f$\cL\f$, the wrapped value can be any value + \f$a + z \in R\f$ where \f$z \in \Zset\f$. + Therefore the parameter \f$(0, \ldots, 0, v_j, 0, \dots, 0)\f$, + where \f$v_j = 1\f$ is added to the generator system for \f$\cL\f$. + +- Overflow wraps. In this case, for each value \f$a\f$ for + \f$v_j\f$ in the grid \f$\cL\f$, the wrapped value can be any value + \f$a + z 2^{w-1} \in R\f$ where \f$z \in \Zset\f$. + Therefore the parameter \f$(0, \ldots, 0, v_j, 0, \dots, 0)\f$, + where \f$v_j = 2^{w-1}\f$ is added to the generator system for \f$\cL\f$. \subsection Grid_Widening Widening Operators diff --git a/src/Grid_public.cc b/src/Grid_public.cc index 1e181b2..8d54946 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2745,21 +2745,20 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // `x' is not a constant in `gr'. if (gr.constrains(x)) // We know that `x' is not a constant, so `x' may wrap to any - // integral value. + // value `x + z' where z is an integer. add_grid_generator(parameter(x)); } else { - // `x' is a constant in `gr'. + // `x' is a constant `v' in `gr'. PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); PPL_DIRTY_TEMP_COEFFICIENT(div_x); coeff_x = gen_sys[0].coefficient(x); div_x = gen_sys[0].divisor(); - // If the value of `x' is not within the range for the bounded - // integer type, then `x' can take any integral value; - // otherwise `x' is unchanged. + // If the value `v' for `x' is not within the range for the + // bounded integer type, then `x' may wrap to any value `v + z' + // where `z' is an integer; otherwise `x' is unchanged. if (coeff_x > max_value * div_x || coeff_x < min_value * div_x) { - unconstrain(x); - add_congruence(x %= 0); + add_grid_generator(parameter(x)); } } }

1 0

[GIT] ppl/ppl(master): Improved code for wrap_assign() for grids for constant values.
by Patricia Hill 11 May '09

11 May '09

Module: ppl/ppl Branch: master Commit: c3d6b3d44df422a2683d7b2abd313d670123910b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c3d6b3d44df4… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 11 21:32:32 2009 +0100 Improved code for wrap_assign() for grids for constant values. If the value for a variable is already constant, and the constant is outside the range for the bounded integr type, then the outcome depends on the kind of overflow: - if `impossible', then the grid is set empty; - if `undefined', then the variable is set to take any integral value; - if `wraps', then the value is wrapped by the wrap_frequency to a value in the range for the bounded integer type. Comments improved. --- src/Grid.defs.hh | 6 ++-- src/Grid_public.cc | 79 ++++++++++++++++++++++++++++++++++++++++++++------ tests/Grid/wrap1.cc | 77 ++++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 147 insertions(+), 15 deletions(-) diff --git a/src/Grid.defs.hh b/src/Grid.defs.hh index bfb6d12..b8b37ee 100644 --- a/src/Grid.defs.hh +++ b/src/Grid.defs.hh @@ -2135,14 +2135,14 @@ private: /*! \brief Returns <CODE>true</CODE> if and only if \p *this is not empty and - \p expr can takes discrete values in \p *this, in which case the maximum - frequency and minimal value for \p expr in \p *this is computed. + \p expr is discrete in \p *this, in which case the maximum frequency + and the value for \p expr that is closest to zero are computed. \param expr The linear expression for which the frequency is needed; \param freq_n - The numerator of the maximum frequency; + The numerator of the maximum frequency of \p expr; \param freq_d The denominator of the maximum frequency of \p expr; diff --git a/src/Grid_public.cc b/src/Grid_public.cc index be66a1a..1e181b2 100644 --- a/src/Grid_public.cc +++ b/src/Grid_public.cc @@ -2675,11 +2675,26 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, // This is independent of the signedness `s'. PPL_DIRTY_TEMP_COEFFICIENT(wrap_frequency); mul_2exp_assign(wrap_frequency, Coefficient_one(), w); + // Set `min_value' and `max_value' to the minimum and maximum values + // a variable of width `w' and signedness `s' can take. + PPL_DIRTY_TEMP_COEFFICIENT(min_value); + PPL_DIRTY_TEMP_COEFFICIENT(max_value); + if (s == UNSIGNED) { + min_value = 0; + mul_2exp_assign(max_value, Coefficient_one(), w); + --max_value; + } + else { + assert(s == SIGNED_2_COMPLEMENT); + mul_2exp_assign(max_value, Coefficient_one(), w-1); + neg_assign(min_value, max_value); + --max_value; + } // Generators are up-to-date and minimized. const Grid gr = *this; - // Overflow is impossible. So check if value might be constant. + // Overflow is impossible. So check if value might become constant. if (o == OVERFLOW_IMPOSSIBLE) { PPL_DIRTY_TEMP_COEFFICIENT(f_n); PPL_DIRTY_TEMP_COEFFICIENT(f_d); @@ -2688,13 +2703,23 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If the grid frequency for `x' in `vars' is more than half the wrap - // frequency, then `x' can only take a unique (ie constant) value. + // If the grid frequency for `x' in `vars' is more than half the + // `wrap_frequency', then `x' can only take a unique (ie constant) + // value. if (!gr.frequency_no_check(x, f_n, f_d, v_n, v_d)) continue; + if (f_n == 0) { + // `x' is a constant in `gr'. + if ((v_n > max_value * v_d) || (v_n < min_value * v_d)) { + // If the value is outside the range of the bounded integer type, + // then `x' has no possible value and hence `gr' is set empty. + set_empty(); + return; + } + } if (2*f_n > f_d * wrap_frequency) { if (s == UNSIGNED) { - // `v_n' is the value closest to 0 and may be negatve. + // `v_n' is the value closest to 0 and may be negative. if (v_n < 0) { v_n *= f_d; add_mul_assign(v_n, f_n, v_d); @@ -2711,18 +2736,32 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, return; } // If overflow is undefined, then all we know is that the variable - // can take any integer between the wrap bounds. + // may take any integer within the range of the bounded integer type. if (o == OVERFLOW_UNDEFINED) { for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If `x' is a constant, do nothing. if (!gr.bounds_no_check(x)) { + // `x' is not a constant in `gr'. if (gr.constrains(x)) - // We know that `x' is not a constant, - // so `x' may wrap to any integral value. + // We know that `x' is not a constant, so `x' may wrap to any + // integral value. add_grid_generator(parameter(x)); } + else { + // `x' is a constant in `gr'. + PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); + PPL_DIRTY_TEMP_COEFFICIENT(div_x); + coeff_x = gen_sys[0].coefficient(x); + div_x = gen_sys[0].divisor(); + // If the value of `x' is not within the range for the bounded + // integer type, then `x' can take any integral value; + // otherwise `x' is unchanged. + if (coeff_x > max_value * div_x || coeff_x < min_value * div_x) { + unconstrain(x); + add_congruence(x %= 0); + } + } } return; } @@ -2733,13 +2772,33 @@ PPL::Grid::wrap_assign(const Variables_Set& vars, for (Variables_Set::const_iterator i = vars.begin(), vars_end = vars.end(); i != vars.end(); ++i) { const Variable x = Variable(*i); - // If `x' is a constant, do nothing. if (!gr.bounds_no_check(x)) { + // `x' is not a constant in `gr'. if (gr.constrains(x)) - // We know that `x' is not a constant, so `x' may wrap. + // We know that `x' is not a constant, so `x' may wrap + // to a value modulo the `wrap_frequency'. add_grid_generator(parameter(wrap_frequency * x)); } + else { + // `x' is a constant in `gr'. + PPL_DIRTY_TEMP_COEFFICIENT(coeff_x); + PPL_DIRTY_TEMP_COEFFICIENT(f_x); + coeff_x = gen_sys[0].coefficient(x); + f_x = gen_sys[0].divisor(); + // If the value of `x' is not within the range for the bounded + // integer type, then `x' will wrap modulo the `wrap_frequency'; + // otherwise `x' is unchanged. + if (coeff_x > max_value * f_x || coeff_x < min_value * f_x) { + f_x *= wrap_frequency; + coeff_x %= f_x; + if (s == UNSIGNED && coeff_x < 0) + coeff_x += f_x; + unconstrain(x); + add_constraint(x == coeff_x); + } + } } + return; } /*! \relates Parma_Polyhedra_Library::Grid */ diff --git a/tests/Grid/wrap1.cc b/tests/Grid/wrap1.cc index bc78243..235ba02 100644 --- a/tests/Grid/wrap1.cc +++ b/tests/Grid/wrap1.cc @@ -200,7 +200,7 @@ test07() { return ok; } -// Expression of a greater space dimension than the grid. +// Expression with a greater space dimension than the grid. bool test08() { Variable x(0); @@ -226,7 +226,7 @@ test08() { return false; } -// Expression of a greater space dimension than the grid. +// Constraint with a greater space dimension than the grid. bool test09() { Variable x(0); @@ -283,6 +283,76 @@ test10() { return ok; } +bool +test11() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x %= 256) / 0); + gr.add_congruence(y %= 0); + + Variables_Set vars(x); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + + Grid known_result(2); + known_result.add_congruence((x %= 0) / 1); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test12() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x %= 256) / 0); + gr.add_congruence(y %= 0); + + Variables_Set vars(x); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + + Grid known_result(2); + known_result.add_congruence((x %= 0) / 0); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + +bool +test13() { + Variable x(0); + Variable y(1); + Grid gr(2); + gr.add_congruence((x %= 25) / 0); + gr.add_congruence(y %= 0); + + Variables_Set vars(x); + + gr.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + + Grid known_result(2); + known_result.add_congruence((x %= 25) / 0); + known_result.add_congruence(y %= 0); + + bool ok = (gr == known_result); + + print_congruences(gr, "*** gr.wrap_assign(...) ***"); + + return ok; +} + + } // namespace BEGIN_MAIN @@ -296,4 +366,7 @@ BEGIN_MAIN DO_TEST(test08); DO_TEST(test09); DO_TEST_F8(test10); + DO_TEST_F8(test11); + DO_TEST_F8(test12); + DO_TEST_F8(test13); END_MAIN

1 0

[GIT] ppl/ppl(master): Another item dealt with.
by Enea Zaffanella 11 May '09

11 May '09

Module: ppl/ppl Branch: master Commit: 42110bebc56a874568f209c163e082eab144d4ea URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=42110bebc56a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 11 19:06:17 2009 +0200 Another item dealt with. --- TODO | 2 -- 1 files changed, 0 insertions(+), 2 deletions(-) diff --git a/TODO b/TODO index 145be12..1b617f5 100644 --- a/TODO +++ b/TODO @@ -13,8 +13,6 @@ Enhancements for PPL 0.11 - Check the use or the NOT_EQUAL Relation_Symbol everywhere. - Reconsider the datatype for the units parameter in the Watchdog constructors: should we prefer an unsigned? -- Rename set_rational_sqrt_precision_parameter to - set_irrational_precision and make it available on all interfaces. - Intervals are best instantiated with checked numbers with particular policies: review all the interfaced boxes, augment the testsuite, and update the documentation.

1 0

[GIT] ppl/ppl(master): Parameter irrational_precision made available in all language interfaces.
by Enea Zaffanella 11 May '09

11 May '09

Module: ppl/ppl Branch: master Commit: 862f856db64bb43d7c5c36100131da7e577c6297 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=862f856db64b… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 11 18:56:11 2009 +0200 Parameter irrational_precision made available in all language interfaces. --- interfaces/C/ppl_c_header.h | 18 +++++++++++++++++ interfaces/C/ppl_c_implementation_common.cc | 14 +++++++++++++ interfaces/Java/jni/ppl_java_globals.cc | 20 +++++++++++++++++++ .../Parma_Polyhedra_Library.java | 21 ++++++++++++++++--- .../Java/tests/Parma_Polyhedra_Library_test1.java | 2 + interfaces/OCaml/OCaml_interface.dox | 9 ++++++++ interfaces/OCaml/ppl_ocaml_common.cc | 18 +++++++++++++++++ interfaces/OCaml/ppl_ocaml_globals.ml | 6 +++++ interfaces/OCaml/ppl_ocaml_globals.mli | 6 +++++ interfaces/OCaml/tests/test1.ml | 4 +++ interfaces/Prolog/Prolog_interface.dox | 14 +++++++++++++ ...erface_generator_prolog_procedure_generators.m4 | 2 + interfaces/Prolog/ppl_prolog_common.cc | 20 +++++++++++++++++++ interfaces/Prolog/ppl_prolog_common.defs.hh | 6 +++++ interfaces/Prolog/tests/pl_check.pl | 14 ++++++++++++- 15 files changed, 169 insertions(+), 5 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=862f856d…

1 0

[GIT] ppl/ppl(master): Renamed rational_sqrt_precision_parameter to irrational_precision.
by Enea Zaffanella 11 May '09

11 May '09

Module: ppl/ppl Branch: master Commit: b3fe5242d062a0831d1a098d06d4b89456a21429 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b3fe5242d062… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 11 18:53:23 2009 +0200 Renamed rational_sqrt_precision_parameter to irrational_precision. --- src/Init.cc | 2 +- src/checked.cc | 4 ++-- src/checked_mpq.inlines.hh | 24 +++++++++++------------- 3 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/Init.cc b/src/Init.cc index 45e994d..c8b7d9f 100644 --- a/src/Init.cc +++ b/src/Init.cc @@ -175,7 +175,7 @@ PPL::Init::Init() { // The default is choosen to have a precision greater than most // precise IEC559 floating point (112 bits of mantissa). - set_rational_sqrt_precision_parameter(128); + set_irrational_precision(128); } } diff --git a/src/checked.cc b/src/checked.cc index 3529e87..42b57b6 100644 --- a/src/checked.cc +++ b/src/checked.cc @@ -32,8 +32,8 @@ Not_A_Number NOT_A_NUMBER; namespace Checked { -//! Holds the precision parameter used for rational sqrt calculations. -unsigned long rational_sqrt_precision_parameter; +//! Holds the precision parameter used for irrational calculations. +unsigned irrational_precision; struct number_struct { unsigned int base; diff --git a/src/checked_mpq.inlines.hh b/src/checked_mpq.inlines.hh index 436d61e..c99c6e1 100644 --- a/src/checked_mpq.inlines.hh +++ b/src/checked_mpq.inlines.hh @@ -377,7 +377,7 @@ sub_mul_mpq(mpq_class& to, const mpq_class& x, const mpq_class& y, PPL_SPECIALIZE_SUB_MUL(sub_mul_mpq, mpq_class, mpq_class, mpq_class) -extern unsigned long rational_sqrt_precision_parameter; +extern unsigned irrational_precision; template <typename To_Policy, typename From_Policy> inline Result @@ -395,15 +395,13 @@ sqrt_mpq(mpq_class& to, const mpq_class& from, Rounding_Dir dir) { mpz_class& to_b = gt1 ? to.get_den() : to.get_num(); Rounding_Dir rdir = gt1 ? dir : inverse(dir); mul_2exp<To_Policy, From_Policy>(to_a, from_a, - 2*rational_sqrt_precision_parameter, - ROUND_IGNORE); + 2*irrational_precision, ROUND_IGNORE); Result rdiv = div<To_Policy, To_Policy, To_Policy>(to_a, to_a, from_b, rdir); Result rsqrt = sqrt<To_Policy, To_Policy>(to_a, to_a, rdir); to_b = 1; mul_2exp<To_Policy, To_Policy>(to_b, to_b, - rational_sqrt_precision_parameter, - ROUND_IGNORE); + irrational_precision, ROUND_IGNORE); to.canonicalize(); return rdiv != V_EQ ? rdiv : rsqrt; } @@ -457,27 +455,27 @@ PPL_SPECIALIZE_ASSIGN(assign_mpq_long_double, mpq_class, long double) } // namespace Checked -//! Returns the precision parameter used for rational square root calculations. +//! Returns the precision parameter used for irrational calculations. inline unsigned -rational_sqrt_precision_parameter() { - return Checked::rational_sqrt_precision_parameter; +irrational_precision() { + return Checked::irrational_precision; } -//! Sets the precision parameter used for rational square root calculations. +//! Sets the precision parameter used for irrational calculations. /*! The lesser between numerator and denominator is limited to 2**\p p. If \p p is less than or equal to <CODE>INT_MAX</CODE>, sets the - precision parameter used for rational square root calculations to \p p. + precision parameter used for irrational calculations to \p p. \exception std::invalid_argument Thrown if \p p is greater than <CODE>INT_MAX</CODE>. */ inline void -set_rational_sqrt_precision_parameter(const unsigned p) { +set_irrational_precision(const unsigned p) { if (p <= INT_MAX) - Checked::rational_sqrt_precision_parameter = p; + Checked::irrational_precision = p; else - throw std::invalid_argument("PPL::set_rational_sqrt_precision_parameter(p)" + throw std::invalid_argument("PPL::set_irrational_precision(p)" " with p > INT_MAX"); }

1 0

[GIT] ppl/ppl(master): Several tests are expected to fail for checked-in8.
by Patricia Hill 11 May '09

11 May '09

Module: ppl/ppl Branch: master Commit: ca6ac08359877616581492e80dfd2979a3e946d5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ca6ac0835987… Author: Patricia Hill <p.m.hill(a)leeds.ac.uk> Date: Mon May 11 14:24:18 2009 +0100 Several tests are expected to fail for checked-in8. --- tests/Grid/wrap1.cc | 16 ++++++++-------- 1 files changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/Grid/wrap1.cc b/tests/Grid/wrap1.cc index 7b93cc6..bc78243 100644 --- a/tests/Grid/wrap1.cc +++ b/tests/Grid/wrap1.cc @@ -286,14 +286,14 @@ test10() { } // namespace BEGIN_MAIN - DO_TEST(test01); - DO_TEST(test02); - DO_TEST(test03); - DO_TEST(test04); - DO_TEST(test05); - DO_TEST(test06); - DO_TEST(test07); + DO_TEST_F8(test01); + DO_TEST_F8(test02); + DO_TEST_F8(test03); + DO_TEST_F8(test04); + DO_TEST_F8(test05); + DO_TEST_F8(test06); + DO_TEST_F8(test07); DO_TEST(test08); DO_TEST(test09); - DO_TEST(test10); + DO_TEST_F8(test10); END_MAIN

1 0