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