1 /* Declarations for the Sum_Floating_Point_Expression class and 2 its constituents. 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_Sum_Floating_Point_Expression_defs_hh 26 #define PPL_Sum_Floating_Point_Expression_defs_hh 1 27 28 #include "Floating_Point_Expression_defs.hh" 29 #include "globals_defs.hh" 30 #include "Sum_Floating_Point_Expression_types.hh" 31 #include <map> 32 33 namespace Parma_Polyhedra_Library { 34 35 //! Swaps \p x with \p y. 36 /*! \relates Sum_Floating_Point_Expression */ 37 template <typename FP_Interval_Type, typename FP_Format> 38 void swap(Sum_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x, 39 Sum_Floating_Point_Expression<FP_Interval_Type, FP_Format>& y); 40 41 /*! \brief 42 A generic Sum Floating Point Expression. 43 44 \ingroup PPL_CXX_interface 45 46 \par Template type parameters 47 48 - The class template type parameter \p FP_Interval_Type represents the type 49 of the intervals used in the abstract domain. 50 - The class template type parameter \p FP_Format represents the floating 51 point format used in the concrete domain. 52 53 \par Linearization of sum floating-point expressions 54 55 Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and 56 \f$i' + \sum_{v \in \cV}i'_{v}v \f$ 57 be two linear forms and \f$\aslf\f$ a sound abstract operator on linear 58 forms such that: 59 60 \f[ 61 \left(i + \sum_{v \in \cV}i_{v}v \right) 62 \aslf 63 \left(i' + \sum_{v \in \cV}i'_{v}v \right) 64 = 65 \left(i \asifp i'\right) 66 + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v} \right)v. 67 \f] 68 69 Given an expression \f$e_{1} \oplus e_{2}\f$ and a composite 70 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right 71 \rrbracket\f$, we construct the interval linear form 72 \f$\linexprenv{e_{1} \oplus e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$ 73 as follows: 74 \f[ 75 \linexprenv{e_{1} \oplus e_{2}}{\rho^{\#}}{\rho^{\#}_l} 76 = 77 \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} 78 \aslf 79 \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} 80 \aslf 81 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} 82 \right) 83 \aslf 84 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} 85 \right) 86 \aslf 87 mf_{\mathbf{f}}[-1, 1] 88 \f] 89 where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form computed by 90 calling method <CODE>Floating_Point_Expression::relative_error</CODE> 91 on \f$l\f$ and \f$mf_{\mathbf{f}}\f$ is a rounding error defined in 92 <CODE>Floating_Point_Expression::absolute_error</CODE>. 93 */ 94 template <typename FP_Interval_Type, typename FP_Format> 95 class Sum_Floating_Point_Expression 96 : public Floating_Point_Expression<FP_Interval_Type, FP_Format> { 97 98 public: 99 100 /*! \brief 101 Alias for the Linear_Form<FP_Interval_Type> from 102 Floating_Point_Expression. 103 */ 104 typedef typename 105 Floating_Point_Expression<FP_Interval_Type, FP_Format> 106 ::FP_Linear_Form FP_Linear_Form; 107 108 /*! \brief 109 Alias for the Box<FP_Interval_Type> from 110 Floating_Point_Expression. 111 */ 112 typedef typename 113 Floating_Point_Expression<FP_Interval_Type, FP_Format> 114 ::FP_Interval_Abstract_Store FP_Interval_Abstract_Store; 115 116 /*! \brief 117 Alias for the std::map<dimension_type, FP_Linear_Form> from 118 Floating_Point_Expression. 119 */ 120 typedef typename 121 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 122 FP_Linear_Form_Abstract_Store FP_Linear_Form_Abstract_Store; 123 124 /*! \brief 125 Alias for the FP_Interval_Type::boundary_type from 126 Floating_Point_Expression. 127 */ 128 typedef typename 129 Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type 130 boundary_type; 131 132 /*! \brief 133 Alias for the FP_Interval_Type::info_type from Floating_Point_Expression. 134 */ 135 typedef typename 136 Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type info_type; 137 138 //! \name Constructors and Destructor 139 //@{ 140 /*! \brief 141 Constructor with two parameters: builds the sum floating point expression 142 corresponding to \p x \f$\oplus\f$ \p y. 143 */ 144 Sum_Floating_Point_Expression( 145 Floating_Point_Expression<FP_Interval_Type, FP_Format>* const x, 146 Floating_Point_Expression<FP_Interval_Type, FP_Format>* const y); 147 148 //! Destructor. 149 ~Sum_Floating_Point_Expression(); 150 151 //@} // Constructors and Destructor 152 153 /*! \brief 154 Linearizes the expression in a given astract store. 155 156 Makes \p result become the linearization of \p *this in the given 157 composite abstract store. 158 159 \param int_store The interval abstract store. 160 \param lf_store The linear form abstract store. 161 \param result The modified linear form. 162 163 \return <CODE>true</CODE> if the linearization succeeded, 164 <CODE>false</CODE> otherwise. 165 166 Note that all variables occuring in the expressions represented 167 by \p first_operand and \p second_operand MUST have an associated value in 168 \p int_store. If this precondition is not met, calling the method 169 causes an undefined behavior. 170 171 See the class description for a detailed explanation of how \p result 172 is computed. 173 */ 174 bool linearize(const FP_Interval_Abstract_Store& int_store, 175 const FP_Linear_Form_Abstract_Store& lf_store, 176 FP_Linear_Form& result) const; 177 178 //! Swaps \p *this with \p y. 179 void m_swap(Sum_Floating_Point_Expression<FP_Interval_Type, FP_Format>& y); 180 181 private: 182 183 //! Pointer to the first operand. 184 Floating_Point_Expression<FP_Interval_Type, FP_Format>* first_operand; 185 //! Pointer to the second operand. 186 Floating_Point_Expression<FP_Interval_Type, FP_Format>* second_operand; 187 188 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 189 /*! \brief 190 Inhibited copy constructor. 191 */ 192 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 193 Sum_Floating_Point_Expression( 194 const Sum_Floating_Point_Expression<FP_Interval_Type, FP_Format>& e); 195 196 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 197 /*! \brief 198 Inhibited assignment operator. 199 */ 200 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 201 Sum_Floating_Point_Expression<FP_Interval_Type, FP_Format>& 202 operator=(const Sum_Floating_Point_Expression<FP_Interval_Type, 203 FP_Format>& e); 204 205 206 }; // class Sum_Floating_Point_Expression 207 208 } // namespace Parma_Polyhedra_Library 209 210 #include "Sum_Floating_Point_Expression_inlines.hh" 211 #include "Sum_Floating_Point_Expression_templates.hh" 212 213 #endif // !defined(PPL_Sum_Floating_Point_Expression_defs_hh) 214