A linear congruence. More...

#include <ppl.hh>

Public Types
typedef Expression_Adapter_Transparent< Linear_Expression >	expr_type
	The type of the (adapted) internal expression.

Public Member Functions
	Congruence (Representation r=default_representation)
	Constructs the 0 = 0 congruence with space dimension `0` .

	Congruence (const Congruence &cg)
	Ordinary copy constructor. More...

	Congruence (const Congruence &cg, Representation r)
	Copy constructor with specified representation.

	Congruence (const Constraint &c, Representation r=default_representation)
	Copy-constructs (modulo 0) from equality constraint `c`. More...

	~Congruence ()
	Destructor.

Congruence &	operator= (const Congruence &y)
	Assignment operator.

Representation	representation () const
	Returns the current representation of *this.

void	set_representation (Representation r)
	Converts *this to the specified representation.

dimension_type	space_dimension () const
	Returns the dimension of the vector space enclosing `*this`.

expr_type	expression () const
	Partial read access to the (adapted) internal expression.

Coefficient_traits::const_reference	coefficient (Variable v) const
	Returns the coefficient of `v` in `*this`. More...

Coefficient_traits::const_reference	inhomogeneous_term () const
	Returns the inhomogeneous term of `*this`.

Coefficient_traits::const_reference	modulus () const
	Returns a const reference to the modulus of `*this`.

void	set_modulus (Coefficient_traits::const_reference m)

void	scale (Coefficient_traits::const_reference factor)
	Multiplies all the coefficients, including the modulus, by `factor` .

Congruence &	operator/= (Coefficient_traits::const_reference k)
	Multiplies `k` into the modulus of `*this`. More...

bool	is_tautological () const
	Returns `true` if and only if `*this` is a tautology (i.e., an always true congruence). More...

bool	is_inconsistent () const
	Returns `true` if and only if `*this` is inconsistent (i.e., an always false congruence). More...

bool	is_proper_congruence () const
	Returns `true` if the modulus is greater than zero. More...

bool	is_equality () const
	Returns `true` if `*this` is an equality. More...

memory_size_type	total_memory_in_bytes () const
	Returns a lower bound to the total size in bytes of the memory occupied by `*this`.

memory_size_type	external_memory_in_bytes () const
	Returns the size in bytes of the memory managed by `*this`.

bool	OK () const
	Checks if all the invariants are satisfied.

void	ascii_dump () const
	Writes to `std::cerr` an ASCII representation of `*this`.

void	ascii_dump (std::ostream &s) const
	Writes to `s` an ASCII representation of `*this`.

void	print () const
	Prints `*this` to `std::cerr` using `operator<<`.

bool	ascii_load (std::istream &s)
	Loads from `s` an ASCII representation of the internal representation of `*this`.

void	m_swap (Congruence &y)
	Swaps `*this` with `y`.

	Congruence (const Congruence &cg, dimension_type new_space_dimension)
	Copy-constructs with the specified space dimension. More...

	Congruence (const Congruence &cg, dimension_type new_space_dimension, Representation r)
	Copy-constructs with the specified space dimension and representation.

	Congruence (const Constraint &cg, dimension_type new_space_dimension, Representation r=default_representation)

	Congruence (Linear_Expression &le, Coefficient_traits::const_reference m, Recycle_Input)
	Constructs from Linear_Expression `le`, using modulus `m`. More...

void	swap_space_dimensions (Variable v1, Variable v2)
	Swaps the coefficients of the variables `v1` and `v2` .

void	set_space_dimension (dimension_type n)

void	shift_space_dimensions (Variable v, dimension_type n)

void	sign_normalize ()
	Normalizes the signs. More...

void	normalize ()
	Normalizes signs and the inhomogeneous term. More...

void	strong_normalize ()
	Calls normalize, then divides out common factors. More...

Static Public Member Functions
static dimension_type	max_space_dimension ()
	Returns the maximum space dimension a Congruence can handle.

static void	initialize ()
	Initializes the class.

static void	finalize ()
	Finalizes the class.

static const Congruence &	zero_dim_integrality ()
	Returns a reference to the true (zero-dimension space) congruence $0 = 1 \pmod{1}$ , also known as the integrality congruence.

