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