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