static const Congruence &	zero_dim_false ()
	Returns a reference to the false (zero-dimension space) congruence $0 = 1 \pmod{0}$ .

static Congruence	create (const Linear_Expression &e1, const Linear_Expression &e2, Representation r=default_representation)
	Returns the congruence $e1 = e2 \pmod{1}$ .

static Congruence	create (const Linear_Expression &e, Coefficient_traits::const_reference n, Representation r=default_representation)
	Returns the congruence $e = n \pmod{1}$ .

static Congruence	create (Coefficient_traits::const_reference n, const Linear_Expression &e, Representation r=default_representation)
	Returns the congruence $n = e \pmod{1}$ .

Static Public Attributes
static const Representation	default_representation = SPARSE
	The representation used for new Congruences. More...

Related Functions
(Note that these are not member functions.)
bool	operator== (const Congruence &x, const Congruence &y)
	Returns `true` if and only if `x` and `y` are equivalent. More...

bool	operator!= (const Congruence &x, const Congruence &y)
	Returns `false` if and only if `x` and `y` are equivalent. More...

std::ostream &	operator<< (std::ostream &s, const Congruence &c)
	Output operators. More...

Congruence	operator%= (const Linear_Expression &e1, const Linear_Expression &e2)
	Returns the congruence $e1 = e2 \pmod{1}$ . More...

Congruence	operator%= (const Linear_Expression &e, Coefficient_traits::const_reference n)
	Returns the congruence $e = n \pmod{1}$ . More...

Congruence	operator/ (const Congruence &cg, Coefficient_traits::const_reference k)
	Returns a copy of `cg`, multiplying `k` into the copy's modulus. More...

Congruence	operator/ (const Constraint &c, Coefficient_traits::const_reference m)
	Creates a congruence from `c`, with `m` as the modulus. More...

void	swap (Congruence &x, Congruence &y)

Congruence	operator%= (const Linear_Expression &e1, const Linear_Expression &e2)

Congruence	operator%= (const Linear_Expression &e, Coefficient_traits::const_reference n)

Congruence	operator/ (const Congruence &cg, Coefficient_traits::const_reference k)

Congruence	operator/ (const Constraint &c, Coefficient_traits::const_reference m)

bool	operator== (const Congruence &x, const Congruence &y)

bool	operator!= (const Congruence &x, const Congruence &y)

void	swap (Congruence &x, Congruence &y)

Detailed Description

A linear congruence.

An object of the class Congruence is a congruence:

$\cg = \sum_{i=0}^{n-1} a_i x_i + b = 0 \pmod m$

where $n$ is the dimension of the space, $a_i$ is the integer coefficient of variable $x_i$ , $b$ is the integer inhomogeneous term and $m$ is the integer modulus; if $m = 0$ , then $\cg$ represents the equality congruence $\sum_{i=0}^{n-1} a_i x_i + b = 0$ and, if $m \neq 0$ , then the congruence $\cg$ is said to be a proper congruence.

How to build a congruence: Congruences $\pmod{1}$ are typically built by applying the congruence symbol `%=' to a pair of linear expressions. Congruences with modulus m are typically constructed by building a congruence $\pmod{1}$ using the given pair of linear expressions and then adding the modulus m using the modulus symbol is `/'.

The space dimension of a congruence is defined as the maximum space dimension of the arguments of its constructor.

: In the following examples it is assumed that variables x, y and z are defined as follows:
Variable x(0);

Variable y(1);

Variable z(2);

Example 1: The following code builds the equality congruence , having space dimension :
Congruence eq_cg((3*x + 5*y - z %= 0) / 0);

The following code builds the congruence $4x = 2y - 13 \pmod{1}$ , having space dimension :
Congruence mod1_cg(4*x %= 2*y - 13);

The following code builds the congruence $4x = 2y - 13 \pmod{2}$ , having space dimension :
Congruence mod2_cg((4*x %= 2*y - 13) / 2);

An unsatisfiable congruence on the zero-dimension space $\Rset^0$ can be specified as follows:
Congruence false_cg = Congruence::zero_dim_false();

