1 /* Declarations for the Variable_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_Variable_Floating_Point_Expression_defs_hh 26 #define PPL_Variable_Floating_Point_Expression_defs_hh 1 27 28 #include "Floating_Point_Expression_defs.hh" 29 #include "globals_defs.hh" 30 #include "Variable_Floating_Point_Expression_types.hh" 31 #include <map> 32 #include <utility> 33 34 namespace Parma_Polyhedra_Library { 35 36 //! Swaps \p x with \p y. 37 /*! \relates Variable_Floating_Point_Expression */ 38 template<typename FP_Interval_Type, typename FP_Format> 39 void swap(Variable_Floating_Point_Expression<FP_Interval_Type, FP_Format>& x, 40 Variable_Floating_Point_Expression<FP_Interval_Type, FP_Format>& y); 41 42 /*! \brief 43 A generic Variable 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 variable expressions 55 56 Given a variable expression \f$v\f$ and a composite 57 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right 58 \rrbracket\f$, we construct the interval 59 linear form \f$\linexprenv{v}{\rho^{\#}}{\rho^{\#}_l}\f$ as 60 \f$\rho^{\#}_l(v)\f$ if it is defined; otherwise we construct it as 61 \f$[-1, 1]v\f$. 62 */ 63 template <typename FP_Interval_Type, typename FP_Format> 64 class Variable_Floating_Point_Expression 65 : public Floating_Point_Expression<FP_Interval_Type, FP_Format> { 66 67 public: 68 69 /*! \brief 70 Alias for the Linear_Form<FP_Interval_Type> from 71 Floating_Point_Expression 72 */ 73 typedef typename 74 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 75 FP_Linear_Form FP_Linear_Form; 76 77 /*! \brief 78 Alias for the Box<FP_Interval_Type> from 79 Floating_Point_Expression. 80 */ 81 typedef typename 82 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 83 FP_Interval_Abstract_Store FP_Interval_Abstract_Store; 84 85 /*! \brief 86 Alias for the std::map<dimension_type, FP_Linear_Form> from 87 Floating_Point_Expression. 88 */ 89 typedef typename 90 Floating_Point_Expression<FP_Interval_Type, FP_Format>:: 91 FP_Linear_Form_Abstract_Store FP_Linear_Form_Abstract_Store; 92 93 /*! \brief 94 Alias for the FP_Interval_Type::boundary_type from 95 Floating_Point_Expression. 96 */ 97 typedef typename 98 Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type 99 boundary_type; 100 101 /*! \brief 102 Alias for the FP_Interval_Type::info_type from Floating_Point_Expression. 103 */ 104 typedef typename 105 Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type info_type; 106 107 //! \name Constructors and Destructor 108 //@{ 109 /*! \brief 110 Constructor with a parameter: builds the variable floating point 111 expression corresponding to the variable having \p v_index as its index. 112 */ 113 explicit Variable_Floating_Point_Expression(const dimension_type v_index); 114 115 //! Destructor. 116 ~Variable_Floating_Point_Expression(); 117 118 //@} // Constructors and Destructor 119 120 /*! \brief 121 Linearizes the expression in a given abstract store. 122 123 Makes \p result become the linearization of \p *this in the given 124 composite abstract store. 125 126 \param int_store The interval abstract store. 127 \param lf_store The linear form abstract store. 128 \param result The modified linear form. 129 130 \return <CODE>true</CODE> if the linearization succeeded, 131 <CODE>false</CODE> otherwise. 132 133 Note that the variable in the expression MUST have an associated value 134 in \p int_store. If this precondition is not met, calling the method 135 causes an undefined behavior. 136 137 See the class description for a detailed explanation of how \p result is 138 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 /*! \brief 145 Assigns a linear form to the variable with the same index of 146 \p *this in a given linear form abstract store. 147 148 \param lf The linear form assigned to the variable. 149 \param lf_store The linear form abstract store. 150 151 Note that once \p lf is assigned to a variable, all the other entries 152 of \p lf_store which contain that variable are discarded. 153 */ 154 void linear_form_assign(const FP_Linear_Form& lf, 155 FP_Linear_Form_Abstract_Store& lf_store) const; 156 157 //! Swaps \p *this with \p y. 158 void m_swap(Variable_Floating_Point_Expression& y); 159 160 private: 161 162 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 163 /*! \brief 164 Inhibited copy constructor. 165 */ 166 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 167 Variable_Floating_Point_Expression( 168 const Variable_Floating_Point_Expression& y); 169 170 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 171 /*! \brief 172 Inhibited assignment operator. 173 */ 174 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS 175 Variable_Floating_Point_Expression& operator=( 176 const Variable_Floating_Point_Expression& y); 177 178 //! The index of the variable. 179 dimension_type variable_index; 180 181 }; // class Variable_Floating_Point_Expression 182 183 } // namespace Parma_Polyhedra_Library 184 185 #include "Variable_Floating_Point_Expression_inlines.hh" 186 187 #endif // !defined(PPL_Variable_Floating_Point_Expression_defs_hh) 188