1 /* Congruence 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_Congruence_defs_hh 25 #define PPL_Congruence_defs_hh 1 26 27 #include "Congruence_types.hh" 28 29 #include "Coefficient_defs.hh" 30 #include "Variable_defs.hh" 31 32 #include "Constraint_types.hh" 33 #include "Grid_types.hh" 34 #include "Scalar_Products_types.hh" 35 #include "Linear_Expression_defs.hh" 36 #include "Expression_Adapter_defs.hh" 37 38 #include <iosfwd> 39 #include <vector> 40 41 // These are declared here because they are friend of Congruence. 42 namespace Parma_Polyhedra_Library { 43 44 //! Returns <CODE>true</CODE> if and only if \p x and \p y are equivalent. 45 /*! \relates Congruence */ 46 bool 47 operator==(const Congruence& x, const Congruence& y); 48 49 //! Returns <CODE>false</CODE> if and only if \p x and \p y are equivalent. 50 /*! \relates Congruence */ 51 bool 52 operator!=(const Congruence& x, const Congruence& y); 53 54 } // namespace Parma_Polyhedra_Library 55 56 57 //! A linear congruence. 58 /*! \ingroup PPL_CXX_interface 59 An object of the class Congruence is a congruence: 60 - \f$\cg = \sum_{i=0}^{n-1} a_i x_i + b = 0 \pmod m\f$ 61 62 where \f$n\f$ is the dimension of the space, 63 \f$a_i\f$ is the integer coefficient of variable \f$x_i\f$, 64 \f$b\f$ is the integer inhomogeneous term and \f$m\f$ is the integer modulus; 65 if \f$m = 0\f$, then \f$\cg\f$ represents the equality congruence 66 \f$\sum_{i=0}^{n-1} a_i x_i + b = 0\f$ 67 and, if \f$m \neq 0\f$, then the congruence \f$\cg\f$ is 68 said to be a proper congruence. 69 70 \par How to build a congruence 71 Congruences \f$\pmod{1}\f$ are typically built by 72 applying the congruence symbol `<CODE>\%=</CODE>' 73 to a pair of linear expressions. 74 Congruences with modulus \p m 75 are typically constructed by building a congruence \f$\pmod{1}\f$ 76 using the given pair of linear expressions 77 and then adding the modulus \p m 78 using the modulus symbol is `<CODE>/</CODE>'. 79 80 The space dimension of a congruence is defined as the maximum 81 space dimension of the arguments of its constructor. 82 83 \par 84 In the following examples it is assumed that variables 85 <CODE>x</CODE>, <CODE>y</CODE> and <CODE>z</CODE> 86 are defined as follows: 87 \code 88 Variable x(0); 89 Variable y(1); 90 Variable z(2); 91 \endcode 92 93 \par Example 1 94 The following code builds the equality congruence 95 \f$3x + 5y - z = 0\f$, having space dimension \f$3\f$: 96 \code 97 Congruence eq_cg((3*x + 5*y - z %= 0) / 0); 98 \endcode 99 The following code builds the congruence 100 \f$4x = 2y - 13 \pmod{1}\f$, having space dimension \f$2\f$: 101 \code 102 Congruence mod1_cg(4*x %= 2*y - 13); 103 \endcode 104 The following code builds the congruence 105 \f$4x = 2y - 13 \pmod{2}\f$, having space dimension \f$2\f$: 106 \code 107 Congruence mod2_cg((4*x %= 2*y - 13) / 2); 108 \endcode 109 An unsatisfiable congruence on the zero-dimension space \f$\Rset^0\f$ 110 can be specified as follows: 111 \code 112 Congruence false_cg = Congruence::zero_dim_false(); 113 \endcode 114 Equivalent, but more involved ways are the following: 115 \code 116 Congruence false_cg1((Linear_Expression::zero() %= 1) / 0); 117 Congruence false_cg2((Linear_Expression::zero() %= 1) / 2); 118 \endcode 119 In contrast, the following code defines an unsatisfiable congruence 120 having space dimension \f$3\f$: 121 \code 122 Congruence false_cg3((0*z %= 1) / 0); 123 \endcode 124 125 \par How to inspect a congruence 126 Several methods are provided to examine a congruence and extract 127 all the encoded information: its space dimension, its modulus 128 and the value of its integer coefficients. 129 130 \par Example 2 131 The following code shows how it is possible to access the modulus 132 as well as each of the coefficients. 133 Given a congruence with linear expression \p e and modulus \p m 134 (in this case \f$x - 5y + 3z = 4 \pmod{5}\f$), we construct a new 135 congruence with the same modulus \p m but where the linear 136 expression is \f$2 e\f$ (\f$2x - 10y + 6z = 8 \pmod{5}\f$). 137 \code 138 Congruence cg1((x - 5*y + 3*z %= 4) / 5); 139 cout << "Congruence cg1: " << cg1 << endl; 140 const Coefficient& m = cg1.modulus(); 141 if (m == 0) 142 cout << "Congruence cg1 is an equality." << endl; 143 else { 144 Linear_Expression e; 145 for (dimension_type i = cg1.space_dimension(); i-- > 0; ) 146 e += 2 * cg1.coefficient(Variable(i)) * Variable(i); 147 e += 2 * cg1.inhomogeneous_term(); 148 Congruence cg2((e %= 0) / m); 149 cout << "Congruence cg2: " << cg2 << endl; 150 } 151 \endcode 152 The actual output could be the following: 153 \code 154 Congruence cg1: A - 5*B + 3*C %= 4 / 5 155 Congruence cg2: 2*A - 10*B + 6*C %= 8 / 5 156 \endcode 157 Note that, in general, the particular output obtained can be 158 syntactically different from the (semantically equivalent) 159 congruence considered. 160 */ 161 class Parma_Polyhedra_Library::Congruence { 162 public: 163 164 //! The representation used for new Congruences. 165 /*! 166 \note The copy constructor and the copy constructor with specified size 167 use the representation of the original object, so that it is 168 indistinguishable from the original object. 169 */ 170 static const Representation default_representation = SPARSE; 171 172 //! Constructs the 0 = 0 congruence with space dimension \p 0 . 173 explicit Congruence(Representation r = default_representation); 174 175 //! Ordinary copy constructor. 176 /*! 177 \note The new Congruence will have the same representation as `cg', 178 not default_representation, so that they are indistinguishable. 179 */ 180 Congruence(const Congruence& cg); 181 182 //! Copy constructor with specified representation. 183 Congruence(const Congruence& cg, Representation r); 184 185 //! Copy-constructs (modulo 0) from equality constraint \p c. 186 /*! 187 \exception std::invalid_argument 188 Thrown if \p c is an inequality. 189 */ 190 explicit Congruence(const Constraint& c, 191 Representation r = default_representation); 192 193 //! Destructor. 194 ~Congruence(); 195 196 //! Assignment operator. 197 Congruence& operator=(const Congruence& y); 198 199 //! Returns the current representation of *this. 200 Representation representation() const; 201 202 //! Converts *this to the specified representation. 203 void set_representation(Representation r); 204 205 //! Returns the maximum space dimension a Congruence can handle. 206 static dimension_type max_space_dimension(); 207 208 //! Returns the dimension of the vector space enclosing \p *this. 209 dimension_type space_dimension() const; 210 211 void permute_space_dimensions(const std::vector<Variable>& cycles); 212 213 //! The type of the (adapted) internal expression. 214 typedef Expression_Adapter_Transparent<Linear_Expression> expr_type; 215 //! Partial read access to the (adapted) internal expression. 216 expr_type expression() const; 217 218 //! Returns the coefficient of \p v in \p *this. 219 /*! 220 \exception std::invalid_argument thrown if the index of \p v 221 is greater than or equal to the space dimension of \p *this. 222 */ 223 Coefficient_traits::const_reference coefficient(Variable v) const; 224 225 //! Returns the inhomogeneous term of \p *this. 226 Coefficient_traits::const_reference inhomogeneous_term() const; 227 228 //! Returns a const reference to the modulus of \p *this. 229 Coefficient_traits::const_reference modulus() const; 230 231 //! Sets the modulus of \p *this to \p m . 232 //! If \p m is 0, the congruence becomes an equality. 233 void set_modulus(Coefficient_traits::const_reference m); 234 235 //! Multiplies all the coefficients, including the modulus, by \p factor . 236 void scale(Coefficient_traits::const_reference factor); 237 238 // TODO: Document this. 239 void affine_preimage(Variable v, 240 const Linear_Expression& expr, 241 Coefficient_traits::const_reference denominator); 242 243 //! Multiplies \p k into the modulus of \p *this. 244 /*! 245 If called with \p *this representing the congruence \f$ e_1 = e_2 246 \pmod{m}\f$, then it returns with *this representing 247 the congruence \f$ e_1 = e_2 \pmod{mk}\f$. 248 */ 249 Congruence& 250 operator/=(Coefficient_traits::const_reference k); 251 252 /*! \brief 253 Returns <CODE>true</CODE> if and only if \p *this is a tautology 254 (i.e., an always true congruence). 255 256 A tautological congruence has one the following two forms: 257 - an equality: \f$\sum_{i=0}^{n-1} 0 x_i + 0 == 0\f$; or 258 - a proper congruence: \f$\sum_{i=0}^{n-1} 0 x_i + b \%= 0 / m\f$, 259 where \f$b = 0 \pmod{m}\f$. 260 */ 261 bool is_tautological() const; 262 263 /*! \brief 264 Returns <CODE>true</CODE> if and only if 265 \p *this is inconsistent (i.e., an always false congruence). 266 267 An inconsistent congruence has one of the following two forms: 268 - an equality: \f$\sum_{i=0}^{n-1} 0 x_i + b == 0\f$ 269 where \f$b \neq 0\f$; or 270 - a proper congruence: \f$\sum_{i=0}^{n-1} 0 x_i + b \%= 0 / m\f$, 271 where \f$b \neq 0 \pmod{m}\f$. 272 */ 273 bool is_inconsistent() const; 274 275 //! Returns <CODE>true</CODE> if the modulus is greater than zero. 276 /*! 277 A congruence with a modulus of 0 is a linear equality. 278 */ 279 bool is_proper_congruence() const; 280 281 //! Returns <CODE>true</CODE> if \p *this is an equality. 282 /*! 283 A modulus of zero denotes a linear equality. 284 */ 285 bool is_equality() const; 286 287 //! Initializes the class. 288 static void initialize(); 289 290 //! Finalizes the class. 291 static void finalize(); 292 293 /*! \brief 294 Returns a reference to the true (zero-dimension space) congruence 295 \f$0 = 1 \pmod{1}\f$, also known as the <EM>integrality 296 congruence</EM>. 297 */ 298 static const Congruence& zero_dim_integrality(); 299 300 /*! \brief 301 Returns a reference to the false (zero-dimension space) congruence 302 \f$0 = 1 \pmod{0}\f$. 303 */ 304 static const Congruence& zero_dim_false(); 305 306 //! Returns the congruence \f$e1 = e2 \pmod{1}\f$. 307 static Congruence 308 create(const Linear_Expression& e1, const Linear_Expression& e2, 309 Representation r = default_representation); 310 311 //! Returns the congruence \f$e = n \pmod{1}\f$. 312 static Congruence 313 create(const Linear_Expression& e, Coefficient_traits::const_reference n, 314 Representation r = default_representation); 315 316 //! Returns the congruence \f$n = e \pmod{1}\f$. 317 static Congruence 318 create(Coefficient_traits::const_reference n, const Linear_Expression& e, 319 Representation r = default_representation); 320 321 /*! \brief 322 Returns a lower bound to the total size in bytes of the memory 323 occupied by \p *this. 324 */ 325 memory_size_type total_memory_in_bytes() const; 326 327 //! Returns the size in bytes of the memory managed by \p *this. 328 memory_size_type external_memory_in_bytes() const; 329 330 //! Checks if all the invariants are satisfied. 331 bool OK() const; 332 333 PPL_OUTPUT_DECLARATIONS 334 335 /*! \brief 336 Loads from \p s an ASCII representation of the internal 337 representation of \p *this. 338 */ 339 bool ascii_load(std::istream& s); 340 341 //! Swaps \p *this with \p y. 342 void m_swap(Congruence& y); 343 344 //! Copy-constructs with the specified space dimension. 345 /*! 346 \note The new Congruence will have the same representation as `cg', 347 not default_representation, for consistency with the copy 348 constructor. 349 */ 350 Congruence(const Congruence& cg, dimension_type new_space_dimension); 351 352 //! Copy-constructs with the specified space dimension and representation. 353 Congruence(const Congruence& cg, dimension_type new_space_dimension, 354 Representation r); 355 356 //! Copy-constructs from a constraint, with the specified space dimension 357 //! and (optional) representation. 358 Congruence(const Constraint& cg, dimension_type new_space_dimension, 359 Representation r = default_representation); 360 361 //! Constructs from Linear_Expression \p le, using modulus \p m. 362 /*! 363 Builds a congruence with modulus \p m, stealing the coefficients 364 from \p le. 365 366 \note The new Congruence will have the same representation as `le'. 367 368 \param le 369 The Linear_Expression holding the coefficients. 370 371 \param m 372 The modulus for the congruence, which must be zero or greater. 373 */ 374 Congruence(Linear_Expression& le, 375 Coefficient_traits::const_reference m, Recycle_Input); 376 377 //! Swaps the coefficients of the variables \p v1 and \p v2 . 378 void swap_space_dimensions(Variable v1, Variable v2); 379 380 //! Sets the space dimension by \p n , adding or removing coefficients as 381 //! needed. 382 void set_space_dimension(dimension_type n); 383 384 //! Shift by \p n positions the coefficients of variables, starting from 385 //! the coefficient of \p v. This increases the space dimension by \p n. 386 void shift_space_dimensions(Variable v, dimension_type n); 387 388 //! Normalizes the signs. 389 /*! 390 The signs of the coefficients and the inhomogeneous term are 391 normalized, leaving the first non-zero homogeneous coefficient 392 positive. 393 */ 394 void sign_normalize(); 395 396 //! Normalizes signs and the inhomogeneous term. 397 /*! 398 Applies sign_normalize, then reduces the inhomogeneous term to the 399 smallest possible positive number. 400 */ 401 void normalize(); 402 403 //! Calls normalize, then divides out common factors. 404 /*! 405 Strongly normalized Congruences have equivalent semantics if and 406 only if they have the same syntax (as output by operator<<). 407 */ 408 void strong_normalize(); 409 410 private: 411 /*! \brief 412 Holds (between class initialization and finalization) a pointer to 413 the false (zero-dimension space) congruence \f$0 = 1 \pmod{0}\f$. 414 */ 415 static const Congruence* zero_dim_false_p; 416 417 /*! \brief 418 Holds (between class initialization and finalization) a pointer to 419 the true (zero-dimension space) congruence \f$0 = 1 \pmod{1}\f$, 420 also known as the <EM>integrality congruence</EM>. 421 */ 422 static const Congruence* zero_dim_integrality_p; 423 424 Linear_Expression expr; 425 426 Coefficient modulus_; 427 428 /*! \brief 429 Returns <CODE>true</CODE> if \p *this is equal to \p cg in 430 dimension \p v. 431 */ 432 bool is_equal_at_dimension(Variable v, 433 const Congruence& cg) const; 434 435 /*! \brief 436 Throws a <CODE>std::invalid_argument</CODE> exception containing 437 error message \p message. 438 */ 439 void 440 throw_invalid_argument(const char* method, const char* message) const; 441 442 /*! \brief 443 Throws a <CODE>std::invalid_argument</CODE> exception containing 444 the appropriate error message. 445 */ 446 void 447 throw_dimension_incompatible(const char* method, 448 const char* v_name, 449 Variable v) const; 450 451 friend bool 452 operator==(const Congruence& x, const Congruence& y); 453 454 friend bool 455 operator!=(const Congruence& x, const Congruence& y); 456 457 friend class Scalar_Products; 458 friend class Grid; 459 }; 460 461 namespace Parma_Polyhedra_Library { 462 463 namespace IO_Operators { 464 465 //! Output operators. 466 467 /*! \relates Parma_Polyhedra_Library::Congruence */ 468 std::ostream& 469 operator<<(std::ostream& s, const Congruence& c); 470 471 } // namespace IO_Operators 472 473 //! Returns the congruence \f$e1 = e2 \pmod{1}\f$. 474 /*! \relates Congruence */ 475 Congruence 476 operator%=(const Linear_Expression& e1, const Linear_Expression& e2); 477 478 //! Returns the congruence \f$e = n \pmod{1}\f$. 479 /*! \relates Congruence */ 480 Congruence 481 operator%=(const Linear_Expression& e, Coefficient_traits::const_reference n); 482 483 //! Returns a copy of \p cg, multiplying \p k into the copy's modulus. 484 /*! 485 If \p cg represents the congruence \f$ e_1 = e_2 486 \pmod{m}\f$, then the result represents the 487 congruence \f$ e_1 = e_2 \pmod{mk}\f$. 488 \relates Congruence 489 */ 490 Congruence 491 operator/(const Congruence& cg, Coefficient_traits::const_reference k); 492 493 //! Creates a congruence from \p c, with \p m as the modulus. 494 /*! \relates Congruence */ 495 Congruence 496 operator/(const Constraint& c, Coefficient_traits::const_reference m); 497 498 /*! \relates Congruence */ 499 void 500 swap(Congruence& x, Congruence& y); 501 502 } // namespace Parma_Polyhedra_Library 503 504 #include "Congruence_inlines.hh" 505 506 #endif // !defined(PPL_Congruence_defs_hh) 507