Equivalent, but more involved ways are the following:
Congruence false_cg1((Linear_Expression::zero() %= 1) / 0);

Congruence false_cg2((Linear_Expression::zero() %= 1) / 2);

In contrast, the following code defines an unsatisfiable congruence having space dimension :
Congruence false_cg3((0*z %= 1) / 0);

How to inspect a congruence: Several methods are provided to examine a congruence and extract all the encoded information: its space dimension, its modulus and the value of its integer coefficients.

Example 2: The following code shows how it is possible to access the modulus as well as each of the coefficients. Given a congruence with linear expression e and modulus m (in this case $x - 5y + 3z = 4 \pmod{5}$ ), we construct a new congruence with the same modulus m but where the linear expression is ( $2x - 10y + 6z = 8 \pmod{5}$ ).
Congruence cg1((x - 5*y + 3*z %= 4) / 5);

cout << "Congruence cg1: " << cg1 << endl;

const Coefficient& m = cg1.modulus();

if (m == 0)

cout << "Congruence cg1 is an equality." << endl;

else {

Linear_Expression e;

for (dimension_type i = cg1.space_dimension(); i-- > 0; )

e += 2 * cg1.coefficient(Variable(i)) * Variable(i);

e += 2 * cg1.inhomogeneous_term();

Congruence cg2((e %= 0) / m);

cout << "Congruence cg2: " << cg2 << endl;

}

The actual output could be the following:
Congruence cg1: A - 5*B + 3*C %= 4 / 5

Congruence cg2: 2*A - 10*B + 6*C %= 8 / 5

Note that, in general, the particular output obtained can be syntactically different from the (semantically equivalent) congruence considered.

Constructor & Destructor Documentation

Parma_Polyhedra_Library::Congruence::Congruence ( const Congruence & cg )

inline

Ordinary copy constructor.

Note: The new Congruence will have the same representation as `cg', not default_representation, so that they are indistinguishable.

Parma_Polyhedra_Library::Congruence::Congruence	(	const Constraint &	c,
		Representation	r = `default_representation`
	)

explicit

Copy-constructs (modulo 0) from equality constraint c.

Exceptions

std::invalid_argument Thrown if c is an inequality.

Parma_Polyhedra_Library::Congruence::Congruence	(	const Congruence &	cg,
		dimension_type	new_space_dimension
	)

inline

Copy-constructs with the specified space dimension.

Note: The new Congruence will have the same representation as `cg', not default_representation, for consistency with the copy constructor.

Parma_Polyhedra_Library::Congruence::Congruence	(	const Constraint &	cg,
		dimension_type	new_space_dimension,
		Representation	r = `default_representation`
	)

Copy-constructs from a constraint, with the specified space dimension and (optional) representation.

Parma_Polyhedra_Library::Congruence::Congruence	(	Linear_Expression &	le,
		Coefficient_traits::const_reference	m,
		Recycle_Input
	)

inline

Constructs from Linear_Expression le, using modulus m.

Builds a congruence with modulus m, stealing the coefficients from le.

