1 /* Linear_Form class declaration. 2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> 3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) 4 5 This file is part of the Parma Polyhedra Library (PPL). 6 7 The PPL is free software; you can redistribute it and/or modify it 8 under the terms of the GNU General Public License as published by the 9 Free Software Foundation; either version 3 of the License, or (at your 10 option) any later version. 11 12 The PPL is distributed in the hope that it will be useful, but WITHOUT 13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 15 for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software Foundation, 19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 20 21 For the most up-to-date information see the Parma Polyhedra Library 22 site: http://bugseng.com/products/ppl/ . */ 23 24 #ifndef PPL_Linear_Form_defs_hh 25 #define PPL_Linear_Form_defs_hh 1 26 27 #include "Linear_Form_types.hh" 28 #include "Linear_Expression_types.hh" 29 #include "Variable_defs.hh" 30 #include "Box_types.hh" 31 #include "Float_defs.hh" 32 #include <vector> 33 34 namespace Parma_Polyhedra_Library { 35 36 //! Swaps \p x with \p y. 37 /*! \relates Linear_Form */ 38 template <typename C> 39 void swap(Linear_Form<C>& x, Linear_Form<C>& y); 40 41 // Put them in the namespace here to declare them friend later. 42 43 //! Returns the linear form \p f1 + \p f2. 44 /*! \relates Linear_Form */ 45 template <typename C> 46 Linear_Form<C> 47 operator+(const Linear_Form<C>& f1, const Linear_Form<C>& f2); 48 49 //! Returns the linear form \p v + \p f. 50 /*! \relates Linear_Form */ 51 template <typename C> 52 Linear_Form<C> 53 operator+(Variable v, const Linear_Form<C>& f); 54 55 //! Returns the linear form \p f + \p v. 56 /*! \relates Linear_Form */ 57 template <typename C> 58 Linear_Form<C> 59 operator+(const Linear_Form<C>& f, Variable v); 60 61 //! Returns the linear form \p n + \p f. 62 /*! \relates Linear_Form */ 63 template <typename C> 64 Linear_Form<C> 65 operator+(const C& n, const Linear_Form<C>& f); 66 67 //! Returns the linear form \p f + \p n. 68 /*! \relates Linear_Form */ 69 template <typename C> 70 Linear_Form<C> 71 operator+(const Linear_Form<C>& f, const C& n); 72 73 //! Returns the linear form \p f. 74 /*! \relates Linear_Form */ 75 template <typename C> 76 Linear_Form<C> 77 operator+(const Linear_Form<C>& f); 78 79 //! Returns the linear form - \p f. 80 /*! \relates Linear_Form */ 81 template <typename C> 82 Linear_Form<C> 83 operator-(const Linear_Form<C>& f); 84 85 //! Returns the linear form \p f1 - \p f2. 86 /*! \relates Linear_Form */ 87 template <typename C> 88 Linear_Form<C> 89 operator-(const Linear_Form<C>& f1, const Linear_Form<C>& f2); 90 91 //! Returns the linear form \p v - \p f. 92 /*! \relates Linear_Form */ 93 template <typename C> 94 Linear_Form<C> 95 operator-(Variable v, const Linear_Form<C>& f); 96 97 //! Returns the linear form \p f - \p v. 98 /*! \relates Linear_Form */ 99 template <typename C> 100 Linear_Form<C> 101 operator-(const Linear_Form<C>& f, Variable v); 102 103 //! Returns the linear form \p n - \p f. 104 /*! \relates Linear_Form */ 105 template <typename C> 106 Linear_Form<C> 107 operator-(const C& n, const Linear_Form<C>& f); 108 109 //! Returns the linear form \p f - \p n. 110 /*! \relates Linear_Form */ 111 template <typename C> 112 Linear_Form<C> 113 operator-(const Linear_Form<C>& f, const C& n); 114 115 //! Returns the linear form \p n * \p f. 116 /*! \relates Linear_Form */ 117 template <typename C> 118 Linear_Form<C> 119 operator*(const C& n, const Linear_Form<C>& f); 120 121 //! Returns the linear form \p f * \p n. 122 /*! \relates Linear_Form */ 123 template <typename C> 124 Linear_Form<C> 125 operator*(const Linear_Form<C>& f, const C& n); 126 127 //! Returns the linear form \p f1 + \p f2 and assigns it to \p e1. 128 /*! \relates Linear_Form */ 129 template <typename C> 130 Linear_Form<C>& 131 operator+=(Linear_Form<C>& f1, const Linear_Form<C>& f2); 132 133 //! Returns the linear form \p f + \p v and assigns it to \p f. 134 /*! \relates Linear_Form 135 \exception std::length_error 136 Thrown if the space dimension of \p v exceeds 137 <CODE>Linear_Form::max_space_dimension()</CODE>. 138 */ 139 template <typename C> 140 Linear_Form<C>& 141 operator+=(Linear_Form<C>& f, Variable v); 142 143 //! Returns the linear form \p f + \p n and assigns it to \p f. 144 /*! \relates Linear_Form */ 145 template <typename C> 146 Linear_Form<C>& 147 operator+=(Linear_Form<C>& f, const C& n); 148 149 //! Returns the linear form \p f1 - \p f2 and assigns it to \p f1. 150 /*! \relates Linear_Form */ 151 template <typename C> 152 Linear_Form<C>& 153 operator-=(Linear_Form<C>& f1, const Linear_Form<C>& f2); 154 155 //! Returns the linear form \p f - \p v and assigns it to \p f. 156 /*! \relates Linear_Form 157 \exception std::length_error 158 Thrown if the space dimension of \p v exceeds 159 <CODE>Linear_Form::max_space_dimension()</CODE>. 160 */ 161 template <typename C> 162 Linear_Form<C>& 163 operator-=(Linear_Form<C>& f, Variable v); 164 165 //! Returns the linear form \p f - \p n and assigns it to \p f. 166 /*! \relates Linear_Form */ 167 template <typename C> 168 Linear_Form<C>& 169 operator-=(Linear_Form<C>& f, const C& n); 170 171 //! Returns the linear form \p n * \p f and assigns it to \p f. 172 /*! \relates Linear_Form */ 173 template <typename C> 174 Linear_Form<C>& 175 operator*=(Linear_Form<C>& f, const C& n); 176 177 //! Returns the linear form \p f / \p n and assigns it to \p f. 178 /*! 179 \relates Linear_Form 180 Performs the division of a linear form by a scalar. It is up to the user to 181 ensure that division by 0 is not performed. 182 */ 183 template <typename C> 184 Linear_Form<C>& 185 operator/=(Linear_Form<C>& f, const C& n); 186 187 //! Returns <CODE>true</CODE> if and only if \p x and \p y are equal. 188 /*! \relates Linear_Form */ 189 template <typename C> 190 bool 191 operator==(const Linear_Form<C>& x, const Linear_Form<C>& y); 192 193 //! Returns <CODE>true</CODE> if and only if \p x and \p y are different. 194 /*! \relates Linear_Form */ 195 template <typename C> 196 bool 197 operator!=(const Linear_Form<C>& x, const Linear_Form<C>& y); 198 199 namespace IO_Operators { 200 201 //! Output operator. 202 /*! \relates Parma_Polyhedra_Library::Linear_Form */ 203 template <typename C> 204 std::ostream& operator<<(std::ostream& s, const Linear_Form<C>& f); 205 206 } // namespace IO_Operators 207 208 } // namespace Parma_Polyhedra_Library 209 210 //! A linear form with interval coefficients. 211 /*! \ingroup PPL_CXX_interface 212 An object of the class Linear_Form represents the interval linear form 213 \f[ 214 \sum_{i=0}^{n-1} a_i x_i + b 215 \f] 216 where \f$n\f$ is the dimension of the vector space, 217 each \f$a_i\f$ is the coefficient 218 of the \f$i\f$-th variable \f$x_i\f$ 219 and \f$b\f$ is the inhomogeneous term. 220 The coefficients and the inhomogeneous term of the linear form 221 have the template parameter \p C as their type. \p C must be the 222 type of an Interval. 223 224 \par How to build a linear form. 225 A full set of functions is defined in order to provide a convenient 226 interface for building complex linear forms starting from simpler ones 227 and from objects of the classes Variable and \p C. Available operators 228 include binary addition and subtraction, as well as multiplication and 229 division by a coefficient. 230 The space dimension of a linear form is defined as 231 the highest variable dimension among variables that have a nonzero 232 coefficient in the linear form, or zero if no such variable exists. 233 The space dimension for each variable \f$x_i\f$ is given by \f$i + 1\f$. 234 235 \par Example 236 Given the type \p T of an Interval with floating point coefficients (though 237 any integral type may also be used), the following code builds the interval 238 linear form \f$lf = x_5 - x_2 + 1\f$ with space dimension 6: 239 \code 240 Variable x5(5); 241 Variable x2(2); 242 T x5_coefficient; 243 x5_coefficient.lower() = 2.0; 244 x5_coefficient.upper() = 3.0; 245 T inhomogeneous_term; 246 inhomogeneous_term.lower() = 4.0; 247 inhomogeneous_term.upper() = 8.0; 248 Linear_Form<T> lf(x2); 249 lf = -lf; 250 lf += Linear_Form<T>(x2); 251 Linear_Form<T> lf_x5(x5); 252 lf_x5 *= x5_coefficient; 253 lf += lf_x5; 254 \endcode 255 Note that \c lf_x5 is created with space dimension 6, while \c lf is 256 created with space dimension 0 and then extended first to space 257 dimension 2 when \c x2 is subtracted and finally to space dimension 258 6 when \c lf_x5 is added. 259 */ 260 template <typename C> 261 class Parma_Polyhedra_Library::Linear_Form { 262 public: 263 //! Default constructor: returns a copy of Linear_Form::zero(). 264 Linear_Form(); 265 266 //! Ordinary copy constructor. 267 Linear_Form(const Linear_Form& f); 268 269 //! Destructor. 270 ~Linear_Form(); 271 272 //! Builds the linear form corresponding to the inhomogeneous term \p n. 273 explicit Linear_Form(const C& n); 274 275 //! Builds the linear form corresponding to the variable \p v. 276 /*! 277 \exception std::length_error 278 Thrown if the space dimension of \p v exceeds 279 <CODE>Linear_Form::max_space_dimension()</CODE>. 280 */ 281 Linear_Form(Variable v); 282 283 //! Builds a linear form approximating the linear expression \p e. 284 Linear_Form(const Linear_Expression& e); 285 286 //! Returns the maximum space dimension a Linear_Form can handle. 287 static dimension_type max_space_dimension(); 288 289 //! Returns the dimension of the vector space enclosing \p *this. 290 dimension_type space_dimension() const; 291 292 //! Returns the coefficient of \p v in \p *this. 293 const C& coefficient(Variable v) const; 294 295 //! Returns the inhomogeneous term of \p *this. 296 const C& inhomogeneous_term() const; 297 298 //! Negates all the coefficients of \p *this. 299 void negate(); 300 301 /*! \brief 302 Returns a lower bound to the total size in bytes of the memory 303 occupied by \p *this. 304 */ 305 memory_size_type total_memory_in_bytes() const; 306 307 //! Returns the size in bytes of the memory managed by \p *this. 308 memory_size_type external_memory_in_bytes() const; 309 310 PPL_OUTPUT_DECLARATIONS 311 312 /*! \brief 313 Loads from \p s an ASCII representation (as produced by 314 ascii_dump(std::ostream&) const) and sets \p *this accordingly. 315 Returns <CODE>true</CODE> if successful, <CODE>false</CODE> otherwise. 316 */ 317 bool ascii_load(std::istream& s); 318 319 //! Checks if all the invariants are satisfied. 320 bool OK() const; 321 322 //! Swaps \p *this with \p y. 323 void m_swap(Linear_Form& y); 324 325 // Floating point analysis related methods. 326 327 /*! \brief 328 Verifies if the linear form overflows. 329 330 \return 331 Returns <CODE>false</CODE> if all coefficients in \p lf are bounded, 332 <CODE>true</CODE> otherwise. 333 334 \p T must be the type of possibly unbounded quantities. 335 */ 336 bool overflows() const; 337 338 /*! \brief 339 Computes the relative error associated to floating point computations 340 that operate on a quantity that is overapproximated by \p *this. 341 342 \param analyzed_format The floating point format used by the analyzed 343 program. 344 \param result Becomes the linear form corresponding to the relative 345 error committed. 346 347 This method makes <CODE>result</CODE> become a linear form 348 obtained by evaluating the function \f$\varepsilon_{\mathbf{f}}(l)\f$ 349 on the linear form. This function is defined as: 350 \f[ 351 \varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right) 352 \defeq 353 (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}]) 354 + 355 \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) 356 \amifp 357 [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v 358 \f] 359 where p is the fraction size in bits for the format \f$\mathbf{f}\f$ and 360 \f$\beta\f$ the base. 361 362 The result is undefined if \p T is not the type of an interval with 363 floating point boundaries. 364 */ 365 void relative_error(Floating_Point_Format analyzed_format, 366 Linear_Form& result) const; 367 368 /*! \brief 369 Makes \p result become an interval that overapproximates all the 370 possible values of \p *this. 371 372 \param oracle The FP_Oracle to be queried. 373 \param result The linear form that will store the result. 374 375 \return <CODE>true</CODE> if the operation was successful, 376 <CODE>false</CODE> otherwise (the possibility of failure 377 depends on the oracle's implementation). 378 379 \par Template type parameters 380 381 - The class template parameter \p Target specifies the implementation 382 of Concrete_Expression to be used. 383 384 This method makes <CODE>result</CODE> become 385 \f$\iota(lf)\rho^{\#}\f$, that is an interval defined as: 386 \f[ 387 \iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{\#} 388 \defeq 389 i \asifp \left(\bigoplus_{v \in \cV}{}^{\#}i_{v} \amifp 390 \rho^{\#}(v)\right) 391 \f] 392 where \f$\rho^{\#}(v)\f$ is an interval (provided by the oracle) 393 that correctly approximates the value of \f$v\f$. 394 395 The result is undefined if \p C is not the type of an interval with 396 floating point boundaries. 397 */ 398 template <typename Target> 399 bool intervalize(const FP_Oracle<Target,C>& oracle, C& result) const; 400 401 private: 402 //! The generic coefficient equal to the singleton zero. 403 static C zero; 404 405 //! Type of the container vector. 406 typedef std::vector<C> vec_type; 407 408 //! The container vector. 409 vec_type vec; 410 411 //! Implementation sizing constructor. 412 /*! 413 The bool parameter is just to avoid problems with 414 the constructor Linear_Form(const C& n). 415 */ 416 Linear_Form(dimension_type sz, bool); 417 418 /*! \brief 419 Builds the linear form corresponding to the difference of 420 \p v and \p w. 421 422 \exception std::length_error 423 Thrown if the space dimension of \p v or the one of \p w exceed 424 <CODE>Linear_Form::max_space_dimension()</CODE>. 425 */ 426 Linear_Form(Variable v, Variable w); 427 428 //! Gives the number of generic coefficients currently in use. 429 dimension_type size() const; 430 431 //! Extends the vector of \p *this to size \p sz. 432 void extend(dimension_type sz); 433 434 //! Returns a reference to \p vec[i]. 435 C& operator[](dimension_type i); 436 437 //! Returns a const reference to \p vec[i]. 438 const C& operator[](dimension_type i) const; 439 440 friend Linear_Form<C> 441 operator+<C>(const Linear_Form<C>& f1, const Linear_Form<C>& f2); 442 friend Linear_Form<C> 443 operator+<C>(const C& n, const Linear_Form<C>& f); 444 friend Linear_Form<C> 445 operator+<C>(const Linear_Form<C>& f, const C& n); 446 friend Linear_Form<C> 447 operator+<C>(Variable v, const Linear_Form<C>& f); 448 449 friend Linear_Form<C> 450 operator-<C>(const Linear_Form<C>& f); 451 452 friend Linear_Form<C> 453 operator-<C>(const Linear_Form<C>& f1, const Linear_Form<C>& f2); 454 friend Linear_Form<C> 455 operator-<C>(const C& n, const Linear_Form<C>& f); 456 friend Linear_Form<C> 457 operator-<C>(const Linear_Form<C>& f, const C& n); 458 friend Linear_Form<C> 459 operator-<C>(Variable v, const Linear_Form<C>& f); 460 friend Linear_Form<C> 461 operator-<C>(const Linear_Form<C>& f, Variable v); 462 463 friend Linear_Form<C> 464 operator*<C>(const C& n, const Linear_Form<C>& f); 465 friend Linear_Form<C> 466 operator*<C>(const Linear_Form<C>& f, const C& n); 467 468 friend Linear_Form<C>& 469 operator+=<C>(Linear_Form<C>& f1, const Linear_Form<C>& f2); 470 friend Linear_Form<C>& 471 operator+=<C>(Linear_Form<C>& f, Variable v); 472 friend Linear_Form<C>& 473 operator+=<C>(Linear_Form<C>& f, const C& n); 474 475 friend Linear_Form<C>& 476 operator-=<C>(Linear_Form<C>& f1, const Linear_Form<C>& f2); 477 friend Linear_Form<C>& 478 operator-=<C>(Linear_Form<C>& f, Variable v); 479 friend Linear_Form<C>& 480 operator-=<C>(Linear_Form<C>& f, const C& n); 481 482 friend Linear_Form<C>& 483 operator*=<C>(Linear_Form<C>& f, const C& n); 484 485 friend Linear_Form<C>& 486 operator/=<C>(Linear_Form<C>& f, const C& n); 487 488 friend bool 489 operator==<C>(const Linear_Form<C>& x, const Linear_Form<C>& y); 490 491 friend std::ostream& 492 Parma_Polyhedra_Library::IO_Operators 493 ::operator<<<C>(std::ostream& s, const Linear_Form<C>& f); 494 }; 495 496 #include "Linear_Form_inlines.hh" 497 // Linear_Form_templates.hh is not included here on purpose. 498 499 #endif // !defined(PPL_Linear_Form_defs_hh) 500