September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Improved test for class Linear_Form.
by Roberto Amadini 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 3d115f781b8c26b19c6a4fe0b8d491a909e9a82a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3d115f781b8c… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 9 17:55:46 2009 +0200 Improved test for class Linear_Form. --- tests/Floating_Point_Expression/linearform1.cc | 48 ++++++++++++++++++++++-- 1 files changed, 44 insertions(+), 4 deletions(-) diff --git a/tests/Floating_Point_Expression/linearform1.cc b/tests/Floating_Point_Expression/linearform1.cc index bee32ba..c6ba2ab 100644 --- a/tests/Floating_Point_Expression/linearform1.cc +++ b/tests/Floating_Point_Expression/linearform1.cc @@ -219,22 +219,62 @@ test07() { // Tests overflows of space dimension. -// FIXME: works in progress! bool test08() { - Linear_Form<fl_r_oc> f; + Linear_Form<db_r_oc> f; Variable A(f.max_space_dimension()); bool ok1 = false; try { - f = Linear_Form<fl_r_oc>(A); + f = Linear_Form<db_r_oc>(A); } catch(std::length_error e) { nout << "Overflow in Linear_Form(const Variable v)." << endl; ok1 = true; } - return ok1; + bool ok2 = false; + try { + f += A; + } + catch(std::length_error e) { + nout << "Overflow in operator+=(Linear_Form<C>& f, const Variable v)." + << endl; + ok2 = true; + } + + Linear_Form<db_r_oc> g; + bool ok3 = false; + try { + g = f - A; + } + catch(std::length_error e) { + nout << "Overflow in operator-(Linear_Form<C>& f, const Variable v)." + << endl; + ok3 = true; + } + + bool ok4 = false; + try { + g = A - f; + } + catch(std::length_error e) { + nout << "Overflow in operator-(const Variable v, Linear_Form<C>& f)." + << endl; + ok4 = true; + } + + bool ok5 = false; + try { + g = A + f; + } + catch(std::length_error e) { + nout << "Overflow in operator+(const Variable v, Linear_Form<C>& f)." + << endl; + ok5 = true; + } + + return ok1 && ok2 && ok3 && ok4 && ok5; } } // namespace

1 0

[GIT] ppl/ppl(floating_point): Fixed few typo
by Fabio Biselli 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 19b136f854184406ad4ce422922dd816f6f4dc41 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=19b136f85418… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Wed Sep 9 19:39:19 2009 +0200 Fixed few typo --- doc/ppl.sty | 1 + src/Difference_Floating_Point_Expression.defs.hh | 8 ++++---- src/Division_Floating_Point_Expression.defs.hh | 4 ++-- ...ultiplication_Floating_Point_Expression.defs.hh | 5 +++-- 4 files changed, 10 insertions(+), 8 deletions(-) diff --git a/doc/ppl.sty b/doc/ppl.sty index 27055c5..7b3a550 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -24,6 +24,7 @@ \ProvidesPackage{ppl} \RequirePackage{amsmath} \RequirePackage{amssymb} +\RequirePackage{stmaryrd} %% Calligraphic alphabet \newcommand*{\cA}{\ensuremath{\mathcal{A}}} diff --git a/src/Difference_Floating_Point_Expression.defs.hh b/src/Difference_Floating_Point_Expression.defs.hh index cea8ac3..ae56a81 100644 --- a/src/Difference_Floating_Point_Expression.defs.hh +++ b/src/Difference_Floating_Point_Expression.defs.hh @@ -85,13 +85,13 @@ namespace Parma_Polyhedra_Library { \f[ \linexpr{e_{1} \ominus e_{2}}\rho^{\#} = \linexpr{e_{1}}\rho^{\#} - \adifp + \adlf \linexpr{e_{2}}\rho^{\#} - \asifp + \aslf \varepsilon_{\mathbf{f}}\left(\linexpr{e_{1}}\rho^{\#}\right) - \asifp + \aslf \varepsilon_{\mathbf{f}}\left(\linexpr{e_{2}}\rho^{\#}\right) - \asifp + \aslf mf_{\mathbf{f}}[-1;1] \f] where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form obtained diff --git a/src/Division_Floating_Point_Expression.defs.hh b/src/Division_Floating_Point_Expression.defs.hh index ed32977..1f16247 100644 --- a/src/Division_Floating_Point_Expression.defs.hh +++ b/src/Division_Floating_Point_Expression.defs.hh @@ -83,7 +83,7 @@ namespace Parma_Polyhedra_Library { \f[ \linexpr{e_{1} \oslash [a;b]}\rho^{\#} = - \left(\linexpr{e_{2}}\rho^{\#} + \left(\linexpr{e_{1}}\rho^{\#} \adivlf [a;b]\right) \aslf @@ -100,7 +100,7 @@ namespace Parma_Polyhedra_Library { \f[ \linexpr{e_{1} \oslash e_{2}}\rho^{\#} = - \linexpr{e_{1} \oslash \iota\left(\linexpr{e_{2}\rho^{\#}}\right)}\rho^{\#}. + \linexpr{e_{1} \oslash \iota\left(\linexpr{e_{2}}\rho^{\#}\right)\rho^{\#}}. \f] where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form obtained by the method <CODE>Floating_Point_Expression::relative_error()</CODE>, diff --git a/src/Multiplication_Floating_Point_Expression.defs.hh b/src/Multiplication_Floating_Point_Expression.defs.hh index 2265ca7..7da5238 100644 --- a/src/Multiplication_Floating_Point_Expression.defs.hh +++ b/src/Multiplication_Floating_Point_Expression.defs.hh @@ -63,7 +63,7 @@ namespace Parma_Polyhedra_Library { Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and \f$i' + \sum_{v \in \cV}i'_{v}v \f$ be two linear forms, \f$\aslf\f$ and \f$\amlf\f$ two sound abstract - operator on linear forms such that: + operators on linear forms such that: \f[ \left(i + \sum_{v \in \cV}i_{v}v\right) \aslf @@ -112,7 +112,8 @@ namespace Parma_Polyhedra_Library { \f[ \linexpr{e_{1} \otimes e_{2}}\rho^{\#} = - \linexpr{\iota\left(\linexpr{e_{1}\rho^{\#}}\right) \otimes e_{2}}\rho^{\#}. + \linexpr{\iota\left(\linexpr{e_{1}}\rho^{\#}\right)\rho^{\#} + \otimes e_{2}}\rho^{\#}. \f] where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form obtained by the method <CODE>Floating_Point_Expression::relative_error()</CODE>,

1 0

[GIT] ppl/ppl(floating_point): Fixed typo.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 60b9772ac000271a4ab1176e552341cb6e590183 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=60b9772ac000… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 17:40:00 2009 +0200 Fixed typo. --- src/Division_Floating_Point_Expression.defs.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Division_Floating_Point_Expression.defs.hh b/src/Division_Floating_Point_Expression.defs.hh index eb42df9..ed32977 100644 --- a/src/Division_Floating_Point_Expression.defs.hh +++ b/src/Division_Floating_Point_Expression.defs.hh @@ -71,7 +71,7 @@ namespace Parma_Polyhedra_Library { \f] \f[ \left(i + \sum_{v \in \cV}i_{v}v\right) - \divlf + \adivlf i' = \left(i \adivifp i'\right) +

1 0

[GIT] ppl/ppl(pip): Implemented proper handling of nonbasic variables when adding rows.
by François Galea 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: pip Commit: a50f74f87f9702381d9af3a40dbe8941090a6489 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a50f74f87f97… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 9 15:59:09 2009 +0200 Implemented proper handling of nonbasic variables when adding rows. --- src/PIP_Tree.cc | 34 +++++++++++++++++++++------------- src/PIP_Tree.defs.hh | 22 ++++++++++++++++++++-- 2 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 28cfbc9..fc6e1db 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -150,7 +150,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref, dimension_type first_pending_constraint, const Constraint_Sequence &input_cs, const Variables_Set &parameters) { - dimension_type i; + dimension_type i, j; dimension_type n_params = parameters.size(); dimension_type n_vars = external_space_dim - n_params; dimension_type n_vars_int = tableau.s.num_columns(); @@ -168,8 +168,11 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref, for (i=internal_space_dim; i<external_space_dim; ++i) { if (parameters.count(i) == 1) tableau.t.add_zero_columns(1); - else + else { tableau.s.add_zero_columns(1); + basis.push_back(true); + mapping.push_back(tableau.s.num_columns()-1); + } } internal_space_dim = external_space_dim; @@ -178,7 +181,6 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref, for (cst = input_cs.begin() + first_pending_constraint; cst < input_cs.end(); ++cst) { - // FIXME: must handle nonbasic variables aswell int v = 0; int p = 1; Row var(n_vars, Row::Flags()); @@ -190,10 +192,22 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref, param[0] = cnst_term * denom_t; for (i=0; i<internal_space_dim; i++) { if (parameters.count(i) == 1) { - param[p] = cst->coefficient(Variable(i)) * denom_t; - ++p; + param[p++] = cst->coefficient(Variable(i)) * denom_t; } else { - var[v] = cst->coefficient(Variable(i)) * denom_s; + Coefficient c = cst->coefficient(Variable(i)) * denom_s; + dimension_type idx = mapping[v]; + if (basis[v]) + // Basic variable : add c * x_i + var[idx] += c; + else { + // Nonbasic variable : add c * row_i + const Row &sr = tableau.s[idx]; + const Row &st = tableau.t[idx]; + for (j=0; j<sr.size(); j++) + var[j] += c*sr[j]; + for (j=0; j<st.size(); j++) + param[j] += c*st[j]; + } ++v; } } @@ -201,13 +215,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node **parent_ref, tableau.s.add_row(var); tableau.t.add_row(param); } - - // update current basis with newly inserted variables - dimension_type next_var = n_vars_int + n_constr_int; - for (i=n_vars_int; i<n_vars; ++i) - basis.insert(next_var++); + // FIXME: decide emptiness detection (and node removal) } - - } // namespace Parma_Polyhedra_Library diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 63659d8..bf46c8e 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -179,8 +179,26 @@ private: //! The parametric simplex tableau. Tableau tableau; - //! A set containing the internal indices of the basic variables - Variables_Set basis; + /*! \brief + A boolean vector for identifying the basic variables. + + The value for <tt>basis[i]</tt> is: + - \b true if variable \p i is basic, + - \b false if variable \p i is nonbasic. + */ + std::vector<bool> basis; + + /*! \brief + A mapping between the tableau rows/columns and the original variables. + + The value of <tt>mapping[i]</tt> depends of the value of <tt>basis[i]</tt>. + + - If <tt>basis[i]</tt> is \b true, <tt>mapping[i]</tt> encodes the column + index of variable \p i in the \p s matrix of the tableau. + - If <tt>basis[i]</tt> is \b false, <tt>mapping[i]</tt> encodes the row + index of variable \p i in the tableau. + */ + std::vector<dimension_type> mapping; protected: /*! \brief

1 0

[GIT] ppl/ppl(floating_point): Use \infty instead of \infinity.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: b8f6d2ee0afe733869f04cadf1becf4c7c03e8ad URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b8f6d2ee0afe… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 17:37:08 2009 +0200 Use \infty instead of \infinity. --- src/Constant_Floating_Point_Expression.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Constant_Floating_Point_Expression.defs.hh b/src/Constant_Floating_Point_Expression.defs.hh index 2a22bde..bf623b8 100644 --- a/src/Constant_Floating_Point_Expression.defs.hh +++ b/src/Constant_Floating_Point_Expression.defs.hh @@ -65,8 +65,8 @@ namespace Parma_Polyhedra_Library { follow: \f[ \linexpr{\textrm{const}_{\mathbf{f},\mathbf{r}}(c)}\rho^{\#} = - [\textrm{const}_{\mathbf{f},-\infinity}(c); - \textrm{const}_{\mathbf{f},+\infinity}(c)]. + [\textrm{const}_{\mathbf{f},-\infty}(c); + \textrm{const}_{\mathbf{f},+\infty}(c)]. \f] */ template <typename FP_Interval_Type, typename FP_Format>

1 0

[GIT] ppl/ppl(floating_point): Updated documentation
by Fabio Biselli 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 6c80dc54db17383f1cc892e905e3dac804ba158d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6c80dc54db17… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Wed Sep 9 19:08:00 2009 +0200 Updated documentation --- src/Constant_Floating_Point_Expression.defs.hh | 14 ++++ src/Difference_Floating_Point_Expression.defs.hh | 43 +++++++++++-- src/Division_Floating_Point_Expression.defs.hh | 55 +++++++++++++++--- src/Floating_Point_Expression.defs.hh | 14 ++++ ...ultiplication_Floating_Point_Expression.defs.hh | 63 +++++++++++++++++-- src/Sum_Floating_Point_Expression.defs.hh | 26 +++++++-- src/Variable_Floating_Point_Expression.defs.hh | 12 ++++ 7 files changed, 200 insertions(+), 27 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=6c80dc54…

1 0

[GIT] ppl/ppl(floating_point): Predisposed everything to start implementing our own customized version
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: edf215e958a23f0fe12b06c8f1481deaa7473676 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=edf215e958a2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 16:33:27 2009 +0200 Predisposed everything to start implementing our own customized version of method affine_image. --- src/Octagonal_Shape.defs.hh | 11 ++++++ src/Octagonal_Shape.templates.hh | 64 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 5235902..4035b35 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -44,6 +44,8 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Checked_Number.defs.hh" #include "WRD_coefficient_types.defs.hh" #include "Bit_Row.defs.hh" +#include "Interval.types.hh" +#include "Linear_Form.types.hh" #include <vector> #include <cstddef> #include <climits> @@ -1104,6 +1106,10 @@ public: Coefficient_traits::const_reference denominator = Coefficient_one()); + template <typename Interval_Info> + void affine_image(Variable var, + const Linear_Form< Interval<T, Interval_Info> >& lf); + /*! \brief Assigns to \p *this the \ref affine_relation "affine preimage" of \p *this under the function mapping variable \p var into the @@ -2106,6 +2112,11 @@ private: const char* name_row, const Linear_Expression& y) const; + template <typename C> + void throw_dimension_incompatible(const char* method, + const char* name_row, + const Linear_Form<C>& y) const; + void throw_constraint_incompatible(const char* method) const; void throw_expression_too_complex(const char* method, diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index a9590a7..69cf0eb 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -27,6 +27,8 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Generator_System.inlines.hh" #include "Congruence_System.defs.hh" #include "Congruence_System.inlines.hh" +#include "Interval.defs.hh" +#include "Linear_Form.defs.hh" #include "meta_programming.hh" #include "assert.hh" #include <vector> @@ -4670,6 +4672,54 @@ Octagonal_Shape<T>::affine_image(const Variable var, } template <typename T> +template <typename Interval_Info> +void +Octagonal_Shape<T>::affine_image(Variable var, + const Linear_Form< Interval<T, Interval_Info> >& lf) { + /* + 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); + + // Dimension-compatibility checks. + // The dimension of `lf' should not be greater than the dimension + // of `*this'. + const dimension_type lf_space_dim = lf.space_dimension(); + if (space_dim < lf_space_dim) + throw_dimension_incompatible("affine_image(v, l)", "l", lf); + + // `var' should be one of the dimensions of the octagon. + const dimension_type var_id = var.id(); + if (space_dim < var_id + 1) + throw_dimension_incompatible("affine_image(v, l)", var.id()+1); + + strong_closure_assign(); + // The image of an empty octagon is empty too. + if (marked_empty()) + return; + + // Number of non-zero coefficients in `lf': will be set to + // 0, 1, or 2, the latter value meaning any value greater than 1. + dimension_type t = 0; + // Variable-index of the last non-zero coefficient in `lf', if any. + dimension_type w_id = 0; + + // Get information about the number of non-zero coefficients in `lf'. + for (dimension_type i = lf_space_dim; i-- > 0; ) + if (lf.coefficient(Variable(i)) != 0) { + if (t++ == 1) + break; + else + w_id = i; + } + + // FIXME: complete the implementation. + +} + +template <typename T> void Octagonal_Shape<T>::affine_preimage(const Variable var, const Linear_Expression& expr, @@ -7065,6 +7115,20 @@ Octagonal_Shape<T> throw std::invalid_argument(s.str()); } +template <typename T> +template <typename C> +void +Octagonal_Shape<T> +::throw_dimension_incompatible(const char* method, + const char* name_row, + const Linear_Form<C>& y) const { + std::ostringstream s; + s << "PPL::Octagonal_Shape::" << method << ":\n" + << "this->space_dimension() == " << space_dimension() + << ", " << name_row << "->space_dimension() == " + << y.space_dimension() << "."; + throw std::invalid_argument(s.str()); +} template <typename T> void

1 0

[GIT] ppl/ppl(floating_point): Fixed bug in Linear_Form.
by Roberto Amadini 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 37c753c529b2b104fff0dc63ff83119ce1b52b9a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=37c753c529b2… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 9 16:19:06 2009 +0200 Fixed bug in Linear_Form. Copied linearform1.cc in tests/Floating_Point_Expression and improved its tests. --- src/Linear_Form.templates.hh | 1 - tests/Floating_Point_Expression/Makefile.am | 3 +- tests/Floating_Point_Expression/linearform1.cc | 251 ++++++++++++++++++++++++ 3 files changed, 253 insertions(+), 2 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index e7c12f9..335207f 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -109,7 +109,6 @@ operator+(const Linear_Form<C>& f1, const Linear_Form<C>& f2) { r[i] = f1[i]; r[i] += f2[i]; } - return r; } diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am old mode 100644 new mode 100755 index 3fb4233..da6a023 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -49,7 +49,7 @@ $(top_builddir)/tests/libppl_tests.a \ $(top_builddir)/src/libppl.la \ @extra_libraries@ -TESTS = \ +TESTS = linearform1 \ floatingpointexpr1 XFAIL_TESTS = @@ -60,6 +60,7 @@ BUGS = # Sources for the tests # +linearform1_SOURCES = linearform1.cc floatingpointexpr1_SOURCES = floatingpointexpr1.cc check_PROGRAMS = \ diff --git a/tests/Floating_Point_Expression/linearform1.cc b/tests/Floating_Point_Expression/linearform1.cc new file mode 100644 index 0000000..bee32ba --- /dev/null +++ b/tests/Floating_Point_Expression/linearform1.cc @@ -0,0 +1,251 @@ +/* Testing Linear_Expression. + Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +using namespace Parma_Polyhedra_Library::IO_Operators; + +// Test operator-=(Linear_Form<db_r_oc>& f1, const Linear_Form<db_r_oc>& f2): +// in this case the dimension of f2 is strictly greater than +// the dimension of f1. +bool +test01() { + Variable A(0); + Variable B(1); + + Linear_Form<db_r_oc> f; + Linear_Form<db_r_oc> f1 = A; + Linear_Form<db_r_oc> f2 = B; + + f1 += f.coefficient(A); + f1 -= f2; + + Linear_Form<db_r_oc> known_result = A - Linear_Form<db_r_oc>(B); + + bool ok = (f1 == known_result); + + nout << "*** known_result ***" << endl + << known_result << endl; + + return ok; +} + +bool +test02() { + Variable A(15); + Variable B(0); + + Linear_Form<db_r_oc> f1 = A; + Linear_Form<db_r_oc> f2 = B; + + Linear_Form<db_r_oc> known_result1 = f1 + f2; + + bool ok1 = (Linear_Form<db_r_oc>(A) + B == known_result1) + && (B + Linear_Form<db_r_oc>(A) == known_result1) + && (A + Linear_Form<db_r_oc>(B) == known_result1) + && (Linear_Form<db_r_oc>(B) + A == known_result1) + && (Linear_Form<db_r_oc>(B) + Linear_Form<db_r_oc>(A) == known_result1); + + nout << "*** known_result1 ***" << endl + << known_result1 << endl; + + Linear_Form<db_r_oc> known_result2 = f1 + f1; + + bool ok2 = (Linear_Form<db_r_oc>(A) + A == known_result2) + && (A + Linear_Form<db_r_oc>(A) == known_result2) + && (A + Linear_Form<db_r_oc>(A) == known_result2) + && (Linear_Form<db_r_oc>(A) + A == known_result2) + && (Linear_Form<db_r_oc>(A) + Linear_Form<db_r_oc>(A) == known_result2); + + nout << "*** known_result2 ***" << endl + << known_result2 << endl; + + return ok1 && ok2; +} + +bool +test03() { + Variable A(15); + Variable B(10); + + Linear_Form<db_r_oc> f1 = A; + Linear_Form<db_r_oc> f2 = B; + + Linear_Form<db_r_oc> known_result1 = f1 - f2; + + bool ok1 = (Linear_Form<db_r_oc>(A) - B == known_result1) + && (A - Linear_Form<db_r_oc>(B) == known_result1) + && (Linear_Form<db_r_oc>(A) - Linear_Form<db_r_oc>(B) == known_result1); + + nout << "*** known_result1 ***" << endl + << known_result1 << endl; + + Linear_Form<db_r_oc> known_result2 = f2 - f1; + + bool ok2 = (Linear_Form<db_r_oc>(B) - A == known_result2) + && (B - Linear_Form<db_r_oc>(A) == known_result2) + && (Linear_Form<db_r_oc>(B) - Linear_Form<db_r_oc>(A) == known_result2); + + nout << "*** known_result2 ***" << endl + << known_result2 << endl; + + Linear_Form<db_r_oc> known_result3 = f1 - f1; + + bool ok3 = (Linear_Form<db_r_oc>(A) - A == known_result3) + && (A - Linear_Form<db_r_oc>(A) == known_result3) + && (Linear_Form<db_r_oc>(A) - Linear_Form<db_r_oc>(A) == known_result3); + + nout << "*** known_result3 ***" << endl + << known_result3 << endl; + + return ok1 && ok2 && ok3; +} + +// Test operator+=(Linear_Form<db_r_oc>& f1, const Linear_Form<db_r_oc>& f2): +// in this case the dimension of f2 is strictly greater than +// the dimension of f1. +bool +test04() { + Variable A(0); + Variable B(1); + + Linear_Form<db_r_oc> f1 = A; + Linear_Form<db_r_oc> f2 = B; + f1 += f2; + + Linear_Form<db_r_oc> known_result = Linear_Form<db_r_oc>(A) + B; + + bool ok = (f1 == known_result); + + nout << "*** known_result ***" << endl + << known_result << endl; + + return ok; +} + +// Test operator+=(Linear_Form<db_r_oc>& f, Variable v): +// in this case the dimension of v is strictly greater than +// the dimension of f. +bool +test05() { + Variable A(0); + Variable B(1); + + Linear_Form<db_r_oc> f = A; + db_r_oc x(2.0); + x /= 3.0; + f *= x; + + Linear_Form<db_r_oc> known_result = f + B; + + f += B; + + bool ok = (f == known_result); + + nout << "*** known_result ***" << endl + << known_result << endl; + + return ok; +} + +bool +test06() { + Variable A(0); + Variable B(1); + Variable C(16); + Variable D(120); + + Linear_Form<db_r_oc> f = A + 2*B + 16*C + 120*D; + + Linear_Form<db_r_oc> known_result = A; + known_result += db_r_oc(2) * Linear_Form<db_r_oc>(B); + known_result += db_r_oc(16) * Linear_Form<db_r_oc>(C); + known_result += db_r_oc(120) * Linear_Form<db_r_oc>(D); + + bool ok = (f == known_result); + + nout << "*** known_result ***" << endl + << known_result << endl; + + return ok; +} + +// Tests operator==(const Linear_Form<C>& x, const Linear_Form<C>& y) +bool +test07() { + Variable A(0); + Variable B(1); + Variable C(2); + Linear_Form<db_r_oc> f1 = A; + Linear_Form<db_r_oc> f2; + bool known_result = false; + + bool result1 = (f1 == f2); + + f2 += db_r_oc(1.0); + bool result2 = (f1 == f2); + + bool result3 = (f2 == f1); + + f1 += db_r_oc(1.0); + bool result4 = (f2 == f1); + + nout << "*** known_result ***" << endl + << known_result << endl; + + return (known_result == (result1 || result2 || result3 || result4)); +} + + +// Tests overflows of space dimension. +// FIXME: works in progress! +bool +test08() { + Linear_Form<fl_r_oc> f; + Variable A(f.max_space_dimension()); + + bool ok1 = false; + try { + f = Linear_Form<fl_r_oc>(A); + } + catch(std::length_error e) { + nout << "Overflow in Linear_Form(const Variable v)." << endl; + ok1 = true; + } + + return ok1; +} + +} // 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(test08); +END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Use \defeq instead of = for definitions.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 66515df137210d3048db981bd716f900c51e0075 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=66515df13721… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 10:40:06 2009 +0200 Use \defeq instead of = for definitions. Fixed an error concerning frames. --- doc/definitions.dox | 20 ++++++++++++++++---- 1 files changed, 16 insertions(+), 4 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 07cbebd..da987ea 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2665,28 +2665,40 @@ The operations on interval linear forms are intuitively defined as follows: \left(i + \sum_{v \in V}i_{v}v\right) \aslf \left(i' + \sum_{v \in V}i'_{v}v\right) - = + \defeq \left(i \asifp i'\right) + \sum_{v \in V}\left(i_{v} \asifp i'_{v}\right)v, +\f] + +\f[ + \left(i + \sum_{v \in V}i_{v}v\right) \adlf \left(i' + \sum_{v \in V}i'_{v}v\right) - = + \defeq \left(i \adifp i'\right) + \sum_{v \in V}\left(i_{v} \adifp i'_{v}\right)v, +\f] + +\f[ + i \amlf \left(i' + \sum_{v \in V}i'_{v}v\right) - = + \defeq \left(i \amifp i'\right) + \sum_{v \in V}\left(i \amifp i'_{v}\right)v, +\f] + +\f[ + \left(i + \sum_{v \in V}i_{v}v\right) \adivlf i' - = + \defeq \left(i \adivifp i'\right) + \sum_{v \in V}\left(i_{v} \adivifp i'\right)v.

1 0

[GIT] ppl/ppl(floating_point): Use new linearization macro.
by Fabio Bossi 09 Sep '09

09 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 59241488abfbff6a8310a938c96d09de3dab3ce3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=59241488abfb… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 9 10:26:32 2009 +0200 Use new linearization macro. --- doc/definitions.dox | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index 4f241cd..07cbebd 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -2711,7 +2711,8 @@ point expression classes for more information. The linearization of a floating point expression \f$e\f$ in the composite abstract store \f$\left \langle \rho, \rho_l \right \rangle\f$ will be denoted -by \f$\f$. There are two ways a linearization attempt can fail: +by \f$\linexpr{e} \left (\rho, \rho_l \right )\f$. There are two ways a +linearization attempt can fail: - whenever an interval boundary overflows to \f$+\infty\f$ or \f$-\infty\f$, and - when we try to divide by an interval that contains \f$0\f$.

1 0