Note: The new Congruence will have the same representation as `le'.

Parameters

le	The Linear_Expression holding the coefficients.
m	The modulus for the congruence, which must be zero or greater.

Member Function Documentation

Coefficient_traits::const_reference Parma_Polyhedra_Library::Congruence::coefficient ( Variable v ) const

inline

Returns the coefficient of v in *this.

Exceptions

std::invalid_argument thrown if the index of v is greater than or equal to the space dimension of *this.

void Parma_Polyhedra_Library::Congruence::set_modulus ( Coefficient_traits::const_reference m )

inline

Sets the modulus of *this to m . If m is 0, the congruence becomes an equality.

Congruence & Parma_Polyhedra_Library::Congruence::operator/= ( Coefficient_traits::const_reference k )

inline

Multiplies k into the modulus of *this.

If called with *this representing the congruence $e_1 = e_2 \pmod{m}$ , then it returns with *this representing the congruence $e_1 = e_2 \pmod{mk}$ .

bool Parma_Polyhedra_Library::Congruence::is_tautological ( ) const

Returns true if and only if *this is a tautology (i.e., an always true congruence).

A tautological congruence has one the following two forms:

an equality: $\sum_{i=0}^{n-1} 0 x_i + 0 == 0$ ; or
a proper congruence: $\sum_{i=0}^{n-1} 0 x_i + b \%= 0 / m$ , where $b = 0 \pmod{m}$ .

bool Parma_Polyhedra_Library::Congruence::is_inconsistent ( ) const

Returns true if and only if *this is inconsistent (i.e., an always false congruence).

An inconsistent congruence has one of the following two forms:

an equality: $\sum_{i=0}^{n-1} 0 x_i + b == 0$ where $b \neq 0$ ; or
a proper congruence: $\sum_{i=0}^{n-1} 0 x_i + b \%= 0 / m$ , where $b \neq 0 \pmod{m}$ .

bool Parma_Polyhedra_Library::Congruence::is_proper_congruence ( ) const

inline

Returns true if the modulus is greater than zero.

A congruence with a modulus of 0 is a linear equality.

bool Parma_Polyhedra_Library::Congruence::is_equality ( ) const

inline

Returns true if *this is an equality.

A modulus of zero denotes a linear equality.

void Parma_Polyhedra_Library::Congruence::set_space_dimension ( dimension_type n )

inline

Sets the space dimension by n , adding or removing coefficients as needed.

void Parma_Polyhedra_Library::Congruence::shift_space_dimensions	(	Variable	v,
		dimension_type	n
	)

inline

Shift by n positions the coefficients of variables, starting from the coefficient of v. This increases the space dimension by n.

void Parma_Polyhedra_Library::Congruence::sign_normalize ( )

Normalizes the signs.

The signs of the coefficients and the inhomogeneous term are normalized, leaving the first non-zero homogeneous coefficient positive.

void Parma_Polyhedra_Library::Congruence::normalize ( )

Normalizes signs and the inhomogeneous term.

Applies sign_normalize, then reduces the inhomogeneous term to the smallest possible positive number.

void Parma_Polyhedra_Library::Congruence::strong_normalize ( )

Calls normalize, then divides out common factors.

Strongly normalized Congruences have equivalent semantics if and only if they have the same syntax (as output by operator<<).

Friends And Related Function Documentation

bool operator==	(	const Congruence &	x,
		const Congruence &	y
	)

bool operator!=	(	const Congruence &	x,
		const Congruence &	y
	)

std::ostream & operator<<	(	std::ostream &	s,
		const Congruence &	c
	)

Congruence operator%=	(	const Linear_Expression &	e1,
		const Linear_Expression &	e2
	)

Congruence operator%=	(	const Linear_Expression &	e,
		Coefficient_traits::const_reference	n
	)

Congruence operator/	(	const Congruence &	cg,
		Coefficient_traits::const_reference	k
	)

If cg represents the congruence $e_1 = e_2 \pmod{m}$ , then the result represents the congruence $e_1 = e_2 \pmod{mk}$ .

Congruence operator/	(	const Constraint &	c,
		Coefficient_traits::const_reference	m
	)

void swap	(	Congruence &	x,
		Congruence &	y
	)

Congruence operator%=	(	const Linear_Expression &	e1,
		const Linear_Expression &	e2
	)

Congruence operator%=	(	const Linear_Expression &	e,
		Coefficient_traits::const_reference	n
	)

Congruence operator/	(	const Congruence &	cg,
		Coefficient_traits::const_reference	k
	)

Congruence operator/	(	const Constraint &	c,
		Coefficient_traits::const_reference	m
	)

bool operator==	(	const Congruence &	x,
		const Congruence &	y
	)

bool operator!=	(	const Congruence &	x,
		const Congruence &	y
	)

void swap	(	Congruence &	x,
		Congruence &	y
	)

const Representation Parma_Polyhedra_Library::Congruence::default_representation = SPARSE

static

The representation used for new Congruences.

Note: The copy constructor and the copy constructor with specified size use the representation of the original object, so that it is indistinguishable from the original object.

The documentation for this class was generated from the following file:

ppl.hh

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Related Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation