1 /* Declarations for the Cast_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_Cast_Floating_Point_Expression_defs_hh 26 #define PPL_Cast_Floating_Point_Expression_defs_hh 1 27 28 #include "Floating_Point_Expression_defs.hh" 29 #include "globals_defs.hh" 30 #include "Cast_Floating_Point_Expression_types.hh" 31 #include <map> 32 33 namespace Parma_Polyhedra_Library { 34 35 //! Swaps \p x with \p y. 36 /*! \relates Cast_Floating_Point_Expression */ 37 template<typename FP_Interval_Type, typename FP_Format> 38 void 39 swap(Cast_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x, 40 Cast_Floating_Point_Expression<FP_Interval_Type, FP_Format>& y); 41 42 /*! \brief 43 A generic Cast 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 floating-point cast 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 and \f$\aslf\f$ a sound abstract operator on linear 59 forms such that: 60 61 \f[ 62 \left(i + \sum_{v \in \cV}i_{v}v \right) 63 \aslf 64 \left(i' + \sum_{v \in \cV}i'_{v}v \right) 65 = 66 \left(i \asifp i'\right) 67 + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v} \right)v. 68 \f] 69 70 Given a floating point expression \f$e\f$ and a composite abstract store 71 \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket\f$, 72 we construct the interval linear form 73 \f$\linexprenv{cast(e)}{\rho^{\#}}{\rho^{\#}_l}\f$ as follows: 74 \f[ 75 \linexprenv{cast(e)}{\rho^{\#}}{\rho^{\#}_l} 76 = 77 \linexprenv{e}{\rho^{\#}}{\rho^{\#}_l} 78 \aslf 79 \varepsilon_{\mathbf{f}}\left(\linexprenv{e}{\rho^{\#}}{\rho^{\#}_l} 80 \right) 81 \aslf 82 mf_{\mathbf{f}}[-1, 1] 83 \f] 84 where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the linear form computed by 85 calling method <CODE>Floating_Point_Expression::relative_error</CODE> 86 on \f$l\f$ and \f$mf_{\mathbf{f}}\f$ is a rounding error defined in 87 <CODE>Floating_Point_Expression::absolute_error</CODE>. 88 */ 89 template <typename FP_Interval_Type, typename FP_Format> 90 class Cast_Floating_Point_Expression 91 : public Floating_Point_Expression<FP_Interval_Type, FP_Format> { 92 93 public: 94 95 /*! \brief 96 Alias for the Linear_Form<FP_Interval_Type> from 97 Floating_Point_Expression 98 */ 99 typedef typename 100 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 101 FP_Linear_Form FP_Linear_Form; 102 103 /*! \brief 104 Alias for the Box<FP_Interval_Type> from 105 Floating_Point_Expression. 106 */ 107 typedef typename 108 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 109 FP_Interval_Abstract_Store FP_Interval_Abstract_Store; 110 111 /*! \brief 112 Alias for the std::map<dimension_type, FP_Linear_Form> from 113 Floating_Point_Expression. 114 */ 115 typedef typename 116 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 117 FP_Linear_Form_Abstract_Store FP_Linear_Form_Abstract_Store; 118 119 //! \name Constructors and Destructor 120 //@{ 121 /*! \brief 122 Builds a cast floating point expression with the value 123 expressed by \p expr. 124 */ 125 Cast_Floating_Point_Expression( 126 Floating_Point_Expression<FP_Interval_Type, FP_Format>* const expr); 127 128 //! Destructor. 129 ~Cast_Floating_Point_Expression(); 130 131 //@} // Constructors and Destructor 132 133 /*! \brief 134 Linearizes the expression in a given astract store. 135 136 Makes \p result become the linearization of \p *this in the given 137 composite abstract store. 138 139 \param int_store The interval abstract store. 140 \param lf_store The linear form abstract store. 141 \param result The modified linear form. 142 143 \return <CODE>true</CODE> if the linearization succeeded, 144 <CODE>false</CODE> otherwise. 145 146 See the class description for an explanation of how \p result is computed. 147 */ 148 bool linearize(const FP_Interval_Abstract_Store& int_store, 149 const FP_Linear_Form_Abstract_Store& lf_store, 150 FP_Linear_Form& result) const; 151 152 //! Swaps \p *this with \p y. 153 void m_swap(Cast_Floating_Point_Expression& y); 154 155 private: 156 157 //! Pointer to the casted expression. 158 Floating_Point_Expression<FP_Interval_Type, FP_Format>* expr; 159 160 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 161 /*! \brief 162 Inhibited copy constructor. 163 */ 164 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 165 Cast_Floating_Point_Expression( 166 const Cast_Floating_Point_Expression& y); 167 168 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 169 /*! \brief 170 Inhibited assignment operator. 171 */ 172 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAIL 173 Cast_Floating_Point_Expression& operator=( 174 const Cast_Floating_Point_Expression& y); 175 176 }; // class Cast_Floating_Point_Expression 177 178 } // namespace Parma_Polyhedra_Library 179 180 #include "Cast_Floating_Point_Expression_inlines.hh" 181 182 #endif // !defined(PPL_Cast_Floating_Point_Expression_defs_hh) 183