PPL  1.2
Floating_Point_Expression_templates.hh
Go to the documentation of this file.
1 /* Floating_Point_Expression class implementation:
2  non-inline template functions.
3  Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
4  Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
5 
6 This file is part of the Parma Polyhedra Library (PPL).
7 
8 The PPL is free software; you can redistribute it and/or modify it
9 under the terms of the GNU General Public License as published by the
10 Free Software Foundation; either version 3 of the License, or (at your
11 option) any later version.
12 
13 The PPL is distributed in the hope that it will be useful, but WITHOUT
14 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
15 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
16 for more details.
17 
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software Foundation,
20 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
21 
22 For the most up-to-date information see the Parma Polyhedra Library
23 site: http://bugseng.com/products/ppl/ . */
24 
25 #ifndef PPL_Floating_Point_Expression_templates_hh
26 #define PPL_Floating_Point_Expression_templates_hh 1
27 
28 #include "Linear_Form_defs.hh"
29 #include <cmath>
30 
31 namespace Parma_Polyhedra_Library {
32 
33 template<typename FP_Interval_Type, typename FP_Format>
34 void
37 
38  FP_Interval_Type error_propagator;
39  boundary_type lb = -pow(FP_Format::BASE,
41  ::boundary_type>(FP_Format::MANTISSA_BITS));
42  error_propagator.build(i_constraint(GREATER_OR_EQUAL, lb),
44 
45  // Handle the inhomogeneous term.
46  const FP_Interval_Type* current_term = &lf.inhomogeneous_term();
47  assert(current_term->is_bounded());
48 
49  FP_Interval_Type
50  current_multiplier(std::max(std::abs(current_term->lower()),
51  std::abs(current_term->upper())));
52  FP_Linear_Form current_result_term(current_multiplier);
53  current_result_term *= error_propagator;
54  result = FP_Linear_Form(current_result_term);
55 
56  // Handle the other terms.
57  dimension_type dimension = lf.space_dimension();
58  for (dimension_type i = 0; i < dimension; ++i) {
59  current_term = &lf.coefficient(Variable(i));
60  assert(current_term->is_bounded());
61  current_multiplier
62  = FP_Interval_Type(std::max(std::abs(current_term->lower()),
63  std::abs(current_term->upper())));
64  current_result_term = FP_Linear_Form(Variable(i));
65  current_result_term *= current_multiplier;
66  current_result_term *= error_propagator;
67  result += current_result_term;
68  }
69 
70  return;
71 }
72 
73 template<typename FP_Interval_Type, typename FP_Format>
74 void
77  const FP_Interval_Abstract_Store& store,
78  FP_Interval_Type& result) {
79  result = FP_Interval_Type(lf.inhomogeneous_term());
80  dimension_type dimension = lf.space_dimension();
81  assert(dimension <= store.space_dimension());
82  for (dimension_type i = 0; i < dimension; ++i) {
83  FP_Interval_Type current_addend = lf.coefficient(Variable(i));
84  const FP_Interval_Type& curr_int = store.get_interval(Variable(i));
85  current_addend *= curr_int;
86  result += current_addend;
87  }
88 
89  return;
90 }
91 
92 template<typename FP_Interval_Type, typename FP_Format>
93 FP_Interval_Type
97  ::boundary_type Boundary;
98  boundary_type omega;
99  omega = std::max(pow(static_cast<Boundary>(FP_Format::BASE),
100  static_cast<Boundary>(1 - FP_Format::EXPONENT_BIAS
101  - FP_Format::MANTISSA_BITS)),
102  std::numeric_limits<Boundary>::denorm_min());
103  FP_Interval_Type result;
104  result.build(i_constraint(GREATER_OR_EQUAL, -omega),
105  i_constraint(LESS_OR_EQUAL, omega));
106  return result;
107 }
108 
109 } // namespace Parma_Polyhedra_Library
110 
111 #endif // !defined(PPL_Floating_Point_Expression_templates_hh)
FP_Interval_Type::boundary_type boundary_type
The floating point format used by the analyzer.
I_Constraint< T > i_constraint(I_Constraint_Rel rel, const T &v)
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
Definition: Box_inlines.hh:123
size_t dimension_type
An unsigned integral type for representing space dimensions.
const C & coefficient(Variable v) const
Returns the coefficient of v in *this.
dimension_type space_dimension() const
Returns the dimension of the vector space enclosing *this.
static FP_Interval_Type compute_absolute_error()
Computes the absolute error.
A dimension of the vector space.
static void relative_error(const FP_Linear_Form &lf, FP_Linear_Form &result)
Computes the relative error of a given linear form.
A linear form with interval coefficients.
A not necessarily closed, iso-oriented hyperrectangle.
Definition: Box_defs.hh:299
static void intervalize(const FP_Linear_Form &lf, const FP_Interval_Abstract_Store &store, FP_Interval_Type &result)
Makes result become an interval that overapproximates all the possible values of lf in the interval a...
The entire library is confined to this namespace.
Definition: version.hh:61
const ITV & get_interval(Variable var) const
Returns a reference the interval that bounds var.
Definition: Box_inlines.hh:150
const C & inhomogeneous_term() const
Returns the inhomogeneous term of *this.