1 /* Declarations for the Opposite_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_Opposite_Floating_Point_Expression_defs_hh 26 #define PPL_Opposite_Floating_Point_Expression_defs_hh 1 27 28 #include "Floating_Point_Expression_defs.hh" 29 #include "globals_defs.hh" 30 #include "Opposite_Floating_Point_Expression_types.hh" 31 #include <map> 32 33 namespace Parma_Polyhedra_Library { 34 35 //! Swaps \p x with \p y. 36 /*! \relates Opposite_Floating_Point_Expression */ 37 template<typename FP_Interval_Type, typename FP_Format> 38 void swap(Opposite_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x, 39 Opposite_Floating_Point_Expression<FP_Interval_Type, FP_Format>& y); 40 41 /*! \brief 42 A generic Opposite 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 opposite floating-point expressions 54 55 Let \f$i + \sum_{v \in \cV}i_{v}v \f$ be an interval linear form and 56 let \f$\adlf\f$ be a sound unary operator on linear forms such that: 57 58 \f[ 59 \adlf 60 \left(i + \sum_{v \in \cV}i_{v}v\right) 61 = 62 \left(\adifp i\right) 63 + \sum_{v \in \cV}\left(\adifp i_{v} \right)v, 64 \f] 65 66 Given a floating point expression \f$\ominus e\f$ and a composite 67 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right 68 \rrbracket\f$, we construct the interval linear form 69 \f$\linexprenv{\ominus e}{\rho^{\#}}{\rho^{\#}_l}\f$ 70 as follows: 71 \f[ 72 \linexprenv{\ominus e}{\rho^{\#}}{\rho^{\#}_l} 73 = 74 \adlf 75 \left( 76 \linexprenv{e}{\rho^{\#}}{\rho^{\#}_l} 77 \right). 78 \f] 79 */ 80 template <typename FP_Interval_Type, typename FP_Format> 81 class Opposite_Floating_Point_Expression 82 : public Floating_Point_Expression<FP_Interval_Type, FP_Format> { 83 84 public: 85 86 /*! \brief 87 Alias for the Linear_Form<FP_Interval_Type> from 88 Floating_Point_Expression 89 */ 90 typedef typename 91 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 92 FP_Linear_Form FP_Linear_Form; 93 94 /*! \brief 95 Alias for the std::map<dimension_type, FP_Interval_Type> from 96 Floating_Point_Expression. 97 */ 98 typedef typename 99 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 100 FP_Interval_Abstract_Store FP_Interval_Abstract_Store; 101 102 /*! \brief 103 Alias for the std::map<dimension_type, FP_Linear_Form> from 104 Floating_Point_Expression. 105 */ 106 typedef typename 107 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 108 FP_Linear_Form_Abstract_Store FP_Linear_Form_Abstract_Store; 109 110 /*! \brief 111 Alias for the FP_Interval_Type::boundary_type from 112 Floating_Point_Expression. 113 */ 114 typedef typename 115 Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type 116 boundary_type; 117 118 /*! \brief 119 Alias for the FP_Interval_Type::info_type from Floating_Point_Expression. 120 */ 121 typedef typename 122 Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type info_type; 123 124 //! \name Constructors and Destructor 125 //@{ 126 /*! \brief 127 Constructor with one parameter: builds the opposite floating point 128 expression \f$\ominus\f$ \p op. 129 */ 130 explicit Opposite_Floating_Point_Expression( 131 Floating_Point_Expression<FP_Interval_Type, FP_Format>* const op); 132 133 //! Destructor. 134 ~Opposite_Floating_Point_Expression(); 135 136 //@} // Constructors and Destructor 137 138 /*! \brief 139 Linearizes the expression in a given astract store. 140 141 Makes \p result become the linearization of \p *this in the given 142 composite abstract store. 143 144 \param int_store The interval abstract store. 145 \param lf_store The linear form abstract store. 146 \param result The modified linear form. 147 148 \return <CODE>true</CODE> if the linearization succeeded, 149 <CODE>false</CODE> otherwise. 150 151 Note that all variables occuring in the expression represented 152 by \p operand MUST have an associated value in \p int_store. 153 If this precondition is not met, calling the method 154 causes an undefined behavior. 155 156 See the class description for a detailed explanation of how \p result 157 is computed. 158 */ 159 bool linearize(const FP_Interval_Abstract_Store& int_store, 160 const FP_Linear_Form_Abstract_Store& lf_store, 161 FP_Linear_Form& result) const; 162 163 //! Swaps \p *this with \p y. 164 void m_swap(Opposite_Floating_Point_Expression& y); 165 166 private: 167 168 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 169 /*! \brief 170 Inhibited copy constructor. 171 */ 172 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 173 Opposite_Floating_Point_Expression( 174 const Opposite_Floating_Point_Expression& y); 175 176 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 177 /*! \brief 178 Inhibited assignment operator. 179 */ 180 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 181 Opposite_Floating_Point_Expression& operator=( 182 const Opposite_Floating_Point_Expression& y); 183 184 //! Pointer to the operand. 185 Floating_Point_Expression<FP_Interval_Type, FP_Format>* operand; 186 187 }; // class Opposite_Floating_Point_Expression 188 189 } // namespace Parma_Polyhedra_Library 190 191 #include "Opposite_Floating_Point_Expression_inlines.hh" 192 193 #endif // !defined(PPL_Opposite_Floating_Point_Expression_defs_hh) 194