1 /* Declarations for the Constant_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_Constant_Floating_Point_Expression_defs_hh 26 #define PPL_Constant_Floating_Point_Expression_defs_hh 1 27 28 #include "Floating_Point_Expression_defs.hh" 29 #include "globals_defs.hh" 30 #include "Constant_Floating_Point_Expression_types.hh" 31 #include <map> 32 33 namespace Parma_Polyhedra_Library { 34 35 //! Swaps \p x with \p y. 36 /*! \relates Constant_Floating_Point_Expression */ 37 template<typename FP_Interval_Type, typename FP_Format> 38 void swap(Constant_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x, 39 Constant_Floating_Point_Expression<FP_Interval_Type, FP_Format>& y); 40 41 /*! \brief 42 A generic Constant 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 floating-point constant expressions 54 55 The linearization of a constant floating point expression results in a 56 linear form consisting of only the inhomogeneous term 57 \f$[l, u]\f$, where \f$l\f$ and \f$u\f$ are the lower 58 and upper bounds of the constant value given to the class constructor. 59 */ 60 template <typename FP_Interval_Type, typename FP_Format> 61 class Constant_Floating_Point_Expression 62 : public Floating_Point_Expression<FP_Interval_Type, FP_Format> { 63 64 public: 65 66 /*! \brief 67 Alias for the Linear_Form<FP_Interval_Type> from 68 Floating_Point_Expression 69 */ 70 typedef typename 71 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 72 FP_Linear_Form FP_Linear_Form; 73 74 /*! \brief 75 Alias for the Box<FP_Interval_Type> from 76 Floating_Point_Expression. 77 */ 78 typedef typename 79 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 80 FP_Interval_Abstract_Store FP_Interval_Abstract_Store; 81 82 /*! \brief 83 Alias for the std::map<dimension_type, FP_Linear_Form> from 84 Floating_Point_Expression. 85 */ 86 typedef typename 87 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 88 FP_Linear_Form_Abstract_Store FP_Linear_Form_Abstract_Store; 89 90 /*! \brief 91 Alias for the FP_Interval_Type::boundary_type from 92 Floating_Point_Expression. 93 */ 94 typedef typename 95 Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type 96 boundary_type; 97 98 /*! \brief 99 Alias for the FP_Interval_Type::info_type from Floating_Point_Expression. 100 */ 101 typedef typename 102 Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type info_type; 103 104 //! \name Constructors and Destructor 105 //@{ 106 /*! \brief 107 Constructor with two parameters: builds the constant floating point 108 expression from a \p lower_bound and an \p upper_bound of its 109 value in the concrete domain. 110 */ 111 Constant_Floating_Point_Expression(const boundary_type lower_bound, 112 const boundary_type upper_bound); 113 114 /*! \brief 115 Builds a constant floating point expression with the value 116 expressed by the string \p str_value. 117 */ 118 Constant_Floating_Point_Expression(const char* str_value); 119 120 //! Destructor. 121 ~Constant_Floating_Point_Expression(); 122 123 //@} // Constructors and Destructor 124 125 /*! \brief 126 Linearizes the expression in a given astract store. 127 128 Makes \p result become the linearization of \p *this in the given 129 composite abstract store. 130 131 \param int_store The interval abstract store. 132 \param lf_store The linear form abstract store. 133 \param result The modified linear form. 134 135 \return <CODE>true</CODE> if the linearization succeeded, 136 <CODE>false</CODE> otherwise. 137 138 See the class description for an explanation of how \p result is computed. 139 */ 140 bool linearize(const FP_Interval_Abstract_Store& int_store, 141 const FP_Linear_Form_Abstract_Store& lf_store, 142 FP_Linear_Form& result) const; 143 144 //! Swaps \p *this with \p y. 145 void m_swap(Constant_Floating_Point_Expression& y); 146 147 private: 148 149 FP_Interval_Type value; 150 151 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 152 /*! \brief 153 Inhibited copy constructor. 154 */ 155 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 156 Constant_Floating_Point_Expression( 157 const Constant_Floating_Point_Expression& y); 158 159 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 160 /*! \brief 161 Inhibited assignment operator. 162 */ 163 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAIL 164 Constant_Floating_Point_Expression& operator=( 165 const Constant_Floating_Point_Expression& y); 166 167 }; // class Constant_Floating_Point_Expression 168 169 } // namespace Parma_Polyhedra_Library 170 171 #include "Constant_Floating_Point_Expression_inlines.hh" 172 173 #endif // !defined(PPL_Constant_Floating_Point_Expression_defs_hh) 174